Frama-C Bug Tracking System - Frama-C
View Issue Details
IDProjectCategoryView StatusDate SubmittedLast Update
0001696Frama-CPlug-in > E-ACSLpublic2014-03-14 01:402014-09-15 17:20
Reporterploc 
Assigned Tosignoles 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
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 run.me
TagsNo tags attached.
Relationships
Attached Filestgz 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

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 0001695).

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.

Issue History
Date ModifiedUsernameFieldChange
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