Notes |
|
|
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 |
|
|
|
Thanks for the new archive. I reproduced the issue. |
|
|
|
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. |
|
|
|
|
|
|
|