Frama-C Bug Tracking System - Frama-C
View Issue Details
0001696Frama-CPlug-in > E-ACSLpublic2014-03-14 01:402014-09-15 17:20
ploc 
signoles 
normalminoralways
closedfixed 
 
Frama-C Neon-20140301 
0001696: warning: E_ACSL function 'initialize' called with null pointer - seems to affect the behavior
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.
Run the script run.me
No tags attached.
tgz initialize.tgz (2,980) 2014-03-14 01:40
https://bts.frama-c.com/file_download.php?file_id=696&type=bug
tgz initialize.v2.tgz (13,761) 2014-03-14 16:45
https://bts.frama-c.com/file_download.php?file_id=698&type=bug
Issue History
2014-03-14 01:40plocNew Issue
2014-03-14 01:40plocStatusnew => assigned
2014-03-14 01:40plocAssigned To => signoles
2014-03-14 01:40plocFile Added: initialize.tgz
2014-03-14 15:55signolesNote Added: 0004957
2014-03-14 15:55signolesStatusassigned => feedback
2014-03-14 16:45plocFile Added: initialize.v2.tgz
2014-03-14 16:45plocNote Added: 0004961
2014-03-14 16:45plocStatusfeedback => assigned
2014-03-14 16:56signolesNote Added: 0004962
2014-03-14 16:56signolesStatusassigned => acknowledged
2014-03-26 17:24signolesNote Added: 0005014
2014-08-04 16:11signolesNote Added: 0005358
2014-08-04 16:11signolesStatusacknowledged => resolved
2014-08-04 16:11signolesResolutionopen => fixed
2014-09-15 17:20signolesFixed in Version => Frama-C Neon-20140301
2014-09-15 17:20signolesNote Added: 0005462
2014-09-15 17:20signolesStatusresolved => closed

Notes
(0004957)
signoles   
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?
(0004961)
ploc   
2014-03-14 16:45   
New archive with all missing files
(0004962)
signoles   
2014-03-14 16:56   
Thanks for the new archive. I reproduced the issue.
(0005014)
signoles   
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 #1695). Arguably, the documentation could be clarified. That is why I don't close this BTS entry.
(0005358)
signoles   
2014-08-04 16:11   
Manual was clarified.
(0005462)
signoles   
2014-09-15 17:20   
Fixed in E-ACSL v0.4.1.