1

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;               
}
byako
  • 3,372
  • 2
  • 21
  • 36
FedeXu
  • 50
  • 3

3 Answers3

6

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.

Virgile
  • 9,724
  • 18
  • 42
  • thanks for your reply, ok then frama-c do not support very well dynamic memory ? i need to implement a int stack (as you can see from my function) can i have kindly any suggestion to how i can implement in c an array without using of the function malloc() and free() ? – FedeXu Sep 04 '15 at 12:46
  • 1
    As a matter of fact, you might get away with the specification of `malloc` as it stands in Frama-C's own standard library. As long as you're trying to prove functions from the library itself, hence effectively only manipulating one stack at a time, you might not have trouble. Things will get much more problematic if you're using several stacks in a whole application, because there you will have to rely on the separation of the various blocks returned by malloc (as well as from the rest of the memory). – Virgile Sep 04 '15 at 17:21
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.

Lundin
  • 195,001
  • 40
  • 254
  • 396
  • 2
    Frama-C is several things, and here it is not used as a “static analyzer”. You are right that one would hope that people who write even more advanced things than static analysers would get it right, but in their defense, the first thing Frama-C's front-end does is translate the input C program with its casts and implicit conversions into an intermediate language in which all conversions are explicit and are named “Cast”. So one way to look at this mistake is simply that the error message exposes the inner workings of the framework. – Pascal Cuoq Sep 05 '15 at 20:42
  • 1
    In this particular case whoever assigned someone to verify C code with dynamic allocation with WP would have done better to check that this was supported at all beforehand, and the person tasked with doing it could have started with the manual http://frama-c.com/download/frama-c-wp-manual.pdf , section 1 of which starts warning about “heterogeneous cast of pointers” (read “conversion”—the “people …” really don't know the difference) on page 12. You should recommend that the OP read the first ten pages of the documentation before you recommend they report bugs. – Pascal Cuoq Sep 05 '15 at 20:50
  • @PascalCuoq I have yet to encounter a static analyser which isn't full of bugs, and I have tried many. This particular tool obviously gives confusing and misleading error messages: if that is because of misconfiguration or bugs, I don't know or care. – Lundin Sep 07 '15 at 06:21
  • “I don't know or care” You could save even more time by not answering questions about it on StackOverflow. – Pascal Cuoq Sep 07 '15 at 06:45
  • @PascalCuoq As in, I don't know why the tool is misbehaving and I don't care to fix it. I'm answering questions about C programming. If you for some reason feel offended because I'm pointing out incorrect behavior in said tool, kindly enlighten me which parts of my answer that are incorrect, as per the C standard. – Lundin Sep 07 '15 at 06:59
-1

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

ameyCU
  • 16,489
  • 2
  • 26
  • 41
resigned
  • 1,044
  • 1
  • 10
  • 11
  • Actually we should not cast result of `malloc`. – ameyCU Sep 04 '15 at 10:42
  • Yeah, since it's a `void` pointer, the cast is not mandatory (in C, don't know about C++). – Enzo Ferber Sep 04 '15 at 10:42
  • Why on earth would you not want to cat the return from malloc. If you don't do it the complier will do it for you anyway. – resigned Sep 04 '15 at 10:50
  • 1
    It is the most FAQ on SO. http://stackoverflow.com/questions/605845/do-i-cast-the-result-of-malloc – Lundin Sep 04 '15 at 10:52
  • Thanks for your reply, starting from the assure that frama-c is a tool in development and buggy, i give it a try with the cast before the malloc but it didn't resolve my problem..same error is displayed. Yes i include the library a little above this code section. – FedeXu Sep 04 '15 at 10:58