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 
18 class cmdlinet;
19 class symbol_tablet;
20 class namespacet;
21 
24 class configt
25 {
26 public:
27  struct ansi_ct
28  {
29  // for ANSI-C
30  std::size_t int_width;
31  std::size_t long_int_width;
32  std::size_t bool_width;
33  std::size_t char_width;
34  std::size_t short_int_width;
35  std::size_t long_long_int_width;
36  std::size_t pointer_width;
37  std::size_t single_width;
38  std::size_t double_width;
39  std::size_t long_double_width;
40  std::size_t wchar_t_width;
41 
42  // various language options
45  bool ts_18661_3_Floatn_types; // ISO/IEC TS 18661-3:2015
48  enum class c_standardt { C89, C99, C11 } c_standard;
50 
54 
56 
57  void set_16();
58  void set_32();
59  void set_64();
60 
61  // http://www.unix.org/version2/whatsnew/lp64_wp.html
62  void set_LP64(); // int=32, long=64, pointer=64
63  void set_ILP64(); // int=64, long=64, pointer=64
64  void set_LLP64(); // int=32, long=32, pointer=64
65  void set_ILP32(); // int=32, long=32, pointer=32
66  void set_LP32(); // int=16, long=32, pointer=32
67 
68  // minimum alignment (in structs) measured in bytes
69  std::size_t alignment;
70 
71  // maximum minimum size of the operands for a machine
72  // instruction (in bytes)
73  std::size_t memory_operand_size;
74 
77 
78  enum class ost { NO_OS, OS_LINUX, OS_MACOS, OS_WIN };
80 
81  static std::string os_to_string(ost);
82  static ost string_to_os(const std::string &);
83 
85 
86  // architecture-specific integer value of null pointer constant
88 
89  void set_arch_spec_i386();
90  void set_arch_spec_x86_64();
91  void set_arch_spec_power(const irep_idt &subarch);
92  void set_arch_spec_arm(const irep_idt &subarch);
93  void set_arch_spec_alpha();
94  void set_arch_spec_mips(const irep_idt &subarch);
95  void set_arch_spec_riscv64();
96  void set_arch_spec_s390();
97  void set_arch_spec_s390x();
98  void set_arch_spec_sparc(const irep_idt &subarch);
99  void set_arch_spec_ia64();
100  void set_arch_spec_x32();
101  void set_arch_spec_v850();
102  void set_arch_spec_hppa();
103  void set_arch_spec_sh4();
104 
105  enum class flavourt
106  {
107  NONE,
108  ANSI,
109  GCC,
110  ARM,
111  CLANG,
114  };
115  flavourt mode; // the syntax of source files
116 
118  CODEWARRIOR, ARM };
119  preprocessort preprocessor; // the preprocessor to use
120 
121  std::list<std::string> defines;
122  std::list<std::string> undefines;
123  std::list<std::string> preprocessor_options;
124  std::list<std::string> include_paths;
125  std::list<std::string> include_files;
126 
127  enum class libt { LIB_NONE, LIB_FULL };
129 
131 
132  static const std::size_t default_object_bits=8;
133  } ansi_c;
134 
135  struct cppt
136  {
139 
144 
145  static const std::size_t default_object_bits=8;
146  } cpp;
147 
148  struct verilogt
149  {
150  std::list<std::string> include_paths;
151  } verilog;
152 
153  struct javat
154  {
155  typedef std::list<std::string> classpatht;
158 
159  static const std::size_t default_object_bits=16;
160  } java;
161 
163  {
164  // number of bits to encode heap object addresses
165  std::size_t object_bits;
167 
168  static const std::size_t default_object_bits=8;
169  } bv_encoding;
170 
171  // this is the function to start executing
172  std::string main;
173 
174  void set_arch(const irep_idt &);
175 
176  void set_from_symbol_table(const symbol_tablet &);
177 
178  bool set(const cmdlinet &cmdline);
179 
181  std::string object_bits_info();
182 
183  static irep_idt this_architecture();
185 
186 private:
187  void set_classpath(const std::string &cp);
188 };
189 
190 extern configt config;
191 
192 #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:35
configt::ansi_ct::ts_18661_3_Floatn_types
bool ts_18661_3_Floatn_types
Definition: config.h:45
configt::cppt::cpp_standardt::CPP98
configt::bv_encodingt::object_bits
std::size_t object_bits
Definition: config.h:165
configt::ansi_ct::defines
std::list< std::string > defines
Definition: config.h:121
configt::ansi_ct::bool_width
std::size_t bool_width
Definition: config.h:32
configt::object_bits_info
std::string object_bits_info()
Definition: config.cpp:1257
configt::ansi_ct::set_c99
void set_c99()
Definition: config.h:52
symbol_tablet
The symbol table.
Definition: symbol_table.h:19
configt::cppt
Definition: config.h:135
configt::ansi_ct::NULL_is_zero
bool NULL_is_zero
Definition: config.h:87
configt::java
struct configt::javat java
configt::javat::main_class
irep_idt main_class
Definition: config.h:157
configt::ansi_ct::string_to_os
static ost string_to_os(const std::string &)
Definition: config.cpp:1107
configt::ansi_ct::ost
ost
Definition: config.h:78
configt::ansi_ct::for_has_scope
bool for_has_scope
Definition: config.h:44
configt::cppt::cpp_standardt
cpp_standardt
Definition: config.h:137
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:40
configt::ansi_ct::endiannesst
endiannesst
Definition: config.h:75
configt::ansi_ct::ost::OS_MACOS
configt::ansi_ct::preprocessort::CLANG
configt::ansi_ct::include_paths
std::list< std::string > include_paths
Definition: config.h:124
configt::ansi_ct::flavourt::CODEWARRIOR
configt::ansi_ct::set_arch_spec_mips
void set_arch_spec_mips(const irep_idt &subarch)
Definition: config.cpp:352
configt::main
std::string main
Definition: config.h:172
configt::ansi_ct::os
ost os
Definition: config.h:79
configt::cppt::cpp_standardt::CPP03
configt::ansi_ct::flavourt::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::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:55
configt::ansi_ct::alignment
std::size_t alignment
Definition: config.h:69
configt::ansi_c
struct configt::ansi_ct ansi_c
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::verilog
struct configt::verilogt verilog
configt::ansi_ct::undefines
std::list< std::string > undefines
Definition: config.h:122
configt::ansi_ct::flavourt::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:156
configt::ansi_ct::libt::LIB_NONE
configt::ansi_ct::flavourt::CLANG
configt::ansi_ct
Definition: config.h:27
configt
Globally accessible architectural configuration.
Definition: config.h:24
configt::cppt::cpp_standard
enum configt::cppt::cpp_standardt cpp_standard
configt::ansi_ct::flavourt::NONE
configt::ansi_ct::char_width
std::size_t char_width
Definition: config.h:33
configt::bv_encoding
struct configt::bv_encodingt bv_encoding
configt::cppt::set_cpp98
void set_cpp98()
Definition: config.h:140
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
configt::ansi_ct::endiannesst::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:127
configt::ansi_ct::endiannesst::IS_LITTLE_ENDIAN
configt::bv_encodingt
Definition: config.h:162
configt::ansi_ct::c_standardt::C89
configt::cppt::set_cpp14
void set_cpp14()
Definition: config.h:143
cmdlinet
Definition: cmdline.h:19
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:43
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:38
configt::ansi_ct::preprocessor
preprocessort preprocessor
Definition: config.h:119
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:150
configt::ansi_ct::default_object_bits
static const std::size_t default_object_bits
Definition: config.h:132
configt::cppt::default_object_bits
static const std::size_t default_object_bits
Definition: config.h:145
configt::ansi_ct::Float128_type
bool Float128_type
Definition: config.h:46
configt::ansi_ct::string_abstraction
bool string_abstraction
Definition: config.h:130
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:166
configt::cppt::set_cpp11
void set_cpp11()
Definition: config.h:142
configt::ansi_ct::memory_operand_size
std::size_t memory_operand_size
Definition: config.h:73
configt::ansi_ct::ost::OS_LINUX
configt::ansi_ct::flavourt::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:35
configt::this_operating_system
static irep_idt this_operating_system()
Definition: config.cpp:1368
configt::javat::classpatht
std::list< std::string > classpatht
Definition: config.h:155
configt::ansi_ct::arch
irep_idt arch
Definition: config.h:84
configt::ansi_ct::ost::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:1171
ieee_floatt::rounding_modet
rounding_modet
Definition: ieee_float.h:125
configt::ansi_ct::os_to_string
static std::string os_to_string(ost)
Definition: config.cpp:1096
configt::javat::default_object_bits
static const std::size_t default_object_bits
Definition: config.h:159
configt::ansi_ct::preprocessor_options
std::list< std::string > preprocessor_options
Definition: config.h:123
configt::ansi_ct::include_files
std::list< std::string > include_files
Definition: config.h:125
configt::ansi_ct::ost::NO_OS
configt::ansi_ct::preprocessort::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
configt::ansi_ct::c_standard
enum configt::ansi_ct::c_standardt c_standard
configt::ansi_ct::preprocessort::NONE
configt::ansi_ct::set_c11
void set_c11()
Definition: config.h:53
configt::this_architecture
static irep_idt this_architecture()
Definition: config.cpp:1268
configt::ansi_ct::libt::LIB_FULL
configt::verilogt
Definition: config.h:148
configt::ansi_ct::mode
flavourt mode
Definition: config.h:115
configt::ansi_ct::c_standardt::C11
preprocessort
Definition: preprocessor.h:20
configt::ansi_ct::set_c89
void set_c89()
Definition: config.h:51
configt::ansi_ct::preprocessort::VISUAL_STUDIO
configt::ansi_ct::endiannesst::IS_BIG_ENDIAN
configt::set
bool set(const cmdlinet &cmdline)
Definition: config.cpp:767
configt::cppt::default_cpp_standard
static cpp_standardt default_cpp_standard()
Definition: config.cpp:689
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:39
configt::cppt::cpp_standardt::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:34
configt::ansi_ct::char_is_unsigned
bool char_is_unsigned
Definition: config.h:43
configt::ansi_ct::flavourt::GCC
configt::ansi_ct::set_arch_spec_x86_64
void set_arch_spec_x86_64()
Definition: config.cpp:181
configt::cppt::cpp_standardt::CPP11
configt::ansi_ct::set_arch_spec_x32
void set_arch_spec_x32()
Definition: config.cpp:556
configt::ansi_ct::pointer_width
std::size_t pointer_width
Definition: config.h:36
configt::ansi_ct::single_width
std::size_t single_width
Definition: config.h:37
configt::ansi_ct::flavourt
flavourt
Definition: config.h:105
configt::cpp
struct configt::cppt cpp
configt::ansi_ct::lib
libt lib
Definition: config.h:128
configt::set_classpath
void set_classpath(const std::string &cp)
Definition: config.cpp:1352
configt::ansi_ct::single_precision_constant
bool single_precision_constant
Definition: config.h:47
configt::bv_encodingt::default_object_bits
static const std::size_t default_object_bits
Definition: config.h:168
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:1232
configt::ansi_ct::c_standardt
c_standardt
Definition: config.h:48
configt::set_arch
void set_arch(const irep_idt &)
Definition: config.cpp:701
configt::ansi_ct::int_width
std::size_t int_width
Definition: config.h:30
configt::javat
Definition: config.h:153
configt::ansi_ct::preprocessort::ARM
configt::ansi_ct::preprocessort::CODEWARRIOR
configt::ansi_ct::endianness
endiannesst endianness
Definition: config.h:76
configt::ansi_ct::long_int_width
std::size_t long_int_width
Definition: config.h:31
irep.h
configt::cppt::set_cpp03
void set_cpp03()
Definition: config.h:141