Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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