#include <config.h>

Collaboration diagram for configt::ansi_ct:

Public Types
enum class	c_standardt { C89 , C99 , C11 , C17 , C23 }

enum class	endiannesst { NO_ENDIANNESS , IS_LITTLE_ENDIAN , IS_BIG_ENDIAN }

enum class	argument_evaluation_ordert { LEFT_TO_RIGHT , RIGHT_TO_LEFT }

enum class	ost { NO_OS , OS_LINUX , OS_MACOS , OS_WIN }

enum class	flavourt { NONE , ANSI , GCC , ARM , CLANG , VISUAL_STUDIO , CODEWARRIOR }

enum class	preprocessort { NONE , GCC , CLANG , VISUAL_STUDIO , CODEWARRIOR , ARM }

enum class	libt { LIB_NONE , LIB_FULL }

enum	malloc_failure_modet { malloc_failure_mode_none = 0 , malloc_failure_mode_return_null = 1 , malloc_failure_mode_assert_then_assume = 2 }

Public Member Functions
void	set_c89 ()

void	set_c99 ()

void	set_c11 ()

void	set_c17 ()

void	set_c23 ()

void	set_16 ()

void	set_32 ()

void	set_64 ()

void	set_LP64 ()
	int=32, long=64, pointer=64

void	set_ILP64 ()
	int=64, long=64, pointer=64

void	set_LLP64 ()
	int=32, long=32, pointer=64

void	set_ILP32 ()
	int=32, long=32, pointer=32

void	set_LP32 ()
	int=16, long=32, pointer=32

void	set_argument_evaluation_order ()
	Sets the architectural parameter recording the order in which compilers evaluate the arguments of a function call from `mode` and `arch_is_x86_family`: Visual Studio evaluates right-to-left on all architectures (verified on x86, x64, arm64), GCC evaluates right-to-left on the x86 family only, and left-to-right is used in all other cases.

void	set_arch_spec_i386 ()

void	set_arch_spec_x86_64 ()

void	set_arch_spec_power (const irep_idt &subarch)

void	set_arch_spec_arm (const irep_idt &subarch)

void	set_arch_spec_alpha ()

void	set_arch_spec_mips (const irep_idt &subarch)

void	set_arch_spec_riscv64 ()

void	set_arch_spec_s390 ()

void	set_arch_spec_s390x ()

void	set_arch_spec_sparc (const irep_idt &subarch)

void	set_arch_spec_ia64 ()

void	set_arch_spec_x32 ()

void	set_arch_spec_v850 ()
	Sets up the widths of variables for the Renesas V850.

void	set_arch_spec_hppa ()

void	set_arch_spec_sh4 ()

void	set_arch_spec_loongarch64 ()

void	set_arch_spec_emscripten ()

Static Public Member Functions
static c_standardt	default_c_standard ()

static std::string	os_to_string (ost)

static ost	string_to_os (const std::string &)

Public Attributes
std::size_t	int_width

std::size_t	long_int_width

std::size_t	bool_width

std::size_t	char_width

std::size_t	short_int_width

std::size_t	long_long_int_width

std::size_t	pointer_width

std::size_t	single_width

std::size_t	double_width

std::size_t	long_double_width

std::size_t	wchar_t_width

bool	char_is_unsigned

bool	wchar_t_is_unsigned

bool	for_has_scope

bool	ts_18661_3_Floatn_types

bool	gcc__float128_type

bool	__float128_is_keyword

bool	float16_type

bool	bf16_type

bool	fp16_type

bool	single_precision_constant

bool	allow_anonymous_struct_embedding

enum configt::ansi_ct::c_standardt	c_standard

ieee_floatt::rounding_modet	rounding_mode

std::size_t	alignment

std::size_t	memory_operand_size

endiannesst	endianness

argument_evaluation_ordert	argument_evaluation_order

bool	arch_is_x86_family = false

ost	os

irep_idt	arch

bool	NULL_is_zero

flavourt	mode

preprocessort	preprocessor

std::list< std::string >	defines

std::list< std::string >	undefines

std::list< std::string >	preprocessor_options

std::list< std::string >	include_paths

std::list< std::string >	include_files

libt	lib

bool	string_abstraction

bool	malloc_may_fail = true

bool	dfcc_debug_lib = false
	enable debug code in cprover_contracts library

bool	simple_invalid_pointer_model = false
	use simplified invalid pointer model in cprover_contracts library

malloc_failure_modet	malloc_failure_mode = malloc_failure_mode_return_null

std::optional< mp_integer >	max_argc
	Maximum value of argc, which is operating-systems dependent: Windows limits the number of characters accepte by CreateProcess, and Unix systems have sysconf(ARG_MAX).

Static Public Attributes
static const std::size_t	default_object_bits = 8

Detailed Description

Definition at line 146 of file config.h.

Member Enumeration Documentation

◆ argument_evaluation_ordert

enum class configt::ansi_ct::argument_evaluation_ordert

strong

Enumerator
LEFT_TO_RIGHT
RIGHT_TO_LEFT

Definition at line 247 of file config.h.

◆ c_standardt

enum class configt::ansi_ct::c_standardt

strong

Enumerator
C89
C99
C11
C17
C23

Definition at line 172 of file config.h.

◆ endiannesst

enum class configt::ansi_ct::endiannesst

strong

Enumerator
NO_ENDIANNESS
IS_LITTLE_ENDIAN
IS_BIG_ENDIAN

Definition at line 228 of file config.h.

◆ flavourt

enum class configt::ansi_ct::flavourt

strong

Enumerator
NONE
ANSI
GCC
ARM
CLANG
VISUAL_STUDIO
CODEWARRIOR

Definition at line 297 of file config.h.

◆ libt

enum class configt::ansi_ct::libt

strong

Enumerator
LIB_NONE
LIB_FULL

Definition at line 326 of file config.h.

◆ malloc_failure_modet

enum configt::ansi_ct::malloc_failure_modet

Enumerator
malloc_failure_mode_none
malloc_failure_mode_return_null
malloc_failure_mode_assert_then_assume

Definition at line 342 of file config.h.

◆ ost

enum class configt::ansi_ct::ost

strong

Enumerator
NO_OS
OS_LINUX
OS_MACOS
OS_WIN

Definition at line 262 of file config.h.

◆ preprocessort

enum class configt::ansi_ct::preprocessort

strong

Enumerator
NONE
GCC
CLANG
VISUAL_STUDIO
CODEWARRIOR
ARM

Definition at line 309 of file config.h.

Member Function Documentation

◆ default_c_standard()

configt::ansi_ct::c_standardt configt::ansi_ct::default_c_standard ( )

static

Definition at line 789 of file config.cpp.

◆ os_to_string()

std::string configt::ansi_ct::os_to_string ( ost os )

static

Definition at line 1340 of file config.cpp.

◆ set_16()

void configt::ansi_ct::set_16 ( )

Definition at line 27 of file config.cpp.

◆ set_32()

void configt::ansi_ct::set_32 ( )

Definition at line 32 of file config.cpp.

◆ set_64()

void configt::ansi_ct::set_64 ( )

Definition at line 37 of file config.cpp.

◆ set_arch_spec_alpha()

void configt::ansi_ct::set_arch_spec_alpha ( )

Definition at line 354 of file config.cpp.

◆ set_arch_spec_arm()

void configt::ansi_ct::set_arch_spec_arm ( const irep_idt & subarch )

Definition at line 306 of file config.cpp.

◆ set_arch_spec_emscripten()

void configt::ansi_ct::set_arch_spec_emscripten ( )

Definition at line 758 of file config.cpp.

◆ set_arch_spec_hppa()

void configt::ansi_ct::set_arch_spec_hppa ( )

Definition at line 664 of file config.cpp.

◆ set_arch_spec_i386()

void configt::ansi_ct::set_arch_spec_i386 ( )

Definition at line 169 of file config.cpp.

◆ set_arch_spec_ia64()

void configt::ansi_ct::set_arch_spec_ia64 ( )

