Frama-c pointer incompatible type

Question

I've a little problem when I've tried to run my simple code in Frama-c. I'm trying to create a valid pointer to an array structure and return this pointer from my function Stack_init. I don't understand why Frama-c returns this error and doesn't prove my function:

[kernel] preprocessing with "gcc -C -E -I.  /home/federico/Desktop/simple_main_v2.c"
[kernel] warning: Neither code nor specification for function malloc, generating default assigns from the prototype
[wp] Collecting axiomatic usage
[wp] warning: Missing RTE guards
Desktop/simple_main_v2.c:28:[wp] warning: Cast with incompatible pointers types (source: sint8*) (target: sint32*)
[wp] 0 goal scheduled

My intention is to create a function that returns a pointer, without precondition, where the postcondition is that the pointer is valid.

Can someone help me to understand where my error is?

/*
  create_stack

        Inputs: none
        Outputs: S (a stack)
        Preconditions: none
        Postconditions: S is defined and empty 
*/

/*@ 
    ensures  \valid(\result) && \result[0] == 0;
*/
int *Stack_Init()
{       
    int *stack = malloc (sizeof(int[100]));
    stack[0] = 0;               
    return stack;               
}

Answer 1

The WP plugin does not support void * pointers very well, as its internal memory model relies on the static types with which elements are declared. This is the bulk of the error you are witnessing. As you can see in issue 2078, a refined memory model will appear at some point (Frama-C Magnesium version) and provides some help with the matter.

Note however that there is another issue with malloc beyond support for void *, namely support for dynamically allocated memory (predicate fresh and its siblings in ACSL), for which nothing is really planned at the moment as far as I know.

Answer 2

You have no errors.

warning: Cast with incompatible pointers types (source: sint8*) (target: sint32*)

This is nonsense.

• First of all, there is no cast in the code. Cast and conversion are different things. You'd hope people who write such advanced things as static analysers would know the difference...
• There is no sint8* here. malloc returns void* which is a unique type.
• Void pointers are guaranteed to convert to/from any other pointer type without an explicit cast.
• You need to include stdlib.h. The tool should tell you that the function is not declared with a prototype in case you forgot it. It would seem that the first line you get is such a warning.

The only strange thing with this code is that the analyser doesn't complain about the empty parenthesis list in int * Stack_Init(). This is poor practice, as it could potentially cause all kinds of type related bugs in case there is no prototype. A good tool would tell you to declare the function as int * Stack_Init (void).

I would report all of this as bugs in the static analyser.

---

postcondition is the pointer is valid.

Then you need to check the result of malloc and include some sort of error handling in case malloc fails.

Answer 3

This code is basically correct. You probably should add a cast to the return from malloc (mandatory in C++), but from what I remember about C this is optional:

  int * stack = (int*) malloc(sizeof(int[100]);

and don't forget the header stdlib.h