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 
33 #include <goto-programs/loop_ids.h>
50 
55 
56 #include <analyses/call_graph.h>
64 #include <analyses/is_threaded.h>
65 #include <analyses/lexical_loops.h>
68 #include <analyses/natural_loops.h>
70 #include <analyses/sese_regions.h>
71 
72 #include <ansi-c/ansi_c_language.h>
74 #include <ansi-c/cprover_library.h>
75 
76 #include <assembler/remove_asm.h>
77 
78 #include <cpp/cprover_library.h>
79 
80 #include "accelerate/accelerate.h"
81 #include "alignment_checks.h"
82 #include "branch.h"
83 #include "call_sequences.h"
84 #include "code_contracts.h"
85 #include "concurrency.h"
86 #include "document_properties.h"
87 #include "dot.h"
88 #include "dump_c.h"
89 #include "full_slicer.h"
90 #include "function.h"
91 #include "havoc_loops.h"
92 #include "horn_encoding.h"
94 #include "interrupt.h"
95 #include "k_induction.h"
96 #include "mmio.h"
97 #include "model_argc_argv.h"
98 #include "nondet_static.h"
99 #include "nondet_volatile.h"
100 #include "points_to.h"
101 #include "race_check.h"
102 #include "reachability_slicer.h"
103 #include "remove_function.h"
104 #include "rw_set.h"
105 #include "show_locations.h"
106 #include "skip_loops.h"
107 #include "splice_call.h"
108 #include "stack_depth.h"
109 #include "thread_instrumentation.h"
110 #include "undefined_functions.h"
111 #include "uninitialized.h"
112 #include "unwind.h"
113 #include "wmm/weak_memory.h"
114 
117 {
118  if(cmdline.isset("version"))
119  {
120  std::cout << CBMC_VERSION << '\n';
121  return CPROVER_EXIT_SUCCESS;
122  }
123 
124  if(cmdline.args.size()!=1 && cmdline.args.size()!=2)
125  {
126  help();
128  }
129 
132 
133  {
135 
137 
138  {
139  const bool validate_only = cmdline.isset("validate-goto-binary");
140 
141  if(validate_only || cmdline.isset("validate-goto-model"))
142  {
144 
145  if(validate_only)
146  {
147  return CPROVER_EXIT_SUCCESS;
148  }
149  }
150  }
151 
153 
154  if(cmdline.isset("validate-goto-model"))
155  {
157  }
158 
159  {
160  bool unwind_given=cmdline.isset("unwind");
161  bool unwindset_given=cmdline.isset("unwindset");
162  bool unwindset_file_given=cmdline.isset("unwindset-file");
163 
164  if(unwindset_given && unwindset_file_given)
165  throw "only one of --unwindset and --unwindset-file supported at a "
166  "time";
167 
168  if(unwind_given || unwindset_given || unwindset_file_given)
169  {
170  unwindsett unwindset;
171 
172  if(unwind_given)
173  unwindset.parse_unwind(cmdline.get_value("unwind"));
174 
175  if(unwindset_file_given)
176  unwindset.parse_unwindset_file(cmdline.get_value("unwindset-file"));
177 
178  if(unwindset_given)
179  unwindset.parse_unwindset(cmdline.get_values("unwindset"));
180 
181  bool unwinding_assertions=cmdline.isset("unwinding-assertions");
182  bool partial_loops=cmdline.isset("partial-loops");
183  bool continue_as_loops=cmdline.isset("continue-as-loops");
184 
185  if(unwinding_assertions+partial_loops+continue_as_loops>1)
186  throw "more than one of --unwinding-assertions,--partial-loops,"
187  "--continue-as-loops selected";
188 
189  goto_unwindt::unwind_strategyt unwind_strategy=
191 
192  if(unwinding_assertions)
193  {
195  }
196  else if(partial_loops)
197  {
199  }
200  else if(continue_as_loops)
201  {
203  }
204 
205  goto_unwindt goto_unwind;
206  goto_unwind(goto_model, unwindset, unwind_strategy);
207 
208  if(cmdline.isset("log"))
209  {
210  std::string filename=cmdline.get_value("log");
211  bool have_file=!filename.empty() && filename!="-";
212 
213  jsont result=goto_unwind.output_log_json();
214 
215  if(have_file)
216  {
217 #ifdef _MSC_VER
218  std::ofstream of(widen(filename));
219 #else
220  std::ofstream of(filename);
221 #endif
222  if(!of)
223  throw "failed to open file "+filename;
224 
225  of << result;
226  of.close();
227  }
228  else
229  {
230  std::cout << result << '\n';
231  }
232  }
233 
234  // goto_unwind holds references to instructions, only do remove_skip
235  // after having generated the log above
237  }
238  }
239 
240  if(cmdline.isset("show-threaded"))
241  {
243 
244  is_threadedt is_threaded(goto_model);
245 
247  {
248  std::cout << "////\n";
249  std::cout << "//// Function: " << f_it->first << '\n';
250  std::cout << "////\n\n";
251 
252  const goto_programt &goto_program=f_it->second.body;
253 
254  forall_goto_program_instructions(i_it, goto_program)
255  {
256  goto_program.output_instruction(ns, f_it->first, std::cout, *i_it);
257  std::cout << "Is threaded: " << (is_threaded(i_it)?"True":"False")
258  << "\n\n";
259  }
260  }
261 
262  return CPROVER_EXIT_SUCCESS;
263  }
264 
265  if(cmdline.isset("insert-final-assert-false"))
266  {
267  log.status() << "Inserting final assert false" << messaget::eom;
268  bool fail = insert_final_assert_false(
269  goto_model,
270  cmdline.get_value("insert-final-assert-false"),
272  if(fail)
273  {
275  }
276  // otherwise, fall-through to write new binary
277  }
278 
279  if(cmdline.isset("show-value-sets"))
280  {
282 
283  // recalculate numbers, etc.
285 
286  log.status() << "Pointer Analysis" << messaget::eom;
288  value_set_analysist value_set_analysis(ns);
289  value_set_analysis(goto_model.goto_functions);
291  ui_message_handler.get_ui(), goto_model, value_set_analysis);
292  return CPROVER_EXIT_SUCCESS;
293  }
294 
295  if(cmdline.isset("show-global-may-alias"))
296  {
300 
301  // recalculate numbers, etc.
303 
304  global_may_alias_analysist global_may_alias_analysis;
305  global_may_alias_analysis(goto_model);
306  global_may_alias_analysis.output(goto_model, std::cout);
307 
308  return CPROVER_EXIT_SUCCESS;
309  }
310 
311  if(cmdline.isset("show-local-bitvector-analysis"))
312  {
315 
316  // recalculate numbers, etc.
318 
320 
322  {
323  local_bitvector_analysist local_bitvector_analysis(it->second, ns);
324  std::cout << ">>>>\n";
325  std::cout << ">>>> " << it->first << '\n';
326  std::cout << ">>>>\n";
327  local_bitvector_analysis.output(std::cout, it->second, ns);
328  std::cout << '\n';
329  }
330 
331  return CPROVER_EXIT_SUCCESS;
332  }
333 
334  if(cmdline.isset("show-local-safe-pointers") ||
335  cmdline.isset("show-safe-dereferences"))
336  {
337  // Ensure location numbering is unique:
339 
341 
343  {
344  local_safe_pointerst local_safe_pointers;
345  local_safe_pointers(it->second.body);
346  std::cout << ">>>>\n";
347  std::cout << ">>>> " << it->first << '\n';
348  std::cout << ">>>>\n";
349  if(cmdline.isset("show-local-safe-pointers"))
350  local_safe_pointers.output(std::cout, it->second.body, ns);
351  else
352  {
353  local_safe_pointers.output_safe_dereferences(
354  std::cout, it->second.body, ns);
355  }
356  std::cout << '\n';
357  }
358 
359  return CPROVER_EXIT_SUCCESS;
360  }
361 
362  if(cmdline.isset("show-sese-regions"))
363  {
364  // Ensure location numbering is unique:
366 
368 
370  {
371  sese_region_analysist sese_region_analysis;
372  sese_region_analysis(it->second.body);
373  std::cout << ">>>>\n";
374  std::cout << ">>>> " << it->first << '\n';
375  std::cout << ">>>>\n";
376  sese_region_analysis.output(std::cout, it->second.body, ns);
377  std::cout << '\n';
378  }
379 
380  return CPROVER_EXIT_SUCCESS;
381  }
382 
383  if(cmdline.isset("show-custom-bitvector-analysis"))
384  {
388 
390 
391  if(!cmdline.isset("inline"))
392  {
395  }
396 
397  // recalculate numbers, etc.
399 
400  custom_bitvector_analysist custom_bitvector_analysis;
401  custom_bitvector_analysis(goto_model);
402  custom_bitvector_analysis.output(goto_model, std::cout);
403 
404  return CPROVER_EXIT_SUCCESS;
405  }
406 
407  if(cmdline.isset("show-escape-analysis"))
408  {
412 
413  // recalculate numbers, etc.
415 
416  escape_analysist escape_analysis;
417  escape_analysis(goto_model);
418  escape_analysis.output(goto_model, std::cout);
419 
420  return CPROVER_EXIT_SUCCESS;
421  }
422 
423  if(cmdline.isset("custom-bitvector-analysis"))
424  {
428 
430 
431  if(!cmdline.isset("inline"))
432  {
435  }
436 
437  // recalculate numbers, etc.
439 
441 
442  custom_bitvector_analysist custom_bitvector_analysis;
443  custom_bitvector_analysis(goto_model);
444  custom_bitvector_analysis.check(
445  goto_model,
446  cmdline.isset("xml-ui"),
447  std::cout);
448 
449  return CPROVER_EXIT_SUCCESS;
450  }
451 
452  if(cmdline.isset("show-points-to"))
453  {
455 
456  // recalculate numbers, etc.
458 
460 
461  log.status() << "Pointer Analysis" << messaget::eom;
462  points_tot points_to;
463  points_to(goto_model);
464  points_to.output(std::cout);
465  return CPROVER_EXIT_SUCCESS;
466  }
467 
468  if(cmdline.isset("show-intervals"))
469  {
471 
472  // recalculate numbers, etc.
474 
475  log.status() << "Interval Analysis" << messaget::eom;
479  interval_analysis.output(goto_model, std::cout);
480  return CPROVER_EXIT_SUCCESS;
481  }
482 
483  if(cmdline.isset("show-call-sequences"))
484  {
487  return CPROVER_EXIT_SUCCESS;
488  }
489 
490  if(cmdline.isset("check-call-sequence"))
491  {
494  return CPROVER_EXIT_SUCCESS;
495  }
496 
497  if(cmdline.isset("list-calls-args"))
498  {
500 
502 
503  return CPROVER_EXIT_SUCCESS;
504  }
505 
506  if(cmdline.isset("show-rw-set"))
507  {
509 
510  if(!cmdline.isset("inline"))
511  {
513 
514  // recalculate numbers, etc.
516  }
517 
518  log.status() << "Pointer Analysis" << messaget::eom;
519  value_set_analysist value_set_analysis(ns);
520  value_set_analysis(goto_model.goto_functions);
521 
522  const symbolt &symbol=ns.lookup(ID_main);
523  symbol_exprt main(symbol.name, symbol.type);
524 
525  std::cout <<
526  rw_set_functiont(value_set_analysis, goto_model, main);
527  return CPROVER_EXIT_SUCCESS;
528  }
529 
530  if(cmdline.isset("show-symbol-table"))
531  {
533  return CPROVER_EXIT_SUCCESS;
534  }
535 
536  if(cmdline.isset("show-reaching-definitions"))
537  {
539 
541  reaching_definitions_analysist rd_analysis(ns);
542  rd_analysis(goto_model);
543  rd_analysis.output(goto_model, std::cout);
544 
545  return CPROVER_EXIT_SUCCESS;
546  }
547 
548  if(cmdline.isset("show-dependence-graph"))
549  {
551 
553  dependence_grapht dependence_graph(ns);
554  dependence_graph(goto_model);
555  dependence_graph.output(goto_model, std::cout);
556  dependence_graph.output_dot(std::cout);
557 
558  return CPROVER_EXIT_SUCCESS;
559  }
560 
561  if(cmdline.isset("count-eloc"))
562  {
564  return CPROVER_EXIT_SUCCESS;
565  }
566 
567  if(cmdline.isset("list-eloc"))
568  {
570  return CPROVER_EXIT_SUCCESS;
571  }
572 
573  if(cmdline.isset("print-path-lengths"))
574  {
576  return CPROVER_EXIT_SUCCESS;
577  }
578 
579  if(cmdline.isset("print-global-state-size"))
580  {
582  return CPROVER_EXIT_SUCCESS;
583  }
584 
585  if(cmdline.isset("list-symbols"))
586  {
588  return CPROVER_EXIT_SUCCESS;
589  }
590 
591  if(cmdline.isset("show-uninitialized"))
592  {
593  show_uninitialized(goto_model, std::cout);
594  return CPROVER_EXIT_SUCCESS;
595  }
596 
597  if(cmdline.isset("interpreter"))
598  {
599  log.status() << "Starting interpreter" << messaget::eom;
601  return CPROVER_EXIT_SUCCESS;
602  }
603 
604  if(cmdline.isset("show-claims") ||
605  cmdline.isset("show-properties"))
606  {
609  return CPROVER_EXIT_SUCCESS;
610  }
611 
612  if(cmdline.isset("document-claims-html") ||
613  cmdline.isset("document-properties-html"))
614  {
616  return CPROVER_EXIT_SUCCESS;
617  }
618 
619  if(cmdline.isset("document-claims-latex") ||
620  cmdline.isset("document-properties-latex"))
621  {
623  return CPROVER_EXIT_SUCCESS;
624  }
625 
626  if(cmdline.isset("show-loops"))
627  {
629  return CPROVER_EXIT_SUCCESS;
630  }
631 
632  if(cmdline.isset("show-natural-loops"))
633  {
634  show_natural_loops(goto_model, std::cout);
635  return CPROVER_EXIT_SUCCESS;
636  }
637 
638  if(cmdline.isset("show-lexical-loops"))
639  {
640  show_lexical_loops(goto_model, std::cout);
641  }
642 
643  if(cmdline.isset("print-internal-representation"))
644  {
645  for(auto const &pair : goto_model.goto_functions.function_map)
646  for(auto const &ins : pair.second.body.instructions)
647  {
648  if(ins.code.is_not_nil())
649  log.status() << ins.code.pretty() << messaget::eom;
650  if(ins.has_condition())
651  {
652  log.status() << "[guard] " << ins.get_condition().pretty()
653  << messaget::eom;
654  }
655  }
656  return CPROVER_EXIT_SUCCESS;
657  }
658 
659  if(
660  cmdline.isset("show-goto-functions") ||
661  cmdline.isset("list-goto-functions"))
662  {
664  goto_model, ui_message_handler, cmdline.isset("list-goto-functions"));
665  return CPROVER_EXIT_SUCCESS;
666  }
667 
668  if(cmdline.isset("list-undefined-functions"))
669  {
671  return CPROVER_EXIT_SUCCESS;
672  }
673 
674  // experimental: print structs
675  if(cmdline.isset("show-struct-alignment"))
676  {
678  return CPROVER_EXIT_SUCCESS;
679  }
680 
681  if(cmdline.isset("show-locations"))
682  {
684  return CPROVER_EXIT_SUCCESS;
685  }
686 
687  if(
688  cmdline.isset("dump-c") || cmdline.isset("dump-cpp") ||
689  cmdline.isset("dump-c-type-header"))
690  {
691  const bool is_cpp=cmdline.isset("dump-cpp");
692  const bool is_header = cmdline.isset("dump-c-type-header");
693  const bool h_libc=!cmdline.isset("no-system-headers");
694  const bool h_all=cmdline.isset("use-all-headers");
695  const bool harness=cmdline.isset("harness");
697 
698  // restore RETURN instructions in case remove_returns had been
699  // applied
701 
702  // dump_c (actually goto_program2code) requires valid instruction
703  // location numbers:
705 
706  if(cmdline.args.size()==2)
707  {
708  #ifdef _MSC_VER
709  std::ofstream out(widen(cmdline.args[1]));
710  #else
711  std::ofstream out(cmdline.args[1]);
712  #endif
713  if(!out)
714  {
715  log.error() << "failed to write to '" << cmdline.args[1] << "'";
717  }
718  if(is_header)
719  {
722  h_libc,
723  h_all,
724  harness,
725  ns,
726  cmdline.get_value("dump-c-type-header"),
727  out);
728  }
729  else
730  {
731  (is_cpp ? dump_cpp : dump_c)(
732  goto_model.goto_functions, h_libc, h_all, harness, ns, out);
733  }
734  }
735  else
736  {
737  if(is_header)
738  {
741  h_libc,
742  h_all,
743  harness,
744  ns,
745  cmdline.get_value("dump-c-type-header"),
746  std::cout);
747  }
748  else
749  {
750  (is_cpp ? dump_cpp : dump_c)(
751  goto_model.goto_functions, h_libc, h_all, harness, ns, std::cout);
752  }
753  }
754 
755  return CPROVER_EXIT_SUCCESS;
756  }
757 
758  if(cmdline.isset("call-graph"))
759  {
761  call_grapht call_graph(goto_model);
762 
763  if(cmdline.isset("xml"))
764  call_graph.output_xml(std::cout);
765  else if(cmdline.isset("dot"))
766  call_graph.output_dot(std::cout);
767  else
768  call_graph.output(std::cout);
769 
770  return CPROVER_EXIT_SUCCESS;
771  }
772 
773  if(cmdline.isset("reachable-call-graph"))
774  {
776  call_grapht call_graph =
779  if(cmdline.isset("xml"))
780  call_graph.output_xml(std::cout);
781  else if(cmdline.isset("dot"))
782  call_graph.output_dot(std::cout);
783  else
784  call_graph.output(std::cout);
785 
786  return 0;
787  }
788 
789  if(cmdline.isset("show-class-hierarchy"))
790  {
791  class_hierarchyt hierarchy;
792  hierarchy(goto_model.symbol_table);
793  if(cmdline.isset("dot"))
794  hierarchy.output_dot(std::cout);
795  else
797 
798  return CPROVER_EXIT_SUCCESS;
799  }
800 
801  if(cmdline.isset("dot"))
802  {
804 
805  if(cmdline.args.size()==2)
806  {
807  #ifdef _MSC_VER
808  std::ofstream out(widen(cmdline.args[1]));
809  #else
810  std::ofstream out(cmdline.args[1]);
811  #endif
812  if(!out)
813  {
814  log.error() << "failed to write to " << cmdline.args[1] << "'";
816  }
817 
818  dot(goto_model, out);
819  }
820  else
821  dot(goto_model, std::cout);
822 
823  return CPROVER_EXIT_SUCCESS;
824  }
825 
826  if(cmdline.isset("accelerate"))
827  {
829 
831 
832  log.status() << "Performing full inlining" << messaget::eom;
834 
835  log.status() << "Removing calls to functions without a body"
836  << messaget::eom;
837  remove_calls_no_bodyt remove_calls_no_body;
838  remove_calls_no_body(goto_model.goto_functions);
839 
840  log.status() << "Accelerating" << messaget::eom;
841  guard_managert guard_manager;
843  goto_model, ui_message_handler, cmdline.isset("z3"), guard_manager);
845  }
846 
847  if(cmdline.isset("horn-encoding"))
848  {
849  log.status() << "Horn-clause encoding" << messaget::eom;
851 
852  if(cmdline.args.size()==2)
853  {
854  #ifdef _MSC_VER
855  std::ofstream out(widen(cmdline.args[1]));
856  #else
857  std::ofstream out(cmdline.args[1]);
858  #endif
859 
860  if(!out)
861  {
862  log.error() << "Failed to open output file " << cmdline.args[1]
863  << messaget::eom;
865  }
866 
868  }
869  else
870  horn_encoding(goto_model, std::cout);
871 
872  return CPROVER_EXIT_SUCCESS;
873  }
874 
875  if(cmdline.isset("drop-unused-functions"))
876  {
878 
879  log.status() << "Removing unused functions" << messaget::eom;
881  }
882 
883  if(cmdline.isset("undefined-function-is-assume-false"))
884  {
887  }
888 
889  // write new binary?
890  if(cmdline.args.size()==2)
891  {
892  log.status() << "Writing GOTO program to '" << cmdline.args[1] << "'"
893  << messaget::eom;
894 
897  else
898  return CPROVER_EXIT_SUCCESS;
899  }
900  else if(cmdline.args.size() < 2)
901  {
903  "Invalid number of positional arguments passed",
904  "[in] [out]",
905  "goto-instrument needs one input and one output file, aside from other "
906  "flags");
907  }
908 
909  help();
911  }
912 // NOLINTNEXTLINE(readability/fn_size)
913 }
914 
916  bool force)
917 {
918  if(function_pointer_removal_done && !force)
919  return;
920 
922 
923  log.status() << "Function Pointer Removal" << messaget::eom;
925  ui_message_handler, goto_model, cmdline.isset("pointer-check"));
926  log.status() << "Virtual function removal" << messaget::eom;
928  log.status() << "Cleaning inline assembler statements" << messaget::eom;
930 }
931 
936 {
937  // Don't bother if we've already done a full function pointer
938  // removal.
940  {
941  return;
942  }
943 
944  log.status() << "Removing const function pointers only" << messaget::eom;
947  goto_model,
948  cmdline.isset("pointer-check"),
949  true); // abort if we can't resolve via const pointers
950 }
951 
953 {
955  return;
956 
958 
959  if(!cmdline.isset("inline"))
960  {
961  log.status() << "Partial Inlining" << messaget::eom;
963  }
964 }
965 
967 {
969  return;
970 
971  remove_returns_done=true;
972 
973  log.status() << "Removing returns" << messaget::eom;
975 }
976 
978 {
979  log.status() << "Reading GOTO program from '" << cmdline.args[0] << "'"
980  << messaget::eom;
981 
982  config.set(cmdline);
983 
984  auto result = read_goto_binary(cmdline.args[0], ui_message_handler);
985 
986  if(!result.has_value())
987  throw 0;
988 
989  goto_model = std::move(result.value());
990 
992 }
993 
995 {
996  optionst options;
997 
998  // disable simplify when adding various checks?
999  if(cmdline.isset("no-simplify"))
1000  options.set_option("simplify", false);
1001  else
1002  options.set_option("simplify", true);
1003 
1004  // use assumptions instead of assertions?
1005  if(cmdline.isset("assert-to-assume"))
1006  options.set_option("assert-to-assume", true);
1007  else
1008  options.set_option("assert-to-assume", false);
1009 
1010  // all checks supported by goto_check
1012 
1013  // check assertions
1014  if(cmdline.isset("no-assertions"))
1015  options.set_option("assertions", false);
1016  else
1017  options.set_option("assertions", true);
1018 
1019  // use assumptions
1020  if(cmdline.isset("no-assumptions"))
1021  options.set_option("assumptions", false);
1022  else
1023  options.set_option("assumptions", true);
1024 
1025  // magic error label
1026  if(cmdline.isset("error-label"))
1027  options.set_option("error-label", cmdline.get_value("error-label"));
1028 
1029  // unwind loops
1030  if(cmdline.isset("unwind"))
1031  {
1032  log.status() << "Unwinding loops" << messaget::eom;
1033  options.set_option("unwind", cmdline.get_value("unwind"));
1034  }
1035 
1036  // skip over selected loops
1037  if(cmdline.isset("skip-loops"))
1038  {
1039  log.status() << "Adding gotos to skip loops" << messaget::eom;
1040  if(skip_loops(
1042  throw 0;
1043  }
1044 
1046 
1047  // initialize argv with valid pointers
1048  if(cmdline.isset("model-argc-argv"))
1049  {
1050  unsigned max_argc=
1051  safe_string2unsigned(cmdline.get_value("model-argc-argv"));
1052 
1053  log.status() << "Adding up to " << max_argc << " command line arguments"
1054  << messaget::eom;
1056  throw 0;
1057  }
1058 
1059  if(cmdline.isset("remove-function-body"))
1060  {
1062  goto_model,
1063  cmdline.get_values("remove-function-body"),
1065  }
1066 
1067  // we add the library in some cases, as some analyses benefit
1068 
1069  if(cmdline.isset("add-library") ||
1070  cmdline.isset("mm"))
1071  {
1072  if(cmdline.isset("show-custom-bitvector-analysis") ||
1073  cmdline.isset("custom-bitvector-analysis"))
1074  {
1075  config.ansi_c.defines.push_back(
1076  std::string(CPROVER_PREFIX) + "CUSTOM_BITVECTOR_ANALYSIS");
1077  }
1078 
1079  // add the library
1080  log.status() << "Adding CPROVER library (" << config.ansi_c.arch << ")"
1081  << messaget::eom;
1085  }
1086 
1087  // now do full inlining, if requested
1088  if(cmdline.isset("inline"))
1089  {
1091 
1092  if(cmdline.isset("show-custom-bitvector-analysis") ||
1093  cmdline.isset("custom-bitvector-analysis"))
1094  {
1098  }
1099 
1100  log.status() << "Performing full inlining" << messaget::eom;
1102  }
1103 
1104  if(cmdline.isset("show-custom-bitvector-analysis") ||
1105  cmdline.isset("custom-bitvector-analysis"))
1106  {
1107  log.status() << "Propagating Constants" << messaget::eom;
1108  constant_propagator_ait constant_propagator_ai(goto_model);
1110  }
1111 
1112  if(cmdline.isset("escape-analysis"))
1113  {
1117 
1118  // recalculate numbers, etc.
1120 
1121  log.status() << "Escape Analysis" << messaget::eom;
1122  escape_analysist escape_analysis;
1123  escape_analysis(goto_model);
1124  escape_analysis.instrument(goto_model);
1125 
1126  // inline added functions, they are often small
1128 
1129  // recalculate numbers, etc.
1131  }
1132 
1133  // verify and set invariants and pre/post-condition pairs
1134  if(cmdline.isset("apply-code-contracts"))
1135  {
1136  log.status() << "Applying Code Contracts" << messaget::eom;
1138  }
1139 
1140  // replace function pointers, if explicitly requested
1141  if(cmdline.isset("remove-function-pointers"))
1142  {
1144  }
1145  else if(cmdline.isset("remove-const-function-pointers"))
1146  {
1148  }
1149 
1150  if(cmdline.isset("replace-calls"))
1151  {
1153 
1154  replace_callst replace_calls;
1155  replace_calls(goto_model, cmdline.get_values("replace-calls"));
1156  }
1157 
1158  if(cmdline.isset("function-inline"))
1159  {
1160  std::string function=cmdline.get_value("function-inline");
1161  PRECONDITION(!function.empty());
1162 
1163  bool caching=!cmdline.isset("no-caching");
1164 
1166 
1167  log.status() << "Inlining calls of function '" << function << "'"
1168  << messaget::eom;
1169 
1170  if(!cmdline.isset("log"))
1171  {
1173  goto_model, function, ui_message_handler, true, caching);
1174  }
1175  else
1176  {
1177  std::string filename=cmdline.get_value("log");
1178  bool have_file=!filename.empty() && filename!="-";
1179 
1181  goto_model, function, ui_message_handler, true, caching);
1182 
1183  if(have_file)
1184  {
1185 #ifdef _MSC_VER
1186  std::ofstream of(widen(filename));
1187 #else
1188  std::ofstream of(filename);
1189 #endif
1190  if(!of)
1191  throw "failed to open file "+filename;
1192 
1193  of << result;
1194  of.close();
1195  }
1196  else
1197  {
1198  std::cout << result << '\n';
1199  }
1200  }
1201 
1204  }
1205 
1206  if(cmdline.isset("partial-inline"))
1207  {
1209 
1210  log.status() << "Partial inlining" << messaget::eom;
1212 
1215  }
1216 
1217  if(cmdline.isset("remove-calls-no-body"))
1218  {
1219  log.status() << "Removing calls to functions without a body"
1220  << messaget::eom;
1221 
1222  remove_calls_no_bodyt remove_calls_no_body;
1223  remove_calls_no_body(goto_model.goto_functions);
1224 
1227  }
1228 
1229  if(cmdline.isset("constant-propagator"))
1230  {
1232 
1233  log.status() << "Propagating Constants" << messaget::eom;
1234 
1235  constant_propagator_ait constant_propagator_ai(goto_model);
1237  }
1238 
1239  if(cmdline.isset("generate-function-body"))
1240  {
1241  optionst c_object_factory_options;
1242  parse_c_object_factory_options(cmdline, c_object_factory_options);
1243  c_object_factory_parameterst object_factory_parameters(
1244  c_object_factory_options);
1245 
1246  auto generate_implementation = generate_function_bodies_factory(
1247  cmdline.get_value("generate-function-body-options"),
1248  object_factory_parameters,
1252  std::regex(cmdline.get_value("generate-function-body")),
1253  *generate_implementation,
1254  goto_model,
1256  }
1257 
1258  if(cmdline.isset("generate-havocing-body"))
1259  {
1260  optionst c_object_factory_options;
1261  parse_c_object_factory_options(cmdline, c_object_factory_options);
1262  c_object_factory_parameterst object_factory_parameters(
1263  c_object_factory_options);
1264 
1265  auto options_split =
1266  split_string(cmdline.get_value("generate-havocing-body"), ',');
1267  if(options_split.size() < 2)
1269  "not enough arguments for this option", "--generate-havocing-body"};
1270 
1271  if(options_split.size() == 2)
1272  {
1273  auto generate_implementation = generate_function_bodies_factory(
1274  std::string{"havoc,"} + options_split.back(),
1275  object_factory_parameters,
1279  std::regex(options_split[0]),
1280  *generate_implementation,
1281  goto_model,
1283  }
1284  else
1285  {
1286  CHECK_RETURN(options_split.size() % 2 == 1);
1287  for(size_t i = 1; i + 1 < options_split.size(); i += 2)
1288  {
1289  auto generate_implementation = generate_function_bodies_factory(
1290  std::string{"havoc,"} + options_split[i + 1],
1291  object_factory_parameters,
1295  options_split[0],
1296  options_split[i],
1297  *generate_implementation,
1298  goto_model,
1300  }
1301  }
1302  }
1303 
1304  // add generic checks, if needed
1305  goto_check(options, goto_model);
1306 
1307  // check for uninitalized local variables
1308  if(cmdline.isset("uninitialized-check"))
1309  {
1310  log.status() << "Adding checks for uninitialized local variables"
1311  << messaget::eom;
1313  }
1314 
1315  // check for maximum call stack size
1316  if(cmdline.isset("stack-depth"))
1317  {
1318  log.status() << "Adding check for maximum call stack size" << messaget::eom;
1319  stack_depth(
1320  goto_model,
1321  safe_string2size_t(cmdline.get_value("stack-depth")));
1322  }
1323 
1324  // ignore default/user-specified initialization of variables with static
1325  // lifetime
1326  if(cmdline.isset("nondet-static-exclude"))
1327  {
1328  log.status() << "Adding nondeterministic initialization "
1329  "of static/global variables except for "
1330  "the specified ones."
1331  << messaget::eom;
1332 
1333  nondet_static(goto_model, cmdline.get_values("nondet-static-exclude"));
1334  }
1335  else if(cmdline.isset("nondet-static"))
1336  {
1337  log.status() << "Adding nondeterministic initialization "
1338  "of static/global variables"
1339  << messaget::eom;
1341  }
1342 
1343  if(cmdline.isset("slice-global-inits"))
1344  {
1345  log.status() << "Slicing away initializations of unused global variables"
1346  << messaget::eom;
1348  }
1349 
1350  if(cmdline.isset("string-abstraction"))
1351  {
1354 
1355  log.status() << "String Abstraction" << messaget::eom;
1357  }
1358 
1359  // some analyses require function pointer removal and partial inlining
1360 
1361  if(cmdline.isset("remove-pointers") ||
1362  cmdline.isset("race-check") ||
1363  cmdline.isset("mm") ||
1364  cmdline.isset("isr") ||
1365  cmdline.isset("concurrency"))
1366  {
1368 
1369  log.status() << "Pointer Analysis" << messaget::eom;
1370  value_set_analysist value_set_analysis(ns);
1371  value_set_analysis(goto_model.goto_functions);
1372 
1373  if(cmdline.isset("remove-pointers"))
1374  {
1375  // removing pointers
1376  log.status() << "Removing Pointers" << messaget::eom;
1377  remove_pointers(goto_model, value_set_analysis);
1378  }
1379 
1380  if(cmdline.isset("race-check"))
1381  {
1382  log.status() << "Adding Race Checks" << messaget::eom;
1383  race_check(value_set_analysis, goto_model);
1384  }
1385 
1386  if(cmdline.isset("mm"))
1387  {
1388  std::string mm=cmdline.get_value("mm");
1389  memory_modelt model;
1390 
1391  // strategy of instrumentation
1392  instrumentation_strategyt inst_strategy;
1393  if(cmdline.isset("one-event-per-cycle"))
1394  inst_strategy=one_event_per_cycle;
1395  else if(cmdline.isset("minimum-interference"))
1396  inst_strategy=min_interference;
1397  else if(cmdline.isset("read-first"))
1398  inst_strategy=read_first;
1399  else if(cmdline.isset("write-first"))
1400  inst_strategy=write_first;
1401  else if(cmdline.isset("my-events"))
1402  inst_strategy=my_events;
1403  else
1404  /* default: instruments all unsafe pairs */
1405  inst_strategy=all;
1406 
1407  const unsigned max_var=
1408  cmdline.isset("max-var")?
1410  const unsigned max_po_trans=
1411  cmdline.isset("max-po-trans")?
1412  unsafe_string2unsigned(cmdline.get_value("max-po-trans")):0;
1413 
1414  if(mm=="tso")
1415  {
1416  log.status() << "Adding weak memory (TSO) Instrumentation"
1417  << messaget::eom;
1418  model=TSO;
1419  }
1420  else if(mm=="pso")
1421  {
1422  log.status() << "Adding weak memory (PSO) Instrumentation"
1423  << messaget::eom;
1424  model=PSO;
1425  }
1426  else if(mm=="rmo")
1427  {
1428  log.status() << "Adding weak memory (RMO) Instrumentation"
1429  << messaget::eom;
1430  model=RMO;
1431  }
1432  else if(mm=="power")
1433  {
1434  log.status() << "Adding weak memory (Power) Instrumentation"
1435  << messaget::eom;
1436  model=Power;
1437  }
1438  else
1439  {
1440  log.error() << "Unknown weak memory model '" << mm << "'"
1441  << messaget::eom;
1442  model=Unknown;
1443  }
1444 
1446 
1447  if(cmdline.isset("force-loop-duplication"))
1448  loops=all_loops;
1449  if(cmdline.isset("no-loop-duplication"))
1450  loops=no_loop;
1451 
1452  if(model!=Unknown)
1453  weak_memory(
1454  model,
1455  value_set_analysis,
1456  goto_model,
1457  cmdline.isset("scc"),
1458  inst_strategy,
1459  !cmdline.isset("cfg-kill"),
1460  cmdline.isset("no-dependencies"),
1461  loops,
1462  max_var,
1463  max_po_trans,
1464  !cmdline.isset("no-po-rendering"),
1465  cmdline.isset("render-cluster-file"),
1466  cmdline.isset("render-cluster-function"),
1467  cmdline.isset("cav11"),
1468  cmdline.isset("hide-internals"),
1470  cmdline.isset("ignore-arrays"));
1471  }
1472 
1473  // Interrupt handler
1474  if(cmdline.isset("isr"))
1475  {
1476  log.status() << "Instrumenting interrupt handler" << messaget::eom;
1477  interrupt(
1478  value_set_analysis,
1479  goto_model,
1480  cmdline.get_value("isr"));
1481  }
1482 
1483  // Memory-mapped I/O
1484  if(cmdline.isset("mmio"))
1485  {
1486  log.status() << "Instrumenting memory-mapped I/O" << messaget::eom;
1487  mmio(value_set_analysis, goto_model);
1488  }
1489 
1490  if(cmdline.isset("concurrency"))
1491  {
1492  log.status() << "Sequentializing concurrency" << messaget::eom;
1493  concurrency(value_set_analysis, goto_model);
1494  }
1495  }
1496 
1497  if(cmdline.isset("interval-analysis"))
1498  {
1499  log.status() << "Interval analysis" << messaget::eom;
1501  }
1502 
1503  if(cmdline.isset("havoc-loops"))
1504  {
1505  log.status() << "Havocking loops" << messaget::eom;
1507  }
1508 
1509  if(cmdline.isset("k-induction"))
1510  {
1511  bool base_case=cmdline.isset("base-case");
1512  bool step_case=cmdline.isset("step-case");
1513 
1514  if(step_case && base_case)
1515  throw "please specify only one of --step-case and --base-case";
1516  else if(!step_case && !base_case)
1517  throw "please specify one of --step-case and --base-case";
1518 
1519  unsigned k=unsafe_string2unsigned(cmdline.get_value("k-induction"));
1520 
1521  if(k==0)
1522  throw "please give k>=1";
1523 
1524  log.status() << "Instrumenting k-induction for k=" << k << ", "
1525  << (base_case ? "base case" : "step case") << messaget::eom;
1526 
1527  k_induction(goto_model, base_case, step_case, k);
1528  }
1529 
1530  if(cmdline.isset("function-enter"))
1531  {
1532  log.status() << "Function enter instrumentation" << messaget::eom;
1534  goto_model,
1535  cmdline.get_value("function-enter"));
1536  }
1537 
1538  if(cmdline.isset("function-exit"))
1539  {
1540  log.status() << "Function exit instrumentation" << messaget::eom;
1541  function_exit(
1542  goto_model,
1543  cmdline.get_value("function-exit"));
1544  }
1545 
1546  if(cmdline.isset("branch"))
1547  {
1548  log.status() << "Branch instrumentation" << messaget::eom;
1549  branch(
1550  goto_model,
1551  cmdline.get_value("branch"));
1552  }
1553 
1554  // add failed symbols
1556 
1557  // recalculate numbers, etc.
1559 
1560  // add loop ids
1562 
1563  // label the assertions
1565 
1566  // nondet volatile?
1567  if(cmdline.isset("nondet-volatile"))
1568  {
1569  log.status() << "Making volatile variables non-deterministic"
1570  << messaget::eom;
1572  }
1573 
1574  // reachability slice?
1575  if(cmdline.isset("reachability-slice"))
1576  {
1578 
1579  log.status() << "Performing a reachability slice" << messaget::eom;
1580 
1581  // reachability_slicer requires that the model has unique location numbers:
1583 
1584  if(cmdline.isset("property"))
1586  else
1588  }
1589 
1590  if(cmdline.isset("fp-reachability-slice"))
1591  {
1593 
1594  log.status() << "Performing a function pointer reachability slice"
1595  << messaget::eom;
1597  goto_model, cmdline.get_comma_separated_values("fp-reachability-slice"));
1598  }
1599 
1600  // full slice?
1601  if(cmdline.isset("full-slice"))
1602  {
1605 
1606  log.status() << "Performing a full slice" << messaget::eom;
1607  if(cmdline.isset("property"))
1609  else
1610  {
1611  // full_slicer requires that the model has unique location numbers:
1614  }
1615  }
1616 
1617  // splice option
1618  if(cmdline.isset("splice-call"))
1619  {
1620  log.status() << "Performing call splicing" << messaget::eom;
1621  std::string callercallee=cmdline.get_value("splice-call");
1622  if(splice_call(
1624  callercallee,
1627  throw 0;
1628  }
1629 
1630  // aggressive slicer
1631  if(cmdline.isset("aggressive-slice"))
1632  {
1634 
1635  // reachability_slicer requires that the model has unique location numbers:
1637 
1638  log.status() << "Slicing away initializations of unused global variables"
1639  << messaget::eom;
1641 
1642  log.status() << "Performing an aggressive slice" << messaget::eom;
1643  aggressive_slicert aggressive_slicer(goto_model, ui_message_handler);
1644 
1645  if(cmdline.isset("aggressive-slice-call-depth"))
1646  aggressive_slicer.call_depth =
1647  safe_string2unsigned(cmdline.get_value("aggressive-slice-call-depth"));
1648 
1649  if(cmdline.isset("aggressive-slice-preserve-function"))
1650  aggressive_slicer.preserve_functions(
1651  cmdline.get_values("aggressive-slice-preserve-function"));
1652 
1653  if(cmdline.isset("property"))
1654  aggressive_slicer.user_specified_properties =
1655  cmdline.get_values("property");
1656 
1657  if(cmdline.isset("aggressive-slice-preserve-functions-containing"))
1658  aggressive_slicer.name_snippets =
1659  cmdline.get_values("aggressive-slice-preserve-functions-containing");
1660 
1661  aggressive_slicer.preserve_all_direct_paths =
1662  cmdline.isset("aggressive-slice-preserve-all-direct-paths");
1663 
1664  aggressive_slicer.doit();
1665 
1667 
1668  log.status() << "Performing a reachability slice" << messaget::eom;
1669  if(cmdline.isset("property"))
1671  else
1673  }
1674 
1675  if(cmdline.isset("ensure-one-backedge-per-target"))
1676  {
1677  log.status() << "Trying to force one backedge per target" << messaget::eom;
1679  }
1680 
1681  // recalculate numbers, etc.
1683 }
1684 
1687 {
1688  // clang-format off
1689  std::cout << '\n' << banner_string("Goto-Instrument", CBMC_VERSION) << '\n'
1690  << align_center_with_border("Copyright (C) 2008-2013") << '\n'
1691  << align_center_with_border("Daniel Kroening") << '\n'
1692  << align_center_with_border("kroening@kroening.com") << '\n'
1693  <<
1694  "\n"
1695  "Usage: Purpose:\n"
1696  "\n"
1697  " goto-instrument [-?] [-h] [--help] show help\n"
1698  " goto-instrument in out perform instrumentation\n"
1699  "\n"
1700  "Main options:\n"
1701  " --document-properties-html generate HTML property documentation\n"
1702  " --document-properties-latex generate Latex property documentation\n"
1703  " --dump-c generate C source\n"
1704  " --dump-c-type-header m generate a C header for types local in m\n"
1705  " --dump-cpp generate C++ source\n"
1706  " --dot generate CFG graph in DOT format\n"
1707  " --interpreter do concrete execution\n"
1708  "\n"
1709  "Diagnosis:\n"
1710  " --show-loops show the loops in the program\n"
1712  " --show-symbol-table show loaded symbol table\n"
1713  " --list-symbols list symbols with type information\n"
1716  " --drop-unused-functions drop functions trivially unreachable from main function\n" // NOLINT(*)
1717  " --print-internal-representation\n" // NOLINTNEXTLINE(*)
1718  " show verbose internal representation of the program\n"
1719  " --list-undefined-functions list functions without body\n"
1720  " --show-struct-alignment show struct members that might be concurrently accessed\n" // NOLINT(*)
1721  " --show-natural-loops show natural loop heads\n"
1722  // NOLINTNEXTLINE(whitespace/line_length)
1723  " --list-calls-args list all function calls with their arguments\n"
1724  " --call-graph show graph of function calls\n"
1725  // NOLINTNEXTLINE(whitespace/line_length)
1726  " --reachable-call-graph show graph of function calls potentially reachable from main function\n"
1728  // NOLINTNEXTLINE(whitespace/line_length)
1729  " --show-threaded show instructions that may be executed by more than one thread\n"
1730  " --show-local-safe-pointers show pointer expressions that are trivially dominated by a not-null check\n" // NOLINT(*)
1731  " --show-safe-dereferences show pointer expressions that are trivially dominated by a not-null check\n" // NOLINT(*)
1732  " *and* used as a dereference operand\n" // NOLINT(*)
1734  // NOLINTNEXTLINE(whitespace/line_length)
1735  " --validate-goto-binary check the well-formedness of the passed in goto\n"
1736  " binary and then exit\n"
1737  "\n"
1738  "Safety checks:\n"
1739  " --no-assertions ignore user assertions\n"
1741  " --uninitialized-check add checks for uninitialized locals (experimental)\n" // NOLINT(*)
1742  " --error-label label check that label is unreachable\n"
1743  " --stack-depth n add check that call stack size of non-inlined functions never exceeds n\n" // NOLINT(*)
1744  " --race-check add floating-point data race checks\n"
1745  "\n"
1746  "Semantic transformations:\n"
1747  " --nondet-volatile makes reads from volatile variables non-deterministic\n" // NOLINT(*)
1748  " --unwind <n> unwinds the loops <n> times\n"
1749  " --unwindset L:B,... unwind loop L with a bound of B\n"
1750  " --unwindset-file <file> read unwindset from file\n"
1751  " --partial-loops permit paths with partial loops\n"
1752  " --unwinding-assertions generate unwinding assertions\n"
1753  " --continue-as-loops add loop for remaining iterations after unwound part\n" // NOLINT(*)
1754  " --isr <function> instruments an interrupt service routine\n"
1755  " --mmio instruments memory-mapped I/O\n"
1756  " --nondet-static add nondeterministic initialization of variables with static lifetime\n" // NOLINT(*)
1757  " --nondet-static-exclude e same as nondet-static except for the variable e\n" //NOLINT(*)
1758  " (use multiple times if required)\n"
1759  " --check-invariant function instruments invariant checking function\n"
1760  " --remove-pointers converts pointer arithmetic to base+offset expressions\n" // NOLINT(*)
1761  " --splice-call caller,callee prepends a call to callee in the body of caller\n" // NOLINT(*)
1762  " --undefined-function-is-assume-false\n"
1763  // NOLINTNEXTLINE(whitespace/line_length)
1764  " convert each call to an undefined function to assume(false)\n"
1768  "\n"
1769  "Loop transformations:\n"
1770  " --k-induction <k> check loops with k-induction\n"
1771  " --step-case k-induction: do step-case\n"
1772  " --base-case k-induction: do base-case\n"
1773  " --havoc-loops over-approximate all loops\n"
1774  " --accelerate add loop accelerators\n"
1775  " --skip-loops <loop-ids> add gotos to skip selected loops during execution\n" // NOLINT(*)
1776  "\n"
1777  "Memory model instrumentations:\n"
1778  " --mm <tso,pso,rmo,power> instruments a weak memory model\n"
1779  " --scc detects critical cycles per SCC (one thread per SCC)\n" // NOLINT(*)
1780  " --one-event-per-cycle only instruments one event per cycle\n"
1781  " --minimum-interference instruments an optimal number of events\n"
1782  " --my-events only instruments events whose ids appear in inst.evt\n" // NOLINT(*)
1783  " --cfg-kill enables symbolic execution used to reduce spurious cycles\n" // NOLINT(*)
1784  " --no-dependencies no dependency analysis\n"
1785  // NOLINTNEXTLINE(whitespace/line_length)
1786  " --no-po-rendering no representation of the threads in the dot\n"
1787  " --render-cluster-file clusterises the dot by files\n"
1788  " --render-cluster-function clusterises the dot by functions\n"
1789  "\n"
1790  "Slicing:\n"
1792  " --full-slice slice away instructions that don't affect assertions\n" // NOLINT(*)
1793  " --property id slice with respect to specific property only\n" // NOLINT(*)
1794  " --slice-global-inits slice away initializations of unused global variables\n" // NOLINT(*)
1795  " --aggressive-slice remove bodies of any functions not on the shortest path between\n" // NOLINT(*)
1796  " the start function and the function containing the property(s)\n" // NOLINT(*)
1797  " --aggressive-slice-call-depth <n>\n"
1798  " used with aggressive-slice, preserves all functions within <n> function calls\n" // NOLINT(*)
1799  " of the functions on the shortest path\n"
1800  " --aggressive-slice-preserve-function <f>\n"
1801  " force the aggressive slicer to preserve function <f>\n" // NOLINT(*)
1802  " --aggressive-slice-preserve-function containing <f>\n"
1803  " force the aggressive slicer to preserve all functions with names containing <f>\n" // NOLINT(*)
1804  "--aggressive-slice-preserve-all-direct-paths \n"
1805  " force aggressive slicer to preserve all direct paths\n" // NOLINT(*)
1806  "\n"
1807  "Further transformations:\n"
1808  " --constant-propagator propagate constants and simplify expressions\n" // NOLINT(*)
1809  " --inline perform full inlining\n"
1810  " --partial-inline perform partial inlining\n"
1811  " --function-inline <function> transitively inline all calls <function> makes\n" // NOLINT(*)
1812  " --no-caching disable caching of intermediate results during transitive function inlining\n" // NOLINT(*)
1813  " --log <file> log in json format which code segments were inlined, use with --function-inline\n" // NOLINT(*)
1814  " --remove-function-pointers replace function pointers by case statement over function calls\n" // NOLINT(*)
1817  " --add-library add models of C library functions\n"
1818  " --model-argc-argv <n> model up to <n> command line arguments\n"
1819  // NOLINTNEXTLINE(whitespace/line_length)
1820  " --remove-function-body <f> remove the implementation of function <f> (may be repeated)\n"
1822  "\n"
1823  "Other options:\n"
1824  " --no-system-headers with --dump-c/--dump-cpp: generate C source expanding libc includes\n" // NOLINT(*)
1825  " --use-all-headers with --dump-c/--dump-cpp: generate C source with all includes\n" // NOLINT(*)
1826  " --harness with --dump-c/--dump-cpp: include input generator in output\n" // NOLINT(*)
1827  " --version show version and exit\n"
1828  HELP_FLUSH
1829  " --xml-ui use XML-formatted output\n"
1830  " --json-ui use JSON-formatted output\n"
1832  "\n";
1833  // clang-format on
1834 }
cprover_library.h
cmdlinet::args
argst args
Definition: cmdline.h:85
CBMC_VERSION
const char * CBMC_VERSION
Definition: version.cpp:1
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
concurrency.h
horn_encoding
void horn_encoding(const goto_modelt &, std::ostream &)
Definition: horn_encoding.cpp:18
havoc_loops.h
PARSE_OPTIONS_GOTO_CHECK
#define PARSE_OPTIONS_GOTO_CHECK(cmdline, options)
Definition: goto_check.h:60
class_hierarchyt
Non-graph-based representation of the class hierarchy.
Definition: class_hierarchy.h:43
horn_encoding.h
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
cmdlinet::isset
virtual bool isset(char option) const
Definition: cmdline.cpp:28
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:966
goto_instrument_parse_optionst::help
virtual void help()
display command line help
Definition: goto_instrument_parse_options.cpp:1686
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:952
goto_inline.h
optionst
Definition: options.h:23
goto_instrument_parse_optionst::function_pointer_removal_done
bool function_pointer_removal_done
Definition: goto_instrument_parse_options.h:149
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
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:168
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:400
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
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
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
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
remove_asm.h
HELP_SHOW_CLASS_HIERARCHY
#define HELP_SHOW_CLASS_HIERARCHY
Definition: class_hierarchy.h:29
constant_propagator.h
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:742
interpreter.h
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:553
remove_calls_no_body.h
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:935
Power
@ Power
Definition: wmm.h:23
mmio.h
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
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:2143
optionst::set_option
void set_option(const std::string &option, const bool value)
Definition: options.cpp:28
call_graph.h
weak_memory.h
k_induction.h
insert_final_assert_false.h
messaget::eom
static eomt eom
Definition: message.h:283
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
nondet_static.h
jsont
Definition: json.h:25
document_properties.h
nondet_volatile
void nondet_volatile(symbol_tablet &symbol_table, goto_programt &goto_program)
Definition: nondet_volatile.cpp:78
string_instrumentation.h
sese_regions.h
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
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
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:119
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
splice_call.h
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
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)
Given a string s, split into a sequence of substrings when separated by specified delimiter.
Definition: string_utils.cpp:40
set_properties.h
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
full_slicer
void full_slicer(goto_functionst &goto_functions, const namespacet &ns, const slicing_criteriont &criterion)
Definition: full_slicer.cpp:345
dot.h
interrupt.h
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:385
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:146
goto_instrument_parse_optionst::doit
virtual int doit()
invoke main modules
Definition: goto_instrument_parse_options.cpp:116
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:915
goto_instrument_parse_optionst::get_goto_program
void get_goto_program()
Definition: goto_instrument_parse_options.cpp:977
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
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
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
goto_instrument_parse_optionst::instrument_goto_program
void instrument_goto_program()
Definition: goto_instrument_parse_options.cpp:994
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:46
show_symbol_table.h
remove_function.h
HELP_SHOW_PROPERTIES
#define HELP_SHOW_PROPERTIES
Definition: show_properties.h:29
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
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
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
reaching_definitions.h
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:1178
code_contracts
void code_contracts(goto_modelt &goto_model)
Definition: code_contracts.cpp:391
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
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:57
HELP_REPLACE_FUNCTION_BODY
#define HELP_REPLACE_FUNCTION_BODY
Definition: generate_function_bodies.h:93
branch.h
read_goto_binary.h
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
full_slicer.h
goto_instrument_parse_optionst::partial_inlining_done
bool partial_inlining_done
Definition: goto_instrument_parse_options.h:150
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:59
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
remove_unused_functions.h
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
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
points_to.h
goto_instrument_parse_optionst::remove_returns_done
bool remove_returns_done
Definition: goto_instrument_parse_options.h:151
class_hierarchy.h
interval_domain.h
stack_depth.h
show_locations.h
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
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
HELP_GOTO_CHECK
#define HELP_GOTO_CHECK
Definition: goto_check.h:44
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:77
call_sequences.h
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:768
rw_set.h
exit_codes.h
call_grapht::output
void output(std::ostream &out) const
Definition: call_graph.cpp:271
natural_loops.h
constant_propagator_ait
Definition: constant_propagator.h:171
goto_program_dereference.h
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
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
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
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
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
goto_instrument_parse_optionst::goto_model
goto_modelt goto_model
Definition: goto_instrument_parse_options.h:153
model_argc_argv.h
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
add_failed_symbols.h
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
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
havoc_loops
void havoc_loops(goto_modelt &goto_model)
Definition: havoc_loops.cpp:120
alignment_checks.h
ensure_one_backedge_per_target.h
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
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:99
remove_skip.h
list_eloc
void list_eloc(const goto_modelt &goto_model)
Definition: count_eloc.cpp:64
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
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
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:107
remove_function_pointers.h
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:133
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:1172
code_contracts.h
interval_analysis.h
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
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
HELP_FLUSH
#define HELP_FLUSH
Definition: ui_message.h:105
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
HELP_VALIDATE
#define HELP_VALIDATE
Definition: validation_interface.h:16