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.