--- layout: fc_discuss_archives title: Message 122 from Frama-C-discuss on December 2009 ---
Hello, I am trying to avoid arithmetic overflow (using integer model bounded) in a piece of code I am working on. Now i somehow figured out, that Simplify has a problem to prove there's no arithmetic overflow when I use unsigned int as in the reduced example below. Does anyone have an idea why? Alt-ergo, z3, cvc3 and yices dont have problems with it. Using int instead also results in a successful proof by simplify. Thanks in advance, Kerstin (using Beryllium 2, mac os x) __________________ #define TRUE 1 #define FALSE 0 #include "limits.h" /*@ predicate true_or_false(int a) = (a == FALSE) || (a == TRUE); */ /*@ requires y < (UINT_MAX - 5000); //to avoid arithmetic overflow assigns \nothing; ensures true_or_false(\result); ensures (x > (y + 5000)) <==> \result == TRUE; */ int check_time_expired(unsigned int x, unsigned int y) { return (x > (y + 5000)) ? TRUE : FALSE; }