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] Simple loop, overflow and bounds

  • Subject: [Frama-c-discuss] Simple loop, overflow and bounds
  • From: kurt at roeckx.be (Kurt Roeckx)
  • Date: Wed, 2 Sep 2015 22:10:30 +0200
Hi,

I'm looking at frama-c to see what I can do with it to, so I ran
it against some code to see what comes out of it.  The following
is based on a much larger real file, but I think this already
shows the kind of questions I have.

I started with the file:
void foo()
{
    unsigned int X[16];
    int i;

    for (i = 0; i < 16; i++)
    {
        X[i] = 0;
    }

    for (i = 16; i < 64; i += 8)
    {
        X[((i+0)+1) & 0x0f]++;
    }
}

(This function of course makes little sense.)

I run:
frama-c-gui -wp -wp-rte -wp-proof alt-ergo <file>

Which will then show me:
void foo(void)
{
  unsigned int X[16];
  int i;
  i = 0;
  while (i < 16) {
    /*@ assert rte: index_bound: 0 <= i; */
    /*@ assert rte: index_bound: i < 16; */
    X[i] = (unsigned int)0;
    /*@ assert rte: signed_overflow: i+1 <= 2147483647; */
    i ++;
  }
  i = 16;
  while (i < 64) {
    /*@ assert rte: index_bound: 0 <= (int)((int)((int)(i+0)+1)&0x0f); */
    /*@ assert rte: index_bound: (int)((int)((int)(i+0)+1)&0x0f) < 16; */
    /*@ assert rte: signed_overflow: (int)(i+0)+1 <= 2147483647; */
    /*@ assert rte: signed_overflow: i+0 <= 2147483647; */
    /*@ assert
        rte: unsigned_overflow:
          X[(int)((int)((int)(i+0)+1)&0x0f)]+1 <= 4294967295;
    */
    (X[((i + 0) + 1) & 0x0f]) ++;
    /*@ assert rte: signed_overflow: i+8 <= 2147483647; */
    i += 8;
  }
  return;
}

And it show me:
[wp] 9 goals scheduled
[wp] [Qed] Goal typed_foo_assert_rte_index_bound_2 : Valid
[wp] [Alt-Ergo] Goal typed_foo_assert_rte_signed_overflow : Valid (16ms) (5)
[wp] [Alt-Ergo] Goal typed_foo_assert_rte_index_bound : Unknown (400ms)
[wp] [Alt-Ergo] Goal typed_foo_assert_rte_signed_overflow_3 : Valid (28ms) (13)
[wp] [Alt-Ergo] Goal typed_foo_assert_rte_signed_overflow_2 : Valid (32ms) (47)
[wp] [Alt-Ergo] Goal typed_foo_assert_rte_signed_overflow_4 : Valid (28ms) (21)
[wp] [Alt-Ergo] Goal typed_foo_assert_rte_index_bound_4 : Unknown (1.4s)
[wp] [Alt-Ergo] Goal typed_foo_assert_rte_index_bound_3 : Unknown (1.5s)
[wp] [Alt-Ergo] Goal typed_foo_assert_rte_unsigned_overflow : Unknown (961ms)
[wp] Proved goals:    5 / 9
     Qed:             1 
     Alt-Ergo:        4  (16ms-32ms) (47) (unknown: 4)


So I have a some questions about this:
For some reason it can't prove any of the index_bound ones,
except for the 2nd. (i < 16).  If I look at the code, they all
seem fairly easy to figure out (for me), since i always has
a clear limit of the values it's going to have.

Does this require me add things like loop invariants, or something
else?  If I add the following before my first for loop it makes
that whole first loop valid:
/*@ loop invariant 0 <= i <= 16; */

This all seems to be done by Qed in this case, not alt-ergo.
Why can't alt-ergo figure this out?  Is this some shortcomming in
the file that is generated for alt-ergo?

Doing the same for the second loop, but then using the following
doesn't seem to help at all:
/*@ loop invariant 16 <= i <= 64; */

It seems to be unable to prove that, and so the signed overflow checks
that used to be surely_valid are probably turned into the valid_under_hyp
because of that.

I'm not sure why it can't prove the 3rd index_bound.  The only
reason I can think of why it would fail is that it might for some
reason think i could be negative.  So I turned it into an unsigned
int, then get to see:

/*@ assert
        rte: index_bound:
          (unsigned int)((unsigned int)((unsigned int)(i+(unsigned int)0)+(unsigned int)1)&(unsigned int)0x0f)
          < 16;
    */

And it still unknown, while that should be true for all unsigned integers.

Currently a last question is if there is a way to turn off the
unsigned overflow check it adds?  I have code that code actually
relies on the overflow behaviour of unsigned integers.


Kurt