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
void set_arch_spec_arm(const irep_idt &subarch)
Definition: config.cpp:280
void set_LP32()
int=16, long=32, pointer=32
Definition: config.cpp:130
struct configt::ansi_ct ansi_c
void set_arch_spec_power(const irep_idt &subarch)
Definition: config.cpp:219
Globally accessible architectural configuration.
Definition: config.h:24
void set_classpath(const std::string &cp)
Definition: config.cpp:1352
std::size_t alignment
Definition: config.h:69
configt config
Definition: config.cpp:24
std::string object_bits_info()
Definition: config.cpp:1257
static std::string os_to_string(ost)
Definition: config.cpp:1096
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:593
endiannesst endianness
Definition: config.h:76
std::list< std::string > defines
Definition: config.h:121
void set_arch_spec_riscv64()
Definition: config.cpp:402
bool NULL_is_zero
Definition: config.h:87
void set_cpp98()
Definition: config.h:140
void set_LP64()
int=32, long=64, pointer=64
Definition: config.cpp:46
std::size_t double_width
Definition: config.h:38
void set_arch_spec_ia64()
Definition: config.cpp:525
std::list< std::string > undefines
Definition: config.h:122
std::size_t char_width
Definition: config.h:33
static const std::size_t default_object_bits
Definition: config.h:168
void set_16()
Definition: config.cpp:26
void set_arch_spec_mips(const irep_idt &subarch)
Definition: config.cpp:352
static const std::size_t default_object_bits
Definition: config.h:145
struct configt::bv_encodingt bv_encoding
void set_cpp14()
Definition: config.h:143
preprocessort preprocessor
Definition: config.h:119
void set_c89()
Definition: config.h:51
std::list< std::string > include_files
Definition: config.h:125
classpatht classpath
Definition: config.h:156
std::size_t long_long_int_width
Definition: config.h:35
void set_arch_spec_sparc(const irep_idt &subarch)
Definition: config.cpp:485
flavourt mode
Definition: config.h:115
void set_arch_spec_x86_64()
Definition: config.cpp:181
static const std::size_t default_object_bits
Definition: config.h:159
std::string main
Definition: config.h:172
void set_arch(const irep_idt &)
Definition: config.cpp:701
struct configt::verilogt verilog
std::size_t object_bits
Definition: config.h:165
The symbol table.
Definition: symbol_table.h:19
irep_idt arch
Definition: config.h:84
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
void set_arch_spec_alpha()
Definition: config.cpp:323
enum configt::cppt::cpp_standardt cpp_standard
void set_32()
Definition: config.cpp:31
void set_arch_spec_x32()
Definition: config.cpp:556
void set_ILP32()
int=32, long=32, pointer=32
Definition: config.cpp:110
std::size_t int_width
Definition: config.h:30
void set_arch_spec_sh4()
Definition: config.cpp:645
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:35
void set_arch_spec_s390()
Definition: config.cpp:428
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:1171
enum configt::ansi_ct::c_standardt c_standard
static c_standardt default_c_standard()
Definition: config.cpp:675
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:1368
struct configt::cppt cpp
void set_c99()
Definition: config.h:52
std::list< std::string > include_paths
Definition: config.h:150
void set_cpp11()
Definition: config.h:142
ieee_floatt::rounding_modet rounding_mode
Definition: config.h:55
bool string_abstraction
Definition: config.h:130
std::list< std::string > classpatht
Definition: config.h:155
bool is_object_bits_default
Definition: config.h:166
void set_arch_spec_hppa()
Definition: config.cpp:616
void set_arch_spec_i386()
Definition: config.cpp:149
void set_64()
Definition: config.cpp:36
void set_LLP64()
int=32, long=32, pointer=64
Definition: config.cpp:90
static ost string_to_os(const std::string &)
Definition: config.cpp:1107
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:157
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:689
void set_cpp03()
Definition: config.h:141
std::list< std::string > preprocessor_options
Definition: config.h:123
bool ts_18661_3_Floatn_types
Definition: config.h:45
static const std::size_t default_object_bits
Definition: config.h:132
static irep_idt this_architecture()
Definition: config.cpp:1268
std::size_t short_int_width
Definition: config.h:34
void set_arch_spec_s390x()
Definition: config.cpp:457
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:1232
void set_ILP64()
int=64, long=64, pointer=64
Definition: config.cpp:70
std::list< std::string > include_paths
Definition: config.h:124