frama-c - 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 + sizeof(struct mydevice) までの MY_DEVICE_ADDRESS が有効と見なされるように、コードに注釈を付ける方法はありますか?

編集：これはうまくいかない試みです

#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-model 型付き test.c