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] Problem with werify mod 256 and cast to uint8 equivalence for uint64_t

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