type invariants
ID0000025: This issue was created automatically from Mantis Issue 25. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000025 | Frama-C | Plug-in > jessie | public | 2009-04-07 | 2009-09-21 |
| Reporter | virgile | Assigned To | virgile | Resolution | open |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Lithium-20081201 | Target Version | - | Fixed in Version | - |
Description :
(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
Additional Information :
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