如何在ACSL中强制内存位置有效？

Question

我将设备访问定义为这样

volatile struct mydevice * const dev = (struct mydevice *)MY_DEVICE_ADDRESS;

我已经将访问建模为

@ volatile dev->somereg reads somereg_read writes somereg_write;

现在的问题是，当我启用RTE检查时，生成的有效性检查无法被证明。

/*@ assert rte: mem_access: \valid(dev->somereg); */

是否有任何方法对我的代码进行注释，使MY_DEVICE_ADDRESS直到MY_DEVICE_ADDRESS+sizeof(struct )被认为是有效的？

编辑:这里有一个尝试不起作用

#include <stdint.h>

#define MY_DEVICE_ADDRESS (0x80000000)

struct mydevice {
  uint32_t somereg;
  uint32_t someotherreg;
};

volatile struct mydevice * const dev = (struct mydevice *)MY_DEVICE_ADDRESS;

/*@ axiomatic Physical_Memory {
     axiom Dev: \valid((struct mydevice*)MY_DEVICE_ADDRESS);
  } */

int main(int argc, const char *argv[]) {
  //@ assert \valid(dev);
  //@ assert \false;
  return 0;
}

同跑

frama-c-wp -wp-rte -wp-init-const -wp-模型类型测试.c

Answer 1

我不知道(我也试过很多次)。

我找到的唯一解决办法是：

struct mydevice MY_DEVICE_STRUCT;
volatile struct mydevice * const dev = & MY_DEVICE_STRUCT;

您需要“实例化”内存，因为这正是底层LLVM所期望的。当然，通过ACSL表示法强制这样做是很好的。