Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
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.
Attached Filestgz file icon initialize.tgz [^] (2,980 bytes) 2014-03-14 01:40
tgz file icon initialize.v2.tgz [^] (13,761 bytes) 2014-03-14 16:45

- Relationships

-  Notes
(0004957)
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?
(0004961)
ploc (reporter)
2014-03-14 16:45

New archive with all missing files
(0004962)
signoles (manager)
2014-03-14 16:56

Thanks for the new archive. I reproduced the issue.
(0005014)
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.
(0005358)
signoles (manager)
2014-08-04 16:11

Manual was clarified.
(0005462)
signoles (manager)
2014-09-15 17:20

Fixed in E-ACSL v0.4.1.

- 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


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker