0001696: warning: E_ACSL function 'initialize' called with null pointer - seems to affect the behavior

(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 #1695). 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

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 #1695). 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.

Relationships