untypable ACSL in a sliced program containing \result

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

Id	Project	Category	View	Due Date	Updated
ID0000673	Frama-C	Plug-in > slicing	public	2011-01-17	2014-02-12


Reporter	signoles	Assigned To	patrick	Resolution	fixed
Priority	normal	Severity	major	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	Frama-C Carbon-20101202-beta2	Target Version	-	Fixed in Version	Frama-C Carbon-20110201

Description :

If a function contract contains \result, then the sliced function keeps it even if it now returns void.

Steps To Reproduce :

===== bug.c ===== void f(void) { return; }

/@ ensures \result == 0; / int main(void) { f(); return 0; }

$ frama-c bug.c -slice-calls f -then-on "Slicing export" -print -ocode sliced_bug.c $ more sliced_bug.c /* Generated by Frama-C */ void f_slice_1(void) { return; }

/*@ ensures (\result ? 0); */ void main(void) { f_slice_1(); return; }

$ frama-c sliced_bug.c [kernel] preprocessing with "gcc -C -E -I. sliced_bug.c" sliced_bug.c:7:[kernel] user error: \result meaningless in annotation. [kernel] user error: skipping file "sliced_bug.c" that has errors. [kernel] Frama-C aborted because of invalid user input.

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information

untypable ACSL in a sliced program containing \result

Description :

Steps To Reproduce :

/*@ ensures \result == 0; */ int main(void) { f(); return 0; }

/@ ensures \result == 0; / int main(void) { f(); return 0; }