config.h File Reference

#include <unordered_set>
#include <util/config/cmdline.h>
#include <util/config/options.h>
#include <langapi/mode.h>
#include <util/base/compiler_defs.h>
#include <util/ssa/cache_defs.h>

Include dependency graph for config.h:

Go to the source code of this file.

Classes
class	configt
struct	configt::triple
struct	configt::language_stdt
struct	configt::ansi_ct

Macros
#define	dm(char, short, int, long, addr, word, long_dbl)

Enumerations
enum class	c_stdt {   unknown , c89 , c99 , c11 ,   c17 , c23 , c26 }
	C standard version, ordered so that comparisons work naturally. More...
enum class	cxx_stdt {   unknown , cpp98 , cpp11 , cpp14 ,   cpp17 , cpp20 , cpp23 , cpp26 }
	C++ standard version, ordered so that comparisons work naturally. More...

Functions
assert_db &	get_ssa_caching_db ()
	Per-thread SSA assertion cache.

Variables
configt	config

Macro Definition Documentation

dm

#define dm	(		char,
			short,
			int,
			long,
			addr,
			word,
			long_dbl )

Value:

  ((uint64_t)(char) | (uint64_t)(short) << 8 | (uint64_t)(int) << 16 |         \
   (uint64_t)(long) << 24 | (uint64_t)(addr) << 32 | (uint64_t)(word) << 40 |  \
   (uint64_t)(long_dbl) << 48)

Enumeration Type Documentation

c_stdt

enum class c_stdt

strong

C standard version, ordered so that comparisons work naturally.

Enumerator
unknown
c89
c99
c11
c17
c23
c26

cxx_stdt

enum class cxx_stdt

strong

C++ standard version, ordered so that comparisons work naturally.

Enumerator
unknown
cpp98
cpp11
cpp14
cpp17
cpp20
cpp23
cpp26

Function Documentation

get_ssa_caching_db()

assert_db & get_ssa_caching_db

(

)

Per-thread SSA assertion cache.

Was a member of configt and therefore process-global; the thread-based parallel k-induction (BC, FC, IS running concurrently) hit it as a soundness bug — BC marking an assertion as discharged would let IS reach a vacuous UNSAT, declaring safety on programs with real bugs (issue surfaced on regression/k-induction-parallel/ linear_search_bug). The fork-based parallel previously side-stepped this via process isolation.

Variable Documentation

config

configt config

extern