当我试图在Frama-c中运行我的简单代码时,我遇到了一些问题.我正在尝试创建一个指向数组结构的有效指针,并从我的函数返回此指针Stack_init.我不明白为什么Frama-c会返回此错误并且不能证明我的功能:
[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
我的目的是创建一个函数,返回一个没有前置条件的指针,后置条件是指针有效.
有人可以帮我理解我的错误在哪里吗？
/*
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;
}