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] arithmetic overflow unsigned int

  • Subject: [Frama-c-discuss] arithmetic overflow unsigned int
  • From: kerstin.hartig at first.fraunhofer.de (Kerstin Hartig)
  • Date: Mon, 14 Dec 2009 17:10:58 +0100
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;
}