| View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] |
| ID | Project | Category | View Status | Date Submitted | Last Update |
| 0001717 | Frama-C | Plug-in > E-ACSL | public | 2014-03-25 10:48 | 2014-09-15 17:20 |
|
| Reporter | arvidj | |
| Assigned To | signoles | |
| Priority | normal | Severity | minor | Reproducibility | always |
| Status | closed | Resolution | fixed | |
| Platform | | OS | | OS Version | |
| Product Version | | |
| Target Version | | Fixed in Version | Frama-C Neon-20140301 | |
|
| Summary | 0001717: Instrumentation of statements with labels are not inserted at the correct location |
| Description | The assertion on line 8 in the attached program fails since the call to __full_init is placed before the label on line 8, instead of after. |
| Steps To Reproduce | Frama-c run with the following parameters:
-machdep x86_64 -e-acsl bug-annotation-after-label.c -then-on e-acsl -print -ocode bug-annotation-after-label.gen.c
Compiled with the following flags:
export SHARE=`frama-c -print-share-path`
gcc -g -O0 -std=c99 -pedantic -Wall -Wno-long-long -Wno-attributes -Wno-unused-but-set-variable -fno-builtin -o bug-annotation-after-label.c.out $SHARE/e-acsl/e_acsl.c $SHARE/e-acsl/memory_model/e_acsl_bittree.c $SHARE/e-acsl/memory_model/e_acsl_mmodel.c bug-annotation-after-label.gen.c -lgmp
|
| Tags | No tags attached. |
|
| Attached Files |  bug-annotation-after-label.c [^] (289 bytes) 2014-03-25 10:48 [Show Content] [Hide Content]// weirdness with labels
int main(void) {
int a = 10, *p;
goto lbl_1;
lbl_2:
/*@ assert \valid(p); */
return 0;
// the problem is here: the call to __full_init(... p ...) is inserted
// before the label lbl_1, instead of before the assignment.
lbl_1:
p = &a;
goto lbl_2;
}
|
|
Relationships 
Relationships