Defining hardware "storage" for processing by Frama-C EVA

Question

The general structure of the headers for STM32 peripherals inside CMSIS,

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

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

And then a 'call/use' site is,

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

Eva is responding with text like,

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

The define __IO is compiler specific (located in CMSIS) and is volatile. Could I redefine __IO to accommodate frama-c? Or should I be targeting SOC_PER_BASE with an annotation of some sort. Are their pre-defined pre-processor variables to update headers?

Ie,

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

Answer 1

As anol mentioned, you can use -absolute-valid-range. This option has an advantage in the sense that you can specify that the first n bytes are actually invalid. (Here n=0x40003000.)

But the best solution is probably to override the SOC_PER_BASE macro to point to a stub array indeed. You then have two solutions, depending on how clean the code is. If the base value (0x40003000) is never "generated" outside of SOC_PER_BASE then simply define an array of bytes of exactly the right size, and address it starting from 0. If the address is sometimes computed, you may want to define an array of size 0x40003000+MAX_SIZE and address it from 0x40003000. You won't be able to easily prove that you don't access the stub before this variable though.