cprover
goto_instrument_parse_options.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Main Module
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
13 
14 #include <fstream>
15 #include <iostream>
16 #include <memory>
17 
18 #include <util/config.h>
19 #include <util/exception_utils.h>
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/unicode.h>
25 #include <util/version.h>
26 
34 #include <goto-programs/loop_ids.h>
52 
58 
59 #include <analyses/call_graph.h>
67 #include <analyses/is_threaded.h>
68 #include <analyses/lexical_loops.h>
71 #include <analyses/natural_loops.h>
73 #include <analyses/sese_regions.h>
74 
75 #include <ansi-c/ansi_c_language.h>
77 #include <ansi-c/cprover_library.h>
78 
79 #include <assembler/remove_asm.h>
80 
81 #include <cpp/cprover_library.h>
82 
83 #include "accelerate/accelerate.h"
84 #include "alignment_checks.h"
85 #include "branch.h"
86 #include "call_sequences.h"
87 #include "concurrency.h"
88 #include "document_properties.h"
89 #include "dot.h"
90 #include "dump_c.h"
91 #include "full_slicer.h"
92 #include "function.h"
93 #include "havoc_loops.h"
94 #include "horn_encoding.h"
96 #include "interrupt.h"
97 #include "k_induction.h"
98 #include "mmio.h"
99 #include "model_argc_argv.h"
100 #include "nondet_static.h"
101 #include "nondet_volatile.h"
102 #include "points_to.h"
103 #include "race_check.h"
104 #include "reachability_slicer.h"
105 #include "remove_function.h"
106 #include "rw_set.h"
107 #include "show_locations.h"
108 #include "skip_loops.h"
109 #include "splice_call.h"
110 #include "stack_depth.h"
111 #include "thread_instrumentation.h"
112 #include "undefined_functions.h"
113 #include "uninitialized.h"
114 #include "unwind.h"
115 #include "value_set_fi_fp_removal.h"
116 #include "wmm/weak_memory.h"
117 
120 {
121  if(cmdline.isset("version"))
122  {
123  std::cout << CBMC_VERSION << '\n';
124  return CPROVER_EXIT_SUCCESS;
125  }
126 
127  if(cmdline.args.size()!=1 && cmdline.args.size()!=2)
128  {
129  help();
131  }
132 
135 
136  {
138 
140 
141  {
142  const bool validate_only = cmdline.isset("validate-goto-binary");
143 
144  if(validate_only || cmdline.isset("validate-goto-model"))
145  {
147 
148  if(validate_only)
149  {
150  return CPROVER_EXIT_SUCCESS;
151  }
152  }
153  }
154 
156 
157  if(cmdline.isset("validate-goto-model"))
158  {
160  }
161 
162  {
163  bool unwind_given=cmdline.isset("unwind");
164  bool unwindset_given=cmdline.isset("unwindset");
165  bool unwindset_file_given=cmdline.isset("unwindset-file");
166 
167  if(unwindset_given && unwindset_file_given)
168  throw "only one of --unwindset and --unwindset-file supported at a "
169  "time";
170 
171  if(unwind_given || unwindset_given || unwindset_file_given)
172  {
173  unwindsett unwindset;
174 
175  if(unwind_given)
176  unwindset.parse_unwind(cmdline.get_value("unwind"));
177 
178  if(unwindset_file_given)
179  unwindset.parse_unwindset_file(cmdline.get_value("unwindset-file"));
180 
181  if(unwindset_given)
182  unwindset.parse_unwindset(cmdline.get_values("unwindset"));
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 
192  goto_unwindt::unwind_strategyt unwind_strategy=
194 
195  if(unwinding_assertions)
196  {
198  }
199  else if(partial_loops)
200  {
202  }
203  else if(continue_as_loops)
204  {
206  }
207 
208  goto_unwindt goto_unwind;
209  goto_unwind(goto_model, unwindset, unwind_strategy);
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: " << f_it->first << '\n';
253  std::cout << "////\n\n";
254 
255  const goto_programt &goto_program=f_it->second.body;
256 
257  forall_goto_program_instructions(i_it, goto_program)
258  {
259  goto_program.output_instruction(ns, f_it->first, std::cout, *i_it);
260  std::cout << "Is threaded: " << (is_threaded(i_it)?"True":"False")
261  << "\n\n";
262  }
263  }
264 
265  return CPROVER_EXIT_SUCCESS;
266  }
267 
268  if(cmdline.isset("insert-final-assert-false"))
269  {
270  log.status() << "Inserting final assert false" << messaget::eom;
271  bool fail = insert_final_assert_false(
272  goto_model,
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;
291  value_set_analysist value_set_analysis(ns);
292  value_set_analysis(goto_model.goto_functions);
294  ui_message_handler.get_ui(), goto_model, value_set_analysis);
295  return CPROVER_EXIT_SUCCESS;
296  }
297 
298  if(cmdline.isset("show-global-may-alias"))
299  {
303 
304  // recalculate numbers, etc.
306 
307  global_may_alias_analysist global_may_alias_analysis;
308  global_may_alias_analysis(goto_model);
309  global_may_alias_analysis.output(goto_model, std::cout);
310 
311  return CPROVER_EXIT_SUCCESS;
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(it->second, ns);
327  std::cout << ">>>>\n";
328  std::cout << ">>>> " << it->first << '\n';
329  std::cout << ">>>>\n";
330  local_bitvector_analysis.output(std::cout, it->second, ns);
331  std::cout << '\n';
332  }
333 
334  return CPROVER_EXIT_SUCCESS;
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  {
347  local_safe_pointerst local_safe_pointers;
348  local_safe_pointers(it->second.body);
349  std::cout << ">>>>\n";
350  std::cout << ">>>> " << it->first << '\n';
351  std::cout << ">>>>\n";
352  if(cmdline.isset("show-local-safe-pointers"))
353  local_safe_pointers.output(std::cout, it->second.body, ns);
354  else
355  {
356  local_safe_pointers.output_safe_dereferences(
357  std::cout, it->second.body, ns);
358  }
359  std::cout << '\n';
360  }
361 
362  return CPROVER_EXIT_SUCCESS;
363  }
364 
365  if(cmdline.isset("show-sese-regions"))
366  {
367  // Ensure location numbering is unique:
369 
371 
373  {
374  sese_region_analysist sese_region_analysis;
375  sese_region_analysis(it->second.body);
376  std::cout << ">>>>\n";
377  std::cout << ">>>> " << it->first << '\n';
378  std::cout << ">>>>\n";
379  sese_region_analysis.output(std::cout, it->second.body, ns);
380  std::cout << '\n';
381  }
382 
383  return CPROVER_EXIT_SUCCESS;
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 
403  custom_bitvector_analysist custom_bitvector_analysis;
404  custom_bitvector_analysis(goto_model);
405  custom_bitvector_analysis.output(goto_model, std::cout);
406 
407  return CPROVER_EXIT_SUCCESS;
408  }
409 
410  if(cmdline.isset("show-escape-analysis"))
411  {
415 
416  // recalculate numbers, etc.
418 
419  escape_analysist escape_analysis;
420  escape_analysis(goto_model);
421  escape_analysis.output(goto_model, std::cout);
422 
423  return CPROVER_EXIT_SUCCESS;
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 
445  custom_bitvector_analysist custom_bitvector_analysis;
446  custom_bitvector_analysis(goto_model);
447  custom_bitvector_analysis.check(
448  goto_model,
449  cmdline.isset("xml-ui"),
450  std::cout);
451 
452  return CPROVER_EXIT_SUCCESS;
453  }
454 
455  if(cmdline.isset("show-points-to"))
456  {
458 
459  // recalculate numbers, etc.
461 
463 
464  log.status() << "Pointer Analysis" << messaget::eom;
465  points_tot points_to;
466  points_to(goto_model);
467  points_to.output(std::cout);
468  return CPROVER_EXIT_SUCCESS;
469  }
470 
471  if(cmdline.isset("show-intervals"))
472  {
474 
475  // recalculate numbers, etc.
477 
478  log.status() << "Interval Analysis" << messaget::eom;
482  interval_analysis.output(goto_model, std::cout);
483  return CPROVER_EXIT_SUCCESS;
484  }
485 
486  if(cmdline.isset("show-call-sequences"))
487  {
490  return CPROVER_EXIT_SUCCESS;
491  }
492 
493  if(cmdline.isset("check-call-sequence"))
494  {
497  return CPROVER_EXIT_SUCCESS;
498  }
499 
500  if(cmdline.isset("list-calls-args"))
501  {
503 
505 
506  return CPROVER_EXIT_SUCCESS;
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;
522  value_set_analysist value_set_analysis(ns);
523  value_set_analysis(goto_model.goto_functions);
524 
525  const symbolt &symbol=ns.lookup(ID_main);
526  symbol_exprt main(symbol.name, symbol.type);
527 
528  std::cout <<
529  rw_set_functiont(value_set_analysis, goto_model, main);
530  return CPROVER_EXIT_SUCCESS;
531  }
532 
533  if(cmdline.isset("show-symbol-table"))
534  {
536  return CPROVER_EXIT_SUCCESS;
537  }
538 
539  if(cmdline.isset("show-reaching-definitions"))
540  {
542 
544  reaching_definitions_analysist rd_analysis(ns);
545  rd_analysis(goto_model);
546  rd_analysis.output(goto_model, std::cout);
547 
548  return CPROVER_EXIT_SUCCESS;
549  }
550 
551  if(cmdline.isset("show-dependence-graph"))
552  {
554 
556  dependence_grapht dependence_graph(ns);
557  dependence_graph(goto_model);
558  dependence_graph.output(goto_model, std::cout);
559  dependence_graph.output_dot(std::cout);
560 
561  return CPROVER_EXIT_SUCCESS;
562  }
563 
564  if(cmdline.isset("count-eloc"))
565  {
567  return CPROVER_EXIT_SUCCESS;
568  }
569 
570  if(cmdline.isset("list-eloc"))
571  {
573  return CPROVER_EXIT_SUCCESS;
574  }
575 
576  if(cmdline.isset("print-path-lengths"))
577  {
579  return CPROVER_EXIT_SUCCESS;
580  }
581 
582  if(cmdline.isset("print-global-state-size"))
583  {
585  return CPROVER_EXIT_SUCCESS;
586  }
587 
588  if(cmdline.isset("list-symbols"))
589  {
591  return CPROVER_EXIT_SUCCESS;
592  }
593 
594  if(cmdline.isset("show-uninitialized"))
595  {
596  show_uninitialized(goto_model, std::cout);
597  return CPROVER_EXIT_SUCCESS;
598  }
599 
600  if(cmdline.isset("interpreter"))
601  {
602  log.status() << "Starting interpreter" << messaget::eom;
604  return CPROVER_EXIT_SUCCESS;
605  }
606 
607  if(cmdline.isset("show-claims") ||
608  cmdline.isset("show-properties"))
609  {
612  return CPROVER_EXIT_SUCCESS;
613  }
614 
615  if(cmdline.isset("document-claims-html") ||
616  cmdline.isset("document-properties-html"))
617  {
619  return CPROVER_EXIT_SUCCESS;
620  }
621 
622  if(cmdline.isset("document-claims-latex") ||
623  cmdline.isset("document-properties-latex"))
624  {
626  return CPROVER_EXIT_SUCCESS;
627  }
628 
629  if(cmdline.isset("show-loops"))
630  {
632  return CPROVER_EXIT_SUCCESS;
633  }
634 
635  if(cmdline.isset("show-natural-loops"))
636  {
637  show_natural_loops(goto_model, std::cout);
638  return CPROVER_EXIT_SUCCESS;
639  }
640 
641  if(cmdline.isset("show-lexical-loops"))
642  {
643  show_lexical_loops(goto_model, std::cout);
644  }
645 
646  if(cmdline.isset("print-internal-representation"))
647  {
648  for(auto const &pair : goto_model.goto_functions.function_map)
649  for(auto const &ins : pair.second.body.instructions)
650  {
651  if(ins.code.is_not_nil())
652  log.status() << ins.code.pretty() << messaget::eom;
653  if(ins.has_condition())
654  {
655  log.status() << "[guard] " << ins.get_condition().pretty()
656  << messaget::eom;
657  }
658  }
659  return CPROVER_EXIT_SUCCESS;
660  }
661 
662  if(
663  cmdline.isset("show-goto-functions") ||
664  cmdline.isset("list-goto-functions"))
665  {
667  goto_model, ui_message_handler, cmdline.isset("list-goto-functions"));
668  return CPROVER_EXIT_SUCCESS;
669  }
670 
671  if(cmdline.isset("list-undefined-functions"))
672  {
674  return CPROVER_EXIT_SUCCESS;
675  }
676 
677  // experimental: print structs
678  if(cmdline.isset("show-struct-alignment"))
679  {
681  return CPROVER_EXIT_SUCCESS;
682  }
683 
684  if(cmdline.isset("show-locations"))
685  {
687  return CPROVER_EXIT_SUCCESS;
688  }
689 
690  if(
691  cmdline.isset("dump-c") || cmdline.isset("dump-cpp") ||
692  cmdline.isset("dump-c-type-header"))
693  {
694  const bool is_cpp=cmdline.isset("dump-cpp");
695  const bool is_header = cmdline.isset("dump-c-type-header");
696  const bool h_libc=!cmdline.isset("no-system-headers");
697  const bool h_all=cmdline.isset("use-all-headers");
698  const bool harness=cmdline.isset("harness");
700 
701  // restore RETURN instructions in case remove_returns had been
702  // applied
704 
705  // dump_c (actually goto_program2code) requires valid instruction
706  // location numbers:
708 
709  if(cmdline.args.size()==2)
710  {
711  #ifdef _MSC_VER
712  std::ofstream out(widen(cmdline.args[1]));
713  #else
714  std::ofstream out(cmdline.args[1]);
715  #endif
716  if(!out)
717  {
718  log.error() << "failed to write to '" << cmdline.args[1] << "'";
720  }
721  if(is_header)
722  {
725  h_libc,
726  h_all,
727  harness,
728  ns,
729  cmdline.get_value("dump-c-type-header"),
730  out);
731  }
732  else
733  {
734  (is_cpp ? dump_cpp : dump_c)(
735  goto_model.goto_functions, h_libc, h_all, harness, ns, out);
736  }
737  }
738  else
739  {
740  if(is_header)
741  {
744  h_libc,
745  h_all,
746  harness,
747  ns,
748  cmdline.get_value("dump-c-type-header"),
749  std::cout);
750  }
751  else
752  {
753  (is_cpp ? dump_cpp : dump_c)(
754  goto_model.goto_functions, h_libc, h_all, harness, ns, std::cout);
755  }
756  }
757 
758  return CPROVER_EXIT_SUCCESS;
759  }
760 
761  if(cmdline.isset("call-graph"))
762  {
764  call_grapht call_graph(goto_model);
765 
766  if(cmdline.isset("xml"))
767  call_graph.output_xml(std::cout);
768  else if(cmdline.isset("dot"))
769  call_graph.output_dot(std::cout);
770  else
771  call_graph.output(std::cout);
772 
773  return CPROVER_EXIT_SUCCESS;
774  }
775 
776  if(cmdline.isset("reachable-call-graph"))
777  {
779  call_grapht call_graph =
782  if(cmdline.isset("xml"))
783  call_graph.output_xml(std::cout);
784  else if(cmdline.isset("dot"))
785  call_graph.output_dot(std::cout);
786  else
787  call_graph.output(std::cout);
788 
789  return 0;
790  }
791 
792  if(cmdline.isset("show-class-hierarchy"))
793  {
794  class_hierarchyt hierarchy;
795  hierarchy(goto_model.symbol_table);
796  if(cmdline.isset("dot"))
797  hierarchy.output_dot(std::cout);
798  else
800 
801  return CPROVER_EXIT_SUCCESS;
802  }
803 
804  if(cmdline.isset("dot"))
805  {
807 
808  if(cmdline.args.size()==2)
809  {
810  #ifdef _MSC_VER
811  std::ofstream out(widen(cmdline.args[1]));
812  #else
813  std::ofstream out(cmdline.args[1]);
814  #endif
815  if(!out)
816  {
817  log.error() << "failed to write to " << cmdline.args[1] << "'";
819  }
820 
821  dot(goto_model, out);
822  }
823  else
824  dot(goto_model, std::cout);
825 
826  return CPROVER_EXIT_SUCCESS;
827  }
828 
829  if(cmdline.isset("accelerate"))
830  {
832 
834 
835  log.status() << "Performing full inlining" << messaget::eom;
837 
838  log.status() << "Removing calls to functions without a body"
839  << messaget::eom;
840  remove_calls_no_bodyt remove_calls_no_body;
841  remove_calls_no_body(goto_model.goto_functions);
842 
843  log.status() << "Accelerating" << messaget::eom;
844  guard_managert guard_manager;
846  goto_model, ui_message_handler, cmdline.isset("z3"), guard_manager);
848  }
849 
850  if(cmdline.isset("horn-encoding"))
851  {
852  log.status() << "Horn-clause encoding" << messaget::eom;
854 
855  if(cmdline.args.size()==2)
856  {
857  #ifdef _MSC_VER
858  std::ofstream out(widen(cmdline.args[1]));
859  #else
860  std::ofstream out(cmdline.args[1]);
861  #endif
862 
863  if(!out)
864  {
865  log.error() << "Failed to open output file " << cmdline.args[1]
866  << messaget::eom;
868  }
869 
871  }
872  else
873  horn_encoding(goto_model, std::cout);
874 
875  return CPROVER_EXIT_SUCCESS;
876  }
877 
878  if(cmdline.isset("drop-unused-functions"))
879  {
881 
882  log.status() << "Removing unused functions" << messaget::eom;
884  }
885 
886  if(cmdline.isset("undefined-function-is-assume-false"))
887  {
890  }
891 
892  // write new binary?
893  if(cmdline.args.size()==2)
894  {
895  log.status() << "Writing GOTO program to '" << cmdline.args[1] << "'"
896  << messaget::eom;
897 
900  else
901  return CPROVER_EXIT_SUCCESS;
902  }
903  else if(cmdline.args.size() < 2)
904  {
906  "Invalid number of positional arguments passed",
907  "[in] [out]",
908  "goto-instrument needs one input and one output file, aside from other "
909  "flags");
910  }
911 
912  help();
914  }
915 // NOLINTNEXTLINE(readability/fn_size)
916 }
917 
919  bool force)
920 {
921  if(function_pointer_removal_done && !force)
922  return;
923 
925 
926  log.status() << "Function Pointer Removal" << messaget::eom;
928  ui_message_handler, goto_model, cmdline.isset("pointer-check"));
929  log.status() << "Virtual function removal" << messaget::eom;
931  log.status() << "Cleaning inline assembler statements" << messaget::eom;
933 }
934 
939 {
940  // Don't bother if we've already done a full function pointer
941  // removal.
943  {
944  return;
945  }
946 
947  log.status() << "Removing const function pointers only" << messaget::eom;
950  goto_model,
951  cmdline.isset("pointer-check"),
952  true); // abort if we can't resolve via const pointers
953 }
954 
956 {
958  return;
959 
961 
962  if(!cmdline.isset("inline"))
963  {
964  log.status() << "Partial Inlining" << messaget::eom;
966  }
967 }
968 
970 {
972  return;
973 
974  remove_returns_done=true;
975 
976  log.status() << "Removing returns" << messaget::eom;
978 }
979 
981 {
982  log.status() << "Reading GOTO program from '" << cmdline.args[0] << "'"
983  << messaget::eom;
984 
985  config.set(cmdline);
986 
987  auto result = read_goto_binary(cmdline.args[0], ui_message_handler);
988 
989  if(!result.has_value())
990  throw 0;
991 
992  goto_model = std::move(result.value());
993 
995 }
996 
998 {
999  optionst options;
1000 
1002 
1003  // disable simplify when adding various checks?
1004  if(cmdline.isset("no-simplify"))
1005  options.set_option("simplify", false);
1006  else
1007  options.set_option("simplify", true);
1008 
1009  // use assumptions instead of assertions?
1010  if(cmdline.isset("assert-to-assume"))
1011  options.set_option("assert-to-assume", true);
1012  else
1013  options.set_option("assert-to-assume", false);
1014 
1015  // all checks supported by goto_check
1017 
1018  // check assertions
1019  if(cmdline.isset("no-assertions"))
1020  options.set_option("assertions", false);
1021  else
1022  options.set_option("assertions", true);
1023 
1024  // use assumptions
1025  if(cmdline.isset("no-assumptions"))
1026  options.set_option("assumptions", false);
1027  else
1028  options.set_option("assumptions", true);
1029 
1030  // magic error label
1031  if(cmdline.isset("error-label"))
1032  options.set_option("error-label", cmdline.get_value("error-label"));
1033 
1034  // unwind loops
1035  if(cmdline.isset("unwind"))
1036  {
1037  log.status() << "Unwinding loops" << messaget::eom;
1038  options.set_option("unwind", cmdline.get_value("unwind"));
1039  }
1040 
1041  {
1043 
1044  if(
1048  {
1050 
1051  const auto function_pointer_restrictions =
1053  options, goto_model, log.get_message_handler());
1054 
1055  restrict_function_pointers(goto_model, function_pointer_restrictions);
1056  }
1057  }
1058 
1059  // skip over selected loops
1060  if(cmdline.isset("skip-loops"))
1061  {
1062  log.status() << "Adding gotos to skip loops" << messaget::eom;
1063  if(skip_loops(
1065  throw 0;
1066  }
1067 
1069 
1070  // initialize argv with valid pointers
1071  if(cmdline.isset("model-argc-argv"))
1072  {
1073  unsigned max_argc=
1074  safe_string2unsigned(cmdline.get_value("model-argc-argv"));
1075 
1076  log.status() << "Adding up to " << max_argc << " command line arguments"
1077  << messaget::eom;
1079  throw 0;
1080  }
1081 
1082  if(cmdline.isset("remove-function-body"))
1083  {
1085  goto_model,
1086  cmdline.get_values("remove-function-body"),
1088  }
1089 
1090  // we add the library in some cases, as some analyses benefit
1091 
1092  if(cmdline.isset("add-library") ||
1093  cmdline.isset("mm"))
1094  {
1095  if(cmdline.isset("show-custom-bitvector-analysis") ||
1096  cmdline.isset("custom-bitvector-analysis"))
1097  {
1098  config.ansi_c.defines.push_back(
1099  std::string(CPROVER_PREFIX) + "CUSTOM_BITVECTOR_ANALYSIS");
1100  }
1101 
1102  // add the library
1103  log.status() << "Adding CPROVER library (" << config.ansi_c.arch << ")"
1104  << messaget::eom;
1108  }
1109 
1110  // now do full inlining, if requested
1111  if(cmdline.isset("inline"))
1112  {
1114 
1115  if(cmdline.isset("show-custom-bitvector-analysis") ||
1116  cmdline.isset("custom-bitvector-analysis"))
1117  {
1121  }
1122 
1123  log.status() << "Performing full inlining" << messaget::eom;
1125  }
1126 
1127  if(cmdline.isset("show-custom-bitvector-analysis") ||
1128  cmdline.isset("custom-bitvector-analysis"))
1129  {
1130  log.status() << "Propagating Constants" << messaget::eom;
1131  constant_propagator_ait constant_propagator_ai(goto_model);
1133  }
1134 
1135  if(cmdline.isset("escape-analysis"))
1136  {
1140 
1141  // recalculate numbers, etc.
1143 
1144  log.status() << "Escape Analysis" << messaget::eom;
1145  escape_analysist escape_analysis;
1146  escape_analysis(goto_model);
1147  escape_analysis.instrument(goto_model);
1148 
1149  // inline added functions, they are often small
1151 
1152  // recalculate numbers, etc.
1154  }
1155 
1156  const std::list<std::pair<std::string, std::string>> contract_flags(
1159  for(const auto &pair : contract_flags)
1160  {
1161  if(cmdline.isset(pair.first.c_str()) && cmdline.isset(pair.second.c_str()))
1162  {
1163  log.error() << "Pass at most one of --" << pair.first << " and --"
1164  << pair.second << "." << messaget::eom;
1166  }
1167  }
1168 
1169  if(
1173  {
1175 
1177  {
1178  std::set<std::string> to_replace(
1181  if(cont.replace_calls(to_replace))
1183  }
1184 
1186  if(cont.replace_calls())
1188 
1190  {
1191  std::set<std::string> to_enforce(
1194  if(cont.enforce_contracts(to_enforce))
1196  }
1197 
1199  if(cont.enforce_contracts())
1201  }
1202 
1203  if(cmdline.isset("value-set-fi-fp-removal"))
1204  {
1207  }
1208 
1209  // replace function pointers, if explicitly requested
1210  if(cmdline.isset("remove-function-pointers"))
1211  {
1213  }
1214  else if(cmdline.isset("remove-const-function-pointers"))
1215  {
1217  }
1218 
1219  if(cmdline.isset("replace-calls"))
1220  {
1222 
1223  replace_callst replace_calls;
1224  replace_calls(goto_model, cmdline.get_values("replace-calls"));
1225  }
1226 
1227  if(cmdline.isset("function-inline"))
1228  {
1229  std::string function=cmdline.get_value("function-inline");
1230  PRECONDITION(!function.empty());
1231 
1232  bool caching=!cmdline.isset("no-caching");
1233 
1235 
1236  log.status() << "Inlining calls of function '" << function << "'"
1237  << messaget::eom;
1238 
1239  if(!cmdline.isset("log"))
1240  {
1242  goto_model, function, ui_message_handler, true, caching);
1243  }
1244  else
1245  {
1246  std::string filename=cmdline.get_value("log");
1247  bool have_file=!filename.empty() && filename!="-";
1248 
1250  goto_model, function, ui_message_handler, true, caching);
1251 
1252  if(have_file)
1253  {
1254 #ifdef _MSC_VER
1255  std::ofstream of(widen(filename));
1256 #else
1257  std::ofstream of(filename);
1258 #endif
1259  if(!of)
1260  throw "failed to open file "+filename;
1261 
1262  of << result;
1263  of.close();
1264  }
1265  else
1266  {
1267  std::cout << result << '\n';
1268  }
1269  }
1270 
1273  }
1274 
1275  if(cmdline.isset("partial-inline"))
1276  {
1278 
1279  log.status() << "Partial inlining" << messaget::eom;
1281 
1284  }
1285 
1286  if(cmdline.isset("remove-calls-no-body"))
1287  {
1288  log.status() << "Removing calls to functions without a body"
1289  << messaget::eom;
1290 
1291  remove_calls_no_bodyt remove_calls_no_body;
1292  remove_calls_no_body(goto_model.goto_functions);
1293 
1296  }
1297 
1298  if(cmdline.isset("constant-propagator"))
1299  {
1301 
1302  log.status() << "Propagating Constants" << messaget::eom;
1303 
1304  constant_propagator_ait constant_propagator_ai(goto_model);
1306  }
1307 
1308  if(cmdline.isset("generate-function-body"))
1309  {
1310  optionst c_object_factory_options;
1311  parse_c_object_factory_options(cmdline, c_object_factory_options);
1312  c_object_factory_parameterst object_factory_parameters(
1313  c_object_factory_options);
1314 
1315  auto generate_implementation = generate_function_bodies_factory(
1316  cmdline.get_value("generate-function-body-options"),
1317  object_factory_parameters,
1321  std::regex(cmdline.get_value("generate-function-body")),
1322  *generate_implementation,
1323  goto_model,
1325  }
1326 
1327  if(cmdline.isset("generate-havocing-body"))
1328  {
1329  optionst c_object_factory_options;
1330  parse_c_object_factory_options(cmdline, c_object_factory_options);
1331  c_object_factory_parameterst object_factory_parameters(
1332  c_object_factory_options);
1333 
1334  auto options_split =
1335  split_string(cmdline.get_value("generate-havocing-body"), ',');
1336  if(options_split.size() < 2)
1338  "not enough arguments for this option", "--generate-havocing-body"};
1339 
1340  if(options_split.size() == 2)
1341  {
1342  auto generate_implementation = generate_function_bodies_factory(
1343  std::string{"havoc,"} + options_split.back(),
1344  object_factory_parameters,
1348  std::regex(options_split[0]),
1349  *generate_implementation,
1350  goto_model,
1352  }
1353  else
1354  {
1355  CHECK_RETURN(options_split.size() % 2 == 1);
1356  for(size_t i = 1; i + 1 < options_split.size(); i += 2)
1357  {
1358  auto generate_implementation = generate_function_bodies_factory(
1359  std::string{"havoc,"} + options_split[i + 1],
1360  object_factory_parameters,
1364  options_split[0],
1365  options_split[i],
1366  *generate_implementation,
1367  goto_model,
1369  }
1370  }
1371  }
1372 
1373  // add generic checks, if needed
1374  goto_check(options, goto_model);
1375 
1376  // check for uninitalized local variables
1377  if(cmdline.isset("uninitialized-check"))
1378  {
1379  log.status() << "Adding checks for uninitialized local variables"
1380  << messaget::eom;
1382  }
1383 
1384  // check for maximum call stack size
1385  if(cmdline.isset("stack-depth"))
1386  {
1387  log.status() << "Adding check for maximum call stack size" << messaget::eom;
1388  stack_depth(
1389  goto_model,
1390  safe_string2size_t(cmdline.get_value("stack-depth")));
1391  }
1392 
1393  // ignore default/user-specified initialization of variables with static
1394  // lifetime
1395  if(cmdline.isset("nondet-static-exclude"))
1396  {
1397  log.status() << "Adding nondeterministic initialization "
1398  "of static/global variables except for "
1399  "the specified ones."
1400  << messaget::eom;
1401 
1402  nondet_static(goto_model, cmdline.get_values("nondet-static-exclude"));
1403  }
1404  else if(cmdline.isset("nondet-static"))
1405  {
1406  log.status() << "Adding nondeterministic initialization "
1407  "of static/global variables"
1408  << messaget::eom;
1410  }
1411 
1412  if(cmdline.isset("slice-global-inits"))
1413  {
1414  log.status() << "Slicing away initializations of unused global variables"
1415  << messaget::eom;
1417  }
1418 
1419  if(cmdline.isset("string-abstraction"))
1420  {
1423 
1424  log.status() << "String Abstraction" << messaget::eom;
1426  }
1427 
1428  // some analyses require function pointer removal and partial inlining
1429 
1430  if(cmdline.isset("remove-pointers") ||
1431  cmdline.isset("race-check") ||
1432  cmdline.isset("mm") ||
1433  cmdline.isset("isr") ||
1434  cmdline.isset("concurrency"))
1435  {
1437 
1438  log.status() << "Pointer Analysis" << messaget::eom;
1439  value_set_analysist value_set_analysis(ns);
1440  value_set_analysis(goto_model.goto_functions);
1441 
1442  if(cmdline.isset("remove-pointers"))
1443  {
1444  // removing pointers
1445  log.status() << "Removing Pointers" << messaget::eom;
1446  remove_pointers(goto_model, value_set_analysis);
1447  }
1448 
1449  if(cmdline.isset("race-check"))
1450  {
1451  log.status() << "Adding Race Checks" << messaget::eom;
1452  race_check(value_set_analysis, goto_model);
1453  }
1454 
1455  if(cmdline.isset("mm"))
1456  {
1457  std::string mm=cmdline.get_value("mm");
1458  memory_modelt model;
1459 
1460  // strategy of instrumentation
1461  instrumentation_strategyt inst_strategy;
1462  if(cmdline.isset("one-event-per-cycle"))
1463  inst_strategy=one_event_per_cycle;
1464  else if(cmdline.isset("minimum-interference"))
1465  inst_strategy=min_interference;
1466  else if(cmdline.isset("read-first"))
1467  inst_strategy=read_first;
1468  else if(cmdline.isset("write-first"))
1469  inst_strategy=write_first;
1470  else if(cmdline.isset("my-events"))
1471  inst_strategy=my_events;
1472  else
1473  /* default: instruments all unsafe pairs */
1474  inst_strategy=all;
1475 
1476  const unsigned max_var=
1477  cmdline.isset("max-var")?
1479  const unsigned max_po_trans=
1480  cmdline.isset("max-po-trans")?
1481  unsafe_string2unsigned(cmdline.get_value("max-po-trans")):0;
1482 
1483  if(mm=="tso")
1484  {
1485  log.status() << "Adding weak memory (TSO) Instrumentation"
1486  << messaget::eom;
1487  model=TSO;
1488  }
1489  else if(mm=="pso")
1490  {
1491  log.status() << "Adding weak memory (PSO) Instrumentation"
1492  << messaget::eom;
1493  model=PSO;
1494  }
1495  else if(mm=="rmo")
1496  {
1497  log.status() << "Adding weak memory (RMO) Instrumentation"
1498  << messaget::eom;
1499  model=RMO;
1500  }
1501  else if(mm=="power")
1502  {
1503  log.status() << "Adding weak memory (Power) Instrumentation"
1504  << messaget::eom;
1505  model=Power;
1506  }
1507  else
1508  {
1509  log.error() << "Unknown weak memory model '" << mm << "'"
1510  << messaget::eom;
1511  model=Unknown;
1512  }
1513 
1515 
1516  if(cmdline.isset("force-loop-duplication"))
1517  loops=all_loops;
1518  if(cmdline.isset("no-loop-duplication"))
1519  loops=no_loop;
1520 
1521  if(model!=Unknown)
1522  weak_memory(
1523  model,
1524  value_set_analysis,
1525  goto_model,
1526  cmdline.isset("scc"),
1527  inst_strategy,
1528  !cmdline.isset("cfg-kill"),
1529  cmdline.isset("no-dependencies"),
1530  loops,
1531  max_var,
1532  max_po_trans,
1533  !cmdline.isset("no-po-rendering"),
1534  cmdline.isset("render-cluster-file"),
1535  cmdline.isset("render-cluster-function"),
1536  cmdline.isset("cav11"),
1537  cmdline.isset("hide-internals"),
1539  cmdline.isset("ignore-arrays"));
1540  }
1541 
1542  // Interrupt handler
1543  if(cmdline.isset("isr"))
1544  {
1545  log.status() << "Instrumenting interrupt handler" << messaget::eom;
1546  interrupt(
1547  value_set_analysis,
1548  goto_model,
1549  cmdline.get_value("isr"));
1550  }
1551 
1552  // Memory-mapped I/O
1553  if(cmdline.isset("mmio"))
1554  {
1555  log.status() << "Instrumenting memory-mapped I/O" << messaget::eom;
1556  mmio(value_set_analysis, goto_model);
1557  }
1558 
1559  if(cmdline.isset("concurrency"))
1560  {
1561  log.status() << "Sequentializing concurrency" << messaget::eom;
1562  concurrency(value_set_analysis, goto_model);
1563  }
1564  }
1565 
1566  if(cmdline.isset("interval-analysis"))
1567  {
1568  log.status() << "Interval analysis" << messaget::eom;
1570  }
1571 
1572  if(cmdline.isset("havoc-loops"))
1573  {
1574  log.status() << "Havocking loops" << messaget::eom;
1576  }
1577 
1578  if(cmdline.isset("k-induction"))
1579  {
1580  bool base_case=cmdline.isset("base-case");
1581  bool step_case=cmdline.isset("step-case");
1582 
1583  if(step_case && base_case)
1584  throw "please specify only one of --step-case and --base-case";
1585  else if(!step_case && !base_case)
1586  throw "please specify one of --step-case and --base-case";
1587 
1588  unsigned k=unsafe_string2unsigned(cmdline.get_value("k-induction"));
1589 
1590  if(k==0)
1591  throw "please give k>=1";
1592 
1593  log.status() << "Instrumenting k-induction for k=" << k << ", "
1594  << (base_case ? "base case" : "step case") << messaget::eom;
1595 
1596  k_induction(goto_model, base_case, step_case, k);
1597  }
1598 
1599  if(cmdline.isset("function-enter"))
1600  {
1601  log.status() << "Function enter instrumentation" << messaget::eom;
1603  goto_model,
1604  cmdline.get_value("function-enter"));
1605  }
1606 
1607  if(cmdline.isset("function-exit"))
1608  {
1609  log.status() << "Function exit instrumentation" << messaget::eom;
1610  function_exit(
1611  goto_model,
1612  cmdline.get_value("function-exit"));
1613  }
1614 
1615  if(cmdline.isset("branch"))
1616  {
1617  log.status() << "Branch instrumentation" << messaget::eom;
1618  branch(
1619  goto_model,
1620  cmdline.get_value("branch"));
1621  }
1622 
1623  // add failed symbols
1625 
1626  // recalculate numbers, etc.
1628 
1629  // add loop ids
1631 
1632  // label the assertions
1634 
1635  nondet_volatile(goto_model, options);
1636 
1637  // reachability slice?
1638  if(cmdline.isset("reachability-slice"))
1639  {
1641 
1642  log.status() << "Performing a reachability slice" << messaget::eom;
1643 
1644  // reachability_slicer requires that the model has unique location numbers:
1646 
1647  if(cmdline.isset("property"))
1649  else
1651  }
1652 
1653  if(cmdline.isset("fp-reachability-slice"))
1654  {
1656 
1657  log.status() << "Performing a function pointer reachability slice"
1658  << messaget::eom;
1660  goto_model, cmdline.get_comma_separated_values("fp-reachability-slice"));
1661  }
1662 
1663  // full slice?
1664  if(cmdline.isset("full-slice"))
1665  {
1668 
1669  log.status() << "Performing a full slice" << messaget::eom;
1670  if(cmdline.isset("property"))
1672  else
1673  {
1674  // full_slicer requires that the model has unique location numbers:
1677  }
1678  }
1679 
1680  // splice option
1681  if(cmdline.isset("splice-call"))
1682  {
1683  log.status() << "Performing call splicing" << messaget::eom;
1684  std::string callercallee=cmdline.get_value("splice-call");
1685  if(splice_call(
1687  callercallee,
1690  throw 0;
1691  }
1692 
1693  // aggressive slicer
1694  if(cmdline.isset("aggressive-slice"))
1695  {
1697 
1698  // reachability_slicer requires that the model has unique location numbers:
1700 
1701  log.status() << "Slicing away initializations of unused global variables"
1702  << messaget::eom;
1704 
1705  log.status() << "Performing an aggressive slice" << messaget::eom;
1706  aggressive_slicert aggressive_slicer(goto_model, ui_message_handler);
1707 
1708  if(cmdline.isset("aggressive-slice-call-depth"))
1709  aggressive_slicer.call_depth =
1710  safe_string2unsigned(cmdline.get_value("aggressive-slice-call-depth"));
1711 
1712  if(cmdline.isset("aggressive-slice-preserve-function"))
1713  aggressive_slicer.preserve_functions(
1714  cmdline.get_values("aggressive-slice-preserve-function"));
1715 
1716  if(cmdline.isset("property"))
1717  aggressive_slicer.user_specified_properties =
1718  cmdline.get_values("property");
1719 
1720  if(cmdline.isset("aggressive-slice-preserve-functions-containing"))
1721  aggressive_slicer.name_snippets =
1722  cmdline.get_values("aggressive-slice-preserve-functions-containing");
1723 
1724  aggressive_slicer.preserve_all_direct_paths =
1725  cmdline.isset("aggressive-slice-preserve-all-direct-paths");
1726 
1727  aggressive_slicer.doit();
1728 
1730 
1731  log.status() << "Performing a reachability slice" << messaget::eom;
1732  if(cmdline.isset("property"))
1734  else
1736  }
1737 
1738  if(cmdline.isset("ensure-one-backedge-per-target"))
1739  {
1740  log.status() << "Trying to force one backedge per target" << messaget::eom;
1742  }
1743 
1744  // recalculate numbers, etc.
1746 }
1747 
1750 {
1751  // clang-format off
1752  std::cout << '\n' << banner_string("Goto-Instrument", CBMC_VERSION) << '\n'
1753  << align_center_with_border("Copyright (C) 2008-2013") << '\n'
1754  << align_center_with_border("Daniel Kroening") << '\n'
1755  << align_center_with_border("kroening@kroening.com") << '\n'
1756  <<
1757  "\n"
1758  "Usage: Purpose:\n"
1759  "\n"
1760  " goto-instrument [-?] [-h] [--help] show help\n"
1761  " goto-instrument in out perform instrumentation\n"
1762  "\n"
1763  "Main options:\n"
1764  " --document-properties-html generate HTML property documentation\n"
1765  " --document-properties-latex generate Latex property documentation\n"
1766  " --dump-c generate C source\n"
1767  " --dump-c-type-header m generate a C header for types local in m\n"
1768  " --dump-cpp generate C++ source\n"
1769  " --dot generate CFG graph in DOT format\n"
1770  " --interpreter do concrete execution\n"
1771  "\n"
1772  "Diagnosis:\n"
1773  " --show-loops show the loops in the program\n"
1775  " --show-symbol-table show loaded symbol table\n"
1776  " --list-symbols list symbols with type information\n"
1779  " --drop-unused-functions drop functions trivially unreachable from main function\n" // NOLINT(*)
1780  " --print-internal-representation\n" // NOLINTNEXTLINE(*)
1781  " show verbose internal representation of the program\n"
1782  " --list-undefined-functions list functions without body\n"
1783  " --show-struct-alignment show struct members that might be concurrently accessed\n" // NOLINT(*)
1784  " --show-natural-loops show natural loop heads\n"
1785  // NOLINTNEXTLINE(whitespace/line_length)
1786  " --list-calls-args list all function calls with their arguments\n"
1787  " --call-graph show graph of function calls\n"
1788  // NOLINTNEXTLINE(whitespace/line_length)
1789  " --reachable-call-graph show graph of function calls potentially reachable from main function\n"
1791  // NOLINTNEXTLINE(whitespace/line_length)
1792  " --show-threaded show instructions that may be executed by more than one thread\n"
1793  " --show-local-safe-pointers show pointer expressions that are trivially dominated by a not-null check\n" // NOLINT(*)
1794  " --show-safe-dereferences show pointer expressions that are trivially dominated by a not-null check\n" // NOLINT(*)
1795  " *and* used as a dereference operand\n" // NOLINT(*)
1797  // NOLINTNEXTLINE(whitespace/line_length)
1798  " --validate-goto-binary check the well-formedness of the passed in goto\n"
1799  " binary and then exit\n"
1800  "\n"
1801  "Safety checks:\n"
1802  " --no-assertions ignore user assertions\n"
1804  " --uninitialized-check add checks for uninitialized locals (experimental)\n" // NOLINT(*)
1805  " --error-label label check that label is unreachable\n"
1806  " --stack-depth n add check that call stack size of non-inlined functions never exceeds n\n" // NOLINT(*)
1807  " --race-check add floating-point data race checks\n"
1808  "\n"
1809  "Semantic transformations:\n"
1810  << HELP_NONDET_VOLATILE <<
1811  " --unwind <n> unwinds the loops <n> times\n"
1812  " --unwindset L:B,... unwind loop L with a bound of B\n"
1813  " --unwindset-file <file> read unwindset from file\n"
1814  " --partial-loops permit paths with partial loops\n"
1815  " --unwinding-assertions generate unwinding assertions\n"
1816  " --continue-as-loops add loop for remaining iterations after unwound part\n" // NOLINT(*)
1817  " --isr <function> instruments an interrupt service routine\n"
1818  " --mmio instruments memory-mapped I/O\n"
1819  " --nondet-static add nondeterministic initialization of variables with static lifetime\n" // NOLINT(*)
1820  " --nondet-static-exclude e same as nondet-static except for the variable e\n" //NOLINT(*)
1821  " (use multiple times if required)\n"
1822  " --check-invariant function instruments invariant checking function\n"
1823  " --remove-pointers converts pointer arithmetic to base+offset expressions\n" // NOLINT(*)
1824  " --splice-call caller,callee prepends a call to callee in the body of caller\n" // NOLINT(*)
1825  " --undefined-function-is-assume-false\n"
1826  // NOLINTNEXTLINE(whitespace/line_length)
1827  " convert each call to an undefined function to assume(false)\n"
1831  "\n"
1832  "Loop transformations:\n"
1833  " --k-induction <k> check loops with k-induction\n"
1834  " --step-case k-induction: do step-case\n"
1835  " --base-case k-induction: do base-case\n"
1836  " --havoc-loops over-approximate all loops\n"
1837  " --accelerate add loop accelerators\n"
1838  " --skip-loops <loop-ids> add gotos to skip selected loops during execution\n" // NOLINT(*)
1839  "\n"
1840  "Memory model instrumentations:\n"
1841  " --mm <tso,pso,rmo,power> instruments a weak memory model\n"
1842  " --scc detects critical cycles per SCC (one thread per SCC)\n" // NOLINT(*)
1843  " --one-event-per-cycle only instruments one event per cycle\n"
1844  " --minimum-interference instruments an optimal number of events\n"
1845  " --my-events only instruments events whose ids appear in inst.evt\n" // NOLINT(*)
1846  " --cfg-kill enables symbolic execution used to reduce spurious cycles\n" // NOLINT(*)
1847  " --no-dependencies no dependency analysis\n"
1848  // NOLINTNEXTLINE(whitespace/line_length)
1849  " --no-po-rendering no representation of the threads in the dot\n"
1850  " --render-cluster-file clusterises the dot by files\n"
1851  " --render-cluster-function clusterises the dot by functions\n"
1852  "\n"
1853  "Slicing:\n"
1855  " --full-slice slice away instructions that don't affect assertions\n" // NOLINT(*)
1856  " --property id slice with respect to specific property only\n" // NOLINT(*)
1857  " --slice-global-inits slice away initializations of unused global variables\n" // NOLINT(*)
1858  " --aggressive-slice remove bodies of any functions not on the shortest path between\n" // NOLINT(*)
1859  " the start function and the function containing the property(s)\n" // NOLINT(*)
1860  " --aggressive-slice-call-depth <n>\n"
1861  " used with aggressive-slice, preserves all functions within <n> function calls\n" // NOLINT(*)
1862  " of the functions on the shortest path\n"
1863  " --aggressive-slice-preserve-function <f>\n"
1864  " force the aggressive slicer to preserve function <f>\n" // NOLINT(*)
1865  " --aggressive-slice-preserve-function containing <f>\n"
1866  " force the aggressive slicer to preserve all functions with names containing <f>\n" // NOLINT(*)
1867  "--aggressive-slice-preserve-all-direct-paths \n"
1868  " force aggressive slicer to preserve all direct paths\n" // NOLINT(*)
1869  "\n"
1870  "Further transformations:\n"
1871  " --constant-propagator propagate constants and simplify expressions\n" // NOLINT(*)
1872  " --inline perform full inlining\n"
1873  " --partial-inline perform partial inlining\n"
1874  " --function-inline <function> transitively inline all calls <function> makes\n" // NOLINT(*)
1875  " --no-caching disable caching of intermediate results during transitive function inlining\n" // NOLINT(*)
1876  " --log <file> log in json format which code segments were inlined, use with --function-inline\n" // NOLINT(*)
1877  " --remove-function-pointers replace function pointers by case statement over function calls\n" // NOLINT(*)
1878  " --value-set-fi-fp-removal build flow-insensitive value set and replace function pointers by a case statement\n" // NOLINT(*)
1879  " over the possible assignments. If the set of possible assignments is empty the function pointer\n" // NOLINT(*)
1880  " is removed using the standard remove-function-pointers pass. \n" // NOLINT(*)
1884  " --add-library add models of C library functions\n"
1885  " --model-argc-argv <n> model up to <n> command line arguments\n"
1886  // NOLINTNEXTLINE(whitespace/line_length)
1887  " --remove-function-body <f> remove the implementation of function <f> (may be repeated)\n"
1889  "\n"
1890  "Function contracts and invariants:\n"
1895  "\n"
1896  "Other options:\n"
1897  " --no-system-headers with --dump-c/--dump-cpp: generate C source expanding libc includes\n" // NOLINT(*)
1898  " --use-all-headers with --dump-c/--dump-cpp: generate C source with all includes\n" // NOLINT(*)
1899  " --harness with --dump-c/--dump-cpp: include input generator in output\n" // NOLINT(*)
1900  " --version show version and exit\n"
1901  HELP_FLUSH
1902  " --xml-ui use XML-formatted output\n"
1903  " --json-ui use JSON-formatted output\n"
1905  "\n";
1906  // clang-format on
1907 }
cprover_library.h
cmdlinet::args
argst args
Definition: cmdline.h:91
value_set_fi_fp_removal
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...
Definition: value_set_fi_fp_removal.cpp:188
Unknown
@ Unknown
Definition: wmm.h:19
exception_utils.h
HELP_REACHABILITY_SLICER
#define HELP_REACHABILITY_SLICER
Definition: reachability_slicer.h:43
configt::ansi_ct::defines
std::list< std::string > defines
Definition: config.h:122
HELP_SHOW_GOTO_FUNCTIONS
#define HELP_SHOW_GOTO_FUNCTIONS
Definition: show_goto_functions.h:26
no_loop
@ no_loop
Definition: wmm.h:40
TSO
@ TSO
Definition: wmm.h:20
string_abstraction.h
String Abstraction.
concurrency.h
Encoding for Threaded Goto Programs.
horn_encoding
void horn_encoding(const goto_modelt &, std::ostream &)
Definition: horn_encoding.cpp:18
havoc_loops.h
Havoc Loops.
PARSE_OPTIONS_GOTO_CHECK
#define PARSE_OPTIONS_GOTO_CHECK(cmdline, options)
Definition: goto_check.h:61
class_hierarchyt
Non-graph-based representation of the class hierarchy.
Definition: class_hierarchy.h:43
horn_encoding.h
Horn-clause Encoding.
parse_options_baset::ui_message_handler
ui_message_handlert ui_message_handler
Definition: parse_options.h:42
unwindsett::parse_unwindset_file
void parse_unwindset_file(const std::string &file_name)
Definition: unwindset.cpp:94
parse_c_object_factory_options
void parse_c_object_factory_options(const cmdlinet &cmdline, optionst &options)
Parse the c object factory parameters from a given command line.
Definition: c_object_factory_parameters.cpp:11
goto_unwindt::unwind_strategyt
unwind_strategyt
Definition: unwind.h:26
local_bitvector_analysis.h
Field-insensitive, location-sensitive bitvector analysis.
RESTRICT_FUNCTION_POINTER_BY_NAME_OPT
#define RESTRICT_FUNCTION_POINTER_BY_NAME_OPT
Definition: restrict_function_pointers.h:32
cmdlinet::isset
virtual bool isset(char option) const
Definition: cmdline.cpp:29
dependence_grapht
Definition: dependence_graph.h:217
print_global_state_size
void print_global_state_size(const goto_modelt &goto_model)
Definition: count_eloc.cpp:149
goto_instrument_parse_optionst::do_remove_returns
void do_remove_returns()
Definition: goto_instrument_parse_options.cpp:969
goto_instrument_parse_optionst::help
virtual void help()
display command line help
Definition: goto_instrument_parse_options.cpp:1749
stack_depth
void stack_depth(goto_programt &goto_program, const symbol_exprt &symbol, const std::size_t i_depth, const exprt &max_depth)
Definition: stack_depth.cpp:43
RMO
@ RMO
Definition: wmm.h:22
goto_instrument_parse_optionst::do_partial_inlining
void do_partial_inlining()
Definition: goto_instrument_parse_options.cpp:955
goto_inline.h
Function Inlining.
optionst
Definition: options.h:23
goto_instrument_parse_optionst::function_pointer_removal_done
bool function_pointer_removal_done
Definition: goto_instrument_parse_options.h:159
mutex_init_instrumentation
void mutex_init_instrumentation(const symbol_tablet &symbol_table, goto_programt &goto_program, typet lock_type)
Definition: thread_instrumentation.cpp:82
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
string_utils.h
skip_loops.h
Skip over selected loops by adding gotos.
show_class_hierarchy
void show_class_hierarchy(const class_hierarchyt &hierarchy, ui_message_handlert &message_handler, bool children_only)
Output the class hierarchy.
Definition: class_hierarchy.cpp:261
messaget::M_STATISTICS
@ M_STATISTICS
Definition: message.h:171
show_natural_loops
void show_natural_loops(const goto_modelt &goto_model, std::ostream &out)
Definition: natural_loops.h:92
sese_region_analysist::output
void output(std::ostream &out, const goto_programt &goto_program, const namespacet &ns) const
Definition: sese_regions.cpp:230
messaget::status
mstreamt & status() const
Definition: message.h:414
show_properties
void show_properties(const namespacet &ns, const irep_idt &identifier, message_handlert &message_handler, ui_message_handlert::uit ui, const goto_programt &goto_program)
Definition: show_properties.cpp:47
custom_bitvector_analysis.h
Field-insensitive, location-sensitive bitvector analysis.
goto_function_inline_and_log
jsont goto_function_inline_and_log(goto_modelt &goto_model, const irep_idt function, message_handlert &message_handler, bool adjust_function, bool caching)
Definition: goto_inline.cpp:284
goto_partial_inline
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...
Definition: goto_inline.cpp:108
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
concurrency
void concurrency(value_setst &value_sets, goto_modelt &goto_model)
Definition: concurrency.cpp:195
local_safe_pointerst::output_safe_dereferences
void output_safe_dereferences(std::ostream &stream, const goto_programt &program, const namespacet &ns)
Output safely dereferenced expressions per instruction in human-readable format.
Definition: local_safe_pointers.cpp:233
write_goto_binary
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.
Definition: write_goto_binary.cpp:25
dot
void dot(const goto_modelt &src, std::ostream &out)
Definition: dot.cpp:354
remove_skip
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:85
restrict_function_pointers
void restrict_function_pointers(goto_modelt &goto_model, const function_pointer_restrictionst &restrictions)
Apply function pointer restrictions to a goto_model.
Definition: restrict_function_pointers.cpp:215
local_safe_pointerst
A very simple, cheap analysis to determine when dereference operations are trivially guarded by a che...
Definition: local_safe_pointers.h:25
model_argc_argv
bool model_argc_argv(goto_modelt &goto_model, unsigned max_argc, message_handlert &message_handler)
Set up argv with up to max_argc pointers into an array of 4096 bytes.
Definition: model_argc_argv.cpp:39
parameter_assignments
void parameter_assignments(symbol_tablet &symbol_table, goto_functionst &goto_functions)
removes returns
Definition: parameter_assignments.cpp:94
unwindsett::parse_unwindset
void parse_unwindset(const std::string &unwindset)
Definition: unwindset.cpp:57
label_function_pointer_call_sites
void label_function_pointer_call_sites(goto_modelt &goto_model)
This ensures that call instructions can be only one of two things:
Definition: label_function_pointer_call_sites.cpp:13
splice_call
bool splice_call(goto_functionst &goto_functions, const std::string &callercallee, const symbol_tablet &symbol_table, message_handlert &message_handler)
Definition: splice_call.cpp:38
show_lexical_loops
void show_lexical_loops(const goto_modelt &goto_model, std::ostream &out)
Definition: lexical_loops.h:191
skip_loops
static bool skip_loops(goto_programt &goto_program, const loop_idst &loop_ids, messaget &message)
Definition: skip_loops.cpp:24
remove_virtual_functions.h
Functions for replacing virtual function call with a static function calls in functions,...
remove_asm.h
Remove 'asm' statements by compiling them into suitable standard goto program instructions.
HELP_SHOW_CLASS_HIERARCHY
#define HELP_SHOW_CLASS_HIERARCHY
Definition: class_hierarchy.h:29
constant_propagator.h
Constant propagation.
reachability_slicer
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.
Definition: reachability_slicer.cpp:368
PSO
@ PSO
Definition: wmm.h:21
value_set_analysis_templatet
This template class implements a data-flow analysis which keeps track of what values different variab...
Definition: value_set_analysis.h:40
remove_virtual_functions
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...
Definition: remove_virtual_functions.cpp:723
interpreter.h
Interpreter for GOTO Programs.
show_uninitialized
void show_uninitialized(const goto_modelt &goto_model, std::ostream &out)
Definition: uninitialized.cpp:209
race_check
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)
Definition: race_check.cpp:161
goto_unwindt::unwind_strategyt::CONTINUE
@ CONTINUE
add_uninitialized_locals_assertions
void add_uninitialized_locals_assertions(goto_modelt &goto_model)
Definition: uninitialized.cpp:199
ait
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition: ai.h:558
remove_calls_no_body.h
Remove calls to functions without a body.
goto_instrument_parse_optionst::do_remove_const_function_pointers_only
void do_remove_const_function_pointers_only()
Remove function pointers that can be resolved by analysing const variables (i.e.
Definition: goto_instrument_parse_options.cpp:938
Power
@ Power
Definition: wmm.h:23
mmio.h
Memory-mapped I/O Instrumentation for Goto Programs.
show_loop_ids
void show_loop_ids(ui_message_handlert::uit ui, const goto_modelt &goto_model)
Definition: loop_ids.cpp:19
generate_function_bodies
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-...
Definition: generate_function_bodies.cpp:511
goto_unwindt::unwind_strategyt::ASSERT
@ ASSERT
aggressive_slicert::preserve_all_direct_paths
bool preserve_all_direct_paths
Definition: aggressive_slicer.h:70
FLAG_REPLACE_ALL_CALLS
#define FLAG_REPLACE_ALL_CALLS
Definition: code_contracts.h:159
goto_check
void goto_check(const irep_idt &function_identifier, goto_functionst::goto_functiont &goto_function, const namespacet &ns, const optionst &options)
Definition: goto_check.cpp:2231
optionst::set_option
void set_option(const std::string &option, const bool value)
Definition: options.cpp:28
call_graph.h
Function Call Graphs.
FLAG_ENFORCE_ALL_CONTRACTS
#define FLAG_ENFORCE_ALL_CONTRACTS
Definition: code_contracts.h:168
weak_memory.h
Weak Memory Instrumentation for Threaded Goto Programs.
k_induction.h
k-induction
insert_final_assert_false.h
Insert final assert false into a function.
messaget::eom
static eomt eom
Definition: message.h:297
HELP_ENFORCE_CONTRACT
#define HELP_ENFORCE_CONTRACT
Definition: code_contracts.h:165
string_abstraction
void string_abstraction(symbol_tablet &symbol_table, message_handlert &message_handler, goto_programt &dest)
Definition: string_abstraction.cpp:65
show_symbol_table
void show_symbol_table(const symbol_tablet &symbol_table, ui_message_handlert &ui)
Definition: show_symbol_table.cpp:268
ensure_one_backedge_per_target
bool ensure_one_backedge_per_target(goto_programt::targett &it, goto_programt &goto_program)
Definition: ensure_one_backedge_per_target.cpp:21
configt::ansi_c
struct configt::ansi_ct ansi_c
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:27
version.h
remove_unused_functions
void remove_unused_functions(goto_modelt &goto_model, message_handlert &message_handler)
Definition: remove_unused_functions.cpp:18
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
call_grapht::output_xml
void output_xml(std::ostream &out) const
Definition: call_graph.cpp:281
race_check.h
Race Detection for Threaded Goto Programs.
nondet_static.h
Nondeterministically initializes global scope variables, except for constants (such as string literal...
jsont
Definition: json.h:27
document_properties.h
Documentation of Properties.
string_instrumentation.h
String Abstraction.
sese_regions.h
Single-entry, single-exit region analysis.
write_first
@ write_first
Definition: wmm.h:31
loop_strategyt
loop_strategyt
Definition: wmm.h:37
call_grapht::output_dot
void output_dot(std::ostream &out) const
Definition: call_graph.cpp:254
interpreter
void interpreter(const goto_modelt &goto_model, message_handlert &message_handler)
Definition: interpreter.cpp:1083
safe_string2size_t
std::size_t safe_string2size_t(const std::string &str, int base)
Definition: string2int.cpp:26
show_value_sets
void show_value_sets(ui_message_handlert::uit ui, const goto_modelt &goto_model, const value_set_analysist &value_set_analysis)
Definition: show_value_sets.cpp:22
function_pointer_restrictionst::from_options
static function_pointer_restrictionst from_options(const optionst &options, const goto_modelt &goto_model, message_handlert &message_handler)
Parse function pointer restrictions from command line.
Definition: restrict_function_pointers.cpp:437
label_properties
void label_properties(goto_modelt &goto_model)
Definition: set_properties.cpp:43
print_struct_alignment_problems
void print_struct_alignment_problems(const symbol_tablet &symbol_table, std::ostream &out)
Definition: alignment_checks.cpp:21
reaching_definitions_analysist
Definition: reaching_definitions.h:339
nondet_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.
Definition: nondet_static.cpp:79
write_goto_binary.h
Write GOTO binaries.
list_undefined_functions
void list_undefined_functions(const goto_modelt &goto_model, std::ostream &os)
Definition: undefined_functions.cpp:22
cmdlinet::get_comma_separated_values
std::list< std::string > get_comma_separated_values(const char *option) const
Definition: cmdline.cpp:120
call_grapht::create_from_root_function
static call_grapht create_from_root_function(const goto_modelt &model, const irep_idt &root, bool collect_callsites)
Definition: call_graph.h:48
thread_instrumentation.h
lexical_loops.h
Compute lexical loops in a goto_function.
splice_call.h
Harnessing for goto functions.
unwindsett::parse_unwind
void parse_unwind(const std::string &unwind)
Definition: unwindset.cpp:18
goto_unwindt::unwind_strategyt::PARTIAL
@ PARTIAL
validate_goto_model.h
is_threadedt
Definition: is_threaded.h:22
ui_message_handlert::get_ui
virtual uit get_ui() const
Definition: ui_message.h:31
goto_unwindt::unwind_strategyt::ASSUME
@ ASSUME
code_contractst::enforce_contracts
bool enforce_contracts(const std::set< std::string > &)
Turn requires & ensures into assumptions and assertions for each of the named functions.
Definition: code_contracts.cpp:951
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
guard_expr_managert
This is unused by this implementation of guards, but can be used by other implementations of the same...
Definition: guard_expr.h:23
string2int.h
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
split_string
void split_string(const std::string &s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)
Definition: string_utils.cpp:40
set_properties.h
Set the properties to check.
show_call_sequences
void show_call_sequences(const irep_idt &caller, const goto_programt &goto_program)
Definition: call_sequences.cpp:27
aggressive_slicert::doit
void doit()
Removes the body of all functions except those on the shortest path or functions that are reachable f...
Definition: aggressive_slicer.cpp:70
parse_function_pointer_restriction_options_from_cmdline
void parse_function_pointer_restriction_options_from_cmdline(const cmdlinet &cmdline, optionst &options)
Definition: restrict_function_pointers.cpp:229
full_slicer
void full_slicer(goto_functionst &goto_functions, const namespacet &ns, const slicing_criteriont &criterion)
Definition: full_slicer.cpp:345
dot.h
Dump Goto-Program as DOT Graph.
interrupt.h
Interrupt Instrumentation for Goto Programs.
CBMC_VERSION
const char * CBMC_VERSION
escape_analysist
Definition: escape_analysis.h:114
show_symbol_table_brief
void show_symbol_table_brief(const symbol_tablet &symbol_table, ui_message_handlert &ui)
Definition: show_symbol_table.cpp:295
c_object_factory_parameters.h
messaget::error
mstreamt & error() const
Definition: message.h:399
c_object_factory_parameterst
Definition: c_object_factory_parameters.h:15
HELP_INSERT_FINAL_ASSERT_FALSE
#define HELP_INSERT_FINAL_ASSERT_FALSE
Definition: insert_final_assert_false.h:53
banner_string
std::string banner_string(const std::string &front_end, const std::string &version)
Definition: parse_options.cpp:163
goto_instrument_parse_optionst::doit
virtual int doit()
invoke main modules
Definition: goto_instrument_parse_options.cpp:119
goto_programt::output_instruction
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &instruction) const
Output a single instruction.
Definition: goto_program.cpp:41
all_loops
@ all_loops
Definition: wmm.h:39
unwindsett
Definition: unwindset.h:24
branch
void branch(goto_modelt &goto_model, const irep_idt &id)
Definition: branch.cpp:20
goto_instrument_parse_optionst::do_indirect_call_and_rtti_removal
void do_indirect_call_and_rtti_removal(bool force=false)
Definition: goto_instrument_parse_options.cpp:918
restrict_function_pointers.h
Given goto functions and a list of function parameters or globals that are function pointers with lis...
goto_instrument_parse_optionst::get_goto_program
void get_goto_program()
Definition: goto_instrument_parse_options.cpp:980
check_call_sequence
void check_call_sequence(const goto_modelt &goto_model)
Definition: call_sequences.cpp:252
HELP_GOTO_PROGRAM_STATS
#define HELP_GOTO_PROGRAM_STATS
Definition: count_eloc.h:30
points_tot
Definition: points_to.h:23
dump_c
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:1462
undefined_function_abort_path
void undefined_function_abort_path(goto_modelt &goto_model)
Definition: undefined_functions.cpp:34
unwind.h
Loop unwinding.
optionst::is_set
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
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
document_properties_latex
void document_properties_latex(const goto_modelt &goto_model, std::ostream &out)
Definition: document_properties.cpp:370
interrupt
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:53
property_slicer
void property_slicer(goto_functionst &goto_functions, const namespacet &ns, const std::list< std::string > &properties)
Definition: full_slicer.cpp:368
show_properties.h
Show the properties.
remove_pointers
void remove_pointers(goto_modelt &goto_model, value_setst &value_sets)
Remove dereferences in all expressions contained in the program goto_model.
Definition: goto_program_dereference.cpp:285
is_threaded.h
Over-approximate Concurrency for Threaded Goto Programs.
goto_instrument_parse_optionst::instrument_goto_program
void instrument_goto_program()
Definition: goto_instrument_parse_options.cpp:997
goto_unwindt
Definition: unwind.h:24
HELP_REMOVE_CALLS_NO_BODY
#define HELP_REMOVE_CALLS_NO_BODY
Definition: remove_calls_no_body.h:42
dump_c_type_header
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:1507
cmdlinet::get_value
std::string get_value(char option) const
Definition: cmdline.cpp:47
show_symbol_table.h
Show the symbol table.
code_contractst
Definition: code_contracts.h:29
remove_function.h
Remove function definition.
HELP_SHOW_PROPERTIES
#define HELP_SHOW_PROPERTIES
Definition: show_properties.h:29
value_set_fi_fp_removal.h
flow insensitive value set function pointer removal
k_induction
void k_induction(goto_modelt &goto_model, bool base_case, bool step_case, unsigned k)
Definition: k_induction.cpp:162
custom_bitvector_analysist
Definition: custom_bitvector_analysis.h:152
HELP_REMOVE_CONST_FUNCTION_POINTERS
#define HELP_REMOVE_CONST_FUNCTION_POINTERS
Definition: remove_const_function_pointers.h:111
count_eloc
void count_eloc(const goto_modelt &goto_model)
Definition: count_eloc.cpp:50
accelerate.h
Loop Acceleration.
configt::ansi_ct::arch
irep_idt arch
Definition: config.h:85
show_goto_functions
void show_goto_functions(const namespacet &ns, ui_message_handlert &ui_message_handler, const goto_functionst &goto_functions, bool list_only)
Definition: show_goto_functions.cpp:26
FLAG_ENFORCE_CONTRACT
#define FLAG_ENFORCE_CONTRACT
Definition: code_contracts.h:164
aggressive_slicert::call_depth
std::size_t call_depth
Definition: aggressive_slicer.h:68
function_enter
void function_enter(goto_modelt &goto_model, const irep_idt &id)
Definition: function.cpp:72
local_safe_pointers.h
Local safe pointer analysis.
reaching_definitions.h
Range-based reaching definitions analysis (following Field- Sensitive Program Dependence Analysis,...
escape_analysist::instrument
void instrument(goto_modelt &)
Definition: escape_analysis.cpp:458
slice_global_inits
void slice_global_inits(goto_modelt &goto_model)
Definition: slice_global_inits.cpp:31
configt::set_from_symbol_table
void set_from_symbol_table(const symbol_tablet &)
Definition: config.cpp:1205
goto_function_inline
void goto_function_inline(goto_modelt &goto_model, const irep_idt function, message_handlert &message_handler, bool adjust_function, bool caching)
Inline all function calls made from a particular function.
Definition: goto_inline.cpp:216
value_set_analysis_fi.h
Value Set Propagation (flow insensitive)
goto_instrument_parse_optionst::register_languages
void register_languages()
Definition: goto_instrument_languages.cpp:19
goto_functionst::compute_loop_numbers
void compute_loop_numbers()
Definition: goto_functions.cpp:52
CPROVER_EXIT_CONVERSION_FAILED
#define CPROVER_EXIT_CONVERSION_FAILED
Failure to convert / write to another format.
Definition: exit_codes.h:62
widen
std::wstring widen(const char *s)
Definition: unicode.cpp:50
HELP_REPLACE_FUNCTION_BODY
#define HELP_REPLACE_FUNCTION_BODY
Definition: generate_function_bodies.h:93
branch.h
Branch Instrumentation.
read_goto_binary.h
Read Goto Programs.
local_bitvector_analysist::output
void output(std::ostream &out, const goto_functiont &goto_function, const namespacet &ns) const
Definition: local_bitvector_analysis.cpp:358
weak_memory
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)
Definition: weak_memory.cpp:107
parse_nondet_volatile_options
void parse_nondet_volatile_options(const cmdlinet &cmdline, optionst &options)
Definition: nondet_volatile.cpp:406
full_slicer.h
Slicing.
goto_instrument_parse_optionst::partial_inlining_done
bool partial_inlining_done
Definition: goto_instrument_parse_options.h:160
HELP_REPLACE_ALL_CALLS
#define HELP_REPLACE_ALL_CALLS
Definition: code_contracts.h:160
memory_modelt
memory_modelt
Definition: wmm.h:18
my_events
@ my_events
Definition: wmm.h:32
safe_string2unsigned
unsigned safe_string2unsigned(const std::string &str, int base)
Definition: string2int.cpp:19
parse_options_baset::main
virtual int main()
Definition: parse_options.cpp:76
read_first
@ read_first
Definition: wmm.h:30
mmio
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
HELP_ANSI_C_LANGUAGE
#define HELP_ANSI_C_LANGUAGE
Definition: ansi_c_language.h:27
local_safe_pointerst::output
void output(std::ostream &stream, const goto_programt &program, const namespacet &ns)
Output non-null expressions per instruction in human-readable format.
Definition: local_safe_pointers.cpp:189
aggressive_slicert::user_specified_properties
std::list< std::string > user_specified_properties
Definition: aggressive_slicer.h:65
global_may_alias_analysist
This is a may analysis (i.e.
Definition: global_may_alias.h:107
function_path_reachability_slicer
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.
Definition: reachability_slicer.cpp:399
remove_returns.h
Replace function returns by assignments to global variables.
remove_unused_functions.h
Unused function removal.
config
configt config
Definition: config.cpp:24
remove_functions
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...
Definition: remove_function.cpp:68
local_bitvector_analysist
Definition: local_bitvector_analysis.h:24
parse_options_baset::log
messaget log
Definition: parse_options.h:43
function.h
Function Entering and Exiting.
call_grapht
A call graph (https://en.wikipedia.org/wiki/Call_graph) for a GOTO model or GOTO functions collection...
Definition: call_graph.h:39
uninitialized.h
Detection for Uninitialized Local Variables.
points_to.h
Field-sensitive, location-insensitive points-to analysis.
messaget::get_message_handler
message_handlert & get_message_handler()
Definition: message.h:184
goto_instrument_parse_optionst::remove_returns_done
bool remove_returns_done
Definition: goto_instrument_parse_options.h:161
class_hierarchy.h
Class Hierarchy.
interval_domain.h
Interval Domain.
stack_depth.h
Stack depth checks.
show_locations.h
Show program locations.
show_locations
void show_locations(ui_message_handlert::uit ui, const irep_idt function_id, const goto_programt &goto_program)
Definition: show_locations.cpp:23
aggressive_slicert
The aggressive slicer removes the body of all the functions except those on the shortest path,...
Definition: aggressive_slicer.h:37
undefined_functions.h
Handling of functions without body.
min_interference
@ min_interference
Definition: wmm.h:29
arrays_only
@ arrays_only
Definition: wmm.h:38
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
validation_modet::EXCEPTION
@ EXCEPTION
ansi_c_language.h
RESTRICT_FUNCTION_POINTER_OPT
#define RESTRICT_FUNCTION_POINTER_OPT
Definition: restrict_function_pointers.h:29
HELP_REPLACE_CALL
#define HELP_REPLACE_CALL
Definition: code_contracts.h:155
HELP_GOTO_CHECK
#define HELP_GOTO_CHECK
Definition: goto_check.h:45
cprover_c_library_factory
void cprover_c_library_factory(const std::set< irep_idt > &functions, symbol_tablet &symbol_table, message_handlert &message_handler)
Definition: cprover_library.cpp:79
call_sequences.h
Memory-mapped I/O Instrumentation for Goto Programs.
ai_baset::output
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:42
remove_calls_no_bodyt
Definition: remove_calls_no_body.h:20
symbolt
Symbol table entry.
Definition: symbol.h:28
configt::set
bool set(const cmdlinet &cmdline)
Definition: config.cpp:798
rw_set.h
Race Detection for Threaded Goto Programs.
exit_codes.h
Document and give macros for the exit codes of CPROVER binaries.
call_grapht::output
void output(std::ostream &out) const
Definition: call_graph.cpp:271
natural_loops.h
Compute natural loops in a goto_function.
constant_propagator_ait
Definition: constant_propagator.h:171
RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT
#define RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT
Definition: restrict_function_pointers.h:30
goto_program_dereference.h
Value Set.
one_event_per_cycle
@ one_event_per_cycle
Definition: wmm.h:33
remove_returns
void remove_returns(symbol_table_baset &symbol_table, goto_functionst &goto_functions)
removes returns
Definition: remove_returns.cpp:256
show_value_sets.h
Show Value Sets.
aggressive_slicert::name_snippets
std::list< std::string > name_snippets
Definition: aggressive_slicer.h:69
CPROVER_EXIT_USAGE_ERROR
#define CPROVER_EXIT_USAGE_ERROR
A usage error is returned when the command line is invalid or conflicting.
Definition: exit_codes.h:33
nondet_volatile.h
Volatile Variables.
CPROVER_PREFIX
#define CPROVER_PREFIX
Definition: cprover_prefix.h:14
replace_callst
Definition: replace_calls.h:19
unsafe_string2unsigned
unsigned unsafe_string2unsigned(const std::string &str, int base)
Definition: string2int.cpp:38
goto_functionst::update
void update()
Definition: goto_functions.h:81
json.h
remove_asm
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...
Definition: remove_asm.cpp:512
accelerate_functions
void accelerate_functions(goto_modelt &goto_model, message_handlert &message_handler, bool use_z3, guard_managert &guard_manager)
Definition: accelerate.cpp:639
unicode.h
parameter_assignments.h
Add parameter assignments.
aggressive_slicert::preserve_functions
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.
Definition: aggressive_slicer.h:61
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
grapht::output_dot
void output_dot(std::ostream &out) const
Definition: graph.h:963
class_hierarchyt::output_dot
void output_dot(std::ostream &) const
Output class hierarchy in Graphviz DOT format.
Definition: class_hierarchy.cpp:217
custom_bitvector_analysist::check
void check(const goto_modelt &, bool xml, std::ostream &)
Definition: custom_bitvector_analysis.cpp:768
config.h
points_tot::output
void output(std::ostream &out) const
Definition: points_to.cpp:33
insert_final_assert_false
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...
Definition: insert_final_assert_false.cpp:53
read_goto_binary
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.
Definition: read_goto_binary.cpp:59
goto_modelt::validate
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
loop_ids.h
Loop IDs.
forall_goto_functions
#define forall_goto_functions(it, functions)
Definition: goto_functions.h:122
generate_function_bodies_factory
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.
Definition: generate_function_bodies.cpp:385
reachability_slicer.h
Slicing.
code_contractst::replace_calls
bool replace_calls(const std::set< std::string > &)
Replace all calls to each function in the list with that function's contract.
Definition: code_contracts.cpp:876
goto_instrument_parse_optionst::goto_model
goto_modelt goto_model
Definition: goto_instrument_parse_options.h:163
model_argc_argv.h
Initialize command line arguments.
function_exit
void function_exit(goto_modelt &goto_model, const irep_idt &id)
Definition: function.cpp:97
instrumentation_strategyt
instrumentation_strategyt
Definition: wmm.h:27
slice_global_inits.h
Remove initializations of unused global variables.
add_failed_symbols.h
Pointer Dereferencing.
goto_functionst::entry_point
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
Definition: goto_functions.h:90
CPROVER_EXIT_INTERNAL_ERROR
#define CPROVER_EXIT_INTERNAL_ERROR
An error has been encountered during processing the requested analysis.
Definition: exit_codes.h:45
goto_convert_functions.h
Goto Programs with Functions.
document_properties_html
void document_properties_html(const goto_modelt &goto_model, std::ostream &out)
Definition: document_properties.cpp:363
add_failed_symbols
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....
Definition: add_failed_symbols.cpp:76
global_may_alias.h
Field-insensitive, location-sensitive, over-approximative escape analysis.
havoc_loops
void havoc_loops(goto_modelt &goto_model)
Definition: havoc_loops.cpp:120
alignment_checks.h
Alignment Checks.
ensure_one_backedge_per_target.h
Ensure one backedge per target.
CPROVER_EXIT_SUCCESS
#define CPROVER_EXIT_SUCCESS
Success indicates the required analysis has been performed without error.
Definition: exit_codes.h:16
value_set_analysis.h
Value Set Propagation.
HELP_REPLACE_CALLS
#define HELP_REPLACE_CALLS
Definition: replace_calls.h:50
messaget::eval_verbosity
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:104
remove_skip.h
Program Transformation.
list_eloc
void list_eloc(const goto_modelt &goto_model)
Definition: count_eloc.cpp:64
label_function_pointer_call_sites.h
Label function pointer call sites across a goto model.
all
@ all
Definition: wmm.h:28
remove_function_pointers
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)
Definition: remove_function_pointers.cpp:519
nondet_volatile
void nondet_volatile(goto_modelt &goto_model, const optionst &options)
Havoc reads from volatile expressions, if enabled in the options.
Definition: nondet_volatile.cpp:452
invalid_command_line_argument_exceptiont
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
Definition: exception_utils.h:38
dump_c.h
Dump C from Goto Program.
thread_exit_instrumentation
void thread_exit_instrumentation(goto_programt &goto_program)
Definition: thread_instrumentation.cpp:25
cmdlinet::get_values
const std::list< std::string > & get_values(const std::string &option) const
Definition: cmdline.cpp:108
remove_function_pointers.h
Remove Indirect Function Calls.
parse_options_baset::cmdline
cmdlinet cmdline
Definition: parse_options.h:28
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
rw_set_functiont
Definition: rw_set.h:212
align_center_with_border
std::string align_center_with_border(const std::string &text)
Utility for displaying help centered messages borderered by "* *".
Definition: parse_options.cpp:150
print_path_lengths
void print_path_lengths(const goto_modelt &goto_model)
Definition: count_eloc.cpp:81
sese_region_analysist
Definition: sese_regions.h:20
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
cprover_library.h
restore_returns
void restore_returns(goto_modelt &goto_model)
restores return statements
Definition: remove_returns.cpp:403
dump_cpp
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:1480
forall_goto_program_instructions
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:1196
interval_analysis.h
Interval Analysis.
HELP_ENFORCE_ALL_CONTRACTS
#define HELP_ENFORCE_ALL_CONTRACTS
Definition: code_contracts.h:169
list_calls_and_arguments
static void list_calls_and_arguments(const namespacet &ns, const goto_programt &goto_program)
Definition: call_sequences.cpp:271
dependence_graph.h
Field-Sensitive Program Dependence Analysis, Litvak et al., FSE 2010.
FLAG_REPLACE_CALL
#define FLAG_REPLACE_CALL
Definition: code_contracts.h:154
goto_unwindt::output_log_json
jsont output_log_json() const
Definition: unwind.h:72
HELP_TIMESTAMP
#define HELP_TIMESTAMP
Definition: timestamper.h:14
goto_instrument_parse_options.h
Command Line Parsing.
HELP_FLUSH
#define HELP_FLUSH
Definition: ui_message.h:106
HELP_RESTRICT_FUNCTION_POINTER
#define HELP_RESTRICT_FUNCTION_POINTER
Definition: restrict_function_pointers.h:42
interval_analysis
void interval_analysis(goto_modelt &goto_model)
Initialises the abstract interpretation over interval domain and instruments instructions using inter...
Definition: interval_analysis.cpp:89
cprover_cpp_library_factory
void cprover_cpp_library_factory(const std::set< irep_idt > &functions, symbol_tablet &symbol_table, message_handlert &message_handler)
Definition: cprover_library.cpp:38
goto_inline
void goto_inline(goto_modelt &goto_model, message_handlert &message_handler, bool adjust_function)
Definition: goto_inline.cpp:23
escape_analysis.h
Field-insensitive, location-sensitive, over-approximative escape analysis.
HELP_VALIDATE
#define HELP_VALIDATE
Definition: validation_interface.h:16
HELP_NONDET_VOLATILE
#define HELP_NONDET_VOLATILE
Definition: nondet_volatile.h:30