Bitwise logical support

[Mark Tuttle]

Do you have advice on verifying code using bitwise logical operations?

When I run "verifast -target 32bit test1.c1" on the following I get "Assertion might not hold. (Cannot prove bitor(240, 15) <= 255.)":

int main ()

//@ requires true;

//@ ensures true;

{

  int a = 0x000000F0;

  int b = 0x0000000F;

  int c = a | b;

  assert( c <= 0x000000FF );

  return 0;

}

When I run "verifast -target 32bit test2.c1" on the following I get successful verification:

int main ()

//@ requires true;

//@ ensures true;

{

  int a = 0x000000F0;

  int b = 0x0000000F;

  int c = a + b;

  assert( c <= 0x000000FF );

  return 0;

}

Thanks,

Mark

[Bart Jacobs]

Running "verifast -target 32bit -prover z3v4.5 test.c" on the following succeeds.

//@ #include <bitops.gh>

int main ()
//@ requires true;
//@ ensures true;
{
  int a = 0x000000F0;

  //@ Z za = Z_of_uint32(a);
  int b = 0x0000000F;
  //@ Z zb = Z_of_uint32(b);

  int c = a | b;

  //@ bitor_def(a, za, b, zb);
  assert( c <= 0x000000FF);

  return 0;
}

This requires Z3 instead of the built-in Redux because Redux is extremely poor at SAT solving.

--
You received this message because you are subscribed to the Google Groups "VeriFast" group.
To unsubscribe from this group and stop receiving emails from it, send an email to verifast+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/verifast/1fadfd19-c8e7-43ce-95c5-0c78b3a98a11n%40googlegroups.com.