Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000025Frama-CPlug-in > jessiepublic2009-04-07 13:572009-09-21 10:44
Reportervirgile 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityalways
StatusacknowledgedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C Lithium-20081201 
Target VersionFixed in Version 
Summary0000025: type invariants
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 InformationThere 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
TagsNo tags attached.
Attached Files

- Relationships
has duplicate 0000252assignedvirgile type invariants 

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2009-04-07 13:57 virgile New Issue
2009-04-07 15:43 signoles Status new => acknowledged
2009-04-10 10:04 signoles Status acknowledged => assigned
2009-04-10 10:04 signoles Assigned To => virgile
2009-09-21 10:44 signoles Status assigned => acknowledged
2012-01-21 10:50 signoles Relationship added has duplicate 0000252


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker