cprover
config.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 
10 #ifndef CPROVER_UTIL_CONFIG_H
11 #define CPROVER_UTIL_CONFIG_H
12 
13 #include <list>
14 
15 #include "ieee_float.h"
16 #include "irep.h"
17 #include "optional.h"
18 
19 class cmdlinet;
20 class symbol_tablet;
21 class namespacet;
22 
25 class configt
26 {
27 public:
28  struct ansi_ct
29  {
30  // for ANSI-C
31  std::size_t int_width;
32  std::size_t long_int_width;
33  std::size_t bool_width;
34  std::size_t char_width;
35  std::size_t short_int_width;
36  std::size_t long_long_int_width;
37  std::size_t pointer_width;
38  std::size_t single_width;
39  std::size_t double_width;
40  std::size_t long_double_width;
41  std::size_t wchar_t_width;
42 
43  // various language options
46  bool ts_18661_3_Floatn_types; // ISO/IEC TS 18661-3:2015
47  bool gcc__float128_type; // __float128, a gcc extension since 4.3/4.5
49  enum class c_standardt { C89, C99, C11 } c_standard;
51 
55 
57 
58  void set_16();
59  void set_32();
60  void set_64();
61 
62  // http://www.unix.org/version2/whatsnew/lp64_wp.html
63  void set_LP64(); // int=32, long=64, pointer=64
64  void set_ILP64(); // int=64, long=64, pointer=64
65  void set_LLP64(); // int=32, long=32, pointer=64
66  void set_ILP32(); // int=32, long=32, pointer=32
67  void set_LP32(); // int=16, long=32, pointer=32
68 
69  // minimum alignment (in structs) measured in bytes
70  std::size_t alignment;
71 
72  // maximum minimum size of the operands for a machine
73  // instruction (in bytes)
74  std::size_t memory_operand_size;
75 
78 
79  enum class ost { NO_OS, OS_LINUX, OS_MACOS, OS_WIN };
81 
82  static std::string os_to_string(ost);
83  static ost string_to_os(const std::string &);
84 
86 
87  // architecture-specific integer value of null pointer constant
89 
90  void set_arch_spec_i386();
91  void set_arch_spec_x86_64();
92  void set_arch_spec_power(const irep_idt &subarch);
93  void set_arch_spec_arm(const irep_idt &subarch);
94  void set_arch_spec_alpha();
95  void set_arch_spec_mips(const irep_idt &subarch);
96  void set_arch_spec_riscv64();
97  void set_arch_spec_s390();
98  void set_arch_spec_s390x();
99  void set_arch_spec_sparc(const irep_idt &subarch);
100  void set_arch_spec_ia64();
101  void set_arch_spec_x32();
102  void set_arch_spec_v850();
103  void set_arch_spec_hppa();
104  void set_arch_spec_sh4();
105 
106  enum class flavourt
107  {
108  NONE,
109  ANSI,
110  GCC,
111  ARM,
112  CLANG,
115  };
116  flavourt mode; // the syntax of source files
117 
119  CODEWARRIOR, ARM };
120  preprocessort preprocessor; // the preprocessor to use
121 
122  std::list<std::string> defines;
123  std::list<std::string> undefines;
124  std::list<std::string> preprocessor_options;
125  std::list<std::string> include_paths;
126  std::list<std::string> include_files;
127 
128  enum class libt { LIB_NONE, LIB_FULL };
130 
132  bool malloc_may_fail = false;
133 
135  {
139  };
140 
142 
143  static const std::size_t default_object_bits=8;
145 
146  struct cppt
147  {
150 
155 
156  static const std::size_t default_object_bits=8;
157  } cpp;
158 
159  struct verilogt
160  {
161  std::list<std::string> include_paths;
163 
164  struct javat
165  {
166  typedef std::list<std::string> classpatht;
169 
170  static const std::size_t default_object_bits=16;
171  } java;
172 
174  {
175  // number of bits to encode heap object addresses
176  std::size_t object_bits = 8;
179 
180  // this is the function to start executing
182 
183  void set_arch(const irep_idt &);
184 
185  void set_from_symbol_table(const symbol_tablet &);
186 
187  bool set(const cmdlinet &cmdline);
188 
190  std::string object_bits_info();
191 
192  static irep_idt this_architecture();
194 
195 private:
196  void set_classpath(const std::string &cp);
197 };
198 
199 extern configt config;
200 
201 #endif // CPROVER_UTIL_CONFIG_H
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
configt::ansi_ct::ts_18661_3_Floatn_types
bool ts_18661_3_Floatn_types
Definition: config.h:46
configt::cppt::cpp_standardt::CPP98
@ CPP98
configt::bv_encodingt::object_bits
std::size_t object_bits
Definition: config.h:176
configt::ansi_ct::defines
std::list< std::string > defines
Definition: config.h:122
configt::ansi_ct::bool_width
std::size_t bool_width
Definition: config.h:33
configt::verilog
struct configt::verilogt verilog
configt::object_bits_info
std::string object_bits_info()
Definition: config.cpp:1291
configt::ansi_ct::set_c99
void set_c99()
Definition: config.h:53
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
configt::cppt
Definition: config.h:147
configt::ansi_ct::NULL_is_zero
bool NULL_is_zero
Definition: config.h:88
configt::javat::main_class
irep_idt main_class
Definition: config.h:168
configt::ansi_ct::string_to_os
static ost string_to_os(const std::string &)
Definition: config.cpp:1141
configt::ansi_ct::ost
ost
Definition: config.h:79
configt::bv_encoding
struct configt::bv_encodingt bv_encoding
configt::ansi_ct::for_has_scope
bool for_has_scope
Definition: config.h:45
configt::cppt::cpp_standardt
cpp_standardt
Definition: config.h:148
configt::ansi_ct::set_arch_spec_s390x
void set_arch_spec_s390x()
Definition: config.cpp:457
configt::ansi_ct::wchar_t_width
std::size_t wchar_t_width
Definition: config.h:41
configt::ansi_ct::endiannesst
endiannesst
Definition: config.h:76
configt::ansi_ct::ost::OS_MACOS
@ OS_MACOS
configt::ansi_ct::preprocessort::CLANG
@ CLANG
configt::ansi_ct::include_paths
std::list< std::string > include_paths
Definition: config.h:125
configt::ansi_ct::malloc_failure_mode_assert_then_assume
@ malloc_failure_mode_assert_then_assume
Definition: config.h:138
configt::ansi_ct::flavourt::CODEWARRIOR
@ CODEWARRIOR
optional.h
configt::ansi_ct::set_arch_spec_mips
void set_arch_spec_mips(const irep_idt &subarch)
Definition: config.cpp:352
configt::ansi_ct::os
ost os
Definition: config.h:80
configt::cppt::cpp_standardt::CPP03
@ CPP03
configt::ansi_ct::flavourt::VISUAL_STUDIO
@ VISUAL_STUDIO
configt::ansi_ct::set_32
void set_32()
Definition: config.cpp:31
configt::ansi_ct::set_64
void set_64()
Definition: config.cpp:36
configt::main
optionalt< std::string > main
Definition: config.h:181
configt::ansi_ct::set_arch_spec_i386
void set_arch_spec_i386()
Definition: config.cpp:149
configt::ansi_ct::set_16
void set_16()
Definition: config.cpp:26
configt::ansi_ct::rounding_mode
ieee_floatt::rounding_modet rounding_mode
Definition: config.h:56
configt::ansi_ct::alignment
std::size_t alignment
Definition: config.h:70
configt::ansi_ct::set_LP32
void set_LP32()
int=16, long=32, pointer=32
Definition: config.cpp:130
configt::ansi_ct::set_arch_spec_power
void set_arch_spec_power(const irep_idt &subarch)
Definition: config.cpp:219
configt::ansi_ct::undefines
std::list< std::string > undefines
Definition: config.h:123
configt::ansi_c
struct configt::ansi_ct ansi_c
configt::ansi_ct::flavourt::ARM
@ ARM
configt::ansi_ct::set_arch_spec_hppa
void set_arch_spec_hppa()
Definition: config.cpp:616
configt::javat::classpath
classpatht classpath
Definition: config.h:167
configt::ansi_ct::libt::LIB_NONE
@ LIB_NONE
configt::ansi_ct::flavourt::CLANG
@ CLANG
configt::ansi_ct
Definition: config.h:29
configt
Globally accessible architectural configuration.
Definition: config.h:26
configt::ansi_ct::flavourt::NONE
@ NONE
configt::ansi_ct::char_width
std::size_t char_width
Definition: config.h:34
configt::cppt::set_cpp98
void set_cpp98()
Definition: config.h:151
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
configt::ansi_ct::endiannesst::NO_ENDIANNESS
@ NO_ENDIANNESS
configt::ansi_ct::set_arch_spec_ia64
void set_arch_spec_ia64()
Definition: config.cpp:525
config
configt config
Definition: config.cpp:24
configt::ansi_ct::libt
libt
Definition: config.h:128
configt::ansi_ct::endiannesst::IS_LITTLE_ENDIAN
@ IS_LITTLE_ENDIAN
configt::bv_encodingt
Definition: config.h:174
configt::ansi_ct::c_standardt::C89
@ C89
configt::cppt::set_cpp14
void set_cpp14()
Definition: config.h:154
cmdlinet
Definition: cmdline.h:21
configt::ansi_ct::set_arch_spec_arm
void set_arch_spec_arm(const irep_idt &subarch)
Definition: config.cpp:280
configt::ansi_ct::wchar_t_is_unsigned
bool wchar_t_is_unsigned
Definition: config.h:44
configt::ansi_ct::set_arch_spec_s390
void set_arch_spec_s390()
Definition: config.cpp:428
configt::ansi_ct::double_width
std::size_t double_width
Definition: config.h:39
configt::ansi_ct::preprocessor
preprocessort preprocessor
Definition: config.h:120
configt::ansi_ct::malloc_failure_mode_return_null
@ malloc_failure_mode_return_null
Definition: config.h:137
configt::ansi_ct::set_arch_spec_riscv64
void set_arch_spec_riscv64()
Definition: config.cpp:402
configt::verilogt::include_paths
std::list< std::string > include_paths
Definition: config.h:161
configt::ansi_ct::default_object_bits
static const std::size_t default_object_bits
Definition: config.h:143
configt::cppt::default_object_bits
static const std::size_t default_object_bits
Definition: config.h:156
configt::ansi_ct::string_abstraction
bool string_abstraction
Definition: config.h:131
configt::ansi_ct::set_arch_spec_alpha
void set_arch_spec_alpha()
Definition: config.cpp:323
configt::bv_encodingt::is_object_bits_default
bool is_object_bits_default
Definition: config.h:177
configt::cppt::set_cpp11
void set_cpp11()
Definition: config.h:153
configt::ansi_ct::memory_operand_size
std::size_t memory_operand_size
Definition: config.h:74
configt::ansi_ct::ost::OS_LINUX
@ OS_LINUX
configt::ansi_ct::flavourt::ANSI
@ ANSI
configt::ansi_ct::set_ILP64
void set_ILP64()
int=64, long=64, pointer=64
Definition: config.cpp:70
configt::ansi_ct::long_long_int_width
std::size_t long_long_int_width
Definition: config.h:36
configt::this_operating_system
static irep_idt this_operating_system()
Definition: config.cpp:1402
configt::ansi_ct::malloc_failure_mode_none
@ malloc_failure_mode_none
Definition: config.h:136
configt::javat::classpatht
std::list< std::string > classpatht
Definition: config.h:166
configt::ansi_ct::arch
irep_idt arch
Definition: config.h:85
configt::ansi_ct::ost::OS_WIN
@ OS_WIN
configt::ansi_ct::set_LLP64
void set_LLP64()
int=32, long=32, pointer=64
Definition: config.cpp:90
configt::set_from_symbol_table
void set_from_symbol_table(const symbol_tablet &)
Definition: config.cpp:1205
ieee_floatt::rounding_modet
rounding_modet
Definition: ieee_float.h:126
configt::ansi_ct::os_to_string
static std::string os_to_string(ost)
Definition: config.cpp:1126
configt::javat::default_object_bits
static const std::size_t default_object_bits
Definition: config.h:170
configt::ansi_ct::preprocessor_options
std::list< std::string > preprocessor_options
Definition: config.h:124
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
configt::ansi_ct::include_files
std::list< std::string > include_files
Definition: config.h:126
configt::ansi_ct::ost::NO_OS
@ NO_OS
configt::ansi_ct::preprocessort::GCC
@ GCC
configt::ansi_ct::set_ILP32
void set_ILP32()
int=32, long=32, pointer=32
Definition: config.cpp:110
configt::ansi_ct::default_c_standard
static c_standardt default_c_standard()
Definition: config.cpp:675
configt::ansi_ct::c_standardt::C99
@ C99
configt::ansi_ct::preprocessort::NONE
@ NONE
configt::ansi_ct::set_c11
void set_c11()
Definition: config.h:54
configt::this_architecture
static irep_idt this_architecture()
Definition: config.cpp:1302
configt::ansi_ct::libt::LIB_FULL
@ LIB_FULL
configt::verilogt
Definition: config.h:160
configt::ansi_ct::mode
flavourt mode
Definition: config.h:116
configt::ansi_ct::c_standardt::C11
@ C11
preprocessort
Definition: preprocessor.h:21
configt::ansi_ct::set_c89
void set_c89()
Definition: config.h:52
configt::ansi_ct::preprocessort::VISUAL_STUDIO
@ VISUAL_STUDIO
configt::ansi_ct::endiannesst::IS_BIG_ENDIAN
@ IS_BIG_ENDIAN
configt::set
bool set(const cmdlinet &cmdline)
Definition: config.cpp:798
configt::cppt::default_cpp_standard
static cpp_standardt default_cpp_standard()
Definition: config.cpp:690
configt::ansi_ct::c_standard
enum configt::ansi_ct::c_standardt c_standard
configt::ansi_ct::set_arch_spec_sparc
void set_arch_spec_sparc(const irep_idt &subarch)
Definition: config.cpp:485
ieee_float.h
configt::ansi_ct::set_LP64
void set_LP64()
int=32, long=64, pointer=64
Definition: config.cpp:46
configt::ansi_ct::set_arch_spec_sh4
void set_arch_spec_sh4()
Definition: config.cpp:645
configt::ansi_ct::long_double_width
std::size_t long_double_width
Definition: config.h:40
configt::java
struct configt::javat java
configt::cppt::cpp_standardt::CPP14
@ CPP14
configt::ansi_ct::set_arch_spec_v850
void set_arch_spec_v850()
Sets up the widths of variables for the Renesas V850.
Definition: config.cpp:593
configt::ansi_ct::short_int_width
std::size_t short_int_width
Definition: config.h:35
configt::ansi_ct::char_is_unsigned
bool char_is_unsigned
Definition: config.h:44
configt::ansi_ct::flavourt::GCC
@ GCC
configt::ansi_ct::set_arch_spec_x86_64
void set_arch_spec_x86_64()
Definition: config.cpp:181
configt::cppt::cpp_standardt::CPP11
@ CPP11
configt::ansi_ct::set_arch_spec_x32
void set_arch_spec_x32()
Definition: config.cpp:556
configt::ansi_ct::malloc_failure_mode
malloc_failure_modet malloc_failure_mode
Definition: config.h:141
configt::ansi_ct::pointer_width
std::size_t pointer_width
Definition: config.h:37
configt::ansi_ct::single_width
std::size_t single_width
Definition: config.h:38
configt::ansi_ct::flavourt
flavourt
Definition: config.h:107
configt::ansi_ct::lib
libt lib
Definition: config.h:129
configt::cpp
struct configt::cppt cpp
configt::ansi_ct::malloc_failure_modet
malloc_failure_modet
Definition: config.h:135
configt::set_classpath
void set_classpath(const std::string &cp)
Definition: config.cpp:1386
configt::ansi_ct::malloc_may_fail
bool malloc_may_fail
Definition: config.h:132
configt::ansi_ct::single_precision_constant
bool single_precision_constant
Definition: config.h:48
configt::ansi_ct::gcc__float128_type
bool gcc__float128_type
Definition: config.h:47
configt::set_object_bits_from_symbol_table
void set_object_bits_from_symbol_table(const symbol_tablet &)
Sets the number of bits used for object addresses.
Definition: config.cpp:1266
configt::ansi_ct::c_standardt
c_standardt
Definition: config.h:49
configt::set_arch
void set_arch(const irep_idt &)
Definition: config.cpp:702
configt::ansi_ct::int_width
std::size_t int_width
Definition: config.h:31
configt::javat
Definition: config.h:165
configt::ansi_ct::preprocessort::ARM
@ ARM
configt::ansi_ct::preprocessort::CODEWARRIOR
@ CODEWARRIOR
configt::ansi_ct::endianness
endiannesst endianness
Definition: config.h:77
configt::ansi_ct::long_int_width
std::size_t long_int_width
Definition: config.h:32
irep.h
configt::cppt::cpp_standard
enum configt::cppt::cpp_standardt cpp_standard
configt::cppt::set_cpp03
void set_cpp03()
Definition: config.h:152