--- layout: fc_discuss_archives title: Message 122 from Frama-C-discuss on December 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] arithmetic overflow unsigned int



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;
}