cprover
config.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "config.h"
10 
11 #include <cstdlib>
12 
13 #include "arith_tools.h"
14 #include "cmdline.h"
15 #include "cprover_prefix.h"
16 #include "exception_utils.h"
17 #include "namespace.h"
18 #include "simplify_expr.h"
19 #include "std_expr.h"
20 #include "string2int.h"
21 #include "string_utils.h"
22 #include "symbol_table.h"
23 
25 
27 {
28  set_LP32();
29 }
30 
32 {
33  set_ILP32();
34 }
35 
37 {
38  #ifdef _WIN32
39  set_LLP64();
40  #else
41  set_LP64();
42  #endif
43 }
44 
47 {
48  bool_width=1*8;
49  int_width=4*8;
50  long_int_width=8*8;
51  char_width=1*8;
52  short_int_width=2*8;
53  long_long_int_width=8*8;
54  pointer_width=8*8;
55  single_width=4*8;
56  double_width=8*8;
57  long_double_width=16*8;
58  char_is_unsigned=false;
59  wchar_t_is_unsigned=false;
60  wchar_t_width=4*8;
61  alignment=1;
62  memory_operand_size=int_width/8;
63 }
64 
66 // TODO: find the alignment restrictions (per type) of the different
67 // architectures (currently: sizeof=alignedof)
68 // TODO: implement the __attribute__((__aligned__(val)))
69 
71 {
72  bool_width=1*8;
73  int_width=8*8;
74  long_int_width=8*8;
75  char_width=1*8;
76  short_int_width=2*8;
77  long_long_int_width=8*8;
78  pointer_width=8*8;
79  single_width=4*8;
80  double_width=8*8;
81  long_double_width=8*8;
82  char_is_unsigned=false;
83  wchar_t_is_unsigned=false;
84  wchar_t_width=4*8;
85  alignment=1;
86  memory_operand_size=int_width/8;
87 }
88 
91 {
92  bool_width=1*8;
93  int_width=4*8;
94  long_int_width=4*8;
95  char_width=1*8;
96  short_int_width=2*8;
97  long_long_int_width=8*8;
98  pointer_width=8*8;
99  single_width=4*8;
100  double_width=8*8;
101  long_double_width=8*8;
102  char_is_unsigned=false;
103  wchar_t_is_unsigned=false;
104  wchar_t_width=4*8;
105  alignment=1;
106  memory_operand_size=int_width/8;
107 }
108 
111 {
112  bool_width=1*8;
113  int_width=4*8;
114  long_int_width=4*8;
115  char_width=1*8;
116  short_int_width=2*8;
117  long_long_int_width=8*8;
118  pointer_width=4*8;
119  single_width=4*8;
120  double_width=8*8;
121  long_double_width=12*8; // really 96 bits on GCC
122  char_is_unsigned=false;
123  wchar_t_is_unsigned=false;
124  wchar_t_width=4*8;
125  alignment=1;
126  memory_operand_size=int_width/8;
127 }
128 
131 {
132  bool_width=1*8;
133  int_width=2*8;
134  long_int_width=4*8;
135  char_width=1*8;
136  short_int_width=2*8;
137  long_long_int_width=8*8;
138  pointer_width=4*8;
139  single_width=4*8;
140  double_width=8*8;
141  long_double_width=8*8;
142  char_is_unsigned=false;
143  wchar_t_is_unsigned=false;
144  wchar_t_width=4*8;
145  alignment=1;
146  memory_operand_size=int_width/8;
147 }
148 
150 {
151  set_ILP32();
152  endianness=endiannesst::IS_LITTLE_ENDIAN;
153  char_is_unsigned=false;
154  NULL_is_zero=true;
155 
156  switch(mode)
157  {
158  case flavourt::GCC:
159  case flavourt::CLANG:
160  defines.push_back("i386");
161  defines.push_back("__i386");
162  defines.push_back("__i386__");
163  if(mode == flavourt::CLANG)
164  defines.push_back("__LITTLE_ENDIAN__");
165  break;
166 
167  case flavourt::VISUAL_STUDIO:
168  defines.push_back("_M_IX86");
169  break;
170 
171  case flavourt::CODEWARRIOR:
172  case flavourt::ARM:
173  case flavourt::ANSI:
174  break;
175 
176  case flavourt::NONE:
177  UNREACHABLE;
178  }
179 }
180 
182 {
183  set_LP64();
184  endianness=endiannesst::IS_LITTLE_ENDIAN;
185  long_double_width=16*8;
186  char_is_unsigned=false;
187  NULL_is_zero=true;
188 
189  switch(mode)
190  {
191  case flavourt::GCC:
192  case flavourt::CLANG:
193  defines.push_back("__LP64__");
194  defines.push_back("__x86_64");
195  defines.push_back("__x86_64__");
196  defines.push_back("_LP64");
197  defines.push_back("__amd64__");
198  defines.push_back("__amd64");
199 
200  if(os == ost::OS_MACOS)
201  defines.push_back("__LITTLE_ENDIAN__");
202  break;
203 
204  case flavourt::VISUAL_STUDIO:
205  defines.push_back("_M_X64");
206  defines.push_back("_M_AMD64");
207  break;
208 
209  case flavourt::CODEWARRIOR:
210  case flavourt::ARM:
211  case flavourt::ANSI:
212  break;
213 
214  case flavourt::NONE:
215  UNREACHABLE;
216  }
217 }
218 
220 {
221  if(subarch=="powerpc")
222  set_ILP32();
223  else // ppc64 or ppc64le
224  set_LP64();
225 
226  if(subarch=="ppc64le")
227  endianness=endiannesst::IS_LITTLE_ENDIAN;
228  else
229  endianness=endiannesst::IS_BIG_ENDIAN;
230 
231  long_double_width=16*8;
232  char_is_unsigned=true;
233  NULL_is_zero=true;
234 
235  switch(mode)
236  {
237  case flavourt::GCC:
238  case flavourt::CLANG:
239  defines.push_back("__powerpc");
240  defines.push_back("__powerpc__");
241  defines.push_back("__POWERPC__");
242  defines.push_back("__ppc__");
243 
244  if(os == ost::OS_MACOS)
245  defines.push_back("__BIG_ENDIAN__");
246 
247  if(subarch!="powerpc")
248  {
249  defines.push_back("__powerpc64");
250  defines.push_back("__powerpc64__");
251  defines.push_back("__PPC64__");
252  defines.push_back("__ppc64__");
253  if(subarch=="ppc64le")
254  {
255  defines.push_back("_CALL_ELF=2");
256  defines.push_back("__LITTLE_ENDIAN__");
257  }
258  else
259  {
260  defines.push_back("_CALL_ELF=1");
261  defines.push_back("__BIG_ENDIAN__");
262  }
263  }
264  break;
265 
266  case flavourt::VISUAL_STUDIO:
267  defines.push_back("_M_PPC");
268  break;
269 
270  case flavourt::CODEWARRIOR:
271  case flavourt::ARM:
272  case flavourt::ANSI:
273  break;
274 
275  case flavourt::NONE:
276  UNREACHABLE;
277  }
278 }
279 
281 {
282  if(subarch=="arm64")
283  {
284  set_LP64();
285  long_double_width=16*8;
286  }
287  else
288  {
289  set_ILP32();
290  long_double_width=8*8;
291  }
292 
293  endianness=endiannesst::IS_LITTLE_ENDIAN;
294  char_is_unsigned=true;
295  NULL_is_zero=true;
296 
297  switch(mode)
298  {
299  case flavourt::GCC:
300  case flavourt::CLANG:
301  if(subarch=="arm64")
302  defines.push_back("__aarch64__");
303  else
304  defines.push_back("__arm__");
305  if(subarch=="armhf")
306  defines.push_back("__ARM_PCS_VFP");
307  break;
308 
309  case flavourt::VISUAL_STUDIO:
310  defines.push_back("_M_ARM");
311  break;
312 
313  case flavourt::CODEWARRIOR:
314  case flavourt::ARM:
315  case flavourt::ANSI:
316  break;
317 
318  case flavourt::NONE:
319  UNREACHABLE;
320  }
321 }
322 
324 {
325  set_LP64();
326  endianness=endiannesst::IS_LITTLE_ENDIAN;
327  long_double_width=16*8;
328  char_is_unsigned=false;
329  NULL_is_zero=true;
330 
331  switch(mode)
332  {
333  case flavourt::GCC:
334  defines.push_back("__alpha__");
335  break;
336 
337  case flavourt::VISUAL_STUDIO:
338  defines.push_back("_M_ALPHA");
339  break;
340 
341  case flavourt::CLANG:
342  case flavourt::CODEWARRIOR:
343  case flavourt::ARM:
344  case flavourt::ANSI:
345  break;
346 
347  case flavourt::NONE:
348  UNREACHABLE;
349  }
350 }
351 
353 {
354  if(subarch=="mipsel" ||
355  subarch=="mips" ||
356  subarch=="mipsn32el" ||
357  subarch=="mipsn32")
358  {
359  set_ILP32();
360  long_double_width=8*8;
361  }
362  else
363  {
364  set_LP64();
365  long_double_width=16*8;
366  }
367 
368  if(subarch=="mipsel" ||
369  subarch=="mipsn32el" ||
370  subarch=="mips64el")
371  endianness=endiannesst::IS_LITTLE_ENDIAN;
372  else
373  endianness=endiannesst::IS_BIG_ENDIAN;
374 
375  char_is_unsigned=false;
376  NULL_is_zero=true;
377 
378  switch(mode)
379  {
380  case flavourt::GCC:
381  defines.push_back("__mips__");
382  defines.push_back("mips");
383  defines.push_back(
384  "_MIPS_SZPTR="+std::to_string(config.ansi_c.pointer_width));
385  break;
386 
387  case flavourt::VISUAL_STUDIO:
388  UNREACHABLE; // not supported by Visual Studio
389  break;
390 
391  case flavourt::CLANG:
392  case flavourt::CODEWARRIOR:
393  case flavourt::ARM:
394  case flavourt::ANSI:
395  break;
396 
397  case flavourt::NONE:
398  UNREACHABLE;
399  }
400 }
401 
403 {
404  set_LP64();
405  endianness = endiannesst::IS_LITTLE_ENDIAN;
406  long_double_width = 16 * 8;
407  char_is_unsigned = true;
408  NULL_is_zero = true;
409 
410  switch(mode)
411  {
412  case flavourt::GCC:
413  defines.push_back("__riscv");
414  break;
415 
416  case flavourt::VISUAL_STUDIO:
417  case flavourt::CLANG:
418  case flavourt::CODEWARRIOR:
419  case flavourt::ARM:
420  case flavourt::ANSI:
421  break;
422 
423  case flavourt::NONE:
424  UNREACHABLE;
425  }
426 }
427 
429 {
430  set_ILP32();
431  endianness=endiannesst::IS_BIG_ENDIAN;
432  long_double_width=16*8;
433  char_is_unsigned=true;
434  NULL_is_zero=true;
435 
436  switch(mode)
437  {
438  case flavourt::GCC:
439  defines.push_back("__s390__");
440  break;
441 
442  case flavourt::VISUAL_STUDIO:
443  UNREACHABLE; // not supported by Visual Studio
444  break;
445 
446  case flavourt::CLANG:
447  case flavourt::CODEWARRIOR:
448  case flavourt::ARM:
449  case flavourt::ANSI:
450  break;
451 
452  case flavourt::NONE:
453  UNREACHABLE;
454  }
455 }
456 
458 {
459  set_LP64();
460  endianness=endiannesst::IS_BIG_ENDIAN;
461  char_is_unsigned=true;
462  NULL_is_zero=true;
463 
464  switch(mode)
465  {
466  case flavourt::GCC:
467  defines.push_back("__s390x__");
468  break;
469 
470  case flavourt::VISUAL_STUDIO:
471  UNREACHABLE; // not supported by Visual Studio
472  break;
473 
474  case flavourt::CLANG:
475  case flavourt::CODEWARRIOR:
476  case flavourt::ARM:
477  case flavourt::ANSI:
478  break;
479 
480  case flavourt::NONE:
481  UNREACHABLE;
482  }
483 }
484 
486 {
487  if(subarch=="sparc64")
488  {
489  set_LP64();
490  long_double_width=16*8;
491  }
492  else
493  {
494  set_ILP32();
495  long_double_width=16*8;
496  }
497 
498  endianness=endiannesst::IS_BIG_ENDIAN;
499  char_is_unsigned=false;
500  NULL_is_zero=true;
501 
502  switch(mode)
503  {
504  case flavourt::GCC:
505  defines.push_back("__sparc__");
506  if(subarch=="sparc64")
507  defines.push_back("__arch64__");
508  break;
509 
510  case flavourt::VISUAL_STUDIO:
511  UNREACHABLE; // not supported by Visual Studio
512  break;
513 
514  case flavourt::CLANG:
515  case flavourt::CODEWARRIOR:
516  case flavourt::ARM:
517  case flavourt::ANSI:
518  break;
519 
520  case flavourt::NONE:
521  UNREACHABLE;
522  }
523 }
524 
526 {
527  set_LP64();
528  long_double_width=16*8;
529  endianness=endiannesst::IS_LITTLE_ENDIAN;
530  char_is_unsigned=false;
531  NULL_is_zero=true;
532 
533  switch(mode)
534  {
535  case flavourt::GCC:
536  defines.push_back("__ia64__");
537  defines.push_back("_IA64");
538  defines.push_back("__IA64__");
539  break;
540 
541  case flavourt::VISUAL_STUDIO:
542  defines.push_back("_M_IA64");
543  break;
544 
545  case flavourt::CLANG:
546  case flavourt::CODEWARRIOR:
547  case flavourt::ARM:
548  case flavourt::ANSI:
549  break;
550 
551  case flavourt::NONE:
552  UNREACHABLE;
553  }
554 }
555 
557 {
558  // This is a variant of x86_64 that has
559  // 32-bit long int and 32-bit pointers.
560  set_ILP32();
561  long_double_width=16*8; // different from i386
562  endianness=endiannesst::IS_LITTLE_ENDIAN;
563  char_is_unsigned=false;
564  NULL_is_zero=true;
565 
566  switch(mode)
567  {
568  case flavourt::GCC:
569  defines.push_back("__ILP32__");
570  defines.push_back("__x86_64");
571  defines.push_back("__x86_64__");
572  defines.push_back("__amd64__");
573  defines.push_back("__amd64");
574  break;
575 
576  case flavourt::VISUAL_STUDIO:
577  UNREACHABLE; // not supported by Visual Studio
578  break;
579 
580  case flavourt::CLANG:
581  case flavourt::CODEWARRIOR:
582  case flavourt::ARM:
583  case flavourt::ANSI:
584  break;
585 
586  case flavourt::NONE:
587  UNREACHABLE;
588  }
589 }
590 
594 {
595  // The Renesas V850 is a 32-bit microprocessor used in
596  // many automotive applications. This spec is written from the
597  // architecture manual rather than having access to a running
598  // system. Thus some assumptions have been made.
599 
600  set_ILP32();
601 
602  // Technically, the V850's don't have floating-point at all.
603  // However, the RH850, aimed at automotive has both 32-bit and
604  // 64-bit IEEE-754 float.
605  double_width=8*8;
606  long_double_width=8*8;
607  endianness=endiannesst::IS_LITTLE_ENDIAN;
608 
609  // Without information about the compiler and RTOS, these are guesses
610  char_is_unsigned=false;
611  NULL_is_zero=true;
612 
613  // No preprocessor definitions due to lack of information
614 }
615 
617 {
618  set_ILP32();
619  long_double_width=8*8; // different from i386
620  endianness=endiannesst::IS_BIG_ENDIAN;
621  char_is_unsigned=false;
622  NULL_is_zero=true;
623 
624  switch(mode)
625  {
626  case flavourt::GCC:
627  defines.push_back("__hppa__");
628  break;
629 
630  case flavourt::VISUAL_STUDIO:
631  UNREACHABLE; // not supported by Visual Studio
632  break;
633 
634  case flavourt::CLANG:
635  case flavourt::CODEWARRIOR:
636  case flavourt::ARM:
637  case flavourt::ANSI:
638  break;
639 
640  case flavourt::NONE:
641  UNREACHABLE;
642  }
643 }
644 
646 {
647  set_ILP32();
648  long_double_width=8*8; // different from i386
649  endianness=endiannesst::IS_LITTLE_ENDIAN;
650  char_is_unsigned=false;
651  NULL_is_zero=true;
652 
653  switch(mode)
654  {
655  case flavourt::GCC:
656  defines.push_back("__sh__");
657  defines.push_back("__SH4__");
658  break;
659 
660  case flavourt::VISUAL_STUDIO:
661  UNREACHABLE; // not supported by Visual Studio
662  break;
663 
664  case flavourt::CLANG:
665  case flavourt::CODEWARRIOR:
666  case flavourt::ARM:
667  case flavourt::ANSI:
668  break;
669 
670  case flavourt::NONE:
671  UNREACHABLE;
672  }
673 }
674 
676 {
677  #if defined(__APPLE__)
678  // By default, clang on the Mac builds C code in GNU C11
679  return c_standardt::C11;
680  #elif defined(__FreeBSD__)
681  // By default, clang on FreeBSD builds C code in GNU C99
682  return c_standardt::C99;
683  #else
684  // By default, gcc 5.4 or higher use gnu11; older versions use gnu89
685  return c_standardt::C11;
686  #endif
687 }
688 
690 {
691  // g++ 6.3 uses gnu++14
692  // g++ 5.4 uses gnu++98
693  // clang 6.0 uses c++14
694  #if defined _WIN32
695  return cpp_standardt::CPP14;
696  #else
697  return cpp_standardt::CPP98;
698  #endif
699 }
700 
701 void configt::set_arch(const irep_idt &arch)
702 {
703  ansi_c.arch=arch;
704 
705  if(arch=="none")
706  {
707  // the architecture for people who can't commit
710  ansi_c.NULL_is_zero=false;
711 
712  if(sizeof(long int)==8)
713  ansi_c.set_64();
714  else
715  ansi_c.set_32();
716  }
717  else if(arch=="alpha")
719  else if(arch=="arm64" ||
720  arch=="armel" ||
721  arch=="armhf" ||
722  arch=="arm")
724  else if(arch=="mips64el" ||
725  arch=="mipsn32el" ||
726  arch=="mipsel" ||
727  arch=="mips64" ||
728  arch=="mipsn32" ||
729  arch=="mips")
731  else if(arch=="powerpc" ||
732  arch=="ppc64" ||
733  arch=="ppc64le")
735  else if(arch == "riscv64")
737  else if(arch=="sparc" ||
738  arch=="sparc64")
740  else if(arch=="ia64")
742  else if(arch=="s390x")
744  else if(arch=="s390")
746  else if(arch=="x32")
748  else if(arch=="v850")
750  else if(arch=="hppa")
752  else if(arch=="sh4")
754  else if(arch=="x86_64")
756  else if(arch=="i386")
758  else
759  {
760  // We run on something new and unknown.
761  // We verify for i386 instead.
763  ansi_c.arch="i386";
764  }
765 }
766 
767 bool configt::set(const cmdlinet &cmdline)
768 {
769  // defaults -- we match the architecture we have ourselves
770 
772 
774  // This will allow us to override by language defaults later.
776 
778  ansi_c.for_has_scope=true; // C99 or later
783  ansi_c.arch="none";
785  // NOLINTNEXTLINE(readability/casting)
786  ansi_c.NULL_is_zero=reinterpret_cast<size_t>(nullptr)==0;
787 
788  // Default is ROUND_TO_EVEN, justified by C99:
789  // 1 At program startup the floating-point environment is initialized as
790  // prescribed by IEC 60559:
791  // - All floating-point exception status flags are cleared.
792  // - The rounding direction mode is rounding to nearest.
794 
795  if(cmdline.isset("function"))
796  main=cmdline.get_value("function");
797 
798  if(cmdline.isset('D'))
799  ansi_c.defines=cmdline.get_values('D');
800 
801  if(cmdline.isset('I'))
802  ansi_c.include_paths=cmdline.get_values('I');
803 
804  if(cmdline.isset("classpath"))
805  {
806  // Specifying -classpath or -cp overrides any setting of the
807  // CLASSPATH environment variable.
808  set_classpath(cmdline.get_value("classpath"));
809  }
810  else if(cmdline.isset("cp"))
811  {
812  // Specifying -classpath or -cp overrides any setting of the
813  // CLASSPATH environment variable.
814  set_classpath(cmdline.get_value("cp"));
815  }
816  else
817  {
818  // environment variable set?
819  const char *CLASSPATH=getenv("CLASSPATH");
820  if(CLASSPATH!=nullptr)
821  set_classpath(CLASSPATH);
822  else
823  set_classpath("."); // default
824  }
825 
826  if(cmdline.isset("main-class"))
827  java.main_class=cmdline.get_value("main-class");
828 
829  if(cmdline.isset("include"))
830  ansi_c.include_files=cmdline.get_values("include");
831 
832  // the default architecture is the one we run on
833  irep_idt this_arch=this_architecture();
834  irep_idt arch=this_arch;
835 
836  // let's pick an OS now
837  // the default is the one we run on
839  irep_idt os=this_os;
840 
841  if(cmdline.isset("i386-linux"))
842  {
843  os="linux";
844  arch="i386";
845  }
846  else if(cmdline.isset("i386-win32") ||
847  cmdline.isset("win32"))
848  {
849  os="windows";
850  arch="i386";
851  }
852  else if(cmdline.isset("winx64"))
853  {
854  os="windows";
855  arch="x86_64";
856  }
857  else if(cmdline.isset("i386-macos"))
858  {
859  os="macos";
860  arch="i386";
861  }
862  else if(cmdline.isset("ppc-macos"))
863  {
864  arch="powerpc";
865  os="macos";
866  }
867 
868  if(cmdline.isset("arch"))
869  {
870  arch=cmdline.get_value("arch");
871  }
872 
873  if(cmdline.isset("os"))
874  {
875  os=cmdline.get_value("os");
876  }
877 
878  if(os=="windows")
879  {
880  // Cygwin uses GCC throughout, use i386-linux
881  // MinGW needs --win32 --gcc
884 
885  if(cmdline.isset("gcc"))
886  {
887  // There are gcc versions that target Windows (MinGW for example),
888  // and we support that.
891 
892  // enable Cygwin
893  #ifdef _WIN32
894  ansi_c.defines.push_back("__CYGWIN__");
895  #endif
896 
897  // MinGW has extra defines
898  ansi_c.defines.push_back("__int64=long long");
899  }
900  else
901  {
902  // On Windows, our default is Visual Studio.
903  // On FreeBSD, it's clang.
904  // On anything else, it's GCC as the preprocessor,
905  // but we recognize the Visual Studio language,
906  // which is somewhat inconsistent.
907  #ifdef _WIN32
910  #elif __FreeBSD__
913  #else
916  #endif
917  }
918  }
919  else if(os=="macos")
920  {
925  }
926  else if(os=="linux" || os=="solaris")
927  {
932  }
933  else if(os=="freebsd")
934  {
939  }
940  else
941  {
942  // give up, but use reasonable defaults
947  }
948 
950  ansi_c.Float128_type = true;
951 
952  set_arch(arch);
953 
954  if(os=="windows")
955  {
956  // note that sizeof(void *)==8, but sizeof(long)==4!
957  if(arch=="x86_64")
958  ansi_c.set_LLP64();
959 
960  // On Windows, wchar_t is unsigned 16 bit, regardless
961  // of the compiler used.
962  ansi_c.wchar_t_width=2*8;
964 
965  // long double is the same as double in Visual Studio,
966  // but it's 16 bytes with GCC with the 64-bit target.
967  if(arch=="x64_64" && cmdline.isset("gcc"))
969  else
971  }
972 
973  // Let's check some of the type widths in case we run
974  // the same architecture and OS that we are verifying for.
975  if(arch==this_arch && os==this_os)
976  {
977  INVARIANT(
978  ansi_c.int_width == sizeof(int) * 8,
979  "int width shall be equal to the system int width");
980  INVARIANT(
981  ansi_c.long_int_width == sizeof(long) * 8,
982  "long int width shall be equal to the system long int width");
983  INVARIANT(
984  ansi_c.bool_width == sizeof(bool) * 8,
985  "bool width shall be equal to the system bool width");
986  INVARIANT(
987  ansi_c.char_width == sizeof(char) * 8,
988  "char width shall be equal to the system char width");
989  INVARIANT(
990  ansi_c.short_int_width == sizeof(short) * 8,
991  "short int width shall be equal to the system short int width");
992  INVARIANT(
993  ansi_c.long_long_int_width == sizeof(long long) * 8,
994  "long long int width shall be equal to the system long long int width");
995  INVARIANT(
996  ansi_c.pointer_width == sizeof(void *) * 8,
997  "pointer width shall be equal to the system pointer width");
998  INVARIANT(
999  ansi_c.single_width == sizeof(float) * 8,
1000  "float width shall be equal to the system float width");
1001  INVARIANT(
1002  ansi_c.double_width == sizeof(double) * 8,
1003  "double width shall be equal to the system double width");
1004  INVARIANT(
1005  ansi_c.char_is_unsigned == (static_cast<char>(255) == 255),
1006  "char_is_unsigned flag shall indicate system char unsignedness");
1007 
1008  #ifndef _WIN32
1009  // On Windows, long double width varies by compiler
1010  INVARIANT(
1011  ansi_c.long_double_width == sizeof(long double) * 8,
1012  "long double width shall be equal to the system long double width");
1013  #endif
1014  }
1015 
1016  // the following allows overriding the defaults
1017 
1018  if(cmdline.isset("16"))
1019  ansi_c.set_16();
1020 
1021  if(cmdline.isset("32"))
1022  ansi_c.set_32();
1023 
1024  if(cmdline.isset("64"))
1025  ansi_c.set_64();
1026 
1027  if(cmdline.isset("LP64"))
1028  ansi_c.set_LP64(); // int=32, long=64, pointer=64
1029 
1030  if(cmdline.isset("ILP64"))
1031  ansi_c.set_ILP64(); // int=64, long=64, pointer=64
1032 
1033  if(cmdline.isset("LLP64"))
1034  ansi_c.set_LLP64(); // int=32, long=32, pointer=64
1035 
1036  if(cmdline.isset("ILP32"))
1037  ansi_c.set_ILP32(); // int=32, long=32, pointer=32
1038 
1039  if(cmdline.isset("LP32"))
1040  ansi_c.set_LP32(); // int=16, long=32, pointer=32
1041 
1042  if(cmdline.isset("string-abstraction"))
1044  else
1045  ansi_c.string_abstraction=false;
1046 
1047  if(cmdline.isset("no-library"))
1049 
1050  if(cmdline.isset("little-endian"))
1052 
1053  if(cmdline.isset("big-endian"))
1055 
1056  if(cmdline.isset("little-endian") &&
1057  cmdline.isset("big-endian"))
1058  return true;
1059 
1060  if(cmdline.isset("unsigned-char"))
1061  ansi_c.char_is_unsigned=true;
1062 
1063  if(cmdline.isset("round-to-even") ||
1064  cmdline.isset("round-to-nearest"))
1066 
1067  if(cmdline.isset("round-to-plus-inf"))
1069 
1070  if(cmdline.isset("round-to-minus-inf"))
1072 
1073  if(cmdline.isset("round-to-zero"))
1075 
1076  if(cmdline.isset("object-bits"))
1077  {
1079  unsafe_string2unsigned(cmdline.get_value("object-bits"));
1080 
1081  if(!(0<bv_encoding.object_bits &&
1083  {
1085  "object-bits must be positive and less than the pointer width (" +
1087  "--object_bits");
1088  }
1089 
1091  }
1092 
1093  return false;
1094 }
1095 
1097 {
1098  switch(os)
1099  {
1100  case ost::OS_LINUX: return "linux";
1101  case ost::OS_MACOS: return "macos";
1102  case ost::OS_WIN: return "win";
1103  default: return "none";
1104  }
1105 }
1106 
1108 {
1109  if(os=="linux")
1110  return ost::OS_LINUX;
1111  else if(os=="macos")
1112  return ost::OS_MACOS;
1113  else if(os=="win")
1114  return ost::OS_WIN;
1115  else
1116  return ost::NO_OS;
1117 }
1118 
1120  const namespacet &ns,
1121  const std::string &what)
1122 {
1123  const irep_idt id=CPROVER_PREFIX "architecture_"+what;
1124  const symbolt *symbol;
1125 
1126  const bool not_found = ns.lookup(id, symbol);
1127  INVARIANT(!not_found, id2string(id) + " must be in namespace");
1128 
1129  const exprt &tmp=symbol->value;
1130 
1131  INVARIANT(
1132  tmp.id() == ID_address_of &&
1133  to_address_of_expr(tmp).object().id() == ID_index &&
1134  to_index_expr(to_address_of_expr(tmp).object()).array().id() ==
1135  ID_string_constant,
1136  "symbol table configuration entry `" + id2string(id) +
1137  "' must be a string constant");
1138 
1139  return to_index_expr(to_address_of_expr(tmp).object()).array().get(ID_value);
1140 }
1141 
1142 static unsigned unsigned_from_ns(
1143  const namespacet &ns,
1144  const std::string &what)
1145 {
1146  const irep_idt id=CPROVER_PREFIX "architecture_"+what;
1147  const symbolt *symbol;
1148 
1149  const bool not_found = ns.lookup(id, symbol);
1150  INVARIANT(!not_found, id2string(id) + " must be in namespace");
1151 
1152  exprt tmp=symbol->value;
1153  simplify(tmp, ns);
1154 
1155  INVARIANT(
1156  tmp.id() == ID_constant,
1157  "symbol table configuration entry `" + id2string(id) +
1158  "' must be a constant");
1159 
1160  mp_integer int_value;
1161 
1162  const bool error = to_integer(to_constant_expr(tmp), int_value);
1163  INVARIANT(
1164  !error,
1165  "symbol table configuration entry `" + id2string(id) +
1166  "' must be convertible to mp_integer");
1167 
1168  return numeric_cast_v<unsigned>(int_value);
1169 }
1170 
1172  const symbol_tablet &symbol_table)
1173 {
1174  // maybe not compiled from C/C++
1175  if(symbol_table.symbols.find(CPROVER_PREFIX "architecture_" "int_width")==
1176  symbol_table.symbols.end())
1177  return;
1178 
1179  namespacet ns(symbol_table);
1180 
1181  // clear defines
1182  ansi_c.defines.clear();
1183 
1184  // first set architecture to get some defaults
1185  if(symbol_table.symbols.find(CPROVER_PREFIX "architecture_" "arch")==
1186  symbol_table.symbols.end())
1188  else
1189  set_arch(string_from_ns(ns, "arch"));
1190 
1191  ansi_c.int_width=unsigned_from_ns(ns, "int_width");
1192  ansi_c.long_int_width=unsigned_from_ns(ns, "long_int_width");
1193  ansi_c.bool_width=1*8;
1194  ansi_c.char_width=unsigned_from_ns(ns, "char_width");
1195  ansi_c.short_int_width=unsigned_from_ns(ns, "short_int_width");
1196  ansi_c.long_long_int_width=unsigned_from_ns(ns, "long_long_int_width");
1197  ansi_c.pointer_width=unsigned_from_ns(ns, "pointer_width");
1198  ansi_c.single_width=unsigned_from_ns(ns, "single_width");
1199  ansi_c.double_width=unsigned_from_ns(ns, "double_width");
1200  ansi_c.long_double_width=unsigned_from_ns(ns, "long_double_width");
1201  ansi_c.wchar_t_width=unsigned_from_ns(ns, "wchar_t_width");
1202 
1203  ansi_c.char_is_unsigned=unsigned_from_ns(ns, "char_is_unsigned")!=0;
1204  ansi_c.wchar_t_is_unsigned=unsigned_from_ns(ns, "wchar_t_is_unsigned")!=0;
1205  // for_has_scope, single_precision_constant, rounding_mode,
1206  // ts_18661_3_Floatn_types are not architectural features,
1207  // and thus not stored in namespace
1208 
1209  ansi_c.alignment=unsigned_from_ns(ns, "alignment");
1210 
1211  ansi_c.memory_operand_size=unsigned_from_ns(ns, "memory_operand_size");
1212 
1214 
1215  if(symbol_table.symbols.find(CPROVER_PREFIX "architecture_" "os")==
1216  symbol_table.symbols.end())
1218  else
1220 
1221  // NULL_is_zero=from_ns("NULL_is_zero");
1222  ansi_c.NULL_is_zero=true;
1223 
1224  // mode, preprocessor (and all preprocessor command line options),
1225  // lib, string_abstraction not stored in namespace
1226 
1227  set_object_bits_from_symbol_table(symbol_table);
1228 }
1229 
1233  const symbol_tablet &symbol_table)
1234 {
1235  // has been overridden by command line option,
1236  // thus do not apply language defaults
1238  return;
1239 
1240  // set object_bits according to entry point language
1241  if(const auto maybe_symbol=symbol_table.lookup(CPROVER_PREFIX "_start"))
1242  {
1243  const symbolt &entry_point_symbol=*maybe_symbol;
1244 
1245  if(entry_point_symbol.mode==ID_java)
1247  else if(entry_point_symbol.mode==ID_C)
1249  else if(entry_point_symbol.mode==ID_cpp)
1253  "object_bits should fit into pointer width");
1254  }
1255 }
1256 
1258 {
1259  return "Running with "+std::to_string(bv_encoding.object_bits)+
1260  " object bits, "+
1262  " offset bits ("+
1263  (bv_encoding.is_object_bits_default ? "default" : "user-specified")+
1264  ")";
1265 }
1266 
1267 // clang-format off
1269 {
1270  irep_idt this_arch;
1271 
1272  // following http://wiki.debian.org/ArchitectureSpecificsMemo
1273 
1274  #ifdef __alpha__
1275  this_arch = "alpha";
1276  #elif defined(__armel__)
1277  this_arch = "armel";
1278  #elif defined(__aarch64__)
1279  this_arch = "arm64";
1280  #elif defined(__arm__)
1281  #ifdef __ARM_PCS_VFP
1282  this_arch = "armhf"; // variant of arm with hard float
1283  #else
1284  this_arch = "arm";
1285  #endif
1286  #elif defined(__mipsel__)
1287  #if _MIPS_SIM==_ABIO32
1288  this_arch = "mipsel";
1289  #elif _MIPS_SIM==_ABIN32
1290  this_arch = "mipsn32el";
1291  #else
1292  this_arch = "mips64el";
1293  #endif
1294  #elif defined(__mips__)
1295  #if _MIPS_SIM==_ABIO32
1296  this_arch = "mips";
1297  #elif _MIPS_SIM==_ABIN32
1298  this_arch = "mipsn32";
1299  #else
1300  this_arch = "mips64";
1301  #endif
1302  #elif defined(__powerpc__)
1303  #if defined(__ppc64__) || defined(__PPC64__) || \
1304  defined(__powerpc64__) || defined(__POWERPC64__)
1305  #ifdef __LITTLE_ENDIAN__
1306  this_arch = "ppc64le";
1307  #else
1308  this_arch = "ppc64";
1309  #endif
1310  #else
1311  this_arch = "powerpc";
1312  #endif
1313  #elif defined(__riscv)
1314  this_arch = "riscv64";
1315  #elif defined(__sparc__)
1316  #ifdef __arch64__
1317  this_arch = "sparc64";
1318  #else
1319  this_arch = "sparc";
1320  #endif
1321  #elif defined(__ia64__)
1322  this_arch = "ia64";
1323  #elif defined(__s390x__)
1324  this_arch = "s390x";
1325  #elif defined(__s390__)
1326  this_arch = "s390";
1327  #elif defined(__x86_64__)
1328  #ifdef __ILP32__
1329  this_arch = "x32"; // variant of x86_64 with 32-bit pointers
1330  #else
1331  this_arch = "x86_64";
1332  #endif
1333  #elif defined(__i386__)
1334  this_arch = "i386";
1335  #elif defined(_WIN64)
1336  this_arch = "x86_64";
1337  #elif defined(_WIN32)
1338  this_arch = "i386";
1339  #elif defined(__hppa__)
1340  this_arch = "hppa";
1341  #elif defined(__sh__)
1342  this_arch = "sh4";
1343  #else
1344  // something new and unknown!
1345  this_arch = "unknown";
1346  #endif
1347 
1348  return this_arch;
1349 }
1350 // clang-format on
1351 
1352 void configt::set_classpath(const std::string &cp)
1353 {
1354 // These are separated by colons on Unix, and semicolons on
1355 // Windows.
1356 #ifdef _WIN32
1357  const char cp_separator = ';';
1358 #else
1359  const char cp_separator = ':';
1360 #endif
1361 
1362  std::vector<std::string> class_path =
1363  split_string(cp, cp_separator);
1364  java.classpath.insert(
1365  java.classpath.end(), class_path.begin(), class_path.end());
1366 }
1367 
1369 {
1370  irep_idt this_os;
1371 
1372  #ifdef _WIN32
1373  this_os="windows";
1374  #elif __APPLE__
1375  this_os="macos";
1376  #elif __FreeBSD__
1377  this_os="freebsd";
1378  #elif __linux__
1379  this_os="linux";
1380  #elif __SVR4
1381  this_os="solaris";
1382  #else
1383  this_os="unknown";
1384  #endif
1385 
1386  return this_os;
1387 }
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:35
configt::ansi_ct::ts_18661_3_Floatn_types
bool ts_18661_3_Floatn_types
Definition: config.h:45
configt::bv_encodingt::object_bits
std::size_t object_bits
Definition: config.h:165
configt::ansi_ct::defines
std::list< std::string > defines
Definition: config.h:121
configt::ansi_ct::bool_width
std::size_t bool_width
Definition: config.h:32
configt::object_bits_info
std::string object_bits_info()
Definition: config.cpp:1257
symbol_tablet
The symbol table.
Definition: symbol_table.h:19
configt::ansi_ct::NULL_is_zero
bool NULL_is_zero
Definition: config.h:87
configt::java
struct configt::javat java
configt::javat::main_class
irep_idt main_class
Definition: config.h:157
to_integer
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:19
configt::ansi_ct::string_to_os
static ost string_to_os(const std::string &)
Definition: config.cpp:1107
configt::ansi_ct::ost
ost
Definition: config.h:78
arith_tools.h
cmdlinet::isset
virtual bool isset(char option) const
Definition: cmdline.cpp:27
configt::ansi_ct::for_has_scope
bool for_has_scope
Definition: config.h:44
address_of_exprt::object
exprt & object()
Definition: std_expr.h:3265
configt::cppt::cpp_standardt
cpp_standardt
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:485
configt::ansi_ct::set_arch_spec_s390x
void set_arch_spec_s390x()
Definition: config.cpp:457
configt::ansi_ct::wchar_t_width
std::size_t wchar_t_width
Definition: config.h:40
configt::ansi_ct::endiannesst
endiannesst
Definition: config.h:75
configt::ansi_ct::ost::OS_MACOS
string_utils.h
configt::ansi_ct::preprocessort::CLANG
configt::ansi_ct::include_paths
std::list< std::string > include_paths
Definition: config.h:124
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1648
configt::ansi_ct::set_arch_spec_mips
void set_arch_spec_mips(const irep_idt &subarch)
Definition: config.cpp:352
mp_integer
BigInt mp_integer
Definition: mp_arith.h:22
configt::main
std::string main
Definition: config.h:172
configt::ansi_ct::os
ost os
Definition: config.h:79
configt::ansi_ct::flavourt::VISUAL_STUDIO
configt::ansi_ct::set_32
void set_32()
Definition: config.cpp:31
configt::ansi_ct::set_64
void set_64()
Definition: config.cpp:36
configt::ansi_ct::set_arch_spec_i386
void set_arch_spec_i386()
Definition: config.cpp:149
configt::ansi_ct::set_16
void set_16()
Definition: config.cpp:26
exprt
Base class for all expressions.
Definition: expr.h:54
configt::ansi_ct::rounding_mode
ieee_floatt::rounding_modet rounding_mode
Definition: config.h:55
configt::ansi_ct::alignment
std::size_t alignment
Definition: config.h:69
configt::ansi_c
struct configt::ansi_ct ansi_c
configt::ansi_ct::set_LP32
void set_LP32()
int=16, long=32, pointer=32
Definition: config.cpp:130
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:53
configt::ansi_ct::set_arch_spec_power
void set_arch_spec_power(const irep_idt &subarch)
Definition: config.cpp:219
namespace.h
configt::ansi_ct::set_arch_spec_hppa
void set_arch_spec_hppa()
Definition: config.cpp:616
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:478
configt::javat::classpath
classpatht classpath
Definition: config.h:156
configt::ansi_ct::libt::LIB_NONE
configt::ansi_ct::flavourt::CLANG
configt
Globally accessible architectural configuration.
Definition: config.h:24
configt::cppt::cpp_standard
enum configt::cppt::cpp_standardt cpp_standard
configt::ansi_ct::char_width
std::size_t char_width
Definition: config.h:33
configt::bv_encoding
struct configt::bv_encodingt bv_encoding
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
configt::ansi_ct::endiannesst::NO_ENDIANNESS
configt::ansi_ct::set_arch_spec_ia64
void set_arch_spec_ia64()
Definition: config.cpp:525
string2int.h
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:166
split_string
void split_string(const std::string &s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)
Given a string s, split into a sequence of substrings when separated by specified delimiter.
Definition: string_utils.cpp:49
configt::ansi_ct::endiannesst::IS_LITTLE_ENDIAN
cmdlinet
Definition: cmdline.h:19
symbolt::mode
irep_idt mode
Language mode.
Definition: symbol.h:49
configt::ansi_ct::set_arch_spec_arm
void set_arch_spec_arm(const irep_idt &subarch)
Definition: config.cpp:280
unsigned_from_ns
static unsigned unsigned_from_ns(const namespacet &ns, const std::string &what)
Definition: config.cpp:1142
configt::ansi_ct::wchar_t_is_unsigned
bool wchar_t_is_unsigned
Definition: config.h:43
to_address_of_expr
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: std_expr.h:3282
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
configt::ansi_ct::set_arch_spec_s390
void set_arch_spec_s390()
Definition: config.cpp:428
configt::ansi_ct::double_width
std::size_t double_width
Definition: config.h:38
configt::ansi_ct::preprocessor
preprocessort preprocessor
Definition: config.h:119
configt::ansi_ct::set_arch_spec_riscv64
void set_arch_spec_riscv64()
Definition: config.cpp:402
configt::ansi_ct::default_object_bits
static const std::size_t default_object_bits
Definition: config.h:132
configt::cppt::default_object_bits
static const std::size_t default_object_bits
Definition: config.h:145
configt::ansi_ct::Float128_type
bool Float128_type
Definition: config.h:46
configt::ansi_ct::string_abstraction
bool string_abstraction
Definition: config.h:130
configt::ansi_ct::set_arch_spec_alpha
void set_arch_spec_alpha()
Definition: config.cpp:323
configt::bv_encodingt::is_object_bits_default
bool is_object_bits_default
Definition: config.h:166
configt::ansi_ct::memory_operand_size
std::size_t memory_operand_size
Definition: config.h:73
cmdlinet::get_value
std::string get_value(char option) const
Definition: cmdline.cpp:45
configt::ansi_ct::ost::OS_LINUX
simplify
bool simplify(exprt &expr, const namespacet &ns)
Definition: simplify_expr.cpp:2320
configt::ansi_ct::long_long_int_width
std::size_t long_long_int_width
Definition: config.h:35
configt::ansi_ct::set_ILP64
void set_ILP64()
int=64, long=64, pointer=64
Definition: config.cpp:70
alignment
mp_integer alignment(const typet &type, const namespacet &ns)
Definition: padding.cpp:21
configt::this_operating_system
static irep_idt this_operating_system()
Definition: config.cpp:1368
index_exprt::array
exprt & array()
Definition: std_expr.h:1621
configt::ansi_ct::arch
irep_idt arch
Definition: config.h:84
configt::ansi_ct::ost::OS_WIN
irept::id
const irep_idt & id() const
Definition: irep.h:259
configt::ansi_ct::set_LLP64
void set_LLP64()
int=32, long=32, pointer=64
Definition: config.cpp:90
configt::set_from_symbol_table
void set_from_symbol_table(const symbol_tablet &)
Definition: config.cpp:1171
configt::ansi_ct::os_to_string
static std::string os_to_string(ost)
Definition: config.cpp:1096
cprover_prefix.h
configt::javat::default_object_bits
static const std::size_t default_object_bits
Definition: config.h:159
configt::ansi_ct::include_files
std::list< std::string > include_files
Definition: config.h:125
configt::ansi_ct::ost::NO_OS
configt::ansi_ct::preprocessort::GCC
configt::ansi_ct::default_c_standard
static c_standardt default_c_standard()
Definition: config.cpp:675
configt::ansi_ct::set_ILP32
void set_ILP32()
int=32, long=32, pointer=32
Definition: config.cpp:110
config
configt config
Definition: config.cpp:24
simplify_expr.h
configt::ansi_ct::c_standard
enum configt::ansi_ct::c_standardt c_standard
configt::this_architecture
static irep_idt this_architecture()
Definition: config.cpp:1268
configt::ansi_ct::libt::LIB_FULL
configt::ansi_ct::mode
flavourt mode
Definition: config.h:115
symbolt::value
exprt value
Initial value of symbol.
Definition: symbol.h:34
configt::ansi_ct::preprocessort::VISUAL_STUDIO
ieee_floatt::ROUND_TO_PLUS_INF
Definition: ieee_float.h:128
configt::ansi_ct::endiannesst::IS_BIG_ENDIAN
ieee_floatt::ROUND_TO_EVEN
Definition: ieee_float.h:127
string_from_ns
static irep_idt string_from_ns(const namespacet &ns, const std::string &what)
Definition: config.cpp:1119
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:212
cmdline.h
symbolt
Symbol table entry.
Definition: symbol.h:27
configt::set
bool set(const cmdlinet &cmdline)
Definition: config.cpp:767
configt::cppt::default_cpp_standard
static cpp_standardt default_cpp_standard()
Definition: config.cpp:689
configt::ansi_ct::set_arch_spec_sparc
void set_arch_spec_sparc(const irep_idt &subarch)
Definition: config.cpp:485
symbol_table_baset::symbols
const symbolst & symbols
Definition: symbol_table_base.h:27
configt::ansi_ct::set_LP64
void set_LP64()
int=32, long=64, pointer=64
Definition: config.cpp:46
configt::ansi_ct::set_arch_spec_sh4
void set_arch_spec_sh4()
Definition: config.cpp:645
configt::ansi_ct::long_double_width
std::size_t long_double_width
Definition: config.h:39
CPROVER_PREFIX
#define CPROVER_PREFIX
Definition: cprover_prefix.h:14
unsafe_string2unsigned
unsigned unsafe_string2unsigned(const std::string &str, int base)
Definition: string2int.cpp:69
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:34
configt::ansi_ct::char_is_unsigned
bool char_is_unsigned
Definition: config.h:43
configt::ansi_ct::flavourt::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:86
configt::ansi_ct::set_arch_spec_x86_64
void set_arch_spec_x86_64()
Definition: config.cpp:181
configt::ansi_ct::set_arch_spec_x32
void set_arch_spec_x32()
Definition: config.cpp:556
configt::ansi_ct::pointer_width
std::size_t pointer_width
Definition: config.h:36
configt::ansi_ct::single_width
std::size_t single_width
Definition: config.h:37
configt::cpp
struct configt::cppt cpp
configt::ansi_ct::lib
libt lib
Definition: config.h:128
symbol_table.h
Author: Diffblue Ltd.
configt::set_classpath
void set_classpath(const std::string &cp)
Definition: config.cpp:1352
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:37
configt::ansi_ct::single_precision_constant
bool single_precision_constant
Definition: config.h:47
configt::bv_encodingt::default_object_bits
static const std::size_t default_object_bits
Definition: config.h:168
cmdlinet::get_values
const std::list< std::string > & get_values(const std::string &option) const
Definition: cmdline.cpp:110
std_expr.h
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:1232
configt::ansi_ct::c_standardt
c_standardt
Definition: config.h:48
configt::set_arch
void set_arch(const irep_idt &)
Definition: config.cpp:701
configt::ansi_ct::int_width
std::size_t int_width
Definition: config.h:30
ieee_floatt::ROUND_TO_MINUS_INF
Definition: ieee_float.h:127
configt::ansi_ct::endianness
endiannesst endianness
Definition: config.h:76
ieee_floatt::ROUND_TO_ZERO
Definition: ieee_float.h:128
configt::ansi_ct::long_int_width
std::size_t long_int_width
Definition: config.h:31
validation_modet::INVARIANT
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:4423