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

There are many peripherals to update. I am using the text 'SOC_PER' as a stand in for things like 'UART1', 'SPI2', 'I2C4', etc. Or `IWDG`... as the quoted eva text produces. — artless noise, Apr 21 '23 at 19:08
*FRAMAC_SOURCE* is used [here](https://github.com/jcarrano/fixed_point_arith/blob/master/Makefile), possibly as a conditional... — artless noise, Apr 21 '23 at 19:29
A similar topic is data structures (arrays) provided by the linker which maybe generated datasets, images, video, or sound files that are used as part of the image. Generally, I have the linker generate a 'size' of the array for systems where a file system is not present. Ie, they are fixed sized memory arrays, like the SOC register banks. — artless noise, Apr 21 '23 at 21:14
Have you considered using `-absolute-valid-range 0x40003000-` ? That option is made for direct memory-mapped hardware accesses. — anol, Apr 22 '23 at 19:47

score 2 · Accepted Answer · answered Apr 23 '23 at 09:57

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.

Thanks. I will use some conditionals. I guess there is no standard 'FRAMAC' pre-defined by the tool. I can add it to the command line. There are many areas that are allocated outside standard 'C' allocation specs. The SOC register range will have holes in it and some conditionalization can document these regions. I think it is a much better option than '-absolute-valid-range' as command line options are more difficult to document. — artless noise, Apr 24 '23 at 14:48

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

1 Answers1