Frama-C Bug Tracking System - Frama-C
View Issue Details
0001717Frama-CPlug-in > E-ACSLpublic2014-03-25 10:482014-09-15 17:20
arvidj 
signoles 
normalminoralways
closedfixed 
 
Frama-C Neon-20140301 
0001717: Instrumentation of statements with labels are not inserted at the correct location
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.
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
No tags attached.
c bug-annotation-after-label.c (289) 2014-03-25 10:48
https://bts.frama-c.com/file_download.php?file_id=708&type=bug
Issue History
2014-03-25 10:48arvidjNew Issue
2014-03-25 10:48arvidjStatusnew => assigned
2014-03-25 10:48arvidjAssigned To => signoles
2014-03-25 10:48arvidjFile Added: bug-annotation-after-label.c
2014-03-27 08:56signolesStatusassigned => confirmed
2014-03-28 14:57signolesStatusconfirmed => resolved
2014-03-28 14:57signolesResolutionopen => fixed
2014-09-15 17:20signolesFixed in Version => Frama-C Neon-20140301
2014-09-15 17:20signolesNote Added: 0005459
2014-09-15 17:20signolesStatusresolved => closed

Notes
(0005459)
signoles   
2014-09-15 17:20   
Fixed in E-ACSL v0.4.1.