--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on March 2016 ---
Hi I think need to add some general axiom aboud mod (not for safe_comp_not). Like this axiom mod_axiom : forall x,y : int. ( (x < 0) and (y < x) ) or ( (x = 0) and (y <> 0) ) or ( (x > 0) and (y > x) ) -> (x = (x % y)) http://www.wolframalpha.com/input/?i=x%3Dmod%28x,y%29 seems legit I also want to try validate this transforms from GCC https://gcc.gnu.org/viewcvs/gcc/trunk/gcc/simplify-rtx.c?view=markup&pathrev=232689#l2062 I hope Alt-Ergo can do this 21.03.2016, 09:12, "Mohamed Iguernlala" <iguer.pro at gmail.com>: > Hi, > > Axioms about safe_comp_mod are in the model. However, axioms that > give the behavior of to_uint8(i) when (0 <= i < 256) is not true are > probably missing. > > I modified a little bit your C code (see below). I have one unproved VC, > for which I get safe_comp_mod(i,256) = 44 in the model. > An axiom like "A_1" would allow to conclude in this case. > > For the generic axiom, a case 0 <= i and i >= j is missing ... > > Regards, > Mohamed. > > #include <stdio.h> > > // Proved by Alt-Ergo // > /*@ requires (1 <= a <= 255); >     ensures \result == 1; > */ > int test_uint8_cast_mod256_eq (int a) > { return ((a)%256 == (unsigned char)(a)); } > > // Proved by Qed // > /*@ requires 300 <= a <= 300; >     ensures \result == 1; > */ > int test_uint8_cast_mod256_eq__v2 (int a) > { return ((a)%256 == (unsigned char)(a)); } > > // Not Proved // > /*@ requires 300 <= a <= 302; >    ensures \result == 1; > */ > int test_uint8_cast_mod256_eq__v3 (int a) > { return ((a)%256 == (unsigned char)(a)); } > > int main (){ >  int b = 300; >  printf("mod     = %d\n", b%256); >  printf("unsigned = %d\n", (unsigned char) (b)); > } > > Le 21/03/2016 02:57, sztfg at yandex.ru a écrit : > >> I was trying to prove this code using alt-ergo: /* ALWAYS TRUE */ /*@ ensures \result == 1; */ uint8_t test_uint8_cast_mod256_eq (uint64_t a) { return ((a)%256 == (uint8_t)(a)); } how it looks like: goal test_uint8_cast_mod256_eq_post: forall i : int. is_uint64(i) -> (to_uint8(i) = (safe_comp_mod(i, 256))) but it failed. Maybe need to add some axioms related safe_comp_mod? Adding new axioms to .mlw file: axiom A_1 : forall i : int. (0 <= i) -> (to_uint8(i) = (safe_comp_mod(i, 256))) axiom A_2 : forall i : int. (0 <= i) -> (to_uint16(i) = (safe_comp_mod(i, 65536))) axiom A_3 : forall i : int. (0 <= i) -> (to_uint32(i) = (safe_comp_mod(i, 4294967296))) axiom A_4 : forall i : int. (0 <= i) -> (to_uint64(i) = (safe_comp_mod(i, 18446744073709551616))) ... and after that I can prove it. But maybe I doing something wrong, and this thing can be proved without adding axioms? Or maybe need to add more general axiom? I tried this axiom: axiom A_GENERIC : forall i,j : int. ((0 <= i) and (i < j)) -> (i = (safe_comp_mod(i, j))) but it doesn't work _______________________________________________ Frama-c-discuss mailing list Frama-c-discuss at lists.gforge.inria.fr http://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss