| View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
| ID | Project | Category | View Status | Date Submitted | Last Update | ||||
|---|---|---|---|---|---|---|---|---|---|
| 0001696 | Frama-C | Plug-in > E-ACSL | public | 2014-03-14 01:40 | 2014-09-15 17:20 | ||||
| Reporter | ploc | ||||||||
| Assigned To | signoles | ||||||||
| Priority | normal | Severity | minor | Reproducibility | always | ||||
| Status | closed | Resolution | fixed | ||||||
| Product Version | |||||||||
| Target Version | Fixed in Version | Frama-C Neon-20140301 | |||||||
| Summary | 0001696: warning: E_ACSL function 'initialize' called with null pointer - seems to affect the behavior | ||||||||
| Description | The file cpt.c contains a function. cpt.c alone is instrumented with e-acsl. Then the main.c file calls this instrumented function. When running the obtained binary, it prints this warning. | ||||||||
| Steps To Reproduce | Run the script run.me | ||||||||
| Tags | No tags attached. | ||||||||
| Attached Files |
| ||||||||
 Relationships |
|
 Relationships |
| Notes |
|
|
signoles (manager) 2014-03-14 15:55 |
Your example is not standalone: 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. [kernel] user error: failed to run: gcc -C -E -I. -DE_ACSL_MACHDEP=x86_64 -I/usr/local/share/frama-c/libc -o ' Could you provide the missing file? |
|
ploc (reporter) 2014-03-14 16:45 |
New archive with all missing files |
|
signoles (manager) 2014-03-14 16:56 |
Thanks for the new archive. I reproduced the issue. |
|
signoles (manager) 2014-03-26 17:24 |
There is actually no bug in E-ACSL here. You analyze a partial application in which the `main` is missing. This `main` initializes the variable `main_mem` which was unknown when running E-ACSL but which must be monitored. So the instrumentation is incomplete because the `main` should be modified to monitor this variable. That is why you get the warning at runtime. If you provide the file main.c when running E-ACSL, there is no issue (after applying the workaround of bts 0001695). Arguably, the documentation could be clarified. That is why I don't close this BTS entry. |
|
signoles (manager) 2014-08-04 16:11 |
Manual was clarified. |
|
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:40 | ploc | New Issue | |
| 2014-03-14 01:40 | ploc | Status | new => assigned |
| 2014-03-14 01:40 | ploc | Assigned To | => signoles |
| 2014-03-14 01:40 | ploc | File Added: initialize.tgz | |
| 2014-03-14 15:55 | signoles | Note Added: 0004957 | |
| 2014-03-14 15:55 | signoles | Status | assigned => feedback |
| 2014-03-14 16:45 | ploc | File Added: initialize.v2.tgz | |
| 2014-03-14 16:45 | ploc | Note Added: 0004961 | |
| 2014-03-14 16:45 | ploc | Status | feedback => assigned |
| 2014-03-14 16:56 | signoles | Note Added: 0004962 | |
| 2014-03-14 16:56 | signoles | Status | assigned => acknowledged |
| 2014-03-26 17:24 | signoles | Note Added: 0005014 | |
| 2014-08-04 16:11 | signoles | Note Added: 0005358 | |
| 2014-08-04 16:11 | signoles | Status | acknowledged => resolved |
| 2014-08-04 16:11 | 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: 0005462 | |
| 2014-09-15 17:20 | signoles | Status | resolved => closed |
| Issue History |