Definition at line 568 of file config.cpp.

◆ set_arch_spec_loongarch64()

void configt::ansi_ct::set_arch_spec_loongarch64 ( )

Definition at line 727 of file config.cpp.

◆ set_arch_spec_mips()

void configt::ansi_ct::set_arch_spec_mips ( const irep_idt & subarch )

Definition at line 385 of file config.cpp.

◆ set_arch_spec_power()

void configt::ansi_ct::set_arch_spec_power ( const irep_idt & subarch )

Definition at line 243 of file config.cpp.

◆ set_arch_spec_riscv64()

void configt::ansi_ct::set_arch_spec_riscv64 ( )

Definition at line 437 of file config.cpp.

◆ set_arch_spec_s390()

void configt::ansi_ct::set_arch_spec_s390 ( )

Definition at line 465 of file config.cpp.

◆ set_arch_spec_s390x()

void configt::ansi_ct::set_arch_spec_s390x ( )

Definition at line 496 of file config.cpp.

◆ set_arch_spec_sh4()

void configt::ansi_ct::set_arch_spec_sh4 ( )

Definition at line 695 of file config.cpp.

◆ set_arch_spec_sparc()

void configt::ansi_ct::set_arch_spec_sparc ( const irep_idt & subarch )

Definition at line 526 of file config.cpp.

◆ set_arch_spec_v850()

void configt::ansi_ct::set_arch_spec_v850 ( )

Sets up the widths of variables for the Renesas V850.

Definition at line 639 of file config.cpp.

◆ set_arch_spec_x32()

void configt::ansi_ct::set_arch_spec_x32 ( )

Definition at line 601 of file config.cpp.

◆ set_arch_spec_x86_64()

void configt::ansi_ct::set_arch_spec_x86_64 ( )

Definition at line 203 of file config.cpp.

◆ set_argument_evaluation_order()

void configt::ansi_ct::set_argument_evaluation_order ( )

Sets the architectural parameter recording the order in which compilers evaluate the arguments of a function call from mode and arch_is_x86_family: Visual Studio evaluates right-to-left on all architectures (verified on x86, x64, arm64), GCC evaluates right-to-left on the x86 family only, and left-to-right is used in all other cases.

This needs to be re-invoked when either input changes; in particular, goto-cc switches mode after the architecture has been configured.

Definition at line 157 of file config.cpp.

◆ set_c11()

void configt::ansi_ct::set_c11 ( )

inline

Definition at line 192 of file config.h.

◆ set_c17()

void configt::ansi_ct::set_c17 ( )

inline

Definition at line 197 of file config.h.

◆ set_c23()

void configt::ansi_ct::set_c23 ( )

inline

Definition at line 202 of file config.h.

◆ set_c89()

void configt::ansi_ct::set_c89 ( )

inline

Definition at line 182 of file config.h.

◆ set_c99()

void configt::ansi_ct::set_c99 ( )

inline

Definition at line 187 of file config.h.

◆ set_ILP32()

void configt::ansi_ct::set_ILP32 ( )

int=32, long=32, pointer=32

Definition at line 111 of file config.cpp.

◆ set_ILP64()

void configt::ansi_ct::set_ILP64 ( )

int=64, long=64, pointer=64

Definition at line 71 of file config.cpp.

◆ set_LLP64()

void configt::ansi_ct::set_LLP64 ( )

int=32, long=32, pointer=64

Definition at line 91 of file config.cpp.

◆ set_LP32()

void configt::ansi_ct::set_LP32 ( )

int=16, long=32, pointer=32

Definition at line 131 of file config.cpp.

◆ set_LP64()

void configt::ansi_ct::set_LP64 ( )

int=32, long=64, pointer=64

Definition at line 47 of file config.cpp.

◆ string_to_os()

configt::ansi_ct::ost configt::ansi_ct::string_to_os ( const std::string & os )

static

Definition at line 1355 of file config.cpp.

Member Data Documentation

◆ __float128_is_keyword

bool configt::ansi_ct::__float128_is_keyword

