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
14#include <fstream>
15#include <iostream>
16#include <memory>
17#include <sstream>
18
20#include <util/exit_codes.h>
21#include <util/json.h>
22#include <util/string2int.h>
23#include <util/string_utils.h>
24#include <util/version.h>
25
26#ifdef _MSC_VER
27# include <util/unicode.h>
28#endif
29
53
57
58#include <analyses/call_graph.h>
73
77
79
80#include <cpp/cprover_library.h>
81
83#include "alignment_checks.h"
84#include "branch.h"
85#include "call_sequences.h"
86#include "concurrency.h"
87#include "dot.h"
88#include "full_slicer.h"
89#include "function.h"
90#include "havoc_loops.h"
91#include "horn_encoding.h"
93#include "interrupt.h"
94#include "k_induction.h"
95#include "mmio.h"
96#include "nondet_static.h"
97#include "nondet_volatile.h"
98#include "points_to.h"
99#include "race_check.h"
100#include "reachability_slicer.h"
101#include "remove_function.h"
102#include "rw_set.h"
103#include "show_locations.h"
104#include "skip_loops.h"
105#include "splice_call.h"
106#include "stack_depth.h"
108#include "undefined_functions.h"
109#include "unwind.h"
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
129
130 {
132
134
135 {
136 const bool validate_only = cmdline.isset("validate-goto-binary");
137
138 if(validate_only || cmdline.isset("validate-goto-model"))
139 {
141
142 if(validate_only)
143 {
145 }
146 }
147 }
148
150
151 if(cmdline.isset("validate-goto-model"))
152 {
154 }
155
156 {
157 bool unwind_given=cmdline.isset("unwind");
158 bool unwindset_given=cmdline.isset("unwindset");
159 bool unwindset_file_given=cmdline.isset("unwindset-file");
160
162 throw "only one of --unwindset and --unwindset-file supported at a "
163 "time";
164
166 {
167 unwindsett unwindset{goto_model};
168
169 if(unwind_given)
170 unwindset.parse_unwind(cmdline.get_value("unwind"));
171
173 {
174 unwindset.parse_unwindset_file(
175 cmdline.get_value("unwindset-file"), ui_message_handler);
176 }
177
179 {
180 unwindset.parse_unwindset(
182 }
183
184 bool unwinding_assertions=cmdline.isset("unwinding-assertions");
185 bool partial_loops=cmdline.isset("partial-loops");
186 bool continue_as_loops=cmdline.isset("continue-as-loops");
187
188 if(unwinding_assertions+partial_loops+continue_as_loops>1)
189 throw "more than one of --unwinding-assertions,--partial-loops,"
190 "--continue-as-loops selected";
191
194
195 if(unwinding_assertions)
196 {
198 }
199 else if(partial_loops)
200 {
202 }
203 else if(continue_as_loops)
204 {
206 }
207
210
211 if(cmdline.isset("log"))
212 {
213 std::string filename=cmdline.get_value("log");
214 bool have_file=!filename.empty() && filename!="-";
215
216 jsont result=goto_unwind.output_log_json();
217
218 if(have_file)
219 {
220#ifdef _MSC_VER
221 std::ofstream of(widen(filename));
222#else
223 std::ofstream of(filename);
224#endif
225 if(!of)
226 throw "failed to open file "+filename;
227
228 of << result;
229 of.close();
230 }
231 else
232 {
233 std::cout << result << '\n';
234 }
235 }
236
237 // goto_unwind holds references to instructions, only do remove_skip
238 // after having generated the log above
240 }
241 }
242
243 if(cmdline.isset("show-threaded"))
244 {
246
247 is_threadedt is_threaded(goto_model);
248
250 {
251 std::cout << "////\n";
252 std::cout << "//// Function: " << gf_entry.first << '\n';
253 std::cout << "////\n\n";
254
255 const goto_programt &goto_program = gf_entry.second.body;
256
258 {
259 goto_program.output_instruction(ns, gf_entry.first, std::cout, *i_it);
260 std::cout << "Is threaded: " << (is_threaded(i_it)?"True":"False")
261 << "\n\n";
262 }
263 }
264
266 }
267
268 if(cmdline.isset("insert-final-assert-false"))
269 {
270 log.status() << "Inserting final assert false" << messaget::eom;
273 cmdline.get_value("insert-final-assert-false"),
275 if(fail)
276 {
278 }
279 // otherwise, fall-through to write new binary
280 }
281
282 if(cmdline.isset("show-value-sets"))
283 {
285
286 // recalculate numbers, etc.
288
289 log.status() << "Pointer Analysis" << messaget::eom;
296 }
297
298 if(cmdline.isset("show-global-may-alias"))
299 {
303
304 // recalculate numbers, etc.
306
310
312 }
313
314 if(cmdline.isset("show-local-bitvector-analysis"))
315 {
318
319 // recalculate numbers, etc.
321
323
325 {
326 local_bitvector_analysist local_bitvector_analysis(gf_entry.second, ns);
327 std::cout << ">>>>\n";
328 std::cout << ">>>> " << gf_entry.first << '\n';
329 std::cout << ">>>>\n";
330 local_bitvector_analysis.output(std::cout, gf_entry.second, ns);
331 std::cout << '\n';
332 }
333
335 }
336
337 if(cmdline.isset("show-local-safe-pointers") ||
338 cmdline.isset("show-safe-dereferences"))
339 {
340 // Ensure location numbering is unique:
342
344
346 {
348 local_safe_pointers(gf_entry.second.body);
349 std::cout << ">>>>\n";
350 std::cout << ">>>> " << gf_entry.first << '\n';
351 std::cout << ">>>>\n";
352 if(cmdline.isset("show-local-safe-pointers"))
353 local_safe_pointers.output(std::cout, gf_entry.second.body, ns);
354 else
355 {
356 local_safe_pointers.output_safe_dereferences(
357 std::cout, gf_entry.second.body, ns);
358 }
359 std::cout << '\n';
360 }
361
363 }
364
365 if(cmdline.isset("show-sese-regions"))
366 {
367 // Ensure location numbering is unique:
369
371
373 {
375 sese_region_analysis(gf_entry.second.body);
376 std::cout << ">>>>\n";
377 std::cout << ">>>> " << gf_entry.first << '\n';
378 std::cout << ">>>>\n";
379 sese_region_analysis.output(std::cout, gf_entry.second.body, ns);
380 std::cout << '\n';
381 }
382
384 }
385
386 if(cmdline.isset("show-custom-bitvector-analysis"))
387 {
391
393
394 if(!cmdline.isset("inline"))
395 {
398 }
399
400 // recalculate numbers, etc.
402
406
408 }
409
410 if(cmdline.isset("show-escape-analysis"))
411 {
415
416 // recalculate numbers, etc.
418
422
424 }
425
426 if(cmdline.isset("custom-bitvector-analysis"))
427 {
431
433
434 if(!cmdline.isset("inline"))
435 {
438 }
439
440 // recalculate numbers, etc.
442
444
449 cmdline.isset("xml-ui"),
450 std::cout);
451
453 }
454
455 if(cmdline.isset("show-points-to"))
456 {
458
459 // recalculate numbers, etc.
461
463
464 log.status() << "Pointer Analysis" << messaget::eom;
467 points_to.output(std::cout);
469 }
470
471 if(cmdline.isset("show-intervals"))
472 {
474
475 // recalculate numbers, etc.
477
478 log.status() << "Interval Analysis" << messaget::eom;
484 }
485
486 if(cmdline.isset("show-call-sequences"))
487 {
491 }
492
493 if(cmdline.isset("check-call-sequence"))
494 {
498 }
499
500 if(cmdline.isset("list-calls-args"))
501 {
503
505
507 }
508
509 if(cmdline.isset("show-rw-set"))
510 {
512
513 if(!cmdline.isset("inline"))
514 {
516
517 // recalculate numbers, etc.
519 }
520
521 log.status() << "Pointer Analysis" << messaget::eom;
524
525 const symbolt &symbol=ns.lookup(ID_main);
526 symbol_exprt main(symbol.name, symbol.type);
527
528 std::cout <<
531 }
532
533 if(cmdline.isset("show-symbol-table"))
534 {
537 }
538
539 if(cmdline.isset("show-reaching-definitions"))
540 {
542
546 rd_analysis.output(goto_model, std::cout);
547
549 }
550
551 if(cmdline.isset("show-dependence-graph"))
552 {
554
559 dependence_graph.output_dot(std::cout);
560
562 }
563
564 if(cmdline.isset("count-eloc"))
565 {
568 }
569
570 if(cmdline.isset("list-eloc"))
571 {
574 }
575
576 if(cmdline.isset("print-path-lengths"))
577 {
580 }
581
582 if(cmdline.isset("print-global-state-size"))
583 {
586 }
587
588 if(cmdline.isset("list-symbols"))
589 {
592 }
593
594 if(cmdline.isset("show-uninitialized"))
595 {
596 show_uninitialized(goto_model, std::cout);
598 }
599
600 if(cmdline.isset("interpreter"))
601 {
604
605 log.status() << "Starting interpreter" << messaget::eom;
608 }
609
610 if(cmdline.isset("show-claims") ||
611 cmdline.isset("show-properties"))
612 {
616 }
617
618 if(cmdline.isset("document-claims-html") ||
619 cmdline.isset("document-properties-html"))
620 {
623 }
624
625 if(cmdline.isset("document-claims-latex") ||
626 cmdline.isset("document-properties-latex"))
627 {
630 }
631
632 if(cmdline.isset("show-loops"))
633 {
636 }
637
638 if(cmdline.isset("show-natural-loops"))
639 {
640 show_natural_loops(goto_model, std::cout);
642 }
643
644 if(cmdline.isset("show-lexical-loops"))
645 {
646 show_lexical_loops(goto_model, std::cout);
647 }
648
649 if(cmdline.isset("print-internal-representation"))
650 {
651 for(auto const &pair : goto_model.goto_functions.function_map)
652 for(auto const &ins : pair.second.body.instructions)
653 {
654 if(ins.get_code().is_not_nil())
655 log.status() << ins.get_code().pretty() << messaget::eom;
656 if(ins.has_condition())
657 {
658 log.status() << "[guard] " << ins.get_condition().pretty()
659 << messaget::eom;
660 }
661 }
663 }
664
665 if(
666 cmdline.isset("show-goto-functions") ||
667 cmdline.isset("list-goto-functions"))
668 {
670 goto_model, ui_message_handler, cmdline.isset("list-goto-functions"));
672 }
673
674 if(cmdline.isset("list-undefined-functions"))
675 {
678 }
679
680 // experimental: print structs
681 if(cmdline.isset("show-struct-alignment"))
682 {
685 }
686
687 if(cmdline.isset("show-locations"))
688 {
691 }
692
693 if(
694 cmdline.isset("dump-c") || cmdline.isset("dump-cpp") ||
695 cmdline.isset("dump-c-type-header"))
696 {
697 const bool is_cpp=cmdline.isset("dump-cpp");
698 const bool is_header = cmdline.isset("dump-c-type-header");
699 const bool h_libc=!cmdline.isset("no-system-headers");
700 const bool h_all=cmdline.isset("use-all-headers");
701 const bool harness=cmdline.isset("harness");
703
704 // restore RETURN instructions in case remove_returns had been
705 // applied
707
708 // dump_c (actually goto_program2code) requires valid instruction
709 // location numbers:
711
712 if(cmdline.args.size()==2)
713 {
714 #ifdef _MSC_VER
715 std::ofstream out(widen(cmdline.args[1]));
716 #else
717 std::ofstream out(cmdline.args[1]);
718 #endif
719 if(!out)
720 {
721 log.error() << "failed to write to '" << cmdline.args[1] << "'";
723 }
724 if(is_header)
725 {
728 h_libc,
729 h_all,
730 harness,
731 ns,
732 cmdline.get_value("dump-c-type-header"),
733 out);
734 }
735 else
736 {
737 (is_cpp ? dump_cpp : dump_c)(
738 goto_model.goto_functions, h_libc, h_all, harness, ns, out);
739 }
740 }
741 else
742 {
743 if(is_header)
744 {
747 h_libc,
748 h_all,
749 harness,
750 ns,
751 cmdline.get_value("dump-c-type-header"),
752 std::cout);
753 }
754 else
755 {
756 (is_cpp ? dump_cpp : dump_c)(
757 goto_model.goto_functions, h_libc, h_all, harness, ns, std::cout);
758 }
759 }
760
762 }
763
764 if(cmdline.isset("call-graph"))
765 {
767 call_grapht call_graph(goto_model);
768
769 if(cmdline.isset("xml"))
770 call_graph.output_xml(std::cout);
771 else if(cmdline.isset("dot"))
772 call_graph.output_dot(std::cout);
773 else
774 call_graph.output(std::cout);
775
777 }
778
779 if(cmdline.isset("reachable-call-graph"))
780 {
782 call_grapht call_graph =
785 if(cmdline.isset("xml"))
786 call_graph.output_xml(std::cout);
787 else if(cmdline.isset("dot"))
788 call_graph.output_dot(std::cout);
789 else
790 call_graph.output(std::cout);
791
792 return 0;
793 }
794
795 if(cmdline.isset("show-class-hierarchy"))
796 {
799 if(cmdline.isset("dot"))
800 hierarchy.output_dot(std::cout);
801 else
803
805 }
806
807 if(cmdline.isset("dot"))
808 {
810
811 if(cmdline.args.size()==2)
812 {
813 #ifdef _MSC_VER
814 std::ofstream out(widen(cmdline.args[1]));
815 #else
816 std::ofstream out(cmdline.args[1]);
817 #endif
818 if(!out)
819 {
820 log.error() << "failed to write to " << cmdline.args[1] << "'";
822 }
823
824 dot(goto_model, out);
825 }
826 else
827 dot(goto_model, std::cout);
828
830 }
831
832 if(cmdline.isset("accelerate"))
833 {
835
837
838 log.status() << "Performing full inlining" << messaget::eom;
840
841 log.status() << "Removing calls to functions without a body"
842 << messaget::eom;
845
846 log.status() << "Accelerating" << messaget::eom;
847 guard_managert guard_manager;
849 goto_model, ui_message_handler, cmdline.isset("z3"), guard_manager);
851 }
852
853 if(cmdline.isset("horn-encoding"))
854 {
855 log.status() << "Horn-clause encoding" << messaget::eom;
857
858 if(cmdline.args.size()==2)
859 {
860 #ifdef _MSC_VER
861 std::ofstream out(widen(cmdline.args[1]));
862 #else
863 std::ofstream out(cmdline.args[1]);
864 #endif
865
866 if(!out)
867 {
868 log.error() << "Failed to open output file " << cmdline.args[1]
869 << messaget::eom;
871 }
872
874 }
875 else
876 horn_encoding(goto_model, std::cout);
877
879 }
880
881 if(cmdline.isset("drop-unused-functions"))
882 {
884
885 log.status() << "Removing unused functions" << messaget::eom;
887 }
888
889 if(cmdline.isset("undefined-function-is-assume-false"))
890 {
893 }
894
895 // write new binary?
896 if(cmdline.args.size()==2)
897 {
898 log.status() << "Writing GOTO program to '" << cmdline.args[1] << "'"
899 << messaget::eom;
900
903 else
905 }
906 else if(cmdline.args.size() < 2)
907 {
909 "Invalid number of positional arguments passed",
910 "[in] [out]",
911 "goto-instrument needs one input and one output file, aside from other "
912 "flags");
913 }
914
915 help();
917 }
918// NOLINTNEXTLINE(readability/fn_size)
919}
920
922 bool force)
923{
925 return;
926
928
929 log.status() << "Function Pointer Removal" << messaget::eom;
931 ui_message_handler, goto_model, cmdline.isset("pointer-check"));
932 log.status() << "Virtual function removal" << messaget::eom;
934 log.status() << "Cleaning inline assembler statements" << messaget::eom;
936}
937
942{
943 // Don't bother if we've already done a full function pointer
944 // removal.
946 {
947 return;
948 }
949
950 log.status() << "Removing const function pointers only" << messaget::eom;
954 cmdline.isset("pointer-check"),
955 true); // abort if we can't resolve via const pointers
956}
957
959{
961 return;
962
964
965 if(!cmdline.isset("inline"))
966 {
967 log.status() << "Partial Inlining" << messaget::eom;
969 }
970}
971
973{
975 return;
976
978
979 log.status() << "Removing returns" << messaget::eom;
981}
982
984{
985 log.status() << "Reading GOTO program from '" << cmdline.args[0] << "'"
986 << messaget::eom;
987
989
991
992 if(!result.has_value())
993 throw 0;
994
995 goto_model = std::move(result.value());
996
998}
999
1001{
1002 optionst options;
1003
1005
1006 // disable simplify when adding various checks?
1007 if(cmdline.isset("no-simplify"))
1008 options.set_option("simplify", false);
1009 else
1010 options.set_option("simplify", true);
1011
1012 // all checks supported by goto_check
1014
1015 // unwind loops
1016 if(cmdline.isset("unwind"))
1017 {
1018 log.status() << "Unwinding loops" << messaget::eom;
1019 options.set_option("unwind", cmdline.get_value("unwind"));
1020 }
1021
1022 {
1024
1025 if(
1029 {
1031
1033 }
1034 }
1035
1036 // skip over selected loops
1037 if(cmdline.isset("skip-loops"))
1038 {
1039 log.status() << "Adding gotos to skip loops" << messaget::eom;
1040 if(skip_loops(
1042 throw 0;
1043 }
1044
1046
1047 // initialize argv with valid pointers
1048 if(cmdline.isset("model-argc-argv"))
1049 {
1050 unsigned max_argc=
1051 safe_string2unsigned(cmdline.get_value("model-argc-argv"));
1052 std::list<std::string> argv;
1053 argv.resize(max_argc);
1054
1055 log.status() << "Adding up to " << max_argc << " command line arguments"
1056 << messaget::eom;
1057
1058 if(model_argc_argv(
1059 goto_model, argv, true /*model_argv*/, ui_message_handler))
1060 throw 0;
1061 }
1062
1063 if(cmdline.isset("add-cmd-line-arg"))
1064 {
1065 const std::list<std::string> &argv = cmdline.get_values("add-cmd-line-arg");
1066 unsigned argc = 0;
1067
1068 std::stringstream ss;
1069 ss << "[";
1070 std::string sep = "";
1071 for(auto const &arg : argv)
1072 {
1073 ss << sep << "\"" << arg << "\"";
1074 argc++;
1075 sep = ", ";
1076 }
1077 ss << "]";
1078
1079 log.status() << "Adding " << argc << " arguments: " << ss.str()
1080 << messaget::eom;
1081
1082 if(model_argc_argv(
1083 goto_model, argv, false /*model_argv*/, ui_message_handler))
1084 throw 0;
1085 }
1086
1087 if(cmdline.isset("remove-function-body"))
1088 {
1090 goto_model,
1091 cmdline.get_values("remove-function-body"),
1093 }
1094
1095 // we add the library in some cases, as some analyses benefit
1096
1097 if(cmdline.isset("add-library") ||
1098 cmdline.isset("mm"))
1099 {
1100 if(cmdline.isset("show-custom-bitvector-analysis") ||
1101 cmdline.isset("custom-bitvector-analysis"))
1102 {
1103 config.ansi_c.defines.push_back(
1104 std::string(CPROVER_PREFIX) + "CUSTOM_BITVECTOR_ANALYSIS");
1105 }
1106
1107 // add the library
1108 log.status() << "Adding CPROVER library (" << config.ansi_c.arch << ")"
1109 << messaget::eom;
1113 }
1114
1115 // now do full inlining, if requested
1116 if(cmdline.isset("inline"))
1117 {
1119
1120 if(cmdline.isset("show-custom-bitvector-analysis") ||
1121 cmdline.isset("custom-bitvector-analysis"))
1122 {
1126 }
1127
1128 log.status() << "Performing full inlining" << messaget::eom;
1130 }
1131
1132 if(cmdline.isset("show-custom-bitvector-analysis") ||
1133 cmdline.isset("custom-bitvector-analysis"))
1134 {
1135 log.status() << "Propagating Constants" << messaget::eom;
1138 }
1139
1140 if(cmdline.isset("escape-analysis"))
1141 {
1145
1146 // recalculate numbers, etc.
1148
1149 log.status() << "Escape Analysis" << messaget::eom;
1152 escape_analysis.instrument(goto_model);
1153
1154 // inline added functions, they are often small
1156
1157 // recalculate numbers, etc.
1159 }
1160
1161 if(
1164 {
1167
1168 std::set<std::string> to_replace(
1171
1172 std::set<std::string> to_enforce(
1175
1176 // It’s important to keep the order of contracts instrumentation, i.e.,
1177 // first replacement then enforcement. We rely on contract replacement
1178 // and inlining of sub-function calls to properly annotate all
1179 // assignments.
1180 contracts.replace_calls(to_replace);
1181 contracts.enforce_contracts(to_enforce);
1182
1184 contracts.apply_loop_contracts();
1185 }
1186
1187 if(cmdline.isset("value-set-fi-fp-removal"))
1188 {
1191 }
1192
1193 // replace function pointers, if explicitly requested
1194 if(cmdline.isset("remove-function-pointers"))
1195 {
1197 }
1198 else if(cmdline.isset("remove-const-function-pointers"))
1199 {
1201 }
1202
1203 if(cmdline.isset("replace-calls"))
1204 {
1206
1207 replace_callst replace_calls;
1208 replace_calls(goto_model, cmdline.get_values("replace-calls"));
1209 }
1210
1211 if(cmdline.isset("function-inline"))
1212 {
1213 std::string function=cmdline.get_value("function-inline");
1214 PRECONDITION(!function.empty());
1215
1216 bool caching=!cmdline.isset("no-caching");
1217
1219
1220 log.status() << "Inlining calls of function '" << function << "'"
1221 << messaget::eom;
1222
1223 if(!cmdline.isset("log"))
1224 {
1226 goto_model, function, ui_message_handler, true, caching);
1227 }
1228 else
1229 {
1230 std::string filename=cmdline.get_value("log");
1231 bool have_file=!filename.empty() && filename!="-";
1232
1234 goto_model, function, ui_message_handler, true, caching);
1235
1236 if(have_file)
1237 {
1238#ifdef _MSC_VER
1239 std::ofstream of(widen(filename));
1240#else
1241 std::ofstream of(filename);
1242#endif
1243 if(!of)
1244 throw "failed to open file "+filename;
1245
1246 of << result;
1247 of.close();
1248 }
1249 else
1250 {
1251 std::cout << result << '\n';
1252 }
1253 }
1254
1257 }
1258
1259 if(cmdline.isset("partial-inline"))
1260 {
1262
1263 log.status() << "Partial inlining" << messaget::eom;
1265
1268 }
1269
1270 if(cmdline.isset("remove-calls-no-body"))
1271 {
1272 log.status() << "Removing calls to functions without a body"
1273 << messaget::eom;
1274
1277
1280 }
1281
1282 if(cmdline.isset("constant-propagator"))
1283 {
1285
1286 log.status() << "Propagating Constants" << messaget::eom;
1287
1290 }
1291
1292 if(cmdline.isset("generate-function-body"))
1293 {
1296 c_object_factory_parameterst object_factory_parameters(
1298
1300 cmdline.get_value("generate-function-body-options"),
1301 object_factory_parameters,
1305 std::regex(cmdline.get_value("generate-function-body")),
1307 goto_model,
1309 }
1310
1311 if(cmdline.isset("generate-havocing-body"))
1312 {
1315 c_object_factory_parameterst object_factory_parameters(
1317
1318 auto options_split =
1319 split_string(cmdline.get_value("generate-havocing-body"), ',');
1320 if(options_split.size() < 2)
1322 "not enough arguments for this option", "--generate-havocing-body"};
1323
1324 if(options_split.size() == 2)
1325 {
1327 std::string{"havoc,"} + options_split.back(),
1328 object_factory_parameters,
1332 std::regex(options_split[0]),
1334 goto_model,
1336 }
1337 else
1338 {
1339 CHECK_RETURN(options_split.size() % 2 == 1);
1340 for(size_t i = 1; i + 1 < options_split.size(); i += 2)
1341 {
1343 std::string{"havoc,"} + options_split[i + 1],
1344 object_factory_parameters,
1348 options_split[0],
1351 goto_model,
1353 }
1354 }
1355 }
1356
1357 // add generic checks, if needed
1359
1360 // check for uninitalized local variables
1361 if(cmdline.isset("uninitialized-check"))
1362 {
1363 log.status() << "Adding checks for uninitialized local variables"
1364 << messaget::eom;
1366 }
1367
1368 // check for maximum call stack size
1369 if(cmdline.isset("stack-depth"))
1370 {
1371 log.status() << "Adding check for maximum call stack size" << messaget::eom;
1373 goto_model,
1374 safe_string2size_t(cmdline.get_value("stack-depth")),
1376 }
1377
1378 // ignore default/user-specified initialization of variables with static
1379 // lifetime
1380 if(cmdline.isset("nondet-static-exclude"))
1381 {
1382 log.status() << "Adding nondeterministic initialization "
1383 "of static/global variables except for "
1384 "the specified ones."
1385 << messaget::eom;
1386
1387 nondet_static(goto_model, cmdline.get_values("nondet-static-exclude"));
1388 }
1389 else if(cmdline.isset("nondet-static"))
1390 {
1391 log.status() << "Adding nondeterministic initialization "
1392 "of static/global variables"
1393 << messaget::eom;
1395 }
1396
1397 if(cmdline.isset("slice-global-inits"))
1398 {
1399 log.status() << "Slicing away initializations of unused global variables"
1400 << messaget::eom;
1402 }
1403
1404 if(cmdline.isset("string-abstraction"))
1405 {
1408
1409 log.status() << "String Abstraction" << messaget::eom;
1411 }
1412
1413 // some analyses require function pointer removal and partial inlining
1414
1415 if(cmdline.isset("remove-pointers") ||
1416 cmdline.isset("race-check") ||
1417 cmdline.isset("mm") ||
1418 cmdline.isset("isr") ||
1419 cmdline.isset("concurrency"))
1420 {
1422
1423 log.status() << "Pointer Analysis" << messaget::eom;
1426
1427 if(cmdline.isset("remove-pointers"))
1428 {
1429 // removing pointers
1430 log.status() << "Removing Pointers" << messaget::eom;
1432 }
1433
1434 if(cmdline.isset("race-check"))
1435 {
1436 log.status() << "Adding Race Checks" << messaget::eom;
1438 }
1439
1440 if(cmdline.isset("mm"))
1441 {
1442 std::string mm=cmdline.get_value("mm");
1443 memory_modelt model;
1444
1445 // strategy of instrumentation
1447 if(cmdline.isset("one-event-per-cycle"))
1449 else if(cmdline.isset("minimum-interference"))
1451 else if(cmdline.isset("read-first"))
1453 else if(cmdline.isset("write-first"))
1455 else if(cmdline.isset("my-events"))
1457 else
1458 /* default: instruments all unsafe pairs */
1460
1461 const unsigned max_var=
1462 cmdline.isset("max-var")?
1464 const unsigned max_po_trans=
1465 cmdline.isset("max-po-trans")?
1466 unsafe_string2unsigned(cmdline.get_value("max-po-trans")):0;
1467
1468 if(mm=="tso")
1469 {
1470 log.status() << "Adding weak memory (TSO) Instrumentation"
1471 << messaget::eom;
1472 model=TSO;
1473 }
1474 else if(mm=="pso")
1475 {
1476 log.status() << "Adding weak memory (PSO) Instrumentation"
1477 << messaget::eom;
1478 model=PSO;
1479 }
1480 else if(mm=="rmo")
1481 {
1482 log.status() << "Adding weak memory (RMO) Instrumentation"
1483 << messaget::eom;
1484 model=RMO;
1485 }
1486 else if(mm=="power")
1487 {
1488 log.status() << "Adding weak memory (Power) Instrumentation"
1489 << messaget::eom;
1490 model=Power;
1491 }
1492 else
1493 {
1494 log.error() << "Unknown weak memory model '" << mm << "'"
1495 << messaget::eom;
1496 model=Unknown;
1497 }
1498
1500
1501 if(cmdline.isset("force-loop-duplication"))
1502 loops=all_loops;
1503 if(cmdline.isset("no-loop-duplication"))
1504 loops=no_loop;
1505
1506 if(model!=Unknown)
1508 model,
1510 goto_model,
1511 cmdline.isset("scc"),
1513 !cmdline.isset("cfg-kill"),
1514 cmdline.isset("no-dependencies"),
1515 loops,
1516 max_var,
1517 max_po_trans,
1518 !cmdline.isset("no-po-rendering"),
1519 cmdline.isset("render-cluster-file"),
1520 cmdline.isset("render-cluster-function"),
1521 cmdline.isset("cav11"),
1522 cmdline.isset("hide-internals"),
1524 cmdline.isset("ignore-arrays"));
1525 }
1526
1527 // Interrupt handler
1528 if(cmdline.isset("isr"))
1529 {
1530 log.status() << "Instrumenting interrupt handler" << messaget::eom;
1531 interrupt(
1533 goto_model,
1534 cmdline.get_value("isr"));
1535 }
1536
1537 // Memory-mapped I/O
1538 if(cmdline.isset("mmio"))
1539 {
1540 log.status() << "Instrumenting memory-mapped I/O" << messaget::eom;
1542 }
1543
1544 if(cmdline.isset("concurrency"))
1545 {
1546 log.status() << "Sequentializing concurrency" << messaget::eom;
1548 }
1549 }
1550
1551 if(cmdline.isset("interval-analysis"))
1552 {
1553 log.status() << "Interval analysis" << messaget::eom;
1555 }
1556
1557 if(cmdline.isset("havoc-loops"))
1558 {
1559 log.status() << "Havocking loops" << messaget::eom;
1561 }
1562
1563 if(cmdline.isset("k-induction"))
1564 {
1565 bool base_case=cmdline.isset("base-case");
1566 bool step_case=cmdline.isset("step-case");
1567
1568 if(step_case && base_case)
1569 throw "please specify only one of --step-case and --base-case";
1570 else if(!step_case && !base_case)
1571 throw "please specify one of --step-case and --base-case";
1572
1573 unsigned k=unsafe_string2unsigned(cmdline.get_value("k-induction"));
1574
1575 if(k==0)
1576 throw "please give k>=1";
1577
1578 log.status() << "Instrumenting k-induction for k=" << k << ", "
1579 << (base_case ? "base case" : "step case") << messaget::eom;
1580
1581 k_induction(goto_model, base_case, step_case, k);
1582 }
1583
1584 if(cmdline.isset("function-enter"))
1585 {
1586 log.status() << "Function enter instrumentation" << messaget::eom;
1588 goto_model,
1589 cmdline.get_value("function-enter"));
1590 }
1591
1592 if(cmdline.isset("function-exit"))
1593 {
1594 log.status() << "Function exit instrumentation" << messaget::eom;
1596 goto_model,
1597 cmdline.get_value("function-exit"));
1598 }
1599
1600 if(cmdline.isset("branch"))
1601 {
1602 log.status() << "Branch instrumentation" << messaget::eom;
1603 branch(
1604 goto_model,
1605 cmdline.get_value("branch"));
1606 }
1607
1608 // add failed symbols
1610
1611 // recalculate numbers, etc.
1613
1614 // add loop ids
1616
1617 // label the assertions
1619
1620 nondet_volatile(goto_model, options);
1621
1622 // reachability slice?
1623 if(cmdline.isset("reachability-slice"))
1624 {
1626
1627 log.status() << "Performing a reachability slice" << messaget::eom;
1628
1629 // reachability_slicer requires that the model has unique location numbers:
1631
1632 if(cmdline.isset("property"))
1634 else
1636 }
1637
1638 if(cmdline.isset("fp-reachability-slice"))
1639 {
1641
1642 log.status() << "Performing a function pointer reachability slice"
1643 << messaget::eom;
1645 goto_model, cmdline.get_comma_separated_values("fp-reachability-slice"));
1646 }
1647
1648 // full slice?
1649 if(cmdline.isset("full-slice"))
1650 {
1653
1654 log.status() << "Performing a full slice" << messaget::eom;
1655 if(cmdline.isset("property"))
1657 else
1658 {
1659 // full_slicer requires that the model has unique location numbers:
1662 }
1663 }
1664
1665 // splice option
1666 if(cmdline.isset("splice-call"))
1667 {
1668 log.status() << "Performing call splicing" << messaget::eom;
1669 std::string callercallee=cmdline.get_value("splice-call");
1670 if(splice_call(
1675 throw 0;
1676 }
1677
1678 // aggressive slicer
1679 if(cmdline.isset("aggressive-slice"))
1680 {
1682
1683 // reachability_slicer requires that the model has unique location numbers:
1685
1686 log.status() << "Slicing away initializations of unused global variables"
1687 << messaget::eom;
1689
1690 log.status() << "Performing an aggressive slice" << messaget::eom;
1692
1693 if(cmdline.isset("aggressive-slice-call-depth"))
1694 aggressive_slicer.call_depth =
1695 safe_string2unsigned(cmdline.get_value("aggressive-slice-call-depth"));
1696
1697 if(cmdline.isset("aggressive-slice-preserve-function"))
1698 aggressive_slicer.preserve_functions(
1699 cmdline.get_values("aggressive-slice-preserve-function"));
1700
1701 if(cmdline.isset("property"))
1702 aggressive_slicer.user_specified_properties =
1703 cmdline.get_values("property");
1704
1705 if(cmdline.isset("aggressive-slice-preserve-functions-containing"))
1706 aggressive_slicer.name_snippets =
1707 cmdline.get_values("aggressive-slice-preserve-functions-containing");
1708
1709 aggressive_slicer.preserve_all_direct_paths =
1710 cmdline.isset("aggressive-slice-preserve-all-direct-paths");
1711
1712 aggressive_slicer.doit();
1713
1715
1716 log.status() << "Performing a reachability slice" << messaget::eom;
1717 if(cmdline.isset("property"))
1719 else
1721 }
1722
1723 if(cmdline.isset("ensure-one-backedge-per-target"))
1724 {
1725 log.status() << "Trying to force one backedge per target" << messaget::eom;
1727 }
1728
1729 // recalculate numbers, etc.
1731}
1732
1735{
1736 // clang-format off
1737 std::cout << '\n' << banner_string("Goto-Instrument", CBMC_VERSION) << '\n'
1738 << align_center_with_border("Copyright (C) 2008-2013") << '\n'
1739 << align_center_with_border("Daniel Kroening") << '\n'
1740 << align_center_with_border("kroening@kroening.com") << '\n'
1741 <<
1742 "\n"
1743 "Usage: Purpose:\n"
1744 "\n"
1745 " goto-instrument [-?] [-h] [--help] show help\n"
1746 " goto-instrument in out perform instrumentation\n"
1747 "\n"
1748 "Main options:\n"
1750 " --dot generate CFG graph in DOT format\n"
1751 " --interpreter do concrete execution\n"
1752 "\n"
1753 "Dump Source:\n"
1755 "\n"
1756 "Diagnosis:\n"
1758 " --show-symbol-table show loaded symbol table\n"
1759 " --list-symbols list symbols with type information\n"
1762 " --drop-unused-functions drop functions trivially unreachable from main function\n" // NOLINT(*)
1763 " --print-internal-representation\n" // NOLINTNEXTLINE(*)
1764 " show verbose internal representation of the program\n"
1765 " --list-undefined-functions list functions without body\n"
1766 " --show-struct-alignment show struct members that might be concurrently accessed\n" // NOLINT(*)
1767 " --show-natural-loops show natural loop heads\n"
1768 // NOLINTNEXTLINE(whitespace/line_length)
1769 " --list-calls-args list all function calls with their arguments\n"
1770 " --call-graph show graph of function calls\n"
1771 // NOLINTNEXTLINE(whitespace/line_length)
1772 " --reachable-call-graph show graph of function calls potentially reachable from main function\n"
1774 // NOLINTNEXTLINE(whitespace/line_length)
1775 " --show-threaded show instructions that may be executed by more than one thread\n"
1776 " --show-local-safe-pointers show pointer expressions that are trivially dominated by a not-null check\n" // NOLINT(*)
1777 " --show-safe-dereferences show pointer expressions that are trivially dominated by a not-null check\n" // NOLINT(*)
1778 " *and* used as a dereference operand\n" // NOLINT(*)
1780 // NOLINTNEXTLINE(whitespace/line_length)
1781 " --validate-goto-binary check the well-formedness of the passed in goto\n"
1782 " binary and then exit\n"
1783 "\n"
1784 "Safety checks:\n"
1785 " --no-assertions ignore user assertions\n"
1788 " --stack-depth n add check that call stack size of non-inlined functions never exceeds n\n" // NOLINT(*)
1789 " --race-check add floating-point data race checks\n"
1790 "\n"
1791 "Semantic transformations:\n"
1794 " --unwindset-file <file> read unwindset from file\n"
1795 " --partial-loops permit paths with partial loops\n"
1796 " --unwinding-assertions generate unwinding assertions\n"
1797 " --continue-as-loops add loop for remaining iterations after unwound part\n" // NOLINT(*)
1798 " --isr <function> instruments an interrupt service routine\n"
1799 " --mmio instruments memory-mapped I/O\n"
1800 " --nondet-static add nondeterministic initialization of variables with static lifetime\n" // NOLINT(*)
1801 " --nondet-static-exclude e same as nondet-static except for the variable e\n" //NOLINT(*)
1802 " (use multiple times if required)\n"
1803 " --check-invariant function instruments invariant checking function\n"
1805 " --splice-call caller,callee prepends a call to callee in the body of caller\n" // NOLINT(*)
1806 " --undefined-function-is-assume-false\n"
1807 // NOLINTNEXTLINE(whitespace/line_length)
1808 " convert each call to an undefined function to assume(false)\n"
1812 "\n"
1813 "Loop transformations:\n"
1814 " --k-induction <k> check loops with k-induction\n"
1815 " --step-case k-induction: do step-case\n"
1816 " --base-case k-induction: do base-case\n"
1817 " --havoc-loops over-approximate all loops\n"
1818 " --accelerate add loop accelerators\n"
1819 " --skip-loops <loop-ids> add gotos to skip selected loops during execution\n" // NOLINT(*)
1820 "\n"
1821 "Memory model instrumentations:\n"
1823 "\n"
1824 "Slicing:\n"
1826 " --full-slice slice away instructions that don't affect assertions\n" // NOLINT(*)
1827 " --property id slice with respect to specific property only\n" // NOLINT(*)
1828 " --slice-global-inits slice away initializations of unused global variables\n" // NOLINT(*)
1829 " --aggressive-slice remove bodies of any functions not on the shortest path between\n" // NOLINT(*)
1830 " the start function and the function containing the property(s)\n" // NOLINT(*)
1831 " --aggressive-slice-call-depth <n>\n"
1832 " used with aggressive-slice, preserves all functions within <n> function calls\n" // NOLINT(*)
1833 " of the functions on the shortest path\n"
1834 " --aggressive-slice-preserve-function <f>\n"
1835 " force the aggressive slicer to preserve function <f>\n" // NOLINT(*)
1836 " --aggressive-slice-preserve-function containing <f>\n"
1837 " force the aggressive slicer to preserve all functions with names containing <f>\n" // NOLINT(*)
1838 "--aggressive-slice-preserve-all-direct-paths \n"
1839 " force aggressive slicer to preserve all direct paths\n" // NOLINT(*)
1840 "\n"
1841 "Further transformations:\n"
1842 " --constant-propagator propagate constants and simplify expressions\n" // NOLINT(*)
1843 " --inline perform full inlining\n"
1844 " --partial-inline perform partial inlining\n"
1845 " --function-inline <function> transitively inline all calls <function> makes\n" // NOLINT(*)
1846 " --no-caching disable caching of intermediate results during transitive function inlining\n" // NOLINT(*)
1847 " --log <file> log in json format which code segments were inlined, use with --function-inline\n" // NOLINT(*)
1848 " --remove-function-pointers replace function pointers by case statement over function calls\n" // NOLINT(*)
1849 " --value-set-fi-fp-removal build flow-insensitive value set and replace function pointers by a case statement\n" // NOLINT(*)
1850 " over the possible assignments. If the set of possible assignments is empty the function pointer\n" // NOLINT(*)
1851 " is removed using the standard remove-function-pointers pass. \n" // NOLINT(*)
1855 " --add-library add models of C library functions\n"
1858 // NOLINTNEXTLINE(whitespace/line_length)
1859 " --remove-function-body <f> remove the implementation of function <f> (may be repeated)\n"
1861 "\n"
1862 "Code contracts:\n"
1866 "\n"
1867 "Other options:\n"
1868 " --version show version and exit\n"
1870 " --xml output files in XML where supported\n"
1871 " --xml-ui use XML-formatted output\n"
1872 " --json-ui use JSON-formatted output\n"
1874 "\n";
1875 // clang-format on
1876}
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_tablet &symbol_table, std::ostream &out)
Alignment Checks.
void cprover_c_library_factory(const std::set< irep_idt > &functions, symbol_tablet &symbol_table, message_handlert &message_handler)
#define HELP_ANSI_C_LANGUAGE
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,...
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:40
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
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.
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 set_from_symbol_table(const symbol_tablet &)
Definition config.cpp:1254
bool set(const cmdlinet &cmdline)
Definition config.cpp:798
struct configt::ansi_ct ansi_c
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:98
symbol_tablet symbol_table
Symbol table.
Definition goto_model.h:30
goto_functionst goto_functions
GOTO functions.
Definition goto_model.h:33
A generic container class for the GOTO intermediate representation of one function.
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &instruction) const
Output a single instruction.
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...
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
@ 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
Expression to hold a symbol (variable)
Definition std_expr.h:80
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.
configt config
Definition config.cpp:25
#define HELP_CONFIG_LIBRARY
Definition config.h:62
Constant propagation.
#define HELP_REPLACE_CALL
Definition contracts.h:40
#define FLAG_REPLACE_CALL
Definition contracts.h:39
#define FLAG_ENFORCE_CONTRACT
Definition contracts.h:44
#define HELP_LOOP_CONTRACTS
Definition contracts.h:35
#define FLAG_LOOP_CONTRACTS
Definition contracts.h:34
#define HELP_ENFORCE_CONTRACT
Definition contracts.h:45
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, symbol_tablet &symbol_table, message_handlert &message_handler)
#define CPROVER_PREFIX
Field-insensitive, location-sensitive bitvector analysis.
Field-Sensitive Program Dependence Analysis, Litvak et al., FSE 2010.
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:353
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:1597
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:1584
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:1619
#define HELP_DUMP_C
Definition dump_c.h:52
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:101
void function_enter(goto_modelt &goto_model, const irep_idt &id)
Definition function.cpp:76
Function Entering and Exiting.
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.
void goto_check(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 havoc_loops(goto_modelt &goto_model)
Havoc Loops.
void horn_encoding(const goto_modelt &, std::ostream &)
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)
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
void parameter_assignments(symbol_tablet &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_tablet &symbol_table, const irep_idt &function_id, goto_programt &goto_program, w_guardst &w_guards)
Race Detection for Threaded Goto Programs.
void function_path_reachability_slicer(goto_modelt &goto_model, const std::list< std::string > &functions_list)
Perform reachability slicing on goto_model for selected functions.
void reachability_slicer(goto_modelt &goto_model, const bool include_forward_reachability)
Perform reachability slicing on goto_model, with respect to the criterion given by all properties.
#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.
bool remove_function_pointers(message_handlert &_message_handler, symbol_tablet &symbol_table, const goto_functionst &goto_functions, goto_programt &goto_program, const irep_idt &function_id, bool add_safety_assertion, 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
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.
void show_goto_functions(const namespacet &ns, ui_message_handlert &ui_message_handler, const goto_functionst &goto_functions, bool list_only)
#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_tablet &symbol_table, ui_message_handlert &ui)
void show_symbol_table_brief(const symbol_tablet &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_tablet &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(symbol_tablet &symbol_table, message_handlert &message_handler, goto_functionst &dest)
String Abstraction.
void split_string(const std::string &s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)
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.
std::wstring widen(const char *s)
Definition unicode.cpp:49
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:76
#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:94
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
bool write_goto_binary(std::ostream &out, const symbol_tablet &symbol_table, const goto_functionst &goto_functions, irep_serializationt &irepconverter)
Writes a goto program to disc, using goto binary format.
Write GOTO binaries.