ACSL in autogenerated source files

Introduction

A lot of source files are generated:

• from SVD specification of the SoC for kernel drivers
• drom device trees for managers, using python dts-utils (see dts/examples)

In both case, source files are suffixed .in and hold jinja content to forge C code from python dictionary

ACSL in autogenerated files

Generated hardware IP definitions from SVD (register address, offset, name and access mode (read-only or read-write).

As SVD files are considered valid (hypothesis), some ACSL code is generated so that any register access method in a given driver can use ACSL lema and axiomatics in order to demonstrate that only SVD-valid local-IP relative registers are accessed.

For device-tree based content, some ACSL can be added for various use cases such as device table access index control, etc.

limitation of autogenerated files and frama-C

When using meson generator to forge C or H files, these files are generated in a separated directory that can't be used through the db input reading from frama-C, and needs to be replaced by another meson generation model using custom_target().

By now, we have replaced, in the kernel/src/arch subdir, the usage of generators with custom targets, but this make the meson syntax heavy.