cprover
config.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "config.h"
10 
11 #include <cstdlib>
12 
13 #include "arith_tools.h"
14 #include "cmdline.h"
15 #include "cprover_prefix.h"
16 #include "exception_utils.h"
17 #include "namespace.h"
18 #include "simplify_expr.h"
19 #include "std_expr.h"
20 #include "string2int.h"
21 #include "string_utils.h"
22 #include "symbol_table.h"
23 
25 
27 {
28  set_LP32();
29 }
30 
32 {
33  set_ILP32();
34 }
35 
37 {
38  #ifdef _WIN32
39  set_LLP64();
40  #else
41  set_LP64();
42  #endif
43 }
44 
47 {
48  bool_width=1*8;
49  int_width=4*8;
50  long_int_width=8*8;
51  char_width=1*8;
52  short_int_width=2*8;
53  long_long_int_width=8*8;
54  pointer_width=8*8;
55  single_width=4*8;
56  double_width=8*8;
57  long_double_width=16*8;
58  char_is_unsigned=false;
59  wchar_t_is_unsigned=false;
60  wchar_t_width=4*8;
61  alignment=1;
62  memory_operand_size=int_width/8;
63 }
64 
66 // TODO: find the alignment restrictions (per type) of the different
67 // architectures (currently: sizeof=alignedof)
68 // TODO: implement the __attribute__((__aligned__(val)))
69 
71 {
72  bool_width=1*8;
73  int_width=8*8;
74  long_int_width=8*8;
75  char_width=1*8;
76  short_int_width=2*8;
77  long_long_int_width=8*8;
78  pointer_width=8*8;
79  single_width=4*8;
80  double_width=8*8;
81  long_double_width=8*8;
82  char_is_unsigned=false;
83  wchar_t_is_unsigned=false;
84  wchar_t_width=4*8;
85  alignment=1;
86  memory_operand_size=int_width/8;
87 }
88 
91 {
92  bool_width=1*8;
93  int_width=4*8;
94  long_int_width=4*8;
95  char_width=1*8;
96  short_int_width=2*8;
97  long_long_int_width=8*8;
98  pointer_width=8*8;
99  single_width=4*8;
100  double_width=8*8;
101  long_double_width=8*8;
102  char_is_unsigned=false;
103  wchar_t_is_unsigned=false;
104  wchar_t_width=4*8;
105  alignment=1;
106  memory_operand_size=int_width/8;
107 }
108 
111 {
112  bool_width=1*8;
113  int_width=4*8;
114  long_int_width=4*8;
115  char_width=1*8;
116  short_int_width=2*8;
117  long_long_int_width=8*8;
118  pointer_width=4*8;
119  single_width=4*8;
120  double_width=8*8;
121  long_double_width=12*8; // really 96 bits on GCC
122  char_is_unsigned=false;
123  wchar_t_is_unsigned=false;
124  wchar_t_width=4*8;
125  alignment=1;
126  memory_operand_size=int_width/8;
127 }
128 
131 {
132  bool_width=1*8;
133  int_width=2*8;
134  long_int_width=4*8;
135  char_width=1*8;
136  short_int_width=2*8;
137  long_long_int_width=8*8;
138  pointer_width=4*8;
139  single_width=4*8;
140  double_width=8*8;
141  long_double_width=8*8;
142  char_is_unsigned=false;
143  wchar_t_is_unsigned=false;
144  wchar_t_width=4*8;
145  alignment=1;
146  memory_operand_size=int_width/8;
147 }
148 
150 {
151  set_ILP32();
152  endianness=endiannesst::IS_LITTLE_ENDIAN;
153  char_is_unsigned=false;
154  NULL_is_zero=true;
155 
156  switch(mode)
157  {
158  case flavourt::GCC:
159  case flavourt::CLANG:
160  defines.push_back("i386");
161  defines.push_back("__i386");
162  defines.push_back("__i386__");
163  if(mode == flavourt::CLANG)
164  defines.push_back("__LITTLE_ENDIAN__");
165  break;
166 
167  case flavourt::VISUAL_STUDIO:
168  defines.push_back("_M_IX86");
169  break;
170 
171  case flavourt::CODEWARRIOR:
172  case flavourt::ARM:
173  case flavourt::ANSI:
174  break;
175 
176  case flavourt::NONE:
177  UNREACHABLE;
178  }
179 }
180 
182 {
183  set_LP64();
184  endianness=endiannesst::IS_LITTLE_ENDIAN;
185  long_double_width=16*8;
186  char_is_unsigned=false;
187  NULL_is_zero=true;
188 
189  switch(mode)
190  {
191  case flavourt::GCC:
192  case flavourt::CLANG:
193  defines.push_back("__LP64__");
194  defines.push_back("__x86_64");
195  defines.push_back("__x86_64__");
196  defines.push_back("_LP64");
197  defines.push_back("__amd64__");
198  defines.push_back("__amd64");
199 
200  if(os == ost::OS_MACOS)
201  defines.push_back("__LITTLE_ENDIAN__");
202  break;
203 
204  case flavourt::VISUAL_STUDIO:
205  defines.push_back("_M_X64");
206  defines.push_back("_M_AMD64");
207  break;
208 
209  case flavourt::CODEWARRIOR:
210  case flavourt::ARM:
211  case flavourt::ANSI:
212  break;
213 
214  case flavourt::NONE:
215  UNREACHABLE;
216  }
217 }
218 
220 {
221  if(subarch=="powerpc")
222  set_ILP32();
223  else // ppc64 or ppc64le
224  set_LP64();
225 
226  if(subarch=="ppc64le")
227  endianness=endiannesst::IS_LITTLE_ENDIAN;
228  else
229  endianness=endiannesst::IS_BIG_ENDIAN;
230 
231  long_double_width=16*8;
232  char_is_unsigned=true;
233  NULL_is_zero=true;
234 
235  switch(mode)
236  {
237  case flavourt::GCC:
238  case flavourt::CLANG:
239  defines.push_back("__powerpc");
240  defines.push_back("__powerpc__");
241  defines.push_back("__POWERPC__");
242  defines.push_back("__ppc__");
243 
244  if(os == ost::OS_MACOS)
245  defines.push_back("__BIG_ENDIAN__");
246 
247  if(subarch!="powerpc")
248  {
249  defines.push_back("__powerpc64");
250  defines.push_back("__powerpc64__");
251  defines.push_back("__PPC64__");
252  defines.push_back("__ppc64__");
253  if(subarch=="ppc64le")
254  {
255  defines.push_back("_CALL_ELF=2");
256  defines.push_back("__LITTLE_ENDIAN__");
257  }
258  else
259  {
260  defines.push_back("_CALL_ELF=1");
261  defines.push_back("__BIG_ENDIAN__");
262  }
263  }
264  break;
265 
266  case flavourt::VISUAL_STUDIO:
267  defines.push_back("_M_PPC");
268  break;
269 
270  case flavourt::CODEWARRIOR:
271  case flavourt::ARM:
272  case flavourt::ANSI:
273  break;
274 
275  case flavourt::NONE:
276  UNREACHABLE;
277  }
278 }
279 
281 {
282  if(subarch=="arm64")
283  {
284  set_LP64();
285  long_double_width=16*8;
286  }
287  else
288  {
289  set_ILP32();
290  long_double_width=8*8;
291  }
292 
293  endianness=endiannesst::IS_LITTLE_ENDIAN;
294  char_is_unsigned=true;
295  NULL_is_zero=true;
296 
297  switch(mode)
298  {
299  case flavourt::GCC:
300  case flavourt::CLANG:
301  if(subarch=="arm64")
302  defines.push_back("__aarch64__");
303  else
304  defines.push_back("__arm__");
305  if(subarch=="armhf")
306  defines.push_back("__ARM_PCS_VFP");
307  break;
308 
309  case flavourt::VISUAL_STUDIO:
310  defines.push_back("_M_ARM");
311  break;
312 
313  case flavourt::CODEWARRIOR:
314  case flavourt::ARM:
315  case flavourt::ANSI:
316  break;
317 
318  case flavourt::NONE:
319  UNREACHABLE;
320  }
321 }
322 
324 {
325  set_LP64();
326  endianness=endiannesst::IS_LITTLE_ENDIAN;
327  long_double_width=16*8;
328  char_is_unsigned=false;
329  NULL_is_zero=true;
330 
331  switch(mode)
332  {
333  case flavourt::GCC:
334  defines.push_back("__alpha__");
335  break;
336 
337  case flavourt::VISUAL_STUDIO:
338  defines.push_back("_M_ALPHA");
339  break;
340 
341  case flavourt::CLANG:
342  case flavourt::CODEWARRIOR:
343  case flavourt::ARM:
344  case flavourt::ANSI:
345  break;
346 
347  case flavourt::NONE:
348  UNREACHABLE;
349  }
350 }
351 
353 {
354  if(subarch=="mipsel" ||
355  subarch=="mips" ||
356  subarch=="mipsn32el" ||
357  subarch=="mipsn32")
358  {
359  set_ILP32();
360  long_double_width=8*8;
361  }
362  else
363  {
364  set_LP64();
365  long_double_width=16*8;
366  }
367 
368  if(subarch=="mipsel" ||
369  subarch=="mipsn32el" ||
370  subarch=="mips64el")
371  endianness=endiannesst::IS_LITTLE_ENDIAN;
372  else
373  endianness=endiannesst::IS_BIG_ENDIAN;
374 
375  char_is_unsigned=false;
376  NULL_is_zero=true;
377 
378  switch(mode)
379  {
380  case flavourt::GCC:
381  defines.push_back("__mips__");
382  defines.push_back("mips");
383  defines.push_back(
384  "_MIPS_SZPTR="+std::to_string(config.ansi_c.pointer_width));
385  break;
386 
387  case flavourt::VISUAL_STUDIO:
388  UNREACHABLE; // not supported by Visual Studio
389  break;
390 
391  case flavourt::CLANG:
392  case flavourt::CODEWARRIOR:
393  case flavourt::ARM:
394  case flavourt::ANSI:
395  break;
396 
397  case flavourt::NONE:
398  UNREACHABLE;
399  }
400 }
401 
403 {
404  set_LP64();
405  endianness = endiannesst::IS_LITTLE_ENDIAN;
406  long_double_width = 16 * 8;
407  char_is_unsigned = true;
408  NULL_is_zero = true;
409 
410  switch(mode)
411  {
412  case flavourt::GCC:
413  defines.push_back("__riscv");
414  break;
415 
416  case flavourt::VISUAL_STUDIO:
417  case flavourt::CLANG:
418  case flavourt::CODEWARRIOR:
419  case flavourt::ARM:
420  case flavourt::ANSI:
421  break;
422 
423  case flavourt::NONE:
424  UNREACHABLE;
425  }
426 }
427 
429 {
430  set_ILP32();
431  endianness=endiannesst::IS_BIG_ENDIAN;
432  long_double_width=16*8;
433  char_is_unsigned=true;
434  NULL_is_zero=true;
435 
436  switch(mode)
437  {
438  case flavourt::GCC:
439  defines.push_back("__s390__");
440  break;
441 
442  case flavourt::VISUAL_STUDIO:
443  UNREACHABLE; // not supported by Visual Studio
444  break;
445 
446  case flavourt::CLANG:
447  case flavourt::CODEWARRIOR:
448  case flavourt::ARM:
449  case flavourt::ANSI:
450  break;
451 
452  case flavourt::NONE:
453  UNREACHABLE;
454  }
455 }
456 
458 {
459  set_LP64();
460  endianness=endiannesst::IS_BIG_ENDIAN;
461  char_is_unsigned=true;
462  NULL_is_zero=true;
463 
464  switch(mode)
465  {
466  case flavourt::GCC:
467  defines.push_back("__s390x__");
468  break;
469 
470  case flavourt::VISUAL_STUDIO:
471  UNREACHABLE; // not supported by Visual Studio
472  break;
473 
474  case flavourt::CLANG:
475  case flavourt::CODEWARRIOR:
476  case flavourt::ARM:
477  case flavourt::ANSI:
478  break;
479 
480  case flavourt::NONE:
481  UNREACHABLE;
482  }
483 }
484 
486 {
487  if(subarch=="sparc64")
488  {
489  set_LP64();
490  long_double_width=16*8;
491  }
492  else
493  {
494  set_ILP32();
495  long_double_width=16*8;
496  }
497 
498  endianness=endiannesst::IS_BIG_ENDIAN;
499  char_is_unsigned=false;
500  NULL_is_zero=true;
501 
502  switch(mode)
503  {
504  case flavourt::GCC:
505  defines.push_back("__sparc__");
506  if(subarch=="sparc64")
507  defines.push_back("__arch64__");
508  break;
509 
510  case flavourt::VISUAL_STUDIO:
511  UNREACHABLE; // not supported by Visual Studio
512  break;
513 
514  case flavourt::CLANG:
515  case flavourt::CODEWARRIOR:
516  case flavourt::ARM:
517  case flavourt::ANSI:
518  break;
519 
520  case flavourt::NONE:
521  UNREACHABLE;
522  }
523 }
524 
526 {
527  set_LP64();
528  long_double_width=16*8;
529  endianness=endiannesst::IS_LITTLE_ENDIAN;
530  char_is_unsigned=false;
531  NULL_is_zero=true;
532 
533  switch(mode)
534  {
535  case flavourt::GCC:
536  defines.push_back("__ia64__");
537  defines.push_back("_IA64");
538  defines.push_back("__IA64__");
539  break;
540 
541  case flavourt::VISUAL_STUDIO:
542  defines.push_back("_M_IA64");
543  break;
544 
545  case flavourt::CLANG:
546  case flavourt::CODEWARRIOR:
547  case flavourt::ARM:
548  case flavourt::ANSI:
549  break;
550 
551  case flavourt::NONE:
552  UNREACHABLE;
553  }
554 }
555 
557 {
558  // This is a variant of x86_64 that has
559  // 32-bit long int and 32-bit pointers.
560  set_ILP32();
561  long_double_width=16*8; // different from i386
562  endianness=endiannesst::IS_LITTLE_ENDIAN;
563  char_is_unsigned=false;
564  NULL_is_zero=true;
565 
566  switch(mode)
567  {
568  case flavourt::GCC:
569  defines.push_back("__ILP32__");
570  defines.push_back("__x86_64");
571  defines.push_back("__x86_64__");
572  defines.push_back("__amd64__");
573  defines.push_back("__amd64");
574  break;
575 
576  case flavourt::VISUAL_STUDIO:
577  UNREACHABLE; // not supported by Visual Studio
578  break;
579 
580  case flavourt::CLANG:
581  case flavourt::CODEWARRIOR:
582  case flavourt::ARM:
583  case flavourt::ANSI:
584  break;
585 
586  case flavourt::NONE:
587  UNREACHABLE;
588  }
589 }
590 
594 {
595  // The Renesas V850 is a 32-bit microprocessor used in
596  // many automotive applications. This spec is written from the
597  // architecture manual rather than having access to a running
598  // system. Thus some assumptions have been made.
599 
600  set_ILP32();
601 
602  // Technically, the V850's don't have floating-point at all.
603  // However, the RH850, aimed at automotive has both 32-bit and
604  // 64-bit IEEE-754 float.
605  double_width=8*8;
606  long_double_width=8*8;
607  endianness=endiannesst::IS_LITTLE_ENDIAN;
608 
609  // Without information about the compiler and RTOS, these are guesses
610  char_is_unsigned=false;
611  NULL_is_zero=true;
612 
613  // No preprocessor definitions due to lack of information
614 }
615 
617 {
618  set_ILP32();
619  long_double_width=8*8; // different from i386
620  endianness=endiannesst::IS_BIG_ENDIAN;
621  char_is_unsigned=false;
622  NULL_is_zero=true;
623 
624  switch(mode)
625  {
626  case flavourt::GCC:
627  defines.push_back("__hppa__");
628  break;
629 
630  case flavourt::VISUAL_STUDIO:
631  UNREACHABLE; // not supported by Visual Studio
632  break;
633 
634  case flavourt::CLANG:
635  case flavourt::CODEWARRIOR:
636  case flavourt::ARM:
637  case flavourt::ANSI:
638  break;
639 
640  case flavourt::NONE:
641  UNREACHABLE;
642  }
643 }
644 
646 {
647  set_ILP32();
648  long_double_width=8*8; // different from i386
649  endianness=endiannesst::IS_LITTLE_ENDIAN;
650  char_is_unsigned=false;
651  NULL_is_zero=true;
652 
653  switch(mode)
654  {
655  case flavourt::GCC:
656  defines.push_back("__sh__");
657  defines.push_back("__SH4__");
658  break;
659 
660  case flavourt::VISUAL_STUDIO:
661  UNREACHABLE; // not supported by Visual Studio
662  break;
663 
664  case flavourt::CLANG:
665  case flavourt::CODEWARRIOR:
666  case flavourt::ARM:
667  case flavourt::ANSI:
668  break;
669 
670  case flavourt::NONE:
671  UNREACHABLE;
672  }
673 }
674 
676 {
677 #if defined(__APPLE__)
678  // By default, clang on the Mac builds C code in GNU C11
679  return c_standardt::C11;
680 #elif defined(__FreeBSD__) || defined(__OpenBSD__)
681  // By default, clang on FreeBSD builds C code in GNU C99
682  // By default, clang on OpenBSD builds C code in C99
683  return c_standardt::C99;
684 #else
685  // By default, gcc 5.4 or higher use gnu11; older versions use gnu89
686  return c_standardt::C11;
687 #endif
688 }
689 
691 {
692  // g++ 6.3 uses gnu++14
693  // g++ 5.4 uses gnu++98
694  // clang 6.0 uses c++14
695  #if defined _WIN32
696  return cpp_standardt::CPP14;
697  #else
698  return cpp_standardt::CPP98;
699  #endif
700 }
701 
702 void configt::set_arch(const irep_idt &arch)
703 {
704  ansi_c.arch=arch;
705 
706  if(arch=="none")
707  {
708  // the architecture for people who can't commit
711  ansi_c.NULL_is_zero=false;
712 
713  if(sizeof(long int)==8)
714  ansi_c.set_64();
715  else
716  ansi_c.set_32();
717  }
718  else if(arch=="alpha")
720  else if(arch=="arm64" ||
721  arch=="armel" ||
722  arch=="armhf" ||
723  arch=="arm")
725  else if(arch=="mips64el" ||
726  arch=="mipsn32el" ||
727  arch=="mipsel" ||
728  arch=="mips64" ||
729  arch=="mipsn32" ||
730  arch=="mips")
732  else if(arch=="powerpc" ||
733  arch=="ppc64" ||
734  arch=="ppc64le")
736  else if(arch == "riscv64")
738  else if(arch=="sparc" ||
739  arch=="sparc64")
741  else if(arch=="ia64")
743  else if(arch=="s390x")
745  else if(arch=="s390")
747  else if(arch=="x32")
749  else if(arch=="v850")
751  else if(arch=="hppa")
753  else if(arch=="sh4")
755  else if(arch=="x86_64")
757  else if(arch=="i386")
759  else
760  {
761  // We run on something new and unknown.
762  // We verify for i386 instead.
764  ansi_c.arch="i386";
765  }
766 }
767 
768 bool configt::set(const cmdlinet &cmdline)
769 {
770  // defaults -- we match the architecture we have ourselves
771 
773 
775  // This will allow us to override by language defaults later.
777 
779  ansi_c.for_has_scope=true; // C99 or later
784  ansi_c.arch="none";
786  // NOLINTNEXTLINE(readability/casting)
787  ansi_c.NULL_is_zero=reinterpret_cast<size_t>(nullptr)==0;
788 
789  // Default is ROUND_TO_EVEN, justified by C99:
790  // 1 At program startup the floating-point environment is initialized as
791  // prescribed by IEC 60559:
792  // - All floating-point exception status flags are cleared.
793  // - The rounding direction mode is rounding to nearest.
795 
796  if(cmdline.isset("function"))
797  main=cmdline.get_value("function");
798 
799  if(cmdline.isset('D'))
800  ansi_c.defines=cmdline.get_values('D');
801 
802  if(cmdline.isset('I'))
803  ansi_c.include_paths=cmdline.get_values('I');
804 
805  if(cmdline.isset("classpath"))
806  {
807  // Specifying -classpath or -cp overrides any setting of the
808  // CLASSPATH environment variable.
809  set_classpath(cmdline.get_value("classpath"));
810  }
811  else if(cmdline.isset("cp"))
812  {
813  // Specifying -classpath or -cp overrides any setting of the
814  // CLASSPATH environment variable.
815  set_classpath(cmdline.get_value("cp"));
816  }
817  else
818  {
819  // environment variable set?
820  const char *CLASSPATH=getenv("CLASSPATH");
821  if(CLASSPATH!=nullptr)
822  set_classpath(CLASSPATH);
823  else
824  set_classpath("."); // default
825  }
826 
827  if(cmdline.isset("main-class"))
828  java.main_class=cmdline.get_value("main-class");
829 
830  if(cmdline.isset("include"))
831  ansi_c.include_files=cmdline.get_values("include");
832 
833  // the default architecture is the one we run on
834  irep_idt this_arch=this_architecture();
835  irep_idt arch=this_arch;
836 
837  // let's pick an OS now
838  // the default is the one we run on
840  irep_idt os=this_os;
841 
842  if(cmdline.isset("i386-linux"))
843  {
844  os="linux";
845  arch="i386";
846  }
847  else if(cmdline.isset("i386-win32") ||
848  cmdline.isset("win32"))
849  {
850  os="windows";
851  arch="i386";
852  }
853  else if(cmdline.isset("winx64"))
854  {
855  os="windows";
856  arch="x86_64";
857  }
858  else if(cmdline.isset("i386-macos"))
859  {
860  os="macos";
861  arch="i386";
862  }
863  else if(cmdline.isset("ppc-macos"))
864  {
865  arch="powerpc";
866  os="macos";
867  }
868 
869  if(cmdline.isset("arch"))
870  {
871  arch=cmdline.get_value("arch");
872  }
873 
874  if(cmdline.isset("os"))
875  {
876  os=cmdline.get_value("os");
877  }
878 
879  if(os=="windows")
880  {
881  // Cygwin uses GCC throughout, use i386-linux
882  // MinGW needs --win32 --gcc
885 
886  if(cmdline.isset("gcc"))
887  {
888  // There are gcc versions that target Windows (MinGW for example),
889  // and we support that.
892 
893  // enable Cygwin
894  #ifdef _WIN32
895  ansi_c.defines.push_back("__CYGWIN__");
896  #endif
897 
898  // MinGW has extra defines
899  ansi_c.defines.push_back("__int64=long long");
900  }
901  else
902  {
903  // On Windows, our default is Visual Studio.
904  // On FreeBSD, it's clang.
905  // On anything else, it's GCC as the preprocessor,
906  // but we recognize the Visual Studio language,
907  // which is somewhat inconsistent.
908  #ifdef _WIN32
911  #elif __FreeBSD__
914  #else
917  #endif
918 
920  }
921  }
922  else if(os=="macos")
923  {
928  }
929  else if(os=="linux" || os=="solaris")
930  {
935  }
936  else if(os=="freebsd")
937  {
942  }
943  else
944  {
945  // give up, but use reasonable defaults
950  }
951 
953  ansi_c.gcc__float128_type = true;
954 
955  set_arch(arch);
956 
957  if(os=="windows")
958  {
959  // note that sizeof(void *)==8, but sizeof(long)==4!
960  if(arch=="x86_64")
961  ansi_c.set_LLP64();
962 
963  // On Windows, wchar_t is unsigned 16 bit, regardless
964  // of the compiler used.
965  ansi_c.wchar_t_width=2*8;
967 
968  // long double is the same as double in Visual Studio,
969  // but it's 16 bytes with GCC with the 64-bit target.
970  if(arch=="x64_64" && cmdline.isset("gcc"))
972  else
974  }
975 
976  // Let's check some of the type widths in case we run
977  // the same architecture and OS that we are verifying for.
978  if(arch==this_arch && os==this_os)
979  {
980  INVARIANT(
981  ansi_c.int_width == sizeof(int) * 8,
982  "int width shall be equal to the system int width");
983  INVARIANT(
984  ansi_c.long_int_width == sizeof(long) * 8,
985  "long int width shall be equal to the system long int width");
986  INVARIANT(
987  ansi_c.bool_width == sizeof(bool) * 8,
988  "bool width shall be equal to the system bool width");
989  INVARIANT(
990  ansi_c.char_width == sizeof(char) * 8,
991  "char width shall be equal to the system char width");
992  INVARIANT(
993  ansi_c.short_int_width == sizeof(short) * 8,
994  "short int width shall be equal to the system short int width");
995  INVARIANT(
996  ansi_c.long_long_int_width == sizeof(long long) * 8,
997  "long long int width shall be equal to the system long long int width");
998  INVARIANT(
999  ansi_c.pointer_width == sizeof(void *) * 8,
1000  "pointer width shall be equal to the system pointer width");
1001  INVARIANT(
1002  ansi_c.single_width == sizeof(float) * 8,
1003  "float width shall be equal to the system float width");
1004  INVARIANT(
1005  ansi_c.double_width == sizeof(double) * 8,
1006  "double width shall be equal to the system double width");
1007  INVARIANT(
1008  ansi_c.char_is_unsigned == (static_cast<char>(255) == 255),
1009  "char_is_unsigned flag shall indicate system char unsignedness");
1010 
1011  #ifndef _WIN32
1012  // On Windows, long double width varies by compiler
1013  INVARIANT(
1014  ansi_c.long_double_width == sizeof(long double) * 8,
1015  "long double width shall be equal to the system long double width");
1016  #endif
1017  }
1018 
1019  // the following allows overriding the defaults
1020 
1021  if(cmdline.isset("16"))
1022  ansi_c.set_16();
1023 
1024  if(cmdline.isset("32"))
1025  ansi_c.set_32();
1026 
1027  if(cmdline.isset("64"))
1028  ansi_c.set_64();
1029 
1030  if(cmdline.isset("LP64"))
1031  ansi_c.set_LP64(); // int=32, long=64, pointer=64
1032 
1033  if(cmdline.isset("ILP64"))
1034  ansi_c.set_ILP64(); // int=64, long=64, pointer=64
1035 
1036  if(cmdline.isset("LLP64"))
1037  ansi_c.set_LLP64(); // int=32, long=32, pointer=64
1038 
1039  if(cmdline.isset("ILP32"))
1040  ansi_c.set_ILP32(); // int=32, long=32, pointer=32
1041 
1042  if(cmdline.isset("LP32"))
1043  ansi_c.set_LP32(); // int=16, long=32, pointer=32
1044 
1045  if(cmdline.isset("string-abstraction"))
1047  else
1048  ansi_c.string_abstraction=false;
1049 
1050  if(cmdline.isset("no-library"))
1052 
1053  if(cmdline.isset("little-endian"))
1055 
1056  if(cmdline.isset("big-endian"))
1058 
1059  if(cmdline.isset("little-endian") &&
1060  cmdline.isset("big-endian"))
1061  return true;
1062 
1063  if(cmdline.isset("unsigned-char"))
1064  ansi_c.char_is_unsigned=true;
1065 
1066  if(cmdline.isset("round-to-even") ||
1067  cmdline.isset("round-to-nearest"))
1069 
1070  if(cmdline.isset("round-to-plus-inf"))
1072 
1073  if(cmdline.isset("round-to-minus-inf"))
1075 
1076  if(cmdline.isset("round-to-zero"))
1078 
1079  if(cmdline.isset("object-bits"))
1080  {
1082  unsafe_string2unsigned(cmdline.get_value("object-bits"));
1083 
1084  if(!(0<bv_encoding.object_bits &&
1086  {
1088  "object-bits must be positive and less than the pointer width (" +
1090  "--object_bits");
1091  }
1092 
1094  }
1095 
1096  return false;
1097 }
1098 
1100 {
1101  // clang-format off
1102  switch(os)
1103  {
1104  case ost::OS_LINUX: return "linux";
1105  case ost::OS_MACOS: return "macos";
1106  case ost::OS_WIN: return "win";
1107  case ost::NO_OS: return "none";
1108  }
1109  // clang-format on
1110 
1111  UNREACHABLE;
1112 }
1113 
1115 {
1116  if(os=="linux")
1117  return ost::OS_LINUX;
1118  else if(os=="macos")
1119  return ost::OS_MACOS;
1120  else if(os=="win")
1121  return ost::OS_WIN;
1122  else
1123  return ost::NO_OS;
1124 }
1125 
1127  const namespacet &ns,
1128  const std::string &what)
1129 {
1130  const irep_idt id=CPROVER_PREFIX "architecture_"+what;
1131  const symbolt *symbol;
1132 
1133  const bool not_found = ns.lookup(id, symbol);
1134  INVARIANT(!not_found, id2string(id) + " must be in namespace");
1135 
1136  const exprt &tmp=symbol->value;
1137 
1138  INVARIANT(
1139  tmp.id() == ID_address_of &&
1140  to_address_of_expr(tmp).object().id() == ID_index &&
1141  to_index_expr(to_address_of_expr(tmp).object()).array().id() ==
1142  ID_string_constant,
1143  "symbol table configuration entry '" + id2string(id) +
1144  "' must be a string constant");
1145 
1146  return to_index_expr(to_address_of_expr(tmp).object()).array().get(ID_value);
1147 }
1148 
1149 static unsigned unsigned_from_ns(
1150  const namespacet &ns,
1151  const std::string &what)
1152 {
1153  const irep_idt id=CPROVER_PREFIX "architecture_"+what;
1154  const symbolt *symbol;
1155 
1156  const bool not_found = ns.lookup(id, symbol);
1157  INVARIANT(!not_found, id2string(id) + " must be in namespace");
1158 
1159  exprt tmp=symbol->value;
1160  simplify(tmp, ns);
1161 
1162  INVARIANT(
1163  tmp.id() == ID_constant,
1164  "symbol table configuration entry '" + id2string(id) +
1165  "' must be a constant");
1166 
1167  mp_integer int_value;
1168 
1169  const bool error = to_integer(to_constant_expr(tmp), int_value);
1170  INVARIANT(
1171  !error,
1172  "symbol table configuration entry '" + id2string(id) +
1173  "' must be convertible to mp_integer");
1174 
1175  return numeric_cast_v<unsigned>(int_value);
1176 }
1177 
1179  const symbol_tablet &symbol_table)
1180 {
1181  // maybe not compiled from C/C++
1182  if(symbol_table.symbols.find(CPROVER_PREFIX "architecture_" "int_width")==
1183  symbol_table.symbols.end())
1184  return;
1185 
1186  namespacet ns(symbol_table);
1187 
1188  // clear defines
1189  ansi_c.defines.clear();
1190 
1191  // first set architecture to get some defaults
1192  if(symbol_table.symbols.find(CPROVER_PREFIX "architecture_" "arch")==
1193  symbol_table.symbols.end())
1195  else
1196  set_arch(string_from_ns(ns, "arch"));
1197 
1198  ansi_c.int_width=unsigned_from_ns(ns, "int_width");
1199  ansi_c.long_int_width=unsigned_from_ns(ns, "long_int_width");
1200  ansi_c.bool_width=1*8;
1201  ansi_c.char_width=unsigned_from_ns(ns, "char_width");
1202  ansi_c.short_int_width=unsigned_from_ns(ns, "short_int_width");
1203  ansi_c.long_long_int_width=unsigned_from_ns(ns, "long_long_int_width");
1204  ansi_c.pointer_width=unsigned_from_ns(ns, "pointer_width");
1205  ansi_c.single_width=unsigned_from_ns(ns, "single_width");
1206  ansi_c.double_width=unsigned_from_ns(ns, "double_width");
1207  ansi_c.long_double_width=unsigned_from_ns(ns, "long_double_width");
1208  ansi_c.wchar_t_width=unsigned_from_ns(ns, "wchar_t_width");
1209 
1210  ansi_c.char_is_unsigned=unsigned_from_ns(ns, "char_is_unsigned")!=0;
1211  ansi_c.wchar_t_is_unsigned=unsigned_from_ns(ns, "wchar_t_is_unsigned")!=0;
1212  // for_has_scope, single_precision_constant, rounding_mode,
1213  // ts_18661_3_Floatn_types are not architectural features,
1214  // and thus not stored in namespace
1215 
1216  ansi_c.alignment=unsigned_from_ns(ns, "alignment");
1217 
1218  ansi_c.memory_operand_size=unsigned_from_ns(ns, "memory_operand_size");
1219 
1221 
1222  if(symbol_table.symbols.find(CPROVER_PREFIX "architecture_" "os")==
1223  symbol_table.symbols.end())
1225  else
1227 
1228  // NULL_is_zero=from_ns("NULL_is_zero");
1229  ansi_c.NULL_is_zero=true;
1230 
1231  // mode, preprocessor (and all preprocessor command line options),
1232  // lib, string_abstraction not stored in namespace
1233 
1234  set_object_bits_from_symbol_table(symbol_table);
1235 }
1236 
1240  const symbol_tablet &symbol_table)
1241 {
1242  // has been overridden by command line option,
1243  // thus do not apply language defaults
1245  return;
1246 
1247  // set object_bits according to entry point language
1248  if(const auto maybe_symbol=symbol_table.lookup(CPROVER_PREFIX "_start"))
1249  {
1250  const symbolt &entry_point_symbol=*maybe_symbol;
1251 
1252  if(entry_point_symbol.mode==ID_java)
1254  else if(entry_point_symbol.mode==ID_C)
1256  else if(entry_point_symbol.mode==ID_cpp)
1260  "object_bits should fit into pointer width");
1261  }
1262 }
1263 
1265 {
1266  return "Running with "+std::to_string(bv_encoding.object_bits)+
1267  " object bits, "+
1269  " offset bits ("+
1270  (bv_encoding.is_object_bits_default ? "default" : "user-specified")+
1271  ")";
1272 }
1273 
1274 // clang-format off
1276 {
1277  irep_idt this_arch;
1278 
1279  // following http://wiki.debian.org/ArchitectureSpecificsMemo
1280 
1281  #ifdef __alpha__
1282  this_arch = "alpha";
1283  #elif defined(__armel__)
1284  this_arch = "armel";
1285  #elif defined(__aarch64__)
1286  this_arch = "arm64";
1287  #elif defined(__arm__)
1288  #ifdef __ARM_PCS_VFP
1289  this_arch = "armhf"; // variant of arm with hard float
1290  #else
1291  this_arch = "arm";
1292  #endif
1293  #elif defined(__mipsel__)
1294  #if _MIPS_SIM==_ABIO32
1295  this_arch = "mipsel";
1296  #elif _MIPS_SIM==_ABIN32
1297  this_arch = "mipsn32el";
1298  #else
1299  this_arch = "mips64el";
1300  #endif
1301  #elif defined(__mips__)
1302  #if _MIPS_SIM==_ABIO32
1303  this_arch = "mips";
1304  #elif _MIPS_SIM==_ABIN32
1305  this_arch = "mipsn32";
1306  #else
1307  this_arch = "mips64";
1308  #endif
1309  #elif defined(__powerpc__)
1310  #if defined(__ppc64__) || defined(__PPC64__) || \
1311  defined(__powerpc64__) || defined(__POWERPC64__)
1312  #ifdef __LITTLE_ENDIAN__
1313  this_arch = "ppc64le";
1314  #else
1315  this_arch = "ppc64";
1316  #endif
1317  #else
1318  this_arch = "powerpc";
1319  #endif
1320  #elif defined(__riscv)
1321  this_arch = "riscv64";
1322  #elif defined(__sparc__)
1323  #ifdef __arch64__
1324  this_arch = "sparc64";
1325  #else
1326  this_arch = "sparc";
1327  #endif
1328  #elif defined(__ia64__)
1329  this_arch = "ia64";
1330  #elif defined(__s390x__)
1331  this_arch = "s390x";
1332  #elif defined(__s390__)
1333  this_arch = "s390";
1334  #elif defined(__x86_64__)
1335  #ifdef __ILP32__
1336  this_arch = "x32"; // variant of x86_64 with 32-bit pointers
1337  #else
1338  this_arch = "x86_64";
1339  #endif
1340  #elif defined(__i386__)
1341  this_arch = "i386";
1342  #elif defined(_WIN64)
1343  this_arch = "x86_64";
1344  #elif defined(_WIN32)
1345  this_arch = "i386";
1346  #elif defined(__hppa__)
1347  this_arch = "hppa";
1348  #elif defined(__sh__)
1349  this_arch = "sh4";
1350  #else
1351  // something new and unknown!
1352  this_arch = "unknown";
1353  #endif
1354 
1355  return this_arch;
1356 }
1357 // clang-format on
1358 
1359 void configt::set_classpath(const std::string &cp)
1360 {
1361 // These are separated by colons on Unix, and semicolons on
1362 // Windows.
1363 #ifdef _WIN32
1364  const char cp_separator = ';';
1365 #else
1366  const char cp_separator = ':';
1367 #endif
1368 
1369  std::vector<std::string> class_path =
1370  split_string(cp, cp_separator);
1371  java.classpath.insert(
1372  java.classpath.end(), class_path.begin(), class_path.end());
1373 }
1374 
1376 {
1377  irep_idt this_os;
1378 
1379  #ifdef _WIN32
1380  this_os="windows";
1381  #elif __APPLE__
1382  this_os="macos";
1383  #elif __FreeBSD__
1384  this_os="freebsd";
1385  #elif __linux__
1386  this_os="linux";
1387  #elif __SVR4
1388  this_os="solaris";
1389  #else
1390  this_os="unknown";
1391  #endif
1392 
1393  return this_os;
1394 }
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
exception_utils.h
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
configt::ansi_ct::ts_18661_3_Floatn_types
bool ts_18661_3_Floatn_types
Definition: config.h:46
configt::bv_encodingt::object_bits
std::size_t object_bits
Definition: config.h:166
configt::ansi_ct::defines
std::list< std::string > defines
Definition: config.h:122
configt::ansi_ct::bool_width
std::size_t bool_width
Definition: config.h:33
configt::object_bits_info
std::string object_bits_info()
Definition: config.cpp:1264
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
configt::ansi_ct::NULL_is_zero
bool NULL_is_zero
Definition: config.h:88
configt::javat::main_class
irep_idt main_class
Definition: config.h:158
configt::ansi_ct::string_to_os
static ost string_to_os(const std::string &)
Definition: config.cpp:1114
configt::ansi_ct::ost
ost
Definition: config.h:79
configt::bv_encoding
struct configt::bv_encodingt bv_encoding
arith_tools.h
cmdlinet::isset
virtual bool isset(char option) const
Definition: cmdline.cpp:28
configt::ansi_ct::for_has_scope
bool for_has_scope
Definition: config.h:45
configt::cppt::cpp_standardt
cpp_standardt
Definition: config.h:138
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:41
configt::ansi_ct::endiannesst
endiannesst
Definition: config.h:76
configt::ansi_ct::ost::OS_MACOS
@ OS_MACOS
string_utils.h
configt::ansi_ct::preprocessort::CLANG
@ CLANG
configt::ansi_ct::include_paths
std::list< std::string > include_paths
Definition: config.h:125
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1353
configt::ansi_ct::set_arch_spec_mips
void set_arch_spec_mips(const irep_idt &subarch)
Definition: config.cpp:352
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
configt::ansi_ct::os
ost os
Definition: config.h:80
configt::ansi_ct::flavourt::VISUAL_STUDIO
@ 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::main
optionalt< std::string > main
Definition: config.h:173
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
exprt
Base class for all expressions.
Definition: expr.h:53
configt::ansi_ct::rounding_mode
ieee_floatt::rounding_modet rounding_mode
Definition: config.h:56
configt::ansi_ct::alignment
std::size_t alignment
Definition: config.h:70
to_integer
bool to_integer(const constant_exprt &expr, mp_integer &int_value)
Convert a constant expression expr to an arbitrary-precision integer.
Definition: arith_tools.cpp:19
configt::ansi_ct::set_LP32
void set_LP32()
int=16, long=32, pointer=32
Definition: config.cpp:130
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:55
configt::ansi_ct::set_arch_spec_power
void set_arch_spec_power(const irep_idt &subarch)
Definition: config.cpp:219
configt::ansi_c
struct configt::ansi_ct ansi_c
namespace.h
configt::ansi_ct::set_arch_spec_hppa
void set_arch_spec_hppa()
Definition: config.cpp:616
configt::javat::classpath
classpatht classpath
Definition: config.h:157
configt::ansi_ct::libt::LIB_NONE
@ LIB_NONE
configt::ansi_ct::flavourt::CLANG
@ CLANG
configt
Globally accessible architectural configuration.
Definition: config.h:26
configt::ansi_ct::char_width
std::size_t char_width
Definition: config.h:34
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
configt::ansi_ct::endiannesst::NO_ENDIANNESS
@ NO_ENDIANNESS
configt::ansi_ct::set_arch_spec_ia64
void set_arch_spec_ia64()
Definition: config.cpp:525
string2int.h
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
split_string
void split_string(const std::string &s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)
Given a string s, split into a sequence of substrings when separated by specified delimiter.
Definition: string_utils.cpp:40
configt::ansi_ct::endiannesst::IS_LITTLE_ENDIAN
@ IS_LITTLE_ENDIAN
cmdlinet
Definition: cmdline.h:21
symbolt::mode
irep_idt mode
Language mode.
Definition: symbol.h:49
configt::ansi_ct::set_arch_spec_arm
void set_arch_spec_arm(const irep_idt &subarch)
Definition: config.cpp:280
unsigned_from_ns
static unsigned unsigned_from_ns(const namespacet &ns, const std::string &what)
Definition: config.cpp:1149
configt::ansi_ct::wchar_t_is_unsigned
bool wchar_t_is_unsigned
Definition: config.h:44
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
to_address_of_expr
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: std_expr.h:2852
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
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:39
configt::ansi_ct::preprocessor
preprocessort preprocessor
Definition: config.h:120
configt::ansi_ct::set_arch_spec_riscv64
void set_arch_spec_riscv64()
Definition: config.cpp:402
configt::ansi_ct::default_object_bits
static const std::size_t default_object_bits
Definition: config.h:133
configt::cppt::default_object_bits
static const std::size_t default_object_bits
Definition: config.h:146
configt::ansi_ct::string_abstraction
bool string_abstraction
Definition: config.h:131
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:167
configt::ansi_ct::memory_operand_size
std::size_t memory_operand_size
Definition: config.h:74
cmdlinet::get_value
std::string get_value(char option) const
Definition: cmdline.cpp:46
configt::ansi_ct::ost::OS_LINUX
@ OS_LINUX
simplify
bool simplify(exprt &expr, const namespacet &ns)
Definition: simplify_expr.cpp:2693
configt::ansi_ct::long_long_int_width
std::size_t long_long_int_width
Definition: config.h:36
configt::ansi_ct::set_ILP64
void set_ILP64()
int=64, long=64, pointer=64
Definition: config.cpp:70
alignment
mp_integer alignment(const typet &type, const namespacet &ns)
Definition: padding.cpp:21
configt::this_operating_system
static irep_idt this_operating_system()
Definition: config.cpp:1375
index_exprt::array
exprt & array()
Definition: std_expr.h:1315
configt::ansi_ct::arch
irep_idt arch
Definition: config.h:85
configt::ansi_ct::ost::OS_WIN
@ OS_WIN
irept::id
const irep_idt & id() const
Definition: irep.h:418
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:1178
configt::ansi_ct::os_to_string
static std::string os_to_string(ost)
Definition: config.cpp:1099
cprover_prefix.h
configt::javat::default_object_bits
static const std::size_t default_object_bits
Definition: config.h:160
configt::ansi_ct::include_files
std::list< std::string > include_files
Definition: config.h:126
configt::ansi_ct::ost::NO_OS
@ NO_OS
configt::ansi_ct::preprocessort::GCC
@ GCC
configt::ansi_ct::default_c_standard
static c_standardt default_c_standard()
Definition: config.cpp:675
configt::ansi_ct::set_ILP32
void set_ILP32()
int=32, long=32, pointer=32
Definition: config.cpp:110
config
configt config
Definition: config.cpp:24
simplify_expr.h
configt::this_architecture
static irep_idt this_architecture()
Definition: config.cpp:1275
configt::ansi_ct::libt::LIB_FULL
@ LIB_FULL
configt::ansi_ct::mode
flavourt mode
Definition: config.h:116
symbolt::value
exprt value
Initial value of symbol.
Definition: symbol.h:34
configt::ansi_ct::preprocessort::VISUAL_STUDIO
@ VISUAL_STUDIO
ieee_floatt::ROUND_TO_PLUS_INF
@ ROUND_TO_PLUS_INF
Definition: ieee_float.h:128
configt::ansi_ct::endiannesst::IS_BIG_ENDIAN
@ IS_BIG_ENDIAN
ieee_floatt::ROUND_TO_EVEN
@ ROUND_TO_EVEN
Definition: ieee_float.h:127
string_from_ns
static irep_idt string_from_ns(const namespacet &ns, const std::string &what)
Definition: config.cpp:1126
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
cmdline.h
symbolt
Symbol table entry.
Definition: symbol.h:28
configt::set
bool set(const cmdlinet &cmdline)
Definition: config.cpp:768
configt::cppt::default_cpp_standard
static cpp_standardt default_cpp_standard()
Definition: config.cpp:690
configt::ansi_ct::c_standard
enum configt::ansi_ct::c_standardt c_standard
configt::ansi_ct::set_arch_spec_sparc
void set_arch_spec_sparc(const irep_idt &subarch)
Definition: config.cpp:485
symbol_table_baset::symbols
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Definition: symbol_table_base.h:30
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:40
CPROVER_PREFIX
#define CPROVER_PREFIX
Definition: cprover_prefix.h:14
unsafe_string2unsigned
unsigned unsafe_string2unsigned(const std::string &str, int base)
Definition: string2int.cpp:38
configt::java
struct configt::javat java
configt::cppt::cpp_standardt::CPP14
@ 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
config.h
configt::ansi_ct::short_int_width
std::size_t short_int_width
Definition: config.h:35
configt::ansi_ct::char_is_unsigned
bool char_is_unsigned
Definition: config.h:44
configt::ansi_ct::flavourt::GCC
@ GCC
symbol_table_baset::lookup
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Definition: symbol_table_base.h:95
configt::ansi_ct::set_arch_spec_x86_64
void set_arch_spec_x86_64()
Definition: config.cpp:181
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:37
configt::ansi_ct::single_width
std::size_t single_width
Definition: config.h:38
configt::ansi_ct::lib
libt lib
Definition: config.h:129
symbol_table.h
Author: Diffblue Ltd.
configt::cpp
struct configt::cppt cpp
configt::set_classpath
void set_classpath(const std::string &cp)
Definition: config.cpp:1359
invalid_command_line_argument_exceptiont
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
Definition: exception_utils.h:38
configt::ansi_ct::single_precision_constant
bool single_precision_constant
Definition: config.h:48
configt::bv_encodingt::default_object_bits
static const std::size_t default_object_bits
Definition: config.h:169
cmdlinet::get_values
const std::list< std::string > & get_values(const std::string &option) const
Definition: cmdline.cpp:107
configt::ansi_ct::gcc__float128_type
bool gcc__float128_type
Definition: config.h:47
std_expr.h
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:1239
configt::ansi_ct::c_standardt
c_standardt
Definition: config.h:49
configt::set_arch
void set_arch(const irep_idt &)
Definition: config.cpp:702
configt::ansi_ct::int_width
std::size_t int_width
Definition: config.h:31
ieee_floatt::ROUND_TO_MINUS_INF
@ ROUND_TO_MINUS_INF
Definition: ieee_float.h:127
configt::ansi_ct::endianness
endiannesst endianness
Definition: config.h:77
ieee_floatt::ROUND_TO_ZERO
@ ROUND_TO_ZERO
Definition: ieee_float.h:128
configt::ansi_ct::long_int_width
std::size_t long_int_width
Definition: config.h:32
validation_modet::INVARIANT
@ INVARIANT
configt::cppt::cpp_standard
enum configt::cppt::cpp_standardt cpp_standard
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:3968