c - EVA插件: How to check the add value in "temp = (volatile unsigned short*) add " through the temp variable

Question

我试图通过以下示例中的 temp 变量检查“temp = ( volatile 无符号短*) add ”中的添加值:

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检查增值的答案。

Answer 1

关于:

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

这是尝试将temp的地址(位于堆栈上)与某个地址(堆栈上的该位置除外)进行比较。自然地，assert() 被触发

访问内存中特定地址内容的正确方法是:

temp =  *(unsigned short *) 0x01;