Search code examples
frama-cacsl

Understanding `pointer_comparable` with frama-c

I am trying to use frama-c to verify parts of C code using pointer comparisons.

But I don't understand how to use the \pointer_comparable predicate.

According to the acsl documentation, \pointer_comparable should hold for two pointers pointing to the same array object:

\pointer_comparable takes two pointers to object or function type as arguments. \pointer_comparable{L}(p1,p2) holds if and only if p1 and p2 point to the same function or to an element (or one past the last element) of the same array object.

So I expect both assertions in the following C code snippet to hold:

int main(int argc, char** argv)
{
  unsigned char buffer[1024] = {0};

  unsigned char* a = &buffer[1];
  unsigned char* b = &buffer[8];

  //@ assert \pointer_comparable(a, b);
  //@ assert \pointer_comparable(a, a+7);
}

But when I analyze it with frame-c (version 29.0)

frama-c -eva -eva-precision 11 pointer_comparable.c

I get the warnings

[eva:alarm] pointer_comparable_001.c:8: Warning: assertion got status unknown.
[eva:alarm] pointer_comparable_001.c:9: Warning: assertion got status unknown.

Screenshot of the warning in the GUI (frama-c-gui -eva -eva-precision 11 pointer_comparable.c): screenshot of the warning in the gui

Question

How do I get frama-c to understand that the two pointers are indeed part of the same array and get it to accept an assertion \pointer_comparable as holding.

Solution

  • The current implementation of Eva concerning this predicate is intended to generate \pointer_comparable assertions, but not verify them. Thus currently Eva does not try to verify them at all, and simply emits an unknown status concerning their validity.

    The following code is an example of intended usage for the predicate:

    // pc.c
char b1[5], b2[2];
int main(void) {
  char *p1 = b1, *p2 = b2;
  if (p1 < p2) {
    return 1;
  }
  return 0;
}

    In my machine, if I run gcc pc.c -Wall -Wextra -O0 && ./a.out; echo $?, I have no warnings and an output of 0. If I run gcc pc.c -Wall -Wextra -O1 && ./a.out; echo $? (or -O2, or -O3), I get an output of 1 instead.

    Indeed, the comparison between p1 and p2 using the < operator is undefined, and thus the compiler can do whatever it wants.

    Therefore, when analyzing this code with Frama-C/Eva, we need to emit an alarm about this undefined behavior. So Eva checks each pointer comparison and assesses whether it is well-defined. When Eva cannot prove it, it emits a \pointer_comparable alarm.

    So, the ACSL manual must explain what this alarm means, hence why it is described there. However, since these alarms are currently generated by Eva, and only when Eva cannot prove them, trying to manually write and verify them with Eva is not an intended use case. Eva could of course be extended to try and prove such assertions, but so far the main users of Frama-C/Eva were not particularly interested in such cases. If you have specific scenarios in which this is relevant, consider submitting a feature request.

    In your code example, the comparison is valid, so if you just run Eva without adding the asserts, it will not produce any alarms, even though it did check that the comparisons were allowed by the standard.