I am trying to use Frama-C to check the security 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 this material is not yet implemented in Frama-C Neon.
Suppose we take the following code snippet:
#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, the main thing is that it allocates two memory blocks and passes pointers to them to check the function. The 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 the test, the q pointer remains valid. How can I continue?
It seems that I have to model the heap myself: axiomatize several predicates that talk about the heap and use them to specify malloc and for free, simulating the incomplete parts of ACSL. What would be the easiest way to do this so that I can check the example above?
source share