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 <climits>
12 #include <cstdlib>
13 
14 #include "arith_tools.h"
15 #include "cmdline.h"
16 #include "cprover_prefix.h"
17 #include "exception_utils.h"
18 #include "namespace.h"
19 #include "pointer_expr.h"
20 #include "simplify_expr.h"
21 #include "string2int.h"
22 #include "string_utils.h"
23 #include "symbol_table.h"
24 
26 
28 {
29  set_LP32();
30 }
31 
33 {
34  set_ILP32();
35 }
36 
38 {
39  #ifdef _WIN32
40  set_LLP64();
41  #else
42  set_LP64();
43  #endif
44 }
45 
48 {
49  bool_width=1*8;
50  int_width=4*8;
51  long_int_width=8*8;
52  char_width=1*8;
53  short_int_width=2*8;
54  long_long_int_width=8*8;
55  pointer_width=8*8;
56  single_width=4*8;
57  double_width=8*8;
58  long_double_width=16*8;
59  char_is_unsigned=false;
60  wchar_t_is_unsigned=false;
61  wchar_t_width=4*8;
62  alignment=1;
63  memory_operand_size=int_width/8;
64 }
65 
67 // TODO: find the alignment restrictions (per type) of the different
68 // architectures (currently: sizeof=alignedof)
69 // TODO: implement the __attribute__((__aligned__(val)))
70 
72 {
73  bool_width=1*8;
74  int_width=8*8;
75  long_int_width=8*8;
76  char_width=1*8;
77  short_int_width=2*8;
78  long_long_int_width=8*8;
79  pointer_width=8*8;
80  single_width=4*8;
81  double_width=8*8;
82  long_double_width=8*8;
83  char_is_unsigned=false;
84  wchar_t_is_unsigned=false;
85  wchar_t_width=4*8;
86  alignment=1;
87  memory_operand_size=int_width/8;
88 }
89 
92 {
93  bool_width=1*8;
94  int_width=4*8;
95  long_int_width=4*8;
96  char_width=1*8;
97  short_int_width=2*8;
98  long_long_int_width=8*8;
99  pointer_width=8*8;
100  single_width=4*8;
101  double_width=8*8;
102  long_double_width=8*8;
103  char_is_unsigned=false;
104  wchar_t_is_unsigned=false;
105  wchar_t_width=4*8;
106  alignment=1;
107  memory_operand_size=int_width/8;
108 }
109 
112 {
113  bool_width=1*8;
114  int_width=4*8;
115  long_int_width=4*8;
116  char_width=1*8;
117  short_int_width=2*8;
118  long_long_int_width=8*8;
119  pointer_width=4*8;
120  single_width=4*8;
121  double_width=8*8;
122  long_double_width=12*8; // really 96 bits on GCC
123  char_is_unsigned=false;
124  wchar_t_is_unsigned=false;
125  wchar_t_width=4*8;
126  alignment=1;
127  memory_operand_size=int_width/8;
128 }
129 
132 {
133  bool_width=1*8;
134  int_width=2*8;
135  long_int_width=4*8;
136  char_width=1*8;
137  short_int_width=2*8;
138  long_long_int_width=8*8;
139  pointer_width=4*8;
140  single_width=4*8;
141  double_width=8*8;
142  long_double_width=8*8;
143  char_is_unsigned=false;
144  wchar_t_is_unsigned=false;
145  wchar_t_width=4*8;
146  alignment=1;
147  memory_operand_size=int_width/8;
148 }
149 
151 {
152  set_ILP32();
153  endianness=endiannesst::IS_LITTLE_ENDIAN;
154  char_is_unsigned=false;
155  NULL_is_zero=true;
156 
157  switch(mode)
158  {
159  case flavourt::GCC:
160  case flavourt::CLANG:
161  defines.push_back("i386");
162  defines.push_back("__i386");
163  defines.push_back("__i386__");
164  if(mode == flavourt::CLANG)
165  defines.push_back("__LITTLE_ENDIAN__");
166  break;
167 
168  case flavourt::VISUAL_STUDIO:
169  defines.push_back("_M_IX86");
170  break;
171 
172  case flavourt::CODEWARRIOR:
173  case flavourt::ARM:
174  case flavourt::ANSI:
175  break;
176 
177  case flavourt::NONE:
178  UNREACHABLE;
179  }
180 }
181 
183 {
184  set_LP64();
185  endianness=endiannesst::IS_LITTLE_ENDIAN;
186  long_double_width=16*8;
187  char_is_unsigned=false;
188  NULL_is_zero=true;
189 
190  switch(mode)
191  {
192  case flavourt::GCC:
193  case flavourt::CLANG:
194  defines.push_back("__LP64__");
195  defines.push_back("__x86_64");
196  defines.push_back("__x86_64__");
197  defines.push_back("_LP64");
198  defines.push_back("__amd64__");
199  defines.push_back("__amd64");
200 
201  if(os == ost::OS_MACOS)
202  defines.push_back("__LITTLE_ENDIAN__");
203  break;
204 
205  case flavourt::VISUAL_STUDIO:
206  defines.push_back("_M_X64");
207  defines.push_back("_M_AMD64");
208  break;
209 
210  case flavourt::CODEWARRIOR:
211  case flavourt::ARM:
212  case flavourt::ANSI:
213  break;
214 
215  case flavourt::NONE:
216  UNREACHABLE;
217  }
218 }
219 
221 {
222  if(subarch=="powerpc")
223  set_ILP32();
224  else // ppc64 or ppc64le
225  set_LP64();
226 
227  if(subarch=="ppc64le")
228  endianness=endiannesst::IS_LITTLE_ENDIAN;
229  else
230  endianness=endiannesst::IS_BIG_ENDIAN;
231 
232  long_double_width=16*8;
233  char_is_unsigned=true;
234  NULL_is_zero=true;
235 
236  switch(mode)
237  {
238  case flavourt::GCC:
239  case flavourt::CLANG:
240  defines.push_back("__powerpc");
241  defines.push_back("__powerpc__");
242  defines.push_back("__POWERPC__");
243  defines.push_back("__ppc__");
244 
245  if(os == ost::OS_MACOS)
246  defines.push_back("__BIG_ENDIAN__");
247 
248  if(subarch!="powerpc")
249  {
250  defines.push_back("__powerpc64");
251  defines.push_back("__powerpc64__");
252  defines.push_back("__PPC64__");
253  defines.push_back("__ppc64__");
254  if(subarch=="ppc64le")
255  {
256  defines.push_back("_CALL_ELF=2");
257  defines.push_back("__LITTLE_ENDIAN__");
258  }
259  else
260  {
261  defines.push_back("_CALL_ELF=1");
262  defines.push_back("__BIG_ENDIAN__");
263  }
264  }
265  break;
266 
267  case flavourt::VISUAL_STUDIO:
268  defines.push_back("_M_PPC");
269  break;
270 
271  case flavourt::CODEWARRIOR:
272  case flavourt::ARM:
273  case flavourt::ANSI:
274  break;
275 
276  case flavourt::NONE:
277  UNREACHABLE;
278  }
279 }
280 
282 {
283  if(subarch=="arm64")
284  {
285  set_LP64();
286  long_double_width=16*8;
287  }
288  else
289  {
290  set_ILP32();
291  long_double_width=8*8;
292  }
293 
294  endianness=endiannesst::IS_LITTLE_ENDIAN;
295  char_is_unsigned=true;
296  NULL_is_zero=true;
297 
298  switch(mode)
299  {
300  case flavourt::GCC:
301  case flavourt::CLANG:
302  if(subarch=="arm64")
303  defines.push_back("__aarch64__");
304  else
305  defines.push_back("__arm__");
306  if(subarch=="armhf")
307  defines.push_back("__ARM_PCS_VFP");
308  break;
309 
310  case flavourt::VISUAL_STUDIO:
311  defines.push_back("_M_ARM");
312  break;
313 
314  case flavourt::CODEWARRIOR:
315  case flavourt::ARM:
316  case flavourt::ANSI:
317  break;
318 
319  case flavourt::NONE:
320  UNREACHABLE;
321  }
322 }
323 
325 {
326  set_LP64();
327  endianness=endiannesst::IS_LITTLE_ENDIAN;
328  long_double_width=16*8;
329  char_is_unsigned=false;
330  NULL_is_zero=true;
331 
332  switch(mode)
333  {
334  case flavourt::GCC:
335  defines.push_back("__alpha__");
336  break;
337 
338  case flavourt::VISUAL_STUDIO:
339  defines.push_back("_M_ALPHA");
340  break;
341 
342  case flavourt::CLANG:
343  case flavourt::CODEWARRIOR:
344  case flavourt::ARM:
345  case flavourt::ANSI:
346  break;
347 
348  case flavourt::NONE:
349  UNREACHABLE;
350  }
351 }
352 
354 {
355  if(subarch=="mipsel" ||
356  subarch=="mips" ||
357  subarch=="mipsn32el" ||
358  subarch=="mipsn32")
359  {
360  set_ILP32();
361  long_double_width=8*8;
362  }
363  else
364  {
365  set_LP64();
366  long_double_width=16*8;
367  }
368 
369  if(subarch=="mipsel" ||
370  subarch=="mipsn32el" ||
371  subarch=="mips64el")
372  endianness=endiannesst::IS_LITTLE_ENDIAN;
373  else
374  endianness=endiannesst::IS_BIG_ENDIAN;
375 
376  char_is_unsigned=false;
377  NULL_is_zero=true;
378 
379  switch(mode)
380  {
381  case flavourt::GCC:
382  defines.push_back("__mips__");
383  defines.push_back("mips");
384  defines.push_back(
385  "_MIPS_SZPTR="+std::to_string(config.ansi_c.pointer_width));
386  break;
387 
388  case flavourt::VISUAL_STUDIO:
389  UNREACHABLE; // not supported by Visual Studio
390  break;
391 
392  case flavourt::CLANG:
393  case flavourt::CODEWARRIOR:
394  case flavourt::ARM:
395  case flavourt::ANSI:
396  break;
397 
398  case flavourt::NONE:
399  UNREACHABLE;
400  }
401 }
402 
404 {
405  set_LP64();
406  endianness = endiannesst::IS_LITTLE_ENDIAN;
407  long_double_width = 16 * 8;
408  char_is_unsigned = true;
409  NULL_is_zero = true;
410 
411  switch(mode)
412  {
413  case flavourt::GCC:
414  defines.push_back("__riscv");
415  break;
416 
417  case flavourt::VISUAL_STUDIO:
418  case flavourt::CLANG:
419  case flavourt::CODEWARRIOR:
420  case flavourt::ARM:
421  case flavourt::ANSI:
422  break;
423 
424  case flavourt::NONE:
425  UNREACHABLE;
426  }
427 }
428 
430 {
431  set_ILP32();
432  endianness=endiannesst::IS_BIG_ENDIAN;
433  long_double_width=16*8;
434  char_is_unsigned=true;
435  NULL_is_zero=true;
436 
437  switch(mode)
438  {
439  case flavourt::GCC:
440  defines.push_back("__s390__");
441  break;
442 
443  case flavourt::VISUAL_STUDIO:
444  UNREACHABLE; // not supported by Visual Studio
445  break;
446 
447  case flavourt::CLANG:
448  case flavourt::CODEWARRIOR:
449  case flavourt::ARM:
450  case flavourt::ANSI:
451  break;
452 
453  case flavourt::NONE:
454  UNREACHABLE;
455  }
456 }
457 
459 {
460  set_LP64();
461  endianness=endiannesst::IS_BIG_ENDIAN;
462  char_is_unsigned=true;
463  NULL_is_zero=true;
464 
465  switch(mode)
466  {
467  case flavourt::GCC:
468  defines.push_back("__s390x__");
469  break;
470 
471  case flavourt::VISUAL_STUDIO:
472  UNREACHABLE; // not supported by Visual Studio
473  break;
474 
475  case flavourt::CLANG:
476  case flavourt::CODEWARRIOR:
477  case flavourt::ARM:
478  case flavourt::ANSI:
479  break;
480 
481  case flavourt::NONE:
482  UNREACHABLE;
483  }
484 }
485 
487 {
488  if(subarch=="sparc64")
489  {
490  set_LP64();
491  long_double_width=16*8;
492  }
493  else
494  {
495  set_ILP32();
496  long_double_width=16*8;
497  }
498 
499  endianness=endiannesst::IS_BIG_ENDIAN;
500  char_is_unsigned=false;
501  NULL_is_zero=true;
502 
503  switch(mode)
504  {
505  case flavourt::GCC:
506  defines.push_back("__sparc__");
507  if(subarch=="sparc64")
508  defines.push_back("__arch64__");
509  break;
510 
511  case flavourt::VISUAL_STUDIO:
512  UNREACHABLE; // not supported by Visual Studio
513  break;
514 
515  case flavourt::CLANG:
516  case flavourt::CODEWARRIOR:
517  case flavourt::ARM:
518  case flavourt::ANSI:
519  break;
520 
521  case flavourt::NONE:
522  UNREACHABLE;
523  }
524 }
525 
527 {
528  set_LP64();
529  long_double_width=16*8;
530  endianness=endiannesst::IS_LITTLE_ENDIAN;
531  char_is_unsigned=false;
532  NULL_is_zero=true;
533 
534  switch(mode)
535  {
536  case flavourt::GCC:
537  defines.push_back("__ia64__");
538  defines.push_back("_IA64");
539  defines.push_back("__IA64__");
540  break;
541 
542  case flavourt::VISUAL_STUDIO:
543  defines.push_back("_M_IA64");
544  break;
545 
546  case flavourt::CLANG:
547  case flavourt::CODEWARRIOR:
548  case flavourt::ARM:
549  case flavourt::ANSI:
550  break;
551 
552  case flavourt::NONE:
553  UNREACHABLE;
554  }
555 }
556 
558 {
559  // This is a variant of x86_64 that has
560  // 32-bit long int and 32-bit pointers.
561  set_ILP32();
562  long_double_width=16*8; // different from i386
563  endianness=endiannesst::IS_LITTLE_ENDIAN;
564  char_is_unsigned=false;
565  NULL_is_zero=true;
566 
567  switch(mode)
568  {
569  case flavourt::GCC:
570  defines.push_back("__ILP32__");
571  defines.push_back("__x86_64");
572  defines.push_back("__x86_64__");
573  defines.push_back("__amd64__");
574  defines.push_back("__amd64");
575  break;
576 
577  case flavourt::VISUAL_STUDIO:
578  UNREACHABLE; // not supported by Visual Studio
579  break;
580 
581  case flavourt::CLANG:
582  case flavourt::CODEWARRIOR:
583  case flavourt::ARM:
584  case flavourt::ANSI:
585  break;
586 
587  case flavourt::NONE:
588  UNREACHABLE;
589  }
590 }
591 
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 
776  const std::string &argument,
777  const std::size_t pointer_width)
778 {
779  const auto throw_for_reason = [&](const std::string &reason) {
781  "Value of \"" + argument + "\" given for object-bits is " + reason +
782  ". object-bits must be positive and less than the pointer width (" +
783  std::to_string(pointer_width) + ") ",
784  "--object_bits");
785  };
786  const auto object_bits = string2optional<unsigned int>(argument);
787  if(!object_bits)
788  throw_for_reason("not a valid unsigned integer");
789  if(*object_bits == 0 || *object_bits >= pointer_width)
790  throw_for_reason("out of range");
791 
793  bv_encoding.object_bits = *object_bits;
795  return bv_encoding;
796 }
797 
798 bool configt::set(const cmdlinet &cmdline)
799 {
800  // defaults -- we match the architecture we have ourselves
801 
803 
805  ansi_c.for_has_scope=true; // C99 or later
810  ansi_c.arch="none";
812  // NOLINTNEXTLINE(readability/casting)
813  ansi_c.NULL_is_zero=reinterpret_cast<size_t>(nullptr)==0;
814 
815  // Default is ROUND_TO_EVEN, justified by C99:
816  // 1 At program startup the floating-point environment is initialized as
817  // prescribed by IEC 60559:
818  // - All floating-point exception status flags are cleared.
819  // - The rounding direction mode is rounding to nearest.
821 
822  if(cmdline.isset("function"))
823  main=cmdline.get_value("function");
824 
825  if(cmdline.isset('D'))
826  ansi_c.defines=cmdline.get_values('D');
827 
828  if(cmdline.isset('I'))
829  ansi_c.include_paths=cmdline.get_values('I');
830 
831  if(cmdline.isset("classpath"))
832  {
833  // Specifying -classpath or -cp overrides any setting of the
834  // CLASSPATH environment variable.
835  set_classpath(cmdline.get_value("classpath"));
836  }
837  else if(cmdline.isset("cp"))
838  {
839  // Specifying -classpath or -cp overrides any setting of the
840  // CLASSPATH environment variable.
841  set_classpath(cmdline.get_value("cp"));
842  }
843  else
844  {
845  // environment variable set?
846  const char *CLASSPATH=getenv("CLASSPATH");
847  if(CLASSPATH!=nullptr)
848  set_classpath(CLASSPATH);
849  else
850  set_classpath("."); // default
851  }
852 
853  if(cmdline.isset("main-class"))
854  java.main_class=cmdline.get_value("main-class");
855 
856  if(cmdline.isset("include"))
857  ansi_c.include_files=cmdline.get_values("include");
858 
859  // the default architecture is the one we run on
860  irep_idt this_arch=this_architecture();
861  irep_idt arch=this_arch;
862 
863  // let's pick an OS now
864  // the default is the one we run on
866  irep_idt os=this_os;
867 
868  if(cmdline.isset("i386-linux"))
869  {
870  os="linux";
871  arch="i386";
872  }
873  else if(cmdline.isset("i386-win32") ||
874  cmdline.isset("win32"))
875  {
876  os="windows";
877  arch="i386";
878  }
879  else if(cmdline.isset("winx64"))
880  {
881  os="windows";
882  arch="x86_64";
883  }
884  else if(cmdline.isset("i386-macos"))
885  {
886  os="macos";
887  arch="i386";
888  }
889  else if(cmdline.isset("ppc-macos"))
890  {
891  arch="powerpc";
892  os="macos";
893  }
894 
895  if(cmdline.isset("arch"))
896  {
897  arch=cmdline.get_value("arch");
898  }
899 
900  if(cmdline.isset("os"))
901  {
902  os=cmdline.get_value("os");
903  }
904 
905  if(os=="windows")
906  {
907  // Cygwin uses GCC throughout, use i386-linux
908  // MinGW needs --win32 --gcc
911 
912  if(cmdline.isset("gcc"))
913  {
914  // There are gcc versions that target Windows (MinGW for example),
915  // and we support that.
918 
919  // enable Cygwin
920  #ifdef _WIN32
921  ansi_c.defines.push_back("__CYGWIN__");
922  #endif
923 
924  // MinGW has extra defines
925  ansi_c.defines.push_back("__int64=long long");
926  }
927  else
928  {
929  // On Windows, our default is Visual Studio.
930  // On FreeBSD, it's clang.
931  // On anything else, it's GCC as the preprocessor,
932  // but we recognize the Visual Studio language,
933  // which is somewhat inconsistent.
934  #ifdef _WIN32
937  #elif __FreeBSD__
940  #else
943  #endif
944 
946  }
947  }
948  else if(os=="macos")
949  {
954  }
955  else if(os=="linux" || os=="solaris")
956  {
961  }
962  else if(os=="freebsd")
963  {
968  }
969  else
970  {
971  // give up, but use reasonable defaults
976  }
977 
979  ansi_c.gcc__float128_type = true;
980 
981  set_arch(arch);
982 
983  if(os=="windows")
984  {
985  // note that sizeof(void *)==8, but sizeof(long)==4!
986  if(arch=="x86_64")
987  ansi_c.set_LLP64();
988 
989  // On Windows, wchar_t is unsigned 16 bit, regardless
990  // of the compiler used.
991  ansi_c.wchar_t_width=2*8;
993 
994  // long double is the same as double in Visual Studio,
995  // but it's 16 bytes with GCC with the 64-bit target.
996  if(arch=="x64_64" && cmdline.isset("gcc"))
998  else
1000  }
1001  else if(os == "macos" && arch == "arm64")
1002  {
1003  // https://developer.apple.com/documentation/xcode/
1004  // writing_arm64_code_for_apple_platforms#//apple_ref/doc/uid/TP40013702-SW1
1005  ansi_c.char_is_unsigned = false;
1006  ansi_c.long_double_width = 8 * 8;
1007  }
1008 
1009  // Let's check some of the type widths in case we run
1010  // the same architecture and OS that we are verifying for.
1011  if(arch==this_arch && os==this_os)
1012  {
1013  INVARIANT(
1014  ansi_c.int_width == sizeof(int) * CHAR_BIT,
1015  "int width shall be equal to the system int width");
1016  INVARIANT(
1017  ansi_c.long_int_width == sizeof(long) * CHAR_BIT,
1018  "long int width shall be equal to the system long int width");
1019  INVARIANT(
1020  ansi_c.bool_width == sizeof(bool) * CHAR_BIT,
1021  "bool width shall be equal to the system bool width");
1022  INVARIANT(
1023  ansi_c.char_width == sizeof(char) * CHAR_BIT,
1024  "char width shall be equal to the system char width");
1025  INVARIANT(
1026  ansi_c.short_int_width == sizeof(short) * CHAR_BIT,
1027  "short int width shall be equal to the system short int width");
1028  INVARIANT(
1029  ansi_c.long_long_int_width == sizeof(long long) * CHAR_BIT,
1030  "long long int width shall be equal to the system long long int width");
1031  INVARIANT(
1032  ansi_c.pointer_width == sizeof(void *) * CHAR_BIT,
1033  "pointer width shall be equal to the system pointer width");
1034  INVARIANT(
1035  ansi_c.single_width == sizeof(float) * CHAR_BIT,
1036  "float width shall be equal to the system float width");
1037  INVARIANT(
1038  ansi_c.double_width == sizeof(double) * CHAR_BIT,
1039  "double width shall be equal to the system double width");
1040  INVARIANT(
1042  (static_cast<char>((1 << CHAR_BIT) - 1) == (1 << CHAR_BIT) - 1),
1043  "char_is_unsigned flag shall indicate system char unsignedness");
1044 
1045 #ifndef _WIN32
1046  // On Windows, long double width varies by compiler
1047  INVARIANT(
1048  ansi_c.long_double_width == sizeof(long double) * CHAR_BIT,
1049  "long double width shall be equal to the system long double width");
1050 #endif
1051  }
1052 
1053  // the following allows overriding the defaults
1054 
1055  if(cmdline.isset("16"))
1056  ansi_c.set_16();
1057 
1058  if(cmdline.isset("32"))
1059  ansi_c.set_32();
1060 
1061  if(cmdline.isset("64"))
1062  ansi_c.set_64();
1063 
1064  if(cmdline.isset("LP64"))
1065  ansi_c.set_LP64(); // int=32, long=64, pointer=64
1066 
1067  if(cmdline.isset("ILP64"))
1068  ansi_c.set_ILP64(); // int=64, long=64, pointer=64
1069 
1070  if(cmdline.isset("LLP64"))
1071  ansi_c.set_LLP64(); // int=32, long=32, pointer=64
1072 
1073  if(cmdline.isset("ILP32"))
1074  ansi_c.set_ILP32(); // int=32, long=32, pointer=32
1075 
1076  if(cmdline.isset("LP32"))
1077  ansi_c.set_LP32(); // int=16, long=32, pointer=32
1078 
1079  if(cmdline.isset("string-abstraction"))
1081  else
1082  ansi_c.string_abstraction=false;
1083 
1084  if(cmdline.isset("no-library"))
1086 
1087  if(cmdline.isset("little-endian"))
1089 
1090  if(cmdline.isset("big-endian"))
1092 
1093  if(cmdline.isset("little-endian") &&
1094  cmdline.isset("big-endian"))
1095  return true;
1096 
1097  if(cmdline.isset("unsigned-char"))
1098  ansi_c.char_is_unsigned=true;
1099 
1100  if(cmdline.isset("round-to-even") ||
1101  cmdline.isset("round-to-nearest"))
1103 
1104  if(cmdline.isset("round-to-plus-inf"))
1106 
1107  if(cmdline.isset("round-to-minus-inf"))
1109 
1110  if(cmdline.isset("round-to-zero"))
1112 
1113  if(cmdline.isset("object-bits"))
1114  {
1116  cmdline.get_value("object-bits"), ansi_c.pointer_width);
1117  }
1118 
1119  if(cmdline.isset("malloc-fail-assert") && cmdline.isset("malloc-fail-null"))
1120  {
1122  "at most one malloc failure mode is acceptable", "--malloc-fail-null"};
1123  }
1124  if(cmdline.isset("malloc-fail-null"))
1126  if(cmdline.isset("malloc-fail-assert"))
1128 
1129  ansi_c.malloc_may_fail = cmdline.isset("malloc-may-fail");
1130 
1131  if(cmdline.isset("c89"))
1132  ansi_c.set_c89();
1133 
1134  if(cmdline.isset("c99"))
1135  ansi_c.set_c99();
1136 
1137  if(cmdline.isset("c11"))
1138  ansi_c.set_c11();
1139 
1140  if(cmdline.isset("cpp98"))
1141  cpp.set_cpp98();
1142 
1143  if(cmdline.isset("cpp03"))
1144  cpp.set_cpp03();
1145 
1146  if(cmdline.isset("cpp11"))
1147  cpp.set_cpp11();
1148 
1149  return false;
1150 }
1151 
1153 {
1154  // clang-format off
1155  switch(os)
1156  {
1157  case ost::OS_LINUX: return "linux";
1158  case ost::OS_MACOS: return "macos";
1159  case ost::OS_WIN: return "win";
1160  case ost::NO_OS: return "none";
1161  }
1162  // clang-format on
1163 
1164  UNREACHABLE;
1165 }
1166 
1168 {
1169  if(os=="linux")
1170  return ost::OS_LINUX;
1171  else if(os=="macos")
1172  return ost::OS_MACOS;
1173  else if(os=="win")
1174  return ost::OS_WIN;
1175  else
1176  return ost::NO_OS;
1177 }
1178 
1180  const namespacet &ns,
1181  const std::string &what)
1182 {
1183  const irep_idt id=CPROVER_PREFIX "architecture_"+what;
1184  const symbolt *symbol;
1185 
1186  const bool not_found = ns.lookup(id, symbol);
1187  INVARIANT(!not_found, id2string(id) + " must be in namespace");
1188 
1189  const exprt &tmp=symbol->value;
1190 
1191  INVARIANT(
1192  tmp.id() == ID_address_of &&
1193  to_address_of_expr(tmp).object().id() == ID_index &&
1194  to_index_expr(to_address_of_expr(tmp).object()).array().id() ==
1195  ID_string_constant,
1196  "symbol table configuration entry '" + id2string(id) +
1197  "' must be a string constant");
1198 
1199  return to_index_expr(to_address_of_expr(tmp).object()).array().get(ID_value);
1200 }
1201 
1202 static unsigned unsigned_from_ns(
1203  const namespacet &ns,
1204  const std::string &what)
1205 {
1206  const irep_idt id=CPROVER_PREFIX "architecture_"+what;
1207  const symbolt *symbol;
1208 
1209  const bool not_found = ns.lookup(id, symbol);
1210  INVARIANT(!not_found, id2string(id) + " must be in namespace");
1211 
1212  exprt tmp=symbol->value;
1213  simplify(tmp, ns);
1214 
1215  INVARIANT(
1216  tmp.id() == ID_constant,
1217  "symbol table configuration entry '" + id2string(id) +
1218  "' must be a constant");
1219 
1220  mp_integer int_value;
1221 
1222  const bool error = to_integer(to_constant_expr(tmp), int_value);
1223  INVARIANT(
1224  !error,
1225  "symbol table configuration entry '" + id2string(id) +
1226  "' must be convertible to mp_integer");
1227 
1228  return numeric_cast_v<unsigned>(int_value);
1229 }
1230 
1232  const symbol_tablet &symbol_table)
1233 {
1234  // maybe not compiled from C/C++
1235  if(symbol_table.symbols.find(CPROVER_PREFIX "architecture_" "int_width")==
1236  symbol_table.symbols.end())
1237  return;
1238 
1239  namespacet ns(symbol_table);
1240 
1241  // clear defines
1242  ansi_c.defines.clear();
1243 
1244  // first set architecture to get some defaults
1245  if(symbol_table.symbols.find(CPROVER_PREFIX "architecture_" "arch")==
1246  symbol_table.symbols.end())
1248  else
1249  set_arch(string_from_ns(ns, "arch"));
1250 
1251  ansi_c.int_width=unsigned_from_ns(ns, "int_width");
1252  ansi_c.long_int_width=unsigned_from_ns(ns, "long_int_width");
1253  ansi_c.bool_width=1*8;
1254  ansi_c.char_width=unsigned_from_ns(ns, "char_width");
1255  ansi_c.short_int_width=unsigned_from_ns(ns, "short_int_width");
1256  ansi_c.long_long_int_width=unsigned_from_ns(ns, "long_long_int_width");
1257  ansi_c.pointer_width=unsigned_from_ns(ns, "pointer_width");
1258  ansi_c.single_width=unsigned_from_ns(ns, "single_width");
1259  ansi_c.double_width=unsigned_from_ns(ns, "double_width");
1260  ansi_c.long_double_width=unsigned_from_ns(ns, "long_double_width");
1261  ansi_c.wchar_t_width=unsigned_from_ns(ns, "wchar_t_width");
1262 
1263  ansi_c.char_is_unsigned=unsigned_from_ns(ns, "char_is_unsigned")!=0;
1264  ansi_c.wchar_t_is_unsigned=unsigned_from_ns(ns, "wchar_t_is_unsigned")!=0;
1265  // for_has_scope, single_precision_constant, rounding_mode,
1266  // ts_18661_3_Floatn_types are not architectural features,
1267  // and thus not stored in namespace
1268 
1269  ansi_c.alignment=unsigned_from_ns(ns, "alignment");
1270 
1271  ansi_c.memory_operand_size=unsigned_from_ns(ns, "memory_operand_size");
1272 
1274 
1275  if(symbol_table.symbols.find(CPROVER_PREFIX "architecture_" "os")==
1276  symbol_table.symbols.end())
1278  else
1280 
1281  ansi_c.NULL_is_zero = unsigned_from_ns(ns, "NULL_is_zero") != 0;
1282 
1283  // mode, preprocessor (and all preprocessor command line options),
1284  // lib, string_abstraction not stored in namespace
1285 
1286  set_object_bits_from_symbol_table(symbol_table);
1287 }
1288 
1292  const symbol_tablet &symbol_table)
1293 {
1294  // has been overridden by command line option,
1295  // thus do not apply language defaults
1297  return;
1298 
1299  // set object_bits according to entry point language
1300  if(const auto maybe_symbol=symbol_table.lookup(CPROVER_PREFIX "_start"))
1301  {
1302  const symbolt &entry_point_symbol=*maybe_symbol;
1303 
1304  if(entry_point_symbol.mode==ID_java)
1306  else if(entry_point_symbol.mode==ID_C)
1308  else if(entry_point_symbol.mode==ID_cpp)
1312  "object_bits should fit into pointer width");
1313  }
1314 }
1315 
1317 {
1318  return "Running with "+std::to_string(bv_encoding.object_bits)+
1319  " object bits, "+
1321  " offset bits ("+
1322  (bv_encoding.is_object_bits_default ? "default" : "user-specified")+
1323  ")";
1324 }
1325 
1326 // clang-format off
1328 {
1329  irep_idt this_arch;
1330 
1331  // following http://wiki.debian.org/ArchitectureSpecificsMemo
1332 
1333  #ifdef __alpha__
1334  this_arch = "alpha";
1335  #elif defined(__armel__)
1336  this_arch = "armel";
1337  #elif defined(__aarch64__)
1338  this_arch = "arm64";
1339  #elif defined(__arm__)
1340  #ifdef __ARM_PCS_VFP
1341  this_arch = "armhf"; // variant of arm with hard float
1342  #else
1343  this_arch = "arm";
1344  #endif
1345  #elif defined(__mipsel__)
1346  #if _MIPS_SIM==_ABIO32
1347  this_arch = "mipsel";
1348  #elif _MIPS_SIM==_ABIN32
1349  this_arch = "mipsn32el";
1350  #else
1351  this_arch = "mips64el";
1352  #endif
1353  #elif defined(__mips__)
1354  #if _MIPS_SIM==_ABIO32
1355  this_arch = "mips";
1356  #elif _MIPS_SIM==_ABIN32
1357  this_arch = "mipsn32";
1358  #else
1359  this_arch = "mips64";
1360  #endif
1361  #elif defined(__powerpc__)
1362  #if defined(__ppc64__) || defined(__PPC64__) || \
1363  defined(__powerpc64__) || defined(__POWERPC64__)
1364  #ifdef __LITTLE_ENDIAN__
1365  this_arch = "ppc64le";
1366  #else
1367  this_arch = "ppc64";
1368  #endif
1369  #else
1370  this_arch = "powerpc";
1371  #endif
1372  #elif defined(__riscv)
1373  this_arch = "riscv64";
1374  #elif defined(__sparc__)
1375  #ifdef __arch64__
1376  this_arch = "sparc64";
1377  #else
1378  this_arch = "sparc";
1379  #endif
1380  #elif defined(__ia64__)
1381  this_arch = "ia64";
1382  #elif defined(__s390x__)
1383  this_arch = "s390x";
1384  #elif defined(__s390__)
1385  this_arch = "s390";
1386  #elif defined(__x86_64__)
1387  #ifdef __ILP32__
1388  this_arch = "x32"; // variant of x86_64 with 32-bit pointers
1389  #else
1390  this_arch = "x86_64";
1391  #endif
1392  #elif defined(__i386__)
1393  this_arch = "i386";
1394  #elif defined(_WIN64)
1395  this_arch = "x86_64";
1396  #elif defined(_WIN32)
1397  this_arch = "i386";
1398  #elif defined(__hppa__)
1399  this_arch = "hppa";
1400  #elif defined(__sh__)
1401  this_arch = "sh4";
1402  #else
1403  // something new and unknown!
1404  this_arch = "unknown";
1405  #endif
1406 
1407  return this_arch;
1408 }
1409 // clang-format on
1410 
1411 void configt::set_classpath(const std::string &cp)
1412 {
1413 // These are separated by colons on Unix, and semicolons on
1414 // Windows.
1415 #ifdef _WIN32
1416  const char cp_separator = ';';
1417 #else
1418  const char cp_separator = ':';
1419 #endif
1420 
1421  std::vector<std::string> class_path =
1422  split_string(cp, cp_separator);
1423  java.classpath.insert(
1424  java.classpath.end(), class_path.begin(), class_path.end());
1425 }
1426 
1428 {
1429  irep_idt this_os;
1430 
1431  #ifdef _WIN32
1432  this_os="windows";
1433  #elif __APPLE__
1434  this_os="macos";
1435  #elif __FreeBSD__
1436  this_os="freebsd";
1437  #elif __linux__
1438  this_os="linux";
1439  #elif __SVR4
1440  this_os="solaris";
1441  #else
1442  this_os="unknown";
1443  #endif
1444 
1445  return this_os;
1446 }
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
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:125
configt::bv_encodingt::object_bits
std::size_t object_bits
Definition: config.h:255
configt::ansi_ct::defines
std::list< std::string > defines
Definition: config.h:201
configt::ansi_ct::bool_width
std::size_t bool_width
Definition: config.h:112
configt::object_bits_info
std::string object_bits_info()
Definition: config.cpp:1316
configt::ansi_ct::set_c99
void set_c99()
Definition: config.h:132
symbol_tablet
The symbol table.
Definition: symbol_table.h:14
configt::ansi_ct::NULL_is_zero
bool NULL_is_zero
Definition: config.h:167
configt::javat::main_class
irep_idt main_class
Definition: config.h:247
mp_integer
BigInt mp_integer
Definition: smt_terms.h:12
configt::ansi_ct::string_to_os
static ost string_to_os(const std::string &)
Definition: config.cpp:1167
configt::ansi_ct::ost
ost
Definition: config.h:158
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:124
configt::cppt::cpp_standardt
cpp_standardt
Definition: config.h:227
configt::ansi_ct::set_arch_spec_s390x
void set_arch_spec_s390x()
Definition: config.cpp:458
configt::ansi_ct::wchar_t_width
std::size_t wchar_t_width
Definition: config.h:120
configt::ansi_ct::endiannesst
endiannesst
Definition: config.h:155
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:204
configt::ansi_ct::malloc_failure_mode_assert_then_assume
@ malloc_failure_mode_assert_then_assume
Definition: config.h:217
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1382
configt::ansi_ct::set_arch_spec_mips
void set_arch_spec_mips(const irep_idt &subarch)
Definition: config.cpp:353
configt::ansi_ct::os
ost os
Definition: config.h:159
configt::ansi_ct::flavourt::VISUAL_STUDIO
@ VISUAL_STUDIO
configt::ansi_ct::set_32
void set_32()
Definition: config.cpp:32
configt::ansi_ct::set_64
void set_64()
Definition: config.cpp:37
configt::main
optionalt< std::string > main
Definition: config.h:260
configt::ansi_ct::set_arch_spec_i386
void set_arch_spec_i386()
Definition: config.cpp:150
configt::ansi_ct::set_16
void set_16()
Definition: config.cpp:27
exprt
Base class for all expressions.
Definition: expr.h:54
configt::ansi_ct::rounding_mode
ieee_floatt::rounding_modet rounding_mode
Definition: config.h:135
configt::ansi_ct::alignment
std::size_t alignment
Definition: config.h:149
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:131
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:57
configt::ansi_ct::set_arch_spec_power
void set_arch_spec_power(const irep_idt &subarch)
Definition: config.cpp:220
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:246
configt::ansi_ct::libt::LIB_NONE
@ LIB_NONE
configt::ansi_ct::flavourt::CLANG
@ CLANG
configt
Globally accessible architectural configuration.
Definition: config.h:105
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:775
configt::ansi_ct::char_width
std::size_t char_width
Definition: config.h:113
configt::cppt::set_cpp98
void set_cpp98()
Definition: config.h:230
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
configt::ansi_ct::endiannesst::NO_ENDIANNESS
@ NO_ENDIANNESS
configt::ansi_ct::set_arch_spec_ia64
void set_arch_spec_ia64()
Definition: config.cpp:526
string2int.h
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
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:253
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:281
unsigned_from_ns
static unsigned unsigned_from_ns(const namespacet &ns, const std::string &what)
Definition: config.cpp:1202
configt::ansi_ct::wchar_t_is_unsigned
bool wchar_t_is_unsigned
Definition: config.h:123
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:510
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:429
configt::ansi_ct::double_width
std::size_t double_width
Definition: config.h:118
configt::ansi_ct::preprocessor
preprocessort preprocessor
Definition: config.h:199
configt::ansi_ct::malloc_failure_mode_return_null
@ malloc_failure_mode_return_null
Definition: config.h:216
configt::ansi_ct::set_arch_spec_riscv64
void set_arch_spec_riscv64()
Definition: config.cpp:403
configt::ansi_ct::default_object_bits
static const std::size_t default_object_bits
Definition: config.h:222
configt::cppt::default_object_bits
static const std::size_t default_object_bits
Definition: config.h:235
configt::ansi_ct::string_abstraction
bool string_abstraction
Definition: config.h:210
configt::ansi_ct::set_arch_spec_alpha
void set_arch_spec_alpha()
Definition: config.cpp:324
pointer_expr.h
API to expression classes for Pointers.
configt::bv_encodingt::is_object_bits_default
bool is_object_bits_default
Definition: config.h:256
configt::cppt::set_cpp11
void set_cpp11()
Definition: config.h:232
configt::ansi_ct::memory_operand_size
std::size_t memory_operand_size
Definition: config.h:153
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:2654
configt::ansi_ct::long_long_int_width
std::size_t long_long_int_width
Definition: config.h:115
configt::ansi_ct::set_ILP64
void set_ILP64()
int=64, long=64, pointer=64
Definition: config.cpp:71
alignment
mp_integer alignment(const typet &type, const namespacet &ns)
Definition: padding.cpp:23
configt::this_operating_system
static irep_idt this_operating_system()
Definition: config.cpp:1427
index_exprt::array
exprt & array()
Definition: std_expr.h:1344
configt::ansi_ct::arch
irep_idt arch
Definition: config.h:164
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:91
configt::set_from_symbol_table
void set_from_symbol_table(const symbol_tablet &)
Definition: config.cpp:1231
configt::ansi_ct::os_to_string
static std::string os_to_string(ost)
Definition: config.cpp:1152
cprover_prefix.h
configt::javat::default_object_bits
static const std::size_t default_object_bits
Definition: config.h:249
configt::ansi_ct::include_files
std::list< std::string > include_files
Definition: config.h:205
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:111
config
configt config
Definition: config.cpp:25
simplify_expr.h
configt::ansi_ct::set_c11
void set_c11()
Definition: config.h:133
configt::this_architecture
static irep_idt this_architecture()
Definition: config.cpp:1327
configt::ansi_ct::libt::LIB_FULL
@ LIB_FULL
configt::ansi_ct::mode
flavourt mode
Definition: config.h:195
symbolt::value
exprt value
Initial value of symbol.
Definition: symbol.h:34
configt::ansi_ct::set_c89
void set_c89()
Definition: config.h:131
configt::ansi_ct::preprocessort::VISUAL_STUDIO
@ VISUAL_STUDIO
ieee_floatt::ROUND_TO_PLUS_INF
@ ROUND_TO_PLUS_INF
Definition: ieee_float.h:126
configt::ansi_ct::endiannesst::IS_BIG_ENDIAN
@ IS_BIG_ENDIAN
ieee_floatt::ROUND_TO_EVEN
@ ROUND_TO_EVEN
Definition: ieee_float.h:125
string_from_ns
static irep_idt string_from_ns(const namespacet &ns, const std::string &what)
Definition: config.cpp:1179
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:45
cmdline.h
symbolt
Symbol table entry.
Definition: symbol.h:28
configt::set
bool set(const cmdlinet &cmdline)
Definition: config.cpp:798
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:486
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:47
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:119
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:593
config.h
configt::ansi_ct::short_int_width
std::size_t short_int_width
Definition: config.h:114
configt::ansi_ct::char_is_unsigned
bool char_is_unsigned
Definition: config.h:123
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:182
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:378
configt::ansi_ct::set_arch_spec_x32
void set_arch_spec_x32()
Definition: config.cpp:557
configt::ansi_ct::malloc_failure_mode
malloc_failure_modet malloc_failure_mode
Definition: config.h:220
configt::ansi_ct::pointer_width
std::size_t pointer_width
Definition: config.h:116
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423
configt::ansi_ct::single_width
std::size_t single_width
Definition: config.h:117
configt::ansi_ct::lib
libt lib
Definition: config.h:208
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:1411
configt::ansi_ct::malloc_may_fail
bool malloc_may_fail
Definition: config.h:211
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:127
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:126
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:1291
configt::ansi_ct::c_standardt
c_standardt
Definition: config.h:128
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:110
ieee_floatt::ROUND_TO_MINUS_INF
@ ROUND_TO_MINUS_INF
Definition: ieee_float.h:125
configt::ansi_ct::endianness
endiannesst endianness
Definition: config.h:156
ieee_floatt::ROUND_TO_ZERO
@ ROUND_TO_ZERO
Definition: ieee_float.h:126
configt::ansi_ct::long_int_width
std::size_t long_int_width
Definition: config.h:111
configt::cppt::cpp_standard
enum configt::cppt::cpp_standardt cpp_standard
configt::cppt::set_cpp03
void set_cpp03()
Definition: config.h:231
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2786