| View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
| ID | Project | Category | View Status | Date Submitted | Last Update | ||||
|---|---|---|---|---|---|---|---|---|---|
| 0001695 | Frama-C | Plug-in > E-ACSL | public | 2014-03-14 01:29 | 2014-09-15 17:20 | ||||
| Reporter | ploc | ||||||||
| Assigned To | signoles | ||||||||
| Priority | normal | Severity | major | Reproducibility | always | ||||
| Status | closed | Resolution | fixed | ||||||
| Product Version | |||||||||
| Target Version | Fixed in Version | Frama-C Neon-20140301 | |||||||
| Summary | 0001695: Impossible to compile the eacsl produced source | ||||||||
| Description | This 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 Reproduce | Run the run.me script. | ||||||||
| Tags | No tags attached. | ||||||||
| Attached Files |
| ||||||||
 Relationships |
|
 Relationships |
| Notes |
|
|
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? |
|
ploc (reporter) 2014-03-14 16:44 |
New archive with all required files. |
|
signoles (manager) 2014-03-14 16:56 |
Thanks for the new archive. I reproduced the issue. |
|
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.. |
|
ploc (reporter) 2014-03-14 23:41 |
The hack "grep -v _fc_stdout" works pretty well. The code is compiled and behave as expected. |
|
signoles (manager) 2014-07-16 10:00 |
Have been fixed by commit cd42fcb91. |
|
signoles (manager) 2014-09-15 17:20 |
Fixed in E-ACSL v0.4.1. |
| Notes |
| 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-03-25 14:17 | signoles | Source_changeset_attached | => e-acsl master ebc816d8 |
| 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 |
| Issue History |