Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002134Frama-CKernel > ACSL implementationpublic2015-06-12 18:262015-06-12 18:26
Reportergaggarwal 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityhave not tried
StatusassignedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C Neon-20140301 
Target VersionFixed in Version 
Summary0002134: Weak and Strong Invariants are not supported
DescriptionACSL 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 ReproduceI 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'
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2015-06-12 18:26 gaggarwal New Issue
2015-06-12 18:26 gaggarwal Status new => assigned
2015-06-12 18:26 gaggarwal Assigned To => virgile


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker