--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on September 2015 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Simple loop, overflow and bounds



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