2021-01-24 23:34 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001696Frama-CPlug-in > E-ACSLpublic2014-09-15 17:20
Reporterploc 
Assigned Tosignoles 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
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 Files

-Relationships
+Relationships

-Notes

~0004957

signoles (manager)

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)

New archive with all missing files

~0004962

signoles (manager)

Thanks for the new archive. I reproduced the issue.

~0005014

signoles (manager)

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)

Manual was clarified.

~0005462

signoles (manager)

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