Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001717Frama-CPlug-in > E-ACSLpublic2014-03-25 10:482014-09-15 17:20
Reporterarvidj 
Assigned Tosignoles 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product Version 
Target VersionFixed in VersionFrama-C Neon-20140301 
Summary0001717: Instrumentation of statements with labels are not inserted at the correct location
DescriptionThe 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 ReproduceFrama-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
TagsNo tags attached.
Attached Filesc file icon bug-annotation-after-label.c [^] (289 bytes) 2014-03-25 10:48 [Show Content]

- Relationships

-  Notes
(0005459)
signoles (manager)
2014-09-15 17:20

Fixed in E-ACSL v0.4.1.

- Issue History
Date Modified Username Field Change
2014-03-25 10:48 arvidj New Issue
2014-03-25 10:48 arvidj Status new => assigned
2014-03-25 10:48 arvidj Assigned To => signoles
2014-03-25 10:48 arvidj File Added: bug-annotation-after-label.c
2014-03-27 08:56 signoles Status assigned => confirmed
2014-03-28 14:57 signoles Status confirmed => resolved
2014-03-28 14:57 signoles Resolution open => fixed
2014-09-15 17:20 signoles Fixed in Version => Frama-C Neon-20140301
2014-09-15 17:20 signoles Note Added: 0005459
2014-09-15 17:20 signoles Status resolved => closed


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker