Образец Frama-c несовместим с типом

Question

У меня небольшая проблема, когда я пытался запустить свой простой код в Frama-c. Я пытаюсь создать действительный указатель на структуру массива и вернуть этот указатель из моей функции Stack_init. Я не понимаю, почему Frama-с возвращает эту ошибку и не доказать свою функцию:

[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;    
} 

Answer 1

Этот код в основном правильный. Вы, вероятно, следует добавить бросок к возвращению из таНос (обязательное в C++), но от того, что я помню о C это необязательно:

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

и не забудьте заголовке stdlib.h

Answer 2

У Вас нет ошибки.

предупреждение: Cast с несовместимыми указатели типов (источник: sint8 *) (цель: sint32 *)

Это нонсенс.

• Прежде всего, в коде отсутствует листинг. Литые и конверсия это разные вещи. Вы надеетесь, что люди, которые пишут такие продвинутые вещи, как статические анализаторы, знают разницу ...
• Здесь нет sint8*. malloc возвращает void*, который является уникальным типом.
• Указатели Void гарантированно преобразуются в любой тип указателя без каких-либо явных приемов.
• Вам необходимо включить stdlib.h. Инструмент должен сказать вам, что функция не объявлена ​​прототипом, если вы ее забыли. Казалось бы, первая строка, которую вы получаете, является таким предупреждением.

Единственное странное в этом коде состоит в том, что анализатор не жалуется на пустой список скобок в int * Stack_Init(). Это плохая практика, так как это может привести к возникновению всех типов связанных с типом ошибок ошибок в случае отсутствия прототипа. Хороший инструмент сказал бы вам объявить функцию как int * Stack_Init (void).

Я бы сообщил об этом как об ошибках в статическом анализаторе.

---

Постусловие является указателем является действительным.

Затем вам нужно проверить результат malloc и включить обработку ошибок в случае сбоя malloc.

Answer 3

Плагин WP не поддерживает void * указатели очень хорошо, так как его модель внутренней памяти основана на статических типах, с которыми объявлены элементы.Это основная часть ошибки, которую вы наблюдаете. Как вы можете видеть в issue 2078, в какой-то момент появится усовершенствованная модель памяти (версия Magna-C Magnesium) и поможет вам в этом.

Однако обратите внимание, что есть еще одна проблема с malloc за поддержку void *, а именно поддержка динамически распределяемой памяти (предиката fresh и его братьев и сестер в ACSL), для которого ничего не действительно запланированном на данный момент, насколько я знаю.