portugalfuturista/seL4
2
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

utils: wrap config_set for verification

Browse source 
Wrap config_set macro in a static inline function so that verification
automation does not simplify away dead code branches based on it, but
the compiler still does.

In most parts of the proofs we want to pretend that we don't know the
config value yet and consider both options. This makes the proofs more
independent on the config value that is selected.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
Gerwin Klein 2025-03-20 09:58:09 +11:00
parent f7b95a9756
commit 6d8b1eaeec
1 changed files with 10 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
include/util.h
View file

@ -109,8 +109,16 @@ void __builtin_unreachable(void);
/* need that for compiling with c99 instead of gnu99 */
#define asm __asm__
/* Evaluate a Kconfig-provided configuration setting at compile-time. */
#define config_set(macro) _is_set_(macro)
/* Wrapping an int literal such as 0 or 1 in a function to prevent it from being
simplified away in verification while still allowing the compiler to optimise
it out and do code elimination on the result. */
static inline int wrap_config_set(int x)
{
return x;
}
/* Evaluate a CMake configuration setting at compile-time. */
#define config_set(macro) wrap_config_set(_is_set_(macro))
#define _macrotest_1 ,
#define _is_set_(value) _is_set__(_macrotest_##value)
#define _is_set__(comma) _is_set___(comma 1, 0)