Definition at line 166 of file config.h.

◆ alignment

std::size_t configt::ansi_ct::alignment

Definition at line 222 of file config.h.

◆ allow_anonymous_struct_embedding

bool configt::ansi_ct::allow_anonymous_struct_embedding

Definition at line 171 of file config.h.

◆ arch

irep_idt configt::ansi_ct::arch

Definition at line 274 of file config.h.

◆ arch_is_x86_family

bool configt::ansi_ct::arch_is_x86_family = false

Definition at line 258 of file config.h.

◆ argument_evaluation_order

argument_evaluation_ordert configt::ansi_ct::argument_evaluation_order

Definition at line 252 of file config.h.

◆ bf16_type

bool configt::ansi_ct::bf16_type

Definition at line 168 of file config.h.

◆ bool_width

std::size_t configt::ansi_ct::bool_width

Definition at line 151 of file config.h.

◆ c_standard

enum configt::ansi_ct::c_standardt configt::ansi_ct::c_standard

◆ char_is_unsigned

bool configt::ansi_ct::char_is_unsigned

Definition at line 162 of file config.h.

◆ char_width

std::size_t configt::ansi_ct::char_width

Definition at line 152 of file config.h.

◆ default_object_bits

const std::size_t configt::ansi_ct::default_object_bits = 8

static

Definition at line 351 of file config.h.

◆ defines

std::list<std::string> configt::ansi_ct::defines

Definition at line 320 of file config.h.

◆ dfcc_debug_lib

bool configt::ansi_ct::dfcc_debug_lib = false

enable debug code in cprover_contracts library

Definition at line 337 of file config.h.

◆ double_width

std::size_t configt::ansi_ct::double_width

Definition at line 157 of file config.h.

◆ endianness

endiannesst configt::ansi_ct::endianness

Definition at line 234 of file config.h.

◆ float16_type

bool configt::ansi_ct::float16_type

Definition at line 167 of file config.h.

◆ for_has_scope

bool configt::ansi_ct::for_has_scope

Definition at line 163 of file config.h.

◆ fp16_type

bool configt::ansi_ct::fp16_type

Definition at line 169 of file config.h.

◆ gcc__float128_type

bool configt::ansi_ct::gcc__float128_type

Definition at line 165 of file config.h.

◆ include_files

std::list<std::string> configt::ansi_ct::include_files

Definition at line 324 of file config.h.

◆ include_paths

std::list<std::string> configt::ansi_ct::include_paths

Definition at line 323 of file config.h.

◆ int_width

std::size_t configt::ansi_ct::int_width

Definition at line 149 of file config.h.

◆ lib

libt configt::ansi_ct::lib

Definition at line 331 of file config.h.

◆ long_double_width

std::size_t configt::ansi_ct::long_double_width

Definition at line 158 of file config.h.

◆ long_int_width

std::size_t configt::ansi_ct::long_int_width

Definition at line 150 of file config.h.

◆ long_long_int_width

std::size_t configt::ansi_ct::long_long_int_width

Definition at line 154 of file config.h.

◆ malloc_failure_mode

malloc_failure_modet configt::ansi_ct::malloc_failure_mode = malloc_failure_mode_return_null

Definition at line 349 of file config.h.

◆ malloc_may_fail

bool configt::ansi_ct::malloc_may_fail = true

Definition at line 334 of file config.h.

◆ max_argc

std::optional<mp_integer> configt::ansi_ct::max_argc

Maximum value of argc, which is operating-systems dependent: Windows limits the number of characters accepte by CreateProcess, and Unix systems have sysconf(ARG_MAX).

Definition at line 356 of file config.h.

◆ memory_operand_size

std::size_t configt::ansi_ct::memory_operand_size

Definition at line 226 of file config.h.

◆ mode

flavourt configt::ansi_ct::mode

Definition at line 307 of file config.h.

◆ NULL_is_zero

bool configt::ansi_ct::NULL_is_zero

Definition at line 277 of file config.h.

◆ os

ost configt::ansi_ct::os

Definition at line 269 of file config.h.

