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 "namespace.h"
14 #include "symbol_table.h"
15 #include "arith_tools.h"
16 #include "cmdline.h"
17 #include "simplify_expr.h"
18 #include "std_expr.h"
19 #include "cprover_prefix.h"
20 
22 
24 {
25  set_LP32();
26 }
27 
29 {
30  set_ILP32();
31 }
32 
34 {
35  #ifdef _WIN32
36  set_LLP64();
37  #else
38  set_LP64();
39  #endif
40 }
41 
44 {
45  bool_width=1*8;
46  int_width=4*8;
47  long_int_width=8*8;
48  char_width=1*8;
49  short_int_width=2*8;
51  pointer_width=8*8;
52  single_width=4*8;
53  double_width=8*8;
54  long_double_width=16*8;
55  char_is_unsigned=false;
56  wchar_t_is_unsigned=false;
57  wchar_t_width=4*8;
58  alignment=1;
60 }
61 
63 // TODO: find the alignment restrictions (per type) of the different
64 // architectures (currently: sizeof=alignedof)
65 // TODO: implement the __attribute__((__aligned__(val)))
66 
68 {
69  bool_width=1*8;
70  int_width=8*8;
71  long_int_width=8*8;
72  char_width=1*8;
73  short_int_width=2*8;
75  pointer_width=8*8;
76  single_width=4*8;
77  double_width=8*8;
79  char_is_unsigned=false;
80  wchar_t_is_unsigned=false;
81  wchar_t_width=4*8;
82  alignment=1;
84 }
85 
88 {
89  bool_width=1*8;
90  int_width=4*8;
91  long_int_width=4*8;
92  char_width=1*8;
93  short_int_width=2*8;
95  pointer_width=8*8;
96  single_width=4*8;
97  double_width=8*8;
99  char_is_unsigned=false;
100  wchar_t_is_unsigned=false;
101  wchar_t_width=4*8;
102  alignment=1;
104 }
105 
108 {
109  bool_width=1*8;
110  int_width=4*8;
111  long_int_width=4*8;
112  char_width=1*8;
113  short_int_width=2*8;
115  pointer_width=4*8;
116  single_width=4*8;
117  double_width=8*8;
118  long_double_width=12*8; // really 96 bits on GCC
119  char_is_unsigned=false;
120  wchar_t_is_unsigned=false;
121  wchar_t_width=4*8;
122  alignment=1;
124 }
125 
128 {
129  bool_width=1*8;
130  int_width=2*8;
131  long_int_width=4*8;
132  char_width=1*8;
133  short_int_width=2*8;
135  pointer_width=4*8;
136  single_width=4*8;
137  double_width=8*8;
138  long_double_width=8*8;
139  char_is_unsigned=false;
140  wchar_t_is_unsigned=false;
141  wchar_t_width=4*8;
142  alignment=1;
144 }
145 
147 {
148  set_ILP32();
150  char_is_unsigned=false;
151  NULL_is_zero=true;
152 
153  switch(mode)
154  {
155  case flavourt::GCC:
156  case flavourt::APPLE:
157  defines.push_back("i386");
158  defines.push_back("__i386");
159  defines.push_back("__i386__");
160  if(mode==flavourt::APPLE)
161  defines.push_back("__LITTLE_ENDIAN__");
162  break;
163 
165  defines.push_back("_M_IX86");
166  break;
167 
169  case flavourt::ARM:
170  case flavourt::ANSI:
171  break;
172 
173  case flavourt::NONE:
174  assert(false);
175  }
176 }
177 
179 {
180  set_LP64();
182  long_double_width=16*8;
183  char_is_unsigned=false;
184  NULL_is_zero=true;
185 
186  switch(mode)
187  {
188  case flavourt::GCC:
189  case flavourt::APPLE:
190  defines.push_back("__LP64__");
191  defines.push_back("__x86_64");
192  defines.push_back("__x86_64__");
193  defines.push_back("_LP64");
194  defines.push_back("__amd64__");
195  defines.push_back("__amd64");
196  if(mode==flavourt::APPLE)
197  defines.push_back("__LITTLE_ENDIAN__");
198  break;
199 
201  defines.push_back("_M_X64");
202  defines.push_back("_M_AMD64");
203  break;
204 
206  case flavourt::ARM:
207  case flavourt::ANSI:
208  break;
209 
210  case flavourt::NONE:
211  assert(false);
212  }
213 }
214 
216 {
217  if(subarch=="powerpc")
218  set_ILP32();
219  else // ppc64 or ppc64le
220  set_LP64();
221 
222  if(subarch=="ppc64le")
224  else
226 
227  long_double_width=16*8;
228  char_is_unsigned=true;
229  NULL_is_zero=true;
230 
231  switch(mode)
232  {
233  case flavourt::GCC:
234  case flavourt::APPLE:
235  defines.push_back("__powerpc");
236  defines.push_back("__powerpc__");
237  defines.push_back("__POWERPC__");
238  defines.push_back("__ppc__");
239 
240  if(mode==flavourt::APPLE)
241  defines.push_back("__BIG_ENDIAN__");
242 
243  if(subarch!="powerpc")
244  {
245  defines.push_back("__powerpc64");
246  defines.push_back("__powerpc64__");
247  defines.push_back("__PPC64__");
248  defines.push_back("__ppc64__");
249  if(subarch=="ppc64le")
250  {
251  defines.push_back("_CALL_ELF=2");
252  defines.push_back("__LITTLE_ENDIAN__");
253  }
254  else
255  {
256  defines.push_back("_CALL_ELF=1");
257  defines.push_back("__BIG_ENDIAN__");
258  }
259  }
260  break;
261 
263  defines.push_back("_M_PPC");
264  break;
265 
267  case flavourt::ARM:
268  case flavourt::ANSI:
269  break;
270 
271  case flavourt::NONE:
272  assert(false);
273  }
274 }
275 
277 {
278  if(subarch=="arm64")
279  {
280  set_LP64();
281  long_double_width=16*8;
282  }
283  else
284  {
285  set_ILP32();
286  long_double_width=8*8;
287  }
288 
290  char_is_unsigned=true;
291  NULL_is_zero=true;
292 
293  switch(mode)
294  {
295  case flavourt::GCC:
296  case flavourt::APPLE:
297  if(subarch=="arm64")
298  defines.push_back("__aarch64__");
299  else
300  defines.push_back("__arm__");
301  if(subarch=="armhf")
302  defines.push_back("__ARM_PCS_VFP");
303  break;
304 
306  defines.push_back("_M_ARM");
307  break;
308 
310  case flavourt::ARM:
311  case flavourt::ANSI:
312  break;
313 
314  case flavourt::NONE:
315  assert(false);
316  }
317 }
318 
320 {
321  set_LP64();
323  long_double_width=16*8;
324  char_is_unsigned=false;
325  NULL_is_zero=true;
326 
327  switch(mode)
328  {
329  case flavourt::GCC:
330  defines.push_back("__alpha__");
331  break;
332 
334  defines.push_back("_M_ALPHA");
335  break;
336 
337  case flavourt::APPLE:
339  case flavourt::ARM:
340  case flavourt::ANSI:
341  break;
342 
343  case flavourt::NONE:
344  assert(false);
345  }
346 }
347 
349 {
350  if(subarch=="mipsel" ||
351  subarch=="mips" ||
352  subarch=="mipsn32el" ||
353  subarch=="mipsn32")
354  {
355  set_ILP32();
356  long_double_width=8*8;
357  }
358  else
359  {
360  set_LP64();
361  long_double_width=16*8;
362  }
363 
364  if(subarch=="mipsel" ||
365  subarch=="mipsn32el" ||
366  subarch=="mips64el")
368  else
370 
371  char_is_unsigned=false;
372  NULL_is_zero=true;
373 
374  switch(mode)
375  {
376  case flavourt::GCC:
377  defines.push_back("__mips__");
378  defines.push_back("mips");
379  defines.push_back(
380  "_MIPS_SZPTR="+std::to_string(config.ansi_c.pointer_width));
381  break;
382 
384  assert(false); // not supported by Visual Studio
385  break;
386 
387  case flavourt::APPLE:
389  case flavourt::ARM:
390  case flavourt::ANSI:
391  break;
392 
393  case flavourt::NONE:
394  assert(false);
395  }
396 }
397 
399 {
400  set_ILP32();
402  long_double_width=16*8;
403  char_is_unsigned=true;
404  NULL_is_zero=true;
405 
406  switch(mode)
407  {
408  case flavourt::GCC:
409  defines.push_back("__s390__");
410  break;
411 
413  assert(false); // not supported by Visual Studio
414  break;
415 
416  case flavourt::APPLE:
418  case flavourt::ARM:
419  case flavourt::ANSI:
420  break;
421 
422  case flavourt::NONE:
423  assert(false);
424  }
425 }
426 
428 {
429  set_LP64();
431  char_is_unsigned=true;
432  NULL_is_zero=true;
433 
434  switch(mode)
435  {
436  case flavourt::GCC:
437  defines.push_back("__s390x__");
438  break;
439 
441  assert(false); // not supported by Visual Studio
442  break;
443 
444  case flavourt::APPLE:
446  case flavourt::ARM:
447  case flavourt::ANSI:
448  break;
449 
450  case flavourt::NONE:
451  assert(false);
452  }
453 }
454 
456 {
457  if(subarch=="sparc64")
458  {
459  set_LP64();
460  long_double_width=16*8;
461  }
462  else
463  {
464  set_ILP32();
465  long_double_width=16*8;
466  }
467 
469  char_is_unsigned=false;
470  NULL_is_zero=true;
471 
472  switch(mode)
473  {
474  case flavourt::GCC:
475  defines.push_back("__sparc__");
476  if(subarch=="sparc64")
477  defines.push_back("__arch64__");
478  break;
479 
481  assert(false); // not supported by Visual Studio
482  break;
483 
484  case flavourt::APPLE:
486  case flavourt::ARM:
487  case flavourt::ANSI:
488  break;
489 
490  case flavourt::NONE:
491  assert(false);
492  }
493 }
494 
496 {
497  set_LP64();
498  long_double_width=16*8;
500  char_is_unsigned=false;
501  NULL_is_zero=true;
502 
503  switch(mode)
504  {
505  case flavourt::GCC:
506  defines.push_back("__ia64__");
507  defines.push_back("_IA64");
508  defines.push_back("__IA64__");
509  break;
510 
512  defines.push_back("_M_IA64");
513  break;
514 
515  case flavourt::APPLE:
517  case flavourt::ARM:
518  case flavourt::ANSI:
519  break;
520 
521  case flavourt::NONE:
522  assert(false);
523  }
524 }
525 
527 {
528  // This is a variant of x86_64 that has
529  // 32-bit long int and 32-bit pointers.
530  set_ILP32();
531  long_double_width=16*8; // different from i386
533  char_is_unsigned=false;
534  NULL_is_zero=true;
535 
536  switch(mode)
537  {
538  case flavourt::GCC:
539  defines.push_back("__ILP32__");
540  defines.push_back("__x86_64");
541  defines.push_back("__x86_64__");
542  defines.push_back("__amd64__");
543  defines.push_back("__amd64");
544  break;
545 
547  assert(false); // not supported by Visual Studio
548  break;
549 
550  case flavourt::APPLE:
552  case flavourt::ARM:
553  case flavourt::ANSI:
554  break;
555 
556  case flavourt::NONE:
557  assert(false);
558  }
559 }
560 
564 {
565  // The Renesas V850 is a 32-bit microprocessor used in
566  // many automotive applications. This spec is written from the
567  // architecture manual rather than having access to a running
568  // system. Thus some assumptions have been made.
569 
570  set_ILP32();
571 
572  // Technically, the V850's don't have floating-point at all.
573  // However, the RH850, aimed at automotive has both 32-bit and
574  // 64-bit IEEE-754 float.
575  double_width=8*8;
576  long_double_width=8*8;
578 
579  // Without information about the compiler and RTOS, these are guesses
580  char_is_unsigned=false;
581  NULL_is_zero=true;
582 
583  // No preprocessor definitions due to lack of information
584 }
585 
587 {
588  set_ILP32();
589  long_double_width=8*8; // different from i386
591  char_is_unsigned=false;
592  NULL_is_zero=true;
593 
594  switch(mode)
595  {
596  case flavourt::GCC:
597  defines.push_back("__hppa__");
598  break;
599 
601  assert(false); // not supported by Visual Studio
602  break;
603 
604  case flavourt::APPLE:
606  case flavourt::ARM:
607  case flavourt::ANSI:
608  break;
609 
610  case flavourt::NONE:
611  assert(false);
612  }
613 }
614 
616 {
617  set_ILP32();
618  long_double_width=8*8; // different from i386
620  char_is_unsigned=false;
621  NULL_is_zero=true;
622 
623  switch(mode)
624  {
625  case flavourt::GCC:
626  defines.push_back("__sh__");
627  defines.push_back("__SH4__");
628  break;
629 
631  assert(false); // not supported by Visual Studio
632  break;
633 
634  case flavourt::APPLE:
636  case flavourt::ARM:
637  case flavourt::ANSI:
638  break;
639 
640  case flavourt::NONE:
641  assert(false);
642  }
643 }
644 
646 {
647  #if defined(__APPLE__)
648  // By default, clang on the Mac builds C code in GNU C11
649  return c_standardt::C11;
650  #elif defined(__FreeBSD__)
651  // By default, clang on FreeBSD builds C code in GNU C99
652  return c_standardt::C99;
653  #else
654  return c_standardt::C99;
655  #endif
656 }
657 
659 {
660  return cpp_standardt::CPP98;
661 }
662 
664 {
665  ansi_c.arch=arch;
666 
667  if(arch=="none")
668  {
669  // the architecture for people who can't commit
672  ansi_c.NULL_is_zero=false;
673 
674  if(sizeof(long int)==8)
675  ansi_c.set_64();
676  else
677  ansi_c.set_32();
678  }
679  else if(arch=="alpha")
681  else if(arch=="arm64" ||
682  arch=="armel" ||
683  arch=="armhf" ||
684  arch=="arm")
686  else if(arch=="mips64el" ||
687  arch=="mipsn32el" ||
688  arch=="mipsel" ||
689  arch=="mips64" ||
690  arch=="mipsn32" ||
691  arch=="mips")
693  else if(arch=="powerpc" ||
694  arch=="ppc64" ||
695  arch=="ppc64le")
697  else if(arch=="sparc" ||
698  arch=="sparc64")
700  else if(arch=="ia64")
702  else if(arch=="s390x")
704  else if(arch=="s390")
706  else if(arch=="x32")
708  else if(arch=="v850")
710  else if(arch=="hppa")
712  else if(arch=="sh4")
714  else if(arch=="x86_64")
716  else if(arch=="i386")
718  else
719  {
720  // We run on something new and unknown.
721  // We verify for i386 instead.
723  ansi_c.arch="i386";
724  }
725 }
726 
727 bool configt::set(const cmdlinet &cmdline)
728 {
729  // defaults -- we match the architecture we have ourselves
730 
732 
734  ansi_c.for_has_scope=true; // C99 or later
739  ansi_c.arch="none";
741  // NOLINTNEXTLINE(readability/casting)
742  ansi_c.NULL_is_zero=reinterpret_cast<size_t>(nullptr)==0;
743 
744  // Default is ROUND_TO_EVEN, justified by C99:
745  // 1 At program startup the floating-point environment is initialized as
746  // prescribed by IEC 60559:
747  // - All floating-point exception status flags are cleared.
748  // - The rounding direction mode is rounding to nearest.
750 
751  if(cmdline.isset("function"))
752  main=cmdline.get_value("function");
753 
754  if(cmdline.isset('D'))
755  ansi_c.defines=cmdline.get_values('D');
756 
757  if(cmdline.isset('I'))
758  ansi_c.include_paths=cmdline.get_values('I');
759 
760  if(cmdline.isset("classpath"))
761  {
762  // Specifying -classpath or -cp overrides any setting of the
763  // CLASSPATH environment variable.
764  set_classpath(cmdline.get_value("classpath"));
765  }
766  else if(cmdline.isset("cp"))
767  {
768  // Specifying -classpath or -cp overrides any setting of the
769  // CLASSPATH environment variable.
770  set_classpath(cmdline.get_value("cp"));
771  }
772  else
773  {
774  // environment variable set?
775  const char *CLASSPATH=getenv("CLASSPATH");
776  if(CLASSPATH!=nullptr)
777  set_classpath(CLASSPATH);
778  else
779  set_classpath("."); // default
780  }
781 
782  if(cmdline.isset("main-class"))
783  java.main_class=cmdline.get_value("main-class");
784 
785  if(cmdline.isset("include"))
786  ansi_c.include_files=cmdline.get_values("include");
787 
788  if(cmdline.isset("floatbv"))
790 
791  if(cmdline.isset("fixedbv"))
793 
794  // the default architecture is the one we run on
795  irep_idt this_arch=this_architecture();
796  irep_idt arch=this_arch;
797 
798  // let's pick an OS now
799  // the default is the one we run on
801  irep_idt os=this_os;
802 
803  if(cmdline.isset("i386-linux"))
804  {
805  os="linux";
806  arch="i386";
807  }
808  else if(cmdline.isset("i386-win32") ||
809  cmdline.isset("win32"))
810  {
811  os="windows";
812  arch="i386";
813  }
814  else if(cmdline.isset("winx64"))
815  {
816  os="windows";
817  arch="x86_64";
818  }
819  else if(cmdline.isset("i386-macos"))
820  {
821  os="macos";
822  arch="i386";
823  }
824  else if(cmdline.isset("ppc-macos"))
825  {
826  arch="powerpc";
827  os="macos";
828  }
829 
830  if(cmdline.isset("arch"))
831  {
832  arch=cmdline.get_value("arch");
833  }
834 
835  if(cmdline.isset("os"))
836  {
837  os=cmdline.get_value("os");
838  }
839 
840  if(os=="windows")
841  {
842  // Cygwin uses GCC throughout, use i386-linux
843  // MinGW needs --win32 --gcc
846 
847  if(cmdline.isset("gcc"))
848  {
849  // There are gcc versions that target Windows (MinGW for example),
850  // and we support that.
853 
854  // enable Cygwin
855  #ifdef _WIN32
856  ansi_c.defines.push_back("__CYGWIN__");
857  #endif
858 
859  // MinGW has extra defines
860  ansi_c.defines.push_back("__int64=\"long long\"");
861  }
862  else
863  {
864  // On Windows, our default is Visual Studio.
865  // On FreeBSD, it's clang.
866  // On anything else, it's GCC as the preprocessor,
867  // but we recognize the Visual Studio language,
868  // which is somewhat inconsistent.
869  #ifdef _WIN32
872  #elif __FreeBSD__
875  #else
878  #endif
879  }
880  }
881  else if(os=="macos")
882  {
887  }
888  else if(os=="linux" || os=="solaris")
889  {
894  }
895  else if(os=="freebsd")
896  {
901  }
902  else
903  {
904  // give up, but use reasonable defaults
909  }
910 
911  set_arch(arch);
912 
913  if(os=="windows")
914  {
915  // note that sizeof(void *)==8, but sizeof(long)==4!
916  if(arch=="x86_64")
917  ansi_c.set_LLP64();
918 
919  // On Windows, wchar_t is unsigned 16 bit, regardless
920  // of the compiler used.
921  ansi_c.wchar_t_width=2*8;
923 
924  // long double is the same as double in Visual Studio,
925  // but it's 16 bytes with GCC with the 64-bit target.
926  if(arch=="x64_64" && cmdline.isset("gcc"))
928  else
930  }
931 
932  // Let's check some of the type widths in case we run
933  // the same architecture and OS that we are verifying for.
934  if(arch==this_arch && os==this_os)
935  {
936  assert(ansi_c.int_width==sizeof(int)*8);
937  assert(ansi_c.long_int_width==sizeof(long)*8);
938  assert(ansi_c.bool_width==sizeof(bool)*8);
939  assert(ansi_c.char_width==sizeof(char)*8);
940  assert(ansi_c.short_int_width==sizeof(short)*8);
941  assert(ansi_c.long_long_int_width==sizeof(long long)*8);
942  assert(ansi_c.pointer_width==sizeof(void *)*8);
943  assert(ansi_c.single_width==sizeof(float)*8);
944  assert(ansi_c.double_width==sizeof(double)*8);
945  assert(ansi_c.char_is_unsigned==(static_cast<char>(255)==255));
946 
947  #ifndef _WIN32
948  // On Windows, long double width varies by compiler
949  assert(ansi_c.long_double_width==sizeof(long double)*8);
950  #endif
951  }
952 
953  // the following allows overriding the defaults
954 
955  if(cmdline.isset("16"))
956  ansi_c.set_16();
957 
958  if(cmdline.isset("32"))
959  ansi_c.set_32();
960 
961  if(cmdline.isset("64"))
962  ansi_c.set_64();
963 
964  if(cmdline.isset("LP64"))
965  ansi_c.set_LP64(); // int=32, long=64, pointer=64
966 
967  if(cmdline.isset("ILP64"))
968  ansi_c.set_ILP64(); // int=64, long=64, pointer=64
969 
970  if(cmdline.isset("LLP64"))
971  ansi_c.set_LLP64(); // int=32, long=32, pointer=64
972 
973  if(cmdline.isset("ILP32"))
974  ansi_c.set_ILP32(); // int=32, long=32, pointer=32
975 
976  if(cmdline.isset("LP32"))
977  ansi_c.set_LP32(); // int=16, long=32, pointer=32
978 
979  if(cmdline.isset("string-abstraction"))
981  else
983 
984  if(cmdline.isset("no-library"))
986 
987  if(cmdline.isset("little-endian"))
989 
990  if(cmdline.isset("big-endian"))
992 
993  if(cmdline.isset("little-endian") &&
994  cmdline.isset("big-endian"))
995  return true;
996 
997  if(cmdline.isset("unsigned-char"))
999 
1000  if(cmdline.isset("round-to-even") ||
1001  cmdline.isset("round-to-nearest"))
1003 
1004  if(cmdline.isset("round-to-plus-inf"))
1006 
1007  if(cmdline.isset("round-to-minus-inf"))
1009 
1010  if(cmdline.isset("round-to-zero"))
1012 
1013  return false;
1014 }
1015 
1017 {
1018  switch(os)
1019  {
1020  case ost::OS_LINUX: return "linux";
1021  case ost::OS_MACOS: return "macos";
1022  case ost::OS_WIN: return "win";
1023  default: return "none";
1024  }
1025 }
1026 
1028 {
1029  if(os=="linux")
1030  return ost::OS_LINUX;
1031  else if(os=="macos")
1032  return ost::OS_MACOS;
1033  else if(os=="win")
1034  return ost::OS_WIN;
1035  else
1036  return ost::NO_OS;
1037 }
1038 
1040  const namespacet &ns,
1041  const std::string &what)
1042 {
1043  const irep_idt id=CPROVER_PREFIX "architecture_"+what;
1044  const symbolt *symbol;
1045 
1046  if(ns.lookup(id, symbol))
1047  throw "failed to find "+id2string(id);
1048 
1049  const exprt &tmp=symbol->value;
1050 
1051  if(tmp.id()!=ID_address_of ||
1052  tmp.operands().size()!=1 ||
1053  tmp.op0().id()!=ID_index ||
1054  tmp.op0().operands().size()!=2 ||
1055  tmp.op0().op0().id()!=ID_string_constant)
1056  {
1057  throw
1058  "symbol table configuration entry `"+id2string(id)+
1059  "' is not a string constant";
1060  }
1061 
1062  return tmp.op0().op0().get(ID_value);
1063 }
1064 
1065 static unsigned unsigned_from_ns(
1066  const namespacet &ns,
1067  const std::string &what)
1068 {
1069  const irep_idt id=CPROVER_PREFIX "architecture_"+what;
1070  const symbolt *symbol;
1071 
1072  if(ns.lookup(id, symbol))
1073  throw "failed to find "+id2string(id);
1074 
1075  exprt tmp=symbol->value;
1076  simplify(tmp, ns);
1077 
1078  if(tmp.id()!=ID_constant)
1079  throw
1080  "symbol table configuration entry `"+id2string(id)+"' is not a constant";
1081 
1082  mp_integer int_value;
1083 
1084  if(to_integer(to_constant_expr(tmp), int_value))
1085  throw
1086  "failed to convert symbol table configuration entry `"+id2string(id)+"'";
1087 
1088  return integer2unsigned(int_value);
1089 }
1090 
1092  const symbol_tablet &symbol_table)
1093 {
1094  // maybe not compiled from C/C++
1095  if(symbol_table.symbols.find(CPROVER_PREFIX "architecture_" "int_width")==
1096  symbol_table.symbols.end())
1097  return;
1098 
1099  namespacet ns(symbol_table);
1100 
1101  // clear defines
1102  ansi_c.defines.clear();
1103 
1104  // first set architecture to get some defaults
1105  if(symbol_table.symbols.find(CPROVER_PREFIX "architecture_" "arch")==
1106  symbol_table.symbols.end())
1108  else
1109  set_arch(string_from_ns(ns, "arch"));
1110 
1111  ansi_c.int_width=unsigned_from_ns(ns, "int_width");
1112  ansi_c.long_int_width=unsigned_from_ns(ns, "long_int_width");
1113  ansi_c.bool_width=1*8;
1114  ansi_c.char_width=unsigned_from_ns(ns, "char_width");
1115  ansi_c.short_int_width=unsigned_from_ns(ns, "short_int_width");
1116  ansi_c.long_long_int_width=unsigned_from_ns(ns, "long_long_int_width");
1117  ansi_c.pointer_width=unsigned_from_ns(ns, "pointer_width");
1118  ansi_c.single_width=unsigned_from_ns(ns, "single_width");
1119  ansi_c.double_width=unsigned_from_ns(ns, "double_width");
1120  ansi_c.long_double_width=unsigned_from_ns(ns, "long_double_width");
1121  ansi_c.wchar_t_width=unsigned_from_ns(ns, "wchar_t_width");
1122 
1123  ansi_c.char_is_unsigned=unsigned_from_ns(ns, "char_is_unsigned")!=0;
1124  ansi_c.wchar_t_is_unsigned=unsigned_from_ns(ns, "wchar_t_is_unsigned")!=0;
1125  ansi_c.use_fixed_for_float=unsigned_from_ns(ns, "fixed_for_float")!=0;
1126  // for_has_scope, single_precision_constant, rounding_mode not
1127  // stored in namespace
1128 
1129  ansi_c.alignment=unsigned_from_ns(ns, "alignment");
1130 
1131  ansi_c.memory_operand_size=unsigned_from_ns(ns, "memory_operand_size");
1132 
1134 
1135  if(symbol_table.symbols.find(CPROVER_PREFIX "architecture_" "os")==
1136  symbol_table.symbols.end())
1138  else
1140 
1141  // NULL_is_zero=from_ns("NULL_is_zero");
1142  ansi_c.NULL_is_zero=true;
1143 
1144  // mode, preprocessor (and all preprocessor command line options),
1145  // lib, string_abstraction not stored in namespace
1146 }
1147 
1149 {
1150  irep_idt this_arch;
1151 
1152  // following http://wiki.debian.org/ArchitectureSpecificsMemo
1153 
1154  #ifdef __alpha__
1155  this_arch="alpha";
1156  #elif __armel__
1157  this_arch="armel";
1158  #elif __aarch64__
1159  this_arch="arm64";
1160  #elif __arm__
1161  #ifdef __ARM_PCS_VFP
1162  this_arch="armhf"; // variant of arm with hard float
1163  #else
1164  this_arch="arm";
1165  #endif
1166  #elif __mipsel__
1167  #if _MIPS_SIM==_ABIO32
1168  this_arch="mipsel";
1169  #elif _MIPS_SIM==_ABIN32
1170  this_arch="mipsn32el";
1171  #else
1172  this_arch="mips64el";
1173  #endif
1174  #elif __mips__
1175  #if _MIPS_SIM==_ABIO32
1176  this_arch="mips";
1177  #elif _MIPS_SIM==_ABIN32
1178  this_arch="mipsn32";
1179  #else
1180  this_arch="mips64";
1181  #endif
1182  #elif __powerpc__
1183  #if defined(__ppc64__) || defined(__PPC64__) || \
1184  defined(__powerpc64__) || defined(__POWERPC64__)
1185  #ifdef __LITTLE_ENDIAN__
1186  this_arch="ppc64le";
1187  #else
1188  this_arch="ppc64";
1189  #endif
1190  #else
1191  this_arch="powerpc";
1192  #endif
1193  #elif __sparc__
1194  #ifdef __arch64__
1195  this_arch="sparc64";
1196  #else
1197  this_arch="sparc";
1198  #endif
1199  #elif __ia64__
1200  this_arch="ia64";
1201  #elif __s390x__
1202  this_arch="s390x";
1203  #elif __s390__
1204  this_arch="s390";
1205  #elif __x86_64__
1206  #ifdef __ILP32__
1207  this_arch="x32"; // variant of x86_64 with 32-bit pointers
1208  #else
1209  this_arch="x86_64";
1210  #endif
1211  #elif __i386__
1212  this_arch="i386";
1213  #elif _WIN64
1214  this_arch="x86_64";
1215  #elif _WIN32
1216  this_arch="i386";
1217  #elif __hppa__
1218  this_arch="hppa";
1219  #elif __sh__
1220  this_arch="sh4";
1221  #else
1222  // something new and unknown!
1223  this_arch="unknown";
1224  #endif
1225 
1226  return this_arch;
1227 }
1228 
1229 void configt::set_classpath(const std::string &cp)
1230 {
1231  std::string current;
1232  for(std::size_t pos=0; pos<cp.size(); pos++)
1233  {
1234  // These are separated by colons on Unix, and semicolons on
1235  // Windows.
1236  #ifdef _WIN32
1237  const char cp_separator=';';
1238  #else
1239  const char cp_separator=':';
1240  #endif
1241 
1242  if(cp[pos]==cp_separator)
1243  {
1244  if(!current.empty())
1245  {
1246  java.classpath.push_back(current);
1247  current.clear();
1248  }
1249  }
1250  else
1251  current+=cp[pos];
1252  }
1253 
1254  if(!current.empty())
1255  java.classpath.push_back(current);
1256 }
1257 
1259 {
1260  irep_idt this_os;
1261 
1262  #ifdef _WIN32
1263  this_os="windows";
1264  #elif __APPLE__
1265  this_os="macos";
1266  #elif __FreeBSD__
1267  this_os="freebsd";
1268  #elif __linux__
1269  this_os="linux";
1270  #elif __SVR4
1271  this_os="solaris";
1272  #else
1273  this_os="unknown";
1274  #endif
1275 
1276  return this_os;
1277 }
void set_arch_spec_arm(const irep_idt &subarch)
Definition: config.cpp:276
const std::list< std::string > & get_values(const std::string &option) const
Definition: cmdline.cpp:90
void set_LP32()
int=16, long=32, pointer=32
Definition: config.cpp:127
struct configt::ansi_ct ansi_c
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
Definition: namespace.cpp:139
BigInt mp_integer
Definition: mp_arith.h:19
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
void set_arch_spec_power(const irep_idt &subarch)
Definition: config.cpp:215
unsigned int_width
Definition: config.h:30
Globally accessible architectural configuration.
Definition: config.h:24
unsigned single_width
Definition: config.h:37
exprt & op0()
Definition: expr.h:84
#define CPROVER_PREFIX
void set_classpath(const std::string &cp)
Definition: config.cpp:1229
static std::string os_to_string(ost)
Definition: config.cpp:1016
unsigned alignment
Definition: config.h:68
bool single_precision_constant
Definition: config.h:46
void set_arch_spec_v850()
Sets up the widths of variables for the Renesas V850.
Definition: config.cpp:563
endiannesst endianness
Definition: config.h:75
std::list< std::string > defines
Definition: config.h:111
literalt pos(literalt a)
Definition: literal.h:193
static irep_idt string_from_ns(const namespacet &ns, const std::string &what)
Definition: config.cpp:1039
exprt value
Initial value of symbol.
Definition: symbol.h:40
std::string get_value(char option) const
Definition: cmdline.cpp:46
unsigned short_int_width
Definition: config.h:34
bool NULL_is_zero
Definition: config.h:86
void set_LP64()
int=32, long=64, pointer=64
Definition: config.cpp:43
void set_arch_spec_ia64()
Definition: config.cpp:495
unsigned char_width
Definition: config.h:33
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
configt config
Definition: config.cpp:21
void set_16()
Definition: config.cpp:23
void set_arch_spec_mips(const irep_idt &subarch)
Definition: config.cpp:348
preprocessort preprocessor
Definition: config.h:109
unsigned wchar_t_width
Definition: config.h:40
bool set(const cmdlinet &cmdline)
Definition: config.cpp:727
const irep_idt & id() const
Definition: irep.h:189
std::list< std::string > include_files
Definition: config.h:115
classpatht classpath
Definition: config.h:142
virtual bool isset(char option) const
Definition: cmdline.cpp:30
symbolst symbols
Definition: symbol_table.h:57
void set_arch_spec_sparc(const irep_idt &subarch)
Definition: config.cpp:455
flavourt mode
Definition: config.h:105
void set_arch_spec_x86_64()
Definition: config.cpp:178
static unsigned unsigned_from_ns(const namespacet &ns, const std::string &what)
Definition: config.cpp:1065
unsigned long_long_int_width
Definition: config.h:35
std::string main
Definition: config.h:147
void set_arch(const irep_idt &)
Definition: config.cpp:663
API to expression classes.
The symbol table.
Definition: symbol_table.h:52
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
irep_idt arch
Definition: config.h:83
TO_BE_DOCUMENTED.
Definition: namespace.h:62
void set_arch_spec_alpha()
Definition: config.cpp:319
enum configt::cppt::cpp_standardt cpp_standard
void set_32()
Definition: config.cpp:28
void set_arch_spec_x32()
Definition: config.cpp:526
void set_ILP32()
int=32, long=32, pointer=32
Definition: config.cpp:107
void set_arch_spec_sh4()
Definition: config.cpp:615
unsigned memory_operand_size
Definition: config.h:72
bool for_has_scope
Definition: config.h:45
struct configt::javat java
Symbol table.
void set_arch_spec_s390()
Definition: config.cpp:398
bool char_is_unsigned
Definition: config.h:43
bool use_fixed_for_float
Definition: config.h:44
void set_from_symbol_table(const symbol_tablet &)
Definition: config.cpp:1091
enum configt::ansi_ct::c_standardt c_standard
unsigned integer2unsigned(const mp_integer &n)
Definition: mp_arith.cpp:203
static c_standardt default_c_standard()
Definition: config.cpp:645
static irep_idt this_operating_system()
Definition: config.cpp:1258
struct configt::cppt cpp
ieee_floatt::rounding_modet rounding_mode
Definition: config.h:54
bool string_abstraction
Definition: config.h:120
Base class for all expressions.
Definition: expr.h:46
unsigned bool_width
Definition: config.h:32
void set_arch_spec_hppa()
Definition: config.cpp:586
void set_arch_spec_i386()
Definition: config.cpp:146
unsigned long_double_width
Definition: config.h:39
void set_64()
Definition: config.cpp:33
void set_LLP64()
int=32, long=32, pointer=64
Definition: config.cpp:87
static ost string_to_os(const std::string &)
Definition: config.cpp:1027
unsigned double_width
Definition: config.h:38
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:18
irep_idt main_class
Definition: config.h:143
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
Definition: std_expr.h:3725
unsigned long_int_width
Definition: config.h:31
bool wchar_t_is_unsigned
Definition: config.h:43
unsigned pointer_width
Definition: config.h:36
operandst & operands()
Definition: expr.h:70
static cpp_standardt default_cpp_standard()
Definition: config.cpp:658
static irep_idt this_architecture()
Definition: config.cpp:1148
void set_arch_spec_s390x()
Definition: config.cpp:427
bool simplify(exprt &expr, const namespacet &ns)
void set_ILP64()
int=64, long=64, pointer=64
Definition: config.cpp:67
std::list< std::string > include_paths
Definition: config.h:114