Плагин EVA: как проверить добавочную стоимость в «temp = (volatile unsigned short *) add» через переменную temp - PullRequest
Новая
       46

Плагин EVA: как проверить добавочную стоимость в «temp = (volatile unsigned short *) add» через переменную temp

0 голосов
/ 22 февраля 2019

Я пытаюсь проверить добавленное значение в "temp = (volatile unsigned short *) add" через переменную temp в следующем примере: 

main() {
    unsigned short add = 0x01;
    unsigned short val = 0x00;
    unsigned short *temp;
    temp = (volatile unsigned short*) add;
    *temp = val;
    //@ assert &temp == (unsigned short) 0x01;
}

Но я получил эту ошибку в строке "// @ assert & temp == (unsigned short) 0x01; "

[kernel] user error: incompatible types unsigned short and unsigned short **
[kernel] user error: stopping on file "test_func_call.c" that has errors. Add '-kernel-msg-key pp'for preprocessing command.

Я знаю, что это может быть все о C, но я также использую тег Frama-C.Надеюсь, что я смогу получить ответ о проверке добавочной стоимости Frama-C.

1 Ответ

0 голосов
/ 22 февраля 2019

относительно: 

assert &temp == (unsigned short) 0x01;

Это попытка сравнить адрес temp (который находится в стеке) с некоторым адресом (отличным от этого местоположения в стеке).Естественно, assert() срабатывает

Правильный способ доступа к содержимому определенного адреса в памяти: 

temp =  *(unsigned short *) 0x01;
...