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 { NONE, ANSI, GCC, ARM, APPLE,
106  flavourt mode; // the syntax of source files
107 
109  CODEWARRIOR, ARM };
110  preprocessort preprocessor; // the preprocessor to use
111 
112  std::list<std::string> defines;
113  std::list<std::string> undefines;
114  std::list<std::string> preprocessor_options;
115  std::list<std::string> include_paths;
116  std::list<std::string> include_files;
117 
118  enum class libt { LIB_NONE, LIB_FULL };
120 
122 
123  static const std::size_t default_object_bits=8;
124  } ansi_c;
125 
126  struct cppt
127  {
130 
135 
136  static const std::size_t default_object_bits=8;
137  } cpp;
138 
139  struct verilogt
140  {
141  std::list<std::string> include_paths;
142  } verilog;
143 
144  struct javat
145  {
146  typedef std::list<std::string> classpatht;
149 
150  static const std::size_t default_object_bits=16;
151  } java;
152 
154  {
155  // number of bits to encode heap object addresses
156  std::size_t object_bits;
158 
159  static const std::size_t default_object_bits=8;
160  } bv_encoding;
161 
162  // this is the function to start executing
163  std::string main;
164 
165  void set_arch(const irep_idt &);
166 
167  void set_from_symbol_table(const symbol_tablet &);
168 
169  bool set(const cmdlinet &cmdline);
170 
172  std::string object_bits_info();
173 
174  static irep_idt this_architecture();
176 
177 private:
178  void set_classpath(const std::string &cp);
179 };
180 
181 extern configt config;
182 
183 #endif // CPROVER_UTIL_CONFIG_H
void set_arch_spec_arm(const irep_idt &subarch)
Definition: config.cpp:278
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:217
Globally accessible architectural configuration.
Definition: config.h:24
void set_classpath(const std::string &cp)
Definition: config.cpp:1293
std::size_t alignment
Definition: config.h:69
configt config
Definition: config.cpp:23
std::string object_bits_info()
Definition: config.cpp:1202
static std::string os_to_string(ost)
Definition: config.cpp:1041
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:565
endiannesst endianness
Definition: config.h:76
std::list< std::string > defines
Definition: config.h:112
bool NULL_is_zero
Definition: config.h:87
void set_cpp98()
Definition: config.h:131
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:497
std::list< std::string > undefines
Definition: config.h:113
std::size_t char_width
Definition: config.h:33
static const std::size_t default_object_bits
Definition: config.h:159
void set_16()
Definition: config.cpp:25
void set_arch_spec_mips(const irep_idt &subarch)
Definition: config.cpp:350
static const std::size_t default_object_bits
Definition: config.h:136
struct configt::bv_encodingt bv_encoding
void set_cpp14()
Definition: config.h:134
preprocessort preprocessor
Definition: config.h:110
void set_c89()
Definition: config.h:51
std::list< std::string > include_files
Definition: config.h:116
classpatht classpath
Definition: config.h:147
std::size_t long_long_int_width
Definition: config.h:35
void set_arch_spec_sparc(const irep_idt &subarch)
Definition: config.cpp:457
flavourt mode
Definition: config.h:106
void set_arch_spec_x86_64()
Definition: config.cpp:180
static const std::size_t default_object_bits
Definition: config.h:150
std::string main
Definition: config.h:163
void set_arch(const irep_idt &)
Definition: config.cpp:673
struct configt::verilogt verilog
std::size_t object_bits
Definition: config.h:156
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:321
enum configt::cppt::cpp_standardt cpp_standard
void set_32()
Definition: config.cpp:30
void set_arch_spec_x32()
Definition: config.cpp:528
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:617
bool for_has_scope
Definition: config.h:44
struct configt::javat java
void set_arch_spec_s390()
Definition: config.cpp:400
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:1116
enum configt::ansi_ct::c_standardt c_standard
static c_standardt default_c_standard()
Definition: config.cpp:647
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:1309
struct configt::cppt cpp
void set_c99()
Definition: config.h:52
std::list< std::string > include_paths
Definition: config.h:141
void set_cpp11()
Definition: config.h:133
ieee_floatt::rounding_modet rounding_mode
Definition: config.h:55
bool string_abstraction
Definition: config.h:121
std::list< std::string > classpatht
Definition: config.h:146
bool is_object_bits_default
Definition: config.h:157
void set_arch_spec_hppa()
Definition: config.cpp:588
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:1052
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:148
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:661
void set_cpp03()
Definition: config.h:132
std::list< std::string > preprocessor_options
Definition: config.h:114
bool ts_18661_3_Floatn_types
Definition: config.h:45
static const std::size_t default_object_bits
Definition: config.h:123
static irep_idt this_architecture()
Definition: config.cpp:1212
std::size_t short_int_width
Definition: config.h:34
void set_arch_spec_s390x()
Definition: config.cpp:429
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:1177
void set_ILP64()
int=64, long=64, pointer=64
Definition: config.cpp:69
std::list< std::string > include_paths
Definition: config.h:115