0001695: Impossible to compile the eacsl produced source

(0004958)
signoles (manager)
2014-03-14 15:56

Your example is not standalone:

Generating non instrumented binary
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.
cpt_cpt.c:3:52: fatal error: /usr/local/include/lustrec/io_frontend.h: No such file or directory
compilation terminated.

Could you provide the missing files?

(0004960)
ploc (reporter)
2014-03-14 16:44

New archive with all required files.

(0004963)
signoles (manager)
2014-03-14 16:56

Thanks for the new archive. I reproduced the issue.

(0004964)
signoles (manager)
2014-03-14 17:16

Here is a small reproducible example:
=====
#include <stdio.h>

int main(void) {
  int x = 2;
  printf("x = %d\n", x);
  return 0;
}
=====

The issue comes from using some functions of stdio.h and the way they are defined in the Frama-C libc library..

(0004968)
ploc (reporter)
2014-03-14 23:41

The hack "grep -v _fc_stdout" works pretty well. The code is compiled and behave as expected.

(0005262)
signoles (manager)
2014-07-16 10:00

Have been fixed by commit cd42fcb91.

(0005463)
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:29	ploc	New Issue
2014-03-14 01:29	ploc	Status	new => assigned
2014-03-14 01:29	ploc	Assigned To	=> signoles
2014-03-14 01:29	ploc	File Added: fc_stdout_gcc_error.tgz
2014-03-14 15:56	signoles	Note Added: 0004958
2014-03-14 15:56	signoles	Status	assigned => feedback
2014-03-14 16:44	ploc	Note Added: 0004960
2014-03-14 16:44	ploc	Status	feedback => assigned
2014-03-14 16:45	ploc	File Added: fc_stdout_gcc_error.v2.tgz
2014-03-14 16:56	signoles	Note Added: 0004963
2014-03-14 16:56	signoles	Status	assigned => acknowledged
2014-03-14 17:16	signoles	Note Added: 0004964
2014-03-14 17:16	signoles	Status	acknowledged => confirmed
2014-03-14 23:41	ploc	Note Added: 0004968
2014-07-16 10:00	signoles	Note Added: 0005262
2014-07-16 10:00	signoles	Status	confirmed => resolved
2014-07-16 10:00	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: 0005463
2014-09-15 17:20	signoles	Status	resolved => closed

Notes
(0004958) signoles (manager) 2014-03-14 15:56	Your example is not standalone: Generating non instrumented binary 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. cpt_cpt.c:3:52: fatal error: /usr/local/include/lustrec/io_frontend.h: No such file or directory compilation terminated. Could you provide the missing files?

(0004960) ploc (reporter) 2014-03-14 16:44	New archive with all required files.

(0004963) signoles (manager) 2014-03-14 16:56	Thanks for the new archive. I reproduced the issue.

(0004964) signoles (manager) 2014-03-14 17:16	Here is a small reproducible example: ===== #include <stdio.h> int main(void) { int x = 2; printf("x = %d\n", x); return 0; } ===== The issue comes from using some functions of stdio.h and the way they are defined in the Frama-C libc library..

(0004968) ploc (reporter) 2014-03-14 23:41	The hack "grep -v _fc_stdout" works pretty well. The code is compiled and behave as expected.

(0005262) signoles (manager) 2014-07-16 10:00	Have been fixed by commit cd42fcb91.

(0005463) signoles (manager) 2014-09-15 17:20	Fixed in E-ACSL v0.4.1.

Relationships