GitLab

ID0001589: This issue was created automatically from Mantis Issue 1589. Further discussion may take place here.

---

Id	Project	Category	View	Due Date	Updated
ID0001589	Frama-C	Kernel	public	2013-12-26	2014-03-13

Reporter	pascal	Assigned To	virgile	Resolution	fixed
Priority	normal	Severity	minor	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	Frama-C GIT, precise the release id	Target Version	-	Fixed in Version	Frama-C Neon-20140301

Description :

~ $ cat n.c volatile int x;

int main(){ x; x; x; } ~ $ ~/ppc/bin/toplevel.opt -print n.c [kernel] preprocessing with "gcc -C -E -I. n.c" /* Generated by Frama-C */ int volatile x; int main(void) { int __retres; __retres = 0; return __retres; }

This transformation does not respect the semantics of the program because x is volatile.