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>
53 
59 
60 #include <analyses/call_graph.h>
68 #include <analyses/is_threaded.h>
69 #include <analyses/lexical_loops.h>
72 #include <analyses/natural_loops.h>
74 #include <analyses/sese_regions.h>
75 
76 #include <ansi-c/ansi_c_language.h>
78 #include <ansi-c/cprover_library.h>
79 
80 #include <assembler/remove_asm.h>
81 
82 #include <cpp/cprover_library.h>
83 
84 #include "accelerate/accelerate.h"
85 #include "alignment_checks.h"
86 #include "branch.h"
87 #include "call_sequences.h"
88 #include "concurrency.h"
89 #include "document_properties.h"
90 #include "dot.h"
91 #include "dump_c.h"
92 #include "full_slicer.h"
93 #include "function.h"
94 #include "havoc_loops.h"
95 #include "horn_encoding.h"
97 #include "interrupt.h"
98 #include "k_induction.h"
99 #include "mmio.h"
100 #include "model_argc_argv.h"
101 #include "nondet_static.h"
102 #include "nondet_volatile.h"
103 #include "points_to.h"
104 #include "race_check.h"
105 #include "reachability_slicer.h"
106 #include "remove_function.h"
107 #include "rw_set.h"
108 #include "show_locations.h"
109 #include "skip_loops.h"
110 #include "splice_call.h"
111 #include "stack_depth.h"
112 #include "thread_instrumentation.h"
113 #include "undefined_functions.h"
114 #include "uninitialized.h"
115 #include "unwind.h"
116 #include "value_set_fi_fp_removal.h"
117 #include "wmm/weak_memory.h"
118 
121 {
122  if(cmdline.isset("version"))
123  {
124  std::cout << CBMC_VERSION << '\n';
125  return CPROVER_EXIT_SUCCESS;
126  }
127 
128  if(cmdline.args.size()!=1 && cmdline.args.size()!=2)
129  {
130  help();
132  }
133 
136 
137  {
139 
141 
142  {
143  const bool validate_only = cmdline.isset("validate-goto-binary");
144 
145  if(validate_only || cmdline.isset("validate-goto-model"))
146  {
148 
149  if(validate_only)
150  {
151  return CPROVER_EXIT_SUCCESS;
152  }
153  }
154  }
155 
157 
158  if(cmdline.isset("validate-goto-model"))
159  {
161  }
162 
163  {
164  bool unwind_given=cmdline.isset("unwind");
165  bool unwindset_given=cmdline.isset("unwindset");
166  bool unwindset_file_given=cmdline.isset("unwindset-file");
167 
168  if(unwindset_given && unwindset_file_given)
169  throw "only one of --unwindset and --unwindset-file supported at a "
170  "time";
171 
172  if(unwind_given || unwindset_given || unwindset_file_given)
173  {
174  unwindsett unwindset;
175 
176  if(unwind_given)
177  unwindset.parse_unwind(cmdline.get_value("unwind"));
178 
179  if(unwindset_file_given)
180  unwindset.parse_unwindset_file(cmdline.get_value("unwindset-file"));
181 
182  if(unwindset_given)
183  unwindset.parse_unwindset(cmdline.get_values("unwindset"));
184 
185  bool unwinding_assertions=cmdline.isset("unwinding-assertions");
186  bool partial_loops=cmdline.isset("partial-loops");
187  bool continue_as_loops=cmdline.isset("continue-as-loops");
188 
189  if(unwinding_assertions+partial_loops+continue_as_loops>1)
190  throw "more than one of --unwinding-assertions,--partial-loops,"
191  "--continue-as-loops selected";
192 
193  goto_unwindt::unwind_strategyt unwind_strategy=
195 
196  if(unwinding_assertions)
197  {
199  }
200  else if(partial_loops)
201  {
203  }
204  else if(continue_as_loops)
205  {
207  }
208 
209  goto_unwindt goto_unwind;
210  goto_unwind(goto_model, unwindset, unwind_strategy);
211 
212  if(cmdline.isset("log"))
213  {
214  std::string filename=cmdline.get_value("log");
215  bool have_file=!filename.empty() && filename!="-";
216 
217  jsont result=goto_unwind.output_log_json();
218 
219  if(have_file)
220  {
221 #ifdef _MSC_VER
222  std::ofstream of(widen(filename));
223 #else
224  std::ofstream of(filename);
225 #endif
226  if(!of)
227  throw "failed to open file "+filename;
228 
229  of << result;
230  of.close();
231  }
232  else
233  {
234  std::cout << result << '\n';
235  }
236  }
237 
238  // goto_unwind holds references to instructions, only do remove_skip
239  // after having generated the log above
241  }
242  }
243 
244  if(cmdline.isset("show-threaded"))
245  {
247 
248  is_threadedt is_threaded(goto_model);
249 
250  for(const auto &gf_entry : goto_model.goto_functions.function_map)
251  {
252  std::cout << "////\n";
253  std::cout << "//// Function: " << gf_entry.first << '\n';
254  std::cout << "////\n\n";
255 
256  const goto_programt &goto_program = gf_entry.second.body;
257 
258  forall_goto_program_instructions(i_it, goto_program)
259  {
260  goto_program.output_instruction(ns, gf_entry.first, std::cout, *i_it);
261  std::cout << "Is threaded: " << (is_threaded(i_it)?"True":"False")
262  << "\n\n";
263  }
264  }
265 
266  return CPROVER_EXIT_SUCCESS;
267  }
268 
269  if(cmdline.isset("insert-final-assert-false"))
270  {
271  log.status() << "Inserting final assert false" << messaget::eom;
272  bool fail = insert_final_assert_false(
273  goto_model,
274  cmdline.get_value("insert-final-assert-false"),
276  if(fail)
277  {
279  }
280  // otherwise, fall-through to write new binary
281  }
282 
283  if(cmdline.isset("show-value-sets"))
284  {
286 
287  // recalculate numbers, etc.
289 
290  log.status() << "Pointer Analysis" << messaget::eom;
292  value_set_analysist value_set_analysis(ns);
293  value_set_analysis(goto_model.goto_functions);
295  ui_message_handler.get_ui(), goto_model, value_set_analysis);
296  return CPROVER_EXIT_SUCCESS;
297  }
298 
299  if(cmdline.isset("show-global-may-alias"))
300  {
304 
305  // recalculate numbers, etc.
307 
308  global_may_alias_analysist global_may_alias_analysis;
309  global_may_alias_analysis(goto_model);
310  global_may_alias_analysis.output(goto_model, std::cout);
311 
312  return CPROVER_EXIT_SUCCESS;
313  }
314 
315  if(cmdline.isset("show-local-bitvector-analysis"))
316  {
319 
320  // recalculate numbers, etc.
322 
324 
325  for(const auto &gf_entry : goto_model.goto_functions.function_map)
326  {
327  local_bitvector_analysist local_bitvector_analysis(gf_entry.second, ns);
328  std::cout << ">>>>\n";
329  std::cout << ">>>> " << gf_entry.first << '\n';
330  std::cout << ">>>>\n";
331  local_bitvector_analysis.output(std::cout, gf_entry.second, ns);
332  std::cout << '\n';
333  }
334 
335  return CPROVER_EXIT_SUCCESS;
336  }
337 
338  if(cmdline.isset("show-local-safe-pointers") ||
339  cmdline.isset("show-safe-dereferences"))
340  {
341  // Ensure location numbering is unique:
343 
345 
346  for(const auto &gf_entry : goto_model.goto_functions.function_map)
347  {
348  local_safe_pointerst local_safe_pointers;
349  local_safe_pointers(gf_entry.second.body);
350  std::cout << ">>>>\n";
351  std::cout << ">>>> " << gf_entry.first << '\n';
352  std::cout << ">>>>\n";
353  if(cmdline.isset("show-local-safe-pointers"))
354  local_safe_pointers.output(std::cout, gf_entry.second.body, ns);
355  else
356  {
357  local_safe_pointers.output_safe_dereferences(
358  std::cout, gf_entry.second.body, ns);
359  }
360  std::cout << '\n';
361  }
362 
363  return CPROVER_EXIT_SUCCESS;
364  }
365 
366  if(cmdline.isset("show-sese-regions"))
367  {
368  // Ensure location numbering is unique:
370 
372 
373  for(const auto &gf_entry : goto_model.goto_functions.function_map)
374  {
375  sese_region_analysist sese_region_analysis;
376  sese_region_analysis(gf_entry.second.body);
377  std::cout << ">>>>\n";
378  std::cout << ">>>> " << gf_entry.first << '\n';
379  std::cout << ">>>>\n";
380  sese_region_analysis.output(std::cout, gf_entry.second.body, ns);
381  std::cout << '\n';
382  }
383 
384  return CPROVER_EXIT_SUCCESS;
385  }
386 
387  if(cmdline.isset("show-custom-bitvector-analysis"))
388  {
392 
394 
395  if(!cmdline.isset("inline"))
396  {
399  }
400 
401  // recalculate numbers, etc.
403 
404  custom_bitvector_analysist custom_bitvector_analysis;
405  custom_bitvector_analysis(goto_model);
406  custom_bitvector_analysis.output(goto_model, std::cout);
407 
408  return CPROVER_EXIT_SUCCESS;
409  }
410 
411  if(cmdline.isset("show-escape-analysis"))
412  {
416 
417  // recalculate numbers, etc.
419 
420  escape_analysist escape_analysis;
421  escape_analysis(goto_model);
422  escape_analysis.output(goto_model, std::cout);
423 
424  return CPROVER_EXIT_SUCCESS;
425  }
426 
427  if(cmdline.isset("custom-bitvector-analysis"))
428  {
432 
434 
435  if(!cmdline.isset("inline"))
436  {
439  }
440 
441  // recalculate numbers, etc.
443 
445 
446  custom_bitvector_analysist custom_bitvector_analysis;
447  custom_bitvector_analysis(goto_model);
448  custom_bitvector_analysis.check(
449  goto_model,
450  cmdline.isset("xml-ui"),
451  std::cout);
452 
453  return CPROVER_EXIT_SUCCESS;
454  }
455 
456  if(cmdline.isset("show-points-to"))
457  {
459 
460  // recalculate numbers, etc.
462 
464 
465  log.status() << "Pointer Analysis" << messaget::eom;
466  points_tot points_to;
467  points_to(goto_model);
468  points_to.output(std::cout);
469  return CPROVER_EXIT_SUCCESS;
470  }
471 
472  if(cmdline.isset("show-intervals"))
473  {
475 
476  // recalculate numbers, etc.
478 
479  log.status() << "Interval Analysis" << messaget::eom;
483  interval_analysis.output(goto_model, std::cout);
484  return CPROVER_EXIT_SUCCESS;
485  }
486 
487  if(cmdline.isset("show-call-sequences"))
488  {
491  return CPROVER_EXIT_SUCCESS;
492  }
493 
494  if(cmdline.isset("check-call-sequence"))
495  {
498  return CPROVER_EXIT_SUCCESS;
499  }
500 
501  if(cmdline.isset("list-calls-args"))
502  {
504 
506 
507  return CPROVER_EXIT_SUCCESS;
508  }
509 
510  if(cmdline.isset("show-rw-set"))
511  {
513 
514  if(!cmdline.isset("inline"))
515  {
517 
518  // recalculate numbers, etc.
520  }
521 
522  log.status() << "Pointer Analysis" << messaget::eom;
523  value_set_analysist value_set_analysis(ns);
524  value_set_analysis(goto_model.goto_functions);
525 
526  const symbolt &symbol=ns.lookup(ID_main);
527  symbol_exprt main(symbol.name, symbol.type);
528 
529  std::cout <<
530  rw_set_functiont(value_set_analysis, goto_model, main);
531  return CPROVER_EXIT_SUCCESS;
532  }
533 
534  if(cmdline.isset("show-symbol-table"))
535  {
537  return CPROVER_EXIT_SUCCESS;
538  }
539 
540  if(cmdline.isset("show-reaching-definitions"))
541  {
543 
545  reaching_definitions_analysist rd_analysis(ns);
546  rd_analysis(goto_model);
547  rd_analysis.output(goto_model, std::cout);
548 
549  return CPROVER_EXIT_SUCCESS;
550  }
551 
552  if(cmdline.isset("show-dependence-graph"))
553  {
555 
557  dependence_grapht dependence_graph(ns);
558  dependence_graph(goto_model);
559  dependence_graph.output(goto_model, std::cout);
560  dependence_graph.output_dot(std::cout);
561 
562  return CPROVER_EXIT_SUCCESS;
563  }
564 
565  if(cmdline.isset("count-eloc"))
566  {
568  return CPROVER_EXIT_SUCCESS;
569  }
570 
571  if(cmdline.isset("list-eloc"))
572  {
574  return CPROVER_EXIT_SUCCESS;
575  }
576 
577  if(cmdline.isset("print-path-lengths"))
578  {
580  return CPROVER_EXIT_SUCCESS;
581  }
582 
583  if(cmdline.isset("print-global-state-size"))
584  {
586  return CPROVER_EXIT_SUCCESS;
587  }
588 
589  if(cmdline.isset("list-symbols"))
590  {
592  return CPROVER_EXIT_SUCCESS;
593  }
594 
595  if(cmdline.isset("show-uninitialized"))
596  {
597  show_uninitialized(goto_model, std::cout);
598  return CPROVER_EXIT_SUCCESS;
599  }
600 
601  if(cmdline.isset("interpreter"))
602  {
605 
606  log.status() << "Starting interpreter" << messaget::eom;
608  return CPROVER_EXIT_SUCCESS;
609  }
610 
611  if(cmdline.isset("show-claims") ||
612  cmdline.isset("show-properties"))
613  {
616  return CPROVER_EXIT_SUCCESS;
617  }
618 
619  if(cmdline.isset("document-claims-html") ||
620  cmdline.isset("document-properties-html"))
621  {
623  return CPROVER_EXIT_SUCCESS;
624  }
625 
626  if(cmdline.isset("document-claims-latex") ||
627  cmdline.isset("document-properties-latex"))
628  {
630  return CPROVER_EXIT_SUCCESS;
631  }
632 
633  if(cmdline.isset("show-loops"))
634  {
636  return CPROVER_EXIT_SUCCESS;
637  }
638 
639  if(cmdline.isset("show-natural-loops"))
640  {
641  show_natural_loops(goto_model, std::cout);
642  return CPROVER_EXIT_SUCCESS;
643  }
644 
645  if(cmdline.isset("show-lexical-loops"))
646  {
647  show_lexical_loops(goto_model, std::cout);
648  }
649 
650  if(cmdline.isset("print-internal-representation"))
651  {
652  for(auto const &pair : goto_model.goto_functions.function_map)
653  for(auto const &ins : pair.second.body.instructions)
654  {
655  if(ins.get_code().is_not_nil())
656  log.status() << ins.get_code().pretty() << messaget::eom;
657  if(ins.has_condition())
658  {
659  log.status() << "[guard] " << ins.get_condition().pretty()
660  << messaget::eom;
661  }
662  }
663  return CPROVER_EXIT_SUCCESS;
664  }
665 
666  if(
667  cmdline.isset("show-goto-functions") ||
668  cmdline.isset("list-goto-functions"))
669  {
671  goto_model, ui_message_handler, cmdline.isset("list-goto-functions"));
672  return CPROVER_EXIT_SUCCESS;
673  }
674 
675  if(cmdline.isset("list-undefined-functions"))
676  {
678  return CPROVER_EXIT_SUCCESS;
679  }
680 
681  // experimental: print structs
682  if(cmdline.isset("show-struct-alignment"))
683  {
685  return CPROVER_EXIT_SUCCESS;
686  }
687 
688  if(cmdline.isset("show-locations"))
689  {
691  return CPROVER_EXIT_SUCCESS;
692  }
693 
694  if(
695  cmdline.isset("dump-c") || cmdline.isset("dump-cpp") ||
696  cmdline.isset("dump-c-type-header"))
697  {
698  const bool is_cpp=cmdline.isset("dump-cpp");
699  const bool is_header = cmdline.isset("dump-c-type-header");
700  const bool h_libc=!cmdline.isset("no-system-headers");
701  const bool h_all=cmdline.isset("use-all-headers");
702  const bool harness=cmdline.isset("harness");
704 
705  // restore RETURN instructions in case remove_returns had been
706  // applied
708 
709  // dump_c (actually goto_program2code) requires valid instruction
710  // location numbers:
712 
713  if(cmdline.args.size()==2)
714  {
715  #ifdef _MSC_VER
716  std::ofstream out(widen(cmdline.args[1]));
717  #else
718  std::ofstream out(cmdline.args[1]);
719  #endif
720  if(!out)
721  {
722  log.error() << "failed to write to '" << cmdline.args[1] << "'";
724  }
725  if(is_header)
726  {
729  h_libc,
730  h_all,
731  harness,
732  ns,
733  cmdline.get_value("dump-c-type-header"),
734  out);
735  }
736  else
737  {
738  (is_cpp ? dump_cpp : dump_c)(
739  goto_model.goto_functions, h_libc, h_all, harness, ns, out);
740  }
741  }
742  else
743  {
744  if(is_header)
745  {
748  h_libc,
749  h_all,
750  harness,
751  ns,
752  cmdline.get_value("dump-c-type-header"),
753  std::cout);
754  }
755  else
756  {
757  (is_cpp ? dump_cpp : dump_c)(
758  goto_model.goto_functions, h_libc, h_all, harness, ns, std::cout);
759  }
760  }
761 
762  return CPROVER_EXIT_SUCCESS;
763  }
764 
765  if(cmdline.isset("call-graph"))
766  {
768  call_grapht call_graph(goto_model);
769 
770  if(cmdline.isset("xml"))
771  call_graph.output_xml(std::cout);
772  else if(cmdline.isset("dot"))
773  call_graph.output_dot(std::cout);
774  else
775  call_graph.output(std::cout);
776 
777  return CPROVER_EXIT_SUCCESS;
778  }
779 
780  if(cmdline.isset("reachable-call-graph"))
781  {
783  call_grapht call_graph =
786  if(cmdline.isset("xml"))
787  call_graph.output_xml(std::cout);
788  else if(cmdline.isset("dot"))
789  call_graph.output_dot(std::cout);
790  else
791  call_graph.output(std::cout);
792 
793  return 0;
794  }
795 
796  if(cmdline.isset("show-class-hierarchy"))
797  {
798  class_hierarchyt hierarchy;
799  hierarchy(goto_model.symbol_table);
800  if(cmdline.isset("dot"))
801  hierarchy.output_dot(std::cout);
802  else
804 
805  return CPROVER_EXIT_SUCCESS;
806  }
807 
808  if(cmdline.isset("dot"))
809  {
811 
812  if(cmdline.args.size()==2)
813  {
814  #ifdef _MSC_VER
815  std::ofstream out(widen(cmdline.args[1]));
816  #else
817  std::ofstream out(cmdline.args[1]);
818  #endif
819  if(!out)
820  {
821  log.error() << "failed to write to " << cmdline.args[1] << "'";
823  }
824 
825  dot(goto_model, out);
826  }
827  else
828  dot(goto_model, std::cout);
829 
830  return CPROVER_EXIT_SUCCESS;
831  }
832 
833  if(cmdline.isset("accelerate"))
834  {
836 
838 
839  log.status() << "Performing full inlining" << messaget::eom;
841 
842  log.status() << "Removing calls to functions without a body"
843  << messaget::eom;
844  remove_calls_no_bodyt remove_calls_no_body;
845  remove_calls_no_body(goto_model.goto_functions);
846 
847  log.status() << "Accelerating" << messaget::eom;
848  guard_managert guard_manager;
850  goto_model, ui_message_handler, cmdline.isset("z3"), guard_manager);
852  }
853 
854  if(cmdline.isset("horn-encoding"))
855  {
856  log.status() << "Horn-clause encoding" << messaget::eom;
858 
859  if(cmdline.args.size()==2)
860  {
861  #ifdef _MSC_VER
862  std::ofstream out(widen(cmdline.args[1]));
863  #else
864  std::ofstream out(cmdline.args[1]);
865  #endif
866 
867  if(!out)
868  {
869  log.error() << "Failed to open output file " << cmdline.args[1]
870  << messaget::eom;
872  }
873 
875  }
876  else
877  horn_encoding(goto_model, std::cout);
878 
879  return CPROVER_EXIT_SUCCESS;
880  }
881 
882  if(cmdline.isset("drop-unused-functions"))
883  {
885 
886  log.status() << "Removing unused functions" << messaget::eom;
888  }
889 
890  if(cmdline.isset("undefined-function-is-assume-false"))
891  {
894  }
895 
896  // write new binary?
897  if(cmdline.args.size()==2)
898  {
899  log.status() << "Writing GOTO program to '" << cmdline.args[1] << "'"
900  << messaget::eom;
901 
904  else
905  return CPROVER_EXIT_SUCCESS;
906  }
907  else if(cmdline.args.size() < 2)
908  {
910  "Invalid number of positional arguments passed",
911  "[in] [out]",
912  "goto-instrument needs one input and one output file, aside from other "
913  "flags");
914  }
915 
916  help();
918  }
919 // NOLINTNEXTLINE(readability/fn_size)
920 }
921 
923  bool force)
924 {
925  if(function_pointer_removal_done && !force)
926  return;
927 
929 
930  log.status() << "Function Pointer Removal" << messaget::eom;
932  ui_message_handler, goto_model, cmdline.isset("pointer-check"));
933  log.status() << "Virtual function removal" << messaget::eom;
935  log.status() << "Cleaning inline assembler statements" << messaget::eom;
937 }
938 
943 {
944  // Don't bother if we've already done a full function pointer
945  // removal.
947  {
948  return;
949  }
950 
951  log.status() << "Removing const function pointers only" << messaget::eom;
954  goto_model,
955  cmdline.isset("pointer-check"),
956  true); // abort if we can't resolve via const pointers
957 }
958 
960 {
962  return;
963 
965 
966  if(!cmdline.isset("inline"))
967  {
968  log.status() << "Partial Inlining" << messaget::eom;
970  }
971 }
972 
974 {
976  return;
977 
978  remove_returns_done=true;
979 
980  log.status() << "Removing returns" << messaget::eom;
982 }
983 
985 {
986  log.status() << "Reading GOTO program from '" << cmdline.args[0] << "'"
987  << messaget::eom;
988 
989  config.set(cmdline);
990 
991  auto result = read_goto_binary(cmdline.args[0], ui_message_handler);
992 
993  if(!result.has_value())
994  throw 0;
995 
996  goto_model = std::move(result.value());
997 
999 }
1000 
1002 {
1003  optionst options;
1004 
1006 
1007  // disable simplify when adding various checks?
1008  if(cmdline.isset("no-simplify"))
1009  options.set_option("simplify", false);
1010  else
1011  options.set_option("simplify", true);
1012 
1013  // all checks supported by goto_check
1015 
1016  // unwind loops
1017  if(cmdline.isset("unwind"))
1018  {
1019  log.status() << "Unwinding loops" << messaget::eom;
1020  options.set_option("unwind", cmdline.get_value("unwind"));
1021  }
1022 
1023  {
1025 
1026  if(
1030  {
1032 
1033  const auto function_pointer_restrictions =
1035  options, goto_model, log.get_message_handler());
1036 
1037  restrict_function_pointers(goto_model, function_pointer_restrictions);
1038  }
1039  }
1040 
1041  // skip over selected loops
1042  if(cmdline.isset("skip-loops"))
1043  {
1044  log.status() << "Adding gotos to skip loops" << messaget::eom;
1045  if(skip_loops(
1047  throw 0;
1048  }
1049 
1051 
1052  // initialize argv with valid pointers
1053  if(cmdline.isset("model-argc-argv"))
1054  {
1055  unsigned max_argc=
1056  safe_string2unsigned(cmdline.get_value("model-argc-argv"));
1057 
1058  log.status() << "Adding up to " << max_argc << " command line arguments"
1059  << messaget::eom;
1061  throw 0;
1062  }
1063 
1064  if(cmdline.isset("remove-function-body"))
1065  {
1067  goto_model,
1068  cmdline.get_values("remove-function-body"),
1070  }
1071 
1072  // we add the library in some cases, as some analyses benefit
1073 
1074  if(cmdline.isset("add-library") ||
1075  cmdline.isset("mm"))
1076  {
1077  if(cmdline.isset("show-custom-bitvector-analysis") ||
1078  cmdline.isset("custom-bitvector-analysis"))
1079  {
1080  config.ansi_c.defines.push_back(
1081  std::string(CPROVER_PREFIX) + "CUSTOM_BITVECTOR_ANALYSIS");
1082  }
1083 
1084  // add the library
1085  log.status() << "Adding CPROVER library (" << config.ansi_c.arch << ")"
1086  << messaget::eom;
1090  }
1091 
1092  // now do full inlining, if requested
1093  if(cmdline.isset("inline"))
1094  {
1096 
1097  if(cmdline.isset("show-custom-bitvector-analysis") ||
1098  cmdline.isset("custom-bitvector-analysis"))
1099  {
1103  }
1104 
1105  log.status() << "Performing full inlining" << messaget::eom;
1107  }
1108 
1109  if(cmdline.isset("show-custom-bitvector-analysis") ||
1110  cmdline.isset("custom-bitvector-analysis"))
1111  {
1112  log.status() << "Propagating Constants" << messaget::eom;
1113  constant_propagator_ait constant_propagator_ai(goto_model);
1115  }
1116 
1117  if(cmdline.isset("escape-analysis"))
1118  {
1122 
1123  // recalculate numbers, etc.
1125 
1126  log.status() << "Escape Analysis" << messaget::eom;
1127  escape_analysist escape_analysis;
1128  escape_analysis(goto_model);
1129  escape_analysis.instrument(goto_model);
1130 
1131  // inline added functions, they are often small
1133 
1134  // recalculate numbers, etc.
1136  }
1137 
1138  const std::list<std::pair<std::string, std::string>> contract_flags(
1141  for(const auto &pair : contract_flags)
1142  {
1143  if(cmdline.isset(pair.first.c_str()) && cmdline.isset(pair.second.c_str()))
1144  {
1145  log.error() << "Pass at most one of --" << pair.first << " and --"
1146  << pair.second << "." << messaget::eom;
1148  }
1149  }
1150 
1151  if(
1155  {
1157 
1159  {
1160  std::set<std::string> to_replace(
1163  if(cont.replace_calls(to_replace))
1165  }
1166 
1168  if(cont.replace_calls())
1170 
1172  {
1173  std::set<std::string> to_enforce(
1176  if(cont.enforce_contracts(to_enforce))
1178  }
1179 
1181  if(cont.enforce_contracts())
1183  }
1184 
1185  if(cmdline.isset("value-set-fi-fp-removal"))
1186  {
1189  }
1190 
1191  // replace function pointers, if explicitly requested
1192  if(cmdline.isset("remove-function-pointers"))
1193  {
1195  }
1196  else if(cmdline.isset("remove-const-function-pointers"))
1197  {
1199  }
1200 
1201  if(cmdline.isset("replace-calls"))
1202  {
1204 
1205  replace_callst replace_calls;
1206  replace_calls(goto_model, cmdline.get_values("replace-calls"));
1207  }
1208 
1209  if(cmdline.isset("function-inline"))
1210  {
1211  std::string function=cmdline.get_value("function-inline");
1212  PRECONDITION(!function.empty());
1213 
1214  bool caching=!cmdline.isset("no-caching");
1215 
1217 
1218  log.status() << "Inlining calls of function '" << function << "'"
1219  << messaget::eom;
1220 
1221  if(!cmdline.isset("log"))
1222  {
1224  goto_model, function, ui_message_handler, true, caching);
1225  }
1226  else
1227  {
1228  std::string filename=cmdline.get_value("log");
1229  bool have_file=!filename.empty() && filename!="-";
1230 
1232  goto_model, function, ui_message_handler, true, caching);
1233 
1234  if(have_file)
1235  {
1236 #ifdef _MSC_VER
1237  std::ofstream of(widen(filename));
1238 #else
1239  std::ofstream of(filename);
1240 #endif
1241  if(!of)
1242  throw "failed to open file "+filename;
1243 
1244  of << result;
1245  of.close();
1246  }
1247  else
1248  {
1249  std::cout << result << '\n';
1250  }
1251  }
1252 
1255  }
1256 
1257  if(cmdline.isset("partial-inline"))
1258  {
1260 
1261  log.status() << "Partial inlining" << messaget::eom;
1263 
1266  }
1267 
1268  if(cmdline.isset("remove-calls-no-body"))
1269  {
1270  log.status() << "Removing calls to functions without a body"
1271  << messaget::eom;
1272 
1273  remove_calls_no_bodyt remove_calls_no_body;
1274  remove_calls_no_body(goto_model.goto_functions);
1275 
1278  }
1279 
1280  if(cmdline.isset("constant-propagator"))
1281  {
1283 
1284  log.status() << "Propagating Constants" << messaget::eom;
1285 
1286  constant_propagator_ait constant_propagator_ai(goto_model);
1288  }
1289 
1290  if(cmdline.isset("generate-function-body"))
1291  {
1292  optionst c_object_factory_options;
1293  parse_c_object_factory_options(cmdline, c_object_factory_options);
1294  c_object_factory_parameterst object_factory_parameters(
1295  c_object_factory_options);
1296 
1297  auto generate_implementation = generate_function_bodies_factory(
1298  cmdline.get_value("generate-function-body-options"),
1299  object_factory_parameters,
1303  std::regex(cmdline.get_value("generate-function-body")),
1304  *generate_implementation,
1305  goto_model,
1307  }
1308 
1309  if(cmdline.isset("generate-havocing-body"))
1310  {
1311  optionst c_object_factory_options;
1312  parse_c_object_factory_options(cmdline, c_object_factory_options);
1313  c_object_factory_parameterst object_factory_parameters(
1314  c_object_factory_options);
1315 
1316  auto options_split =
1317  split_string(cmdline.get_value("generate-havocing-body"), ',');
1318  if(options_split.size() < 2)
1320  "not enough arguments for this option", "--generate-havocing-body"};
1321 
1322  if(options_split.size() == 2)
1323  {
1324  auto generate_implementation = generate_function_bodies_factory(
1325  std::string{"havoc,"} + options_split.back(),
1326  object_factory_parameters,
1330  std::regex(options_split[0]),
1331  *generate_implementation,
1332  goto_model,
1334  }
1335  else
1336  {
1337  CHECK_RETURN(options_split.size() % 2 == 1);
1338  for(size_t i = 1; i + 1 < options_split.size(); i += 2)
1339  {
1340  auto generate_implementation = generate_function_bodies_factory(
1341  std::string{"havoc,"} + options_split[i + 1],
1342  object_factory_parameters,
1346  options_split[0],
1347  options_split[i],
1348  *generate_implementation,
1349  goto_model,
1351  }
1352  }
1353  }
1354 
1355  // add generic checks, if needed
1356  goto_check(options, goto_model);
1357 
1358  // check for uninitalized local variables
1359  if(cmdline.isset("uninitialized-check"))
1360  {
1361  log.status() << "Adding checks for uninitialized local variables"
1362  << messaget::eom;
1364  }
1365 
1366  // check for maximum call stack size
1367  if(cmdline.isset("stack-depth"))
1368  {
1369  log.status() << "Adding check for maximum call stack size" << messaget::eom;
1370  stack_depth(
1371  goto_model,
1372  safe_string2size_t(cmdline.get_value("stack-depth")));
1373  }
1374 
1375  // ignore default/user-specified initialization of variables with static
1376  // lifetime
1377  if(cmdline.isset("nondet-static-exclude"))
1378  {
1379  log.status() << "Adding nondeterministic initialization "
1380  "of static/global variables except for "
1381  "the specified ones."
1382  << messaget::eom;
1383 
1384  nondet_static(goto_model, cmdline.get_values("nondet-static-exclude"));
1385  }
1386  else if(cmdline.isset("nondet-static"))
1387  {
1388  log.status() << "Adding nondeterministic initialization "
1389  "of static/global variables"
1390  << messaget::eom;
1392  }
1393 
1394  if(cmdline.isset("slice-global-inits"))
1395  {
1396  log.status() << "Slicing away initializations of unused global variables"
1397  << messaget::eom;
1399  }
1400 
1401  if(cmdline.isset("string-abstraction"))
1402  {
1405 
1406  log.status() << "String Abstraction" << messaget::eom;
1408  }
1409 
1410  // some analyses require function pointer removal and partial inlining
1411 
1412  if(cmdline.isset("remove-pointers") ||
1413  cmdline.isset("race-check") ||
1414  cmdline.isset("mm") ||
1415  cmdline.isset("isr") ||
1416  cmdline.isset("concurrency"))
1417  {
1419 
1420  log.status() << "Pointer Analysis" << messaget::eom;
1421  value_set_analysist value_set_analysis(ns);
1422  value_set_analysis(goto_model.goto_functions);
1423 
1424  if(cmdline.isset("remove-pointers"))
1425  {
1426  // removing pointers
1427  log.status() << "Removing Pointers" << messaget::eom;
1428  remove_pointers(goto_model, value_set_analysis);
1429  }
1430 
1431  if(cmdline.isset("race-check"))
1432  {
1433  log.status() << "Adding Race Checks" << messaget::eom;
1434  race_check(value_set_analysis, goto_model);
1435  }
1436 
1437  if(cmdline.isset("mm"))
1438  {
1439  std::string mm=cmdline.get_value("mm");
1440  memory_modelt model;
1441 
1442  // strategy of instrumentation
1443  instrumentation_strategyt inst_strategy;
1444  if(cmdline.isset("one-event-per-cycle"))
1445  inst_strategy=one_event_per_cycle;
1446  else if(cmdline.isset("minimum-interference"))
1447  inst_strategy=min_interference;
1448  else if(cmdline.isset("read-first"))
1449  inst_strategy=read_first;
1450  else if(cmdline.isset("write-first"))
1451  inst_strategy=write_first;
1452  else if(cmdline.isset("my-events"))
1453  inst_strategy=my_events;
1454  else
1455  /* default: instruments all unsafe pairs */
1456  inst_strategy=all;
1457 
1458  const unsigned max_var=
1459  cmdline.isset("max-var")?
1461  const unsigned max_po_trans=
1462  cmdline.isset("max-po-trans")?
1463  unsafe_string2unsigned(cmdline.get_value("max-po-trans")):0;
1464 
1465  if(mm=="tso")
1466  {
1467  log.status() << "Adding weak memory (TSO) Instrumentation"
1468  << messaget::eom;
1469  model=TSO;
1470  }
1471  else if(mm=="pso")
1472  {
1473  log.status() << "Adding weak memory (PSO) Instrumentation"
1474  << messaget::eom;
1475  model=PSO;
1476  }
1477  else if(mm=="rmo")
1478  {
1479  log.status() << "Adding weak memory (RMO) Instrumentation"
1480  << messaget::eom;
1481  model=RMO;
1482  }
1483  else if(mm=="power")
1484  {
1485  log.status() << "Adding weak memory (Power) Instrumentation"
1486  << messaget::eom;
1487  model=Power;
1488  }
1489  else
1490  {
1491  log.error() << "Unknown weak memory model '" << mm << "'"
1492  << messaget::eom;
1493  model=Unknown;
1494  }
1495 
1497 
1498  if(cmdline.isset("force-loop-duplication"))
1499  loops=all_loops;
1500  if(cmdline.isset("no-loop-duplication"))
1501  loops=no_loop;
1502 
1503  if(model!=Unknown)
1504  weak_memory(
1505  model,
1506  value_set_analysis,
1507  goto_model,
1508  cmdline.isset("scc"),
1509  inst_strategy,
1510  !cmdline.isset("cfg-kill"),
1511  cmdline.isset("no-dependencies"),
1512  loops,
1513  max_var,
1514  max_po_trans,
1515  !cmdline.isset("no-po-rendering"),
1516  cmdline.isset("render-cluster-file"),
1517  cmdline.isset("render-cluster-function"),
1518  cmdline.isset("cav11"),
1519  cmdline.isset("hide-internals"),
1521  cmdline.isset("ignore-arrays"));
1522  }
1523 
1524  // Interrupt handler
1525  if(cmdline.isset("isr"))
1526  {
1527  log.status() << "Instrumenting interrupt handler" << messaget::eom;
1528  interrupt(
1529  value_set_analysis,
1530  goto_model,
1531  cmdline.get_value("isr"));
1532  }
1533 
1534  // Memory-mapped I/O
1535  if(cmdline.isset("mmio"))
1536  {
1537  log.status() << "Instrumenting memory-mapped I/O" << messaget::eom;
1538  mmio(value_set_analysis, goto_model);
1539  }
1540 
1541  if(cmdline.isset("concurrency"))
1542  {
1543  log.status() << "Sequentializing concurrency" << messaget::eom;
1544  concurrency(value_set_analysis, goto_model);
1545  }
1546  }
1547 
1548  if(cmdline.isset("interval-analysis"))
1549  {
1550  log.status() << "Interval analysis" << messaget::eom;
1552  }
1553 
1554  if(cmdline.isset("havoc-loops"))
1555  {
1556  log.status() << "Havocking loops" << messaget::eom;
1558  }
1559 
1560  if(cmdline.isset("k-induction"))
1561  {
1562  bool base_case=cmdline.isset("base-case");
1563  bool step_case=cmdline.isset("step-case");
1564 
1565  if(step_case && base_case)
1566  throw "please specify only one of --step-case and --base-case";
1567  else if(!step_case && !base_case)
1568  throw "please specify one of --step-case and --base-case";
1569 
1570  unsigned k=unsafe_string2unsigned(cmdline.get_value("k-induction"));
1571 
1572  if(k==0)
1573  throw "please give k>=1";
1574 
1575  log.status() << "Instrumenting k-induction for k=" << k << ", "
1576  << (base_case ? "base case" : "step case") << messaget::eom;
1577 
1578  k_induction(goto_model, base_case, step_case, k);
1579  }
1580 
1581  if(cmdline.isset("function-enter"))
1582  {
1583  log.status() << "Function enter instrumentation" << messaget::eom;
1585  goto_model,
1586  cmdline.get_value("function-enter"));
1587  }
1588 
1589  if(cmdline.isset("function-exit"))
1590  {
1591  log.status() << "Function exit instrumentation" << messaget::eom;
1592  function_exit(
1593  goto_model,
1594  cmdline.get_value("function-exit"));
1595  }
1596 
1597  if(cmdline.isset("branch"))
1598  {
1599  log.status() << "Branch instrumentation" << messaget::eom;
1600  branch(
1601  goto_model,
1602  cmdline.get_value("branch"));
1603  }
1604 
1605  // add failed symbols
1607 
1608  // recalculate numbers, etc.
1610 
1611  // add loop ids
1613 
1614  // label the assertions
1616 
1617  nondet_volatile(goto_model, options);
1618 
1619  // reachability slice?
1620  if(cmdline.isset("reachability-slice"))
1621  {
1623 
1624  log.status() << "Performing a reachability slice" << messaget::eom;
1625 
1626  // reachability_slicer requires that the model has unique location numbers:
1628 
1629  if(cmdline.isset("property"))
1631  else
1633  }
1634 
1635  if(cmdline.isset("fp-reachability-slice"))
1636  {
1638 
1639  log.status() << "Performing a function pointer reachability slice"
1640  << messaget::eom;
1642  goto_model, cmdline.get_comma_separated_values("fp-reachability-slice"));
1643  }
1644 
1645  // full slice?
1646  if(cmdline.isset("full-slice"))
1647  {
1650 
1651  log.status() << "Performing a full slice" << messaget::eom;
1652  if(cmdline.isset("property"))
1654  else
1655  {
1656  // full_slicer requires that the model has unique location numbers:
1659  }
1660  }
1661 
1662  // splice option
1663  if(cmdline.isset("splice-call"))
1664  {
1665  log.status() << "Performing call splicing" << messaget::eom;
1666  std::string callercallee=cmdline.get_value("splice-call");
1667  if(splice_call(
1669  callercallee,
1672  throw 0;
1673  }
1674 
1675  // aggressive slicer
1676  if(cmdline.isset("aggressive-slice"))
1677  {
1679 
1680  // reachability_slicer requires that the model has unique location numbers:
1682 
1683  log.status() << "Slicing away initializations of unused global variables"
1684  << messaget::eom;
1686 
1687  log.status() << "Performing an aggressive slice" << messaget::eom;
1688  aggressive_slicert aggressive_slicer(goto_model, ui_message_handler);
1689 
1690  if(cmdline.isset("aggressive-slice-call-depth"))
1691  aggressive_slicer.call_depth =
1692  safe_string2unsigned(cmdline.get_value("aggressive-slice-call-depth"));
1693 
1694  if(cmdline.isset("aggressive-slice-preserve-function"))
1695  aggressive_slicer.preserve_functions(
1696  cmdline.get_values("aggressive-slice-preserve-function"));
1697 
1698  if(cmdline.isset("property"))
1699  aggressive_slicer.user_specified_properties =
1700  cmdline.get_values("property");
1701 
1702  if(cmdline.isset("aggressive-slice-preserve-functions-containing"))
1703  aggressive_slicer.name_snippets =
1704  cmdline.get_values("aggressive-slice-preserve-functions-containing");
1705 
1706  aggressive_slicer.preserve_all_direct_paths =
1707  cmdline.isset("aggressive-slice-preserve-all-direct-paths");
1708 
1709  aggressive_slicer.doit();
1710 
1712 
1713  log.status() << "Performing a reachability slice" << messaget::eom;
1714  if(cmdline.isset("property"))
1716  else
1718  }
1719 
1720  if(cmdline.isset("ensure-one-backedge-per-target"))
1721  {
1722  log.status() << "Trying to force one backedge per target" << messaget::eom;
1724  }
1725 
1726  // recalculate numbers, etc.
1728 }
1729 
1732 {
1733  // clang-format off
1734  std::cout << '\n' << banner_string("Goto-Instrument", CBMC_VERSION) << '\n'
1735  << align_center_with_border("Copyright (C) 2008-2013") << '\n'
1736  << align_center_with_border("Daniel Kroening") << '\n'
1737  << align_center_with_border("kroening@kroening.com") << '\n'
1738  <<
1739  "\n"
1740  "Usage: Purpose:\n"
1741  "\n"
1742  " goto-instrument [-?] [-h] [--help] show help\n"
1743  " goto-instrument in out perform instrumentation\n"
1744  "\n"
1745  "Main options:\n"
1746  " --document-properties-html generate HTML property documentation\n"
1747  " --document-properties-latex generate Latex property documentation\n"
1748  " --dump-c generate C source\n"
1749  " --dump-c-type-header m generate a C header for types local in m\n"
1750  " --dump-cpp generate C++ source\n"
1751  " --dot generate CFG graph in DOT format\n"
1752  " --interpreter do concrete execution\n"
1753  "\n"
1754  "Diagnosis:\n"
1755  " --show-loops show the loops in the program\n"
1757  " --show-symbol-table show loaded symbol table\n"
1758  " --list-symbols list symbols with type information\n"
1761  " --drop-unused-functions drop functions trivially unreachable from main function\n" // NOLINT(*)
1762  " --print-internal-representation\n" // NOLINTNEXTLINE(*)
1763  " show verbose internal representation of the program\n"
1764  " --list-undefined-functions list functions without body\n"
1765  " --show-struct-alignment show struct members that might be concurrently accessed\n" // NOLINT(*)
1766  " --show-natural-loops show natural loop heads\n"
1767  // NOLINTNEXTLINE(whitespace/line_length)
1768  " --list-calls-args list all function calls with their arguments\n"
1769  " --call-graph show graph of function calls\n"
1770  // NOLINTNEXTLINE(whitespace/line_length)
1771  " --reachable-call-graph show graph of function calls potentially reachable from main function\n"
1773  // NOLINTNEXTLINE(whitespace/line_length)
1774  " --show-threaded show instructions that may be executed by more than one thread\n"
1775  " --show-local-safe-pointers show pointer expressions that are trivially dominated by a not-null check\n" // NOLINT(*)
1776  " --show-safe-dereferences show pointer expressions that are trivially dominated by a not-null check\n" // NOLINT(*)
1777  " *and* used as a dereference operand\n" // NOLINT(*)
1779  // NOLINTNEXTLINE(whitespace/line_length)
1780  " --validate-goto-binary check the well-formedness of the passed in goto\n"
1781  " binary and then exit\n"
1782  "\n"
1783  "Safety checks:\n"
1784  " --no-assertions ignore user assertions\n"
1786  " --uninitialized-check add checks for uninitialized locals (experimental)\n" // NOLINT(*)
1787  " --stack-depth n add check that call stack size of non-inlined functions never exceeds n\n" // NOLINT(*)
1788  " --race-check add floating-point data race checks\n"
1789  "\n"
1790  "Semantic transformations:\n"
1791  << HELP_NONDET_VOLATILE <<
1792  " --unwind <n> unwinds the loops <n> times\n"
1793  " --unwindset L:B,... unwind loop L with a bound of B\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"
1804  " --remove-pointers converts pointer arithmetic to base+offset expressions\n" // NOLINT(*)
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"
1822  " --mm <tso,pso,rmo,power> instruments a weak memory model\n"
1823  " --scc detects critical cycles per SCC (one thread per SCC)\n" // NOLINT(*)
1824  " --one-event-per-cycle only instruments one event per cycle\n"
1825  " --minimum-interference instruments an optimal number of events\n"
1826  " --my-events only instruments events whose ids appear in inst.evt\n" // NOLINT(*)
1827  " --cfg-kill enables symbolic execution used to reduce spurious cycles\n" // NOLINT(*)
1828  " --no-dependencies no dependency analysis\n"
1829  // NOLINTNEXTLINE(whitespace/line_length)
1830  " --no-po-rendering no representation of the threads in the dot\n"
1831  " --render-cluster-file clusterises the dot by files\n"
1832  " --render-cluster-function clusterises the dot by functions\n"
1833  "\n"
1834  "Slicing:\n"
1836  " --full-slice slice away instructions that don't affect assertions\n" // NOLINT(*)
1837  " --property id slice with respect to specific property only\n" // NOLINT(*)
1838  " --slice-global-inits slice away initializations of unused global variables\n" // NOLINT(*)
1839  " --aggressive-slice remove bodies of any functions not on the shortest path between\n" // NOLINT(*)
1840  " the start function and the function containing the property(s)\n" // NOLINT(*)
1841  " --aggressive-slice-call-depth <n>\n"
1842  " used with aggressive-slice, preserves all functions within <n> function calls\n" // NOLINT(*)
1843  " of the functions on the shortest path\n"
1844  " --aggressive-slice-preserve-function <f>\n"
1845  " force the aggressive slicer to preserve function <f>\n" // NOLINT(*)
1846  " --aggressive-slice-preserve-function containing <f>\n"
1847  " force the aggressive slicer to preserve all functions with names containing <f>\n" // NOLINT(*)
1848  "--aggressive-slice-preserve-all-direct-paths \n"
1849  " force aggressive slicer to preserve all direct paths\n" // NOLINT(*)
1850  "\n"
1851  "Further transformations:\n"
1852  " --constant-propagator propagate constants and simplify expressions\n" // NOLINT(*)
1853  " --inline perform full inlining\n"
1854  " --partial-inline perform partial inlining\n"
1855  " --function-inline <function> transitively inline all calls <function> makes\n" // NOLINT(*)
1856  " --no-caching disable caching of intermediate results during transitive function inlining\n" // NOLINT(*)
1857  " --log <file> log in json format which code segments were inlined, use with --function-inline\n" // NOLINT(*)
1858  " --remove-function-pointers replace function pointers by case statement over function calls\n" // NOLINT(*)
1859  " --value-set-fi-fp-removal build flow-insensitive value set and replace function pointers by a case statement\n" // NOLINT(*)
1860  " over the possible assignments. If the set of possible assignments is empty the function pointer\n" // NOLINT(*)
1861  " is removed using the standard remove-function-pointers pass. \n" // NOLINT(*)
1865  " --add-library add models of C library functions\n"
1866  " --model-argc-argv <n> model up to <n> command line arguments\n"
1867  // NOLINTNEXTLINE(whitespace/line_length)
1868  " --remove-function-body <f> remove the implementation of function <f> (may be repeated)\n"
1870  "\n"
1871  "Function contracts and invariants:\n"
1876  "\n"
1877  "Other options:\n"
1878  " --no-system-headers with --dump-c/--dump-cpp: generate C source expanding libc includes\n" // NOLINT(*)
1879  " --use-all-headers with --dump-c/--dump-cpp: generate C source with all includes\n" // NOLINT(*)
1880  " --harness with --dump-c/--dump-cpp: include input generator in output\n" // NOLINT(*)
1881  " --version show version and exit\n"
1882  HELP_FLUSH
1883  " --xml-ui use XML-formatted output\n"
1884  " --json-ui use JSON-formatted output\n"
1886  "\n";
1887  // clang-format on
1888 }
cprover_library.h
cmdlinet::args
argst args
Definition: cmdline.h:143
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:186
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:202
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:70
rewrite_union.h
Symbolic Execution.
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:91
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:214
print_global_state_size
void print_global_state_size(const goto_modelt &goto_model)
Definition: count_eloc.cpp:158
goto_instrument_parse_optionst::do_remove_returns
void do_remove_returns()
Definition: goto_instrument_parse_options.cpp:973
goto_instrument_parse_optionst::help
virtual void help()
display command line help
Definition: goto_instrument_parse_options.cpp:1731
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:44
RMO
@ RMO
Definition: wmm.h:22
goto_instrument_parse_optionst::do_partial_inlining
void do_partial_inlining()
Definition: goto_instrument_parse_options.cpp:959
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:158
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:106
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:353
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:86
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:218
local_safe_pointerst
A very simple, cheap analysis to determine when dereference operations are trivially guarded by a che...
Definition: local_safe_pointers.h:27
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
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:14
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:370
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:725
interpreter.h
Interpreter for GOTO Programs.
show_uninitialized
void show_uninitialized(const goto_modelt &goto_model, std::ostream &out)
Definition: uninitialized.cpp:208
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:198
ait
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition: ai.h:559
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:942
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:512
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:191
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:2338
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:200
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:197
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:80
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.
string_abstraction
void string_abstraction(symbol_tablet &symbol_table, message_handlert &message_handler, goto_functionst &dest)
Definition: string_abstraction.cpp:69
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:1077
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:440
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:336
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:989
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:141
split_string
void split_string(const std::string &s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)
Definition: string_utils.cpp:39
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:232
full_slicer
void full_slicer(goto_functionst &goto_functions, const namespacet &ns, const slicing_criteriont &criterion)
Definition: full_slicer.cpp:347
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:111
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:120
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:42
all_loops
@ all_loops
Definition: wmm.h:39
unwindsett
Definition: unwindset.h:23
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:922
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:984
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:1577
undefined_function_abort_path
void undefined_function_abort_path(goto_modelt &goto_model)
Definition: undefined_functions.cpp:35
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:371
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:370
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:269
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:1001
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:1612
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:34
remove_function.h
Remove function definition.
rewrite_union
void rewrite_union(exprt &expr)
We rewrite u.c for unions u into byte_extract(u, 0), and { .c = v } into byte_update(NIL,...
Definition: rewrite_union.cpp:66
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:149
HELP_REMOVE_CONST_FUNCTION_POINTERS
#define HELP_REMOVE_CONST_FUNCTION_POINTERS
Definition: remove_const_function_pointers.h:112
count_eloc
void count_eloc(const goto_modelt &goto_model)
Definition: count_eloc.cpp:54
accelerate.h
Loop Acceleration.
configt::ansi_ct::arch
irep_idt arch
Definition: config.h:165
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:196
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:73
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:452
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:1229
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:353
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:413
full_slicer.h
Slicing.
goto_instrument_parse_optionst::partial_inlining_done
bool partial_inlining_done
Definition: goto_instrument_parse_options.h:159
HELP_REPLACE_ALL_CALLS
#define HELP_REPLACE_ALL_CALLS
Definition: code_contracts.h:192
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:104
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:401
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:160
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
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:187
HELP_GOTO_CHECK
#define HELP_GOTO_CHECK
Definition: goto_check.h:49
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:41
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:797
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:257
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:511
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:74
grapht::output_dot
void output_dot(std::ostream &out) const
Definition: graph.h:962
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:769
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
unwindsett::parse_unwindset
void parse_unwindset(const std::list< std::string > &unwindset)
Definition: unwindset.cpp:57
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.
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:386
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:910
goto_instrument_parse_optionst::goto_model
goto_modelt goto_model
Definition: goto_instrument_parse_options.h:162
model_argc_argv.h
Initialize command line arguments.
function_exit
void function_exit(goto_modelt &goto_model, const irep_idt &id)
Definition: function.cpp:98
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:364
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:68
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:524
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:459
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:26
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:204
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:85
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:404
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:1590
forall_goto_program_instructions
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:1180
interval_analysis.h
Interval Analysis.
HELP_ENFORCE_ALL_CONTRACTS
#define HELP_ENFORCE_ALL_CONTRACTS
Definition: code_contracts.h:201
list_calls_and_arguments
static void list_calls_and_arguments(const namespacet &ns, const goto_programt &goto_program)
Definition: call_sequences.cpp:271
validation_modet::INVARIANT
@ INVARIANT
dependence_graph.h
Field-Sensitive Program Dependence Analysis, Litvak et al., FSE 2010.
FLAG_REPLACE_CALL
#define FLAG_REPLACE_CALL
Definition: code_contracts.h:186
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:21
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