GitLab

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

---

Id	Project	Category	View	Due Date	Updated
ID0000877	Frama-C	Plug-in > RTE	public	2011-07-06	2012-05-16

Reporter	yakobowski	Assigned To	pherrmann	Resolution	fixed
Priority	normal	Severity	major	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	Frama-C GIT, precise the release id	Target Version	-	Fixed in Version	Frama-C Nitrogen-20111001

Description :

Calling the WP (or Jessie for that matter) on the following code results in all goals being proven. Yet, there is a RTE on the call to max, because a is not initialized. I tend to think that -rte-precond should add \initialized(a) and \initialized(b) to the local contract for the call to max, but there is perhaps another better way. Anyway, either RTE or the WP are faulty here.

/*@ ensures \result == (a < b ? a : b); */ int max(int a, int b) { return (a < b ? a : b); }

int main () { int a; int b = 2; return max (a, b); }