--- layout: fc_discuss_archives title: Message 33 from Frama-C-discuss on June 2011 ---
Hello Nicolas, Le lun. 20 juin 2011 14:07:21 CEST, Nicolas Ayache <nicolas.ayache at gmail.com> a ?crit : > > void f () { > int i = 0; > //@ ghost L: > i = 1; > /*@ assert \at(i, L) == 0; */ > } > > I would have expected the assertion to be true. But running the jessie that's right, the value of i at L is 0. In fact, the WP plugin discharges the assertion directly, without having to call a prover. > plug-in leads to a proof obligation that none of the automatic provers > on my computer has been able to discharge. Indeed, the produced proof > obligation seems impossible to prove: > > H1: true > result: int32 > result0: int32 > H3: integer_of_int32(result0) = 0 > i: int32 > H4: i = result0 > result1: int32 > H5: integer_of_int(result1) = 1 > i0: int32 > H6: i0 = result1 > ------------------------------------------------ > integer_of_int32(result) = 0 Indeed, there is an issue here. I guess that this is worth a bug report on Why/Jessie. In fact, if you have a look at the intermediate files, the .jc appears to be OK: ============ unit f() behavior default: ensures (C_4 : true); { (var int32 i); { (C_1 : (i = 0)); (L : ()); (C_2 : (i = 1)); { (assert for default: (C_3 : (\at(i,L) == 0))); () }; (return ()) } } ============= but in the corresponding .why the label L occurs before initialization of i: ============= let f_ensures_default = fun (tt : unit) -> { (JC_4: true) } (init: try begin (let i = ref (any_int32 void) in (C_1: (L: (C_2: begin (let jessie_6 = (i := (safe_int32_of_integer_ (0))) in void); void; (let jessie_8 = (i := (safe_int32_of_integer_ (1))) in void); (assert { (JC_10: eq_int(integer_of_int32(i at L), (0))) }; void); void; (raise Return) end)))); (raise Return) end with Return -> void end) { (JC_5: true) } ============== If you put L: at its right place between jessie_6 and jessie_8, the generated PO looks normal. Thus my best guess so far is that there's an issue in the translation of labels from Jessie to Why. Best regards, -- E tutto per oggi, a la prossima volta. Virgile