Weak and Strong Invariants are not supported
ID0002134: This issue was created automatically from Mantis Issue 2134. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002134 | Frama-C | Kernel > ACSL implementation | public | 2015-06-12 | 2015-06-12 |
| Reporter | gaggarwal | Assigned To | virgile | Resolution | open |
| Priority | normal | Severity | minor | Reproducibility | have not tried |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Neon-20140301 | Target Version | - | Fixed in Version | - |
Description :
ACSL manual version 1.8, in Figure 2.23 explains grammar of data-invariant and type-invariant. Section 2.11(Data invariants) explains the difference between between strong and weak invariants.
I tried running the example manual have for strong invariant in the same section. But it seems like weak and strong invariants are not supported and ACSL parser is not able to parse the invariants with inv-strength.
Steps To Reproduce :
I used example ACSL manual version 1.8 have :
int a; //@ global invariant a_is_positive: a >= 0 ;
typedef double temperature; /@ strong type invariant temp_in_celsius(temperature t) = @ t >= -273.15 ; @/
struct S { int f; };
//@ type invariant S_f_is_positive(struct S s) = s.f >= 0 ;
Ran "frama-c -wp file.c" command and got following kernel error:
file.c:5:[kernel] user error: unexpected token 'type'