Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001289Frama-CPlug-in > aoraïpublic2012-10-25 18:432014-03-13 15:57
ReporterJochen 
Assigned Tovirgile 
PrioritynormalSeveritycrashReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Oxygen-20120901 
Target VersionFixed in VersionFrama-C Neon-20140301 
Summary0001289: aorai causes failed assertion
DescriptionRunning "frama-c ftest.c -aorai-automata ftest.ya" on the attached program causes an unexpectyed error in file cil_datatype.ml; see attached stdout log.
TagsNo tags attached.
Attached Filesc file icon ftest.c [^] (93 bytes) 2012-10-25 18:43 [Show Content]
? file icon ftest.ya [^] (66 bytes) 2012-10-25 18:43
txt file icon log.txt [^] (1,795 bytes) 2012-10-25 18:44 [Show Content]

- Relationships

-  Notes
(0004010)
virgile (developer)
2013-07-26 11:37

Note that the code does not conform to the automaton, because the automaton do not keep track of call and return to main. A conforming automaton ensuring that a is called an even number of times would be

%init: init;
%accept: S;
init: { CALL(main) } -> S;
S: { a() } -> T
 | { RETURN(main) } -> S;
T: { a() } -> S;

- Issue History
Date Modified Username Field Change
2012-10-25 18:43 Jochen New Issue
2012-10-25 18:43 Jochen Status new => assigned
2012-10-25 18:43 Jochen Assigned To => virgile
2012-10-25 18:43 Jochen File Added: ftest.c
2012-10-25 18:43 Jochen File Added: ftest.ya
2012-10-25 18:44 Jochen File Added: log.txt
2012-10-26 15:56 virgile Status assigned => acknowledged
2013-07-26 11:30 svn Checkin
2013-07-26 11:30 svn Status acknowledged => resolved
2013-07-26 11:30 svn Resolution open => fixed
2013-07-26 11:37 virgile Note Added: 0004010
2014-03-13 15:56 signoles Fixed in Version => Frama-C Neon-20140301
2014-03-13 15:57 signoles Status resolved => closed


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker