GitLab

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

---

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

Reporter	bobot	Assigned To	cmarche	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 Beryllium-20090902

Description :

An example with a label in a ghost (or not) statement,

label.c :

void myfun(int p){ p = 1; //@ ghost Mylabel: p = 2; //@ assert \at(p,Mylabel)==p-1; }

Why complains about an unbound label.

frama-c -jessie-analysis label.c :

[...] File "why/label.why", line 350, characters 30-47: Unbound label 'Mylabel'

In fact the label is defined in the jessie file.

label.jc :

unit myfun(int32 p) behavior default: assumes true; ensures (C_4 : true); {
{ (C_1 : (p = 1)); (Mylabel : ()); (C_2 : (p = 2));

  {  
     (assert for default: (C_3 : (\at(p,Mylabel) == (p - 1))));
     ()
  };
  
  (return ())

} }

and in the why file, but perhaps not well scoped.

why/label.why :

let myfun_safety = fun (p : int32) -> { (JC_4: true) } (let mutable_p = ref p in (init: try begin (C_1: (let jessie_1 = (mutable_p := (safe_int32_of_integer_ (1))) in void)); (Mylabel: (let jessie_2 = (mutable_p := (safe_int32_of_integer_ (2))) in void)); [ { } unit reads mutable_p { (JC_9: eq_int(integer_of_int32(mutable_p@Mylabel), sub_int(integer_of_int32(mutable_p), (1)))) } ]; void; (raise Return); (raise Return) end with Return -> void end)) { true }

Additional Information :

frama-c release 5186