Frama-C Bug Tracking System - Frama-C
View Issue Details
IDProjectCategoryView StatusDate SubmittedLast Update
0001695Frama-CPlug-in > E-ACSLpublic2014-03-14 01:292014-09-15 17:20
Reporterploc 
Assigned Tosignoles 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product Version 
Target VersionFixed in VersionFrama-C Neon-20140301 
Summary0001695: Impossible to compile the eacsl produced source
DescriptionThis code is generated. It is compilable. However when instrumented on a part of the code, gcc is not anymore able to compile it: /tmp/cc3Hv08h.o: In function `__e_acsl_memory_init': test4.c:(.text+0x43c): undefined reference to `__fc_stdout' /tmp/cc3Hv08h.o: In function `main': test4.c:(.text+0x52b): undefined reference to `__fc_stdout' collect2: error: ld returned 1 exit status Same behavior when applied on all the code.
Steps To ReproduceRun the run.me script.
Additional Information
TagsNo tags attached.
Relationships
Attached Filestgz fc_stdout_gcc_error.tgz (2,628) 2014-03-14 01:29
https://bts.frama-c.com/file_download.php?file_id=695&type=bug
tgz fc_stdout_gcc_error.v2.tgz (6,114) 2014-03-14 16:45
https://bts.frama-c.com/file_download.php?file_id=699&type=bug
Issue History
Date ModifiedUsernameFieldChange
2014-03-14 01:29plocNew Issue
2014-03-14 01:29plocStatusnew => assigned
2014-03-14 01:29plocAssigned To => signoles
2014-03-14 01:29plocFile Added: fc_stdout_gcc_error.tgz
2014-03-14 15:56signolesNote Added: 0004958
2014-03-14 15:56signolesStatusassigned => feedback
2014-03-14 16:44plocNote Added: 0004960
2014-03-14 16:44plocStatusfeedback => assigned
2014-03-14 16:45plocFile Added: fc_stdout_gcc_error.v2.tgz
2014-03-14 16:56signolesNote Added: 0004963
2014-03-14 16:56signolesStatusassigned => acknowledged
2014-03-14 17:16signolesNote Added: 0004964
2014-03-14 17:16signolesStatusacknowledged => confirmed
2014-03-14 23:41plocNote Added: 0004968
2014-07-16 10:00signolesNote Added: 0005262
2014-07-16 10:00signolesStatusconfirmed => resolved
2014-07-16 10:00signolesResolutionopen => fixed
2014-09-15 17:20signolesFixed in Version => Frama-C Neon-20140301
2014-09-15 17:20signolesNote Added: 0005463
2014-09-15 17:20signolesStatusresolved => closed

Notes
(0004958)
signoles   
2014-03-14 15:56   
Your example is not standalone: Generating non instrumented binary In file included from cpt.c:3:0: cpt.h:9:46: fatal error: /usr/local/include/lustrec/arrow.h: No such file or directory compilation terminated. cpt_cpt.c:3:52: fatal error: /usr/local/include/lustrec/io_frontend.h: No such file or directory compilation terminated. Could you provide the missing files?
(0004960)
ploc   
2014-03-14 16:44   
New archive with all required files.
(0004963)
signoles   
2014-03-14 16:56   
Thanks for the new archive. I reproduced the issue.
(0004964)
signoles   
2014-03-14 17:16   
Here is a small reproducible example: ===== #include int main(void) { int x = 2; printf("x = %d\n", x); return 0; } ===== The issue comes from using some functions of stdio.h and the way they are defined in the Frama-C libc library..
(0004968)
ploc   
2014-03-14 23:41   
The hack "grep -v _fc_stdout" works pretty well. The code is compiled and behave as expected.
(0005262)
signoles   
2014-07-16 10:00   
Have been fixed by commit cd42fcb91.
(0005463)
signoles   
2014-09-15 17:20   
Fixed in E-ACSL v0.4.1.