2021-03-01 05:41 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001290Frama-CPlug-in > aoraïpublic2014-02-12 16:58
ReporterJochen 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
Product VersionFrama-C Oxygen-20120901 
Target VersionFixed in VersionFrama-C Fluorine-20130401 
Summary0001290: aorai doesn't enrich user's "loop assigns" by generated internal variables
DescriptionRunning "frama-c ftest.c -aorai-automata ftest.ya" on the attached files yields an annotated file "ftest_annot.c" (also attached) with a wrong "loop assigns" clause. In line 74, the user-given clause (from line 3 of "ftest.c") is just copied, while the assignment to the generated variable "aorai_Loop_Init_11" in line 78 should lead to the inclusion of that variable into the loop assigns clause.
TagsNo tags attached.
Attached Files
  • c file icon ftest.c (71 bytes) 2012-10-25 19:00 -
    void main(void)
    {
    	//@ loop assigns i;
    	for (int i=0; i<10; ++i)
    		;
    }
    
    c file icon ftest.c (71 bytes) 2012-10-25 19:00 +
  • ? file icon ftest.ya (33 bytes) 2012-10-25 19:00
  • c file icon ftest_annot.c (1,773 bytes) 2012-10-25 19:01 -
    /* Generated by Frama-C */
    //****************
    //* BEGIN Primitives generated for LTL verification
    //* 
    //* 
    //* Some constants
    enum aorai_ListOper {
        op_main = 0
    };
    enum aorai_ListOper aorai_CurOperation = op_main;
    enum aorai_OpStatusList {
        aorai_Terminated = 1,
        aorai_Called = 0
    };
    enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called;
    //* 
    //* States and Trans Variables
    int S = 1;
    //* 
    //* Loops management
    int aorai_Loop_Init_11 = 0;
    //* 
    //****************** 
    //* Auxiliary variables used in transition conditions
    //*
    //* 
    //* END Primitives generated for LTL verification
    //****************
    /*@ ensures aorai_CurOpStatus == aorai_Called;
        ensures aorai_CurOperation == op_main;
        assigns aorai_CurOpStatus, aorai_CurOperation,
        S;
        behavior buch_state_S_in:
          assumes 1 == S;
          ensures 1 == S;
          
        behavior buch_state_S_out:
          assumes 0 == S;
          ensures 0 == S;
          
      
    */
    void main_pre_func(void);
    /*@ requires 1 == S;
        ensures aorai_CurOpStatus == aorai_Terminated;
        
        ensures aorai_CurOperation == op_main;
        assigns aorai_CurOpStatus, aorai_CurOperation,
        S;
        behavior buch_state_S_in:
          assumes 1 == S;
          ensures 1 == S;
          
        behavior buch_state_S_out:
          assumes 0 == S;
          ensures 0 == S;
          
      
    */
    void main_post_func(void);
    /*@ requires 1 == S;
        behavior Buchi_property_behavior:
          ensures \true;
          ensures 1 == S;
          
      
    */
    void main(void)
    {
      int i;
      main_pre_func();
      i = 0;
      /*@ ghost aorai_Loop_Init_11 = 1; */
      /*@ loop assigns i;
          loop invariant 1 == S; */
      while (1) {
        if (! (i < 10)) { goto while_0_break; }
        /*@ ghost aorai_Loop_Init_11 = 0; */
        i ++;
      }
      while_0_break: /* internal */ ;
      main_post_func();
      return;
    }
    
    
    
    c file icon ftest_annot.c (1,773 bytes) 2012-10-25 19:01 +

-Relationships
+Relationships

-Notes

~0004610

Fix committed to stable/neon branch.
+Notes

-Issue History
Date Modified Username Field Change
2012-10-25 19:00 Jochen New Issue
2012-10-25 19:00 Jochen Status new => assigned
2012-10-25 19:00 Jochen Assigned To => virgile
2012-10-25 19:00 Jochen File Added: ftest.c
2012-10-25 19:00 Jochen File Added: ftest.ya
2012-10-25 19:01 Jochen File Added: ftest_annot.c
2012-10-26 15:53 virgile Status assigned => acknowledged
2012-10-31 16:55 svn
2012-10-31 16:55 svn Status acknowledged => resolved
2012-10-31 16:55 svn Resolution open => fixed
2013-04-19 11:05 signoles Fixed in Version => Frama-C Fluorine
2013-04-19 11:05 signoles Status resolved => closed
2013-12-19 01:11 Source_changeset_attached => framac master e04a4382
2014-02-12 16:53 Source_changeset_attached => framac stable/neon e04a4382
2014-02-12 16:58 Note Added: 0004610
2014-02-12 16:58 Status closed => resolved
+Issue History