◆ pointer_width

std::size_t configt::ansi_ct::pointer_width

Definition at line 155 of file config.h.

◆ preprocessor

preprocessort configt::ansi_ct::preprocessor

Definition at line 318 of file config.h.

◆ preprocessor_options

std::list<std::string> configt::ansi_ct::preprocessor_options

Definition at line 322 of file config.h.

◆ rounding_mode

ieee_floatt::rounding_modet configt::ansi_ct::rounding_mode

Definition at line 208 of file config.h.

◆ short_int_width

std::size_t configt::ansi_ct::short_int_width

Definition at line 153 of file config.h.

◆ simple_invalid_pointer_model

bool configt::ansi_ct::simple_invalid_pointer_model = false

use simplified invalid pointer model in cprover_contracts library

Definition at line 340 of file config.h.

◆ single_precision_constant

bool configt::ansi_ct::single_precision_constant

Definition at line 170 of file config.h.

◆ single_width

std::size_t configt::ansi_ct::single_width

Definition at line 156 of file config.h.

◆ string_abstraction

bool configt::ansi_ct::string_abstraction

Definition at line 333 of file config.h.

◆ ts_18661_3_Floatn_types

bool configt::ansi_ct::ts_18661_3_Floatn_types

Definition at line 164 of file config.h.

◆ undefines

std::list<std::string> configt::ansi_ct::undefines

Definition at line 321 of file config.h.

◆ wchar_t_is_unsigned

bool configt::ansi_ct::wchar_t_is_unsigned

Definition at line 162 of file config.h.

◆ wchar_t_width

std::size_t configt::ansi_ct::wchar_t_width

Definition at line 159 of file config.h.

The documentation for this struct was generated from the following files:

/home/runner/work/cbmc/cbmc/src/util/config.h
/home/runner/work/cbmc/cbmc/src/util/config.cpp

Public Types

Public Member Functions

Static Public Member Functions

Public Attributes

Static Public Attributes

Detailed Description

Member Enumeration Documentation

◆ argument_evaluation_ordert

◆ c_standardt

◆ endiannesst

◆ flavourt

◆ libt

◆ malloc_failure_modet

◆ ost

◆ preprocessort

Member Function Documentation

◆ default_c_standard()

◆ os_to_string()

◆ set_16()

◆ set_32()

◆ set_64()

◆ set_arch_spec_alpha()

◆ set_arch_spec_arm()

◆ set_arch_spec_emscripten()

◆ set_arch_spec_hppa()

◆ set_arch_spec_i386()

◆ set_arch_spec_ia64()

◆ set_arch_spec_loongarch64()

◆ set_arch_spec_mips()

◆ set_arch_spec_power()

◆ set_arch_spec_riscv64()

◆ set_arch_spec_s390()

◆ set_arch_spec_s390x()

◆ set_arch_spec_sh4()

◆ set_arch_spec_sparc()

◆ set_arch_spec_v850()

◆ set_arch_spec_x32()

◆ set_arch_spec_x86_64()

◆ set_argument_evaluation_order()

◆ set_c11()

◆ set_c17()

◆ set_c23()

◆ set_c89()

◆ set_c99()

◆ set_ILP32()

◆ set_ILP64()

◆ set_LLP64()

◆ set_LP32()

◆ set_LP64()

◆ string_to_os()

Member Data Documentation

◆ __float128_is_keyword

◆ alignment

◆ allow_anonymous_struct_embedding

◆ arch

◆ arch_is_x86_family

◆ argument_evaluation_order

◆ bf16_type

◆ bool_width

◆ c_standard

◆ char_is_unsigned

◆ char_width

◆ default_object_bits

◆ defines

◆ dfcc_debug_lib

◆ double_width

◆ endianness

◆ float16_type

◆ for_has_scope

◆ fp16_type

◆ gcc__float128_type

◆ include_files

◆ include_paths

◆ int_width

◆ lib

◆ long_double_width

◆ long_int_width

◆ long_long_int_width

◆ malloc_failure_mode

◆ malloc_may_fail