5

I am trying to use Frama-C to verify safety properties of C code that includes dynamic memory allocation. The current version of the ACSL specification language (1.8) seems to be able to express a lot about dynamically allocated memory. However, most of that stuff is not yet implemented in Frama-C Neon.

Suppose we take the following snippet of code:

#include <stdlib.h>

/*@ requires \valid(p) && \valid(q) && \separated(p, q);
  @ ensures \valid(q);
  @*/
void test(char *p, char *q) {
  free(p);
}

int main(void) {
  char *p = (char *) malloc(10);
  char *q = (char *) malloc(10);

  test(p, q);

  return 0;
}

So, main allocates two blocks of memory, and passes pointers to them to function test. Test frees the block pointed to by p, but not the block pointed to by q. Suppose I want to prove that at the end of test, pointer q is still valid. How would I proceed?

It seems that I have to model the heap on my own: axiomatize a few predicates that talk about the heap, and use them to specify malloc and free, mimicking the non-implemented parts of ACSL. What would be the simplest approach to do that, so that I can verify the example above?

Filip Nikšić
  • 151
  • 1
  • 4
  • I do not want to discourage you, but the reason `allocates` clauses were added to the ACSL definition is that dynamic allocation cannot really be added to the specification language as user-defined predicates. For the same reason, if the dynamic allocation extensions are not available yet, you are not going to be able to implement them with user predicates. – Pascal Cuoq Oct 19 '14 at 15:53
  • Could you be more specific as to why this cannot be done at the user level? – Filip Nikšić Oct 21 '14 at 17:32
  • 2
    I cannot list everything that does not work in the room of a comment, but I note that your function does not have an `assigns` clause, and if your function had an `assigns` clause, any `assigns` clause, that clause would not express that `p` ceases to be valid after calling `test`, for the same reason that when a function does not have `\valid(&a)` in its post-condition, that does not mean that `&a` is no longer valid after the function has been executed. – Pascal Cuoq Oct 21 '14 at 17:54
  • 1
    I see. Yes, I thought this would be the main problem. But it seems to me that I could then define a new predicate, say MyValid, and use it everywhere instead of the built-in one. Essentially, I would have a memory model that is completely separated from the built-in one, and that can only talk about dynamically allocated memory. – Filip Nikšić Oct 21 '14 at 18:43
  • Yes, that could work. – Pascal Cuoq Oct 21 '14 at 19:12

0 Answers0