Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
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.
TagsNo tags attached.
Attached Filestgz file icon fc_stdout_gcc_error.tgz [^] (2,628 bytes) 2014-03-14 01:29
tgz file icon fc_stdout_gcc_error.v2.tgz [^] (6,114 bytes) 2014-03-14 16:45

- Relationships

-  Notes
(0004958)
signoles (manager)
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 (reporter)
2014-03-14 16:44

New archive with all required files.
(0004963)
signoles (manager)
2014-03-14 16:56

Thanks for the new archive. I reproduced the issue.
(0004964)
signoles (manager)
2014-03-14 17:16

Here is a small reproducible example:
=====
#include <stdio.h>

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 (reporter)
2014-03-14 23:41

The hack "grep -v _fc_stdout" works pretty well. The code is compiled and behave as expected.
(0005262)
signoles (manager)
2014-07-16 10:00

Have been fixed by commit cd42fcb91.
(0005463)
signoles (manager)
2014-09-15 17:20

Fixed in E-ACSL v0.4.1.

- Issue History
Date Modified Username Field Change
2014-03-14 01:29 ploc New Issue
2014-03-14 01:29 ploc Status new => assigned
2014-03-14 01:29 ploc Assigned To => signoles
2014-03-14 01:29 ploc File Added: fc_stdout_gcc_error.tgz
2014-03-14 15:56 signoles Note Added: 0004958
2014-03-14 15:56 signoles Status assigned => feedback
2014-03-14 16:44 ploc Note Added: 0004960
2014-03-14 16:44 ploc Status feedback => assigned
2014-03-14 16:45 ploc File Added: fc_stdout_gcc_error.v2.tgz
2014-03-14 16:56 signoles Note Added: 0004963
2014-03-14 16:56 signoles Status assigned => acknowledged
2014-03-14 17:16 signoles Note Added: 0004964
2014-03-14 17:16 signoles Status acknowledged => confirmed
2014-03-14 23:41 ploc Note Added: 0004968
2014-07-16 10:00 signoles Note Added: 0005262
2014-07-16 10:00 signoles Status confirmed => resolved
2014-07-16 10:00 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: 0005463
2014-09-15 17:20 signoles Status resolved => closed


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker