Frama-C Bug Tracking System - Frama-C
View Issue Details
0001696Frama-CPlug-in > E-ACSLpublic2014-03-14 01:402014-09-15 17:20
Assigned Tosignoles 
PlatformOSOS Version
Product Version 
Target VersionFixed in VersionFrama-C Neon-20140301 
Summary0001696: warning: E_ACSL function 'initialize' called with null pointer - seems to affect the behavior
DescriptionThe 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 ReproduceRun the script
TagsNo tags attached.
Attached Filestgz initialize.tgz (2,980) 2014-03-14 01:40
tgz initialize.v2.tgz (13,761) 2014-03-14 16:45

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?
2014-03-14 16:45   
New archive with all missing files
2014-03-14 16:56   
Thanks for the new archive. I reproduced the issue.
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.
2014-08-04 16:11   
Manual was clarified.
2014-09-15 17:20   
Fixed in E-ACSL v0.4.1.

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