In your example, none of the annotations are attached to a statement. The requires
and the ensures
are part of a function contract and are attached to the function g
, not to any statement of g
.
An annotation that would be attached to a statement would for instance be /*@ assert x == 150; */
after the line x=x+50;
.
If I modify condi.c
to insert this assertion, then with the same commandline, I get:
Empty List Empty List Empty List Empty List Number of Annotations: 1 -> s1 Empty List Empty List Empty List Empty List Empty List Empty List Empty List
It seems that your script is working as expected, for a value of “expected” that corresponds to printing annotations attached to statements.