Meaning of @init_class?

[Sophie Lathouwers]

Hi everyone,

I was looking at some examples for VeriFast and came across the annotation "//@ init_class();". What is the meaning of this annotation? It is used in several examples, e.g. in examples/java/prodcons/client.java. I tried looking for the meaning in the tutorial, papers, and some other sources but didn't manage to find an answer.

Thanks!
Kind regards,
Sophie Lathouwers