Frama-C Bug Tracking System - Frama-C
View Issue Details
0002134Frama-CKernel > ACSL implementationpublic2015-06-12 18:262015-06-12 18:26
gaggarwal 
virgile 
normalminorhave not tried
assignedopen 
Frama-C Neon-20140301 
 
0002134: Weak and Strong Invariants are not supported
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.
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'
No tags attached.
Issue History
2015-06-12 18:26gaggarwalNew Issue
2015-06-12 18:26gaggarwalStatusnew => assigned
2015-06-12 18:26gaggarwalAssigned To => virgile

There are no notes attached to this issue.