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