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_s390();
96  void set_arch_spec_s390x();
97  void set_arch_spec_sparc(const irep_idt &subarch);
98  void set_arch_spec_ia64();
99  void set_arch_spec_x32();
100  void set_arch_spec_v850();
101  void set_arch_spec_hppa();
102  void set_arch_spec_sh4();
103 
104  enum class flavourt
105  {
106  NONE,
107  ANSI,
108  GCC,
109  ARM,
110  CLANG,
113  };
114  flavourt mode; // the syntax of source files
115 
117  CODEWARRIOR, ARM };
118  preprocessort preprocessor; // the preprocessor to use
119 
120  std::list<std::string> defines;
121  std::list<std::string> undefines;
122  std::list<std::string> preprocessor_options;
123  std::list<std::string> include_paths;
124  std::list<std::string> include_files;
125 
126  enum class libt { LIB_NONE, LIB_FULL };
128 
130 
131  static const std::size_t default_object_bits=8;
132  } ansi_c;
133 
134  struct cppt
135  {
138 
143 
144  static const std::size_t default_object_bits=8;
145  } cpp;
146 
147  struct verilogt
148  {
149  std::list<std::string> include_paths;
150  } verilog;
151 
152  struct javat
153  {
154  typedef std::list<std::string> classpatht;
157 
158  static const std::size_t default_object_bits=16;
159  } java;
160 
162  {
163  // number of bits to encode heap object addresses
164  std::size_t object_bits;
166 
167  static const std::size_t default_object_bits=8;
168  } bv_encoding;
169 
170  // this is the function to start executing
171  std::string main;
172 
173  void set_arch(const irep_idt &);
174 
175  void set_from_symbol_table(const symbol_tablet &);
176 
177  bool set(const cmdlinet &cmdline);
178 
180  std::string object_bits_info();
181 
182  static irep_idt this_architecture();
184 
185 private:
186  void set_classpath(const std::string &cp);
187 };
188 
189 extern configt config;
190 
191 #endif // CPROVER_UTIL_CONFIG_H
void set_arch_spec_arm(const irep_idt &subarch)
Definition: config.cpp:279
void set_LP32()
int=16, long=32, pointer=32
Definition: config.cpp:129
struct configt::ansi_ct ansi_c
void set_arch_spec_power(const irep_idt &subarch)
Definition: config.cpp:218
Globally accessible architectural configuration.
Definition: config.h:24
void set_classpath(const std::string &cp)
Definition: config.cpp:1294
std::size_t alignment
Definition: config.h:69
configt config
Definition: config.cpp:23
std::string object_bits_info()
Definition: config.cpp:1203
static std::string os_to_string(ost)
Definition: config.cpp:1042
std::size_t single_width
Definition: config.h:37
bool single_precision_constant
Definition: config.h:47
void set_arch_spec_v850()
Sets up the widths of variables for the Renesas V850.
Definition: config.cpp:566
endiannesst endianness
Definition: config.h:76
std::list< std::string > defines
Definition: config.h:120
bool NULL_is_zero
Definition: config.h:87
void set_cpp98()
Definition: config.h:139
void set_LP64()
int=32, long=64, pointer=64
Definition: config.cpp:45
std::size_t double_width
Definition: config.h:38
void set_arch_spec_ia64()
Definition: config.cpp:498
std::list< std::string > undefines
Definition: config.h:121
std::size_t char_width
Definition: config.h:33
static const std::size_t default_object_bits
Definition: config.h:167
void set_16()
Definition: config.cpp:25
void set_arch_spec_mips(const irep_idt &subarch)
Definition: config.cpp:351
static const std::size_t default_object_bits
Definition: config.h:144
struct configt::bv_encodingt bv_encoding
void set_cpp14()
Definition: config.h:142
preprocessort preprocessor
Definition: config.h:118
void set_c89()
Definition: config.h:51
std::list< std::string > include_files
Definition: config.h:124
classpatht classpath
Definition: config.h:155
std::size_t long_long_int_width
Definition: config.h:35
void set_arch_spec_sparc(const irep_idt &subarch)
Definition: config.cpp:458
flavourt mode
Definition: config.h:114
void set_arch_spec_x86_64()
Definition: config.cpp:180
static const std::size_t default_object_bits
Definition: config.h:158
std::string main
Definition: config.h:171
void set_arch(const irep_idt &)
Definition: config.cpp:674
struct configt::verilogt verilog
std::size_t object_bits
Definition: config.h:164
The symbol table.
Definition: symbol_table.h:19
irep_idt arch
Definition: config.h:84
TO_BE_DOCUMENTED.
Definition: namespace.h:74
void set_arch_spec_alpha()
Definition: config.cpp:322
enum configt::cppt::cpp_standardt cpp_standard
void set_32()
Definition: config.cpp:30
void set_arch_spec_x32()
Definition: config.cpp:529
void set_ILP32()
int=32, long=32, pointer=32
Definition: config.cpp:109
std::size_t int_width
Definition: config.h:30
void set_arch_spec_sh4()
Definition: config.cpp:618
bool for_has_scope
Definition: config.h:44
struct configt::javat java
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
void set_arch_spec_s390()
Definition: config.cpp:401
std::size_t pointer_width
Definition: config.h:36
bool char_is_unsigned
Definition: config.h:43
void set_c11()
Definition: config.h:53
void set_from_symbol_table(const symbol_tablet &)
Definition: config.cpp:1117
enum configt::ansi_ct::c_standardt c_standard
static c_standardt default_c_standard()
Definition: config.cpp:648
std::size_t wchar_t_width
Definition: config.h:40
bool Float128_type
Definition: config.h:46
static irep_idt this_operating_system()
Definition: config.cpp:1310
struct configt::cppt cpp
void set_c99()
Definition: config.h:52
std::list< std::string > include_paths
Definition: config.h:149
void set_cpp11()
Definition: config.h:141
ieee_floatt::rounding_modet rounding_mode
Definition: config.h:55
bool string_abstraction
Definition: config.h:129
std::list< std::string > classpatht
Definition: config.h:154
bool is_object_bits_default
Definition: config.h:165
void set_arch_spec_hppa()
Definition: config.cpp:589
void set_arch_spec_i386()
Definition: config.cpp:148
void set_64()
Definition: config.cpp:35
void set_LLP64()
int=32, long=32, pointer=64
Definition: config.cpp:89
static ost string_to_os(const std::string &)
Definition: config.cpp:1053
std::size_t memory_operand_size
Definition: config.h:73
std::size_t bool_width
Definition: config.h:32
irep_idt main_class
Definition: config.h:156
bool wchar_t_is_unsigned
Definition: config.h:43
std::size_t long_int_width
Definition: config.h:31
static cpp_standardt default_cpp_standard()
Definition: config.cpp:662
void set_cpp03()
Definition: config.h:140
std::list< std::string > preprocessor_options
Definition: config.h:122
bool ts_18661_3_Floatn_types
Definition: config.h:45
static const std::size_t default_object_bits
Definition: config.h:131
static irep_idt this_architecture()
Definition: config.cpp:1213
std::size_t short_int_width
Definition: config.h:34
void set_arch_spec_s390x()
Definition: config.cpp:430
std::size_t long_double_width
Definition: config.h:39
void set_object_bits_from_symbol_table(const symbol_tablet &)
Sets the number of bits used for object addresses.
Definition: config.cpp:1178
void set_ILP64()
int=64, long=64, pointer=64
Definition: config.cpp:69
std::list< std::string > include_paths
Definition: config.h:123