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 <climits>
12 #include <cstdlib>
13 
14 #include "arith_tools.h"
15 #include "cmdline.h"
16 #include "cprover_prefix.h"
17 #include "exception_utils.h"
18 #include "namespace.h"
19 #include "pointer_expr.h"
20 #include "simplify_expr.h"
21 #include "string2int.h"
22 #include "string_utils.h"
23 #include "symbol_table.h"
24 
25 configt config;
26 
27 void configt::ansi_ct::set_16()
28 {
29  set_LP32();
30 }
31 
32 void configt::ansi_ct::set_32()
33 {
34  set_ILP32();
35 }
36 
37 void configt::ansi_ct::set_64()
38 {
39  #ifdef _WIN32
40  set_LLP64();
41  #else
42  set_LP64();
43  #endif
44 }
45 
47 void configt::ansi_ct::set_LP64()
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 
71 void configt::ansi_ct::set_ILP64()
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 
91 void configt::ansi_ct::set_LLP64()
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 
111 void configt::ansi_ct::set_ILP32()
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 
131 void configt::ansi_ct::set_LP32()
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 
150 void configt::ansi_ct::set_arch_spec_i386()
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 
182 void configt::ansi_ct::set_arch_spec_x86_64()
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 
220 void configt::ansi_ct::set_arch_spec_power(const irep_idt &subarch)
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 
281 void configt::ansi_ct::set_arch_spec_arm(const irep_idt &subarch)
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 
324 void configt::ansi_ct::set_arch_spec_alpha()
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 
353 void configt::ansi_ct::set_arch_spec_mips(const irep_idt &subarch)
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 
403 void configt::ansi_ct::set_arch_spec_riscv64()
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 
429 void configt::ansi_ct::set_arch_spec_s390()
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 
458 void configt::ansi_ct::set_arch_spec_s390x()
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 
486 void configt::ansi_ct::set_arch_spec_sparc(const irep_idt &subarch)
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 
526 void configt::ansi_ct::set_arch_spec_ia64()
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 
557 void configt::ansi_ct::set_arch_spec_x32()
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 
593 void configt::ansi_ct::set_arch_spec_v850()
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 
616 void configt::ansi_ct::set_arch_spec_hppa()
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 
645 void configt::ansi_ct::set_arch_spec_sh4()
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 
675 configt::ansi_ct::c_standardt configt::ansi_ct::default_c_standard()
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 
690 configt::cppt::cpp_standardt configt::cppt::default_cpp_standard()
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
709  ansi_c.endianness=configt::ansi_ct::endiannesst::NO_ENDIANNESS;
710  ansi_c.lib=configt::ansi_ct::libt::LIB_NONE;
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")
719  ansi_c.set_arch_spec_alpha();
720  else if(arch=="arm64" ||
721  arch=="armel" ||
722  arch=="armhf" ||
723  arch=="arm")
724  ansi_c.set_arch_spec_arm(arch);
725  else if(arch=="mips64el" ||
726  arch=="mipsn32el" ||
727  arch=="mipsel" ||
728  arch=="mips64" ||
729  arch=="mipsn32" ||
730  arch=="mips")
731  ansi_c.set_arch_spec_mips(arch);
732  else if(arch=="powerpc" ||
733  arch=="ppc64" ||
734  arch=="ppc64le")
735  ansi_c.set_arch_spec_power(arch);
736  else if(arch == "riscv64")
737  ansi_c.set_arch_spec_riscv64();
738  else if(arch=="sparc" ||
739  arch=="sparc64")
740  ansi_c.set_arch_spec_sparc(arch);
741  else if(arch=="ia64")
742  ansi_c.set_arch_spec_ia64();
743  else if(arch=="s390x")
744  ansi_c.set_arch_spec_s390x();
745  else if(arch=="s390")
746  ansi_c.set_arch_spec_s390();
747  else if(arch=="x32")
748  ansi_c.set_arch_spec_x32();
749  else if(arch=="v850")
750  ansi_c.set_arch_spec_v850();
751  else if(arch=="hppa")
752  ansi_c.set_arch_spec_hppa();
753  else if(arch=="sh4")
754  ansi_c.set_arch_spec_sh4();
755  else if(arch=="x86_64")
756  ansi_c.set_arch_spec_x86_64();
757  else if(arch=="i386")
758  ansi_c.set_arch_spec_i386();
759  else
760  {
761  // We run on something new and unknown.
762  // We verify for i386 instead.
763  ansi_c.set_arch_spec_i386();
764  ansi_c.arch="i386";
765  }
766 }
767 
775 configt::bv_encodingt parse_object_bits_encoding(
776  const std::string &argument,
777  const std::size_t pointer_width)
778 {
779  const auto throw_for_reason = [&](const std::string &reason) {
780  throw invalid_command_line_argument_exceptiont(
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 
792  configt::bv_encodingt bv_encoding;
793  bv_encoding.object_bits = *object_bits;
794  bv_encoding.is_object_bits_default = false;
795  return bv_encoding;
796 }
797 
798 bool configt::set(const cmdlinet &cmdline)
799 {
800  // defaults -- we match the architecture we have ourselves
801 
802  cpp.cpp_standard=cppt::default_cpp_standard();
803 
804  ansi_c.single_precision_constant=false;
805  ansi_c.for_has_scope=true; // C99 or later
806  ansi_c.ts_18661_3_Floatn_types=false;
807  ansi_c.c_standard=ansi_ct::default_c_standard();
808  ansi_c.endianness=ansi_ct::endiannesst::NO_ENDIANNESS;
809  ansi_c.os=ansi_ct::ost::NO_OS;
810  ansi_c.arch="none";
811  ansi_c.lib=configt::ansi_ct::libt::LIB_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.
820  ansi_c.rounding_mode=ieee_floatt::ROUND_TO_EVEN;
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
865  irep_idt this_os=this_operating_system();
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
909  ansi_c.lib=configt::ansi_ct::libt::LIB_FULL;
910  ansi_c.os=configt::ansi_ct::ost::OS_WIN;
911 
912  if(cmdline.isset("gcc"))
913  {
914  // There are gcc versions that target Windows (MinGW for example),
915  // and we support that.
916  ansi_c.preprocessor=ansi_ct::preprocessort::GCC;
917  ansi_c.mode=ansi_ct::flavourt::GCC;
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
935  ansi_c.preprocessor=ansi_ct::preprocessort::VISUAL_STUDIO;
936  ansi_c.mode=ansi_ct::flavourt::VISUAL_STUDIO;
937  #elif __FreeBSD__
938  ansi_c.preprocessor=ansi_ct::preprocessort::CLANG;
939  ansi_c.mode=ansi_ct::flavourt::VISUAL_STUDIO;
940  #else
941  ansi_c.preprocessor=ansi_ct::preprocessort::GCC;
942  ansi_c.mode=ansi_ct::flavourt::VISUAL_STUDIO;
943  #endif
944 
945  cpp.cpp_standard = cppt::cpp_standardt::CPP14;
946  }
947  }
948  else if(os=="macos")
949  {
950  ansi_c.lib=configt::ansi_ct::libt::LIB_FULL;
951  ansi_c.os=configt::ansi_ct::ost::OS_MACOS;
952  ansi_c.mode = ansi_ct::flavourt::CLANG;
953  ansi_c.preprocessor=ansi_ct::preprocessort::CLANG;
954  }
955  else if(os=="linux" || os=="solaris")
956  {
957  ansi_c.lib=configt::ansi_ct::libt::LIB_FULL;
958  ansi_c.os=configt::ansi_ct::ost::OS_LINUX;
959  ansi_c.mode=ansi_ct::flavourt::GCC;
960  ansi_c.preprocessor=ansi_ct::preprocessort::GCC;
961  }
962  else if(os=="freebsd")
963  {
964  ansi_c.lib=configt::ansi_ct::libt::LIB_FULL;
965  ansi_c.os=configt::ansi_ct::ost::OS_LINUX;
966  ansi_c.mode=ansi_ct::flavourt::CLANG;
967  ansi_c.preprocessor=ansi_ct::preprocessort::CLANG;
968  }
969  else
970  {
971  // give up, but use reasonable defaults
972  ansi_c.lib=configt::ansi_ct::libt::LIB_FULL;
973  ansi_c.os=configt::ansi_ct::ost::OS_LINUX;
974  ansi_c.mode=ansi_ct::flavourt::GCC;
975  ansi_c.preprocessor=ansi_ct::preprocessort::GCC;
976  }
977 
978  if(ansi_c.preprocessor == ansi_ct::preprocessort::GCC)
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;
992  ansi_c.wchar_t_is_unsigned=true;
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 == "x86_64" && cmdline.isset("gcc"))
997  ansi_c.long_double_width=16*8;
998  else
999  ansi_c.long_double_width=8*8;
1000  }
1001  else if(os == "macos" && arch == "arm64")
1002  {
1003  // https://developer.apple.com/documentation/xcode/
1004  // writing_arm64_code_for_apple_platforms#//apple_ref/doc/uid/TP40013702-SW1
1005  ansi_c.char_is_unsigned = false;
1006  ansi_c.long_double_width = 8 * 8;
1007  }
1008 
1009  // Let's check some of the type widths in case we run
1010  // the same architecture and OS that we are verifying for.
1011  if(arch==this_arch && os==this_os)
1012  {
1013  INVARIANT(
1014  ansi_c.int_width == sizeof(int) * CHAR_BIT,
1015  "int width shall be equal to the system int width");
1016  INVARIANT(
1017  ansi_c.long_int_width == sizeof(long) * CHAR_BIT,
1018  "long int width shall be equal to the system long int width");
1019  INVARIANT(
1020  ansi_c.bool_width == sizeof(bool) * CHAR_BIT,
1021  "bool width shall be equal to the system bool width");
1022  INVARIANT(
1023  ansi_c.char_width == sizeof(char) * CHAR_BIT,
1024  "char width shall be equal to the system char width");
1025  INVARIANT(
1026  ansi_c.short_int_width == sizeof(short) * CHAR_BIT,
1027  "short int width shall be equal to the system short int width");
1028  INVARIANT(
1029  ansi_c.long_long_int_width == sizeof(long long) * CHAR_BIT,
1030  "long long int width shall be equal to the system long long int width");
1031  INVARIANT(
1032  ansi_c.pointer_width == sizeof(void *) * CHAR_BIT,
1033  "pointer width shall be equal to the system pointer width");
1034  INVARIANT(
1035  ansi_c.single_width == sizeof(float) * CHAR_BIT,
1036  "float width shall be equal to the system float width");
1037  INVARIANT(
1038  ansi_c.double_width == sizeof(double) * CHAR_BIT,
1039  "double width shall be equal to the system double width");
1040  INVARIANT(
1041  ansi_c.char_is_unsigned ==
1042  (static_cast<char>((1 << CHAR_BIT) - 1) == (1 << CHAR_BIT) - 1),
1043  "char_is_unsigned flag shall indicate system char unsignedness");
1044 
1045 #ifndef _WIN32
1046  // On Windows, long double width varies by compiler
1047  INVARIANT(
1048  ansi_c.long_double_width == sizeof(long double) * CHAR_BIT,
1049  "long double width shall be equal to the system long double width");
1050 #endif
1051  }
1052 
1053  // the following allows overriding the defaults
1054 
1055  if(cmdline.isset("16"))
1056  ansi_c.set_16();
1057 
1058  if(cmdline.isset("32"))
1059  ansi_c.set_32();
1060 
1061  if(cmdline.isset("64"))
1062  ansi_c.set_64();
1063 
1064  if(cmdline.isset("LP64"))
1065  ansi_c.set_LP64(); // int=32, long=64, pointer=64
1066 
1067  if(cmdline.isset("ILP64"))
1068  ansi_c.set_ILP64(); // int=64, long=64, pointer=64
1069 
1070  if(cmdline.isset("LLP64"))
1071  ansi_c.set_LLP64(); // int=32, long=32, pointer=64
1072 
1073  if(cmdline.isset("ILP32"))
1074  ansi_c.set_ILP32(); // int=32, long=32, pointer=32
1075 
1076  if(cmdline.isset("LP32"))
1077  ansi_c.set_LP32(); // int=16, long=32, pointer=32
1078 
1079  if(cmdline.isset("string-abstraction"))
1080  ansi_c.string_abstraction=true;
1081  else
1082  ansi_c.string_abstraction=false;
1083 
1084  if(cmdline.isset("no-library"))
1085  ansi_c.lib=configt::ansi_ct::libt::LIB_NONE;
1086 
1087  if(cmdline.isset("little-endian"))
1088  ansi_c.endianness=configt::ansi_ct::endiannesst::IS_LITTLE_ENDIAN;
1089 
1090  if(cmdline.isset("big-endian"))
1091  ansi_c.endianness=configt::ansi_ct::endiannesst::IS_BIG_ENDIAN;
1092 
1093  if(cmdline.isset("little-endian") &&
1094  cmdline.isset("big-endian"))
1095  return true;
1096 
1097  if(cmdline.isset("unsigned-char"))
1098  ansi_c.char_is_unsigned=true;
1099 
1100  if(cmdline.isset("round-to-even") ||
1101  cmdline.isset("round-to-nearest"))
1102  ansi_c.rounding_mode=ieee_floatt::ROUND_TO_EVEN;
1103 
1104  if(cmdline.isset("round-to-plus-inf"))
1105  ansi_c.rounding_mode=ieee_floatt::ROUND_TO_PLUS_INF;
1106 
1107  if(cmdline.isset("round-to-minus-inf"))
1108  ansi_c.rounding_mode=ieee_floatt::ROUND_TO_MINUS_INF;
1109 
1110  if(cmdline.isset("round-to-zero"))
1111  ansi_c.rounding_mode=ieee_floatt::ROUND_TO_ZERO;
1112 
1113  if(cmdline.isset("object-bits"))
1114  {
1115  bv_encoding = parse_object_bits_encoding(
1116  cmdline.get_value("object-bits"), ansi_c.pointer_width);
1117  }
1118 
1119  if(cmdline.isset("malloc-fail-assert") && cmdline.isset("malloc-fail-null"))
1120  {
1121  throw invalid_command_line_argument_exceptiont{
1122  "at most one malloc failure mode is acceptable", "--malloc-fail-null"};
1123  }
1124  if(cmdline.isset("malloc-fail-null"))
1125  ansi_c.malloc_failure_mode = ansi_c.malloc_failure_mode_return_null;
1126  if(cmdline.isset("malloc-fail-assert"))
1127  ansi_c.malloc_failure_mode = ansi_c.malloc_failure_mode_assert_then_assume;
1128 
1129  ansi_c.malloc_may_fail = cmdline.isset("malloc-may-fail");
1130 
1131  if(cmdline.isset("c89"))
1132  ansi_c.set_c89();
1133 
1134  if(cmdline.isset("c99"))
1135  ansi_c.set_c99();
1136 
1137  if(cmdline.isset("c11"))
1138  ansi_c.set_c11();
1139 
1140  if(cmdline.isset("cpp98"))
1141  cpp.set_cpp98();
1142 
1143  if(cmdline.isset("cpp03"))
1144  cpp.set_cpp03();
1145 
1146  if(cmdline.isset("cpp11"))
1147  cpp.set_cpp11();
1148 
1149  // set the upper bound for argc
1150  if(os == "windows")
1151  {
1152  // On Windows, CreateProcess accepts no more than 32767 characters, so make
1153  // that a hard limit.
1154  ansi_c.max_argc = mp_integer{32767};
1155  }
1156  else
1157  {
1158  // For other systems assume argc is no larger than the what would make argv
1159  // consume all available memory space:
1160  // 2^pointer_width / (pointer_width / char_width) is the maximum number of
1161  // argv elements sysconf(ARG_MAX) is likely much lower than this, but we
1162  // don't know that value for the verification target platform.
1163  const auto pointer_bits_2log =
1164  address_bits(ansi_c.pointer_width / ansi_c.char_width);
1165  if(ansi_c.pointer_width - pointer_bits_2log <= ansi_c.int_width)
1166  {
1167  ansi_c.max_argc = power(2, config.ansi_c.int_width - pointer_bits_2log);
1168  }
1169  // otherwise we leave argc unconstrained
1170  }
1171 
1172  return false;
1173 }
1174 
1175 std::string configt::ansi_ct::os_to_string(ost os)
1176 {
1177  // clang-format off
1178  switch(os)
1179  {
1180  case ost::OS_LINUX: return "linux";
1181  case ost::OS_MACOS: return "macos";
1182  case ost::OS_WIN: return "win";
1183  case ost::NO_OS: return "none";
1184  }
1185  // clang-format on
1186 
1187  UNREACHABLE;
1188 }
1189 
1190 configt::ansi_ct::ost configt::ansi_ct::string_to_os(const std::string &os)
1191 {
1192  if(os=="linux")
1193  return ost::OS_LINUX;
1194  else if(os=="macos")
1195  return ost::OS_MACOS;
1196  else if(os=="win")
1197  return ost::OS_WIN;
1198  else
1199  return ost::NO_OS;
1200 }
1201 
1202 static irep_idt string_from_ns(
1203  const namespacet &ns,
1204  const std::string &what)
1205 {
1206  const irep_idt id=CPROVER_PREFIX "architecture_"+what;
1207  const symbolt *symbol;
1208 
1209  const bool not_found = ns.lookup(id, symbol);
1210  INVARIANT(!not_found, id2string(id) + " must be in namespace");
1211 
1212  const exprt &tmp=symbol->value;
1213 
1214  INVARIANT(
1215  tmp.id() == ID_address_of &&
1216  to_address_of_expr(tmp).object().id() == ID_index &&
1217  to_index_expr(to_address_of_expr(tmp).object()).array().id() ==
1218  ID_string_constant,
1219  "symbol table configuration entry '" + id2string(id) +
1220  "' must be a string constant");
1221 
1222  return to_index_expr(to_address_of_expr(tmp).object()).array().get(ID_value);
1223 }
1224 
1225 static unsigned unsigned_from_ns(
1226  const namespacet &ns,
1227  const std::string &what)
1228 {
1229  const irep_idt id=CPROVER_PREFIX "architecture_"+what;
1230  const symbolt *symbol;
1231 
1232  const bool not_found = ns.lookup(id, symbol);
1233  INVARIANT(!not_found, id2string(id) + " must be in namespace");
1234 
1235  exprt tmp=symbol->value;
1236  simplify(tmp, ns);
1237 
1238  INVARIANT(
1239  tmp.id() == ID_constant,
1240  "symbol table configuration entry '" + id2string(id) +
1241  "' must be a constant");
1242 
1243  mp_integer int_value;
1244 
1245  const bool error = to_integer(to_constant_expr(tmp), int_value);
1246  INVARIANT(
1247  !error,
1248  "symbol table configuration entry '" + id2string(id) +
1249  "' must be convertible to mp_integer");
1250 
1251  return numeric_cast_v<unsigned>(int_value);
1252 }
1253 
1254 void configt::set_from_symbol_table(
1255  const symbol_tablet &symbol_table)
1256 {
1257  // maybe not compiled from C/C++
1258  if(symbol_table.symbols.find(CPROVER_PREFIX "architecture_" "int_width")==
1259  symbol_table.symbols.end())
1260  return;
1261 
1262  namespacet ns(symbol_table);
1263 
1264  // clear defines
1265  ansi_c.defines.clear();
1266 
1267  // first set architecture to get some defaults
1268  if(symbol_table.symbols.find(CPROVER_PREFIX "architecture_" "arch")==
1269  symbol_table.symbols.end())
1270  set_arch(id2string(this_architecture()));
1271  else
1272  set_arch(string_from_ns(ns, "arch"));
1273 
1274  ansi_c.int_width=unsigned_from_ns(ns, "int_width");
1275  ansi_c.long_int_width=unsigned_from_ns(ns, "long_int_width");
1276  ansi_c.bool_width=1*8;
1277  ansi_c.char_width=unsigned_from_ns(ns, "char_width");
1278  ansi_c.short_int_width=unsigned_from_ns(ns, "short_int_width");
1279  ansi_c.long_long_int_width=unsigned_from_ns(ns, "long_long_int_width");
1280  ansi_c.pointer_width=unsigned_from_ns(ns, "pointer_width");
1281  ansi_c.single_width=unsigned_from_ns(ns, "single_width");
1282  ansi_c.double_width=unsigned_from_ns(ns, "double_width");
1283  ansi_c.long_double_width=unsigned_from_ns(ns, "long_double_width");
1284  ansi_c.wchar_t_width=unsigned_from_ns(ns, "wchar_t_width");
1285 
1286  ansi_c.char_is_unsigned=unsigned_from_ns(ns, "char_is_unsigned")!=0;
1287  ansi_c.wchar_t_is_unsigned=unsigned_from_ns(ns, "wchar_t_is_unsigned")!=0;
1288  // for_has_scope, single_precision_constant, rounding_mode,
1289  // ts_18661_3_Floatn_types are not architectural features,
1290  // and thus not stored in namespace
1291 
1292  ansi_c.alignment=unsigned_from_ns(ns, "alignment");
1293 
1294  ansi_c.memory_operand_size=unsigned_from_ns(ns, "memory_operand_size");
1295 
1296  ansi_c.endianness=(ansi_ct::endiannesst)unsigned_from_ns(ns, "endianness");
1297 
1298  if(symbol_table.symbols.find(CPROVER_PREFIX "architecture_" "os")==
1299  symbol_table.symbols.end())
1300  ansi_c.os=ansi_ct::string_to_os(id2string(this_operating_system()));
1301  else
1302  ansi_c.os=ansi_ct::string_to_os(id2string(string_from_ns(ns, "os")));
1303 
1304  ansi_c.NULL_is_zero = unsigned_from_ns(ns, "NULL_is_zero") != 0;
1305 
1306  // mode, preprocessor (and all preprocessor command line options),
1307  // lib, string_abstraction not stored in namespace
1308 
1309  set_object_bits_from_symbol_table(symbol_table);
1310 }
1311 
1314 void configt::set_object_bits_from_symbol_table(
1315  const symbol_tablet &symbol_table)
1316 {
1317  // has been overridden by command line option,
1318  // thus do not apply language defaults
1319  if(!bv_encoding.is_object_bits_default)
1320  return;
1321 
1322  // set object_bits according to entry point language
1323  if(const auto maybe_symbol=symbol_table.lookup(CPROVER_PREFIX "_start"))
1324  {
1325  const symbolt &entry_point_symbol=*maybe_symbol;
1326 
1327  if(entry_point_symbol.mode==ID_java)
1328  bv_encoding.object_bits=java.default_object_bits;
1329  else if(entry_point_symbol.mode==ID_C)
1330  bv_encoding.object_bits=ansi_c.default_object_bits;
1331  else if(entry_point_symbol.mode==ID_cpp)
1332  bv_encoding.object_bits=cpp.default_object_bits;
1333  DATA_INVARIANT(
1334  0<bv_encoding.object_bits && bv_encoding.object_bits<ansi_c.pointer_width,
1335  "object_bits should fit into pointer width");
1336  }
1337 }
1338 
1339 std::string configt::object_bits_info()
1340 {
1341  return "Running with "+std::to_string(bv_encoding.object_bits)+
1342  " object bits, "+
1343  std::to_string(ansi_c.pointer_width-bv_encoding.object_bits)+
1344  " offset bits ("+
1345  (bv_encoding.is_object_bits_default ? "default" : "user-specified")+
1346  ")";
1347 }
1348 
1349 // clang-format off
1350 irep_idt configt::this_architecture()
1351 {
1352  irep_idt this_arch;
1353 
1354  // following http://wiki.debian.org/ArchitectureSpecificsMemo
1355 
1356  #ifdef __alpha__
1357  this_arch = "alpha";
1358  #elif defined(__armel__)
1359  this_arch = "armel";
1360  #elif defined(__aarch64__)
1361  this_arch = "arm64";
1362  #elif defined(__arm__)
1363  #ifdef __ARM_PCS_VFP
1364  this_arch = "armhf"; // variant of arm with hard float
1365  #else
1366  this_arch = "arm";
1367  #endif
1368  #elif defined(__mipsel__)
1369  #if _MIPS_SIM==_ABIO32
1370  this_arch = "mipsel";
1371  #elif _MIPS_SIM==_ABIN32
1372  this_arch = "mipsn32el";
1373  #else
1374  this_arch = "mips64el";
1375  #endif
1376  #elif defined(__mips__)
1377  #if _MIPS_SIM==_ABIO32
1378  this_arch = "mips";
1379  #elif _MIPS_SIM==_ABIN32
1380  this_arch = "mipsn32";
1381  #else
1382  this_arch = "mips64";
1383  #endif
1384  #elif defined(__powerpc__)
1385  #if defined(__ppc64__) || defined(__PPC64__) || \
1386  defined(__powerpc64__) || defined(__POWERPC64__)
1387  #ifdef __LITTLE_ENDIAN__
1388  this_arch = "ppc64le";
1389  #else
1390  this_arch = "ppc64";
1391  #endif
1392  #else
1393  this_arch = "powerpc";
1394  #endif
1395  #elif defined(__riscv)
1396  this_arch = "riscv64";
1397  #elif defined(__sparc__)
1398  #ifdef __arch64__
1399  this_arch = "sparc64";
1400  #else
1401  this_arch = "sparc";
1402  #endif
1403  #elif defined(__ia64__)
1404  this_arch = "ia64";
1405  #elif defined(__s390x__)
1406  this_arch = "s390x";
1407  #elif defined(__s390__)
1408  this_arch = "s390";
1409  #elif defined(__x86_64__)
1410  #ifdef __ILP32__
1411  this_arch = "x32"; // variant of x86_64 with 32-bit pointers
1412  #else
1413  this_arch = "x86_64";
1414  #endif
1415  #elif defined(__i386__)
1416  this_arch = "i386";
1417  #elif defined(_WIN64)
1418  this_arch = "x86_64";
1419  #elif defined(_WIN32)
1420  this_arch = "i386";
1421  #elif defined(__hppa__)
1422  this_arch = "hppa";
1423  #elif defined(__sh__)
1424  this_arch = "sh4";
1425  #else
1426  // something new and unknown!
1427  this_arch = "unknown";
1428  #endif
1429 
1430  return this_arch;
1431 }
1432 // clang-format on
1433 
1434 void configt::set_classpath(const std::string &cp)
1435 {
1436 // These are separated by colons on Unix, and semicolons on
1437 // Windows.
1438 #ifdef _WIN32
1439  const char cp_separator = ';';
1440 #else
1441  const char cp_separator = ':';
1442 #endif
1443 
1444  std::vector<std::string> class_path =
1445  split_string(cp, cp_separator);
1446  java.classpath.insert(
1447  java.classpath.end(), class_path.begin(), class_path.end());
1448 }
1449 
1450 irep_idt configt::this_operating_system()
1451 {
1452  irep_idt this_os;
1453 
1454  #ifdef _WIN32
1455  this_os="windows";
1456  #elif __APPLE__
1457  this_os="macos";
1458  #elif __FreeBSD__
1459  this_os="freebsd";
1460  #elif __linux__
1461  this_os="linux";
1462  #elif __SVR4
1463  this_os="solaris";
1464  #else
1465  this_os="unknown";
1466  #endif
1467 
1468  return this_os;
1469 }
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
exception_utils.h
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:36
configt::ansi_ct::ts_18661_3_Floatn_types
bool ts_18661_3_Floatn_types
Definition: config.h:139
configt::bv_encodingt::object_bits
std::size_t object_bits
Definition: config.h:336
configt::ansi_ct::defines
std::list< std::string > defines
Definition: config.h:250
configt::ansi_ct::bool_width
std::size_t bool_width
Definition: config.h:126
configt::object_bits_info
std::string object_bits_info()
Definition: config.cpp:1339
configt::ansi_ct::set_c99
void set_c99()
Definition: config.h:155
symbol_tablet
The symbol table.
Definition: symbol_table.h:13
configt::ansi_ct::NULL_is_zero
bool NULL_is_zero
Definition: config.h:209
configt::javat::main_class
irep_idt main_class
Definition: config.h:328
mp_integer
BigInt mp_integer
Definition: smt_terms.h:17
configt::ansi_ct::string_to_os
static ost string_to_os(const std::string &)
Definition: config.cpp:1190
configt::ansi_ct::ost
ost
Definition: config.h:194
configt::bv_encoding
struct configt::bv_encodingt bv_encoding
arith_tools.h
cmdlinet::isset
virtual bool isset(char option) const
Definition: cmdline.cpp:30
configt::ansi_ct::for_has_scope
bool for_has_scope
Definition: config.h:138
configt::cppt::cpp_standardt
cpp_standardt
Definition: config.h:285
configt::ansi_ct::set_arch_spec_s390x
void set_arch_spec_s390x()
Definition: config.cpp:458
configt::ansi_ct::wchar_t_width
std::size_t wchar_t_width
Definition: config.h:134
configt::ansi_ct::endiannesst
endiannesst
Definition: config.h:186
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:253
configt::ansi_ct::malloc_failure_mode_assert_then_assume
@ malloc_failure_mode_assert_then_assume
Definition: config.h:270
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1478
configt::ansi_ct::set_arch_spec_mips
void set_arch_spec_mips(const irep_idt &subarch)
Definition: config.cpp:353
configt::ansi_ct::os
ost os
Definition: config.h:201
configt::ansi_ct::flavourt::VISUAL_STUDIO
@ VISUAL_STUDIO
configt::ansi_ct::set_32
void set_32()
Definition: config.cpp:32
configt::ansi_ct::set_64
void set_64()
Definition: config.cpp:37
configt::main
optionalt< std::string > main
Definition: config.h:341
configt::ansi_ct::set_arch_spec_i386
void set_arch_spec_i386()
Definition: config.cpp:150
configt::ansi_ct::set_16
void set_16()
Definition: config.cpp:27
exprt
Base class for all expressions.
Definition: expr.h:55
configt::ansi_ct::rounding_mode
ieee_floatt::rounding_modet rounding_mode
Definition: config.h:166
configt::ansi_ct::alignment
std::size_t alignment
Definition: config.h:180
to_integer
bool to_integer(const constant_exprt &expr, mp_integer &int_value)
Convert a constant expression expr to an arbitrary-precision integer.
Definition: arith_tools.cpp:20
configt::ansi_ct::set_LP32
void set_LP32()
int=16, long=32, pointer=32
Definition: config.cpp:131
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:58
configt::ansi_ct::set_arch_spec_power
void set_arch_spec_power(const irep_idt &subarch)
Definition: config.cpp:220
configt::ansi_c
struct configt::ansi_ct ansi_c
namespace.h
configt::ansi_ct::set_arch_spec_hppa
void set_arch_spec_hppa()
Definition: config.cpp:616
configt::javat::classpath
classpatht classpath
Definition: config.h:327
configt::ansi_ct::libt::LIB_NONE
@ LIB_NONE
configt::ansi_ct::flavourt::CLANG
@ CLANG
configt
Globally accessible architectural configuration.
Definition: config.h:118
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
irept::get
const irep_idt & get(const irep_idt &name) const
Definition: irep.cpp:45
configt::ansi_ct::char_width
std::size_t char_width
Definition: config.h:127
address_bits
std::size_t address_bits(const mp_integer &size)
ceil(log2(size))
Definition: arith_tools.cpp:177
configt::cppt::set_cpp98
void set_cpp98()
Definition: config.h:295
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:90
configt::ansi_ct::endiannesst::NO_ENDIANNESS
@ NO_ENDIANNESS
configt::ansi_ct::set_arch_spec_ia64
void set_arch_spec_ia64()
Definition: config.cpp:526
string2int.h
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
split_string
void split_string(const std::string &s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)
Definition: string_utils.cpp:39
configt::ansi_ct::endiannesst::IS_LITTLE_ENDIAN
@ IS_LITTLE_ENDIAN
configt::bv_encodingt
Definition: config.h:333
cmdlinet
Definition: cmdline.h:20
symbolt::mode
irep_idt mode
Language mode.
Definition: symbol.h:49
configt::ansi_ct::set_arch_spec_arm
void set_arch_spec_arm(const irep_idt &subarch)
Definition: config.cpp:281
unsigned_from_ns
static unsigned unsigned_from_ns(const namespacet &ns, const std::string &what)
Definition: config.cpp:1225
configt::ansi_ct::wchar_t_is_unsigned
bool wchar_t_is_unsigned
Definition: config.h:137
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:510
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
configt::ansi_ct::set_arch_spec_s390
void set_arch_spec_s390()
Definition: config.cpp:429
configt::ansi_ct::double_width
std::size_t double_width
Definition: config.h:132
configt::ansi_ct::preprocessor
preprocessort preprocessor
Definition: config.h:248
configt::ansi_ct::malloc_failure_mode_return_null
@ malloc_failure_mode_return_null
Definition: config.h:269
configt::ansi_ct::set_arch_spec_riscv64
void set_arch_spec_riscv64()
Definition: config.cpp:403
configt::ansi_ct::default_object_bits
static const std::size_t default_object_bits
Definition: config.h:275
configt::cppt::default_object_bits
static const std::size_t default_object_bits
Definition: config.h:316
configt::ansi_ct::string_abstraction
bool string_abstraction
Definition: config.h:263
configt::ansi_ct::set_arch_spec_alpha
void set_arch_spec_alpha()
Definition: config.cpp:324
pointer_expr.h
configt::bv_encodingt::is_object_bits_default
bool is_object_bits_default
Definition: config.h:337
configt::cppt::set_cpp11
void set_cpp11()
Definition: config.h:303
configt::ansi_ct::memory_operand_size
std::size_t memory_operand_size
Definition: config.h:184
cmdlinet::get_value
std::string get_value(char option) const
Definition: cmdline.cpp:48
configt::ansi_ct::ost::OS_LINUX
@ OS_LINUX
configt::ansi_ct::max_argc
optionalt< mp_integer > max_argc
Maximum value of argc, which is operating-systems dependent: Windows limits the number of characters ...
Definition: config.h:280
simplify
bool simplify(exprt &expr, const namespacet &ns)
Definition: simplify_expr.cpp:2926
configt::ansi_ct::long_long_int_width
std::size_t long_long_int_width
Definition: config.h:129
configt::ansi_ct::set_ILP64
void set_ILP64()
int=64, long=64, pointer=64
Definition: config.cpp:71
alignment
mp_integer alignment(const typet &type, const namespacet &ns)
Definition: padding.cpp:23
configt::this_operating_system
static irep_idt this_operating_system()
Definition: config.cpp:1450
index_exprt::array
exprt & array()
Definition: std_expr.h:1440
configt::ansi_ct::arch
irep_idt arch
Definition: config.h:206
configt::ansi_ct::ost::OS_WIN
@ OS_WIN
irept::id
const irep_idt & id() const
Definition: irep.h:396
configt::ansi_ct::set_LLP64
void set_LLP64()
int=32, long=32, pointer=64
Definition: config.cpp:91
configt::set_from_symbol_table
void set_from_symbol_table(const symbol_tablet &)
Definition: config.cpp:1254
configt::ansi_ct::os_to_string
static std::string os_to_string(ost)
Definition: config.cpp:1175
cprover_prefix.h
configt::javat::default_object_bits
static const std::size_t default_object_bits
Definition: config.h:330
configt::ansi_ct::include_files
std::list< std::string > include_files
Definition: config.h:254
configt::ansi_ct::ost::NO_OS
@ NO_OS
configt::ansi_ct::preprocessort::GCC
@ GCC
configt::ansi_ct::default_c_standard
static c_standardt default_c_standard()
Definition: config.cpp:675
configt::ansi_ct::set_ILP32
void set_ILP32()
int=32, long=32, pointer=32
Definition: config.cpp:111
config
configt config
Definition: config.cpp:25
simplify_expr.h
configt::ansi_ct::set_c11
void set_c11()
Definition: config.h:160
configt::this_architecture
static irep_idt this_architecture()
Definition: config.cpp:1350
configt::ansi_ct::libt::LIB_FULL
@ LIB_FULL
configt::ansi_ct::mode
flavourt mode
Definition: config.h:237
symbolt::value
exprt value
Initial value of symbol.
Definition: symbol.h:34
configt::ansi_ct::set_c89
void set_c89()
Definition: config.h:150
configt::ansi_ct::preprocessort::VISUAL_STUDIO
@ VISUAL_STUDIO
ieee_floatt::ROUND_TO_PLUS_INF
@ ROUND_TO_PLUS_INF
Definition: ieee_float.h:126
configt::ansi_ct::endiannesst::IS_BIG_ENDIAN
@ IS_BIG_ENDIAN
ieee_floatt::ROUND_TO_EVEN
@ ROUND_TO_EVEN
Definition: ieee_float.h:125
string_from_ns
static irep_idt string_from_ns(const namespacet &ns, const std::string &what)
Definition: config.cpp:1202
cmdline.h
symbolt
Symbol table entry.
Definition: symbol.h:27
configt::set
bool set(const cmdlinet &cmdline)
Definition: config.cpp:798
configt::cppt::default_cpp_standard
static cpp_standardt default_cpp_standard()
Definition: config.cpp:690
configt::ansi_ct::c_standard
enum configt::ansi_ct::c_standardt c_standard
configt::ansi_ct::set_arch_spec_sparc
void set_arch_spec_sparc(const irep_idt &subarch)
Definition: config.cpp:486
symbol_table_baset::symbols
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Definition: symbol_table_base.h:30
configt::ansi_ct::set_LP64
void set_LP64()
int=32, long=64, pointer=64
Definition: config.cpp:47
configt::ansi_ct::set_arch_spec_sh4
void set_arch_spec_sh4()
Definition: config.cpp:645
configt::ansi_ct::long_double_width
std::size_t long_double_width
Definition: config.h:133
CPROVER_PREFIX
#define CPROVER_PREFIX
Definition: cprover_prefix.h:14
power
mp_integer power(const mp_integer &base, const mp_integer &exponent)
A multi-precision implementation of the power operator.
Definition: arith_tools.cpp:195
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:128
configt::ansi_ct::char_is_unsigned
bool char_is_unsigned
Definition: config.h:137
configt::ansi_ct::flavourt::GCC
@ GCC
symbol_table_baset::lookup
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Definition: symbol_table_base.h:95
configt::ansi_ct::set_arch_spec_x86_64
void set_arch_spec_x86_64()
Definition: config.cpp:182
to_address_of_expr
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:408
configt::ansi_ct::set_arch_spec_x32
void set_arch_spec_x32()
Definition: config.cpp:557
configt::ansi_ct::malloc_failure_mode
malloc_failure_modet malloc_failure_mode
Definition: config.h:273
configt::ansi_ct::pointer_width
std::size_t pointer_width
Definition: config.h:130
configt::ansi_ct::single_width
std::size_t single_width
Definition: config.h:131
configt::ansi_ct::lib
libt lib
Definition: config.h:261
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:1434
configt::ansi_ct::malloc_may_fail
bool malloc_may_fail
Definition: config.h:264
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:50
configt::ansi_ct::single_precision_constant
bool single_precision_constant
Definition: config.h:141
cmdlinet::get_values
const std::list< std::string > & get_values(const std::string &option) const
Definition: cmdline.cpp:109
configt::ansi_ct::gcc__float128_type
bool gcc__float128_type
Definition: config.h:140
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:1314
configt::ansi_ct::c_standardt
c_standardt
Definition: config.h:142
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:124
ieee_floatt::ROUND_TO_MINUS_INF
@ ROUND_TO_MINUS_INF
Definition: ieee_float.h:125
configt::ansi_ct::endianness
endiannesst endianness
Definition: config.h:192
ieee_floatt::ROUND_TO_ZERO
@ ROUND_TO_ZERO
Definition: ieee_float.h:126
configt::ansi_ct::long_int_width
std::size_t long_int_width
Definition: config.h:125
validation_modet::INVARIANT
@ INVARIANT
configt::cppt::cpp_standard
enum configt::cppt::cpp_standardt cpp_standard
configt::cppt::set_cpp03
void set_cpp03()
Definition: config.h:299
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2992