Frama-C Bug Tracking System - Frama-C
View Issue Details
0001289Frama-CPlug-in > aoraïpublic2012-10-25 18:432014-03-13 15:57
Jochen 
virgile 
normalcrashalways
closedfixed 
Frama-C Oxygen-20120901 
Frama-C Neon-20140301 
0001289: aorai causes failed assertion
Running "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.
No tags attached.
c ftest.c (93) 2012-10-25 18:43
https://bts.frama-c.com/file_download.php?file_id=434&type=bug
? ftest.ya (66) 2012-10-25 18:43
https://bts.frama-c.com/file_download.php?file_id=435&type=bug
txt log.txt (1,795) 2012-10-25 18:44
https://bts.frama-c.com/file_download.php?file_id=436&type=bug
Issue History
2012-10-25 18:43JochenNew Issue
2012-10-25 18:43JochenStatusnew => assigned
2012-10-25 18:43JochenAssigned To => virgile
2012-10-25 18:43JochenFile Added: ftest.c
2012-10-25 18:43JochenFile Added: ftest.ya
2012-10-25 18:44JochenFile Added: log.txt
2012-10-26 15:56virgileStatusassigned => acknowledged
2013-07-26 11:30svnCheckin
2013-07-26 11:30svnStatusacknowledged => resolved
2013-07-26 11:30svnResolutionopen => fixed
2013-07-26 11:37virgileNote Added: 0004010
2014-03-13 15:56signolesFixed in Version => Frama-C Neon-20140301
2014-03-13 15:57signolesStatusresolved => closed

Notes
(0004010)
virgile   
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;