GitLab

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

---

Id	Project	Category	View	Due Date	Updated
ID0000072	Frama-C	Plug-in > jessie	public	2009-04-30	2010-02-12

Reporter	bobot	Assigned To	cmarche	Resolution	open
Priority	normal	Severity	minor	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	Frama-C GIT, precise the release id	Target Version	-	Fixed in Version	-

Description :

No vc are produced with this function.

spec_statement.c :

void myfun(int p){ p = 1; /@ requires p==1; @ ensures \old(p)==p-1; @/ p = 2; }

spec_statement.jc:

unit myfun(integer p) behavior default: assumes true; ensures (C_3 : true); {
{ (C_1 : (p = 1)); (C_2 : (p = 2));

  (return ())

} }

Additional Information :

frama-c : 5186