Verifying global variable

[Bo C]

Hi VeriFast team:

I try to use VeriFast to verify global variables in  a C program. I notice that there is a example on https://people.cs.kuleuven.be/~bart.jacobs/verifast/examples/globals.c.html

However, when I use Vfide to verify globals.c, VeriFast complains that: "No such variable, constructor, regular function, predicate, enum element, global variable, or module: globals".

How can I solve this problem?

Sincerely,

Owen