--- layout: fc_discuss_archives title: Message 33 from Frama-C-discuss on June 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Ghost label and \at construct



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