CBMC
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 "arith_tools.h"
12 #include "cmdline.h"
13 #include "cprover_prefix.h"
14 #include "exception_utils.h"
15 #include "namespace.h"
16 #include "pointer_expr.h"
17 #include "simplify_expr.h"
18 #include "string2int.h"
19 #include "string_utils.h"
20 #include "symbol_table_base.h"
21 
22 #include <climits>
23 #include <cstdlib>
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
807  ansi_c.float16_type = false;
808  ansi_c.bf16_type = false;
812  ansi_c.arch="none";
814  // NOLINTNEXTLINE(readability/casting)
815  ansi_c.NULL_is_zero=reinterpret_cast<size_t>(nullptr)==0;
816 
817  // Default is ROUND_TO_EVEN, justified by C99:
818  // 1 At program startup the floating-point environment is initialized as
819  // prescribed by IEC 60559:
820  // - All floating-point exception status flags are cleared.
821  // - The rounding direction mode is rounding to nearest.
823 
824  if(cmdline.isset("function"))
825  main=cmdline.get_value("function");
826 
827  if(cmdline.isset('D'))
828  ansi_c.defines=cmdline.get_values('D');
829 
830  if(cmdline.isset('I'))
831  ansi_c.include_paths=cmdline.get_values('I');
832 
833  if(cmdline.isset("classpath"))
834  {
835  // Specifying -classpath or -cp overrides any setting of the
836  // CLASSPATH environment variable.
837  set_classpath(cmdline.get_value("classpath"));
838  }
839  else if(cmdline.isset("cp"))
840  {
841  // Specifying -classpath or -cp overrides any setting of the
842  // CLASSPATH environment variable.
843  set_classpath(cmdline.get_value("cp"));
844  }
845  else
846  {
847  // environment variable set?
848  const char *CLASSPATH=getenv("CLASSPATH");
849  if(CLASSPATH!=nullptr)
850  set_classpath(CLASSPATH);
851  else
852  set_classpath("."); // default
853  }
854 
855  if(cmdline.isset("main-class"))
856  java.main_class=cmdline.get_value("main-class");
857 
858  if(cmdline.isset("include"))
859  ansi_c.include_files=cmdline.get_values("include");
860 
861  // the default architecture is the one we run on
862  irep_idt this_arch=this_architecture();
863  irep_idt arch=this_arch;
864 
865  // let's pick an OS now
866  // the default is the one we run on
868  irep_idt os=this_os;
869 
870  if(cmdline.isset("i386-linux"))
871  {
872  os="linux";
873  arch="i386";
874  }
875  else if(cmdline.isset("i386-win32") ||
876  cmdline.isset("win32"))
877  {
878  os="windows";
879  arch="i386";
880  }
881  else if(cmdline.isset("winx64"))
882  {
883  os="windows";
884  arch="x86_64";
885  }
886  else if(cmdline.isset("i386-macos"))
887  {
888  os="macos";
889  arch="i386";
890  }
891  else if(cmdline.isset("ppc-macos"))
892  {
893  arch="powerpc";
894  os="macos";
895  }
896 
897  if(cmdline.isset("arch"))
898  {
899  arch=cmdline.get_value("arch");
900  }
901 
902  if(cmdline.isset("os"))
903  {
904  os=cmdline.get_value("os");
905  }
906 
907  if(os=="windows")
908  {
909  // Cygwin uses GCC throughout, use i386-linux
910  // MinGW needs --win32 --gcc
913 
914  if(cmdline.isset("gcc"))
915  {
916  // There are gcc versions that target Windows (MinGW for example),
917  // and we support that.
920 
921  // enable Cygwin
922  #ifdef _WIN32
923  ansi_c.defines.push_back("__CYGWIN__");
924  #endif
925 
926  // MinGW has extra defines
927  ansi_c.defines.push_back("__int64=long long");
928  }
929  else
930  {
931  // On Windows, our default is Visual Studio.
932  // On FreeBSD, it's clang.
933  // On anything else, it's GCC as the preprocessor,
934  // but we recognize the Visual Studio language,
935  // which is somewhat inconsistent.
936  #ifdef _WIN32
939 #elif defined(__FreeBSD__) || defined(__OpenBSD__)
942 #else
945 #endif
946 
948  }
949  }
950  else if(os=="macos")
951  {
956  }
957  else if(os == "linux" || os == "solaris" || os == "netbsd")
958  {
963  }
964  else if(os == "freebsd" || os == "openbsd")
965  {
970  }
971  else
972  {
973  // give up, but use reasonable defaults
978  }
979 
981  ansi_c.gcc__float128_type = true;
982 
983  set_arch(arch);
984 
985  if(os=="windows")
986  {
987  // note that sizeof(void *)==8, but sizeof(long)==4!
988  if(arch=="x86_64")
989  ansi_c.set_LLP64();
990 
991  // On Windows, wchar_t is unsigned 16 bit, regardless
992  // of the compiler used.
993  ansi_c.wchar_t_width=2*8;
995 
996  // long double is the same as double in Visual Studio,
997  // but it's 16 bytes with GCC with the 64-bit target.
998  if(arch == "x86_64" && cmdline.isset("gcc"))
1000  else
1002  }
1003  else if(os == "macos" && arch == "arm64")
1004  {
1005  // https://developer.apple.com/documentation/xcode/
1006  // writing_arm64_code_for_apple_platforms#//apple_ref/doc/uid/TP40013702-SW1
1007  ansi_c.char_is_unsigned = false;
1008  ansi_c.long_double_width = 8 * 8;
1009  }
1010 
1011  // Let's check some of the type widths in case we run
1012  // the same architecture and OS that we are verifying for.
1013  if(arch==this_arch && os==this_os)
1014  {
1015  INVARIANT(
1016  ansi_c.int_width == sizeof(int) * CHAR_BIT,
1017  "int width shall be equal to the system int width");
1018  INVARIANT(
1019  ansi_c.long_int_width == sizeof(long) * CHAR_BIT,
1020  "long int width shall be equal to the system long int width");
1021  INVARIANT(
1022  ansi_c.bool_width == sizeof(bool) * CHAR_BIT,
1023  "bool width shall be equal to the system bool width");
1024  INVARIANT(
1025  ansi_c.char_width == sizeof(char) * CHAR_BIT,
1026  "char width shall be equal to the system char width");
1027  INVARIANT(
1028  ansi_c.short_int_width == sizeof(short) * CHAR_BIT,
1029  "short int width shall be equal to the system short int width");
1030  INVARIANT(
1031  ansi_c.long_long_int_width == sizeof(long long) * CHAR_BIT,
1032  "long long int width shall be equal to the system long long int width");
1033  INVARIANT(
1034  ansi_c.pointer_width == sizeof(void *) * CHAR_BIT,
1035  "pointer width shall be equal to the system pointer width");
1036  INVARIANT(
1037  ansi_c.single_width == sizeof(float) * CHAR_BIT,
1038  "float width shall be equal to the system float width");
1039  INVARIANT(
1040  ansi_c.double_width == sizeof(double) * CHAR_BIT,
1041  "double width shall be equal to the system double width");
1042  INVARIANT(
1044  (static_cast<char>((1 << CHAR_BIT) - 1) == (1 << CHAR_BIT) - 1),
1045  "char_is_unsigned flag shall indicate system char unsignedness");
1046 
1047 #ifndef _WIN32
1048  // On Windows, long double width varies by compiler
1049  INVARIANT(
1050  ansi_c.long_double_width == sizeof(long double) * CHAR_BIT,
1051  "long double width shall be equal to the system long double width");
1052 #endif
1053  }
1054 
1055  // the following allows overriding the defaults
1056 
1057  if(cmdline.isset("16"))
1058  ansi_c.set_16();
1059 
1060  if(cmdline.isset("32"))
1061  ansi_c.set_32();
1062 
1063  if(cmdline.isset("64"))
1064  ansi_c.set_64();
1065 
1066  if(cmdline.isset("LP64"))
1067  ansi_c.set_LP64(); // int=32, long=64, pointer=64
1068 
1069  if(cmdline.isset("ILP64"))
1070  ansi_c.set_ILP64(); // int=64, long=64, pointer=64
1071 
1072  if(cmdline.isset("LLP64"))
1073  ansi_c.set_LLP64(); // int=32, long=32, pointer=64
1074 
1075  if(cmdline.isset("ILP32"))
1076  ansi_c.set_ILP32(); // int=32, long=32, pointer=32
1077 
1078  if(cmdline.isset("LP32"))
1079  ansi_c.set_LP32(); // int=16, long=32, pointer=32
1080 
1081  if(cmdline.isset("string-abstraction"))
1083  else
1084  ansi_c.string_abstraction=false;
1085 
1086  if(cmdline.isset("no-library"))
1088 
1089  if(cmdline.isset("little-endian"))
1091 
1092  if(cmdline.isset("big-endian"))
1094 
1095  if(cmdline.isset("little-endian") &&
1096  cmdline.isset("big-endian"))
1097  return true;
1098 
1099  if(cmdline.isset("unsigned-char"))
1100  ansi_c.char_is_unsigned=true;
1101 
1102  if(cmdline.isset("round-to-even") ||
1103  cmdline.isset("round-to-nearest"))
1105 
1106  if(cmdline.isset("round-to-plus-inf"))
1108 
1109  if(cmdline.isset("round-to-minus-inf"))
1111 
1112  if(cmdline.isset("round-to-zero"))
1114 
1115  if(cmdline.isset("object-bits"))
1116  {
1118  cmdline.get_value("object-bits"), ansi_c.pointer_width);
1119  }
1120 
1121  if(cmdline.isset("malloc-fail-assert") && cmdline.isset("malloc-fail-null"))
1122  {
1124  "at most one malloc failure mode is acceptable", "--malloc-fail-null"};
1125  }
1126  if(cmdline.isset("malloc-fail-null"))
1128  if(cmdline.isset("malloc-fail-assert"))
1130 
1131  if(cmdline.isset("malloc-may-fail"))
1132  {
1133  ansi_c.malloc_may_fail = true;
1134  }
1135  if(cmdline.isset("no-malloc-may-fail"))
1136  {
1137  ansi_c.malloc_may_fail = false;
1139  }
1140 
1141  if(cmdline.isset("c89"))
1142  ansi_c.set_c89();
1143 
1144  if(cmdline.isset("c99"))
1145  ansi_c.set_c99();
1146 
1147  if(cmdline.isset("c11"))
1148  ansi_c.set_c11();
1149 
1150  if(cmdline.isset("cpp98"))
1151  cpp.set_cpp98();
1152 
1153  if(cmdline.isset("cpp03"))
1154  cpp.set_cpp03();
1155 
1156  if(cmdline.isset("cpp11"))
1157  cpp.set_cpp11();
1158 
1159  // set the upper bound for argc
1160  if(os == "windows")
1161  {
1162  // On Windows, CreateProcess accepts no more than 32767 characters, so make
1163  // that a hard limit.
1164  ansi_c.max_argc = mp_integer{32767};
1165  }
1166  else
1167  {
1168  // For other systems assume argc is no larger than the what would make argv
1169  // the largest representable array (when using signed integers to represent
1170  // array sizes):
1171  // 2^(pointer_width - 1) / (pointer_width / char_width) is the maximum
1172  // number of argv elements sysconf(ARG_MAX) is likely much lower than this,
1173  // but we don't know that value for the verification target platform.
1174  const auto pointer_bits_2log =
1176  if(ansi_c.pointer_width - pointer_bits_2log - 1 <= ansi_c.int_width)
1177  {
1178  ansi_c.max_argc =
1179  power(2, config.ansi_c.int_width - pointer_bits_2log - 1);
1180  }
1181  // otherwise we leave argc unconstrained
1182  }
1183 
1184  return false;
1185 }
1186 
1188 {
1189  // clang-format off
1190  switch(os)
1191  {
1192  case ost::OS_LINUX: return "linux";
1193  case ost::OS_MACOS: return "macos";
1194  case ost::OS_WIN: return "win";
1195  case ost::NO_OS: return "none";
1196  }
1197  // clang-format on
1198 
1199  UNREACHABLE;
1200 }
1201 
1203 {
1204  if(os=="linux")
1205  return ost::OS_LINUX;
1206  else if(os=="macos")
1207  return ost::OS_MACOS;
1208  else if(os=="win")
1209  return ost::OS_WIN;
1210  else
1211  return ost::NO_OS;
1212 }
1213 
1215  const namespacet &ns,
1216  const std::string &what)
1217 {
1218  const irep_idt id=CPROVER_PREFIX "architecture_"+what;
1219  const symbolt *symbol;
1220 
1221  const bool not_found = ns.lookup(id, symbol);
1222  INVARIANT(!not_found, id2string(id) + " must be in namespace");
1223 
1224  const exprt &tmp=symbol->value;
1225 
1226  INVARIANT(
1227  tmp.id() == ID_address_of &&
1228  to_address_of_expr(tmp).object().id() == ID_index &&
1229  to_index_expr(to_address_of_expr(tmp).object()).array().id() ==
1230  ID_string_constant,
1231  "symbol table configuration entry '" + id2string(id) +
1232  "' must be a string constant");
1233 
1234  return to_index_expr(to_address_of_expr(tmp).object()).array().get(ID_value);
1235 }
1236 
1237 static unsigned unsigned_from_ns(
1238  const namespacet &ns,
1239  const std::string &what)
1240 {
1241  const irep_idt id=CPROVER_PREFIX "architecture_"+what;
1242  const symbolt *symbol;
1243 
1244  const bool not_found = ns.lookup(id, symbol);
1245  INVARIANT(!not_found, id2string(id) + " must be in namespace");
1246 
1247  exprt tmp=symbol->value;
1248  simplify(tmp, ns);
1249 
1250  INVARIANT(
1251  tmp.is_constant(),
1252  "symbol table configuration entry '" + id2string(id) +
1253  "' must be a constant");
1254 
1255  mp_integer int_value;
1256 
1257  const bool error = to_integer(to_constant_expr(tmp), int_value);
1258  INVARIANT(
1259  !error,
1260  "symbol table configuration entry '" + id2string(id) +
1261  "' must be convertible to mp_integer");
1262 
1263  return numeric_cast_v<unsigned>(int_value);
1264 }
1265 
1267 {
1268  // maybe not compiled from C/C++
1269  if(symbol_table.symbols.find(CPROVER_PREFIX "architecture_" "int_width")==
1270  symbol_table.symbols.end())
1271  return;
1272 
1273  namespacet ns(symbol_table);
1274 
1275  // clear defines
1276  ansi_c.defines.clear();
1277 
1278  // first set architecture to get some defaults
1279  if(symbol_table.symbols.find(CPROVER_PREFIX "architecture_" "arch")==
1280  symbol_table.symbols.end())
1282  else
1283  set_arch(string_from_ns(ns, "arch"));
1284 
1285  ansi_c.int_width=unsigned_from_ns(ns, "int_width");
1286  ansi_c.long_int_width=unsigned_from_ns(ns, "long_int_width");
1287  ansi_c.bool_width=1*8;
1288  ansi_c.char_width=unsigned_from_ns(ns, "char_width");
1289  ansi_c.short_int_width=unsigned_from_ns(ns, "short_int_width");
1290  ansi_c.long_long_int_width=unsigned_from_ns(ns, "long_long_int_width");
1291  ansi_c.pointer_width=unsigned_from_ns(ns, "pointer_width");
1292  ansi_c.single_width=unsigned_from_ns(ns, "single_width");
1293  ansi_c.double_width=unsigned_from_ns(ns, "double_width");
1294  ansi_c.long_double_width=unsigned_from_ns(ns, "long_double_width");
1295  ansi_c.wchar_t_width=unsigned_from_ns(ns, "wchar_t_width");
1296 
1297  ansi_c.char_is_unsigned=unsigned_from_ns(ns, "char_is_unsigned")!=0;
1298  ansi_c.wchar_t_is_unsigned=unsigned_from_ns(ns, "wchar_t_is_unsigned")!=0;
1299  // for_has_scope, single_precision_constant, rounding_mode,
1300  // ts_18661_3_Floatn_types, float16_type, bf16_type are not architectural
1301  // features, and thus not stored in namespace
1302 
1303  ansi_c.alignment=unsigned_from_ns(ns, "alignment");
1304 
1305  ansi_c.memory_operand_size=unsigned_from_ns(ns, "memory_operand_size");
1306 
1308 
1309  if(symbol_table.symbols.find(CPROVER_PREFIX "architecture_" "os")==
1310  symbol_table.symbols.end())
1312  else
1314 
1315  ansi_c.NULL_is_zero = unsigned_from_ns(ns, "NULL_is_zero") != 0;
1316 
1317  // mode, preprocessor (and all preprocessor command line options),
1318  // lib, string_abstraction not stored in namespace
1319 
1320  set_object_bits_from_symbol_table(symbol_table);
1321 }
1322 
1326  const symbol_table_baset &symbol_table)
1327 {
1328  // has been overridden by command line option,
1329  // thus do not apply language defaults
1331  return;
1332 
1333  // set object_bits according to entry point language
1334  if(const auto maybe_symbol=symbol_table.lookup(CPROVER_PREFIX "_start"))
1335  {
1336  const symbolt &entry_point_symbol=*maybe_symbol;
1337 
1338  if(entry_point_symbol.mode==ID_java)
1340  else if(entry_point_symbol.mode==ID_C)
1342  else if(entry_point_symbol.mode==ID_cpp)
1346  "object_bits should fit into pointer width");
1347  }
1348 }
1349 
1351 {
1352  return "Running with "+std::to_string(bv_encoding.object_bits)+
1353  " object bits, "+
1355  " offset bits ("+
1356  (bv_encoding.is_object_bits_default ? "default" : "user-specified")+
1357  ")";
1358 }
1359 
1360 // clang-format off
1362 {
1363  irep_idt this_arch;
1364 
1365  // following http://wiki.debian.org/ArchitectureSpecificsMemo
1366 
1367  #ifdef __alpha__
1368  this_arch = "alpha";
1369  #elif defined(__armel__)
1370  this_arch = "armel";
1371  #elif defined(__aarch64__)
1372  this_arch = "arm64";
1373  #elif defined(__arm__)
1374  #ifdef __ARM_PCS_VFP
1375  this_arch = "armhf"; // variant of arm with hard float
1376  #else
1377  this_arch = "arm";
1378  #endif
1379  #elif defined(_MIPSEL)
1380  #if _MIPS_SIM==_ABIO32
1381  this_arch = "mipsel";
1382  #elif _MIPS_SIM==_ABIN32
1383  this_arch = "mipsn32el";
1384  #else
1385  this_arch = "mips64el";
1386  #endif
1387  #elif defined(__mips__)
1388  #if _MIPS_SIM==_ABIO32
1389  this_arch = "mips";
1390  #elif _MIPS_SIM==_ABIN32
1391  this_arch = "mipsn32";
1392  #else
1393  this_arch = "mips64";
1394  #endif
1395  #elif defined(__powerpc__)
1396  #if defined(__ppc64__) || defined(__PPC64__) || \
1397  defined(__powerpc64__) || defined(__POWERPC64__)
1398  #ifdef __LITTLE_ENDIAN__
1399  this_arch = "ppc64le";
1400  #else
1401  this_arch = "ppc64";
1402  #endif
1403  #else
1404  this_arch = "powerpc";
1405  #endif
1406  #elif defined(__riscv)
1407  this_arch = "riscv64";
1408  #elif defined(__sparc__)
1409  #ifdef __arch64__
1410  this_arch = "sparc64";
1411  #else
1412  this_arch = "sparc";
1413  #endif
1414  #elif defined(__ia64__)
1415  this_arch = "ia64";
1416  #elif defined(__s390x__)
1417  this_arch = "s390x";
1418  #elif defined(__s390__)
1419  this_arch = "s390";
1420  #elif defined(__x86_64__)
1421  #ifdef __ILP32__
1422  this_arch = "x32"; // variant of x86_64 with 32-bit pointers
1423  #else
1424  this_arch = "x86_64";
1425  #endif
1426  #elif defined(__i386__)
1427  this_arch = "i386";
1428  #elif defined(_WIN64)
1429  this_arch = "x86_64";
1430  #elif defined(_WIN32)
1431  this_arch = "i386";
1432  #elif defined(__hppa__)
1433  this_arch = "hppa";
1434  #elif defined(__sh__)
1435  this_arch = "sh4";
1436  #else
1437  // something new and unknown!
1438  this_arch = "unknown";
1439  #endif
1440 
1441  return this_arch;
1442 }
1443 // clang-format on
1444 
1445 void configt::set_classpath(const std::string &cp)
1446 {
1447 // These are separated by colons on Unix, and semicolons on
1448 // Windows.
1449 #ifdef _WIN32
1450  const char cp_separator = ';';
1451 #else
1452  const char cp_separator = ':';
1453 #endif
1454 
1455  std::vector<std::string> class_path =
1456  split_string(cp, cp_separator);
1457  java.classpath.insert(
1458  java.classpath.end(), class_path.begin(), class_path.end());
1459 }
1460 
1462 {
1463  irep_idt this_os;
1464 
1465  #ifdef _WIN32
1466  this_os="windows";
1467  #elif __APPLE__
1468  this_os="macos";
1469  #elif __FreeBSD__
1470  this_os="freebsd";
1471 #elif __OpenBSD__
1472  this_os = "openbsd";
1473 #elif __NetBSD__
1474  this_os = "netbsd";
1475 #elif __linux__
1476  this_os="linux";
1477 #elif __SVR4
1478  this_os="solaris";
1479 #else
1480  this_os="unknown";
1481 #endif
1482 
1483  return this_os;
1484 }
std::size_t address_bits(const mp_integer &size)
ceil(log2(size))
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
mp_integer power(const mp_integer &base, const mp_integer &exponent)
A multi-precision implementation of the power operator.
std::string get_value(char option) const
Definition: cmdline.cpp:48
virtual bool isset(char option) const
Definition: cmdline.cpp:30
const std::list< std::string > & get_values(const std::string &option) const
Definition: cmdline.cpp:109
Globally accessible architectural configuration.
Definition: config.h:132
void set_object_bits_from_symbol_table(const symbol_table_baset &)
Sets the number of bits used for object addresses.
Definition: config.cpp:1325
void set_arch(const irep_idt &)
Definition: config.cpp:702
struct configt::bv_encodingt bv_encoding
bool set(const cmdlinet &cmdline)
Definition: config.cpp:798
std::string object_bits_info()
Definition: config.cpp:1350
void set_classpath(const std::string &cp)
Definition: config.cpp:1445
void set_from_symbol_table(const symbol_table_baset &)
Definition: config.cpp:1266
static irep_idt this_architecture()
Definition: config.cpp:1361
std::optional< std::string > main
Definition: config.h:356
struct configt::javat java
struct configt::cppt cpp
static irep_idt this_operating_system()
Definition: config.cpp:1461
struct configt::ansi_ct ansi_c
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
Base class for all expressions.
Definition: expr.h:56
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.h:212
@ ROUND_TO_PLUS_INF
Definition: ieee_float.h:125
@ ROUND_TO_MINUS_INF
Definition: ieee_float.h:124
exprt & array()
Definition: std_expr.h:1495
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
const irep_idt & get(const irep_idt &name) const
Definition: irep.cpp:44
const irep_idt & id() const
Definition: irep.h:384
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:148
The symbol table base class interface.
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Symbol table entry.
Definition: symbol.h:28
exprt value
Initial value of symbol.
Definition: symbol.h:34
irep_idt mode
Language mode.
Definition: symbol.h:49
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
static unsigned unsigned_from_ns(const namespacet &ns, const std::string &what)
Definition: config.cpp:1237
configt config
Definition: config.cpp:25
static irep_idt string_from_ns(const namespacet &ns, const std::string &what)
Definition: config.cpp:1214
#define CPROVER_PREFIX
const std::string & id2string(const irep_idt &d)
Definition: irep.h:40
mp_integer alignment(const typet &type, const namespacet &ns)
Definition: padding.cpp:23
API to expression classes for Pointers.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:577
bool simplify(exprt &expr, const namespacet &ns)
BigInt mp_integer
Definition: smt_terms.h:17
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:525
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:534
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:3037
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1533
char * getenv(const char *name)
Definition: stdlib.c:496
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
void split_string(const std::string &s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)
std::size_t long_double_width
Definition: config.h:146
std::list< std::string > include_paths
Definition: config.h:268
bool for_has_scope
Definition: config.h:151
void set_arch_spec_x32()
Definition: config.cpp:557
enum configt::ansi_ct::c_standardt c_standard
void set_32()
Definition: config.cpp:32
void set_arch_spec_riscv64()
Definition: config.cpp:403
endiannesst endianness
Definition: config.h:207
bool float16_type
Definition: config.h:154
void set_16()
Definition: config.cpp:27
void set_arch_spec_sh4()
Definition: config.cpp:645
bool bf16_type
Definition: config.h:155
void set_ILP32()
int=32, long=32, pointer=32
Definition: config.cpp:111
bool ts_18661_3_Floatn_types
Definition: config.h:152
void set_arch_spec_v850()
Sets up the widths of variables for the Renesas V850.
Definition: config.cpp:593
bool wchar_t_is_unsigned
Definition: config.h:150
void set_arch_spec_hppa()
Definition: config.cpp:616
static std::string os_to_string(ost)
Definition: config.cpp:1187
std::size_t pointer_width
Definition: config.h:143
bool gcc__float128_type
Definition: config.h:153
std::optional< mp_integer > max_argc
Maximum value of argc, which is operating-systems dependent: Windows limits the number of characters ...
Definition: config.h:295
void set_c89()
Definition: config.h:165
std::list< std::string > include_files
Definition: config.h:269
void set_ILP64()
int=64, long=64, pointer=64
Definition: config.cpp:71
irep_idt arch
Definition: config.h:221
ieee_floatt::rounding_modet rounding_mode
Definition: config.h:181
void set_64()
Definition: config.cpp:37
void set_arch_spec_sparc(const irep_idt &subarch)
Definition: config.cpp:486
static ost string_to_os(const std::string &)
Definition: config.cpp:1202
std::list< std::string > defines
Definition: config.h:265
void set_c99()
Definition: config.h:170
bool single_precision_constant
Definition: config.h:156
void set_LLP64()
int=32, long=32, pointer=64
Definition: config.cpp:91
void set_arch_spec_arm(const irep_idt &subarch)
Definition: config.cpp:281
std::size_t wchar_t_width
Definition: config.h:147
preprocessort preprocessor
Definition: config.h:263
@ malloc_failure_mode_return_null
Definition: config.h:284
@ malloc_failure_mode_none
Definition: config.h:283
@ malloc_failure_mode_assert_then_assume
Definition: config.h:285
std::size_t double_width
Definition: config.h:145
bool malloc_may_fail
Definition: config.h:279
bool char_is_unsigned
Definition: config.h:150
static c_standardt default_c_standard()
Definition: config.cpp:675
void set_arch_spec_alpha()
Definition: config.cpp:324
std::size_t alignment
Definition: config.h:195
void set_arch_spec_power(const irep_idt &subarch)
Definition: config.cpp:220
std::size_t bool_width
Definition: config.h:139
bool string_abstraction
Definition: config.h:278
void set_arch_spec_s390()
Definition: config.cpp:429
void set_LP64()
int=32, long=64, pointer=64
Definition: config.cpp:47
void set_arch_spec_x86_64()
Definition: config.cpp:182
void set_LP32()
int=16, long=32, pointer=32
Definition: config.cpp:131
std::size_t memory_operand_size
Definition: config.h:199
std::size_t long_long_int_width
Definition: config.h:142
void set_arch_spec_s390x()
Definition: config.cpp:458
bool NULL_is_zero
Definition: config.h:224
std::size_t long_int_width
Definition: config.h:138
void set_arch_spec_mips(const irep_idt &subarch)
Definition: config.cpp:353
std::size_t single_width
Definition: config.h:144
void set_arch_spec_i386()
Definition: config.cpp:150
std::size_t short_int_width
Definition: config.h:141
std::size_t char_width
Definition: config.h:140
void set_c11()
Definition: config.h:175
static const std::size_t default_object_bits
Definition: config.h:290
flavourt mode
Definition: config.h:252
std::size_t int_width
Definition: config.h:137
malloc_failure_modet malloc_failure_mode
Definition: config.h:288
void set_arch_spec_ia64()
Definition: config.cpp:526
bool is_object_bits_default
Definition: config.h:352
std::size_t object_bits
Definition: config.h:351
enum configt::cppt::cpp_standardt cpp_standard
void set_cpp11()
Definition: config.h:318
static const std::size_t default_object_bits
Definition: config.h:331
void set_cpp03()
Definition: config.h:314
static cpp_standardt default_cpp_standard()
Definition: config.cpp:690
void set_cpp98()
Definition: config.h:310
classpatht classpath
Definition: config.h:342
irep_idt main_class
Definition: config.h:343
static const std::size_t default_object_bits
Definition: config.h:345
Author: Diffblue Ltd.