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  if(subarch == "arm64")
312  defines.push_back("_M_ARM64");
313  else
314  defines.push_back("_M_ARM");
315  break;
316 
317  case flavourt::CODEWARRIOR:
318  case flavourt::ARM:
319  case flavourt::ANSI:
320  break;
321 
322  case flavourt::NONE:
323  UNREACHABLE;
324  }
325 }
326 
328 {
329  set_LP64();
330  endianness=endiannesst::IS_LITTLE_ENDIAN;
331  long_double_width=16*8;
332  char_is_unsigned=false;
333  NULL_is_zero=true;
334 
335  switch(mode)
336  {
337  case flavourt::GCC:
338  defines.push_back("__alpha__");
339  break;
340 
341  case flavourt::VISUAL_STUDIO:
342  defines.push_back("_M_ALPHA");
343  break;
344 
345  case flavourt::CLANG:
346  case flavourt::CODEWARRIOR:
347  case flavourt::ARM:
348  case flavourt::ANSI:
349  break;
350 
351  case flavourt::NONE:
352  UNREACHABLE;
353  }
354 }
355 
357 {
358  if(subarch=="mipsel" ||
359  subarch=="mips" ||
360  subarch=="mipsn32el" ||
361  subarch=="mipsn32")
362  {
363  set_ILP32();
364  long_double_width=8*8;
365  }
366  else
367  {
368  set_LP64();
369  long_double_width=16*8;
370  }
371 
372  if(subarch=="mipsel" ||
373  subarch=="mipsn32el" ||
374  subarch=="mips64el")
375  endianness=endiannesst::IS_LITTLE_ENDIAN;
376  else
377  endianness=endiannesst::IS_BIG_ENDIAN;
378 
379  char_is_unsigned=false;
380  NULL_is_zero=true;
381 
382  switch(mode)
383  {
384  case flavourt::GCC:
385  defines.push_back("__mips__");
386  defines.push_back("mips");
387  defines.push_back(
388  "_MIPS_SZPTR="+std::to_string(config.ansi_c.pointer_width));
389  break;
390 
391  case flavourt::VISUAL_STUDIO:
392  UNREACHABLE; // not supported by Visual Studio
393  break;
394 
395  case flavourt::CLANG:
396  case flavourt::CODEWARRIOR:
397  case flavourt::ARM:
398  case flavourt::ANSI:
399  break;
400 
401  case flavourt::NONE:
402  UNREACHABLE;
403  }
404 }
405 
407 {
408  set_LP64();
409  endianness = endiannesst::IS_LITTLE_ENDIAN;
410  long_double_width = 16 * 8;
411  char_is_unsigned = true;
412  NULL_is_zero = true;
413 
414  switch(mode)
415  {
416  case flavourt::GCC:
417  defines.push_back("__riscv");
418  break;
419 
420  case flavourt::VISUAL_STUDIO:
421  case flavourt::CLANG:
422  case flavourt::CODEWARRIOR:
423  case flavourt::ARM:
424  case flavourt::ANSI:
425  break;
426 
427  case flavourt::NONE:
428  UNREACHABLE;
429  }
430 }
431 
433 {
434  set_ILP32();
435  endianness=endiannesst::IS_BIG_ENDIAN;
436  long_double_width=16*8;
437  char_is_unsigned=true;
438  NULL_is_zero=true;
439 
440  switch(mode)
441  {
442  case flavourt::GCC:
443  defines.push_back("__s390__");
444  break;
445 
446  case flavourt::VISUAL_STUDIO:
447  UNREACHABLE; // not supported by Visual Studio
448  break;
449 
450  case flavourt::CLANG:
451  case flavourt::CODEWARRIOR:
452  case flavourt::ARM:
453  case flavourt::ANSI:
454  break;
455 
456  case flavourt::NONE:
457  UNREACHABLE;
458  }
459 }
460 
462 {
463  set_LP64();
464  endianness=endiannesst::IS_BIG_ENDIAN;
465  char_is_unsigned=true;
466  NULL_is_zero=true;
467 
468  switch(mode)
469  {
470  case flavourt::GCC:
471  defines.push_back("__s390x__");
472  break;
473 
474  case flavourt::VISUAL_STUDIO:
475  UNREACHABLE; // not supported by Visual Studio
476  break;
477 
478  case flavourt::CLANG:
479  case flavourt::CODEWARRIOR:
480  case flavourt::ARM:
481  case flavourt::ANSI:
482  break;
483 
484  case flavourt::NONE:
485  UNREACHABLE;
486  }
487 }
488 
490 {
491  if(subarch=="sparc64")
492  {
493  set_LP64();
494  long_double_width=16*8;
495  }
496  else
497  {
498  set_ILP32();
499  long_double_width=16*8;
500  }
501 
502  endianness=endiannesst::IS_BIG_ENDIAN;
503  char_is_unsigned=false;
504  NULL_is_zero=true;
505 
506  switch(mode)
507  {
508  case flavourt::GCC:
509  defines.push_back("__sparc__");
510  if(subarch=="sparc64")
511  defines.push_back("__arch64__");
512  break;
513 
514  case flavourt::VISUAL_STUDIO:
515  UNREACHABLE; // not supported by Visual Studio
516  break;
517 
518  case flavourt::CLANG:
519  case flavourt::CODEWARRIOR:
520  case flavourt::ARM:
521  case flavourt::ANSI:
522  break;
523 
524  case flavourt::NONE:
525  UNREACHABLE;
526  }
527 }
528 
530 {
531  set_LP64();
532  long_double_width=16*8;
533  endianness=endiannesst::IS_LITTLE_ENDIAN;
534  char_is_unsigned=false;
535  NULL_is_zero=true;
536 
537  switch(mode)
538  {
539  case flavourt::GCC:
540  defines.push_back("__ia64__");
541  defines.push_back("_IA64");
542  defines.push_back("__IA64__");
543  break;
544 
545  case flavourt::VISUAL_STUDIO:
546  defines.push_back("_M_IA64");
547  break;
548 
549  case flavourt::CLANG:
550  case flavourt::CODEWARRIOR:
551  case flavourt::ARM:
552  case flavourt::ANSI:
553  break;
554 
555  case flavourt::NONE:
556  UNREACHABLE;
557  }
558 }
559 
561 {
562  // This is a variant of x86_64 that has
563  // 32-bit long int and 32-bit pointers.
564  set_ILP32();
565  long_double_width=16*8; // different from i386
566  endianness=endiannesst::IS_LITTLE_ENDIAN;
567  char_is_unsigned=false;
568  NULL_is_zero=true;
569 
570  switch(mode)
571  {
572  case flavourt::GCC:
573  defines.push_back("__ILP32__");
574  defines.push_back("__x86_64");
575  defines.push_back("__x86_64__");
576  defines.push_back("__amd64__");
577  defines.push_back("__amd64");
578  break;
579 
580  case flavourt::VISUAL_STUDIO:
581  UNREACHABLE; // not supported by Visual Studio
582  break;
583 
584  case flavourt::CLANG:
585  case flavourt::CODEWARRIOR:
586  case flavourt::ARM:
587  case flavourt::ANSI:
588  break;
589 
590  case flavourt::NONE:
591  UNREACHABLE;
592  }
593 }
594 
597 {
598  // The Renesas V850 is a 32-bit microprocessor used in
599  // many automotive applications. This spec is written from the
600  // architecture manual rather than having access to a running
601  // system. Thus some assumptions have been made.
602 
603  set_ILP32();
604 
605  // Technically, the V850's don't have floating-point at all.
606  // However, the RH850, aimed at automotive has both 32-bit and
607  // 64-bit IEEE-754 float.
608  double_width=8*8;
609  long_double_width=8*8;
610  endianness=endiannesst::IS_LITTLE_ENDIAN;
611 
612  // Without information about the compiler and RTOS, these are guesses
613  char_is_unsigned=false;
614  NULL_is_zero=true;
615 
616  // No preprocessor definitions due to lack of information
617 }
618 
620 {
621  set_ILP32();
622  long_double_width=8*8; // different from i386
623  endianness=endiannesst::IS_BIG_ENDIAN;
624  char_is_unsigned=false;
625  NULL_is_zero=true;
626 
627  switch(mode)
628  {
629  case flavourt::GCC:
630  defines.push_back("__hppa__");
631  break;
632 
633  case flavourt::VISUAL_STUDIO:
634  UNREACHABLE; // not supported by Visual Studio
635  break;
636 
637  case flavourt::CLANG:
638  case flavourt::CODEWARRIOR:
639  case flavourt::ARM:
640  case flavourt::ANSI:
641  break;
642 
643  case flavourt::NONE:
644  UNREACHABLE;
645  }
646 }
647 
649 {
650  set_ILP32();
651  long_double_width=8*8; // different from i386
652  endianness=endiannesst::IS_LITTLE_ENDIAN;
653  char_is_unsigned=false;
654  NULL_is_zero=true;
655 
656  switch(mode)
657  {
658  case flavourt::GCC:
659  defines.push_back("__sh__");
660  defines.push_back("__SH4__");
661  break;
662 
663  case flavourt::VISUAL_STUDIO:
664  UNREACHABLE; // not supported by Visual Studio
665  break;
666 
667  case flavourt::CLANG:
668  case flavourt::CODEWARRIOR:
669  case flavourt::ARM:
670  case flavourt::ANSI:
671  break;
672 
673  case flavourt::NONE:
674  UNREACHABLE;
675  }
676 }
677 
679 {
680  set_LP64();
681  endianness = endiannesst::IS_LITTLE_ENDIAN;
682  long_double_width = 16 * 8;
683  char_is_unsigned = false;
684  NULL_is_zero = true;
685 
686  switch(mode)
687  {
688  case flavourt::GCC:
689  defines.push_back("__loongarch__");
690  break;
691 
692  case flavourt::VISUAL_STUDIO:
693  UNREACHABLE; // not supported by Visual Studio
694  break;
695 
696  case flavourt::CODEWARRIOR:
697  case flavourt::CLANG:
698  case flavourt::ARM:
699  case flavourt::ANSI:
700  break;
701 
702  case flavourt::NONE:
703  UNREACHABLE;
704  }
705 }
706 
708 {
709  set_ILP32();
710  endianness = endiannesst::IS_LITTLE_ENDIAN;
711  long_double_width = 16 * 8;
712  char_is_unsigned = false;
713  NULL_is_zero = true;
714 
715  switch(mode)
716  {
717  case flavourt::CLANG:
718  defines.push_back("__EMSCRIPTEN__");
719  break;
720 
721  case flavourt::VISUAL_STUDIO:
722  UNREACHABLE; // not supported by Visual Studio
723  break;
724 
725  case flavourt::GCC:
726  case flavourt::CODEWARRIOR:
727  case flavourt::ARM:
728  case flavourt::ANSI:
729  break;
730 
731  case flavourt::NONE:
732  UNREACHABLE;
733  }
734 }
735 
737 {
738 #if defined(__APPLE__)
739  // By default, clang on the Mac builds C code in GNU C11
740  return c_standardt::C11;
741 #elif defined(__FreeBSD__) || defined(__OpenBSD__)
742  // By default, clang on FreeBSD builds C code in GNU C99
743  // By default, clang on OpenBSD builds C code in C99
744  return c_standardt::C99;
745 #else
746  // By default, gcc 5.4 or higher use gnu11; older versions use gnu89
747  return c_standardt::C11;
748 #endif
749 }
750 
752 {
753  // g++ 6.3 uses gnu++14
754  // g++ 5.4 uses gnu++98
755  // clang 6.0 uses c++14
756  #if defined _WIN32
757  return cpp_standardt::CPP14;
758  #else
759  return cpp_standardt::CPP98;
760  #endif
761 }
762 
763 void configt::set_arch(const irep_idt &arch)
764 {
765  ansi_c.arch=arch;
766 
767  if(arch=="none")
768  {
769  // the architecture for people who can't commit
772  ansi_c.NULL_is_zero=false;
773 
774  if(sizeof(long int)==8)
775  ansi_c.set_64();
776  else
777  ansi_c.set_32();
778  }
779  else if(arch=="alpha")
781  else if(arch=="arm64" ||
782  arch=="armel" ||
783  arch=="armhf" ||
784  arch=="arm")
786  else if(arch=="mips64el" ||
787  arch=="mipsn32el" ||
788  arch=="mipsel" ||
789  arch=="mips64" ||
790  arch=="mipsn32" ||
791  arch=="mips")
793  else if(arch=="powerpc" ||
794  arch=="ppc64" ||
795  arch=="ppc64le")
797  else if(arch == "riscv64")
799  else if(arch=="sparc" ||
800  arch=="sparc64")
802  else if(arch=="ia64")
804  else if(arch=="s390x")
806  else if(arch=="s390")
808  else if(arch=="x32")
810  else if(arch=="v850")
812  else if(arch=="hppa")
814  else if(arch=="sh4")
816  else if(arch=="x86_64")
818  else if(arch=="i386")
820  else if(arch == "loongarch64")
822  else if(arch == "emscripten")
824  else
825  {
826  // We run on something new and unknown.
827  // We verify for i386 instead.
829  ansi_c.arch="i386";
830  }
831 }
832 
841  const std::string &argument,
842  const std::size_t pointer_width)
843 {
844  const auto throw_for_reason = [&](const std::string &reason) {
846  "Value of \"" + argument + "\" given for object-bits is " + reason +
847  ". object-bits must be positive and less than the pointer width (" +
848  std::to_string(pointer_width) + ") ",
849  "--object_bits");
850  };
851  const auto object_bits = string2optional<unsigned int>(argument);
852  if(!object_bits)
853  throw_for_reason("not a valid unsigned integer");
854  if(*object_bits == 0 || *object_bits >= pointer_width)
855  throw_for_reason("out of range");
856 
858  bv_encoding.object_bits = *object_bits;
860  return bv_encoding;
861 }
862 
863 bool configt::set(const cmdlinet &cmdline)
864 {
865  // defaults -- we match the architecture we have ourselves
866 
868 
870  ansi_c.for_has_scope=true; // C99 or later
873  ansi_c.float16_type = false;
874  ansi_c.bf16_type = false;
875  ansi_c.fp16_type = false;
879  ansi_c.arch="none";
881  // NOLINTNEXTLINE(readability/casting)
882  ansi_c.NULL_is_zero=reinterpret_cast<size_t>(nullptr)==0;
883 
884  // Default is ROUND_TO_EVEN, justified by C99:
885  // 1 At program startup the floating-point environment is initialized as
886  // prescribed by IEC 60559:
887  // - All floating-point exception status flags are cleared.
888  // - The rounding direction mode is rounding to nearest.
890 
891  if(cmdline.isset("function"))
892  main=cmdline.get_value("function");
893 
894  if(cmdline.isset('D'))
895  ansi_c.defines=cmdline.get_values('D');
896 
897  if(cmdline.isset('I'))
898  ansi_c.include_paths=cmdline.get_values('I');
899 
900  if(cmdline.isset("classpath"))
901  {
902  // Specifying -classpath or -cp overrides any setting of the
903  // CLASSPATH environment variable.
904  set_classpath(cmdline.get_value("classpath"));
905  }
906  else if(cmdline.isset("cp"))
907  {
908  // Specifying -classpath or -cp overrides any setting of the
909  // CLASSPATH environment variable.
910  set_classpath(cmdline.get_value("cp"));
911  }
912  else
913  {
914  // environment variable set?
915  const char *CLASSPATH=getenv("CLASSPATH");
916  if(CLASSPATH!=nullptr)
917  set_classpath(CLASSPATH);
918  else
919  set_classpath("."); // default
920  }
921 
922  if(cmdline.isset("main-class"))
923  java.main_class=cmdline.get_value("main-class");
924 
925  if(cmdline.isset("include"))
926  ansi_c.include_files=cmdline.get_values("include");
927 
928  // the default architecture is the one we run on
929  irep_idt this_arch=this_architecture();
930  irep_idt arch=this_arch;
931 
932  // let's pick an OS now
933  // the default is the one we run on
935  irep_idt os=this_os;
936 
937  if(cmdline.isset("i386-linux"))
938  {
939  os="linux";
940  arch="i386";
941  }
942  else if(cmdline.isset("i386-win32") ||
943  cmdline.isset("win32"))
944  {
945  os="windows";
946  arch="i386";
947  }
948  else if(cmdline.isset("winx64"))
949  {
950  os="windows";
951  arch="x86_64";
952  }
953  else if(cmdline.isset("i386-macos"))
954  {
955  os="macos";
956  arch="i386";
957  }
958  else if(cmdline.isset("ppc-macos"))
959  {
960  arch="powerpc";
961  os="macos";
962  }
963 
964  if(cmdline.isset("arch"))
965  {
966  arch=cmdline.get_value("arch");
967  }
968 
969  if(cmdline.isset("os"))
970  {
971  os=cmdline.get_value("os");
972  }
973 
974  if(os=="windows")
975  {
976  // Cygwin uses GCC throughout, use i386-linux
977  // MinGW needs --win32 --gcc
980 
981  if(cmdline.isset("gcc"))
982  {
983  // There are gcc versions that target Windows (MinGW for example),
984  // and we support that.
987 
988  // enable Cygwin
989  #ifdef _WIN32
990  ansi_c.defines.push_back("__CYGWIN__");
991  #endif
992 
993  // MinGW has extra defines
994  ansi_c.defines.push_back("__int64=long long");
995  }
996  else
997  {
998  // On Windows, our default is Visual Studio.
999  // On FreeBSD, it's clang.
1000  // On anything else, it's GCC as the preprocessor,
1001  // but we recognize the Visual Studio language,
1002  // which is somewhat inconsistent.
1003  #ifdef _WIN32
1006 #elif defined(__FreeBSD__) || defined(__OpenBSD__)
1009 #else
1012 #endif
1013 
1015  }
1016  }
1017  else if(os=="macos")
1018  {
1023  // configure_gcc sets these with additional version-of-clang level of
1024  // detail, but the below are reasonable defaults for modern clang
1025  // installations
1027  ansi_c.float16_type = true;
1028  ansi_c.bf16_type = true;
1029  ansi_c.fp16_type = true;
1030  }
1031  else if(os == "linux" || os == "solaris" || os == "netbsd" || os == "hurd")
1032  {
1037  }
1038  else if(os == "freebsd" || os == "openbsd")
1039  {
1044  // configure_gcc sets these with additional version-of-clang level of
1045  // detail, but the below are reasonable defaults for modern clang
1046  // installations
1048  ansi_c.float16_type = true;
1049  ansi_c.bf16_type = true;
1050  ansi_c.fp16_type = true;
1051  }
1052  else
1053  {
1054  // give up, but use reasonable defaults
1059  }
1060 
1062  ansi_c.gcc__float128_type = true;
1063 
1064  set_arch(arch);
1065 
1066  if(os=="windows")
1067  {
1068  // note that sizeof(void *)==8, but sizeof(long)==4!
1069  if(arch=="x86_64")
1070  ansi_c.set_LLP64();
1071 
1072  // On Windows, wchar_t is unsigned 16 bit, regardless
1073  // of the compiler used.
1074  ansi_c.wchar_t_width=2*8;
1076 
1077  // long double is the same as double in Visual Studio,
1078  // but it's 16 bytes with GCC with the 64-bit target.
1079  if(arch == "x86_64" && cmdline.isset("gcc"))
1081  else
1083  }
1084  else if(os == "macos" && arch == "arm64")
1085  {
1086  // https://developer.apple.com/documentation/xcode/
1087  // writing_arm64_code_for_apple_platforms#//apple_ref/doc/uid/TP40013702-SW1
1088  ansi_c.char_is_unsigned = false;
1089  ansi_c.long_double_width = 8 * 8;
1090  }
1091 
1092  // Let's check some of the type widths in case we run
1093  // the same architecture and OS that we are verifying for.
1094  if(arch==this_arch && os==this_os)
1095  {
1096  INVARIANT(
1097  ansi_c.int_width == sizeof(int) * CHAR_BIT,
1098  "int width shall be equal to the system int width");
1099  INVARIANT(
1100  ansi_c.long_int_width == sizeof(long) * CHAR_BIT,
1101  "long int width shall be equal to the system long int width");
1102  INVARIANT(
1103  ansi_c.bool_width == sizeof(bool) * CHAR_BIT,
1104  "bool width shall be equal to the system bool width");
1105  INVARIANT(
1106  ansi_c.char_width == sizeof(char) * CHAR_BIT,
1107  "char width shall be equal to the system char width");
1108  INVARIANT(
1109  ansi_c.short_int_width == sizeof(short) * CHAR_BIT,
1110  "short int width shall be equal to the system short int width");
1111  INVARIANT(
1112  ansi_c.long_long_int_width == sizeof(long long) * CHAR_BIT,
1113  "long long int width shall be equal to the system long long int width");
1114  INVARIANT(
1115  ansi_c.pointer_width == sizeof(void *) * CHAR_BIT,
1116  "pointer width shall be equal to the system pointer width");
1117  INVARIANT(
1118  ansi_c.single_width == sizeof(float) * CHAR_BIT,
1119  "float width shall be equal to the system float width");
1120  INVARIANT(
1121  ansi_c.double_width == sizeof(double) * CHAR_BIT,
1122  "double width shall be equal to the system double width");
1123  INVARIANT(
1125  (static_cast<char>((1 << CHAR_BIT) - 1) == (1 << CHAR_BIT) - 1),
1126  "char_is_unsigned flag shall indicate system char unsignedness");
1127 
1128 #ifndef _WIN32
1129  // On Windows, long double width varies by compiler
1130  INVARIANT(
1131  ansi_c.long_double_width == sizeof(long double) * CHAR_BIT,
1132  "long double width shall be equal to the system long double width");
1133 #endif
1134  }
1135 
1136  // the following allows overriding the defaults
1137 
1138  if(cmdline.isset("16"))
1139  ansi_c.set_16();
1140 
1141  if(cmdline.isset("32"))
1142  ansi_c.set_32();
1143 
1144  if(cmdline.isset("64"))
1145  ansi_c.set_64();
1146 
1147  if(cmdline.isset("LP64"))
1148  ansi_c.set_LP64(); // int=32, long=64, pointer=64
1149 
1150  if(cmdline.isset("ILP64"))
1151  ansi_c.set_ILP64(); // int=64, long=64, pointer=64
1152 
1153  if(cmdline.isset("LLP64"))
1154  ansi_c.set_LLP64(); // int=32, long=32, pointer=64
1155 
1156  if(cmdline.isset("ILP32"))
1157  ansi_c.set_ILP32(); // int=32, long=32, pointer=32
1158 
1159  if(cmdline.isset("LP32"))
1160  ansi_c.set_LP32(); // int=16, long=32, pointer=32
1161 
1162  if(cmdline.isset("string-abstraction"))
1164  else
1165  ansi_c.string_abstraction=false;
1166 
1167  if(cmdline.isset("no-library"))
1169 
1170  if(cmdline.isset("little-endian"))
1172 
1173  if(cmdline.isset("big-endian"))
1175 
1176  if(cmdline.isset("little-endian") &&
1177  cmdline.isset("big-endian"))
1178  return true;
1179 
1180  if(cmdline.isset("unsigned-char"))
1181  ansi_c.char_is_unsigned=true;
1182 
1183  if(cmdline.isset("round-to-even") ||
1184  cmdline.isset("round-to-nearest"))
1186 
1187  if(cmdline.isset("round-to-plus-inf"))
1189 
1190  if(cmdline.isset("round-to-minus-inf"))
1192 
1193  if(cmdline.isset("round-to-zero"))
1195 
1196  if(cmdline.isset("object-bits"))
1197  {
1199  cmdline.get_value("object-bits"), ansi_c.pointer_width);
1200  }
1201 
1202  if(cmdline.isset("malloc-fail-assert") && cmdline.isset("malloc-fail-null"))
1203  {
1205  "at most one malloc failure mode is acceptable", "--malloc-fail-null"};
1206  }
1207  if(cmdline.isset("malloc-fail-null"))
1209  if(cmdline.isset("malloc-fail-assert"))
1211 
1212  if(cmdline.isset("malloc-may-fail"))
1213  {
1214  ansi_c.malloc_may_fail = true;
1215  }
1216  if(cmdline.isset("no-malloc-may-fail"))
1217  {
1218  ansi_c.malloc_may_fail = false;
1220  }
1221 
1222  if(cmdline.isset("c89"))
1223  ansi_c.set_c89();
1224 
1225  if(cmdline.isset("c99"))
1226  ansi_c.set_c99();
1227 
1228  if(cmdline.isset("c11"))
1229  ansi_c.set_c11();
1230 
1231  if(cmdline.isset("cpp98"))
1232  cpp.set_cpp98();
1233 
1234  if(cmdline.isset("cpp03"))
1235  cpp.set_cpp03();
1236 
1237  if(cmdline.isset("cpp11"))
1238  cpp.set_cpp11();
1239 
1240  // set the upper bound for argc
1241  if(os == "windows")
1242  {
1243  // On Windows, CreateProcess accepts no more than 32767 characters, so make
1244  // that a hard limit.
1245  ansi_c.max_argc = mp_integer{32767};
1246  }
1247  else
1248  {
1249  // For other systems assume argc is no larger than the what would make argv
1250  // the largest representable array (when using signed integers to represent
1251  // array sizes):
1252  // 2^(pointer_width - 1) / (pointer_width / char_width) is the maximum
1253  // number of argv elements sysconf(ARG_MAX) is likely much lower than this,
1254  // but we don't know that value for the verification target platform.
1255  const auto pointer_bits_2log =
1257  if(ansi_c.pointer_width - pointer_bits_2log - 1 <= ansi_c.int_width)
1258  {
1259  ansi_c.max_argc =
1260  power(2, config.ansi_c.int_width - pointer_bits_2log - 1);
1261  }
1262  // otherwise we leave argc unconstrained
1263  }
1264 
1265  return false;
1266 }
1267 
1269 {
1270  // clang-format off
1271  switch(os)
1272  {
1273  case ost::OS_LINUX: return "linux";
1274  case ost::OS_MACOS: return "macos";
1275  case ost::OS_WIN: return "win";
1276  case ost::NO_OS: return "none";
1277  }
1278  // clang-format on
1279 
1280  UNREACHABLE;
1281 }
1282 
1284 {
1285  if(os=="linux")
1286  return ost::OS_LINUX;
1287  else if(os=="macos")
1288  return ost::OS_MACOS;
1289  else if(os=="win")
1290  return ost::OS_WIN;
1291  else
1292  return ost::NO_OS;
1293 }
1294 
1296  const namespacet &ns,
1297  const std::string &what)
1298 {
1299  const irep_idt id=CPROVER_PREFIX "architecture_"+what;
1300  const symbolt *symbol;
1301 
1302  const bool not_found = ns.lookup(id, symbol);
1303  INVARIANT(!not_found, id2string(id) + " must be in namespace");
1304 
1305  const exprt &tmp=symbol->value;
1306 
1307  INVARIANT(
1308  tmp.id() == ID_address_of &&
1309  to_address_of_expr(tmp).object().id() == ID_index &&
1310  to_index_expr(to_address_of_expr(tmp).object()).array().id() ==
1311  ID_string_constant,
1312  "symbol table configuration entry '" + id2string(id) +
1313  "' must be a string constant");
1314 
1315  return to_index_expr(to_address_of_expr(tmp).object()).array().get(ID_value);
1316 }
1317 
1318 static unsigned unsigned_from_ns(
1319  const namespacet &ns,
1320  const std::string &what)
1321 {
1322  const irep_idt id=CPROVER_PREFIX "architecture_"+what;
1323  const symbolt *symbol;
1324 
1325  const bool not_found = ns.lookup(id, symbol);
1326  INVARIANT(!not_found, id2string(id) + " must be in namespace");
1327 
1328  exprt tmp=symbol->value;
1329  simplify(tmp, ns);
1330 
1331  INVARIANT(
1332  tmp.is_constant(),
1333  "symbol table configuration entry '" + id2string(id) +
1334  "' must be a constant");
1335 
1336  mp_integer int_value;
1337 
1338  const bool error = to_integer(to_constant_expr(tmp), int_value);
1339  INVARIANT(
1340  !error,
1341  "symbol table configuration entry '" + id2string(id) +
1342  "' must be convertible to mp_integer");
1343 
1344  return numeric_cast_v<unsigned>(int_value);
1345 }
1346 
1348 {
1349  // maybe not compiled from C/C++
1350  if(symbol_table.symbols.find(CPROVER_PREFIX "architecture_" "int_width")==
1351  symbol_table.symbols.end())
1352  return;
1353 
1354  namespacet ns(symbol_table);
1355 
1356  // clear defines
1357  ansi_c.defines.clear();
1358 
1359  // first set architecture to get some defaults
1360  if(symbol_table.symbols.find(CPROVER_PREFIX "architecture_" "arch")==
1361  symbol_table.symbols.end())
1363  else
1364  set_arch(string_from_ns(ns, "arch"));
1365 
1366  ansi_c.int_width=unsigned_from_ns(ns, "int_width");
1367  ansi_c.long_int_width=unsigned_from_ns(ns, "long_int_width");
1368  ansi_c.bool_width=1*8;
1369  ansi_c.char_width=unsigned_from_ns(ns, "char_width");
1370  ansi_c.short_int_width=unsigned_from_ns(ns, "short_int_width");
1371  ansi_c.long_long_int_width=unsigned_from_ns(ns, "long_long_int_width");
1372  ansi_c.pointer_width=unsigned_from_ns(ns, "pointer_width");
1373  ansi_c.single_width=unsigned_from_ns(ns, "single_width");
1374  ansi_c.double_width=unsigned_from_ns(ns, "double_width");
1375  ansi_c.long_double_width=unsigned_from_ns(ns, "long_double_width");
1376  ansi_c.wchar_t_width=unsigned_from_ns(ns, "wchar_t_width");
1377 
1378  ansi_c.char_is_unsigned=unsigned_from_ns(ns, "char_is_unsigned")!=0;
1379  ansi_c.wchar_t_is_unsigned=unsigned_from_ns(ns, "wchar_t_is_unsigned")!=0;
1380  // for_has_scope, single_precision_constant, rounding_mode,
1381  // ts_18661_3_Floatn_types, __float128_is_keyword, float16_type, bf16_type,
1382  // fp16_type are not architectural features, and thus not stored in namespace
1383 
1384  ansi_c.alignment=unsigned_from_ns(ns, "alignment");
1385 
1386  ansi_c.memory_operand_size=unsigned_from_ns(ns, "memory_operand_size");
1387 
1389 
1390  if(symbol_table.symbols.find(CPROVER_PREFIX "architecture_" "os")==
1391  symbol_table.symbols.end())
1393  else
1395 
1396  ansi_c.NULL_is_zero = unsigned_from_ns(ns, "NULL_is_zero") != 0;
1397 
1398  // mode, preprocessor (and all preprocessor command line options),
1399  // lib, string_abstraction not stored in namespace
1400 
1401  set_object_bits_from_symbol_table(symbol_table);
1402 }
1403 
1407  const symbol_table_baset &symbol_table)
1408 {
1409  // has been overridden by command line option,
1410  // thus do not apply language defaults
1412  return;
1413 
1414  // set object_bits according to entry point language
1415  if(const auto maybe_symbol=symbol_table.lookup(CPROVER_PREFIX "_start"))
1416  {
1417  const symbolt &entry_point_symbol=*maybe_symbol;
1418 
1419  if(entry_point_symbol.mode==ID_java)
1421  else if(entry_point_symbol.mode==ID_C)
1423  else if(entry_point_symbol.mode==ID_cpp)
1427  "object_bits should fit into pointer width");
1428  }
1429 }
1430 
1432 {
1433  return "Running with "+std::to_string(bv_encoding.object_bits)+
1434  " object bits, "+
1436  " offset bits ("+
1437  (bv_encoding.is_object_bits_default ? "default" : "user-specified")+
1438  ")";
1439 }
1440 
1441 // clang-format off
1443 {
1444  irep_idt this_arch;
1445 
1446  // following http://wiki.debian.org/ArchitectureSpecificsMemo
1447 
1448  #ifdef __alpha__
1449  this_arch = "alpha";
1450  #elif defined(__armel__)
1451  this_arch = "armel";
1452  #elif defined(__aarch64__)
1453  this_arch = "arm64";
1454  #elif defined(__arm__)
1455  #ifdef __ARM_PCS_VFP
1456  this_arch = "armhf"; // variant of arm with hard float
1457  #else
1458  this_arch = "arm";
1459  #endif
1460  #elif defined(_MIPSEL)
1461  #if _MIPS_SIM==_ABIO32
1462  this_arch = "mipsel";
1463  #elif _MIPS_SIM==_ABIN32
1464  this_arch = "mipsn32el";
1465  #else
1466  this_arch = "mips64el";
1467  #endif
1468  #elif defined(__mips__)
1469  #if _MIPS_SIM==_ABIO32
1470  this_arch = "mips";
1471  #elif _MIPS_SIM==_ABIN32
1472  this_arch = "mipsn32";
1473  #else
1474  this_arch = "mips64";
1475  #endif
1476  #elif defined(__powerpc__)
1477  #if defined(__ppc64__) || defined(__PPC64__) || \
1478  defined(__powerpc64__) || defined(__POWERPC64__)
1479  #ifdef __LITTLE_ENDIAN__
1480  this_arch = "ppc64le";
1481  #else
1482  this_arch = "ppc64";
1483  #endif
1484  #else
1485  this_arch = "powerpc";
1486  #endif
1487  #elif defined(__riscv)
1488  this_arch = "riscv64";
1489  #elif defined(__sparc__)
1490  #ifdef __arch64__
1491  this_arch = "sparc64";
1492  #else
1493  this_arch = "sparc";
1494  #endif
1495  #elif defined(__ia64__)
1496  this_arch = "ia64";
1497  #elif defined(__s390x__)
1498  this_arch = "s390x";
1499  #elif defined(__s390__)
1500  this_arch = "s390";
1501  #elif defined(__x86_64__)
1502  #ifdef __ILP32__
1503  this_arch = "x32"; // variant of x86_64 with 32-bit pointers
1504  #else
1505  this_arch = "x86_64";
1506  #endif
1507  #elif defined(__i386__)
1508  this_arch = "i386";
1509  #elif defined(_WIN64)
1510  this_arch = "x86_64";
1511  #elif defined(_WIN32)
1512  this_arch = "i386";
1513  #elif defined(__hppa__)
1514  this_arch = "hppa";
1515  #elif defined(__sh__)
1516  this_arch = "sh4";
1517  #elif defined(__loongarch__)
1518  this_arch = "loongarch64";
1519  #elif defined(__EMSCRIPTEN__)
1520  this_arch = "emscripten";
1521  #else
1522  // something new and unknown!
1523  this_arch = "unknown";
1524  #endif
1525 
1526  return this_arch;
1527 }
1528 // clang-format on
1529 
1530 void configt::set_classpath(const std::string &cp)
1531 {
1532 // These are separated by colons on Unix, and semicolons on
1533 // Windows.
1534 #ifdef _WIN32
1535  const char cp_separator = ';';
1536 #else
1537  const char cp_separator = ':';
1538 #endif
1539 
1540  std::vector<std::string> class_path =
1541  split_string(cp, cp_separator);
1542  java.classpath.insert(
1543  java.classpath.end(), class_path.begin(), class_path.end());
1544 }
1545 
1547 {
1548  irep_idt this_os;
1549 
1550  #ifdef _WIN32
1551  this_os="windows";
1552  #elif __APPLE__
1553  this_os="macos";
1554  #elif __FreeBSD__
1555  this_os="freebsd";
1556 #elif __OpenBSD__
1557  this_os = "openbsd";
1558 #elif __NetBSD__
1559  this_os = "netbsd";
1560 #elif __linux__
1561  this_os="linux";
1562 #elif __SVR4
1563  this_os="solaris";
1564 #elif __gnu_hurd__
1565  this_os = "hurd";
1566 #elif __EMSCRIPTEN__
1567  this_os = "emscripten";
1568 #else
1569  this_os="unknown";
1570 #endif
1571 
1572  return this_os;
1573 }
1574 
1588 {
1592  const auto offset_bits = ansi_c.pointer_width - bv_encoding.object_bits;
1593  // We require the offset to be able to express upto allocation_size - 1,
1594  // but also down to -allocation_size, therefore the size is allowable
1595  // is number of bits, less the signed bit.
1596  const auto bits_for_positive_offset = offset_bits - 1;
1597  return ((mp_integer)1) << (mp_integer)bits_for_positive_offset;
1598 }
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:119
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:1406
void set_arch(const irep_idt &)
Definition: config.cpp:763
struct configt::bv_encodingt bv_encoding
bool set(const cmdlinet &cmdline)
Definition: config.cpp:863
std::string object_bits_info()
Definition: config.cpp:1431
void set_classpath(const std::string &cp)
Definition: config.cpp:1530
mp_integer max_malloc_size() const
The maximum allocation size is determined by the number of bits that are left in the pointer of width...
Definition: config.cpp:1587
void set_from_symbol_table(const symbol_table_baset &)
Definition: config.cpp:1347
static irep_idt this_architecture()
Definition: config.cpp:1442
std::optional< std::string > main
Definition: config.h:360
struct configt::javat java
struct configt::cppt cpp
static irep_idt this_operating_system()
Definition: config.cpp:1546
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:1500
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:388
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:840
static unsigned unsigned_from_ns(const namespacet &ns, const std::string &what)
Definition: config.cpp:1318
configt config
Definition: config.cpp:25
static irep_idt string_from_ns(const namespacet &ns, const std::string &what)
Definition: config.cpp:1295
#define CPROVER_PREFIX
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
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
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:3055
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1538
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:272
bool for_has_scope
Definition: config.h:151
void set_arch_spec_x32()
Definition: config.cpp:560
enum configt::ansi_ct::c_standardt c_standard
void set_32()
Definition: config.cpp:32
void set_arch_spec_riscv64()
Definition: config.cpp:406
endiannesst endianness
Definition: config.h:209
bool float16_type
Definition: config.h:155
void set_16()
Definition: config.cpp:27
void set_arch_spec_sh4()
Definition: config.cpp:648
void set_arch_spec_loongarch64()
Definition: config.cpp:678
bool bf16_type
Definition: config.h:156
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:596
bool wchar_t_is_unsigned
Definition: config.h:150
void set_arch_spec_hppa()
Definition: config.cpp:619
static std::string os_to_string(ost)
Definition: config.cpp:1268
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:299
void set_c89()
Definition: config.h:167
std::list< std::string > include_files
Definition: config.h:273
void set_ILP64()
int=64, long=64, pointer=64
Definition: config.cpp:71
irep_idt arch
Definition: config.h:223
ieee_floatt::rounding_modet rounding_mode
Definition: config.h:183
bool __float128_is_keyword
Definition: config.h:154
void set_64()
Definition: config.cpp:37
void set_arch_spec_sparc(const irep_idt &subarch)
Definition: config.cpp:489
static ost string_to_os(const std::string &)
Definition: config.cpp:1283
std::list< std::string > defines
Definition: config.h:269
void set_c99()
Definition: config.h:172
bool single_precision_constant
Definition: config.h:158
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:267
@ malloc_failure_mode_return_null
Definition: config.h:288
@ malloc_failure_mode_none
Definition: config.h:287
@ malloc_failure_mode_assert_then_assume
Definition: config.h:289
std::size_t double_width
Definition: config.h:145
bool malloc_may_fail
Definition: config.h:283
bool char_is_unsigned
Definition: config.h:150
static c_standardt default_c_standard()
Definition: config.cpp:736
void set_arch_spec_alpha()
Definition: config.cpp:327
std::size_t alignment
Definition: config.h:197
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:282
void set_arch_spec_s390()
Definition: config.cpp:432
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:201
std::size_t long_long_int_width
Definition: config.h:142
bool fp16_type
Definition: config.h:157
void set_arch_spec_s390x()
Definition: config.cpp:461
bool NULL_is_zero
Definition: config.h:226
std::size_t long_int_width
Definition: config.h:138
void set_arch_spec_mips(const irep_idt &subarch)
Definition: config.cpp:356
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:177
static const std::size_t default_object_bits
Definition: config.h:294
flavourt mode
Definition: config.h:256
std::size_t int_width
Definition: config.h:137
malloc_failure_modet malloc_failure_mode
Definition: config.h:292
void set_arch_spec_ia64()
Definition: config.cpp:529
void set_arch_spec_emscripten()
Definition: config.cpp:707
bool is_object_bits_default
Definition: config.h:356
std::size_t object_bits
Definition: config.h:355
enum configt::cppt::cpp_standardt cpp_standard
void set_cpp11()
Definition: config.h:322
static const std::size_t default_object_bits
Definition: config.h:335
void set_cpp03()
Definition: config.h:318
static cpp_standardt default_cpp_standard()
Definition: config.cpp:751
void set_cpp98()
Definition: config.h:314
classpatht classpath
Definition: config.h:346
irep_idt main_class
Definition: config.h:347
static const std::size_t default_object_bits
Definition: config.h:349
Author: Diffblue Ltd.