cprover
Loading...
Searching...
No Matches
goto_instrument_parse_options.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Main Module
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
13
15#include <util/exit_codes.h>
16#include <util/help_formatter.h>
17#include <util/json.h>
18#include <util/options.h>
19#include <util/string2int.h>
20#include <util/string_utils.h>
21#include <util/unicode.h>
22#include <util/version.h>
23
31#include <goto-programs/mm_io.h>
49
50#include <analyses/call_graph.h>
56#include <analyses/guard.h>
69#include <ansi-c/gcc_version.h>
72#include <cpp/cprover_library.h>
76
77#include "alignment_checks.h"
78#include "branch.h"
79#include "call_sequences.h"
80#include "concurrency.h"
81#include "dot.h"
82#include "full_slicer.h"
83#include "function.h"
84#include "havoc_loops.h"
85#include "horn_encoding.h"
87#include "interrupt.h"
88#include "k_induction.h"
89#include "mmio.h"
90#include "nondet_static.h"
91#include "nondet_volatile.h"
92#include "points_to.h"
93#include "race_check.h"
94#include "remove_function.h"
95#include "rw_set.h"
96#include "show_locations.h"
97#include "skip_loops.h"
98#include "splice_call.h"
99#include "stack_depth.h"
101#include "undefined_functions.h"
102#include "unwind.h"
104
105#include <fstream> // IWYU pragma: keep
106#include <iostream>
107#include <memory>
108#include <sstream>
109
111
114{
115 if(cmdline.isset("version"))
116 {
117 std::cout << CBMC_VERSION << '\n';
119 }
120
121 if(cmdline.args.size()!=1 && cmdline.args.size()!=2)
122 {
123 help();
125 }
126
128 cmdline.get_value("verbosity"), messaget::M_STATUS, ui_message_handler);
129
130 {
132
134
135 // configure gcc, if required -- get_goto_program will have set the config
136 if(config.ansi_c.preprocessor == configt::ansi_ct::preprocessort::GCC)
137 {
138 gcc_versiont gcc_version;
139 gcc_version.get("gcc");
140 configure_gcc(gcc_version);
141 }
142
143 {
144 const bool validate_only = cmdline.isset("validate-goto-binary");
145
146 if(validate_only || cmdline.isset("validate-goto-model"))
147 {
149
150 if(validate_only)
151 {
153 }
154 }
155 }
156
157 // ignore default/user-specified initialization
158 // of matching variables with static lifetime
159 if(cmdline.isset("nondet-static-matching"))
160 {
161 log.status() << "Adding nondeterministic initialization "
162 "of matching static/global variables"
163 << messaget::eom;
165 goto_model, cmdline.get_value("nondet-static-matching"));
166 }
167
169
170 if(cmdline.isset("validate-goto-model"))
171 {
172 goto_model.validate();
173 }
174
175 {
176 bool unwind_given=cmdline.isset("unwind");
177 bool unwindset_given=cmdline.isset("unwindset");
178 bool unwindset_file_given=cmdline.isset("unwindset-file");
179
180 if(unwindset_given && unwindset_file_given)
181 throw "only one of --unwindset and --unwindset-file supported at a "
182 "time";
183
184 if(unwind_given || unwindset_given || unwindset_file_given)
185 {
186 unwindsett unwindset{goto_model};
187
188 if(unwind_given)
189 unwindset.parse_unwind(cmdline.get_value("unwind"));
190
191 if(unwindset_file_given)
192 {
193 unwindset.parse_unwindset_file(
194 cmdline.get_value("unwindset-file"), ui_message_handler);
195 }
196
197 if(unwindset_given)
198 {
199 unwindset.parse_unwindset(
200 cmdline.get_comma_separated_values("unwindset"),
202 }
203
204 bool continue_as_loops=cmdline.isset("continue-as-loops");
205 bool partial_loops = cmdline.isset("partial-loops");
206 bool unwinding_assertions = cmdline.isset("unwinding-assertions") ||
207 (!continue_as_loops && !partial_loops &&
208 !cmdline.isset("no-unwinding-assertions"));
209 if(continue_as_loops)
210 {
211 if(unwinding_assertions)
212 {
213 throw "unwinding assertions cannot be used with "
214 "--continue-as-loops";
215 }
216 else if(partial_loops)
217 throw "partial loops cannot be used with --continue-as-loops";
218 }
219
220 goto_unwindt::unwind_strategyt unwind_strategy=
222
223 if(unwinding_assertions)
224 {
225 if(partial_loops)
227 else
229 }
230 else if(partial_loops)
231 {
233 }
234 else if(continue_as_loops)
235 {
237 }
238
239 goto_unwindt goto_unwind;
240 goto_unwind(goto_model, unwindset, unwind_strategy);
241
242 if(cmdline.isset("log"))
243 {
244 std::string filename=cmdline.get_value("log");
245 bool have_file=!filename.empty() && filename!="-";
246
247 jsont result=goto_unwind.output_log_json();
248
249 if(have_file)
250 {
251 std::ofstream of(widen_if_needed(filename));
252
253 if(!of)
254 throw "failed to open file "+filename;
255
256 of << result;
257 of.close();
258 }
259 else
260 {
261 std::cout << result << '\n';
262 }
263 }
264
265 // goto_unwind holds references to instructions, only do remove_skip
266 // after having generated the log above
268 }
269 }
270
271 if(cmdline.isset("show-threaded"))
272 {
273 namespacet ns(goto_model.symbol_table);
274
275 is_threadedt is_threaded(goto_model);
276
277 for(const auto &gf_entry : goto_model.goto_functions.function_map)
278 {
279 std::cout << "////\n";
280 std::cout << "//// Function: " << gf_entry.first << '\n';
281 std::cout << "////\n\n";
282
283 const goto_programt &goto_program = gf_entry.second.body;
284
285 forall_goto_program_instructions(i_it, goto_program)
286 {
287 i_it->output(std::cout);
288 std::cout << "Is threaded: " << (is_threaded(i_it)?"True":"False")
289 << "\n\n";
290 }
291 }
292
294 }
295
296 if(cmdline.isset("insert-final-assert-false"))
297 {
298 log.status() << "Inserting final assert false" << messaget::eom;
299 bool fail = insert_final_assert_false(
301 cmdline.get_value("insert-final-assert-false"),
303 if(fail)
304 {
306 }
307 // otherwise, fall-through to write new binary
308 }
309
310 if(cmdline.isset("show-value-sets"))
311 {
313
314 // recalculate numbers, etc.
315 goto_model.goto_functions.update();
316
317 log.status() << "Pointer Analysis" << messaget::eom;
318 namespacet ns(goto_model.symbol_table);
319 value_set_analysist value_set_analysis(ns);
320 value_set_analysis(goto_model);
322 ui_message_handler.get_ui(), goto_model, value_set_analysis);
324 }
325
326 if(cmdline.isset("show-global-may-alias"))
327 {
331
332 // recalculate numbers, etc.
333 goto_model.goto_functions.update();
334
335 global_may_alias_analysist global_may_alias_analysis;
336 global_may_alias_analysis(goto_model);
337 global_may_alias_analysis.output(goto_model, std::cout);
338
340 }
341
342 if(cmdline.isset("show-local-bitvector-analysis"))
343 {
346
347 // recalculate numbers, etc.
348 goto_model.goto_functions.update();
349
350 namespacet ns(goto_model.symbol_table);
351
352 for(const auto &gf_entry : goto_model.goto_functions.function_map)
353 {
354 local_bitvector_analysist local_bitvector_analysis(gf_entry.second, ns);
355 std::cout << ">>>>\n";
356 std::cout << ">>>> " << gf_entry.first << '\n';
357 std::cout << ">>>>\n";
358 local_bitvector_analysis.output(std::cout, gf_entry.second, ns);
359 std::cout << '\n';
360 }
361
363 }
364
365 if(cmdline.isset("show-local-safe-pointers") ||
366 cmdline.isset("show-safe-dereferences"))
367 {
368 // Ensure location numbering is unique:
369 goto_model.goto_functions.update();
370
371 namespacet ns(goto_model.symbol_table);
372
373 for(const auto &gf_entry : goto_model.goto_functions.function_map)
374 {
375 local_safe_pointerst local_safe_pointers;
376 local_safe_pointers(gf_entry.second.body);
377 std::cout << ">>>>\n";
378 std::cout << ">>>> " << gf_entry.first << '\n';
379 std::cout << ">>>>\n";
380 if(cmdline.isset("show-local-safe-pointers"))
381 local_safe_pointers.output(std::cout, gf_entry.second.body, ns);
382 else
383 {
384 local_safe_pointers.output_safe_dereferences(
385 std::cout, gf_entry.second.body, ns);
386 }
387 std::cout << '\n';
388 }
389
391 }
392
393 if(cmdline.isset("show-sese-regions"))
394 {
395 // Ensure location numbering is unique:
396 goto_model.goto_functions.update();
397
398 namespacet ns(goto_model.symbol_table);
399
400 for(const auto &gf_entry : goto_model.goto_functions.function_map)
401 {
402 sese_region_analysist sese_region_analysis;
403 sese_region_analysis(gf_entry.second.body);
404 std::cout << ">>>>\n";
405 std::cout << ">>>> " << gf_entry.first << '\n';
406 std::cout << ">>>>\n";
407 sese_region_analysis.output(std::cout, gf_entry.second.body, ns);
408 std::cout << '\n';
409 }
410
412 }
413
414 if(cmdline.isset("show-custom-bitvector-analysis"))
415 {
419
421
422 if(!cmdline.isset("inline"))
423 {
426 }
427
428 // recalculate numbers, etc.
429 goto_model.goto_functions.update();
430
431 custom_bitvector_analysist custom_bitvector_analysis;
432 custom_bitvector_analysis(goto_model);
433 custom_bitvector_analysis.output(goto_model, std::cout);
434
436 }
437
438 if(cmdline.isset("show-escape-analysis"))
439 {
443
444 // recalculate numbers, etc.
445 goto_model.goto_functions.update();
446
447 escape_analysist escape_analysis;
448 escape_analysis(goto_model);
449 escape_analysis.output(goto_model, std::cout);
450
452 }
453
454 if(cmdline.isset("custom-bitvector-analysis"))
455 {
459
461
462 if(!cmdline.isset("inline"))
463 {
466 }
467
468 // recalculate numbers, etc.
469 goto_model.goto_functions.update();
470
471 namespacet ns(goto_model.symbol_table);
472
473 custom_bitvector_analysist custom_bitvector_analysis;
474 custom_bitvector_analysis(goto_model);
475 custom_bitvector_analysis.check(
477 cmdline.isset("xml-ui"),
478 std::cout);
479
481 }
482
483 if(cmdline.isset("show-points-to"))
484 {
486
487 // recalculate numbers, etc.
488 goto_model.goto_functions.update();
489
490 namespacet ns(goto_model.symbol_table);
491
492 log.status() << "Pointer Analysis" << messaget::eom;
493 points_tot points_to;
494 points_to(goto_model);
495 points_to.output(std::cout);
497 }
498
499 if(cmdline.isset("show-intervals"))
500 {
502
503 // recalculate numbers, etc.
504 goto_model.goto_functions.update();
505
506 log.status() << "Interval Analysis" << messaget::eom;
507 namespacet ns(goto_model.symbol_table);
510 interval_analysis.output(goto_model, std::cout);
512 }
513
514 if(cmdline.isset("show-call-sequences"))
515 {
519 }
520
521 if(cmdline.isset("check-call-sequence"))
522 {
526 }
527
528 if(cmdline.isset("list-calls-args"))
529 {
531
533
535 }
536
537 if(cmdline.isset("show-rw-set"))
538 {
539 namespacet ns(goto_model.symbol_table);
540
541 if(!cmdline.isset("inline"))
542 {
544
545 // recalculate numbers, etc.
546 goto_model.goto_functions.update();
547 }
548
549 log.status() << "Pointer Analysis" << messaget::eom;
550 value_set_analysist value_set_analysis(ns);
551 value_set_analysis(goto_model);
552
553 const symbolt &symbol=ns.lookup(ID_main);
554 symbol_exprt main(symbol.name, symbol.type);
555
556 std::cout << rw_set_functiont(
557 value_set_analysis, goto_model, main, ui_message_handler);
559 }
560
561 if(cmdline.isset("show-symbol-table"))
562 {
565 }
566
567 if(cmdline.isset("show-reaching-definitions"))
568 {
571
572 const namespacet ns(goto_model.symbol_table);
574 rd_analysis(goto_model);
575 rd_analysis.output(goto_model, std::cout);
576
578 }
579
580 if(cmdline.isset("show-dependence-graph"))
581 {
584
585 const namespacet ns(goto_model.symbol_table);
586 dependence_grapht dependence_graph(ns, ui_message_handler);
587 dependence_graph(goto_model);
588 dependence_graph.output(goto_model, std::cout);
589 dependence_graph.output_dot(std::cout);
590
592 }
593
594 if(cmdline.isset("count-eloc"))
595 {
598 }
599
600 if(cmdline.isset("list-eloc"))
601 {
604 }
605
606 if(cmdline.isset("print-path-lengths"))
607 {
610 }
611
612 if(cmdline.isset("print-global-state-size"))
613 {
616 }
617
618 if(cmdline.isset("list-symbols"))
619 {
622 }
623
624 if(cmdline.isset("show-uninitialized"))
625 {
626 show_uninitialized(goto_model, std::cout);
628 }
629
630 if(cmdline.isset("interpreter"))
631 {
634
635 log.status() << "Starting interpreter" << messaget::eom;
638 }
639
640 if(cmdline.isset("show-claims") ||
641 cmdline.isset("show-properties"))
642 {
643 const namespacet ns(goto_model.symbol_table);
646 }
647
648 if(cmdline.isset("document-claims-html") ||
649 cmdline.isset("document-properties-html"))
650 {
653 }
654
655 if(cmdline.isset("document-claims-latex") ||
656 cmdline.isset("document-properties-latex"))
657 {
660 }
661
662 if(cmdline.isset("show-loops"))
663 {
666 }
667
668 if(cmdline.isset("show-natural-loops"))
669 {
670 show_natural_loops(goto_model, std::cout);
672 }
673
674 if(cmdline.isset("show-lexical-loops"))
675 {
676 show_lexical_loops(goto_model, std::cout);
678 }
679
680 if(cmdline.isset("print-internal-representation"))
681 {
682 for(auto const &pair : goto_model.goto_functions.function_map)
683 for(auto const &ins : pair.second.body.instructions)
684 {
685 if(ins.code().is_not_nil())
686 log.status() << ins.code().pretty() << messaget::eom;
687 if(ins.has_condition())
688 {
689 log.status() << "[guard] " << ins.condition().pretty()
690 << messaget::eom;
691 }
692 }
694 }
695
696 if(
697 cmdline.isset("show-goto-functions") ||
698 cmdline.isset("list-goto-functions"))
699 {
701 goto_model, ui_message_handler, cmdline.isset("list-goto-functions"));
703 }
704
705 if(cmdline.isset("list-undefined-functions"))
706 {
709 }
710
711 // experimental: print structs
712 if(cmdline.isset("show-struct-alignment"))
713 {
714 print_struct_alignment_problems(goto_model.symbol_table, std::cout);
716 }
717
718 if(cmdline.isset("show-locations"))
719 {
722 }
723
724 if(
725 cmdline.isset("dump-c") || cmdline.isset("dump-cpp") ||
726 cmdline.isset("dump-c-type-header"))
727 {
728 const bool is_cpp=cmdline.isset("dump-cpp");
729 const bool is_header = cmdline.isset("dump-c-type-header");
730 const bool h_libc=!cmdline.isset("no-system-headers");
731 const bool h_all=cmdline.isset("use-all-headers");
732 const bool harness=cmdline.isset("harness");
733 namespacet ns(goto_model.symbol_table);
734
735 // restore RETURN instructions in case remove_returns had been
736 // applied
738
739 // dump_c (actually goto_program2code) requires valid instruction
740 // location numbers:
741 goto_model.goto_functions.update();
742
743 if(cmdline.args.size()==2)
744 {
745 std::ofstream out(widen_if_needed(cmdline.args[1]));
746
747 if(!out)
748 {
749 log.error() << "failed to write to '" << cmdline.args[1] << "'";
751 }
752 if(is_header)
753 {
755 goto_model.goto_functions,
756 h_libc,
757 h_all,
758 harness,
759 ns,
760 cmdline.get_value("dump-c-type-header"),
761 out);
762 }
763 else
764 {
765 (is_cpp ? dump_cpp : dump_c)(
766 goto_model.goto_functions, h_libc, h_all, harness, ns, out);
767 }
768 }
769 else
770 {
771 if(is_header)
772 {
774 goto_model.goto_functions,
775 h_libc,
776 h_all,
777 harness,
778 ns,
779 cmdline.get_value("dump-c-type-header"),
780 std::cout);
781 }
782 else
783 {
784 (is_cpp ? dump_cpp : dump_c)(
785 goto_model.goto_functions, h_libc, h_all, harness, ns, std::cout);
786 }
787 }
788
790 }
791
792 if(cmdline.isset("call-graph"))
793 {
795 call_grapht call_graph(goto_model);
796
797 if(cmdline.isset("xml"))
798 call_graph.output_xml(std::cout);
799 else if(cmdline.isset("dot"))
800 call_graph.output_dot(std::cout);
801 else
802 call_graph.output(std::cout);
803
805 }
806
807 if(cmdline.isset("reachable-call-graph"))
808 {
810 call_grapht call_graph =
813 if(cmdline.isset("xml"))
814 call_graph.output_xml(std::cout);
815 else if(cmdline.isset("dot"))
816 call_graph.output_dot(std::cout);
817 else
818 call_graph.output(std::cout);
819
820 return 0;
821 }
822
823 if(cmdline.isset("show-class-hierarchy"))
824 {
825 class_hierarchyt hierarchy;
826 hierarchy(goto_model.symbol_table);
827 if(cmdline.isset("dot"))
828 hierarchy.output_dot(std::cout);
829 else
831
833 }
834
835 if(cmdline.isset("dot"))
836 {
837 namespacet ns(goto_model.symbol_table);
838
839 if(cmdline.args.size()==2)
840 {
841 std::ofstream out(widen_if_needed(cmdline.args[1]));
842
843 if(!out)
844 {
845 log.error() << "failed to write to " << cmdline.args[1] << "'";
847 }
848
849 dot(goto_model, out);
850 }
851 else
852 dot(goto_model, std::cout);
853
855 }
856
857 if(cmdline.isset("accelerate"))
858 {
860
861 namespacet ns(goto_model.symbol_table);
862
863 log.status() << "Performing full inlining" << messaget::eom;
865
866 log.status() << "Removing calls to functions without a body"
867 << messaget::eom;
868 remove_calls_no_bodyt remove_calls_no_body;
869 remove_calls_no_body(goto_model.goto_functions, ui_message_handler);
870
871 log.status() << "Accelerating" << messaget::eom;
872 guard_managert guard_manager;
874 goto_model, ui_message_handler, cmdline.isset("z3"), guard_manager);
876 }
877
878 if(cmdline.isset("horn"))
879 {
880 log.status() << "Horn-clause encoding" << messaget::eom;
881 namespacet ns(goto_model.symbol_table);
882
883 if(cmdline.args.size()==2)
884 {
885 std::ofstream out(widen_if_needed(cmdline.args[1]));
886
887 if(!out)
888 {
889 log.error() << "Failed to open output file " << cmdline.args[1]
890 << messaget::eom;
892 }
893
895 }
896 else
897 horn_encoding(goto_model, std::cout);
898
900 }
901
902 if(cmdline.isset("drop-unused-functions"))
903 {
906
907 log.status() << "Removing unused functions" << messaget::eom;
909 }
910
911 if(cmdline.isset("undefined-function-is-assume-false"))
912 {
915 }
916
917 // write new binary?
918 if(cmdline.args.size()==2)
919 {
920 log.status() << "Writing GOTO program to '" << cmdline.args[1] << "'"
921 << messaget::eom;
922
925 else
927 }
928 else if(cmdline.args.size() < 2)
929 {
931 "Invalid number of positional arguments passed",
932 "[in] [out]",
933 "goto-instrument needs one input and one output file, aside from other "
934 "flags");
935 }
936
937 help();
939 }
940// NOLINTNEXTLINE(readability/fn_size)
941}
942
944 bool force)
945{
947 return;
948
950
951 log.status() << "Function Pointer Removal" << messaget::eom;
953 log.status() << "Virtual function removal" << messaget::eom;
955 log.status() << "Cleaning inline assembler statements" << messaget::eom;
956 remove_asm(goto_model, log.get_message_handler());
957}
958
963{
964 // Don't bother if we've already done a full function pointer
965 // removal.
967 {
968 return;
969 }
970
971 log.status() << "Removing const function pointers only" << messaget::eom;
975 true); // abort if we can't resolve via const pointers
976}
977
979{
981 return;
982
984
985 if(!cmdline.isset("inline"))
986 {
987 log.status() << "Partial Inlining" << messaget::eom;
989 }
990}
991
993{
995 return;
996
998
999 log.status() << "Removing returns" << messaget::eom;
1001}
1002
1004{
1005 log.status() << "Reading GOTO program from '" << cmdline.args[0] << "'"
1006 << messaget::eom;
1007
1008 config.set(cmdline);
1009
1010 auto result = read_goto_binary(cmdline.args[0], ui_message_handler);
1011
1012 if(!result.has_value())
1013 throw 0;
1014
1015 goto_model = std::move(result.value());
1016
1017 config.set_from_symbol_table(goto_model.symbol_table);
1018}
1019
1021{
1022 optionst options;
1023
1025
1026 // disable simplify when adding various checks?
1027 if(cmdline.isset("no-simplify"))
1028 options.set_option("simplify", false);
1029 else
1030 options.set_option("simplify", true);
1031
1032 // all checks supported by goto_check
1034
1035 // initialize argv with valid pointers
1036 if(cmdline.isset("model-argc-argv"))
1037 {
1038 unsigned max_argc=
1039 safe_string2unsigned(cmdline.get_value("model-argc-argv"));
1040 std::list<std::string> argv;
1041 argv.resize(max_argc);
1042
1043 log.status() << "Adding up to " << max_argc << " command line arguments"
1044 << messaget::eom;
1045
1046 if(model_argc_argv(
1047 goto_model, argv, true /*model_argv*/, ui_message_handler))
1048 throw 0;
1049 }
1050
1051 if(cmdline.isset("add-cmd-line-arg"))
1052 {
1053 const std::list<std::string> &argv = cmdline.get_values("add-cmd-line-arg");
1054 unsigned argc = 0;
1055
1056 std::stringstream ss;
1057 ss << "[";
1058 std::string sep = "";
1059 for(auto const &arg : argv)
1060 {
1061 ss << sep << "\"" << arg << "\"";
1062 argc++;
1063 sep = ", ";
1064 }
1065 ss << "]";
1066
1067 log.status() << "Adding " << argc << " arguments: " << ss.str()
1068 << messaget::eom;
1069
1070 if(model_argc_argv(
1071 goto_model, argv, false /*model_argv*/, ui_message_handler))
1072 throw 0;
1073 }
1074
1075 if(cmdline.isset("remove-function-body"))
1076 {
1078 goto_model,
1079 cmdline.get_values("remove-function-body"),
1081 }
1082
1083 // we add the library in some cases, as some analyses benefit
1084
1085 if(
1086 cmdline.isset("add-library") || cmdline.isset("mm") ||
1087 cmdline.isset("reachability-slice") ||
1088 cmdline.isset("reachability-slice-fb") ||
1089 cmdline.isset("fp-reachability-slice"))
1090 {
1091 if(cmdline.isset("show-custom-bitvector-analysis") ||
1092 cmdline.isset("custom-bitvector-analysis"))
1093 {
1094 config.ansi_c.defines.push_back(
1095 std::string(CPROVER_PREFIX) + "CUSTOM_BITVECTOR_ANALYSIS");
1096 }
1097
1098 // remove inline assembler as that may yield further library function calls
1099 // that need to be resolved
1101
1102 // add the library
1103 log.status() << "Adding CPROVER library (" << config.ansi_c.arch << ")"
1104 << messaget::eom;
1108 // library functions may introduce inline assembler
1109 while(has_asm(goto_model))
1110 {
1116 }
1117 }
1118
1119 {
1121
1122 if(
1126 {
1128
1130 }
1131 }
1132
1133 // skip over selected loops
1134 if(cmdline.isset("skip-loops"))
1135 {
1136 log.status() << "Adding gotos to skip loops" << messaget::eom;
1137 if(skip_loops(
1138 goto_model, cmdline.get_value("skip-loops"), ui_message_handler))
1139 {
1140 throw 0;
1141 }
1142 }
1143
1144 // now do full inlining, if requested
1145 if(cmdline.isset("inline"))
1146 {
1148
1149 if(cmdline.isset("show-custom-bitvector-analysis") ||
1150 cmdline.isset("custom-bitvector-analysis"))
1151 {
1155 }
1156
1157 log.status() << "Performing full inlining" << messaget::eom;
1159 }
1160
1161 if(cmdline.isset("show-custom-bitvector-analysis") ||
1162 cmdline.isset("custom-bitvector-analysis"))
1163 {
1164 log.status() << "Propagating Constants" << messaget::eom;
1165 constant_propagator_ait constant_propagator_ai(goto_model);
1167 }
1168
1169 if(cmdline.isset("escape-analysis"))
1170 {
1174
1175 // recalculate numbers, etc.
1176 goto_model.goto_functions.update();
1177
1178 log.status() << "Escape Analysis" << messaget::eom;
1179 escape_analysist escape_analysis;
1180 escape_analysis(goto_model);
1181 escape_analysis.instrument(goto_model);
1182
1183 // inline added functions, they are often small
1185
1186 // recalculate numbers, etc.
1187 goto_model.goto_functions.update();
1188 }
1189
1190 if(cmdline.isset("loop-contracts-file"))
1191 {
1192 const auto file_name = cmdline.get_value("loop-contracts-file");
1193 contracts_wranglert contracts_wrangler(
1194 goto_model, file_name, ui_message_handler);
1195 }
1196
1197 // Initialize loop contract config from cmdline.
1198 loop_contract_configt loop_contract_config = {
1202
1203 if(
1206 {
1207 // After instrumentation, all annotated loops will be transformed to
1208 // loops execute exactly once. CBMC by default unwinds transformed loops
1209 // by twice.
1210 // Users may want to disable the default unwinding to avoid duplicate
1211 // assertions.
1212 log.warning() << "**** WARNING: transformed loops will not be unwound "
1213 << "after applying loop contracts. Note that transformed "
1214 << "loops require at least unwinding bounds 2 to pass "
1215 << "the unwinding assertions." << messaget::eom;
1216 }
1217
1218 bool use_dfcc = cmdline.isset(FLAG_DFCC);
1219 if(use_dfcc)
1220 {
1221 if(cmdline.get_values(FLAG_DFCC).size() != 1)
1222 {
1224 "Redundant options detected",
1225 "--" FLAG_DFCC,
1226 "Use a single " FLAG_DFCC " option");
1227 }
1228
1230 log.status() << "Trying to force one backedge per target" << messaget::eom;
1232
1233 const irep_idt harness_id(cmdline.get_value(FLAG_DFCC));
1234
1235 std::set<irep_idt> to_replace(
1236 cmdline.get_values(FLAG_REPLACE_CALL).begin(),
1237 cmdline.get_values(FLAG_REPLACE_CALL).end());
1238
1239 if(
1240 !cmdline.get_values(FLAG_ENFORCE_CONTRACT).empty() &&
1241 !cmdline.get_values(FLAG_ENFORCE_CONTRACT_REC).empty())
1242 {
1244 "Mutually exclusive options detected",
1246 "Use either --" FLAG_ENFORCE_CONTRACT
1247 " or --" FLAG_ENFORCE_CONTRACT_REC);
1248 }
1249
1250 auto &to_enforce = !cmdline.get_values(FLAG_ENFORCE_CONTRACT_REC).empty()
1252 : cmdline.get_values(FLAG_ENFORCE_CONTRACT);
1253
1254 bool allow_recursive_calls =
1255 !cmdline.get_values(FLAG_ENFORCE_CONTRACT_REC).empty();
1256
1257 std::set<std::string> to_exclude_from_nondet_static(
1258 cmdline.get_values("nondet-static-exclude").begin(),
1259 cmdline.get_values("nondet-static-exclude").end());
1260
1261 dfcc(
1262 options,
1263 goto_model,
1264 harness_id,
1265 to_enforce.empty() ? std::optional<irep_idt>{}
1266 : std::optional<irep_idt>{to_enforce.front()},
1267 allow_recursive_calls,
1268 to_replace,
1269 loop_contract_config,
1270 to_exclude_from_nondet_static,
1271 log.get_message_handler());
1272 }
1273 else if((cmdline.isset(FLAG_LOOP_CONTRACTS) ||
1274 cmdline.isset(FLAG_REPLACE_CALL) ||
1276 {
1278 log.status() << "Trying to force one backedge per target" << messaget::eom;
1280 code_contractst contracts(goto_model, log, loop_contract_config);
1281
1282 std::set<std::string> to_replace(
1283 cmdline.get_values(FLAG_REPLACE_CALL).begin(),
1284 cmdline.get_values(FLAG_REPLACE_CALL).end());
1285
1286 std::set<std::string> to_enforce(
1287 cmdline.get_values(FLAG_ENFORCE_CONTRACT).begin(),
1288 cmdline.get_values(FLAG_ENFORCE_CONTRACT).end());
1289
1290 std::set<std::string> to_exclude_from_nondet_static(
1291 cmdline.get_values("nondet-static-exclude").begin(),
1292 cmdline.get_values("nondet-static-exclude").end());
1293
1294 // It's important to keep the order of contracts instrumentation, i.e.,
1295 // first replacement then enforcement. We rely on contract replacement
1296 // and inlining of sub-function calls to properly annotate all
1297 // assignments.
1298 contracts.replace_calls(to_replace);
1299 contracts.enforce_contracts(to_enforce, to_exclude_from_nondet_static);
1300
1301 if(cmdline.isset(FLAG_LOOP_CONTRACTS))
1302 {
1303 contracts.apply_loop_contracts(to_exclude_from_nondet_static);
1304 }
1305 }
1306
1307 if(cmdline.isset("value-set-fi-fp-removal"))
1308 {
1311 }
1312
1313 // replace function pointers, if explicitly requested
1314 if(cmdline.isset("remove-function-pointers"))
1315 {
1317 }
1318 else if(cmdline.isset("remove-const-function-pointers"))
1319 {
1321 }
1322
1323 if(cmdline.isset("replace-calls"))
1324 {
1326
1327 replace_callst replace_calls;
1328 replace_calls(goto_model, cmdline.get_values("replace-calls"));
1329 }
1330
1331 if(cmdline.isset("function-inline"))
1332 {
1333 std::string function=cmdline.get_value("function-inline");
1334 PRECONDITION(!function.empty());
1335
1336 bool caching=!cmdline.isset("no-caching");
1337
1339
1340 log.status() << "Inlining calls of function '" << function << "'"
1341 << messaget::eom;
1342
1343 if(!cmdline.isset("log"))
1344 {
1346 goto_model, function, ui_message_handler, true, caching);
1347 }
1348 else
1349 {
1350 std::string filename=cmdline.get_value("log");
1351 bool have_file=!filename.empty() && filename!="-";
1352
1354 goto_model, function, ui_message_handler, true, caching);
1355
1356 if(have_file)
1357 {
1358 std::ofstream of(widen_if_needed(filename));
1359
1360 if(!of)
1361 throw "failed to open file "+filename;
1362
1363 of << result;
1364 of.close();
1365 }
1366 else
1367 {
1368 std::cout << result << '\n';
1369 }
1370 }
1371
1372 goto_model.goto_functions.update();
1373 goto_model.goto_functions.compute_loop_numbers();
1374 }
1375
1376 if(cmdline.isset("partial-inline"))
1377 {
1379
1380 log.status() << "Partial inlining" << messaget::eom;
1382
1383 goto_model.goto_functions.update();
1384 goto_model.goto_functions.compute_loop_numbers();
1385 }
1386
1387 if(cmdline.isset("remove-calls-no-body"))
1388 {
1389 log.status() << "Removing calls to functions without a body"
1390 << messaget::eom;
1391
1392 remove_calls_no_bodyt remove_calls_no_body;
1393 remove_calls_no_body(goto_model.goto_functions, ui_message_handler);
1394
1395 goto_model.goto_functions.update();
1396 goto_model.goto_functions.compute_loop_numbers();
1397 }
1398
1399 if(cmdline.isset("constant-propagator"))
1400 {
1403
1404 log.status() << "Propagating Constants" << messaget::eom;
1405 log.warning() << "**** WARNING: Constant propagation as performed by "
1406 "goto-instrument is not expected to be sound. Do not use "
1407 "--constant-propagator if soundness is important for your "
1408 "use case."
1409 << messaget::eom;
1410
1411 constant_propagator_ait constant_propagator_ai(goto_model);
1413 }
1414
1415 if(cmdline.isset("generate-function-body"))
1416 {
1417 optionst c_object_factory_options;
1418 parse_c_object_factory_options(cmdline, c_object_factory_options);
1419 c_object_factory_parameterst object_factory_parameters(
1420 c_object_factory_options);
1421
1422 auto generate_implementation = generate_function_bodies_factory(
1423 cmdline.get_value("generate-function-body-options"),
1424 object_factory_parameters,
1425 goto_model.symbol_table,
1428 std::regex(cmdline.get_value("generate-function-body")),
1429 *generate_implementation,
1430 goto_model,
1432 }
1433
1434 if(cmdline.isset("generate-havocing-body"))
1435 {
1436 optionst c_object_factory_options;
1437 parse_c_object_factory_options(cmdline, c_object_factory_options);
1438 c_object_factory_parameterst object_factory_parameters(
1439 c_object_factory_options);
1440
1441 auto options_split =
1442 split_string(cmdline.get_value("generate-havocing-body"), ',');
1443 if(options_split.size() < 2)
1445 "not enough arguments for this option", "--generate-havocing-body"};
1446
1447 if(options_split.size() == 2)
1448 {
1449 auto generate_implementation = generate_function_bodies_factory(
1450 std::string{"havoc,"} + options_split.back(),
1451 object_factory_parameters,
1452 goto_model.symbol_table,
1455 std::regex(options_split[0]),
1456 *generate_implementation,
1457 goto_model,
1459 }
1460 else
1461 {
1462 CHECK_RETURN(options_split.size() % 2 == 1);
1463 for(size_t i = 1; i + 1 < options_split.size(); i += 2)
1464 {
1465 auto generate_implementation = generate_function_bodies_factory(
1466 std::string{"havoc,"} + options_split[i + 1],
1467 object_factory_parameters,
1468 goto_model.symbol_table,
1471 options_split[0],
1472 options_split[i],
1473 *generate_implementation,
1474 goto_model,
1476 }
1477 }
1478 }
1479
1480 // add generic checks, if needed
1483
1484 // check for uninitalized local variables
1485 if(cmdline.isset("uninitialized-check"))
1486 {
1487 log.status() << "Adding checks for uninitialized local variables"
1488 << messaget::eom;
1490 }
1491
1492 // check for maximum call stack size
1493 if(cmdline.isset("stack-depth"))
1494 {
1495 log.status() << "Adding check for maximum call stack size" << messaget::eom;
1497 goto_model,
1498 safe_string2size_t(cmdline.get_value("stack-depth")),
1500 }
1501
1502 // ignore default/user-specified initialization of variables with static
1503 // lifetime
1504 if(cmdline.isset("nondet-static-exclude"))
1505 {
1506 log.status() << "Adding nondeterministic initialization "
1507 "of static/global variables except for "
1508 "the specified ones."
1509 << messaget::eom;
1510 std::set<std::string> to_exclude(
1511 cmdline.get_values("nondet-static-exclude").begin(),
1512 cmdline.get_values("nondet-static-exclude").end());
1513 nondet_static(goto_model, to_exclude);
1514 }
1515 else if(cmdline.isset("nondet-static"))
1516 {
1517 log.status() << "Adding nondeterministic initialization "
1518 "of static/global variables"
1519 << messaget::eom;
1521 }
1522
1523 if(cmdline.isset("slice-global-inits"))
1524 {
1526
1527 log.status() << "Slicing away initializations of unused global variables"
1528 << messaget::eom;
1530 }
1531
1532 if(cmdline.isset("string-abstraction"))
1533 {
1536
1537 log.status() << "String Abstraction" << messaget::eom;
1539 }
1540
1541 // some analyses require function pointer removal and partial inlining
1542
1543 if(cmdline.isset("remove-pointers") ||
1544 cmdline.isset("race-check") ||
1545 cmdline.isset("mm") ||
1546 cmdline.isset("isr") ||
1547 cmdline.isset("concurrency"))
1548 {
1550
1551 log.status() << "Pointer Analysis" << messaget::eom;
1552 const namespacet ns(goto_model.symbol_table);
1553 value_set_analysist value_set_analysis(ns);
1554 value_set_analysis(goto_model);
1555
1556 if(cmdline.isset("remove-pointers"))
1557 {
1558 // removing pointers
1559 log.status() << "Removing Pointers" << messaget::eom;
1560 remove_pointers(goto_model, value_set_analysis, ui_message_handler);
1561 }
1562
1563 if(cmdline.isset("race-check"))
1564 {
1565 log.status() << "Adding Race Checks" << messaget::eom;
1566 race_check(value_set_analysis, goto_model, ui_message_handler);
1567 }
1568
1569 if(cmdline.isset("mm"))
1570 {
1571 std::string mm=cmdline.get_value("mm");
1572 memory_modelt model;
1573
1574 // strategy of instrumentation
1575 instrumentation_strategyt inst_strategy;
1576 if(cmdline.isset("one-event-per-cycle"))
1577 inst_strategy=one_event_per_cycle;
1578 else if(cmdline.isset("minimum-interference"))
1579 inst_strategy=min_interference;
1580 else if(cmdline.isset("read-first"))
1581 inst_strategy=read_first;
1582 else if(cmdline.isset("write-first"))
1583 inst_strategy=write_first;
1584 else if(cmdline.isset("my-events"))
1585 inst_strategy=my_events;
1586 else
1587 /* default: instruments all unsafe pairs */
1588 inst_strategy=all;
1589
1590 const unsigned max_var=
1591 cmdline.isset("max-var")?
1592 unsafe_string2unsigned(cmdline.get_value("max-var")):0;
1593 const unsigned max_po_trans=
1594 cmdline.isset("max-po-trans")?
1595 unsafe_string2unsigned(cmdline.get_value("max-po-trans")):0;
1596
1597 if(mm=="tso")
1598 {
1599 log.status() << "Adding weak memory (TSO) Instrumentation"
1600 << messaget::eom;
1601 model=TSO;
1602 }
1603 else if(mm=="pso")
1604 {
1605 log.status() << "Adding weak memory (PSO) Instrumentation"
1606 << messaget::eom;
1607 model=PSO;
1608 }
1609 else if(mm=="rmo")
1610 {
1611 log.status() << "Adding weak memory (RMO) Instrumentation"
1612 << messaget::eom;
1613 model=RMO;
1614 }
1615 else if(mm=="power")
1616 {
1617 log.status() << "Adding weak memory (Power) Instrumentation"
1618 << messaget::eom;
1619 model=Power;
1620 }
1621 else
1622 {
1623 log.error() << "Unknown weak memory model '" << mm << "'"
1624 << messaget::eom;
1625 model=Unknown;
1626 }
1627
1629
1630 if(cmdline.isset("force-loop-duplication"))
1631 loops=all_loops;
1632 if(cmdline.isset("no-loop-duplication"))
1633 loops=no_loop;
1634
1635 if(model!=Unknown)
1637 model,
1638 value_set_analysis,
1639 goto_model,
1640 cmdline.isset("scc"),
1641 inst_strategy,
1642 !cmdline.isset("cfg-kill"),
1643 cmdline.isset("no-dependencies"),
1644 loops,
1645 max_var,
1646 max_po_trans,
1647 !cmdline.isset("no-po-rendering"),
1648 cmdline.isset("render-cluster-file"),
1649 cmdline.isset("render-cluster-function"),
1650 cmdline.isset("cav11"),
1651 cmdline.isset("hide-internals"),
1653 cmdline.isset("ignore-arrays"));
1654 }
1655
1656 // Interrupt handler
1657 if(cmdline.isset("isr"))
1658 {
1659 log.status() << "Instrumenting interrupt handler" << messaget::eom;
1660 interrupt(
1661 value_set_analysis,
1662 goto_model,
1663 cmdline.get_value("isr"),
1665 }
1666
1667 // Memory-mapped I/O
1668 if(cmdline.isset("mmio"))
1669 {
1670 log.status() << "Instrumenting memory-mapped I/O" << messaget::eom;
1671 mmio(value_set_analysis, goto_model, ui_message_handler);
1672 }
1673
1674 if(cmdline.isset("concurrency"))
1675 {
1676 log.status() << "Sequentializing concurrency" << messaget::eom;
1677 concurrency(value_set_analysis, goto_model);
1678 }
1679 }
1680
1681 if(cmdline.isset("interval-analysis"))
1682 {
1683 log.status() << "Interval analysis" << messaget::eom;
1685 }
1686
1687 if(cmdline.isset("havoc-loops"))
1688 {
1689 log.status() << "Havocking loops" << messaget::eom;
1691 }
1692
1693 if(cmdline.isset("k-induction"))
1694 {
1695 bool base_case=cmdline.isset("base-case");
1696 bool step_case=cmdline.isset("step-case");
1697
1698 if(step_case && base_case)
1699 throw "please specify only one of --step-case and --base-case";
1700 else if(!step_case && !base_case)
1701 throw "please specify one of --step-case and --base-case";
1702
1703 unsigned k=unsafe_string2unsigned(cmdline.get_value("k-induction"));
1704
1705 if(k==0)
1706 throw "please give k>=1";
1707
1708 log.status() << "Instrumenting k-induction for k=" << k << ", "
1709 << (base_case ? "base case" : "step case") << messaget::eom;
1710
1711 k_induction(goto_model, base_case, step_case, k);
1712 }
1713
1714 if(cmdline.isset("function-enter"))
1715 {
1716 log.status() << "Function enter instrumentation" << messaget::eom;
1718 goto_model,
1719 cmdline.get_value("function-enter"));
1720 }
1721
1722 if(cmdline.isset("function-exit"))
1723 {
1724 log.status() << "Function exit instrumentation" << messaget::eom;
1726 goto_model,
1727 cmdline.get_value("function-exit"));
1728 }
1729
1730 if(cmdline.isset("branch"))
1731 {
1732 log.status() << "Branch instrumentation" << messaget::eom;
1733 branch(
1734 goto_model,
1735 cmdline.get_value("branch"));
1736 }
1737
1738 // add failed symbols
1739 add_failed_symbols(goto_model.symbol_table);
1740
1741 // recalculate numbers, etc.
1742 goto_model.goto_functions.update();
1743
1744 // add loop ids
1745 goto_model.goto_functions.compute_loop_numbers();
1746
1747 // label the assertions
1749
1750 nondet_volatile(goto_model, options);
1751
1752 // reachability slice?
1753 if(cmdline.isset("reachability-slice"))
1754 {
1756
1757 log.status() << "Performing a reachability slice" << messaget::eom;
1758
1759 // reachability_slicer requires that the model has unique location numbers:
1760 goto_model.goto_functions.update();
1761
1762 if(cmdline.isset("property"))
1763 {
1765 goto_model, cmdline.get_values("property"), ui_message_handler);
1766 }
1767 else
1769 }
1770
1771 if(cmdline.isset("fp-reachability-slice"))
1772 {
1774
1775 log.status() << "Performing a function pointer reachability slice"
1776 << messaget::eom;
1778 goto_model,
1779 cmdline.get_comma_separated_values("fp-reachability-slice"),
1781 }
1782
1783 // full slice?
1784 if(cmdline.isset("full-slice"))
1785 {
1789 // full_slicer requires that the model has unique location numbers:
1790 goto_model.goto_functions.update();
1791
1792 log.warning() << "**** WARNING: Experimental option --full-slice, "
1793 << "analysis results may be unsound. See "
1794 << "https://github.com/diffblue/cbmc/issues/260"
1795 << messaget::eom;
1796 log.status() << "Performing a full slice" << messaget::eom;
1797 if(cmdline.isset("property"))
1799 goto_model, cmdline.get_values("property"), ui_message_handler);
1800 else
1801 {
1803 }
1804 }
1805
1806 // splice option
1807 if(cmdline.isset("splice-call"))
1808 {
1809 log.status() << "Performing call splicing" << messaget::eom;
1810 std::string callercallee=cmdline.get_value("splice-call");
1811 if(splice_call(
1812 goto_model.goto_functions,
1813 callercallee,
1814 goto_model.symbol_table,
1816 throw 0;
1817 }
1818
1819 // aggressive slicer
1820 if(cmdline.isset("aggressive-slice"))
1821 {
1823
1824 // reachability_slicer requires that the model has unique location numbers:
1825 goto_model.goto_functions.update();
1826
1827 log.status() << "Slicing away initializations of unused global variables"
1828 << messaget::eom;
1830
1831 log.status() << "Performing an aggressive slice" << messaget::eom;
1833
1834 if(cmdline.isset("aggressive-slice-call-depth"))
1835 aggressive_slicer.call_depth =
1836 safe_string2unsigned(cmdline.get_value("aggressive-slice-call-depth"));
1837
1838 if(cmdline.isset("aggressive-slice-preserve-function"))
1839 aggressive_slicer.preserve_functions(
1840 cmdline.get_values("aggressive-slice-preserve-function"));
1841
1842 if(cmdline.isset("property"))
1843 aggressive_slicer.user_specified_properties =
1844 cmdline.get_values("property");
1845
1846 if(cmdline.isset("aggressive-slice-preserve-functions-containing"))
1847 aggressive_slicer.name_snippets =
1848 cmdline.get_values("aggressive-slice-preserve-functions-containing");
1849
1850 aggressive_slicer.preserve_all_direct_paths =
1851 cmdline.isset("aggressive-slice-preserve-all-direct-paths");
1852
1853 aggressive_slicer.doit();
1854
1855 goto_model.goto_functions.update();
1856
1857 log.status() << "Performing a reachability slice" << messaget::eom;
1858 if(cmdline.isset("property"))
1859 {
1861 goto_model, cmdline.get_values("property"), ui_message_handler);
1862 }
1863 else
1865 }
1866
1867 if(cmdline.isset("ensure-one-backedge-per-target"))
1868 {
1869 log.status() << "Trying to force one backedge per target" << messaget::eom;
1871 }
1872
1873 // recalculate numbers, etc.
1874 goto_model.goto_functions.update();
1875}
1876
1879{
1880 std::cout << '\n'
1881 << banner_string("Goto-Instrument", CBMC_VERSION) << '\n'
1882 << align_center_with_border("Copyright (C) 2008-2013") << '\n'
1883 << align_center_with_border("Daniel Kroening") << '\n'
1884 << align_center_with_border("kroening@kroening.com") << '\n';
1885
1886 // clang-format off
1887 std::cout << help_formatter(
1888 "\n"
1889 "Usage: \tPurpose:\n"
1890 "\n"
1891 " {bgoto-instrument} [{y-?}] [{y-h}] [{y--help}] \t show this help\n"
1892 " {bgoto-instrument} {y--version} \t show version and exit\n"
1893 " {bgoto-instrument} [options] {uin} [{uout}] \t perform analysis or"
1894 " instrumentation\n"
1895 "\n"
1896 "Dump Source:\n"
1898 " {y--horn} \t print program as constrained horn clauses\n"
1899 "\n"
1900 "Diagnosis:\n"
1903 " {y--show-symbol-table} \t show loaded symbol table\n"
1904 " {y--list-symbols} \t list symbols with type information\n"
1907 " {y--show-locations} \t show all source locations\n"
1908 " {y--dot} \t generate CFG graph in DOT format\n"
1909 " {y--print-internal-representation} \t show verbose internal"
1910 " representation of the program\n"
1911 " {y--list-undefined-functions} \t list functions without body\n"
1912 " {y--list-calls-args} \t list all function calls with their arguments\n"
1913 " {y--call-graph} \t show graph of function calls\n"
1914 " {y--reachable-call-graph} \t show graph of function calls potentially"
1915 " reachable from main function\n"
1918 " {y--validate-goto-binary} \t check the well-formedness of the passed in"
1919 " goto binary and then exit\n"
1920 " {y--interpreter} \t do concrete execution\n"
1921 "\n"
1922 "Data-flow analyses:\n"
1923 " {y--show-struct-alignment} \t show struct members that might be"
1924 " concurrently accessed\n"
1925 " {y--show-threaded} \t show instructions that may be executed by more than"
1926 " one thread\n"
1927 " {y--show-local-safe-pointers} \t show pointer expressions that are"
1928 " trivially dominated by a not-null check\n"
1929 " {y--show-safe-dereferences} \t show pointer expressions that are"
1930 " trivially dominated by a not-null check *and* used as a dereference"
1931 " operand\n"
1932 " {y--show-value-sets} \t show points-to information (using value sets)\n"
1933 " {y--show-global-may-alias} \t show may-alias information over globals\n"
1934 " {y--show-local-bitvector-analysis} \t show procedure-local pointer"
1935 " analysis\n"
1936 " {y--escape-analysis} \t perform escape analysis\n"
1937 " {y--show-escape-analysis} \t show results of escape analysis\n"
1938 " {y--custom-bitvector-analysis} \t perform configurable bitvector"
1939 " analysis\n"
1940 " {y--show-custom-bitvector-analysis} \t show results of configurable"
1941 " bitvector analysis\n"
1942 " {y--interval-analysis} \t perform interval analysis\n"
1943 " {y--show-intervals} \t show results of interval analysis\n"
1944 " {y--show-uninitialized} \t show maybe-uninitialized variables\n"
1945 " {y--show-points-to} \t show points-to information\n"
1946 " {y--show-rw-set} \t show read-write sets\n"
1947 " {y--show-call-sequences} \t show function call sequences\n"
1948 " {y--show-reaching-definitions} \t show reaching definitions\n"
1949 " {y--show-dependence-graph} \t show program-dependence graph\n"
1950 " {y--show-sese-regions} \t show single-entry-single-exit regions\n"
1951 "\n"
1952 "Safety checks:\n"
1953 " {y--no-assertions} \t ignore user assertions\n"
1956 " {y--stack-depth} {un} \t add check that call stack size of non-inlined"
1957 " functions never exceeds {un}\n"
1958 " {y--race-check} \t add floating-point data race checks\n"
1959 "\n"
1960 "Semantic transformations:\n"
1962 " {y--isr} {ufunction} \t instruments an interrupt service routine\n"
1963 " {y--mmio} \t instruments memory-mapped I/O\n"
1964 " {y--nondet-static} \t add nondeterministic initialization of variables"
1965 " with static lifetime\n"
1966 " {y--nondet-static-exclude} {ue} \t same as nondet-static except for the"
1967 " variable {ue} (use multiple times if required)\n"
1968 " {y--nondet-static-matching} {ur} \t add nondeterministic initialization"
1969 " of variables with static lifetime matching regex {ur}\n"
1970 " {y--function-enter} {uf}, {y--function-exit} {uf}, {y--branch} {uf} \t"
1971 " instruments a call to {uf} at the beginning, the exit, or a branch point,"
1972 " respectively\n"
1973 " {y--splice-call} {ucaller},{ucallee} \t prepends a call to {ucallee} in"
1974 " the body of {ucaller}\n"
1975 " {y--check-call-sequence} {useq} \t instruments checks to assert that all"
1976 " call sequences match {useq}\n"
1977 " {y--undefined-function-is-assume-false} \t convert each call to an"
1978 " undefined function to assume(false)\n"
1983 " {y--add-library} \t add models of C library functions\n"
1986 " {y--remove-function-body} {uf} remove the implementation of function {uf}"
1987 " (may be repeated)\n"
1990 "\n"
1991 "Semantics-preserving transformations:\n"
1992 " {y--ensure-one-backedge-per-target} \t transform loop bodies such that"
1993 " there is a single edge back to the loop head\n"
1994 " {y--drop-unused-functions} \t drop functions trivially unreachable from"
1995 " main function\n"
1997 " {y--constant-propagator} \t propagate constants and simplify"
1998 " expressions\n"
1999 " {y--inline} \t perform full inlining\n"
2000 " {y--partial-inline} \t perform partial inlining\n"
2001 " {y--function-inline} {ufunction} \t transitively inline all calls"
2002 " {ufunction} makes\n"
2003 " {y--no-caching} \t disable caching of intermediate results during"
2004 " transitive function inlining\n"
2005 " {y--log} {ufile} \t log in JSON format which code segments were inlined,"
2006 " use with {y--function-inline}\n"
2007 " {y--remove-function-pointers} \t replace function pointers by case"
2008 " statement over function calls\n"
2010 " {y--value-set-fi-fp-removal} \t build flow-insensitive value set and"
2011 " replace function pointers by a case statement over the possible"
2012 " assignments. If the set of possible assignments is empty the function"
2013 " pointer is removed using the standard remove-function-pointers pass.\n"
2014 "\n"
2015 "Loop information and transformations:\n"
2017 " {y--unwindset-file_<file>} \t read unwindset from file\n"
2018 " {y--partial-loops} \t permit paths with partial loops\n"
2019 " {y--unwinding-assertions} \t generate unwinding assertions"
2020 " (enabled by default)\n"
2021 " {y--no-unwinding-assertions} \t do not generate unwinding assertions\n"
2022 " {y--continue-as-loops} \t add loop for remaining iterations after"
2023 " unwound part\n"
2024 " {y--k-induction} {uk} \t check loops with k-induction\n"
2025 " {y--step-case} \t k-induction: do step-case\n"
2026 " {y--base-case} \t k-induction: do base-case\n"
2027 " {y--havoc-loops} \t over-approximate all loops\n"
2028 " {y--accelerate} \t add loop accelerators\n"
2029 " {y--z3} \t use Z3 when computing loop accelerators\n"
2030 " {y--skip-loops {uloop-ids} \t add gotos to skip selected loops during"
2031 " execution\n"
2032 " {y--show-lexical-loops} \t show single-entry-single-back-edge loops\n"
2033 " {y--show-natural-loops} \t show natural loop heads\n"
2034 "\n"
2035 "Memory model instrumentations:\n"
2037 "\n"
2038 "Slicing:\n"
2041 " {y--full-slice} \t slice away instructions that don't affect assertions\n"
2042 " {y--property} {uid} \t slice with respect to specific property only\n"
2043 " {y--slice-global-inits} \t slice away initializations of unused global"
2044 " variables\n"
2045 " {y--aggressive-slice} \t remove bodies of any functions not on the"
2046 " shortest path between the start function and the function containing the"
2047 " property/properties\n"
2048 " {y--aggressive-slice-call-depth} {un} \t used with aggressive-slice,"
2049 " preserves all functions within {un} function calls of the functions on"
2050 " the shortest path\n"
2051 " {y--aggressive-slice-preserve-function} {uf} \t force the aggressive"
2052 " slicer to preserve function {uf}\n"
2053 " {y--aggressive-slice-preserve-functions-containing} {uf} \t force the"
2054 " aggressive slicer to preserve all functions with names containing {uf}\n"
2055 " {y--aggressive-slice-preserve-all-direct-paths} \t force aggressive"
2056 " slicer to preserve all direct paths\n"
2057 "\n"
2058 "Code contracts:\n"
2059 HELP_DFCC
2067 "\n"
2068 "User-interface options:\n"
2070 " {y--xml} \t output files in XML where supported\n"
2071 " {y--xml-ui} \t use XML-formatted output\n"
2072 " {y--json-ui} \t use JSON-formatted output\n"
2073 " {y--verbosity} {u#} \t verbosity level\n"
2075 "\n");
2076 // clang-format on
2077}
void accelerate_functions(goto_modelt &goto_model, message_handlert &message_handler, bool use_z3, guard_managert &guard_manager)
Loop Acceleration.
void add_failed_symbols(symbol_table_baset &symbol_table)
Create a failed-dereference symbol for all symbols in the given table that need one (i....
Pointer Dereferencing.
void print_struct_alignment_problems(const symbol_table_baset &symbol_table, std::ostream &out)
Alignment Checks.
void cprover_c_library_factory(const std::set< irep_idt > &functions, const symbol_table_baset &symbol_table, symbol_table_baset &dest_symbol_table, message_handlert &message_handler)
#define HELP_ANSI_C_LANGUAGE
configt config
Definition config.cpp:25
void branch(goto_modelt &goto_model, const irep_idt &id)
Definition branch.cpp:21
Branch Instrumentation.
void parse_c_object_factory_options(const cmdlinet &cmdline, optionst &options)
Parse the c object factory parameters from a given command line.
Function Call Graphs.
static void list_calls_and_arguments(const namespacet &ns, const goto_programt &goto_program)
void check_call_sequence(const goto_modelt &goto_model)
void show_call_sequences(const irep_idt &caller, const goto_programt &goto_program)
Memory-mapped I/O Instrumentation for Goto Programs.
void show_class_hierarchy(const class_hierarchyt &hierarchy, ui_message_handlert &message_handler, bool children_only)
Output the class hierarchy.
Class Hierarchy.
#define HELP_SHOW_CLASS_HIERARCHY
The aggressive slicer removes the body of all the functions except those on the shortest path,...
std::list< std::string > user_specified_properties
void doit()
Removes the body of all functions except those on the shortest path or functions that are reachable f...
std::list< std::string > name_snippets
void preserve_functions(const std::list< std::string > &function_list)
Adds a list of functions to the set of functions for the aggressive slicer to preserve.
virtual void output(const namespacet &ns, const irep_idt &function_id, const goto_programt &goto_program, std::ostream &out) const
Output the abstract states for a single function.
Definition ai.cpp:39
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
A call graph (https://en.wikipedia.org/wiki/Call_graph) for a GOTO model or GOTO functions collection...
Definition call_graph.h:44
void output_dot(std::ostream &out) const
void output(std::ostream &out) const
static call_grapht create_from_root_function(const goto_modelt &model, const irep_idt &root, bool collect_callsites)
Definition call_graph.h:53
void output_xml(std::ostream &out) const
Non-graph-based representation of the class hierarchy.
void output_dot(std::ostream &) const
Output class hierarchy in Graphviz DOT format.
void apply_loop_contracts(const std::set< std::string > &to_exclude_from_nondet_init={})
Applies loop contract transformations.
void enforce_contracts(const std::set< std::string > &to_enforce, const std::set< std::string > &to_exclude_from_nondet_init={})
Turn requires & ensures into assumptions and assertions for each of the named functions.
void replace_calls(const std::set< std::string > &to_replace)
Replace all calls to each function in the to_replace set with that function's contract.
void check(const goto_modelt &, bool xml, std::ostream &)
bool empty() const
Definition dstring.h:89
void instrument(goto_modelt &)
void get(const std::string &executable)
This is a may analysis (i.e.
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
void help() override
display command line help
void do_remove_const_function_pointers_only()
Remove function pointers that can be resolved by analysing const variables (i.e.
int doit() override
invoke main modules
A generic container class for the GOTO intermediate representation of one function.
std::ostream & output(std::ostream &out) const
Output goto-program to given stream.
jsont output_log_json() const
Definition unwind.h:77
void output_dot(std::ostream &out) const
Definition graph.h:990
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
Definition json.h:27
void output(std::ostream &out, const goto_functiont &goto_function, const namespacet &ns) const
A very simple, cheap analysis to determine when dereference operations are trivially guarded by a che...
void output_safe_dereferences(std::ostream &stream, const goto_programt &program, const namespacet &ns)
Output safely dereferenced expressions per instruction in human-readable format.
void output(std::ostream &stream, const goto_programt &program, const namespacet &ns)
Output non-null expressions per instruction in human-readable format.
static unsigned eval_verbosity(const std::string &user_input, const message_levelt default_verbosity, message_handlert &dest)
Parse a (user-)provided string as a verbosity level and set it as the verbosity of dest.
Definition message.cpp:105
@ M_STATUS
Definition message.h:169
static eomt eom
Definition message.h:289
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:94
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
bool is_set(const std::string &option) const
N.B. opts.is_set("foo") does not imply opts.get_bool_option("foo")
Definition options.cpp:62
void set_option(const std::string &option, const bool value)
Definition options.cpp:28
ui_message_handlert ui_message_handler
void output(std::ostream &out) const
Definition points_to.cpp:33
void output(std::ostream &out, const goto_programt &goto_program, const namespacet &ns) const
Expression to hold a symbol (variable)
Definition std_expr.h:131
Symbol table entry.
Definition symbol.h:28
typet type
Type of symbol.
Definition symbol.h:31
irep_idt name
The unique identifier.
Definition symbol.h:40
void parse_unwind(const std::string &unwind)
Definition unwindset.cpp:23
void concurrency(value_setst &value_sets, goto_modelt &goto_model)
Encoding for Threaded Goto Programs.
#define HELP_CONFIG_LIBRARY
Definition config.h:77
Constant propagation.
#define HELP_REPLACE_CALL
Definition contracts.h:51
#define HELP_DISABLE_SIDE_EFFECT_CHECK
Definition contracts.h:38
#define FLAG_REPLACE_CALL
Definition contracts.h:50
#define FLAG_ENFORCE_CONTRACT
Definition contracts.h:55
#define HELP_LOOP_CONTRACTS
Definition contracts.h:33
#define FLAG_LOOP_CONTRACTS
Definition contracts.h:32
#define HELP_LOOP_CONTRACTS_NO_UNWIND
Definition contracts.h:42
#define HELP_ENFORCE_CONTRACT
Definition contracts.h:56
#define HELP_LOOP_CONTRACTS_FILE
Definition contracts.h:46
#define FLAG_DISABLE_SIDE_EFFECT_CHECK
Definition contracts.h:36
#define FLAG_LOOP_CONTRACTS_NO_UNWIND
Definition contracts.h:41
void count_eloc(const goto_modelt &goto_model)
void print_global_state_size(const goto_modelt &goto_model)
void print_path_lengths(const goto_modelt &goto_model)
void list_eloc(const goto_modelt &goto_model)
#define HELP_GOTO_PROGRAM_STATS
Definition count_eloc.h:30
void cprover_cpp_library_factory(const std::set< irep_idt > &functions, const symbol_table_baset &symbol_table, symbol_table_baset &dest_symbol_table, message_handlert &message_handler)
static void show_goto_functions(const goto_modelt &goto_model)
#define CPROVER_PREFIX
Field-insensitive, location-sensitive bitvector analysis.
Field-Sensitive Program Dependence Analysis, Litvak et al., FSE 2010.
#define FLAG_ENFORCE_CONTRACT_REC
Definition dfcc.h:62
#define FLAG_DFCC
Definition dfcc.h:54
#define HELP_DFCC
Definition dfcc.h:57
#define HELP_ENFORCE_CONTRACT_REC
Definition dfcc.h:64
void document_properties_latex(const goto_modelt &goto_model, std::ostream &out)
void document_properties_html(const goto_modelt &goto_model, std::ostream &out)
#define HELP_DOCUMENT_PROPERTIES
void dot(const goto_modelt &src, std::ostream &out)
Definition dot.cpp:359
Dump Goto-Program as DOT Graph.
void dump_cpp(const goto_functionst &src, const bool use_system_headers, const bool use_all_headers, const bool include_harness, const namespacet &ns, std::ostream &out)
Definition dump_c.cpp:1681
void dump_c(const goto_functionst &src, const bool use_system_headers, const bool use_all_headers, const bool include_harness, const namespacet &ns, std::ostream &out)
Definition dump_c.cpp:1668
void dump_c_type_header(const goto_functionst &src, const bool use_system_headers, const bool use_all_headers, const bool include_harness, const namespacet &ns, const std::string module, std::ostream &out)
Definition dump_c.cpp:1703
#define HELP_DUMP_C
Definition dump_c.h:51
bool ensure_one_backedge_per_target(goto_programt::targett &it, goto_programt &goto_program)
Ensure one backedge per target.
Field-insensitive, location-sensitive, over-approximative escape analysis.
Document and give macros for the exit codes of CPROVER binaries.
#define CPROVER_EXIT_CONVERSION_FAILED
Failure to convert / write to another format.
Definition exit_codes.h:62
#define CPROVER_EXIT_INTERNAL_ERROR
An error has been encountered during processing the requested analysis.
Definition exit_codes.h:45
#define CPROVER_EXIT_USAGE_ERROR
A usage error is returned when the command line is invalid or conflicting.
Definition exit_codes.h:33
#define CPROVER_EXIT_SUCCESS
Success indicates the required analysis has been performed without error.
Definition exit_codes.h:16
void property_slicer(goto_functionst &goto_functions, const namespacet &ns, const std::list< std::string > &properties, message_handlert &message_handler)
void full_slicer(goto_functionst &goto_functions, const namespacet &ns, const slicing_criteriont &criterion, message_handlert &message_handler)
void function_exit(goto_modelt &goto_model, const irep_idt &id)
Definition function.cpp:102
void function_enter(goto_modelt &goto_model, const irep_idt &id)
Definition function.cpp:77
Function Entering and Exiting.
void configure_gcc(const gcc_versiont &gcc_version)
std::unique_ptr< generate_function_bodiest > generate_function_bodies_factory(const std::string &options, const c_object_factory_parameterst &object_factory_parameters, const symbol_tablet &symbol_table, message_handlert &message_handler)
Create the type that actually generates the functions.
void generate_function_bodies(const std::regex &functions_regex, const generate_function_bodiest &generate_function_body, goto_modelt &model, message_handlert &message_handler)
Generate function bodies with some default behavior: assert-false, assume-false, assert-false-assume-...
#define HELP_REPLACE_FUNCTION_BODY
Field-insensitive, location-sensitive, over-approximative escape analysis.
static void transform_assertions_assumptions(goto_programt &goto_program, bool enable_assertions, bool enable_built_in_assertions, bool enable_assumptions)
Checks for Errors in C and Java Programs.
void goto_check_c(const irep_idt &function_identifier, goto_functionst::goto_functiont &goto_function, const namespacet &ns, const optionst &options, message_handlert &message_handler)
#define PARSE_OPTIONS_GOTO_CHECK(cmdline, options)
#define HELP_GOTO_CHECK
void goto_inline(goto_modelt &goto_model, message_handlert &message_handler, bool adjust_function)
Inline every function call into the entry_point() function.
void goto_function_inline(goto_modelt &goto_model, const irep_idt function, message_handlert &message_handler, bool adjust_function, bool caching)
Transitively inline all function calls made from a particular function.
void goto_partial_inline(goto_modelt &goto_model, message_handlert &message_handler, unsigned smallfunc_limit, bool adjust_function)
Inline all function calls to functions either marked as "inlined" or smaller than smallfunc_limit (by...
jsont goto_function_inline_and_log(goto_modelt &goto_model, const irep_idt function, message_handlert &message_handler, bool adjust_function, bool caching)
Function Inlining This gives a number of different interfaces to the function inlining functionality ...
Command Line Parsing.
#define forall_goto_program_instructions(it, program)
void remove_pointers(goto_modelt &goto_model, value_setst &value_sets, message_handlert &message_handler)
Remove dereferences in all expressions contained in the program goto_model.
#define HELP_REMOVE_POINTERS
void dfcc(const optionst &options, goto_modelt &goto_model, const irep_idt &harness_id, const std::optional< irep_idt > &to_check, const bool allow_recursive_calls, const std::set< irep_idt > &to_replace, const loop_contract_configt loop_contract_config, const std::set< std::string > &to_exclude_from_nondet_static, message_handlert &message_handler)
Applies function contracts transformation to GOTO model, using the dynamic frame condition checking a...
Definition dfcc.cpp:113
Guard Data Structure.
guard_expr_managert guard_managert
Definition guard.h:28
void havoc_loops(goto_modelt &goto_model)
Havoc Loops.
Help Formatter.
static help_formattert help_formatter(const std::string &s)
void horn_encoding(const goto_modelt &goto_model, std::ostream &out)
Horn-clause Encoding.
bool insert_final_assert_false(goto_modelt &goto_model, const std::string &function_to_instrument, message_handlert &message_handler)
Transform a goto program by inserting assert(false) at the end of a given function function_to_instru...
Insert final assert false into a function.
#define HELP_INSERT_FINAL_ASSERT_FALSE
void interpreter(const goto_modelt &goto_model, message_handlert &message_handler)
Interpreter for GOTO Programs.
static void interrupt(value_setst &value_sets, const symbol_tablet &symbol_table, const irep_idt &function_id, goto_programt &goto_program, const symbol_exprt &interrupt_handler, const rw_set_baset &isr_rw_set, message_handlert &message_handler)
Definition interrupt.cpp:58
Interrupt Instrumentation for Goto Programs.
void interval_analysis(goto_modelt &goto_model)
Initialises the abstract interpretation over interval domain and instruments instructions using inter...
Interval Analysis.
Interval Domain.
Over-approximate Concurrency for Threaded Goto Programs.
void k_induction(goto_modelt &goto_model, bool base_case, bool step_case, unsigned k)
k-induction
void label_function_pointer_call_sites(goto_modelt &goto_model)
This ensures that call instructions can be only one of two things:
Label function pointer call sites across a goto model.
Compute lexical loops in a goto_function.
void show_lexical_loops(const goto_modelt &goto_model, std::ostream &out)
Field-insensitive, location-sensitive bitvector analysis.
Local safe pointer analysis.
void show_loop_ids(ui_message_handlert::uit ui, const goto_modelt &goto_model)
Definition loop_ids.cpp:21
Loop IDs.
void mm_io(symbol_tablet &symbol_table, goto_functionst &goto_functions, message_handlert &message_handler)
Definition mm_io.cpp:154
Perform Memory-mapped I/O instrumentation.
static void mmio(value_setst &value_sets, const symbol_tablet &symbol_table, const irep_idt &function_id, goto_programt &goto_program, message_handlert &message_handler)
Definition mmio.cpp:24
Memory-mapped I/O Instrumentation for Goto Programs.
bool model_argc_argv(goto_modelt &goto_model, const std::list< std::string > &argv_args, bool model_argv, message_handlert &message_handler)
Set up argv to user-specified values (when model_argv is FALSE) or (when model_argv is TRUE) set up a...
#define HELP_ARGC_ARGV
Compute natural loops in a goto_function.
void show_natural_loops(const goto_modelt &goto_model, std::ostream &out)
void nondet_static_matching(goto_modelt &goto_model, const std::string &regex)
Nondeterministically initializes global scope variables that match the given regex.
static void nondet_static(const namespacet &ns, goto_modelt &goto_model, const irep_idt &fct_name)
Nondeterministically initializes global scope variables in a goto-function.
Nondeterministically initializes global scope variables, except for constants (such as string literal...
void parse_nondet_volatile_options(const cmdlinet &cmdline, optionst &options)
void nondet_volatile(goto_modelt &goto_model, const optionst &options)
Havoc reads from volatile expressions, if enabled in the options.
Volatile Variables.
#define HELP_NONDET_VOLATILE
Options.
void parameter_assignments(symbol_table_baset &symbol_table, goto_functionst &goto_functions)
removes returns
Add parameter assignments.
std::string align_center_with_border(const std::string &text)
Utility for displaying help centered messages borderered by "* *".
std::string banner_string(const std::string &front_end, const std::string &version)
Field-sensitive, location-insensitive points-to analysis.
static void race_check(value_setst &value_sets, symbol_table_baset &symbol_table, const irep_idt &function_id, goto_programt &goto_program, w_guardst &w_guards, message_handlert &message_handler)
Race Detection for Threaded Goto Programs.
void reachability_slicer(goto_modelt &goto_model, const bool include_forward_reachability, message_handlert &message_handler)
Perform reachability slicing on goto_model, with respect to the criterion given by all properties.
void function_path_reachability_slicer(goto_modelt &goto_model, const std::list< std::string > &functions_list, message_handlert &message_handler)
Perform reachability slicing on goto_model for selected functions.
#define HELP_FP_REACHABILITY_SLICER
#define HELP_REACHABILITY_SLICER
Range-based reaching definitions analysis (following Field- Sensitive Program Dependence Analysis,...
static bool read_goto_binary(const std::string &filename, symbol_tablet &, goto_functionst &, message_handlert &)
Read a goto binary from a file, but do not update config.
Read Goto Programs.
void remove_asm(goto_functionst &goto_functions, symbol_tablet &symbol_table, message_handlert &message_handler)
Replaces inline assembly instructions in the goto program (i.e., instructions of kind OTHER with a co...
bool has_asm(const goto_functionst &goto_functions)
returns true iff the given goto functions use asm instructions
Remove 'asm' statements by compiling them into suitable standard goto program instructions.
Remove calls to functions without a body.
#define HELP_REMOVE_CALLS_NO_BODY
#define HELP_REMOVE_CONST_FUNCTION_POINTERS
void remove_functions(goto_modelt &goto_model, const std::list< std::string > &names, message_handlert &message_handler)
Remove the body of all functions listed in "names" such that an analysis will treat it as a side-effe...
Remove function definition.
void remove_function_pointers(message_handlert &_message_handler, goto_modelt &goto_model, bool only_remove_const_fps)
Remove Indirect Function Calls.
void restore_returns(goto_modelt &goto_model)
restores return statements
void remove_returns(symbol_table_baset &symbol_table, goto_functionst &goto_functions)
removes returns
Replace function returns by assignments to global variables.
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Program Transformation.
void remove_unused_functions(goto_modelt &goto_model, message_handlert &message_handler)
Unused function removal.
void remove_virtual_functions(symbol_table_baset &symbol_table, goto_functionst &goto_functions)
Remove virtual function calls from all functions in the specified list and replace them with their mo...
Functions for replacing virtual function call with a static function calls in functions,...
#define HELP_REPLACE_CALLS
void parse_function_pointer_restriction_options_from_cmdline(const cmdlinet &cmdline, optionst &options)
void restrict_function_pointers(message_handlert &message_handler, goto_modelt &goto_model, const optionst &options)
Apply function pointer restrictions to a goto_model.
Given goto functions and a list of function parameters or globals that are function pointers with lis...
#define RESTRICT_FUNCTION_POINTER_OPT
#define RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT
#define HELP_RESTRICT_FUNCTION_POINTER
#define RESTRICT_FUNCTION_POINTER_BY_NAME_OPT
static std::optional< exprt > rewrite_rw_ok(exprt expr, const namespacet &ns)
Rewrite r/w/rw_ok expressions to ones including prophecy variables recording the state.
void rewrite_union(exprt &expr)
We rewrite u.c for unions u into byte_extract(u, 0), and { .c = v } into byte_update(NIL,...
Symbolic Execution.
Race Detection for Threaded Goto Programs.
Single-entry, single-exit region analysis.
void label_properties(goto_modelt &goto_model)
Set the properties to check.
#define HELP_SHOW_GOTO_FUNCTIONS
void show_locations(ui_message_handlert::uit ui, const irep_idt function_id, const goto_programt &goto_program)
Show program locations.
void show_properties(const namespacet &ns, const irep_idt &identifier, message_handlert &message_handler, ui_message_handlert::uit ui, const goto_programt &goto_program)
Show the properties.
#define HELP_SHOW_PROPERTIES
void show_symbol_table(const symbol_table_baset &symbol_table, ui_message_handlert &ui)
void show_symbol_table_brief(const symbol_table_baset &symbol_table, ui_message_handlert &ui)
Show the symbol table.
void show_value_sets(ui_message_handlert::uit ui, const goto_modelt &goto_model, const value_set_analysist &value_set_analysis)
Show Value Sets.
static bool skip_loops(goto_programt &goto_program, const loop_idst &loop_ids, messaget &message)
Skip over selected loops by adding gotos.
void slice_global_inits(goto_modelt &goto_model, message_handlert &message_handler)
Remove initialization of global variables that are not used in any function reachable from the entry ...
Remove initializations of unused global variables.
bool splice_call(goto_functionst &goto_functions, const std::string &callercallee, const symbol_table_baset &symbol_table, message_handlert &message_handler)
Harnessing for goto functions.
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
#define PRECONDITION(CONDITION)
Definition invariant.h:463
static void stack_depth(goto_programt &goto_program, const symbol_exprt &symbol, const std::size_t i_depth, const exprt &max_depth)
Stack depth checks.
unsigned safe_string2unsigned(const std::string &str, int base)
unsigned unsafe_string2unsigned(const std::string &str, int base)
std::size_t safe_string2size_t(const std::string &str, int base)
void string_abstraction(goto_modelt &goto_model, message_handlert &message_handler)
String Abstraction.
void split_string(const std::string &s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)
Loop contract configurations.
void thread_exit_instrumentation(goto_programt &goto_program)
void mutex_init_instrumentation(const symbol_tablet &symbol_table, goto_programt &goto_program, typet lock_type)
#define HELP_TIMESTAMP
Definition timestamper.h:14
#define HELP_FLUSH
Definition ui_message.h:108
void list_undefined_functions(const goto_modelt &goto_model, std::ostream &os)
void undefined_function_abort_path(goto_modelt &goto_model)
Handling of functions without body.
#define widen_if_needed(s)
Definition unicode.h:28
void add_uninitialized_locals_assertions(goto_modelt &goto_model)
void show_uninitialized(const goto_modelt &goto_model, std::ostream &out)
#define HELP_UNINITIALIZED_CHECK
Loop unwinding.
#define HELP_UNWINDSET
Definition unwindset.h:79
#define HELP_VALIDATE
Value Set Propagation.
value_set_analysis_templatet< value_set_domain_templatet< value_sett > > value_set_analysist
void value_set_fi_fp_removal(goto_modelt &goto_model, message_handlert &message_handler)
Builds the flow-insensitive value set for all function pointers and replaces function pointers with a...
flow insensitive value set function pointer removal
dstringt irep_idt
const char * CBMC_VERSION
void weak_memory(memory_modelt model, value_setst &value_sets, goto_modelt &goto_model, bool SCC, instrumentation_strategyt event_strategy, bool no_cfg_kill, bool no_dependencies, loop_strategyt duplicate_body, unsigned input_max_var, unsigned input_max_po_trans, bool render_po, bool render_file, bool render_function, bool cav11_option, bool hide_internals, message_handlert &message_handler, bool ignore_arrays)
#define HELP_WMM_FULL
Definition weak_memory.h:92
memory_modelt
Definition wmm.h:18
@ Unknown
Definition wmm.h:19
@ TSO
Definition wmm.h:20
@ RMO
Definition wmm.h:22
@ PSO
Definition wmm.h:21
@ Power
Definition wmm.h:23
loop_strategyt
Definition wmm.h:37
@ all_loops
Definition wmm.h:39
@ arrays_only
Definition wmm.h:38
@ no_loop
Definition wmm.h:40
instrumentation_strategyt
Definition wmm.h:27
@ my_events
Definition wmm.h:32
@ one_event_per_cycle
Definition wmm.h:33
@ min_interference
Definition wmm.h:29
@ read_first
Definition wmm.h:30
@ all
Definition wmm.h:28
@ write_first
Definition wmm.h:31
static void write_goto_binary(std::ostream &out, const symbol_table_baset &symbol_table, const goto_functionst &goto_functions, irep_serializationt &irepconverter)
Writes a goto program to disc, using goto binary format.
Write GOTO binaries.