--- layout: fc_discuss_archives title: Message 69 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++



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

------------------------------------------------------------------------