aorai doesn't enrich user's "loop assigns" by generated internal variables
ID0001290: This issue was created automatically from Mantis Issue 1290. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001290 | Frama-C | Plug-in > aoraï | public | 2012-10-25 | 2014-02-12 |
| Reporter | Jochen | Assigned To | virgile | Resolution | fixed |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Oxygen-20120901 | Target Version | - | Fixed in Version | Frama-C Fluorine-20130401 |
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.