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  unsigned int_width;
31  unsigned long_int_width;
32  unsigned bool_width;
33  unsigned char_width;
34  unsigned short_int_width;
36  unsigned pointer_width;
37  unsigned single_width;
38  unsigned double_width;
40  unsigned wchar_t_width;
41 
42  // various language options
47  enum class c_standardt { C89, C99, C11 } c_standard;
49 
53 
55 
56  void set_16();
57  void set_32();
58  void set_64();
59 
60  // http://www.unix.org/version2/whatsnew/lp64_wp.html
61  void set_LP64(); // int=32, long=64, pointer=64
62  void set_ILP64(); // int=64, long=64, pointer=64
63  void set_LLP64(); // int=32, long=32, pointer=64
64  void set_ILP32(); // int=32, long=32, pointer=32
65  void set_LP32(); // int=16, long=32, pointer=32
66 
67  // minimum alignment (in structs) measured in bytes
68  unsigned alignment;
69 
70  // maximum minimum size of the operands for a machine
71  // instruction (in bytes)
73 
76 
77  enum class ost { NO_OS, OS_LINUX, OS_MACOS, OS_WIN };
79 
80  static std::string os_to_string(ost);
81  static ost string_to_os(const std::string &);
82 
84 
85  // architecture-specific integer value of null pointer constant
87 
88  void set_arch_spec_i386();
89  void set_arch_spec_x86_64();
90  void set_arch_spec_power(const irep_idt &subarch);
91  void set_arch_spec_arm(const irep_idt &subarch);
92  void set_arch_spec_alpha();
93  void set_arch_spec_mips(const irep_idt &subarch);
94  void set_arch_spec_s390();
95  void set_arch_spec_s390x();
96  void set_arch_spec_sparc(const irep_idt &subarch);
97  void set_arch_spec_ia64();
98  void set_arch_spec_x32();
99  void set_arch_spec_v850();
100  void set_arch_spec_hppa();
101  void set_arch_spec_sh4();
102 
103  enum class flavourt { NONE, ANSI, GCC, ARM, APPLE,
105  flavourt mode; // the syntax of source files
106 
108  CODEWARRIOR, ARM };
109  preprocessort preprocessor; // the preprocessor to use
110 
111  std::list<std::string> defines;
112  std::list<std::string> undefines;
113  std::list<std::string> preprocessor_options;
114  std::list<std::string> include_paths;
115  std::list<std::string> include_files;
116 
117  enum class libt { LIB_NONE, LIB_FULL };
119 
121  } ansi_c;
122 
123  struct cppt
124  {
127 
132  } cpp;
133 
134  struct verilogt
135  {
136  std::list<std::string> include_paths;
137  } verilog;
138 
139  struct javat
140  {
141  typedef std::list<std::string> classpatht;
144  } java;
145 
146  // this is the function to start executing
147  std::string main;
148 
149  void set_arch(const irep_idt &);
150 
151  void set_from_symbol_table(const symbol_tablet &);
152 
153  bool set(const cmdlinet &cmdline);
154 
155  void set_classpath(const std::string &cp);
156 
157  static irep_idt this_architecture();
159 };
160 
161 extern configt config;
162 
163 #endif // CPROVER_UTIL_CONFIG_H
void set_arch_spec_arm(const irep_idt &subarch)
Definition: config.cpp:276
void set_LP32()
int=16, long=32, pointer=32
Definition: config.cpp:127
struct configt::ansi_ct ansi_c
void set_arch_spec_power(const irep_idt &subarch)
Definition: config.cpp:215
unsigned int_width
Definition: config.h:30
Globally accessible architectural configuration.
Definition: config.h:24
unsigned single_width
Definition: config.h:37
void set_classpath(const std::string &cp)
Definition: config.cpp:1229
configt config
Definition: config.cpp:21
static std::string os_to_string(ost)
Definition: config.cpp:1016
unsigned alignment
Definition: config.h:68
bool single_precision_constant
Definition: config.h:46
void set_arch_spec_v850()
Sets up the widths of variables for the Renesas V850.
Definition: config.cpp:563
endiannesst endianness
Definition: config.h:75
std::list< std::string > defines
Definition: config.h:111
unsigned short_int_width
Definition: config.h:34
bool NULL_is_zero
Definition: config.h:86
void set_cpp98()
Definition: config.h:128
void set_LP64()
int=32, long=64, pointer=64
Definition: config.cpp:43
void set_arch_spec_ia64()
Definition: config.cpp:495
unsigned char_width
Definition: config.h:33
std::list< std::string > undefines
Definition: config.h:112
void set_16()
Definition: config.cpp:23
void set_arch_spec_mips(const irep_idt &subarch)
Definition: config.cpp:348
void set_cpp14()
Definition: config.h:131
preprocessort preprocessor
Definition: config.h:109
unsigned wchar_t_width
Definition: config.h:40
void set_c89()
Definition: config.h:50
std::list< std::string > include_files
Definition: config.h:115
classpatht classpath
Definition: config.h:142
void set_arch_spec_sparc(const irep_idt &subarch)
Definition: config.cpp:455
flavourt mode
Definition: config.h:105
void set_arch_spec_x86_64()
Definition: config.cpp:178
unsigned long_long_int_width
Definition: config.h:35
std::string main
Definition: config.h:147
void set_arch(const irep_idt &)
Definition: config.cpp:663
struct configt::verilogt verilog
The symbol table.
Definition: symbol_table.h:52
irep_idt arch
Definition: config.h:83
TO_BE_DOCUMENTED.
Definition: namespace.h:62
void set_arch_spec_alpha()
Definition: config.cpp:319
enum configt::cppt::cpp_standardt cpp_standard
void set_32()
Definition: config.cpp:28
void set_arch_spec_x32()
Definition: config.cpp:526
void set_ILP32()
int=32, long=32, pointer=32
Definition: config.cpp:107
void set_arch_spec_sh4()
Definition: config.cpp:615
unsigned memory_operand_size
Definition: config.h:72
bool for_has_scope
Definition: config.h:45
struct configt::javat java
void set_arch_spec_s390()
Definition: config.cpp:398
bool char_is_unsigned
Definition: config.h:43
void set_c11()
Definition: config.h:52
bool use_fixed_for_float
Definition: config.h:44
void set_from_symbol_table(const symbol_tablet &)
Definition: config.cpp:1091
enum configt::ansi_ct::c_standardt c_standard
static c_standardt default_c_standard()
Definition: config.cpp:645
static irep_idt this_operating_system()
Definition: config.cpp:1258
struct configt::cppt cpp
void set_c99()
Definition: config.h:51
std::list< std::string > include_paths
Definition: config.h:136
void set_cpp11()
Definition: config.h:130
ieee_floatt::rounding_modet rounding_mode
Definition: config.h:54
bool string_abstraction
Definition: config.h:120
std::list< std::string > classpatht
Definition: config.h:141
unsigned bool_width
Definition: config.h:32
void set_arch_spec_hppa()
Definition: config.cpp:586
void set_arch_spec_i386()
Definition: config.cpp:146
unsigned long_double_width
Definition: config.h:39
void set_64()
Definition: config.cpp:33
void set_LLP64()
int=32, long=32, pointer=64
Definition: config.cpp:87
static ost string_to_os(const std::string &)
Definition: config.cpp:1027
unsigned double_width
Definition: config.h:38
irep_idt main_class
Definition: config.h:143
unsigned long_int_width
Definition: config.h:31
bool wchar_t_is_unsigned
Definition: config.h:43
unsigned pointer_width
Definition: config.h:36
static cpp_standardt default_cpp_standard()
Definition: config.cpp:658
void set_cpp03()
Definition: config.h:129
std::list< std::string > preprocessor_options
Definition: config.h:113
static irep_idt this_architecture()
Definition: config.cpp:1148
void set_arch_spec_s390x()
Definition: config.cpp:427
void set_ILP64()
int=64, long=64, pointer=64
Definition: config.cpp:67
std::list< std::string > include_paths
Definition: config.h:114