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
49
50#include <analyses/call_graph.h>
56#include <analyses/guard.h>
69#include <ansi-c/gcc_version.h>
71#include <cpp/cprover_library.h>
75
76#include "alignment_checks.h"
77#include "branch.h"
78#include "call_sequences.h"
79#include "concurrency.h"
80#include "dot.h"
81#include "full_slicer.h"
82#include "function.h"
83#include "havoc_loops.h"
84#include "horn_encoding.h"
86#include "interrupt.h"
87#include "k_induction.h"
88#include "mmio.h"
89#include "nondet_static.h"
90#include "nondet_volatile.h"
91#include "points_to.h"
92#include "race_check.h"
93#include "remove_function.h"
94#include "rw_set.h"
95#include "show_locations.h"
96#include "skip_loops.h"
97#include "splice_call.h"
98#include "stack_depth.h"
100#include "undefined_functions.h"
101#include "unwind.h"
103
104#include <fstream> // IWYU pragma: keep
105#include <iostream>
106#include <memory>
107#include <sstream>
108
110
113{
114 if(cmdline.isset("version"))
115 {
116 std::cout << CBMC_VERSION << '\n';
118 }
119
120 if(cmdline.args.size()!=1 && cmdline.args.size()!=2)
121 {
122 help();
124 }
125
128
129 {
131
133
134 // configure gcc, if required -- get_goto_program will have set the config
136 {
137 gcc_versiont gcc_version;
138 gcc_version.get("gcc");
139 configure_gcc(gcc_version);
140 }
141
142 {
143 const bool validate_only = cmdline.isset("validate-goto-binary");
144
145 if(validate_only || cmdline.isset("validate-goto-model"))
146 {
148
149 if(validate_only)
150 {
152 }
153 }
154 }
155
156 // ignore default/user-specified initialization
157 // of matching variables with static lifetime
158 if(cmdline.isset("nondet-static-matching"))
159 {
160 log.status() << "Adding nondeterministic initialization "
161 "of matching static/global variables"
162 << messaget::eom;
164 goto_model, cmdline.get_value("nondet-static-matching"));
165 }
166
168
169 if(cmdline.isset("validate-goto-model"))
170 {
172 }
173
174 {
175 bool unwind_given=cmdline.isset("unwind");
176 bool unwindset_given=cmdline.isset("unwindset");
177 bool unwindset_file_given=cmdline.isset("unwindset-file");
178
179 if(unwindset_given && unwindset_file_given)
180 throw "only one of --unwindset and --unwindset-file supported at a "
181 "time";
182
183 if(unwind_given || unwindset_given || unwindset_file_given)
184 {
185 unwindsett unwindset{goto_model};
186
187 if(unwind_given)
188 unwindset.parse_unwind(cmdline.get_value("unwind"));
189
190 if(unwindset_file_given)
191 {
192 unwindset.parse_unwindset_file(
193 cmdline.get_value("unwindset-file"), ui_message_handler);
194 }
195
196 if(unwindset_given)
197 {
198 unwindset.parse_unwindset(
201 }
202
203 bool unwinding_assertions=cmdline.isset("unwinding-assertions");
204 bool partial_loops=cmdline.isset("partial-loops");
205 bool continue_as_loops=cmdline.isset("continue-as-loops");
206 if(continue_as_loops)
207 {
208 if(unwinding_assertions)
209 {
210 throw "unwinding assertions cannot be used with "
211 "--continue-as-loops";
212 }
213 else if(partial_loops)
214 throw "partial loops cannot be used with --continue-as-loops";
215 }
216
217 goto_unwindt::unwind_strategyt unwind_strategy=
219
220 if(unwinding_assertions)
221 {
222 if(partial_loops)
224 else
226 }
227 else if(partial_loops)
228 {
230 }
231 else if(continue_as_loops)
232 {
234 }
235
236 goto_unwindt goto_unwind;
237 goto_unwind(goto_model, unwindset, unwind_strategy);
238
239 if(cmdline.isset("log"))
240 {
241 std::string filename=cmdline.get_value("log");
242 bool have_file=!filename.empty() && filename!="-";
243
244 jsont result=goto_unwind.output_log_json();
245
246 if(have_file)
247 {
248 std::ofstream of(widen_if_needed(filename));
249
250 if(!of)
251 throw "failed to open file "+filename;
252
253 of << result;
254 of.close();
255 }
256 else
257 {
258 std::cout << result << '\n';
259 }
260 }
261
262 // goto_unwind holds references to instructions, only do remove_skip
263 // after having generated the log above
265 }
266 }
267
268 if(cmdline.isset("show-threaded"))
269 {
271
272 is_threadedt is_threaded(goto_model);
273
274 for(const auto &gf_entry : goto_model.goto_functions.function_map)
275 {
276 std::cout << "////\n";
277 std::cout << "//// Function: " << gf_entry.first << '\n';
278 std::cout << "////\n\n";
279
280 const goto_programt &goto_program = gf_entry.second.body;
281
282 forall_goto_program_instructions(i_it, goto_program)
283 {
284 i_it->output(std::cout);
285 std::cout << "Is threaded: " << (is_threaded(i_it)?"True":"False")
286 << "\n\n";
287 }
288 }
289
291 }
292
293 if(cmdline.isset("insert-final-assert-false"))
294 {
295 log.status() << "Inserting final assert false" << messaget::eom;
296 bool fail = insert_final_assert_false(
298 cmdline.get_value("insert-final-assert-false"),
300 if(fail)
301 {
303 }
304 // otherwise, fall-through to write new binary
305 }
306
307 if(cmdline.isset("show-value-sets"))
308 {
310
311 // recalculate numbers, etc.
313
314 log.status() << "Pointer Analysis" << messaget::eom;
316 value_set_analysist value_set_analysis(ns);
317 value_set_analysis(goto_model);
319 ui_message_handler.get_ui(), goto_model, value_set_analysis);
321 }
322
323 if(cmdline.isset("show-global-may-alias"))
324 {
328
329 // recalculate numbers, etc.
331
332 global_may_alias_analysist global_may_alias_analysis;
333 global_may_alias_analysis(goto_model);
334 global_may_alias_analysis.output(goto_model, std::cout);
335
337 }
338
339 if(cmdline.isset("show-local-bitvector-analysis"))
340 {
343
344 // recalculate numbers, etc.
346
348
349 for(const auto &gf_entry : goto_model.goto_functions.function_map)
350 {
351 local_bitvector_analysist local_bitvector_analysis(gf_entry.second, ns);
352 std::cout << ">>>>\n";
353 std::cout << ">>>> " << gf_entry.first << '\n';
354 std::cout << ">>>>\n";
355 local_bitvector_analysis.output(std::cout, gf_entry.second, ns);
356 std::cout << '\n';
357 }
358
360 }
361
362 if(cmdline.isset("show-local-safe-pointers") ||
363 cmdline.isset("show-safe-dereferences"))
364 {
365 // Ensure location numbering is unique:
367
369
370 for(const auto &gf_entry : goto_model.goto_functions.function_map)
371 {
372 local_safe_pointerst local_safe_pointers;
373 local_safe_pointers(gf_entry.second.body);
374 std::cout << ">>>>\n";
375 std::cout << ">>>> " << gf_entry.first << '\n';
376 std::cout << ">>>>\n";
377 if(cmdline.isset("show-local-safe-pointers"))
378 local_safe_pointers.output(std::cout, gf_entry.second.body, ns);
379 else
380 {
381 local_safe_pointers.output_safe_dereferences(
382 std::cout, gf_entry.second.body, ns);
383 }
384 std::cout << '\n';
385 }
386
388 }
389
390 if(cmdline.isset("show-sese-regions"))
391 {
392 // Ensure location numbering is unique:
394
396
397 for(const auto &gf_entry : goto_model.goto_functions.function_map)
398 {
399 sese_region_analysist sese_region_analysis;
400 sese_region_analysis(gf_entry.second.body);
401 std::cout << ">>>>\n";
402 std::cout << ">>>> " << gf_entry.first << '\n';
403 std::cout << ">>>>\n";
404 sese_region_analysis.output(std::cout, gf_entry.second.body, ns);
405 std::cout << '\n';
406 }
407
409 }
410
411 if(cmdline.isset("show-custom-bitvector-analysis"))
412 {
416
418
419 if(!cmdline.isset("inline"))
420 {
423 }
424
425 // recalculate numbers, etc.
427
428 custom_bitvector_analysist custom_bitvector_analysis;
429 custom_bitvector_analysis(goto_model);
430 custom_bitvector_analysis.output(goto_model, std::cout);
431
433 }
434
435 if(cmdline.isset("show-escape-analysis"))
436 {
440
441 // recalculate numbers, etc.
443
444 escape_analysist escape_analysis;
445 escape_analysis(goto_model);
446 escape_analysis.output(goto_model, std::cout);
447
449 }
450
451 if(cmdline.isset("custom-bitvector-analysis"))
452 {
456
458
459 if(!cmdline.isset("inline"))
460 {
463 }
464
465 // recalculate numbers, etc.
467
469
470 custom_bitvector_analysist custom_bitvector_analysis;
471 custom_bitvector_analysis(goto_model);
472 custom_bitvector_analysis.check(
474 cmdline.isset("xml-ui"),
475 std::cout);
476
478 }
479
480 if(cmdline.isset("show-points-to"))
481 {
483
484 // recalculate numbers, etc.
486
488
489 log.status() << "Pointer Analysis" << messaget::eom;
490 points_tot points_to;
491 points_to(goto_model);
492 points_to.output(std::cout);
494 }
495
496 if(cmdline.isset("show-intervals"))
497 {
499
500 // recalculate numbers, etc.
502
503 log.status() << "Interval Analysis" << messaget::eom;
507 interval_analysis.output(goto_model, std::cout);
509 }
510
511 if(cmdline.isset("show-call-sequences"))
512 {
516 }
517
518 if(cmdline.isset("check-call-sequence"))
519 {
523 }
524
525 if(cmdline.isset("list-calls-args"))
526 {
528
530
532 }
533
534 if(cmdline.isset("show-rw-set"))
535 {
537
538 if(!cmdline.isset("inline"))
539 {
541
542 // recalculate numbers, etc.
544 }
545
546 log.status() << "Pointer Analysis" << messaget::eom;
547 value_set_analysist value_set_analysis(ns);
548 value_set_analysis(goto_model);
549
550 const symbolt &symbol=ns.lookup(ID_main);
551 symbol_exprt main(symbol.name, symbol.type);
552
553 std::cout <<
554 rw_set_functiont(value_set_analysis, goto_model, main);
556 }
557
558 if(cmdline.isset("show-symbol-table"))
559 {
562 }
563
564 if(cmdline.isset("show-reaching-definitions"))
565 {
568
570 reaching_definitions_analysist rd_analysis(ns);
571 rd_analysis(goto_model);
572 rd_analysis.output(goto_model, std::cout);
573
575 }
576
577 if(cmdline.isset("show-dependence-graph"))
578 {
581
583 dependence_grapht dependence_graph(ns);
584 dependence_graph(goto_model);
585 dependence_graph.output(goto_model, std::cout);
586 dependence_graph.output_dot(std::cout);
587
589 }
590
591 if(cmdline.isset("count-eloc"))
592 {
595 }
596
597 if(cmdline.isset("list-eloc"))
598 {
601 }
602
603 if(cmdline.isset("print-path-lengths"))
604 {
607 }
608
609 if(cmdline.isset("print-global-state-size"))
610 {
613 }
614
615 if(cmdline.isset("list-symbols"))
616 {
619 }
620
621 if(cmdline.isset("show-uninitialized"))
622 {
623 show_uninitialized(goto_model, std::cout);
625 }
626
627 if(cmdline.isset("interpreter"))
628 {
631
632 log.status() << "Starting interpreter" << messaget::eom;
635 }
636
637 if(cmdline.isset("show-claims") ||
638 cmdline.isset("show-properties"))
639 {
643 }
644
645 if(cmdline.isset("document-claims-html") ||
646 cmdline.isset("document-properties-html"))
647 {
650 }
651
652 if(cmdline.isset("document-claims-latex") ||
653 cmdline.isset("document-properties-latex"))
654 {
657 }
658
659 if(cmdline.isset("show-loops"))
660 {
663 }
664
665 if(cmdline.isset("show-natural-loops"))
666 {
667 show_natural_loops(goto_model, std::cout);
669 }
670
671 if(cmdline.isset("show-lexical-loops"))
672 {
673 show_lexical_loops(goto_model, std::cout);
675 }
676
677 if(cmdline.isset("print-internal-representation"))
678 {
679 for(auto const &pair : goto_model.goto_functions.function_map)
680 for(auto const &ins : pair.second.body.instructions)
681 {
682 if(ins.code().is_not_nil())
683 log.status() << ins.code().pretty() << messaget::eom;
684 if(ins.has_condition())
685 {
686 log.status() << "[guard] " << ins.condition().pretty()
687 << messaget::eom;
688 }
689 }
691 }
692
693 if(
694 cmdline.isset("show-goto-functions") ||
695 cmdline.isset("list-goto-functions"))
696 {
698 goto_model, ui_message_handler, cmdline.isset("list-goto-functions"));
700 }
701
702 if(cmdline.isset("list-undefined-functions"))
703 {
706 }
707
708 // experimental: print structs
709 if(cmdline.isset("show-struct-alignment"))
710 {
713 }
714
715 if(cmdline.isset("show-locations"))
716 {
719 }
720
721 if(
722 cmdline.isset("dump-c") || cmdline.isset("dump-cpp") ||
723 cmdline.isset("dump-c-type-header"))
724 {
725 const bool is_cpp=cmdline.isset("dump-cpp");
726 const bool is_header = cmdline.isset("dump-c-type-header");
727 const bool h_libc=!cmdline.isset("no-system-headers");
728 const bool h_all=cmdline.isset("use-all-headers");
729 const bool harness=cmdline.isset("harness");
731
732 // restore RETURN instructions in case remove_returns had been
733 // applied
735
736 // dump_c (actually goto_program2code) requires valid instruction
737 // location numbers:
739
740 if(cmdline.args.size()==2)
741 {
742 std::ofstream out(widen_if_needed(cmdline.args[1]));
743
744 if(!out)
745 {
746 log.error() << "failed to write to '" << cmdline.args[1] << "'";
748 }
749 if(is_header)
750 {
753 h_libc,
754 h_all,
755 harness,
756 ns,
757 cmdline.get_value("dump-c-type-header"),
758 out);
759 }
760 else
761 {
762 (is_cpp ? dump_cpp : dump_c)(
763 goto_model.goto_functions, h_libc, h_all, harness, ns, out);
764 }
765 }
766 else
767 {
768 if(is_header)
769 {
772 h_libc,
773 h_all,
774 harness,
775 ns,
776 cmdline.get_value("dump-c-type-header"),
777 std::cout);
778 }
779 else
780 {
781 (is_cpp ? dump_cpp : dump_c)(
782 goto_model.goto_functions, h_libc, h_all, harness, ns, std::cout);
783 }
784 }
785
787 }
788
789 if(cmdline.isset("call-graph"))
790 {
792 call_grapht call_graph(goto_model);
793
794 if(cmdline.isset("xml"))
795 call_graph.output_xml(std::cout);
796 else if(cmdline.isset("dot"))
797 call_graph.output_dot(std::cout);
798 else
799 call_graph.output(std::cout);
800
802 }
803
804 if(cmdline.isset("reachable-call-graph"))
805 {
807 call_grapht call_graph =
810 if(cmdline.isset("xml"))
811 call_graph.output_xml(std::cout);
812 else if(cmdline.isset("dot"))
813 call_graph.output_dot(std::cout);
814 else
815 call_graph.output(std::cout);
816
817 return 0;
818 }
819
820 if(cmdline.isset("show-class-hierarchy"))
821 {
822 class_hierarchyt hierarchy;
823 hierarchy(goto_model.symbol_table);
824 if(cmdline.isset("dot"))
825 hierarchy.output_dot(std::cout);
826 else
828
830 }
831
832 if(cmdline.isset("dot"))
833 {
835
836 if(cmdline.args.size()==2)
837 {
838 std::ofstream out(widen_if_needed(cmdline.args[1]));
839
840 if(!out)
841 {
842 log.error() << "failed to write to " << cmdline.args[1] << "'";
844 }
845
846 dot(goto_model, out);
847 }
848 else
849 dot(goto_model, std::cout);
850
852 }
853
854 if(cmdline.isset("accelerate"))
855 {
857
859
860 log.status() << "Performing full inlining" << messaget::eom;
862
863 log.status() << "Removing calls to functions without a body"
864 << messaget::eom;
865 remove_calls_no_bodyt remove_calls_no_body;
866 remove_calls_no_body(goto_model.goto_functions, ui_message_handler);
867
868 log.status() << "Accelerating" << messaget::eom;
869 guard_managert guard_manager;
871 goto_model, ui_message_handler, cmdline.isset("z3"), guard_manager);
873 }
874
875 if(cmdline.isset("horn"))
876 {
877 log.status() << "Horn-clause encoding" << messaget::eom;
879
880 if(cmdline.args.size()==2)
881 {
882 std::ofstream out(widen_if_needed(cmdline.args[1]));
883
884 if(!out)
885 {
886 log.error() << "Failed to open output file " << cmdline.args[1]
887 << messaget::eom;
889 }
890
892 }
893 else
894 horn_encoding(goto_model, std::cout);
895
897 }
898
899 if(cmdline.isset("drop-unused-functions"))
900 {
902
903 log.status() << "Removing unused functions" << messaget::eom;
905 }
906
907 if(cmdline.isset("undefined-function-is-assume-false"))
908 {
911 }
912
913 // write new binary?
914 if(cmdline.args.size()==2)
915 {
916 log.status() << "Writing GOTO program to '" << cmdline.args[1] << "'"
917 << messaget::eom;
918
921 else
923 }
924 else if(cmdline.args.size() < 2)
925 {
927 "Invalid number of positional arguments passed",
928 "[in] [out]",
929 "goto-instrument needs one input and one output file, aside from other "
930 "flags");
931 }
932
933 help();
935 }
936// NOLINTNEXTLINE(readability/fn_size)
937}
938
940 bool force)
941{
943 return;
944
946
947 log.status() << "Function Pointer Removal" << messaget::eom;
949 log.status() << "Virtual function removal" << messaget::eom;
951 log.status() << "Cleaning inline assembler statements" << messaget::eom;
953}
954
959{
960 // Don't bother if we've already done a full function pointer
961 // removal.
963 {
964 return;
965 }
966
967 log.status() << "Removing const function pointers only" << messaget::eom;
971 true); // abort if we can't resolve via const pointers
972}
973
975{
977 return;
978
980
981 if(!cmdline.isset("inline"))
982 {
983 log.status() << "Partial Inlining" << messaget::eom;
985 }
986}
987
989{
991 return;
992
994
995 log.status() << "Removing returns" << messaget::eom;
997}
998
1000{
1001 log.status() << "Reading GOTO program from '" << cmdline.args[0] << "'"
1002 << messaget::eom;
1003
1005
1007
1008 if(!result.has_value())
1009 throw 0;
1010
1011 goto_model = std::move(result.value());
1012
1014}
1015
1017{
1018 optionst options;
1019
1021
1022 // disable simplify when adding various checks?
1023 if(cmdline.isset("no-simplify"))
1024 options.set_option("simplify", false);
1025 else
1026 options.set_option("simplify", true);
1027
1028 // all checks supported by goto_check
1030
1031 // initialize argv with valid pointers
1032 if(cmdline.isset("model-argc-argv"))
1033 {
1034 unsigned max_argc=
1035 safe_string2unsigned(cmdline.get_value("model-argc-argv"));
1036 std::list<std::string> argv;
1037 argv.resize(max_argc);
1038
1039 log.status() << "Adding up to " << max_argc << " command line arguments"
1040 << messaget::eom;
1041
1042 if(model_argc_argv(
1043 goto_model, argv, true /*model_argv*/, ui_message_handler))
1044 throw 0;
1045 }
1046
1047 if(cmdline.isset("add-cmd-line-arg"))
1048 {
1049 const std::list<std::string> &argv = cmdline.get_values("add-cmd-line-arg");
1050 unsigned argc = 0;
1051
1052 std::stringstream ss;
1053 ss << "[";
1054 std::string sep = "";
1055 for(auto const &arg : argv)
1056 {
1057 ss << sep << "\"" << arg << "\"";
1058 argc++;
1059 sep = ", ";
1060 }
1061 ss << "]";
1062
1063 log.status() << "Adding " << argc << " arguments: " << ss.str()
1064 << messaget::eom;
1065
1066 if(model_argc_argv(
1067 goto_model, argv, false /*model_argv*/, ui_message_handler))
1068 throw 0;
1069 }
1070
1071 if(cmdline.isset("remove-function-body"))
1072 {
1074 goto_model,
1075 cmdline.get_values("remove-function-body"),
1077 }
1078
1079 // we add the library in some cases, as some analyses benefit
1080
1081 if(
1082 cmdline.isset("add-library") || cmdline.isset("mm") ||
1083 cmdline.isset("reachability-slice") ||
1084 cmdline.isset("reachability-slice-fb") ||
1085 cmdline.isset("fp-reachability-slice"))
1086 {
1087 if(cmdline.isset("show-custom-bitvector-analysis") ||
1088 cmdline.isset("custom-bitvector-analysis"))
1089 {
1090 config.ansi_c.defines.push_back(
1091 std::string(CPROVER_PREFIX) + "CUSTOM_BITVECTOR_ANALYSIS");
1092 }
1093
1094 // remove inline assembler as that may yield further library function calls
1095 // that need to be resolved
1097
1098 // add the library
1099 log.status() << "Adding CPROVER library (" << config.ansi_c.arch << ")"
1100 << messaget::eom;
1104 }
1105
1106 {
1108
1109 if(
1113 {
1115
1117 }
1118 }
1119
1120 // skip over selected loops
1121 if(cmdline.isset("skip-loops"))
1122 {
1123 log.status() << "Adding gotos to skip loops" << messaget::eom;
1124 if(skip_loops(
1126 {
1127 throw 0;
1128 }
1129 }
1130
1131 // now do full inlining, if requested
1132 if(cmdline.isset("inline"))
1133 {
1135
1136 if(cmdline.isset("show-custom-bitvector-analysis") ||
1137 cmdline.isset("custom-bitvector-analysis"))
1138 {
1142 }
1143
1144 log.status() << "Performing full inlining" << messaget::eom;
1146 }
1147
1148 if(cmdline.isset("show-custom-bitvector-analysis") ||
1149 cmdline.isset("custom-bitvector-analysis"))
1150 {
1151 log.status() << "Propagating Constants" << messaget::eom;
1152 constant_propagator_ait constant_propagator_ai(goto_model);
1154 }
1155
1156 if(cmdline.isset("escape-analysis"))
1157 {
1161
1162 // recalculate numbers, etc.
1164
1165 log.status() << "Escape Analysis" << messaget::eom;
1166 escape_analysist escape_analysis;
1167 escape_analysis(goto_model);
1168 escape_analysis.instrument(goto_model);
1169
1170 // inline added functions, they are often small
1172
1173 // recalculate numbers, etc.
1175 }
1176
1177 if(cmdline.isset("loop-contracts-file"))
1178 {
1179 const auto file_name = cmdline.get_value("loop-contracts-file");
1180 contracts_wranglert contracts_wrangler(
1181 goto_model, file_name, ui_message_handler);
1182 }
1183
1184 bool use_dfcc = cmdline.isset(FLAG_DFCC);
1185 if(use_dfcc)
1186 {
1187 if(cmdline.get_values(FLAG_DFCC).size() != 1)
1188 {
1190 "Redundant options detected",
1191 "--" FLAG_DFCC,
1192 "Use a single " FLAG_DFCC " option");
1193 }
1194
1196
1197 const irep_idt harness_id(cmdline.get_value(FLAG_DFCC));
1198
1199 std::set<irep_idt> to_replace(
1202
1203 if(
1206 {
1208 "Mutually exclusive options detected",
1210 "Use either --" FLAG_ENFORCE_CONTRACT
1211 " or --" FLAG_ENFORCE_CONTRACT_REC);
1212 }
1213
1214 auto &to_enforce = !cmdline.get_values(FLAG_ENFORCE_CONTRACT_REC).empty()
1217
1218 bool allow_recursive_calls =
1220
1221 std::set<std::string> to_exclude_from_nondet_static(
1222 cmdline.get_values("nondet-static-exclude").begin(),
1223 cmdline.get_values("nondet-static-exclude").end());
1224
1225 if(
1228 {
1229 // When the model is produced by Kani, we must not automatically unwind
1230 // the backjump introduced by the loop transformation.
1231 // Automatic unwinding duplicates assertions found in the loop body, and
1232 // since Kani expects property identifiers to remain unique. Having
1233 // duplicate instances of the assertions makes Kani fail to handle the
1234 // analysis results.
1235 log.warning() << "**** WARNING: transformed loops will not be unwound "
1236 << "after applying loop contracts. Remember to unwind "
1237 << "them at least twice to pass unwinding-assertions."
1238 << messaget::eom;
1239 }
1240
1241 dfcc(
1242 options,
1243 goto_model,
1244 harness_id,
1245 to_enforce.empty() ? optionalt<irep_idt>{}
1246 : optionalt<irep_idt>{to_enforce.front()},
1247 allow_recursive_calls,
1248 to_replace,
1251 to_exclude_from_nondet_static,
1253 }
1254
1255 if(
1256 !use_dfcc &&
1259 {
1261 code_contractst contracts(goto_model, log);
1262
1263 std::set<std::string> to_replace(
1266
1267 std::set<std::string> to_enforce(
1270
1271 std::set<std::string> to_exclude_from_nondet_static(
1272 cmdline.get_values("nondet-static-exclude").begin(),
1273 cmdline.get_values("nondet-static-exclude").end());
1274
1275 // It's important to keep the order of contracts instrumentation, i.e.,
1276 // first replacement then enforcement. We rely on contract replacement
1277 // and inlining of sub-function calls to properly annotate all
1278 // assignments.
1279 contracts.replace_calls(to_replace);
1280 contracts.enforce_contracts(to_enforce, to_exclude_from_nondet_static);
1281
1283 {
1285 {
1286 contracts.unwind_transformed_loops = false;
1287 // When the model is produced by Kani, we must not automatically unwind
1288 // the backjump introduced by the loop transformation.
1289 // Automatic unwinding duplicates assertions found in the loop body, and
1290 // since Kani expects property identifiers to remain unique. Having
1291 // duplicate instances of the assertions makes Kani fail to handle the
1292 // analysis results.
1293 log.warning() << "**** WARNING: transformed loops will not be unwound "
1294 << "after applying loop contracts. Remember to unwind "
1295 << "them at least twice to pass unwinding-assertions."
1296 << messaget::eom;
1297 }
1298 contracts.apply_loop_contracts(to_exclude_from_nondet_static);
1299 }
1300 }
1301
1302 if(cmdline.isset("value-set-fi-fp-removal"))
1303 {
1306 }
1307
1308 // replace function pointers, if explicitly requested
1309 if(cmdline.isset("remove-function-pointers"))
1310 {
1312 }
1313 else if(cmdline.isset("remove-const-function-pointers"))
1314 {
1316 }
1317
1318 if(cmdline.isset("replace-calls"))
1319 {
1321
1322 replace_callst replace_calls;
1323 replace_calls(goto_model, cmdline.get_values("replace-calls"));
1324 }
1325
1326 if(cmdline.isset("function-inline"))
1327 {
1328 std::string function=cmdline.get_value("function-inline");
1329 PRECONDITION(!function.empty());
1330
1331 bool caching=!cmdline.isset("no-caching");
1332
1334
1335 log.status() << "Inlining calls of function '" << function << "'"
1336 << messaget::eom;
1337
1338 if(!cmdline.isset("log"))
1339 {
1341 goto_model, function, ui_message_handler, true, caching);
1342 }
1343 else
1344 {
1345 std::string filename=cmdline.get_value("log");
1346 bool have_file=!filename.empty() && filename!="-";
1347
1349 goto_model, function, ui_message_handler, true, caching);
1350
1351 if(have_file)
1352 {
1353 std::ofstream of(widen_if_needed(filename));
1354
1355 if(!of)
1356 throw "failed to open file "+filename;
1357
1358 of << result;
1359 of.close();
1360 }
1361 else
1362 {
1363 std::cout << result << '\n';
1364 }
1365 }
1366
1369 }
1370
1371 if(cmdline.isset("partial-inline"))
1372 {
1374
1375 log.status() << "Partial inlining" << messaget::eom;
1377
1380 }
1381
1382 if(cmdline.isset("remove-calls-no-body"))
1383 {
1384 log.status() << "Removing calls to functions without a body"
1385 << messaget::eom;
1386
1387 remove_calls_no_bodyt remove_calls_no_body;
1388 remove_calls_no_body(goto_model.goto_functions, ui_message_handler);
1389
1392 }
1393
1394 if(cmdline.isset("constant-propagator"))
1395 {
1398
1399 log.status() << "Propagating Constants" << messaget::eom;
1400 log.warning() << "**** WARNING: Constant propagation as performed by "
1401 "goto-instrument is not expected to be sound. Do not use "
1402 "--constant-propagator if soundness is important for your "
1403 "use case."
1404 << messaget::eom;
1405
1406 constant_propagator_ait constant_propagator_ai(goto_model);
1408 }
1409
1410 if(cmdline.isset("generate-function-body"))
1411 {
1412 optionst c_object_factory_options;
1413 parse_c_object_factory_options(cmdline, c_object_factory_options);
1414 c_object_factory_parameterst object_factory_parameters(
1415 c_object_factory_options);
1416
1417 auto generate_implementation = generate_function_bodies_factory(
1418 cmdline.get_value("generate-function-body-options"),
1419 object_factory_parameters,
1423 std::regex(cmdline.get_value("generate-function-body")),
1424 *generate_implementation,
1425 goto_model,
1427 }
1428
1429 if(cmdline.isset("generate-havocing-body"))
1430 {
1431 optionst c_object_factory_options;
1432 parse_c_object_factory_options(cmdline, c_object_factory_options);
1433 c_object_factory_parameterst object_factory_parameters(
1434 c_object_factory_options);
1435
1436 auto options_split =
1437 split_string(cmdline.get_value("generate-havocing-body"), ',');
1438 if(options_split.size() < 2)
1440 "not enough arguments for this option", "--generate-havocing-body"};
1441
1442 if(options_split.size() == 2)
1443 {
1444 auto generate_implementation = generate_function_bodies_factory(
1445 std::string{"havoc,"} + options_split.back(),
1446 object_factory_parameters,
1450 std::regex(options_split[0]),
1451 *generate_implementation,
1452 goto_model,
1454 }
1455 else
1456 {
1457 CHECK_RETURN(options_split.size() % 2 == 1);
1458 for(size_t i = 1; i + 1 < options_split.size(); i += 2)
1459 {
1460 auto generate_implementation = generate_function_bodies_factory(
1461 std::string{"havoc,"} + options_split[i + 1],
1462 object_factory_parameters,
1466 options_split[0],
1467 options_split[i],
1468 *generate_implementation,
1469 goto_model,
1471 }
1472 }
1473 }
1474
1475 // add generic checks, if needed
1478
1479 // check for uninitalized local variables
1480 if(cmdline.isset("uninitialized-check"))
1481 {
1482 log.status() << "Adding checks for uninitialized local variables"
1483 << messaget::eom;
1485 }
1486
1487 // check for maximum call stack size
1488 if(cmdline.isset("stack-depth"))
1489 {
1490 log.status() << "Adding check for maximum call stack size" << messaget::eom;
1492 goto_model,
1493 safe_string2size_t(cmdline.get_value("stack-depth")),
1495 }
1496
1497 // ignore default/user-specified initialization of variables with static
1498 // lifetime
1499 if(cmdline.isset("nondet-static-exclude"))
1500 {
1501 log.status() << "Adding nondeterministic initialization "
1502 "of static/global variables except for "
1503 "the specified ones."
1504 << messaget::eom;
1505 std::set<std::string> to_exclude(
1506 cmdline.get_values("nondet-static-exclude").begin(),
1507 cmdline.get_values("nondet-static-exclude").end());
1508 nondet_static(goto_model, to_exclude);
1509 }
1510 else if(cmdline.isset("nondet-static"))
1511 {
1512 log.status() << "Adding nondeterministic initialization "
1513 "of static/global variables"
1514 << messaget::eom;
1516 }
1517
1518 if(cmdline.isset("slice-global-inits"))
1519 {
1521
1522 log.status() << "Slicing away initializations of unused global variables"
1523 << messaget::eom;
1525 }
1526
1527 if(cmdline.isset("string-abstraction"))
1528 {
1531
1532 log.status() << "String Abstraction" << messaget::eom;
1534 }
1535
1536 // some analyses require function pointer removal and partial inlining
1537
1538 if(cmdline.isset("remove-pointers") ||
1539 cmdline.isset("race-check") ||
1540 cmdline.isset("mm") ||
1541 cmdline.isset("isr") ||
1542 cmdline.isset("concurrency"))
1543 {
1545
1546 log.status() << "Pointer Analysis" << messaget::eom;
1548 value_set_analysist value_set_analysis(ns);
1549 value_set_analysis(goto_model);
1550
1551 if(cmdline.isset("remove-pointers"))
1552 {
1553 // removing pointers
1554 log.status() << "Removing Pointers" << messaget::eom;
1555 remove_pointers(goto_model, value_set_analysis);
1556 }
1557
1558 if(cmdline.isset("race-check"))
1559 {
1560 log.status() << "Adding Race Checks" << messaget::eom;
1561 race_check(value_set_analysis, goto_model);
1562 }
1563
1564 if(cmdline.isset("mm"))
1565 {
1566 std::string mm=cmdline.get_value("mm");
1567 memory_modelt model;
1568
1569 // strategy of instrumentation
1570 instrumentation_strategyt inst_strategy;
1571 if(cmdline.isset("one-event-per-cycle"))
1572 inst_strategy=one_event_per_cycle;
1573 else if(cmdline.isset("minimum-interference"))
1574 inst_strategy=min_interference;
1575 else if(cmdline.isset("read-first"))
1576 inst_strategy=read_first;
1577 else if(cmdline.isset("write-first"))
1578 inst_strategy=write_first;
1579 else if(cmdline.isset("my-events"))
1580 inst_strategy=my_events;
1581 else
1582 /* default: instruments all unsafe pairs */
1583 inst_strategy=all;
1584
1585 const unsigned max_var=
1586 cmdline.isset("max-var")?
1588 const unsigned max_po_trans=
1589 cmdline.isset("max-po-trans")?
1590 unsafe_string2unsigned(cmdline.get_value("max-po-trans")):0;
1591
1592 if(mm=="tso")
1593 {
1594 log.status() << "Adding weak memory (TSO) Instrumentation"
1595 << messaget::eom;
1596 model=TSO;
1597 }
1598 else if(mm=="pso")
1599 {
1600 log.status() << "Adding weak memory (PSO) Instrumentation"
1601 << messaget::eom;
1602 model=PSO;
1603 }
1604 else if(mm=="rmo")
1605 {
1606 log.status() << "Adding weak memory (RMO) Instrumentation"
1607 << messaget::eom;
1608 model=RMO;
1609 }
1610 else if(mm=="power")
1611 {
1612 log.status() << "Adding weak memory (Power) Instrumentation"
1613 << messaget::eom;
1614 model=Power;
1615 }
1616 else
1617 {
1618 log.error() << "Unknown weak memory model '" << mm << "'"
1619 << messaget::eom;
1620 model=Unknown;
1621 }
1622
1624
1625 if(cmdline.isset("force-loop-duplication"))
1626 loops=all_loops;
1627 if(cmdline.isset("no-loop-duplication"))
1628 loops=no_loop;
1629
1630 if(model!=Unknown)
1632 model,
1633 value_set_analysis,
1634 goto_model,
1635 cmdline.isset("scc"),
1636 inst_strategy,
1637 !cmdline.isset("cfg-kill"),
1638 cmdline.isset("no-dependencies"),
1639 loops,
1640 max_var,
1641 max_po_trans,
1642 !cmdline.isset("no-po-rendering"),
1643 cmdline.isset("render-cluster-file"),
1644 cmdline.isset("render-cluster-function"),
1645 cmdline.isset("cav11"),
1646 cmdline.isset("hide-internals"),
1648 cmdline.isset("ignore-arrays"));
1649 }
1650
1651 // Interrupt handler
1652 if(cmdline.isset("isr"))
1653 {
1654 log.status() << "Instrumenting interrupt handler" << messaget::eom;
1655 interrupt(
1656 value_set_analysis,
1657 goto_model,
1658 cmdline.get_value("isr"));
1659 }
1660
1661 // Memory-mapped I/O
1662 if(cmdline.isset("mmio"))
1663 {
1664 log.status() << "Instrumenting memory-mapped I/O" << messaget::eom;
1665 mmio(value_set_analysis, goto_model);
1666 }
1667
1668 if(cmdline.isset("concurrency"))
1669 {
1670 log.status() << "Sequentializing concurrency" << messaget::eom;
1671 concurrency(value_set_analysis, goto_model);
1672 }
1673 }
1674
1675 if(cmdline.isset("interval-analysis"))
1676 {
1677 log.status() << "Interval analysis" << messaget::eom;
1679 }
1680
1681 if(cmdline.isset("havoc-loops"))
1682 {
1683 log.status() << "Havocking loops" << messaget::eom;
1685 }
1686
1687 if(cmdline.isset("k-induction"))
1688 {
1689 bool base_case=cmdline.isset("base-case");
1690 bool step_case=cmdline.isset("step-case");
1691
1692 if(step_case && base_case)
1693 throw "please specify only one of --step-case and --base-case";
1694 else if(!step_case && !base_case)
1695 throw "please specify one of --step-case and --base-case";
1696
1697 unsigned k=unsafe_string2unsigned(cmdline.get_value("k-induction"));
1698
1699 if(k==0)
1700 throw "please give k>=1";
1701
1702 log.status() << "Instrumenting k-induction for k=" << k << ", "
1703 << (base_case ? "base case" : "step case") << messaget::eom;
1704
1705 k_induction(goto_model, base_case, step_case, k);
1706 }
1707
1708 if(cmdline.isset("function-enter"))
1709 {
1710 log.status() << "Function enter instrumentation" << messaget::eom;
1712 goto_model,
1713 cmdline.get_value("function-enter"));
1714 }
1715
1716 if(cmdline.isset("function-exit"))
1717 {
1718 log.status() << "Function exit instrumentation" << messaget::eom;
1720 goto_model,
1721 cmdline.get_value("function-exit"));
1722 }
1723
1724 if(cmdline.isset("branch"))
1725 {
1726 log.status() << "Branch instrumentation" << messaget::eom;
1727 branch(
1728 goto_model,
1729 cmdline.get_value("branch"));
1730 }
1731
1732 // add failed symbols
1734
1735 // recalculate numbers, etc.
1737
1738 // add loop ids
1740
1741 // label the assertions
1743
1744 nondet_volatile(goto_model, options);
1745
1746 // reachability slice?
1747 if(cmdline.isset("reachability-slice"))
1748 {
1750
1751 log.status() << "Performing a reachability slice" << messaget::eom;
1752
1753 // reachability_slicer requires that the model has unique location numbers:
1755
1756 if(cmdline.isset("property"))
1757 {
1760 }
1761 else
1763 }
1764
1765 if(cmdline.isset("fp-reachability-slice"))
1766 {
1768
1769 log.status() << "Performing a function pointer reachability slice"
1770 << messaget::eom;
1772 goto_model,
1773 cmdline.get_comma_separated_values("fp-reachability-slice"),
1775 }
1776
1777 // full slice?
1778 if(cmdline.isset("full-slice"))
1779 {
1783
1784 log.warning() << "**** WARNING: Experimental option --full-slice, "
1785 << "analysis results may be unsound. See "
1786 << "https://github.com/diffblue/cbmc/issues/260"
1787 << messaget::eom;
1788 log.status() << "Performing a full slice" << messaget::eom;
1789 if(cmdline.isset("property"))
1791 else
1792 {
1793 // full_slicer requires that the model has unique location numbers:
1796 }
1797 }
1798
1799 // splice option
1800 if(cmdline.isset("splice-call"))
1801 {
1802 log.status() << "Performing call splicing" << messaget::eom;
1803 std::string callercallee=cmdline.get_value("splice-call");
1804 if(splice_call(
1806 callercallee,
1809 throw 0;
1810 }
1811
1812 // aggressive slicer
1813 if(cmdline.isset("aggressive-slice"))
1814 {
1816
1817 // reachability_slicer requires that the model has unique location numbers:
1819
1820 log.status() << "Slicing away initializations of unused global variables"
1821 << messaget::eom;
1823
1824 log.status() << "Performing an aggressive slice" << messaget::eom;
1826
1827 if(cmdline.isset("aggressive-slice-call-depth"))
1828 aggressive_slicer.call_depth =
1829 safe_string2unsigned(cmdline.get_value("aggressive-slice-call-depth"));
1830
1831 if(cmdline.isset("aggressive-slice-preserve-function"))
1832 aggressive_slicer.preserve_functions(
1833 cmdline.get_values("aggressive-slice-preserve-function"));
1834
1835 if(cmdline.isset("property"))
1836 aggressive_slicer.user_specified_properties =
1837 cmdline.get_values("property");
1838
1839 if(cmdline.isset("aggressive-slice-preserve-functions-containing"))
1840 aggressive_slicer.name_snippets =
1841 cmdline.get_values("aggressive-slice-preserve-functions-containing");
1842
1843 aggressive_slicer.preserve_all_direct_paths =
1844 cmdline.isset("aggressive-slice-preserve-all-direct-paths");
1845
1846 aggressive_slicer.doit();
1847
1849
1850 log.status() << "Performing a reachability slice" << messaget::eom;
1851 if(cmdline.isset("property"))
1852 {
1855 }
1856 else
1858 }
1859
1860 if(cmdline.isset("ensure-one-backedge-per-target"))
1861 {
1862 log.status() << "Trying to force one backedge per target" << messaget::eom;
1864 }
1865
1866 // recalculate numbers, etc.
1868}
1869
1872{
1873 std::cout << '\n'
1874 << banner_string("Goto-Instrument", CBMC_VERSION) << '\n'
1875 << align_center_with_border("Copyright (C) 2008-2013") << '\n'
1876 << align_center_with_border("Daniel Kroening") << '\n'
1877 << align_center_with_border("kroening@kroening.com") << '\n';
1878
1879 // clang-format off
1880 std::cout << help_formatter(
1881 "\n"
1882 "Usage: \tPurpose:\n"
1883 "\n"
1884 " {bgoto-instrument} [{y-?}] [{y-h}] [{y--help}] \t show this help\n"
1885 " {bgoto-instrument} {y--version} \t show version and exit\n"
1886 " {bgoto-instrument} [options] {uin} [{uout}] \t perform analysis or"
1887 " instrumentation\n"
1888 "\n"
1889 "Dump Source:\n"
1891 " {y--horn} \t print program as constrained horn clauses\n"
1892 "\n"
1893 "Diagnosis:\n"
1896 " {y--show-symbol-table} \t show loaded symbol table\n"
1897 " {y--list-symbols} \t list symbols with type information\n"
1900 " {y--show-locations} \t show all source locations\n"
1901 " {y--dot} \t generate CFG graph in DOT format\n"
1902 " {y--print-internal-representation} \t show verbose internal"
1903 " representation of the program\n"
1904 " {y--list-undefined-functions} \t list functions without body\n"
1905 " {y--list-calls-args} \t list all function calls with their arguments\n"
1906 " {y--call-graph} \t show graph of function calls\n"
1907 " {y--reachable-call-graph} \t show graph of function calls potentially"
1908 " reachable from main function\n"
1911 " {y--validate-goto-binary} \t check the well-formedness of the passed in"
1912 " goto binary and then exit\n"
1913 " {y--interpreter} \t do concrete execution\n"
1914 "\n"
1915 "Data-flow analyses:\n"
1916 " {y--show-struct-alignment} \t show struct members that might be"
1917 " concurrently accessed\n"
1918 " {y--show-threaded} \t show instructions that may be executed by more than"
1919 " one thread\n"
1920 " {y--show-local-safe-pointers} \t show pointer expressions that are"
1921 " trivially dominated by a not-null check\n"
1922 " {y--show-safe-dereferences} \t show pointer expressions that are"
1923 " trivially dominated by a not-null check *and* used as a dereference"
1924 " operand\n"
1925 " {y--show-value-sets} \t show points-to information (using value sets)\n"
1926 " {y--show-global-may-alias} \t show may-alias information over globals\n"
1927 " {y--show-local-bitvector-analysis} \t show procedure-local pointer"
1928 " analysis\n"
1929 " {y--escape-analysis} \t perform escape analysis\n"
1930 " {y--show-escape-analysis} \t show results of escape analysis\n"
1931 " {y--custom-bitvector-analysis} \t perform configurable bitvector"
1932 " analysis\n"
1933 " {y--show-custom-bitvector-analysis} \t show results of configurable"
1934 " bitvector analysis\n"
1935 " {y--interval-analysis} \t perform interval analysis\n"
1936 " {y--show-intervals} \t show results of interval analysis\n"
1937 " {y--show-uninitialized} \t show maybe-uninitialized variables\n"
1938 " {y--show-points-to} \t show points-to information\n"
1939 " {y--show-rw-set} \t show read-write sets\n"
1940 " {y--show-call-sequences} \t show function call sequences\n"
1941 " {y--show-reaching-definitions} \t show reaching definitions\n"
1942 " {y--show-dependence-graph} \t show program-dependence graph\n"
1943 " {y--show-sese-regions} \t show single-entry-single-exit regions\n"
1944 "\n"
1945 "Safety checks:\n"
1946 " {y--no-assertions} \t ignore user assertions\n"
1949 " {y--stack-depth} {un} \t add check that call stack size of non-inlined"
1950 " functions never exceeds {un}\n"
1951 " {y--race-check} \t add floating-point data race checks\n"
1952 "\n"
1953 "Semantic transformations:\n"
1955 " {y--isr} {ufunction} \t instruments an interrupt service routine\n"
1956 " {y--mmio} \t instruments memory-mapped I/O\n"
1957 " {y--nondet-static} \t add nondeterministic initialization of variables"
1958 " with static lifetime\n"
1959 " {y--nondet-static-exclude} {ue} \t same as nondet-static except for the"
1960 " variable {ue} (use multiple times if required)\n"
1961 " {y--nondet-static-matching} {ur} \t add nondeterministic initialization"
1962 " of variables with static lifetime matching regex {ur}\n"
1963 " {y--function-enter} {uf}, {y--function-exit} {uf}, {y--branch} {uf} \t"
1964 " instruments a call to {uf} at the beginning, the exit, or a branch point,"
1965 " respectively\n"
1966 " {y--splice-call} {ucaller},{ucallee} \t prepends a call to {ucallee} in"
1967 " the body of {ucaller}\n"
1968 " {y--check-call-sequence} {useq} \t instruments checks to assert that all"
1969 " call sequences match {useq}\n"
1970 " {y--undefined-function-is-assume-false} \t convert each call to an"
1971 " undefined function to assume(false)\n"
1976 " {y--add-library} \t add models of C library functions\n"
1979 " {y--remove-function-body} {uf} remove the implementation of function {uf}"
1980 " (may be repeated)\n"
1983 "\n"
1984 "Semantics-preserving transformations:\n"
1985 " {y--ensure-one-backedge-per-target} \t transform loop bodies such that"
1986 " there is a single edge back to the loop head\n"
1987 " {y--drop-unused-functions} \t drop functions trivially unreachable from"
1988 " main function\n"
1990 " {y--constant-propagator} \t propagate constants and simplify"
1991 " expressions\n"
1992 " {y--inline} \t perform full inlining\n"
1993 " {y--partial-inline} \t perform partial inlining\n"
1994 " {y--function-inline} {ufunction} \t transitively inline all calls"
1995 " {ufunction} makes\n"
1996 " {y--no-caching} \t disable caching of intermediate results during"
1997 " transitive function inlining\n"
1998 " {y--log} {ufile} \t log in JSON format which code segments were inlined,"
1999 " use with {y--function-inline}\n"
2000 " {y--remove-function-pointers} \t replace function pointers by case"
2001 " statement over function calls\n"
2003 " {y--value-set-fi-fp-removal} \t build flow-insensitive value set and"
2004 " replace function pointers by a case statement over the possible"
2005 " assignments. If the set of possible assignments is empty the function"
2006 " pointer is removed using the standard remove-function-pointers pass.\n"
2007 "\n"
2008 "Loop information and transformations:\n"
2010 " {y--unwindset-file_<file>} \t read unwindset from file\n"
2011 " {y--partial-loops} \t permit paths with partial loops\n"
2012 " {y--unwinding-assertions} \t generate unwinding assertions\n"
2013 " {y--continue-as-loops} \t add loop for remaining iterations after"
2014 " unwound part\n"
2015 " {y--k-induction} {uk} \t check loops with k-induction\n"
2016 " {y--step-case} \t k-induction: do step-case\n"
2017 " {y--base-case} \t k-induction: do base-case\n"
2018 " {y--havoc-loops} \t over-approximate all loops\n"
2019 " {y--accelerate} \t add loop accelerators\n"
2020 " {y--z3} \t use Z3 when computing loop accelerators\n"
2021 " {y--skip-loops {uloop-ids} \t add gotos to skip selected loops during"
2022 " execution\n"
2023 " {y--show-lexical-loops} \t show single-entry-single-back-edge loops\n"
2024 " {y--show-natural-loops} \t show natural loop heads\n"
2025 "\n"
2026 "Memory model instrumentations:\n"
2028 "\n"
2029 "Slicing:\n"
2032 " {y--full-slice} \t slice away instructions that don't affect assertions\n"
2033 " {y--property} {uid} \t slice with respect to specific property only\n"
2034 " {y--slice-global-inits} \t slice away initializations of unused global"
2035 " variables\n"
2036 " {y--aggressive-slice} \t remove bodies of any functions not on the"
2037 " shortest path between the start function and the function containing the"
2038 " property/properties\n"
2039 " {y--aggressive-slice-call-depth} {un} \t used with aggressive-slice,"
2040 " preserves all functions within {un} function calls of the functions on"
2041 " the shortest path\n"
2042 " {y--aggressive-slice-preserve-function} {uf} \t force the aggressive"
2043 " slicer to preserve function {uf}\n"
2044 " {y--aggressive-slice-preserve-functions-containing} {uf} \t force the"
2045 " aggressive slicer to preserve all functions with names containing {uf}\n"
2046 " {y--aggressive-slice-preserve-all-direct-paths} \t force aggressive"
2047 " slicer to preserve all direct paths\n"
2048 "\n"
2049 "Code contracts:\n"
2050 HELP_DFCC
2057 "\n"
2058 "User-interface options:\n"
2060 " {y--xml} \t output files in XML where supported\n"
2061 " {y--xml-ui} \t use XML-formatted output\n"
2062 " {y--json-ui} \t use JSON-formatted output\n"
2063 " {y--verbosity} {u#} \t verbosity level\n"
2065 "\n");
2066 // clang-format on
2067}
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:22
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:563
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.
std::string get_value(char option) const
Definition cmdline.cpp:48
virtual bool isset(char option) const
Definition cmdline.cpp:30
std::list< std::string > get_comma_separated_values(const char *option) const
Collect all occurrences of option option and split their values on each comma, merging them into a si...
Definition cmdline.cpp:121
argst args
Definition cmdline.h:145
const std::list< std::string > & get_values(const std::string &option) const
Definition cmdline.cpp:109
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.
bool unwind_transformed_loops
Definition contracts.h:145
bool set(const cmdlinet &cmdline)
Definition config.cpp:798
void set_from_symbol_table(const symbol_table_baset &)
Definition config.cpp:1258
struct configt::ansi_ct ansi_c
void check(const goto_modelt &, bool xml, std::ostream &)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
bool empty() const
Definition dstring.h:90
void instrument(goto_modelt &)
void get(const std::string &executable)
This is a may analysis (i.e.
function_mapt function_map
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
void validate(const validation_modet vm=validation_modet::INVARIANT, const goto_model_validation_optionst &goto_model_validation_options=goto_model_validation_optionst{}) const override
Check that the goto model is well-formed.
Definition goto_model.h:105
symbol_tablet symbol_table
Symbol table.
Definition goto_model.h:31
goto_functionst goto_functions
GOTO functions.
Definition goto_model.h:34
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
mstreamt & error() const
Definition message.h:399
message_handlert & get_message_handler()
Definition message.h:184
mstreamt & warning() const
Definition message.h:404
@ M_STATISTICS
Definition message.h:171
static eomt eom
Definition message.h:297
mstreamt & status() const
Definition message.h:414
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
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:113
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
virtual uit get_ui() const
Definition ui_message.h:33
This template class implements a data-flow analysis which keeps track of what values different variab...
void concurrency(value_setst &value_sets, goto_modelt &goto_model)
Encoding for Threaded Goto Programs.
#define HELP_CONFIG_LIBRARY
Definition config.h:76
Constant propagation.
#define HELP_REPLACE_CALL
Definition contracts.h:46
#define FLAG_REPLACE_CALL
Definition contracts.h:45
#define FLAG_ENFORCE_CONTRACT
Definition contracts.h:50
#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:37
#define HELP_ENFORCE_CONTRACT
Definition contracts.h:51
#define HELP_LOOP_CONTRACTS_FILE
Definition contracts.h:41
#define FLAG_LOOP_CONTRACTS_NO_UNWIND
Definition contracts.h:36
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:63
#define FLAG_DFCC
Definition dfcc.h:55
#define HELP_DFCC
Definition dfcc.h:58
#define HELP_ENFORCE_CONTRACT_REC
Definition dfcc.h:65
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:1658
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:1645
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:1680
#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 full_slicer(goto_functionst &goto_functions, const namespacet &ns, const slicing_criteriont &criterion)
void property_slicer(goto_functionst &goto_functions, const namespacet &ns, const std::list< std::string > &properties)
void function_exit(goto_modelt &goto_model, const irep_idt &id)
Definition function.cpp:103
void function_enter(goto_modelt &goto_model, const irep_idt &id)
Definition function.cpp:78
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)
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 optionalt< irep_idt > &to_check, const bool allow_recursive_calls, const std::set< irep_idt > &to_replace, const bool apply_loop_contracts, const bool unwind_transformed_loops, 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:116
Guard Data Structure.
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)
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.
static void mmio(value_setst &value_sets, const symbol_tablet &symbol_table, const irep_idt &function_id, goto_programt &goto_program)
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_functionst &goto_functions, 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
nonstd::optional< T > optionalt
Definition optional.h:35
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)
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)
Replaces inline assembly instructions in the goto program (i.e., instructions of kind OTHER with a co...
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 optionalt< 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)
irep_idt arch
Definition config.h:218
std::list< std::string > defines
Definition config.h:262
preprocessort preprocessor
Definition config.h:260
This is unused by this implementation of guards, but can be used by other implementations of the same...
Definition guard_expr.h:20
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:78
#define HELP_VALIDATE
Value Set Propagation.
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
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.