config.cpp File Reference

#include <algorithm>
#include <regex>
#include <util/config/config.h>
#include <util/message/message.h>
#include <ac_config.h>

Include dependency graph for config.cpp:

Functions
assert_db &	get_ssa_caching_db ()
	Per-thread SSA assertion cache.
static const eregex	WINDOWS_ABI ("mingw.*|win[0-9]{2}|windows|msys")
static const eregex	FREEBSD ("k?freebsd.*")
static const eregex	MACOS ("macos|osx.*")
static const eregex	X86 ("i[3456]86|x86_64|x64")
static const eregex	ARM ("(arm|thumb|aarch64c?)(eb|_be)?")
static const eregex	MIPS ("mips(64|isa64|isa64sb1)?(r[0-9]+)?(el|le)?.*")
static const eregex	POWERPC ("(ppc|powerpc)(64)?(le)?")
static const eregex	RISCV ("riscv(32|64)(be)?")
static configt::ansi_ct::endianesst	arch_endianness (const std::string &arch)

Variables
configt	config

Function Documentation

arch_endianness()

configt::ansi_ct::endianesst arch_endianness ( const std::string & arch )

static

ARM()

const eregex ARM ( "(arm|thumb|aarch64c?)(eb|_be)?" )

static

FREEBSD()

const eregex FREEBSD ( "k?freebsd.*" )

static

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.

MACOS()

const eregex MACOS ( "macos|osx.*" )

static

MIPS()

const eregex MIPS ( "mips(64|isa64|isa64sb1)?(r[0-9]+)?(el|le)?.*" )

static

POWERPC()

const eregex POWERPC ( "(ppc|powerpc)(64)?(le)?" )

static

RISCV()

const eregex RISCV ( "riscv(32|64)(be)?" )

static

WINDOWS_ABI()

const eregex WINDOWS_ABI ( "mingw.*|win{2}|windows|msys" [0-9] )

static

X86()

const eregex X86 ( "i86|x86_64|x64" [3456] )

static

Variable Documentation

config

configt config