Frama-C Bug Tracking System - Frama-C
View Issue Details
0000025Frama-CPlug-in > jessiepublic2009-04-07 13:572009-09-21 10:44
virgile 
virgile 
normalminoralways
acknowledgedopen 
Frama-C Lithium-20081201 
 
0000025: type invariants
(bts 6836) I tried the code-example from the 1.4 ACSL document. void out_char(char c) { int col = 0; //@ global invariant I : 0 <= col <= 79; col++; if (col >= 80) col = 0; } Doing this, I get: $ frama-c -jessie-analysis -jessie-int-model exact -jessie-gui invariant.c Parsing [preprocessing] running gcc -C -E -I. -include C:\Frama-C\share\frama-c\jessie\j essie_prolog.h -D JESSIE_EXACT_INT_MODEL -dD invariant.c invariant.c[14:0-0] : syntax error Parsing error Skipping file "invariant.c" that has errors. Cleaning unused parts Symbolic link Your code cannot be parsed. Aborting analysis. Starting semantical analysis Starting Jessie translation Nothing to process. There was probably an error before. Cheers Christoph
There are two issues here: - global invariant inside function body is not implemented in current Frama-C release - the ACSL documentation states that global invariant are meant to be enforced on global data. Hence they are primarily global annotation. They can be found as code annotation when dealing with static local variables (which are in fact global variables with specific scoping rules), but they do not apply to plain local variables such as col in the example above
No tags attached.
has duplicate 0000252assigned virgile type invariants 
Issue History
2009-04-07 13:57virgileNew Issue
2009-04-07 15:43signolesStatusnew => acknowledged
2009-04-10 10:04signolesStatusacknowledged => assigned
2009-04-10 10:04signolesAssigned To => virgile
2009-09-21 10:44signolesStatusassigned => acknowledged
2012-01-21 10:50signolesRelationship addedhas duplicate 0000252

There are no notes attached to this issue.