为Frama-C EVA适配STM32外设硬件存储定义的技术咨询

在使用Frama-C EVA进行代码分析时，需要处理硬件“存储”相关的定义。CMSIS提供的STM32外设头文件通用结构如下：

typedef struct {
    __IO uint32 REGn;
    // ...
} SOC_PER_TypeDef;

#define SOC_PER_BASE                 0x40003000
#define SOC_PER                 ((SOC_PER_TypeDef *) SOC_PER_BASE)

代码中调用外设寄存器的示例：

if(SOC_PER->REGn != 0) /* xxx */;

此时EVA会返回越界读取的错误：

out of bounds read.
  assert \valid_read(&((IWDG_TypeDef *)((uint32_t)(0x40000000 + 0x3000)))->SR);

注：__IO是CMSIS定义的编译器相关宏，等价于volatile。

现咨询以下问题：

• 能否重新定义__IO来适配Frama-C？
• 是否需要为SOC_PER_BASE添加某种注解？
• Frama-C是否提供预定义的预处理变量，用于修改头文件逻辑？

另外提供了一个示例方案供参考：

#ifdef FRAMA_C
  extern SOC_PER_TypeDef SOC_PER_stub;
  #define SOC_PER_BASE &SOC_PER_stub
#else
    #define SOC_PER_BASE                 0x40003000
#endif

内容的提问来源于stack exchange，提问作者artless-noise-bye-due2AI