2021-03-02 01:54 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001289Frama-CPlug-in > aoraïpublic2014-03-13 15:57
ReporterJochen 
Assigned Tovirgile 
PrioritynormalSeveritycrashReproducibilityalways
StatusclosedResolutionfixed 
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 Files
  • c file icon ftest.c (93 bytes) 2012-10-25 18:43 -
    void a(void) {}
    
    void main(void)
    {
    	//@ loop assigns i;
    	for (int i=0; i<10; ++i)
    		a();
    }
    
    
    c file icon ftest.c (93 bytes) 2012-10-25 18:43 +
  • ? file icon ftest.ya (66 bytes) 2012-10-25 18:43
  • txt file icon log.txt (1,795 bytes) 2012-10-25 18:44 -
    [kernel] preprocessing with "gcc -C -E -I.  ftest.c"
    [aorai] Welcome to the Aorai plugin
    [kernel] The full backtrace is:
             Raised at file "cil/src/cil_datatype.ml", line 339, characters 17-29
             Called from file "src/aorai/aorai_dataflow.ml", line 470, characters 44-79
             Called from file "src/aorai/aorai_dataflow.ml", line 517, characters 9-53
             Called from file "src/aorai/aorai_dataflow.ml", line 862, characters 2-20
             Called from file "src/aorai/aorai_register.ml", line 303, characters 10-35
             Called from file "src/project/project.ml", line 367, characters 12-15
             Called from file "src/project/project.ml", line 372, characters 17-22
             Re-raised at file "src/project/project.ml", line 372, characters 56-57
             Called from file "src/aorai/aorai_register.ml", line 372, characters 4-31
             Called from file "src/project/state_builder.ml", line 812, characters 9-13
             Re-raised at file "src/project/state_builder.ml", line 820, characters 15-18
             Called from file "queue.ml", line 135, characters 6-20
             Called from file "src/kernel/boot.ml", line 38, characters 4-20
             Called from file "src/kernel/cmdline.ml", line 720, characters 2-9
             Called from file "src/kernel/cmdline.ml", line 197, characters 4-8
             
             Unexpected error (File "cil/src/cil_datatype.ml", line 339, characters 17-23: Assertion failed).
             Please report as 'crash' at http://bts.frama-c.com/.
             Your Frama-C version is Oxygen-20120901.
             Note that a version and a backtrace alone often do not contain enough
             information to understand the bug. Guidelines for reporting bugs are at:
             http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines
    
    txt file icon log.txt (1,795 bytes) 2012-10-25 18:44 +

-Relationships
+Relationships

-Notes

~0004010

virgile (developer)

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;
+Notes

-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
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
+Issue History