View Issue Details [ Jump to Notes ] [ Related Changesets ] | [ Issue History ] [ Print ] |
ID | Project | Category | View Status | Date Submitted | Last Update |
0001290 | Frama-C | Plug-in > aoraï | public | 2012-10-25 19:00 | 2014-02-12 16:58 |
|
Reporter | Jochen | |
Assigned To | virgile | |
Priority | normal | Severity | minor | Reproducibility | always |
Status | closed | Resolution | fixed | |
Platform | | OS | | OS Version | |
Product Version | Frama-C Oxygen-20120901 | |
Target Version | | Fixed in Version | Frama-C Fluorine-20130401 | |
|
Summary | 0001290: aorai doesn't enrich user's "loop assigns" by generated internal variables |
Description | Running "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. |
Tags | No tags attached. |
|
Attached Files | ftest.c [^] (71 bytes) 2012-10-25 19:00 [Show Content] [Hide Content]void main(void)
{
//@ loop assigns i;
for (int i=0; i<10; ++i)
;
}
ftest.ya [^] (33 bytes) 2012-10-25 19:00
ftest_annot.c [^] (1,773 bytes) 2012-10-25 19:01 [Show Content] [Hide Content]/* 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;
}
|
|