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/exit_codes.h>
20 #include <util/json.h>
21 #include <util/string2int.h>
22 #include <util/unicode.h>
23 #include <util/version.h>
24 
39 #include <goto-programs/loop_ids.h>
47 
52 
53 #include <analyses/natural_loops.h>
58 #include <analyses/call_graph.h>
64 #include <analyses/is_threaded.h>
66 
67 #include <ansi-c/cprover_library.h>
68 #include <cpp/cprover_library.h>
69 
70 #include "accelerate/accelerate.h"
71 #include "alignment_checks.h"
72 #include "branch.h"
73 #include "call_sequences.h"
74 #include "code_contracts.h"
75 #include "concurrency.h"
76 #include "document_properties.h"
77 #include "dot.h"
78 #include "dump_c.h"
79 #include "full_slicer.h"
80 #include "function.h"
81 #include "havoc_loops.h"
82 #include "horn_encoding.h"
83 #include "interrupt.h"
84 #include "k_induction.h"
85 #include "mmio.h"
86 #include "model_argc_argv.h"
87 #include "nondet_static.h"
88 #include "nondet_volatile.h"
89 #include "points_to.h"
90 #include "race_check.h"
91 #include "reachability_slicer.h"
92 #include "remove_function.h"
93 #include "rw_set.h"
94 #include "show_locations.h"
95 #include "skip_loops.h"
96 #include "splice_call.h"
97 #include "stack_depth.h"
98 #include "thread_instrumentation.h"
99 #include "undefined_functions.h"
100 #include "uninitialized.h"
101 #include "unwind.h"
102 #include "wmm/weak_memory.h"
103 
106 {
107  if(cmdline.isset("version"))
108  {
109  std::cout << CBMC_VERSION << '\n';
110  return CPROVER_EXIT_SUCCESS;
111  }
112 
113  if(cmdline.args.size()!=1 && cmdline.args.size()!=2)
114  {
115  help();
117  }
118 
121 
122  try
123  {
125 
127 
129 
130  {
131  bool unwind_given=cmdline.isset("unwind");
132  bool unwindset_given=cmdline.isset("unwindset");
133  bool unwindset_file_given=cmdline.isset("unwindset-file");
134 
135  if(unwindset_given && unwindset_file_given)
136  throw "only one of --unwindset and --unwindset-file supported at a "
137  "time";
138 
139  if(unwind_given || unwindset_given || unwindset_file_given)
140  {
141  unwindsett unwindset;
142 
143  if(unwind_given)
144  unwindset.parse_unwind(cmdline.get_value("unwind"));
145 
146  if(unwindset_file_given)
147  unwindset.parse_unwindset_file(cmdline.get_value("unwindset-file"));
148 
149  if(unwindset_given)
150  unwindset.parse_unwindset(cmdline.get_value("unwindset"));
151 
152  bool unwinding_assertions=cmdline.isset("unwinding-assertions");
153  bool partial_loops=cmdline.isset("partial-loops");
154  bool continue_as_loops=cmdline.isset("continue-as-loops");
155 
156  if(unwinding_assertions+partial_loops+continue_as_loops>1)
157  throw "more than one of --unwinding-assertions,--partial-loops,"
158  "--continue-as-loops selected";
159 
160  goto_unwindt::unwind_strategyt unwind_strategy=
162 
163  if(unwinding_assertions)
164  {
166  }
167  else if(partial_loops)
168  {
170  }
171  else if(continue_as_loops)
172  {
174  }
175 
176  goto_unwindt goto_unwind;
177  goto_unwind(goto_model, unwindset, unwind_strategy);
178 
179  if(cmdline.isset("log"))
180  {
181  std::string filename=cmdline.get_value("log");
182  bool have_file=!filename.empty() && filename!="-";
183 
184  jsont result=goto_unwind.output_log_json();
185 
186  if(have_file)
187  {
188 #ifdef _MSC_VER
189  std::ofstream of(widen(filename));
190 #else
191  std::ofstream of(filename);
192 #endif
193  if(!of)
194  throw "failed to open file "+filename;
195 
196  of << result;
197  of.close();
198  }
199  else
200  {
201  std::cout << result << '\n';
202  }
203  }
204 
205  // goto_unwind holds references to instructions, only do remove_skip
206  // after having generated the log above
208  }
209  }
210 
211  if(cmdline.isset("show-threaded"))
212  {
214 
215  is_threadedt is_threaded(goto_model);
216 
218  {
219  std::cout << "////\n";
220  std::cout << "//// Function: " << f_it->first << '\n';
221  std::cout << "////\n\n";
222 
223  const goto_programt &goto_program=f_it->second.body;
224 
226  {
227  goto_program.output_instruction(ns, "", std::cout, *i_it);
228  std::cout << "Is threaded: " << (is_threaded(i_it)?"True":"False")
229  << "\n\n";
230  }
231  }
232 
233  return CPROVER_EXIT_SUCCESS;
234  }
235 
236  if(cmdline.isset("show-value-sets"))
237  {
239 
240  // recalculate numbers, etc.
242 
243  status() << "Pointer Analysis" << eom;
245  value_set_analysist value_set_analysis(ns);
246  value_set_analysis(goto_model.goto_functions);
247  show_value_sets(get_ui(), goto_model, value_set_analysis);
248  return CPROVER_EXIT_SUCCESS;
249  }
250 
251  if(cmdline.isset("show-global-may-alias"))
252  {
256 
257  // recalculate numbers, etc.
259 
260  global_may_alias_analysist global_may_alias_analysis;
261  global_may_alias_analysis(goto_model);
262  global_may_alias_analysis.output(goto_model, std::cout);
263 
264  return CPROVER_EXIT_SUCCESS;
265  }
266 
267  if(cmdline.isset("show-local-bitvector-analysis"))
268  {
271 
272  // recalculate numbers, etc.
274 
276 
278  {
279  local_bitvector_analysist local_bitvector_analysis(it->second);
280  std::cout << ">>>>\n";
281  std::cout << ">>>> " << it->first << '\n';
282  std::cout << ">>>>\n";
283  local_bitvector_analysis.output(std::cout, it->second, ns);
284  std::cout << '\n';
285  }
286 
287  return CPROVER_EXIT_SUCCESS;
288  }
289 
290  if(cmdline.isset("show-local-safe-pointers") ||
291  cmdline.isset("show-safe-dereferences"))
292  {
293  // Ensure location numbering is unique:
295 
297 
299  {
300  local_safe_pointerst local_safe_pointers(ns);
301  local_safe_pointers(it->second.body);
302  std::cout << ">>>>\n";
303  std::cout << ">>>> " << it->first << '\n';
304  std::cout << ">>>>\n";
305  if(cmdline.isset("show-local-safe-pointers"))
306  local_safe_pointers.output(std::cout, it->second.body);
307  else
308  {
309  local_safe_pointers.output_safe_dereferences(
310  std::cout, it->second.body);
311  }
312  std::cout << '\n';
313  }
314 
315  return CPROVER_EXIT_SUCCESS;
316  }
317 
318  if(cmdline.isset("show-custom-bitvector-analysis"))
319  {
323 
325 
326  if(!cmdline.isset("inline"))
327  {
330  }
331 
332  // recalculate numbers, etc.
334 
335  custom_bitvector_analysist custom_bitvector_analysis;
336  custom_bitvector_analysis(goto_model);
337  custom_bitvector_analysis.output(goto_model, std::cout);
338 
339  return CPROVER_EXIT_SUCCESS;
340  }
341 
342  if(cmdline.isset("show-escape-analysis"))
343  {
347 
348  // recalculate numbers, etc.
350 
351  escape_analysist escape_analysis;
352  escape_analysis(goto_model);
353  escape_analysis.output(goto_model, std::cout);
354 
355  return CPROVER_EXIT_SUCCESS;
356  }
357 
358  if(cmdline.isset("custom-bitvector-analysis"))
359  {
363 
365 
366  if(!cmdline.isset("inline"))
367  {
370  }
371 
372  // recalculate numbers, etc.
374 
376 
377  custom_bitvector_analysist custom_bitvector_analysis;
378  custom_bitvector_analysis(goto_model);
379  custom_bitvector_analysis.check(
380  goto_model,
381  cmdline.isset("xml-ui"),
382  std::cout);
383 
384  return CPROVER_EXIT_SUCCESS;
385  }
386 
387  if(cmdline.isset("show-points-to"))
388  {
390 
391  // recalculate numbers, etc.
393 
395 
396  status() << "Pointer Analysis" << eom;
397  points_tot points_to;
398  points_to(goto_model);
399  points_to.output(std::cout);
400  return CPROVER_EXIT_SUCCESS;
401  }
402 
403  if(cmdline.isset("show-intervals"))
404  {
406 
407  // recalculate numbers, etc.
409 
410  status() << "Interval Analysis" << eom;
414  interval_analysis.output(goto_model, std::cout);
415  return CPROVER_EXIT_SUCCESS;
416  }
417 
418  if(cmdline.isset("show-call-sequences"))
419  {
422  return CPROVER_EXIT_SUCCESS;
423  }
424 
425  if(cmdline.isset("check-call-sequence"))
426  {
429  return CPROVER_EXIT_SUCCESS;
430  }
431 
432  if(cmdline.isset("list-calls-args"))
433  {
435 
437 
438  return CPROVER_EXIT_SUCCESS;
439  }
440 
441  if(cmdline.isset("show-rw-set"))
442  {
444 
445  if(!cmdline.isset("inline"))
446  {
448 
449  // recalculate numbers, etc.
451  }
452 
453  status() << "Pointer Analysis" << eom;
454  value_set_analysist value_set_analysis(ns);
455  value_set_analysis(goto_model.goto_functions);
456 
457  const symbolt &symbol=ns.lookup(ID_main);
458  symbol_exprt main(symbol.name, symbol.type);
459 
460  std::cout <<
461  rw_set_functiont(value_set_analysis, goto_model, main);
462  return CPROVER_EXIT_SUCCESS;
463  }
464 
465  if(cmdline.isset("show-symbol-table"))
466  {
468  return CPROVER_EXIT_SUCCESS;
469  }
470 
471  if(cmdline.isset("show-reaching-definitions"))
472  {
474 
476  reaching_definitions_analysist rd_analysis(ns);
477  rd_analysis(goto_model);
478  rd_analysis.output(goto_model, std::cout);
479 
480  return CPROVER_EXIT_SUCCESS;
481  }
482 
483  if(cmdline.isset("show-dependence-graph"))
484  {
486 
488  dependence_grapht dependence_graph(ns);
489  dependence_graph(goto_model);
490  dependence_graph.output(goto_model, std::cout);
491  dependence_graph.output_dot(std::cout);
492 
493  return CPROVER_EXIT_SUCCESS;
494  }
495 
496  if(cmdline.isset("count-eloc"))
497  {
499  return CPROVER_EXIT_SUCCESS;
500  }
501 
502  if(cmdline.isset("list-eloc"))
503  {
505  return CPROVER_EXIT_SUCCESS;
506  }
507 
508  if(cmdline.isset("print-path-lengths"))
509  {
511  return CPROVER_EXIT_SUCCESS;
512  }
513 
514  if(cmdline.isset("print-global-state-size"))
515  {
517  return CPROVER_EXIT_SUCCESS;
518  }
519 
520  if(cmdline.isset("list-symbols"))
521  {
523  return CPROVER_EXIT_SUCCESS;
524  }
525 
526  if(cmdline.isset("show-uninitialized"))
527  {
528  show_uninitialized(goto_model, std::cout);
529  return CPROVER_EXIT_SUCCESS;
530  }
531 
532  if(cmdline.isset("interpreter"))
533  {
534  status() << "Starting interpreter" << eom;
536  return CPROVER_EXIT_SUCCESS;
537  }
538 
539  if(cmdline.isset("show-claims") ||
540  cmdline.isset("show-properties"))
541  {
544  return CPROVER_EXIT_SUCCESS;
545  }
546 
547  if(cmdline.isset("document-claims-html") ||
548  cmdline.isset("document-properties-html"))
549  {
551  return CPROVER_EXIT_SUCCESS;
552  }
553 
554  if(cmdline.isset("document-claims-latex") ||
555  cmdline.isset("document-properties-latex"))
556  {
558  return CPROVER_EXIT_SUCCESS;
559  }
560 
561  if(cmdline.isset("show-loops"))
562  {
564  return CPROVER_EXIT_SUCCESS;
565  }
566 
567  if(cmdline.isset("show-natural-loops"))
568  {
569  show_natural_loops(goto_model, std::cout);
570  return CPROVER_EXIT_SUCCESS;
571  }
572 
573  if(cmdline.isset("print-internal-representation"))
574  {
575  for(auto const &pair : goto_model.goto_functions.function_map)
576  for(auto const &ins : pair.second.body.instructions)
577  {
578  if(ins.code.is_not_nil())
579  status() << ins.code.pretty() << eom;
580  if(ins.guard.is_not_nil())
581  status() << "[guard] " << ins.guard.pretty() << eom;
582  }
583  return CPROVER_EXIT_SUCCESS;
584  }
585 
586  if(
587  cmdline.isset("show-goto-functions") ||
588  cmdline.isset("list-goto-functions"))
589  {
591  goto_model,
594  cmdline.isset("list-goto-functions"));
595  return CPROVER_EXIT_SUCCESS;
596  }
597 
598  if(cmdline.isset("list-undefined-functions"))
599  {
601  return CPROVER_EXIT_SUCCESS;
602  }
603 
604  // experimental: print structs
605  if(cmdline.isset("show-struct-alignment"))
606  {
608  return CPROVER_EXIT_SUCCESS;
609  }
610 
611  if(cmdline.isset("show-locations"))
612  {
614  return CPROVER_EXIT_SUCCESS;
615  }
616 
617  if(cmdline.isset("dump-c") || cmdline.isset("dump-cpp"))
618  {
619  const bool is_cpp=cmdline.isset("dump-cpp");
620  const bool h_libc=!cmdline.isset("no-system-headers");
621  const bool h_all=cmdline.isset("use-all-headers");
622  const bool harness=cmdline.isset("harness");
624 
625  // restore RETURN instructions in case remove_returns had been
626  // applied
628 
629  if(cmdline.args.size()==2)
630  {
631  #ifdef _MSC_VER
632  std::ofstream out(widen(cmdline.args[1]));
633  #else
634  std::ofstream out(cmdline.args[1]);
635  #endif
636  if(!out)
637  {
638  error() << "failed to write to `" << cmdline.args[1] << "'";
640  }
641  (is_cpp ? dump_cpp : dump_c)(
643  h_libc,
644  h_all,
645  harness,
646  ns,
647  out);
648  }
649  else
650  (is_cpp ? dump_cpp : dump_c)(
652  h_libc,
653  h_all,
654  harness,
655  ns,
656  std::cout);
657 
658  return CPROVER_EXIT_SUCCESS;
659  }
660 
661  if(cmdline.isset("call-graph"))
662  {
664  call_grapht call_graph(goto_model);
665 
666  if(cmdline.isset("xml"))
667  call_graph.output_xml(std::cout);
668  else if(cmdline.isset("dot"))
669  call_graph.output_dot(std::cout);
670  else
671  call_graph.output(std::cout);
672 
673  return CPROVER_EXIT_SUCCESS;
674  }
675 
676  if(cmdline.isset("reachable-call-graph"))
677  {
679  call_grapht call_graph =
682  if(cmdline.isset("xml"))
683  call_graph.output_xml(std::cout);
684  else if(cmdline.isset("dot"))
685  call_graph.output_dot(std::cout);
686  else
687  call_graph.output(std::cout);
688 
689  return 0;
690  }
691 
692  if(cmdline.isset("show-class-hierarchy"))
693  {
694  class_hierarchyt hierarchy;
695  hierarchy(goto_model.symbol_table);
696  if(cmdline.isset("dot"))
697  hierarchy.output_dot(std::cout);
698  else
701 
702  return CPROVER_EXIT_SUCCESS;
703  }
704 
705  if(cmdline.isset("dot"))
706  {
708 
709  if(cmdline.args.size()==2)
710  {
711  #ifdef _MSC_VER
712  std::ofstream out(widen(cmdline.args[1]));
713  #else
714  std::ofstream out(cmdline.args[1]);
715  #endif
716  if(!out)
717  {
718  error() << "failed to write to " << cmdline.args[1] << "'";
720  }
721 
722  dot(goto_model, out);
723  }
724  else
725  dot(goto_model, std::cout);
726 
727  return CPROVER_EXIT_SUCCESS;
728  }
729 
730  if(cmdline.isset("accelerate"))
731  {
733 
735 
736  status() << "Performing full inlining" << eom;
738 
739  status() << "Removing calls to functions without a body" << eom;
740  remove_calls_no_bodyt remove_calls_no_body;
741  remove_calls_no_body(goto_model.goto_functions);
742 
743  status() << "Accelerating" << eom;
747  }
748 
749  if(cmdline.isset("horn-encoding"))
750  {
751  status() << "Horn-clause encoding" << eom;
753 
754  if(cmdline.args.size()==2)
755  {
756  #ifdef _MSC_VER
757  std::ofstream out(widen(cmdline.args[1]));
758  #else
759  std::ofstream out(cmdline.args[1]);
760  #endif
761 
762  if(!out)
763  {
764  error() << "Failed to open output file "
765  << cmdline.args[1] << eom;
767  }
768 
770  }
771  else
772  horn_encoding(goto_model, std::cout);
773 
774  return CPROVER_EXIT_SUCCESS;
775  }
776 
777  if(cmdline.isset("drop-unused-functions"))
778  {
780 
781  status() << "Removing unused functions" << eom;
783  }
784 
785  if(cmdline.isset("undefined-function-is-assume-false"))
786  {
789  }
790 
791  // write new binary?
792  if(cmdline.args.size()==2)
793  {
794  status() << "Writing GOTO program to `" << cmdline.args[1] << "'" << eom;
795 
799  else
800  return CPROVER_EXIT_SUCCESS;
801  }
802 
803  help();
805  }
806 
807  catch(const char *e)
808  {
809  error() << e << eom;
811  }
812 
813  catch(const std::string &e)
814  {
815  error() << e << eom;
817  }
818 
819  catch(int e)
820  {
821  error() << "Numeric exception : " << e << eom;
823  }
824 
825  catch(const std::bad_alloc &)
826  {
827  error() << "Out of memory" << eom;
829  }
830 // NOLINTNEXTLINE(readability/fn_size)
831 }
832 
834  bool force)
835 {
836  if(function_pointer_removal_done && !force)
837  return;
838 
840 
841  status() << "Function Pointer Removal" << eom;
844  goto_model,
845  cmdline.isset("pointer-check"));
846  status() << "Virtual function removal" << eom;
848  status() << "Cleaning inline assembler statements" << eom;
850 }
851 
856 {
857  // Don't bother if we've already done a full function pointer
858  // removal.
860  {
861  return;
862  }
863 
864  status() << "Removing const function pointers only" << eom;
867  goto_model,
868  cmdline.isset("pointer-check"),
869  true); // abort if we can't resolve via const pointers
870 }
871 
873 {
875  return;
876 
878 
879  if(!cmdline.isset("inline"))
880  {
881  status() << "Partial Inlining" << eom;
883  }
884 }
885 
887 {
889  return;
890 
891  remove_returns_done=true;
892 
893  status() << "Removing returns" << eom;
895 }
896 
898 {
899  status() << "Reading GOTO program from `" << cmdline.args[0] << "'" << eom;
900 
903  throw 0;
904 
905  config.set(cmdline);
906 }
907 
909 {
910  optionst options;
911 
912  // disable simplify when adding various checks?
913  if(cmdline.isset("no-simplify"))
914  options.set_option("simplify", false);
915  else
916  options.set_option("simplify", true);
917 
918  // use assumptions instead of assertions?
919  if(cmdline.isset("assert-to-assume"))
920  options.set_option("assert-to-assume", true);
921  else
922  options.set_option("assert-to-assume", false);
923 
924  // all checks supported by goto_check
926 
927  // check assertions
928  if(cmdline.isset("no-assertions"))
929  options.set_option("assertions", false);
930  else
931  options.set_option("assertions", true);
932 
933  // use assumptions
934  if(cmdline.isset("no-assumptions"))
935  options.set_option("assumptions", false);
936  else
937  options.set_option("assumptions", true);
938 
939  // magic error label
940  if(cmdline.isset("error-label"))
941  options.set_option("error-label", cmdline.get_value("error-label"));
942 
943  // unwind loops
944  if(cmdline.isset("unwind"))
945  {
946  status() << "Unwinding loops" << eom;
947  options.set_option("unwind", cmdline.get_value("unwind"));
948  }
949 
950  // skip over selected loops
951  if(cmdline.isset("skip-loops"))
952  {
953  status() << "Adding gotos to skip loops" << eom;
954  if(skip_loops(
955  goto_model,
956  cmdline.get_value("skip-loops"),
958  throw 0;
959  }
960 
962 
963  // initialize argv with valid pointers
964  if(cmdline.isset("model-argc-argv"))
965  {
966  unsigned max_argc=
967  safe_string2unsigned(cmdline.get_value("model-argc-argv"));
968 
969  status() << "Adding up to " << max_argc
970  << " command line arguments" << eom;
971  if(model_argc_argv(
972  goto_model,
973  max_argc,
975  throw 0;
976  }
977 
978  if(cmdline.isset("remove-function-body"))
979  {
981  goto_model,
982  cmdline.get_values("remove-function-body"),
984  }
985 
986  // we add the library in some cases, as some analyses benefit
987 
988  if(cmdline.isset("add-library") ||
989  cmdline.isset("mm"))
990  {
991  if(cmdline.isset("show-custom-bitvector-analysis") ||
992  cmdline.isset("custom-bitvector-analysis"))
993  config.ansi_c.defines.push_back("__CPROVER_CUSTOM_BITVECTOR_ANALYSIS");
994 
995  // add the library
996  status() << "Adding CPROVER library (" << config.ansi_c.arch << ")" << eom;
1001  }
1002 
1003  // now do full inlining, if requested
1004  if(cmdline.isset("inline"))
1005  {
1007 
1008  if(cmdline.isset("show-custom-bitvector-analysis") ||
1009  cmdline.isset("custom-bitvector-analysis"))
1010  {
1014  }
1015 
1016  status() << "Performing full inlining" << eom;
1018  }
1019 
1020  if(cmdline.isset("show-custom-bitvector-analysis") ||
1021  cmdline.isset("custom-bitvector-analysis"))
1022  {
1023  status() << "Propagating Constants" << eom;
1024  constant_propagator_ait constant_propagator_ai(goto_model);
1026  }
1027 
1028  if(cmdline.isset("escape-analysis"))
1029  {
1033 
1034  // recalculate numbers, etc.
1036 
1037  status() << "Escape Analysis" << eom;
1038  escape_analysist escape_analysis;
1039  escape_analysis(goto_model);
1040  escape_analysis.instrument(goto_model);
1041 
1042  // inline added functions, they are often small
1044 
1045  // recalculate numbers, etc.
1047  }
1048 
1049  // verify and set invariants and pre/post-condition pairs
1050  if(cmdline.isset("apply-code-contracts"))
1051  {
1052  status() << "Applying Code Contracts" << eom;
1054  }
1055 
1056  // replace function pointers, if explicitly requested
1057  if(cmdline.isset("remove-function-pointers"))
1058  {
1060  }
1061  else if(cmdline.isset("remove-const-function-pointers"))
1062  {
1064  }
1065 
1066  if(cmdline.isset("replace-calls"))
1067  {
1069 
1070  replace_callst replace_calls;
1071  replace_calls(goto_model, cmdline.get_values("replace-calls"));
1072  }
1073 
1074  if(cmdline.isset("function-inline"))
1075  {
1076  std::string function=cmdline.get_value("function-inline");
1077  PRECONDITION(!function.empty());
1078 
1079  bool caching=!cmdline.isset("no-caching");
1080 
1082 
1083  status() << "Inlining calls of function `" << function << "'" << eom;
1084 
1085  if(!cmdline.isset("log"))
1086  {
1088  goto_model,
1089  function,
1091  true,
1092  caching);
1093  }
1094  else
1095  {
1096  std::string filename=cmdline.get_value("log");
1097  bool have_file=!filename.empty() && filename!="-";
1098 
1099  jsont result=
1101  goto_model,
1102  function,
1104  true,
1105  caching);
1106 
1107  if(have_file)
1108  {
1109 #ifdef _MSC_VER
1110  std::ofstream of(widen(filename));
1111 #else
1112  std::ofstream of(filename);
1113 #endif
1114  if(!of)
1115  throw "failed to open file "+filename;
1116 
1117  of << result;
1118  of.close();
1119  }
1120  else
1121  {
1122  std::cout << result << '\n';
1123  }
1124  }
1125 
1128  }
1129 
1130  if(cmdline.isset("partial-inline"))
1131  {
1133 
1134  status() << "Partial inlining" << eom;
1136 
1139  }
1140 
1141  if(cmdline.isset("remove-calls-no-body"))
1142  {
1143  status() << "Removing calls to functions without a body" << eom;
1144 
1145  remove_calls_no_bodyt remove_calls_no_body;
1146  remove_calls_no_body(goto_model.goto_functions);
1147 
1150  }
1151 
1152  if(cmdline.isset("constant-propagator"))
1153  {
1155 
1156  status() << "Propagating Constants" << eom;
1157 
1158  constant_propagator_ait constant_propagator_ai(goto_model);
1160  }
1161 
1162  // add generic checks, if needed
1163  goto_check(options, goto_model);
1164 
1165  // check for uninitalized local variables
1166  if(cmdline.isset("uninitialized-check"))
1167  {
1168  status() << "Adding checks for uninitialized local variables" << eom;
1170  }
1171 
1172  // check for maximum call stack size
1173  if(cmdline.isset("stack-depth"))
1174  {
1175  status() << "Adding check for maximum call stack size" << eom;
1176  stack_depth(
1177  goto_model,
1178  unsafe_string2unsigned(cmdline.get_value("stack-depth")));
1179  }
1180 
1181  // ignore default/user-specified initialization of variables with static
1182  // lifetime
1183  if(cmdline.isset("nondet-static"))
1184  {
1185  status() << "Adding nondeterministic initialization of static/global "
1186  "variables" << eom;
1188  }
1189 
1190  if(cmdline.isset("slice-global-inits"))
1191  {
1192  status() << "Slicing away initializations of unused global variables"
1193  << eom;
1195  }
1196 
1197  if(cmdline.isset("string-abstraction"))
1198  {
1201 
1202  status() << "String Abstraction" << eom;
1204  goto_model,
1206  }
1207 
1208  // some analyses require function pointer removal and partial inlining
1209 
1210  if(cmdline.isset("remove-pointers") ||
1211  cmdline.isset("race-check") ||
1212  cmdline.isset("mm") ||
1213  cmdline.isset("isr") ||
1214  cmdline.isset("concurrency"))
1215  {
1217 
1218  status() << "Pointer Analysis" << eom;
1219  value_set_analysist value_set_analysis(ns);
1220  value_set_analysis(goto_model.goto_functions);
1221 
1222  if(cmdline.isset("remove-pointers"))
1223  {
1224  // removing pointers
1225  status() << "Removing Pointers" << eom;
1226  remove_pointers(goto_model, value_set_analysis);
1227  }
1228 
1229  if(cmdline.isset("race-check"))
1230  {
1231  status() << "Adding Race Checks" << eom;
1232  race_check(value_set_analysis, goto_model);
1233  }
1234 
1235  if(cmdline.isset("mm"))
1236  {
1237  std::string mm=cmdline.get_value("mm");
1238  memory_modelt model;
1239 
1240  // strategy of instrumentation
1241  instrumentation_strategyt inst_strategy;
1242  if(cmdline.isset("one-event-per-cycle"))
1243  inst_strategy=one_event_per_cycle;
1244  else if(cmdline.isset("minimum-interference"))
1245  inst_strategy=min_interference;
1246  else if(cmdline.isset("read-first"))
1247  inst_strategy=read_first;
1248  else if(cmdline.isset("write-first"))
1249  inst_strategy=write_first;
1250  else if(cmdline.isset("my-events"))
1251  inst_strategy=my_events;
1252  else
1253  /* default: instruments all unsafe pairs */
1254  inst_strategy=all;
1255 
1256  const unsigned max_var=
1257  cmdline.isset("max-var")?
1259  const unsigned max_po_trans=
1260  cmdline.isset("max-po-trans")?
1261  unsafe_string2unsigned(cmdline.get_value("max-po-trans")):0;
1262 
1263  if(mm=="tso")
1264  {
1265  status() << "Adding weak memory (TSO) Instrumentation" << eom;
1266  model=TSO;
1267  }
1268  else if(mm=="pso")
1269  {
1270  status() << "Adding weak memory (PSO) Instrumentation" << eom;
1271  model=PSO;
1272  }
1273  else if(mm=="rmo")
1274  {
1275  status() << "Adding weak memory (RMO) Instrumentation" << eom;
1276  model=RMO;
1277  }
1278  else if(mm=="power")
1279  {
1280  status() << "Adding weak memory (Power) Instrumentation" << eom;
1281  model=Power;
1282  }
1283  else
1284  {
1285  error() << "Unknown weak memory model `" << mm << "'" << eom;
1286  model=Unknown;
1287  }
1288 
1290 
1291  if(cmdline.isset("force-loop-duplication"))
1292  loops=all_loops;
1293  if(cmdline.isset("no-loop-duplication"))
1294  loops=no_loop;
1295 
1296  if(model!=Unknown)
1297  weak_memory(
1298  model,
1299  value_set_analysis,
1300  goto_model,
1301  cmdline.isset("scc"),
1302  inst_strategy,
1303  !cmdline.isset("cfg-kill"),
1304  cmdline.isset("no-dependencies"),
1305  loops,
1306  max_var,
1307  max_po_trans,
1308  !cmdline.isset("no-po-rendering"),
1309  cmdline.isset("render-cluster-file"),
1310  cmdline.isset("render-cluster-function"),
1311  cmdline.isset("cav11"),
1312  cmdline.isset("hide-internals"),
1314  cmdline.isset("ignore-arrays"));
1315  }
1316 
1317  // Interrupt handler
1318  if(cmdline.isset("isr"))
1319  {
1320  status() << "Instrumenting interrupt handler" << eom;
1321  interrupt(
1322  value_set_analysis,
1323  goto_model,
1324  cmdline.get_value("isr"));
1325  }
1326 
1327  // Memory-mapped I/O
1328  if(cmdline.isset("mmio"))
1329  {
1330  status() << "Instrumenting memory-mapped I/O" << eom;
1331  mmio(value_set_analysis, goto_model);
1332  }
1333 
1334  if(cmdline.isset("concurrency"))
1335  {
1336  status() << "Sequentializing concurrency" << eom;
1337  concurrency(value_set_analysis, goto_model);
1338  }
1339  }
1340 
1341  if(cmdline.isset("interval-analysis"))
1342  {
1343  status() << "Interval analysis" << eom;
1345  }
1346 
1347  if(cmdline.isset("havoc-loops"))
1348  {
1349  status() << "Havocking loops" << eom;
1351  }
1352 
1353  if(cmdline.isset("k-induction"))
1354  {
1355  bool base_case=cmdline.isset("base-case");
1356  bool step_case=cmdline.isset("step-case");
1357 
1358  if(step_case && base_case)
1359  throw "please specify only one of --step-case and --base-case";
1360  else if(!step_case && !base_case)
1361  throw "please specify one of --step-case and --base-case";
1362 
1363  unsigned k=unsafe_string2unsigned(cmdline.get_value("k-induction"));
1364 
1365  if(k==0)
1366  throw "please give k>=1";
1367 
1368  status() << "Instrumenting k-induction for k=" << k << ", "
1369  << (base_case?"base case":"step case") << eom;
1370 
1371  k_induction(goto_model, base_case, step_case, k);
1372  }
1373 
1374  if(cmdline.isset("function-enter"))
1375  {
1376  status() << "Function enter instrumentation" << eom;
1378  goto_model,
1379  cmdline.get_value("function-enter"));
1380  }
1381 
1382  if(cmdline.isset("function-exit"))
1383  {
1384  status() << "Function exit instrumentation" << eom;
1385  function_exit(
1386  goto_model,
1387  cmdline.get_value("function-exit"));
1388  }
1389 
1390  if(cmdline.isset("branch"))
1391  {
1392  status() << "Branch instrumentation" << eom;
1393  branch(
1394  goto_model,
1395  cmdline.get_value("branch"));
1396  }
1397 
1398  // add failed symbols
1400 
1401  // recalculate numbers, etc.
1403 
1404  // add loop ids
1406 
1407  // label the assertions
1409 
1410  // nondet volatile?
1411  if(cmdline.isset("nondet-volatile"))
1412  {
1413  status() << "Making volatile variables non-deterministic" << eom;
1415  }
1416 
1417  // reachability slice?
1418  if(cmdline.isset("reachability-slice"))
1419  {
1421 
1422  status() << "Performing a reachability slice" << eom;
1423  if(cmdline.isset("property"))
1425  else
1427  }
1428 
1429  // full slice?
1430  if(cmdline.isset("full-slice"))
1431  {
1434 
1435  status() << "Performing a full slice" << eom;
1436  if(cmdline.isset("property"))
1438  else
1440  }
1441 
1442  // splice option
1443  if(cmdline.isset("splice-call"))
1444  {
1445  status() << "Performing call splicing" << eom;
1446  std::string callercallee=cmdline.get_value("splice-call");
1447  if(splice_call(
1449  callercallee,
1452  throw 0;
1453  }
1454 
1455  if(cmdline.isset("generate-function-body"))
1456  {
1457  auto generate_implementation = generate_function_bodies_factory(
1458  cmdline.get_value("generate-function-body-options"),
1460  *message_handler);
1462  std::regex(cmdline.get_value("generate-function-body")),
1463  *generate_implementation,
1464  goto_model,
1465  *message_handler);
1466  }
1467 
1468  // aggressive slicer
1469  if(cmdline.isset("aggressive-slice"))
1470  {
1472 
1473  status() << "Slicing away initializations of unused global variables"
1474  << eom;
1476 
1477  status() << "Performing an aggressive slice" << eom;
1478  aggressive_slicert aggressive_slicer(goto_model, get_message_handler());
1479 
1480  if(cmdline.isset("aggressive-slice-call-depth"))
1481  aggressive_slicer.call_depth =
1482  safe_string2unsigned(cmdline.get_value("aggressive-slice-call-depth"));
1483 
1484  if(cmdline.isset("aggressive-slice-preserve-function"))
1485  aggressive_slicer.preserve_functions(
1486  cmdline.get_values("aggressive-slice-preserve-function"));
1487 
1488  if(cmdline.isset("property"))
1489  aggressive_slicer.user_specified_properties =
1490  cmdline.get_values("property");
1491 
1492  if(cmdline.isset("aggressive-slice-preserve-functions-containing"))
1493  aggressive_slicer.name_snippets =
1494  cmdline.get_values("aggressive-slice-preserve-functions-containing");
1495 
1496  aggressive_slicer.preserve_all_direct_paths =
1497  cmdline.isset("aggressive-slice-preserve-all-direct-paths");
1498 
1499  aggressive_slicer.doit();
1500 
1501  status() << "Performing a reachability slice" << eom;
1502  if(cmdline.isset("property"))
1504  else
1506  }
1507 
1508  // recalculate numbers, etc.
1510 }
1511 
1514 {
1515  // clang-format off
1516  std::cout << '\n' << banner_string("Goto-Instrument", CBMC_VERSION) << '\n'
1517  <<
1518  "* * Copyright (C) 2008-2013 * *\n"
1519  "* * Daniel Kroening * *\n"
1520  "* * kroening@kroening.com * *\n"
1521  "\n"
1522  "Usage: Purpose:\n"
1523  "\n"
1524  " goto-instrument [-?] [-h] [--help] show help\n"
1525  " goto-instrument in out perform instrumentation\n"
1526  "\n"
1527  "Main options:\n"
1528  " --document-properties-html generate HTML property documentation\n"
1529  " --document-properties-latex generate Latex property documentation\n"
1530  " --dump-c generate C source\n"
1531  " --dump-cpp generate C++ source\n"
1532  " --dot generate CFG graph in DOT format\n"
1533  " --interpreter do concrete execution\n"
1534  "\n"
1535  "Diagnosis:\n"
1536  " --show-loops show the loops in the program\n"
1538  " --show-symbol-table show loaded symbol table\n"
1539  " --list-symbols list symbols with type information\n"
1542  " --drop-unused-functions drop functions trivially unreachable from main function\n" // NOLINT(*)
1543  " --print-internal-representation\n" // NOLINTNEXTLINE(*)
1544  " show verbose internal representation of the program\n"
1545  " --list-undefined-functions list functions without body\n"
1546  " --show-struct-alignment show struct members that might be concurrently accessed\n" // NOLINT(*)
1547  " --show-natural-loops show natural loop heads\n"
1548  // NOLINTNEXTLINE(whitespace/line_length)
1549  " --list-calls-args list all function calls with their arguments\n"
1550  " --call-graph show graph of function calls\n"
1551  // NOLINTNEXTLINE(whitespace/line_length)
1552  " --reachable-call-graph show graph of function calls potentially reachable from main function\n"
1554  // NOLINTNEXTLINE(whitespace/line_length)
1555  " --show-threaded show instructions that may be executed by more than one thread\n"
1556  " --show-local-safe-pointers show pointer expressions that are trivially dominated by a not-null check\n" // NOLINT(*)
1557  " --show-safe-dereferences show pointer expressions that are trivially dominated by a not-null check\n" // NOLINT(*)
1558  " *and* used as a dereference operand\n" // NOLINT(*)
1559  "\n"
1560  "Safety checks:\n"
1561  " --no-assertions ignore user assertions\n"
1563  " --uninitialized-check add checks for uninitialized locals (experimental)\n" // NOLINT(*)
1564  " --error-label label check that label is unreachable\n"
1565  " --stack-depth n add check that call stack size of non-inlined functions never exceeds n\n" // NOLINT(*)
1566  " --race-check add floating-point data race checks\n"
1567  "\n"
1568  "Semantic transformations:\n"
1569  " --nondet-volatile makes reads from volatile variables non-deterministic\n" // NOLINT(*)
1570  " --unwind <n> unwinds the loops <n> times\n"
1571  " --unwindset L:B,... unwind loop L with a bound of B\n"
1572  " --unwindset-file <file> read unwindset from file\n"
1573  " --partial-loops permit paths with partial loops\n"
1574  " --unwinding-assertions generate unwinding assertions\n"
1575  " --continue-as-loops add loop for remaining iterations after unwound part\n" // NOLINT(*)
1576  " --isr <function> instruments an interrupt service routine\n"
1577  " --mmio instruments memory-mapped I/O\n"
1578  " --nondet-static add nondeterministic initialization of variables with static lifetime\n" // NOLINT(*)
1579  " --check-invariant function instruments invariant checking function\n"
1580  " --remove-pointers converts pointer arithmetic to base+offset expressions\n" // NOLINT(*)
1581  " --splice-call caller,callee prepends a call to callee in the body of caller\n" // NOLINT(*)
1582  " --undefined-function-is-assume-false\n"
1583  // NOLINTNEXTLINE(whitespace/line_length)
1584  " convert each call to an undefined function to assume(false)\n"
1586  "\n"
1587  "Loop transformations:\n"
1588  " --k-induction <k> check loops with k-induction\n"
1589  " --step-case k-induction: do step-case\n"
1590  " --base-case k-induction: do base-case\n"
1591  " --havoc-loops over-approximate all loops\n"
1592  " --accelerate add loop accelerators\n"
1593  " --skip-loops <loop-ids> add gotos to skip selected loops during execution\n" // NOLINT(*)
1594  "\n"
1595  "Memory model instrumentations:\n"
1596  " --mm <tso,pso,rmo,power> instruments a weak memory model\n"
1597  " --scc detects critical cycles per SCC (one thread per SCC)\n" // NOLINT(*)
1598  " --one-event-per-cycle only instruments one event per cycle\n"
1599  " --minimum-interference instruments an optimal number of events\n"
1600  " --my-events only instruments events whose ids appear in inst.evt\n" // NOLINT(*)
1601  " --cfg-kill enables symbolic execution used to reduce spurious cycles\n" // NOLINT(*)
1602  " --no-dependencies no dependency analysis\n"
1603  // NOLINTNEXTLINE(whitespace/line_length)
1604  " --no-po-rendering no representation of the threads in the dot\n"
1605  " --render-cluster-file clusterises the dot by files\n"
1606  " --render-cluster-function clusterises the dot by functions\n"
1607  "\n"
1608  "Slicing:\n"
1609  " --reachability-slice slice away instructions that can't reach assertions\n" // NOLINT(*)
1610  " --full-slice slice away instructions that don't affect assertions\n" // NOLINT(*)
1611  " --property id slice with respect to specific property only\n" // NOLINT(*)
1612  " --slice-global-inits slice away initializations of unused global variables\n" // NOLINT(*)
1613  " --aggressive-slice remove bodies of any functions not on the shortest path between\n" // NOLINT(*)
1614  " the start function and the function containing the property(s)\n" // NOLINT(*)
1615  " --aggressive-slice-call-depth <n>\n"
1616  " used with aggressive-slice, preserves all functions within <n> function calls\n" // NOLINT(*)
1617  " of the functions on the shortest path\n"
1618  " --aggressive-slice-preserve-function <f>\n"
1619  " force the aggressive slicer to preserve function <f>\n" // NOLINT(*)
1620  " --aggressive-slice-preserve-function containing <f>\n"
1621  " force the aggressive slicer to preserve all functions with names containing <f>\n" // NOLINT(*)
1622  "--aggressive-slice-preserve-all-direct-paths \n"
1623  " force aggressive slicer to preserve all direct paths\n" // NOLINT(*)
1624  "\n"
1625  "Further transformations:\n"
1626  " --constant-propagator propagate constants and simplify expressions\n" // NOLINT(*)
1627  " --inline perform full inlining\n"
1628  " --partial-inline perform partial inlining\n"
1629  " --function-inline <function> transitively inline all calls <function> makes\n" // NOLINT(*)
1630  " --no-caching disable caching of intermediate results during transitive function inlining\n" // NOLINT(*)
1631  " --log <file> log in json format which code segments were inlined, use with --function-inline\n" // NOLINT(*)
1632  " --remove-function-pointers replace function pointers by case statement over function calls\n" // NOLINT(*)
1635  " --add-library add models of C library functions\n"
1636  " --model-argc-argv <n> model up to <n> command line arguments\n"
1637  // NOLINTNEXTLINE(whitespace/line_length)
1638  " --remove-function-body <f> remove the implementation of function <f> (may be repeated)\n"
1640  "\n"
1641  "Other options:\n"
1642  " --no-system-headers with --dump-c/--dump-cpp: generate C source expanding libc includes\n" // NOLINT(*)
1643  " --use-all-headers with --dump-c/--dump-cpp: generate C source with all includes\n" // NOLINT(*)
1644  " --harness with --dump-c/--dump-cpp: include input generator in output\n" // NOLINT(*)
1645  " --version show version and exit\n"
1646  HELP_FLUSH
1647  " --xml-ui use XML-formatted output\n"
1648  " --json-ui use JSON-formatted output\n"
1650  "\n";
1651  // clang-format on
1652 }
void do_indirect_call_and_rtti_removal(bool force=false)
irep_idt name
The unique identifier.
Definition: symbol.h:43
const std::list< std::string > & get_values(const std::string &option) const
Definition: cmdline.cpp:110
Loop Acceleration.
Detection for Uninitialized Local Variables.
void show_loop_ids(ui_message_handlert::uit ui, const goto_modelt &goto_model)
Definition: loop_ids.cpp:21
struct configt::ansi_ct ansi_c
jsont output_log_json() const
Definition: unwind.h:70
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...
Field-insensitive, location-sensitive bitvector analysis.
void string_abstraction(symbol_tablet &symbol_table, message_handlert &message_handler, goto_programt &dest)
Show Value Sets.
Function Entering and Exiting.
Over-approximate Concurrency for Threaded Goto Programs.
void undefined_function_abort_path(goto_modelt &goto_model)
Skip over selected loops by adding gotos.
void output_safe_dereferences(std::ostream &stream, const goto_programt &program)
Output safely dereferenced expressions per instruction in human-readable format.
Interval Analysis.
Remove initializations of unused global variables.
Initialize command line arguments.
void mutex_init_instrumentation(const symbol_tablet &symbol_table, goto_programt &goto_program, typet lock_type)
Remove Indirect Function Calls.
std::wstring widen(const char *s)
Definition: unicode.cpp:46
instrumentation_strategyt
Definition: wmm.h:26
void concurrency(value_setst &value_sets, goto_modelt &goto_model)
Remove Virtual Function (Method) Calls.
Non-graph-based representation of the class hierarchy.
void parameter_assignments(symbol_tablet &symbol_table, goto_functionst &goto_functions)
removes returns
void remove_pointers(goto_programt &goto_program, symbol_tablet &symbol_table, value_setst &value_sets)
Command Line Parsing.
void list_undefined_functions(const goto_modelt &goto_model, std::ostream &os)
Field-Sensitive Program Dependence Analysis, Litvak et al., FSE 2010.
static bool skip_loops(goto_programt &goto_program, const loop_idst &loop_ids, messaget &message)
Definition: skip_loops.cpp:24
uit get_ui() const
Definition: ui_message.h:37
virtual int main()
Field-sensitive, location-insensitive points-to analysis.
unsigned unsafe_string2unsigned(const std::string &str, int base)
Definition: string2int.cpp:69
void compute_loop_numbers()
Definition: wmm.h:23
Definition: wmm.h:39
Show the symbol table.
Remove function definition.
Definition: json.h:23
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:78
void print_struct_alignment_problems(const symbol_tablet &symbol_table, std::ostream &out)
std::list< std::string > defines
Definition: config.h:120
Definition: ai.h:294
Read Goto Programs.
#define HELP_SHOW_CLASS_HIERARCHY
Branch Instrumentation.
Remove calls to functions without a body.
Function Call Graphs.
Dump C from Goto Program.
std::string get_value(char option) const
Definition: cmdline.cpp:45
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: wmm.h:22
void remove_unused_functions(goto_modelt &goto_model, message_handlert &message_handler)
function_mapt function_map
Race Detection for Threaded Goto Programs.
Field-insensitive, location-sensitive bitvector analysis.
Stack depth checks.
Memory-mapped I/O Instrumentation for Goto Programs.
void mmio(value_setst &value_sets, const symbol_tablet &symbol_table, goto_programt &goto_program)
Definition: mmio.cpp:24
Interpreter for GOTO Programs.
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
void show_uninitialized(const goto_modelt &goto_model, std::ostream &out)
Pointer Dereferencing.
jsont goto_function_inline_and_log(goto_modelt &goto_model, const irep_idt function, message_handlert &message_handler, bool adjust_function, bool caching)
Definition: wmm.h:30
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
void show_goto_functions(const namespacet &ns, message_handlert &message_handler, ui_message_handlert::uit ui, const goto_functionst &goto_functions, bool list_only)
Weak Memory Instrumentation for Threaded Goto Programs.
String Abstraction.
configt config
Definition: config.cpp:23
virtual int doit()
invoke main modules
Remove &#39;asm&#39; statements by compiling into suitable standard code.
void nondet_volatile(symbol_tablet &symbol_table, goto_programt &goto_program)
void remove_virtual_functions(const symbol_table_baset &symbol_table, goto_functionst &goto_functions)
void print_path_lengths(const goto_modelt &goto_model)
Definition: count_eloc.cpp:81
loop_strategyt
Definition: wmm.h:36
Documentation of Properties.
k-induction
void cprover_c_library_factory(const std::set< irep_idt > &functions, symbol_tablet &symbol_table, message_handlert &message_handler)
#define CPROVER_EXIT_SUCCESS
Success indicates the required analysis has been performed without error.
Definition: exit_codes.h:16
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.
unwind_strategyt
Definition: unwind.h:27
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...
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.
Set the properties to check.
#define HELP_GOTO_CHECK
Definition: goto_check.h:42
Class Hierarchy.
Unused function removal.
virtual void output(const namespacet &ns, const goto_functionst &goto_functions, std::ostream &out) const
Definition: ai.cpp:24
bool set(const cmdlinet &cmdline)
Definition: config.cpp:738
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:1400
void dot(const goto_modelt &src, std::ostream &out)
Definition: dot.cpp:354
void horn_encoding(const goto_modelt &, std::ostream &)
void show_symbol_table_brief(const symbol_tablet &symbol_table, ui_message_handlert::uit ui)
bool read_goto_binary(const std::string &filename, goto_modelt &dest, message_handlert &message_handler)
void accelerate_functions(goto_modelt &goto_model, message_handlert &message_handler, bool use_z3)
Definition: accelerate.cpp:649
void check(const goto_modelt &, bool xml, std::ostream &)
void interpreter(const goto_modelt &goto_model, message_handlert &message_handler)
#define HELP_TIMESTAMP
Definition: timestamper.h:14
void show_symbol_table(const symbol_tablet &symbol_table, ui_message_handlert::uit ui)
argst args
Definition: cmdline.h:37
virtual bool isset(char option) const
Definition: cmdline.cpp:27
memory_modelt
Definition: wmm.h:17
bool write_goto_binary(std::ostream &out, const goto_modelt &goto_model, int version)
Writes a goto program to disc.
Value Set Propagation.
String Abstraction.
#define HELP_SHOW_PROPERTIES
void output_xml(std::ostream &out) const
Definition: call_graph.cpp:281
Nondeterministic initialization of certain global scope variables.
void list_eloc(const goto_modelt &goto_model)
Definition: count_eloc.cpp:64
#define HELP_FLUSH
Definition: ui_message.h:108
void output_dot(std::ostream &out) const
Definition: call_graph.cpp:254
std::list< std::string > name_snippets
#define HELP_REPLACE_CALLS
Definition: replace_calls.h:50
void function_enter(goto_modelt &goto_model, const irep_idt &id)
Definition: function.cpp:77
Dump Goto-Program as DOT Graph.
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...
mstreamt & error() const
Definition: message.h:302
irep_idt arch
Definition: config.h:84
TO_BE_DOCUMENTED.
Definition: namespace.h:74
Function Inlining.
Loop IDs.
Definition: wmm.h:21
#define PRECONDITION(CONDITION)
Definition: invariant.h:242
void slice_global_inits(goto_modelt &goto_model)
bool remove_function_pointers(message_handlert &_message_handler, symbol_tablet &symbol_table, const goto_functionst &goto_functions, goto_programt &goto_program, bool add_safety_assertion, bool only_remove_const_fps)
Field-insensitive, location-sensitive, over-approximative escape analysis.
void parse_unwindset_file(const std::string &file_name)
Definition: unwindset.cpp:85
void restore_returns(goto_modelt &goto_model)
restores return statements
void output(std::ostream &out, const goto_functiont &goto_function, const namespacet &ns) const
void full_slicer(goto_functionst &goto_functions, const namespacet &ns, slicing_criteriont &criterion)
Volatile Variables.
static call_grapht create_from_root_function(const goto_modelt &model, const irep_idt &root, bool collect_callsites)
Definition: call_graph.h:31
void doit()
Removes the body of all functions except those on the shortest path or functions that are reachable f...
void cprover_cpp_library_factory(const std::set< irep_idt > &functions, symbol_tablet &symbol_table, message_handlert &message_handler)
Remove function returns.
void property_slicer(goto_functionst &goto_functions, const namespacet &ns, const std::list< std::string > &properties)
Havoc Loops.
void show_value_sets(ui_message_handlert::uit ui, const goto_modelt &goto_model, const value_set_analysist &value_set_analysis)
std::string banner_string(const std::string &front_end, const std::string &version)
Loop unwinding.
void output(std::ostream &stream, const goto_programt &program)
Output non-null expressions per instruction in human-readable format.
#define PARSE_OPTIONS_GOTO_CHECK(cmdline, options)
Definition: goto_check.h:56
void output_dot(std::ostream &out) const
Definition: graph.h:914
void remove_returns(symbol_table_baset &symbol_table, goto_functionst &goto_functions)
removes returns
void output(std::ostream &out) const
Definition: call_graph.cpp:271
void goto_check(const namespacet &ns, const optionst &options, const irep_idt &mode, goto_functionst::goto_functiont &goto_function)
#define HELP_REMOVE_CONST_FUNCTION_POINTERS
void document_properties_latex(const goto_modelt &goto_model, std::ostream &out)
void parse_unwindset(const std::string &unwindset)
Definition: unwindset.cpp:24
#define HELP_GOTO_PROGRAM_STATS
Definition: count_eloc.h:30
void document_properties_html(const goto_modelt &goto_model, std::ostream &out)
Interrupt Instrumentation for Goto Programs.
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70
void remove_asm(goto_functionst &goto_functions, symbol_tablet &symbol_table)
removes assembler
Definition: remove_asm.cpp:482
void show_natural_loops(const goto_modelt &goto_model, std::ostream &out)
Range-based reaching definitions analysis (following Field- Sensitive Program Dependence Analysis...
Show program locations.
Verify and use annotated invariants and pre/post-conditions.
Definition: wmm.h:32
unsigned safe_string2unsigned(const std::string &str, int base)
Definition: string2int.cpp:54
#define HELP_REMOVE_CALLS_NO_BODY
void havoc_loops(goto_modelt &goto_model)
void output(std::ostream &out) const
Definition: points_to.cpp:36
Interval Domain.
std::unique_ptr< generate_function_bodiest > generate_function_bodies_factory(const std::string &options, const symbol_tablet &symbol_table, message_handlert &message_handler)
Create the type that actually generates the functions.
typet type
Type of symbol.
Definition: symbol.h:34
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 A list of currently accepted command line argumen...
message_handlert & get_message_handler()
Definition: message.h:153
std::list< std::string > user_specified_properties
Goto Programs with Functions.
static irep_idt entry_point()
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &it) const
Output a single instruction.
Document and give macros for the exit codes of CPROVER binaries.
Definition: wmm.h:19
mstreamt & result() const
Definition: message.h:312
void show_call_sequences(const irep_idt &caller, const goto_programt &goto_program)
void k_induction(goto_modelt &goto_model, bool base_case, bool step_case, unsigned k)
mstreamt & status() const
Definition: message.h:317
#define HELP_SHOW_GOTO_FUNCTIONS
const char * CBMC_VERSION
Definition: version.cpp:1
virtual void help()
display command line help
void goto_inline(goto_modelt &goto_model, message_handlert &message_handler, bool adjust_function)
Definition: goto_inline.cpp:24
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...
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:86
Constant propagation.
Harnessing for goto functions.
#define CPROVER_EXIT_CONVERSION_FAILED
Failure to convert / write to another format.
Definition: exit_codes.h:58
void check_call_sequence(const goto_modelt &goto_model)
void show_class_hierarchy(const class_hierarchyt &hierarchy, message_handlert &message_handler, ui_message_handlert::uit ui, bool children_only)
Output the class hierarchy.
Definition: wmm.h:20
Slicing.
void add_uninitialized_locals_assertions(goto_modelt &goto_model)
Handling of functions without body.
Local safe pointer analysis.
void weak_memory(memory_modelt model, value_setst &value_sets, goto_modelt &goto_model, bool SCC, instrumentation_strategyt event_strategy, bool no_cfg_kill, bool no_dependencies, loop_strategyt duplicate_body, unsigned input_max_var, unsigned input_max_po_trans, bool render_po, bool render_file, bool render_function, bool cav11_option, bool hide_internals, message_handlert &message_handler, bool ignore_arrays)
#define HELP_REPLACE_FUNCTION_BODY
void count_eloc(const goto_modelt &goto_model)
Definition: count_eloc.cpp:50
A very simple, cheap analysis to determine when dereference operations are trivially guarded by a che...
goto_programt & goto_program
Definition: cover.cpp:63
void interrupt(value_setst &value_sets, const symbol_tablet &symbol_table, goto_programt &goto_program, const symbol_exprt &interrupt_handler, const rw_set_baset &isr_rw_set)
Definition: interrupt.cpp:53
void race_check(value_setst &value_sets, symbol_tablet &symbol_table, goto_programt &goto_program, w_guardst &w_guards)
Definition: race_check.cpp:161
Alignment Checks.
void interval_analysis(goto_modelt &goto_model)
Expression to hold a symbol (variable)
Definition: std_expr.h:90
static void list_calls_and_arguments(const namespacet &ns, const goto_programt &goto_program)
Horn-clause Encoding.
Show the properties.
void code_contracts(goto_modelt &goto_model)
#define CPROVER_EXIT_EXCEPTION_GOTO_INSTRUMENT
Definition: exit_codes.h:38
void show_locations(ui_message_handlert::uit ui, const irep_idt function_id, const goto_programt &goto_program)
Definition: wmm.h:40
Compute natural loops in a goto_function.
void set_option(const std::string &option, const bool value)
Definition: options.cpp:24
void do_remove_const_function_pointers_only()
Remove function pointers that can be resolved by analysing const variables (i.e.
Memory-mapped I/O Instrumentation for Goto Programs.
Encoding for Threaded Goto Programs.
The aggressive slicer removes the body of all the functions except those on the shortest path...
void parse_unwind(const std::string &unwind)
Definition: unwindset.cpp:18
void instrument(goto_modelt &)
Program Transformation.
#define forall_goto_functions(it, functions)
void output_dot(std::ostream &) const
Output class hierarchy in Graphviz DOT format.
void function_exit(goto_modelt &goto_model, const irep_idt &id)
Definition: function.cpp:103
#define CPROVER_EXIT_USAGE_ERROR
A usage error is returned when the command line is invalid or conflicting.
Definition: exit_codes.h:28
Field-insensitive, location-sensitive, over-approximative escape analysis.
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:735
Add parameter assignments.
message_handlert * message_handler
Definition: message.h:342
void label_properties(goto_modelt &goto_model)
Write GOTO binaries.
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
Definition: namespace.cpp:136
void print_global_state_size(const goto_modelt &goto_model)
Definition: count_eloc.cpp:149
void nondet_static(const namespacet &ns, goto_functionst &goto_functions, const irep_idt &fct_name)
void branch(goto_modelt &goto_model, const irep_idt &id)
Definition: branch.cpp:19
void thread_exit_instrumentation(goto_programt &goto_program)
Definition: wmm.h:28
Race Detection for Threaded Goto Programs.
void show_properties(const namespacet &ns, const irep_idt &identifier, message_handlert &message_handler, ui_message_handlert::uit ui, const goto_programt &goto_program)
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
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:1418
void stack_depth(goto_programt &goto_program, const symbol_exprt &symbol, const int i_depth, const exprt &max_depth)
Definition: stack_depth.cpp:43