--- layout: fc_discuss_archives title: Message 70 from Frama-C-discuss on April 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] verifying overflow in x++



Hi,
Which version of Frama-C/Wp are you using ?
Latest release Fluorine leads to :

[wp] 3 goals scheduled
[wp] [Qed] Goal typed_f_assign : Valid
[wp] [Qed] Goal typed_f_B_post : Valid
[wp] [Alt-Ergo] Goal typed_f_A_post : Valid (21ms) (11)

By the way, resources for reasoning over machine integers are limited in WP for automated provers.
The reason is that reasoning with modulus generally drives alt-ergo and such into larger research space.
You have all the necessary axiomatizations in Coq, however.

A common practice is to insert assertions and lemmas to be proven in Coq.
Example : assumes the following code, where you know that "c" potentially overflows.
{ unsigned char c; ... c++; ... }

You may add the following lemma :
/*@ lemma uint8_incr : \forall integer x ; (unsigned char) (x-256) == (unsigned char) x ; */

Prove it in CoqIde :

Proof.
  intros.
  unfold to_uint8.
  unfold to_range.
  simpl.
  replace (x_0 - 0) -> x_0 by auto with zarith.
  replace (x_0 - 256 - 0) -> (x_0 + (-1) * 256) by ring.
  symmetry.
  apply Z_mod_plus_full.
Qed.

And now, Alt-Ergo and such can use this fact.
	L.

Le 26 avr. 2013 ? 17:20, Damien Karkinsky a ?crit :

> Hello,
> 
> I had a simple function with the following contract:
> 
> #include<stdint.h>
> 
> uint16_t x;
> 
> /*@
>  assigns x;
> 
>  behavior A:
>  assumes x < 65535;
>  ensures x == \old(x) + 1;
> 
>  behavior B:
>  assumes x == 65535;
>  ensures x == 0;
> */
> void f();
> 
> 
> void f(){
>  ++x;
> }
> 
> void main(){
>  f();
> }
> 
> I cannot verify the post condition for behaviour B. WP states
> Goal store_f_B_post_2:
>  forall x_0:int.
>  is_uint16(x_0) ->
>  (x_0 = 65535) ->
>  (let x_1 = as_uint16(65536) in
>   (x_1 = 0))
> 
> I suppose  as_uint16(65536) = 0  is not derived to be the case.
> 
> Would any one care to comment? Is that a bug?
> 
> Thank you and all the best
> Damien
> 
> -- 
> ------------------------------------------------------------------------
> 
> Dr. Damien Karkinsky
> 
> Safety-Critical Systems Consultant
> 
> Adelard LLP. (www.adelard.com)
> 
> Exmouth House, 3-11 Pine Street, London, EC1R 0JH
> 
> tel: +44(0)20-7832-5854   mob: +44(0)779-568-1233
> 
> ------------------------------------------------------------------------
> 
> 
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss