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 "pointer_expr.h"
19 #include "simplify_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 
593 {
594  // The Renesas V850 is a 32-bit microprocessor used in
595  // many automotive applications. This spec is written from the
596  // architecture manual rather than having access to a running
597  // system. Thus some assumptions have been made.
598 
599  set_ILP32();
600 
601  // Technically, the V850's don't have floating-point at all.
602  // However, the RH850, aimed at automotive has both 32-bit and
603  // 64-bit IEEE-754 float.
604  double_width=8*8;
605  long_double_width=8*8;
606  endianness=endiannesst::IS_LITTLE_ENDIAN;
607 
608  // Without information about the compiler and RTOS, these are guesses
609  char_is_unsigned=false;
610  NULL_is_zero=true;
611 
612  // No preprocessor definitions due to lack of information
613 }
614 
616 {
617  set_ILP32();
618  long_double_width=8*8; // different from i386
619  endianness=endiannesst::IS_BIG_ENDIAN;
620  char_is_unsigned=false;
621  NULL_is_zero=true;
622 
623  switch(mode)
624  {
625  case flavourt::GCC:
626  defines.push_back("__hppa__");
627  break;
628 
629  case flavourt::VISUAL_STUDIO:
630  UNREACHABLE; // not supported by Visual Studio
631  break;
632 
633  case flavourt::CLANG:
634  case flavourt::CODEWARRIOR:
635  case flavourt::ARM:
636  case flavourt::ANSI:
637  break;
638 
639  case flavourt::NONE:
640  UNREACHABLE;
641  }
642 }
643 
645 {
646  set_ILP32();
647  long_double_width=8*8; // different from i386
648  endianness=endiannesst::IS_LITTLE_ENDIAN;
649  char_is_unsigned=false;
650  NULL_is_zero=true;
651 
652  switch(mode)
653  {
654  case flavourt::GCC:
655  defines.push_back("__sh__");
656  defines.push_back("__SH4__");
657  break;
658 
659  case flavourt::VISUAL_STUDIO:
660  UNREACHABLE; // not supported by Visual Studio
661  break;
662 
663  case flavourt::CLANG:
664  case flavourt::CODEWARRIOR:
665  case flavourt::ARM:
666  case flavourt::ANSI:
667  break;
668 
669  case flavourt::NONE:
670  UNREACHABLE;
671  }
672 }
673 
675 {
676 #if defined(__APPLE__)
677  // By default, clang on the Mac builds C code in GNU C11
678  return c_standardt::C11;
679 #elif defined(__FreeBSD__) || defined(__OpenBSD__)
680  // By default, clang on FreeBSD builds C code in GNU C99
681  // By default, clang on OpenBSD builds C code in C99
682  return c_standardt::C99;
683 #else
684  // By default, gcc 5.4 or higher use gnu11; older versions use gnu89
685  return c_standardt::C11;
686 #endif
687 }
688 
690 {
691  // g++ 6.3 uses gnu++14
692  // g++ 5.4 uses gnu++98
693  // clang 6.0 uses c++14
694  #if defined _WIN32
695  return cpp_standardt::CPP14;
696  #else
697  return cpp_standardt::CPP98;
698  #endif
699 }
700 
701 void configt::set_arch(const irep_idt &arch)
702 {
703  ansi_c.arch=arch;
704 
705  if(arch=="none")
706  {
707  // the architecture for people who can't commit
710  ansi_c.NULL_is_zero=false;
711 
712  if(sizeof(long int)==8)
713  ansi_c.set_64();
714  else
715  ansi_c.set_32();
716  }
717  else if(arch=="alpha")
719  else if(arch=="arm64" ||
720  arch=="armel" ||
721  arch=="armhf" ||
722  arch=="arm")
724  else if(arch=="mips64el" ||
725  arch=="mipsn32el" ||
726  arch=="mipsel" ||
727  arch=="mips64" ||
728  arch=="mipsn32" ||
729  arch=="mips")
731  else if(arch=="powerpc" ||
732  arch=="ppc64" ||
733  arch=="ppc64le")
735  else if(arch == "riscv64")
737  else if(arch=="sparc" ||
738  arch=="sparc64")
740  else if(arch=="ia64")
742  else if(arch=="s390x")
744  else if(arch=="s390")
746  else if(arch=="x32")
748  else if(arch=="v850")
750  else if(arch=="hppa")
752  else if(arch=="sh4")
754  else if(arch=="x86_64")
756  else if(arch=="i386")
758  else
759  {
760  // We run on something new and unknown.
761  // We verify for i386 instead.
763  ansi_c.arch="i386";
764  }
765 }
766 
775  const std::string &argument,
776  const std::size_t pointer_width)
777 {
778  const auto throw_for_reason = [&](const std::string &reason) {
780  "Value of \"" + argument + "\" given for object-bits is " + reason +
781  ". object-bits must be positive and less than the pointer width (" +
782  std::to_string(pointer_width) + ") ",
783  "--object_bits");
784  };
785  const auto object_bits = string2optional<unsigned int>(argument);
786  if(!object_bits)
787  throw_for_reason("not a valid unsigned integer");
788  if(*object_bits == 0 || *object_bits >= pointer_width)
789  throw_for_reason("out of range");
790 
792  bv_encoding.object_bits = *object_bits;
794  return bv_encoding;
795 }
796 
797 bool configt::set(const cmdlinet &cmdline)
798 {
799  // defaults -- we match the architecture we have ourselves
800 
802 
804  ansi_c.for_has_scope=true; // C99 or later
809  ansi_c.arch="none";
811  // NOLINTNEXTLINE(readability/casting)
812  ansi_c.NULL_is_zero=reinterpret_cast<size_t>(nullptr)==0;
813 
814  // Default is ROUND_TO_EVEN, justified by C99:
815  // 1 At program startup the floating-point environment is initialized as
816  // prescribed by IEC 60559:
817  // - All floating-point exception status flags are cleared.
818  // - The rounding direction mode is rounding to nearest.
820 
821  if(cmdline.isset("function"))
822  main=cmdline.get_value("function");
823 
824  if(cmdline.isset('D'))
825  ansi_c.defines=cmdline.get_values('D');
826 
827  if(cmdline.isset('I'))
828  ansi_c.include_paths=cmdline.get_values('I');
829 
830  if(cmdline.isset("classpath"))
831  {
832  // Specifying -classpath or -cp overrides any setting of the
833  // CLASSPATH environment variable.
834  set_classpath(cmdline.get_value("classpath"));
835  }
836  else if(cmdline.isset("cp"))
837  {
838  // Specifying -classpath or -cp overrides any setting of the
839  // CLASSPATH environment variable.
840  set_classpath(cmdline.get_value("cp"));
841  }
842  else
843  {
844  // environment variable set?
845  const char *CLASSPATH=getenv("CLASSPATH");
846  if(CLASSPATH!=nullptr)
847  set_classpath(CLASSPATH);
848  else
849  set_classpath("."); // default
850  }
851 
852  if(cmdline.isset("main-class"))
853  java.main_class=cmdline.get_value("main-class");
854 
855  if(cmdline.isset("include"))
856  ansi_c.include_files=cmdline.get_values("include");
857 
858  // the default architecture is the one we run on
859  irep_idt this_arch=this_architecture();
860  irep_idt arch=this_arch;
861 
862  // let's pick an OS now
863  // the default is the one we run on
865  irep_idt os=this_os;
866 
867  if(cmdline.isset("i386-linux"))
868  {
869  os="linux";
870  arch="i386";
871  }
872  else if(cmdline.isset("i386-win32") ||
873  cmdline.isset("win32"))
874  {
875  os="windows";
876  arch="i386";
877  }
878  else if(cmdline.isset("winx64"))
879  {
880  os="windows";
881  arch="x86_64";
882  }
883  else if(cmdline.isset("i386-macos"))
884  {
885  os="macos";
886  arch="i386";
887  }
888  else if(cmdline.isset("ppc-macos"))
889  {
890  arch="powerpc";
891  os="macos";
892  }
893 
894  if(cmdline.isset("arch"))
895  {
896  arch=cmdline.get_value("arch");
897  }
898 
899  if(cmdline.isset("os"))
900  {
901  os=cmdline.get_value("os");
902  }
903 
904  if(os=="windows")
905  {
906  // Cygwin uses GCC throughout, use i386-linux
907  // MinGW needs --win32 --gcc
910 
911  if(cmdline.isset("gcc"))
912  {
913  // There are gcc versions that target Windows (MinGW for example),
914  // and we support that.
917 
918  // enable Cygwin
919  #ifdef _WIN32
920  ansi_c.defines.push_back("__CYGWIN__");
921  #endif
922 
923  // MinGW has extra defines
924  ansi_c.defines.push_back("__int64=long long");
925  }
926  else
927  {
928  // On Windows, our default is Visual Studio.
929  // On FreeBSD, it's clang.
930  // On anything else, it's GCC as the preprocessor,
931  // but we recognize the Visual Studio language,
932  // which is somewhat inconsistent.
933  #ifdef _WIN32
936  #elif __FreeBSD__
939  #else
942  #endif
943 
945  }
946  }
947  else if(os=="macos")
948  {
953  }
954  else if(os=="linux" || os=="solaris")
955  {
960  }
961  else if(os=="freebsd")
962  {
967  }
968  else
969  {
970  // give up, but use reasonable defaults
975  }
976 
978  ansi_c.gcc__float128_type = true;
979 
980  set_arch(arch);
981 
982  if(os=="windows")
983  {
984  // note that sizeof(void *)==8, but sizeof(long)==4!
985  if(arch=="x86_64")
986  ansi_c.set_LLP64();
987 
988  // On Windows, wchar_t is unsigned 16 bit, regardless
989  // of the compiler used.
990  ansi_c.wchar_t_width=2*8;
992 
993  // long double is the same as double in Visual Studio,
994  // but it's 16 bytes with GCC with the 64-bit target.
995  if(arch=="x64_64" && cmdline.isset("gcc"))
997  else
999  }
1000  else if(os == "macos" && arch == "arm64")
1001  {
1002  // https://developer.apple.com/documentation/xcode/
1003  // writing_arm64_code_for_apple_platforms#//apple_ref/doc/uid/TP40013702-SW1
1004  ansi_c.char_is_unsigned = false;
1005  ansi_c.long_double_width = 8 * 8;
1006  }
1007 
1008  // Let's check some of the type widths in case we run
1009  // the same architecture and OS that we are verifying for.
1010  if(arch==this_arch && os==this_os)
1011  {
1012  INVARIANT(
1013  ansi_c.int_width == sizeof(int) * 8,
1014  "int width shall be equal to the system int width");
1015  INVARIANT(
1016  ansi_c.long_int_width == sizeof(long) * 8,
1017  "long int width shall be equal to the system long int width");
1018  INVARIANT(
1019  ansi_c.bool_width == sizeof(bool) * 8,
1020  "bool width shall be equal to the system bool width");
1021  INVARIANT(
1022  ansi_c.char_width == sizeof(char) * 8,
1023  "char width shall be equal to the system char width");
1024  INVARIANT(
1025  ansi_c.short_int_width == sizeof(short) * 8,
1026  "short int width shall be equal to the system short int width");
1027  INVARIANT(
1028  ansi_c.long_long_int_width == sizeof(long long) * 8,
1029  "long long int width shall be equal to the system long long int width");
1030  INVARIANT(
1031  ansi_c.pointer_width == sizeof(void *) * 8,
1032  "pointer width shall be equal to the system pointer width");
1033  INVARIANT(
1034  ansi_c.single_width == sizeof(float) * 8,
1035  "float width shall be equal to the system float width");
1036  INVARIANT(
1037  ansi_c.double_width == sizeof(double) * 8,
1038  "double width shall be equal to the system double width");
1039  INVARIANT(
1040  ansi_c.char_is_unsigned == (static_cast<char>(255) == 255),
1041  "char_is_unsigned flag shall indicate system char unsignedness");
1042 
1043  #ifndef _WIN32
1044  // On Windows, long double width varies by compiler
1045  INVARIANT(
1046  ansi_c.long_double_width == sizeof(long double) * 8,
1047  "long double width shall be equal to the system long double width");
1048  #endif
1049  }
1050 
1051  // the following allows overriding the defaults
1052 
1053  if(cmdline.isset("16"))
1054  ansi_c.set_16();
1055 
1056  if(cmdline.isset("32"))
1057  ansi_c.set_32();
1058 
1059  if(cmdline.isset("64"))
1060  ansi_c.set_64();
1061 
1062  if(cmdline.isset("LP64"))
1063  ansi_c.set_LP64(); // int=32, long=64, pointer=64
1064 
1065  if(cmdline.isset("ILP64"))
1066  ansi_c.set_ILP64(); // int=64, long=64, pointer=64
1067 
1068  if(cmdline.isset("LLP64"))
1069  ansi_c.set_LLP64(); // int=32, long=32, pointer=64
1070 
1071  if(cmdline.isset("ILP32"))
1072  ansi_c.set_ILP32(); // int=32, long=32, pointer=32
1073 
1074  if(cmdline.isset("LP32"))
1075  ansi_c.set_LP32(); // int=16, long=32, pointer=32
1076 
1077  if(cmdline.isset("string-abstraction"))
1079  else
1080  ansi_c.string_abstraction=false;
1081 
1082  if(cmdline.isset("no-library"))
1084 
1085  if(cmdline.isset("little-endian"))
1087 
1088  if(cmdline.isset("big-endian"))
1090 
1091  if(cmdline.isset("little-endian") &&
1092  cmdline.isset("big-endian"))
1093  return true;
1094 
1095  if(cmdline.isset("unsigned-char"))
1096  ansi_c.char_is_unsigned=true;
1097 
1098  if(cmdline.isset("round-to-even") ||
1099  cmdline.isset("round-to-nearest"))
1101 
1102  if(cmdline.isset("round-to-plus-inf"))
1104 
1105  if(cmdline.isset("round-to-minus-inf"))
1107 
1108  if(cmdline.isset("round-to-zero"))
1110 
1111  if(cmdline.isset("object-bits"))
1112  {
1114  cmdline.get_value("object-bits"), ansi_c.pointer_width);
1115  }
1116 
1117  if(cmdline.isset("malloc-fail-assert") && cmdline.isset("malloc-fail-null"))
1118  {
1120  "at most one malloc failure mode is acceptable", "--malloc-fail-null"};
1121  }
1122  if(cmdline.isset("malloc-fail-null"))
1124  if(cmdline.isset("malloc-fail-assert"))
1126 
1127  ansi_c.malloc_may_fail = cmdline.isset("malloc-may-fail");
1128 
1129  if(cmdline.isset("c89"))
1130  ansi_c.set_c89();
1131 
1132  if(cmdline.isset("c99"))
1133  ansi_c.set_c99();
1134 
1135  if(cmdline.isset("c11"))
1136  ansi_c.set_c11();
1137 
1138  if(cmdline.isset("cpp98"))
1139  cpp.set_cpp98();
1140 
1141  if(cmdline.isset("cpp03"))
1142  cpp.set_cpp03();
1143 
1144  if(cmdline.isset("cpp11"))
1145  cpp.set_cpp11();
1146 
1147  return false;
1148 }
1149 
1151 {
1152  // clang-format off
1153  switch(os)
1154  {
1155  case ost::OS_LINUX: return "linux";
1156  case ost::OS_MACOS: return "macos";
1157  case ost::OS_WIN: return "win";
1158  case ost::NO_OS: return "none";
1159  }
1160  // clang-format on
1161 
1162  UNREACHABLE;
1163 }
1164 
1166 {
1167  if(os=="linux")
1168  return ost::OS_LINUX;
1169  else if(os=="macos")
1170  return ost::OS_MACOS;
1171  else if(os=="win")
1172  return ost::OS_WIN;
1173  else
1174  return ost::NO_OS;
1175 }
1176 
1178  const namespacet &ns,
1179  const std::string &what)
1180 {
1181  const irep_idt id=CPROVER_PREFIX "architecture_"+what;
1182  const symbolt *symbol;
1183 
1184  const bool not_found = ns.lookup(id, symbol);
1185  INVARIANT(!not_found, id2string(id) + " must be in namespace");
1186 
1187  const exprt &tmp=symbol->value;
1188 
1189  INVARIANT(
1190  tmp.id() == ID_address_of &&
1191  to_address_of_expr(tmp).object().id() == ID_index &&
1192  to_index_expr(to_address_of_expr(tmp).object()).array().id() ==
1193  ID_string_constant,
1194  "symbol table configuration entry '" + id2string(id) +
1195  "' must be a string constant");
1196 
1197  return to_index_expr(to_address_of_expr(tmp).object()).array().get(ID_value);
1198 }
1199 
1200 static unsigned unsigned_from_ns(
1201  const namespacet &ns,
1202  const std::string &what)
1203 {
1204  const irep_idt id=CPROVER_PREFIX "architecture_"+what;
1205  const symbolt *symbol;
1206 
1207  const bool not_found = ns.lookup(id, symbol);
1208  INVARIANT(!not_found, id2string(id) + " must be in namespace");
1209 
1210  exprt tmp=symbol->value;
1211  simplify(tmp, ns);
1212 
1213  INVARIANT(
1214  tmp.id() == ID_constant,
1215  "symbol table configuration entry '" + id2string(id) +
1216  "' must be a constant");
1217 
1218  mp_integer int_value;
1219 
1220  const bool error = to_integer(to_constant_expr(tmp), int_value);
1221  INVARIANT(
1222  !error,
1223  "symbol table configuration entry '" + id2string(id) +
1224  "' must be convertible to mp_integer");
1225 
1226  return numeric_cast_v<unsigned>(int_value);
1227 }
1228 
1230  const symbol_tablet &symbol_table)
1231 {
1232  // maybe not compiled from C/C++
1233  if(symbol_table.symbols.find(CPROVER_PREFIX "architecture_" "int_width")==
1234  symbol_table.symbols.end())
1235  return;
1236 
1237  namespacet ns(symbol_table);
1238 
1239  // clear defines
1240  ansi_c.defines.clear();
1241 
1242  // first set architecture to get some defaults
1243  if(symbol_table.symbols.find(CPROVER_PREFIX "architecture_" "arch")==
1244  symbol_table.symbols.end())
1246  else
1247  set_arch(string_from_ns(ns, "arch"));
1248 
1249  ansi_c.int_width=unsigned_from_ns(ns, "int_width");
1250  ansi_c.long_int_width=unsigned_from_ns(ns, "long_int_width");
1251  ansi_c.bool_width=1*8;
1252  ansi_c.char_width=unsigned_from_ns(ns, "char_width");
1253  ansi_c.short_int_width=unsigned_from_ns(ns, "short_int_width");
1254  ansi_c.long_long_int_width=unsigned_from_ns(ns, "long_long_int_width");
1255  ansi_c.pointer_width=unsigned_from_ns(ns, "pointer_width");
1256  ansi_c.single_width=unsigned_from_ns(ns, "single_width");
1257  ansi_c.double_width=unsigned_from_ns(ns, "double_width");
1258  ansi_c.long_double_width=unsigned_from_ns(ns, "long_double_width");
1259  ansi_c.wchar_t_width=unsigned_from_ns(ns, "wchar_t_width");
1260 
1261  ansi_c.char_is_unsigned=unsigned_from_ns(ns, "char_is_unsigned")!=0;
1262  ansi_c.wchar_t_is_unsigned=unsigned_from_ns(ns, "wchar_t_is_unsigned")!=0;
1263  // for_has_scope, single_precision_constant, rounding_mode,
1264  // ts_18661_3_Floatn_types are not architectural features,
1265  // and thus not stored in namespace
1266 
1267  ansi_c.alignment=unsigned_from_ns(ns, "alignment");
1268 
1269  ansi_c.memory_operand_size=unsigned_from_ns(ns, "memory_operand_size");
1270 
1272 
1273  if(symbol_table.symbols.find(CPROVER_PREFIX "architecture_" "os")==
1274  symbol_table.symbols.end())
1276  else
1278 
1279  ansi_c.NULL_is_zero = unsigned_from_ns(ns, "NULL_is_zero") != 0;
1280 
1281  // mode, preprocessor (and all preprocessor command line options),
1282  // lib, string_abstraction not stored in namespace
1283 
1284  set_object_bits_from_symbol_table(symbol_table);
1285 }
1286 
1290  const symbol_tablet &symbol_table)
1291 {
1292  // has been overridden by command line option,
1293  // thus do not apply language defaults
1295  return;
1296 
1297  // set object_bits according to entry point language
1298  if(const auto maybe_symbol=symbol_table.lookup(CPROVER_PREFIX "_start"))
1299  {
1300  const symbolt &entry_point_symbol=*maybe_symbol;
1301 
1302  if(entry_point_symbol.mode==ID_java)
1304  else if(entry_point_symbol.mode==ID_C)
1306  else if(entry_point_symbol.mode==ID_cpp)
1310  "object_bits should fit into pointer width");
1311  }
1312 }
1313 
1315 {
1316  return "Running with "+std::to_string(bv_encoding.object_bits)+
1317  " object bits, "+
1319  " offset bits ("+
1320  (bv_encoding.is_object_bits_default ? "default" : "user-specified")+
1321  ")";
1322 }
1323 
1324 // clang-format off
1326 {
1327  irep_idt this_arch;
1328 
1329  // following http://wiki.debian.org/ArchitectureSpecificsMemo
1330 
1331  #ifdef __alpha__
1332  this_arch = "alpha";
1333  #elif defined(__armel__)
1334  this_arch = "armel";
1335  #elif defined(__aarch64__)
1336  this_arch = "arm64";
1337  #elif defined(__arm__)
1338  #ifdef __ARM_PCS_VFP
1339  this_arch = "armhf"; // variant of arm with hard float
1340  #else
1341  this_arch = "arm";
1342  #endif
1343  #elif defined(__mipsel__)
1344  #if _MIPS_SIM==_ABIO32
1345  this_arch = "mipsel";
1346  #elif _MIPS_SIM==_ABIN32
1347  this_arch = "mipsn32el";
1348  #else
1349  this_arch = "mips64el";
1350  #endif
1351  #elif defined(__mips__)
1352  #if _MIPS_SIM==_ABIO32
1353  this_arch = "mips";
1354  #elif _MIPS_SIM==_ABIN32
1355  this_arch = "mipsn32";
1356  #else
1357  this_arch = "mips64";
1358  #endif
1359  #elif defined(__powerpc__)
1360  #if defined(__ppc64__) || defined(__PPC64__) || \
1361  defined(__powerpc64__) || defined(__POWERPC64__)
1362  #ifdef __LITTLE_ENDIAN__
1363  this_arch = "ppc64le";
1364  #else
1365  this_arch = "ppc64";
1366  #endif
1367  #else
1368  this_arch = "powerpc";
1369  #endif
1370  #elif defined(__riscv)
1371  this_arch = "riscv64";
1372  #elif defined(__sparc__)
1373  #ifdef __arch64__
1374  this_arch = "sparc64";
1375  #else
1376  this_arch = "sparc";
1377  #endif
1378  #elif defined(__ia64__)
1379  this_arch = "ia64";
1380  #elif defined(__s390x__)
1381  this_arch = "s390x";
1382  #elif defined(__s390__)
1383  this_arch = "s390";
1384  #elif defined(__x86_64__)
1385  #ifdef __ILP32__
1386  this_arch = "x32"; // variant of x86_64 with 32-bit pointers
1387  #else
1388  this_arch = "x86_64";
1389  #endif
1390  #elif defined(__i386__)
1391  this_arch = "i386";
1392  #elif defined(_WIN64)
1393  this_arch = "x86_64";
1394  #elif defined(_WIN32)
1395  this_arch = "i386";
1396  #elif defined(__hppa__)
1397  this_arch = "hppa";
1398  #elif defined(__sh__)
1399  this_arch = "sh4";
1400  #else
1401  // something new and unknown!
1402  this_arch = "unknown";
1403  #endif
1404 
1405  return this_arch;
1406 }
1407 // clang-format on
1408 
1409 void configt::set_classpath(const std::string &cp)
1410 {
1411 // These are separated by colons on Unix, and semicolons on
1412 // Windows.
1413 #ifdef _WIN32
1414  const char cp_separator = ';';
1415 #else
1416  const char cp_separator = ':';
1417 #endif
1418 
1419  std::vector<std::string> class_path =
1420  split_string(cp, cp_separator);
1421  java.classpath.insert(
1422  java.classpath.end(), class_path.begin(), class_path.end());
1423 }
1424 
1426 {
1427  irep_idt this_os;
1428 
1429  #ifdef _WIN32
1430  this_os="windows";
1431  #elif __APPLE__
1432  this_os="macos";
1433  #elif __FreeBSD__
1434  this_os="freebsd";
1435  #elif __linux__
1436  this_os="linux";
1437  #elif __SVR4
1438  this_os="solaris";
1439  #else
1440  this_os="unknown";
1441  #endif
1442 
1443  return this_os;
1444 }
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:126
configt::bv_encodingt::object_bits
std::size_t object_bits
Definition: config.h:256
configt::ansi_ct::defines
std::list< std::string > defines
Definition: config.h:202
configt::ansi_ct::bool_width
std::size_t bool_width
Definition: config.h:113
configt::object_bits_info
std::string object_bits_info()
Definition: config.cpp:1314
configt::ansi_ct::set_c99
void set_c99()
Definition: config.h:133
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
configt::ansi_ct::NULL_is_zero
bool NULL_is_zero
Definition: config.h:168
configt::javat::main_class
irep_idt main_class
Definition: config.h:248
configt::ansi_ct::string_to_os
static ost string_to_os(const std::string &)
Definition: config.cpp:1165
configt::ansi_ct::ost
ost
Definition: config.h:159
configt::bv_encoding
struct configt::bv_encodingt bv_encoding
arith_tools.h
cmdlinet::isset
virtual bool isset(char option) const
Definition: cmdline.cpp:29
configt::ansi_ct::for_has_scope
bool for_has_scope
Definition: config.h:125
configt::cppt::cpp_standardt
cpp_standardt
Definition: config.h:228
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:121
configt::ansi_ct::endiannesst
endiannesst
Definition: config.h:156
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:205
configt::ansi_ct::malloc_failure_mode_assert_then_assume
@ malloc_failure_mode_assert_then_assume
Definition: config.h:218
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1296
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:160
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:261
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:54
configt::ansi_ct::rounding_mode
ieee_floatt::rounding_modet rounding_mode
Definition: config.h:136
configt::ansi_ct::alignment
std::size_t alignment
Definition: config.h:150
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:20
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:615
configt::javat::classpath
classpatht classpath
Definition: config.h:247
configt::ansi_ct::libt::LIB_NONE
@ LIB_NONE
configt::ansi_ct::flavourt::CLANG
@ CLANG
configt
Globally accessible architectural configuration.
Definition: config.h:106
parse_object_bits_encoding
configt::bv_encodingt parse_object_bits_encoding(const std::string &argument, const std::size_t pointer_width)
Parses the object_bits argument from the command line arguments.
Definition: config.cpp:774
configt::ansi_ct::char_width
std::size_t char_width
Definition: config.h:114
configt::cppt::set_cpp98
void set_cpp98()
Definition: config.h:231
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:141
split_string
void split_string(const std::string &s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)
Definition: string_utils.cpp:39
configt::ansi_ct::endiannesst::IS_LITTLE_ENDIAN
@ IS_LITTLE_ENDIAN
configt::bv_encodingt
Definition: config.h:254
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:1200
configt::ansi_ct::wchar_t_is_unsigned
bool wchar_t_is_unsigned
Definition: config.h:124
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
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
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:119
configt::ansi_ct::preprocessor
preprocessort preprocessor
Definition: config.h:200
configt::ansi_ct::malloc_failure_mode_return_null
@ malloc_failure_mode_return_null
Definition: config.h:217
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:223
configt::cppt::default_object_bits
static const std::size_t default_object_bits
Definition: config.h:236
configt::ansi_ct::string_abstraction
bool string_abstraction
Definition: config.h:211
configt::ansi_ct::set_arch_spec_alpha
void set_arch_spec_alpha()
Definition: config.cpp:323
pointer_expr.h
API to expression classes for Pointers.
configt::bv_encodingt::is_object_bits_default
bool is_object_bits_default
Definition: config.h:257
configt::cppt::set_cpp11
void set_cpp11()
Definition: config.h:233
configt::ansi_ct::memory_operand_size
std::size_t memory_operand_size
Definition: config.h:154
cmdlinet::get_value
std::string get_value(char option) const
Definition: cmdline.cpp:47
configt::ansi_ct::ost::OS_LINUX
@ OS_LINUX
simplify
bool simplify(exprt &expr, const namespacet &ns)
Definition: simplify_expr.cpp:2552
configt::ansi_ct::long_long_int_width
std::size_t long_long_int_width
Definition: config.h:116
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:22
configt::this_operating_system
static irep_idt this_operating_system()
Definition: config.cpp:1425
index_exprt::array
exprt & array()
Definition: std_expr.h:1258
configt::ansi_ct::arch
irep_idt arch
Definition: config.h:165
configt::ansi_ct::ost::OS_WIN
@ OS_WIN
irept::id
const irep_idt & id() const
Definition: irep.h:407
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:1229
configt::ansi_ct::os_to_string
static std::string os_to_string(ost)
Definition: config.cpp:1150
cprover_prefix.h
configt::javat::default_object_bits
static const std::size_t default_object_bits
Definition: config.h:250
configt::ansi_ct::include_files
std::list< std::string > include_files
Definition: config.h:206
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:674
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::ansi_ct::set_c11
void set_c11()
Definition: config.h:134
configt::this_architecture
static irep_idt this_architecture()
Definition: config.cpp:1325
configt::ansi_ct::libt::LIB_FULL
@ LIB_FULL
configt::ansi_ct::mode
flavourt mode
Definition: config.h:196
symbolt::value
exprt value
Initial value of symbol.
Definition: symbol.h:34
configt::ansi_ct::set_c89
void set_c89()
Definition: config.h:132
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:1177
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:797
configt::cppt::default_cpp_standard
static cpp_standardt default_cpp_standard()
Definition: config.cpp:689
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:644
configt::ansi_ct::long_double_width
std::size_t long_double_width
Definition: config.h:120
CPROVER_PREFIX
#define CPROVER_PREFIX
Definition: cprover_prefix.h:14
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:592
config.h
configt::ansi_ct::short_int_width
std::size_t short_int_width
Definition: config.h:115
configt::ansi_ct::char_is_unsigned
bool char_is_unsigned
Definition: config.h:124
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
to_address_of_expr
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:367
configt::ansi_ct::set_arch_spec_x32
void set_arch_spec_x32()
Definition: config.cpp:556
configt::ansi_ct::malloc_failure_mode
malloc_failure_modet malloc_failure_mode
Definition: config.h:221
configt::ansi_ct::pointer_width
std::size_t pointer_width
Definition: config.h:117
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:424
configt::ansi_ct::single_width
std::size_t single_width
Definition: config.h:118
configt::ansi_ct::lib
libt lib
Definition: config.h:209
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:1409
configt::ansi_ct::malloc_may_fail
bool malloc_may_fail
Definition: config.h:212
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:128
cmdlinet::get_values
const std::list< std::string > & get_values(const std::string &option) const
Definition: cmdline.cpp:108
configt::ansi_ct::gcc__float128_type
bool gcc__float128_type
Definition: config.h:127
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:1289
configt::ansi_ct::c_standardt
c_standardt
Definition: config.h:129
configt::set_arch
void set_arch(const irep_idt &)
Definition: config.cpp:701
configt::ansi_ct::int_width
std::size_t int_width
Definition: config.h:111
ieee_floatt::ROUND_TO_MINUS_INF
@ ROUND_TO_MINUS_INF
Definition: ieee_float.h:127
configt::ansi_ct::endianness
endiannesst endianness
Definition: config.h:157
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:112
configt::cppt::cpp_standard
enum configt::cppt::cpp_standardt cpp_standard
configt::cppt::set_cpp03
void set_cpp03()
Definition: config.h:232
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2700