GitLab

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

---

Id	Project	Category	View	Due Date	Updated
ID0000544	Frama-C	Plug-in > jessie	public	2010-07-17	2010-07-17

Reporter	logan	Assigned To	cmarche	Resolution	open
Priority	normal	Severity	feature	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	Frama-C Boron-20100401	Target Version	-	Fixed in Version	-

Description :

Consider the following functions. Both function violates ACSL specification, and all of the theorem prover gives UNKNOWN as result (which is correct and expected).

However, the name of proof obligation of test2() is "loop invariants initially holds" which is a little confusing. Since the problem is actually on the assign statement instead of the while-loop. I think it will be better to have an independent check for @assigns annotation just like the "postcondition" proof obligation of test1().

---

int global;

/*@ assigns \nothing; */ int test1() { global = 1; }

/*@ assigns \nothing; */ int test2() { global = 2;

/*@ loop variant 0; */ while (0) { } }