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