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/string2int.h>
20 #include <util/unicode.h>
21 #include <util/json.h>
22 #include <util/exit_codes.h>
23 
38 #include <goto-programs/loop_ids.h>
46 
51 
52 #include <analyses/natural_loops.h>
57 #include <analyses/call_graph.h>
63 #include <analyses/is_threaded.h>
64 
65 #include <ansi-c/cprover_library.h>
66 #include <cpp/cprover_library.h>
67 
68 #include "document_properties.h"
69 #include "uninitialized.h"
70 #include "full_slicer.h"
71 #include "reachability_slicer.h"
72 #include "show_locations.h"
73 #include "points_to.h"
74 #include "alignment_checks.h"
75 #include "race_check.h"
76 #include "nondet_volatile.h"
77 #include "interrupt.h"
78 #include "mmio.h"
79 #include "stack_depth.h"
80 #include "nondet_static.h"
81 #include "rw_set.h"
82 #include "concurrency.h"
83 #include "dump_c.h"
84 #include "dot.h"
85 #include "havoc_loops.h"
86 #include "k_induction.h"
87 #include "function.h"
88 #include "branch.h"
89 #include "wmm/weak_memory.h"
90 #include "call_sequences.h"
91 #include "accelerate/accelerate.h"
92 #include "horn_encoding.h"
93 #include "thread_instrumentation.h"
94 #include "skip_loops.h"
95 #include "code_contracts.h"
96 #include "unwind.h"
97 #include "model_argc_argv.h"
98 #include "undefined_functions.h"
99 #include "remove_function.h"
100 #include "splice_call.h"
101 
104 {
105  if(cmdline.isset("version"))
106  {
107  std::cout << CBMC_VERSION << '\n';
108  return CPROVER_EXIT_SUCCESS;
109  }
110 
111  if(cmdline.args.size()!=1 && cmdline.args.size()!=2)
112  {
113  help();
115  }
116 
119 
120  try
121  {
123 
125 
127 
128  {
129  bool unwind_given=cmdline.isset("unwind");
130  bool unwindset_given=cmdline.isset("unwindset");
131  bool unwindset_file_given=cmdline.isset("unwindset-file");
132 
133  if(unwindset_given && unwindset_file_given)
134  throw "only one of --unwindset and --unwindset-file supported at a "
135  "time";
136 
137  if(unwind_given || unwindset_given || unwindset_file_given)
138  {
139  unwindsett unwindset;
140 
141  if(unwind_given)
142  unwindset.parse_unwind(cmdline.get_value("unwind"));
143 
144  if(unwindset_file_given)
145  unwindset.parse_unwindset_file(cmdline.get_value("unwindset-file"));
146 
147  if(unwindset_given)
148  unwindset.parse_unwindset(cmdline.get_value("unwindset"));
149 
150  bool unwinding_assertions=cmdline.isset("unwinding-assertions");
151  bool partial_loops=cmdline.isset("partial-loops");
152  bool continue_as_loops=cmdline.isset("continue-as-loops");
153 
154  if(unwinding_assertions+partial_loops+continue_as_loops>1)
155  throw "more than one of --unwinding-assertions,--partial-loops,"
156  "--continue-as-loops selected";
157 
158  goto_unwindt::unwind_strategyt unwind_strategy=
160 
161  if(unwinding_assertions)
162  {
164  }
165  else if(partial_loops)
166  {
168  }
169  else if(continue_as_loops)
170  {
172  }
173 
174  goto_unwindt goto_unwind;
175  goto_unwind(goto_model, unwindset, unwind_strategy);
176 
177  if(cmdline.isset("log"))
178  {
179  std::string filename=cmdline.get_value("log");
180  bool have_file=!filename.empty() && filename!="-";
181 
182  jsont result=goto_unwind.output_log_json();
183 
184  if(have_file)
185  {
186 #ifdef _MSC_VER
187  std::ofstream of(widen(filename));
188 #else
189  std::ofstream of(filename);
190 #endif
191  if(!of)
192  throw "failed to open file "+filename;
193 
194  of << result;
195  of.close();
196  }
197  else
198  {
199  std::cout << result << '\n';
200  }
201  }
202 
203  // goto_unwind holds references to instructions, only do remove_skip
204  // after having generated the log above
206  }
207  }
208 
209  if(cmdline.isset("show-threaded"))
210  {
212 
213  is_threadedt is_threaded(goto_model);
214 
216  {
217  std::cout << "////\n";
218  std::cout << "//// Function: " << f_it->first << '\n';
219  std::cout << "////\n\n";
220 
221  const goto_programt &goto_program=f_it->second.body;
222 
224  {
225  goto_program.output_instruction(ns, "", std::cout, *i_it);
226  std::cout << "Is threaded: " << (is_threaded(i_it)?"True":"False")
227  << "\n\n";
228  }
229  }
230 
231  return CPROVER_EXIT_SUCCESS;
232  }
233 
234  if(cmdline.isset("show-value-sets"))
235  {
237 
238  // recalculate numbers, etc.
240 
241  status() << "Pointer Analysis" << eom;
243  value_set_analysist value_set_analysis(ns);
244  value_set_analysis(goto_model.goto_functions);
245  show_value_sets(get_ui(), goto_model, value_set_analysis);
246  return CPROVER_EXIT_SUCCESS;
247  }
248 
249  if(cmdline.isset("show-global-may-alias"))
250  {
254 
255  // recalculate numbers, etc.
257 
258  global_may_alias_analysist global_may_alias_analysis;
259  global_may_alias_analysis(goto_model);
260  global_may_alias_analysis.output(goto_model, std::cout);
261 
262  return CPROVER_EXIT_SUCCESS;
263  }
264 
265  if(cmdline.isset("show-local-bitvector-analysis"))
266  {
269 
270  // recalculate numbers, etc.
272 
274 
276  {
277  local_bitvector_analysist local_bitvector_analysis(it->second);
278  std::cout << ">>>>\n";
279  std::cout << ">>>> " << it->first << '\n';
280  std::cout << ">>>>\n";
281  local_bitvector_analysis.output(std::cout, it->second, ns);
282  std::cout << '\n';
283  }
284 
285  return CPROVER_EXIT_SUCCESS;
286  }
287 
288  if(cmdline.isset("show-custom-bitvector-analysis"))
289  {
293 
295 
296  if(!cmdline.isset("inline"))
297  {
300  }
301 
302  // recalculate numbers, etc.
304 
305  custom_bitvector_analysist custom_bitvector_analysis;
306  custom_bitvector_analysis(goto_model);
307  custom_bitvector_analysis.output(goto_model, std::cout);
308 
309  return CPROVER_EXIT_SUCCESS;
310  }
311 
312  if(cmdline.isset("show-escape-analysis"))
313  {
317 
318  // recalculate numbers, etc.
320 
321  escape_analysist escape_analysis;
322  escape_analysis(goto_model);
323  escape_analysis.output(goto_model, std::cout);
324 
325  return CPROVER_EXIT_SUCCESS;
326  }
327 
328  if(cmdline.isset("custom-bitvector-analysis"))
329  {
333 
335 
336  if(!cmdline.isset("inline"))
337  {
340  }
341 
342  // recalculate numbers, etc.
344 
346 
347  custom_bitvector_analysist custom_bitvector_analysis;
348  custom_bitvector_analysis(goto_model);
349  custom_bitvector_analysis.check(
350  goto_model,
351  cmdline.isset("xml-ui"),
352  std::cout);
353 
354  return CPROVER_EXIT_SUCCESS;
355  }
356 
357  if(cmdline.isset("show-points-to"))
358  {
360 
361  // recalculate numbers, etc.
363 
365 
366  status() << "Pointer Analysis" << eom;
367  points_tot points_to;
368  points_to(goto_model);
369  points_to.output(std::cout);
370  return CPROVER_EXIT_SUCCESS;
371  }
372 
373  if(cmdline.isset("show-intervals"))
374  {
376 
377  // recalculate numbers, etc.
379 
380  status() << "Interval Analysis" << eom;
384  interval_analysis.output(goto_model, std::cout);
385  return CPROVER_EXIT_SUCCESS;
386  }
387 
388  if(cmdline.isset("show-call-sequences"))
389  {
392  return CPROVER_EXIT_SUCCESS;
393  }
394 
395  if(cmdline.isset("check-call-sequence"))
396  {
399  return CPROVER_EXIT_SUCCESS;
400  }
401 
402  if(cmdline.isset("list-calls-args"))
403  {
405 
407 
408  return CPROVER_EXIT_SUCCESS;
409  }
410 
411  if(cmdline.isset("show-rw-set"))
412  {
414 
415  if(!cmdline.isset("inline"))
416  {
418 
419  // recalculate numbers, etc.
421  }
422 
423  status() << "Pointer Analysis" << eom;
424  value_set_analysist value_set_analysis(ns);
425  value_set_analysis(goto_model.goto_functions);
426 
427  const symbolt &symbol=ns.lookup(ID_main);
428  symbol_exprt main(symbol.name, symbol.type);
429 
430  std::cout <<
431  rw_set_functiont(value_set_analysis, goto_model, main);
432  return CPROVER_EXIT_SUCCESS;
433  }
434 
435  if(cmdline.isset("show-symbol-table"))
436  {
438  return CPROVER_EXIT_SUCCESS;
439  }
440 
441  if(cmdline.isset("show-reaching-definitions"))
442  {
444 
446  reaching_definitions_analysist rd_analysis(ns);
447  rd_analysis(goto_model);
448  rd_analysis.output(goto_model, std::cout);
449 
450  return CPROVER_EXIT_SUCCESS;
451  }
452 
453  if(cmdline.isset("show-dependence-graph"))
454  {
456 
458  dependence_grapht dependence_graph(ns);
459  dependence_graph(goto_model);
460  dependence_graph.output(goto_model, std::cout);
461  dependence_graph.output_dot(std::cout);
462 
463  return CPROVER_EXIT_SUCCESS;
464  }
465 
466  if(cmdline.isset("count-eloc"))
467  {
469  return CPROVER_EXIT_SUCCESS;
470  }
471 
472  if(cmdline.isset("list-eloc"))
473  {
475  return CPROVER_EXIT_SUCCESS;
476  }
477 
478  if(cmdline.isset("print-path-lengths"))
479  {
481  return CPROVER_EXIT_SUCCESS;
482  }
483 
484  if(cmdline.isset("print-global-state-size"))
485  {
487  return CPROVER_EXIT_SUCCESS;
488  }
489 
490  if(cmdline.isset("list-symbols"))
491  {
493  return CPROVER_EXIT_SUCCESS;
494  }
495 
496  if(cmdline.isset("show-uninitialized"))
497  {
498  show_uninitialized(goto_model, std::cout);
499  return CPROVER_EXIT_SUCCESS;
500  }
501 
502  if(cmdline.isset("interpreter"))
503  {
504  status() << "Starting interpreter" << eom;
506  return CPROVER_EXIT_SUCCESS;
507  }
508 
509  if(cmdline.isset("show-claims") ||
510  cmdline.isset("show-properties"))
511  {
514  return CPROVER_EXIT_SUCCESS;
515  }
516 
517  if(cmdline.isset("document-claims-html") ||
518  cmdline.isset("document-properties-html"))
519  {
521  return CPROVER_EXIT_SUCCESS;
522  }
523 
524  if(cmdline.isset("document-claims-latex") ||
525  cmdline.isset("document-properties-latex"))
526  {
528  return CPROVER_EXIT_SUCCESS;
529  }
530 
531  if(cmdline.isset("show-loops"))
532  {
534  return CPROVER_EXIT_SUCCESS;
535  }
536 
537  if(cmdline.isset("show-natural-loops"))
538  {
539  show_natural_loops(goto_model, std::cout);
540  return CPROVER_EXIT_SUCCESS;
541  }
542 
543  if(cmdline.isset("print-internal-representation"))
544  {
545  for(auto const &pair : goto_model.goto_functions.function_map)
546  for(auto const &ins : pair.second.body.instructions)
547  {
548  if(ins.code.is_not_nil())
549  status() << ins.code.pretty() << eom;
550  if(ins.guard.is_not_nil())
551  status() << "[guard] " << ins.guard.pretty() << eom;
552  }
553  return CPROVER_EXIT_SUCCESS;
554  }
555 
556  if(
557  cmdline.isset("show-goto-functions") ||
558  cmdline.isset("list-goto-functions"))
559  {
561  goto_model,
564  cmdline.isset("list-goto-functions"));
565  return CPROVER_EXIT_SUCCESS;
566  }
567 
568  if(cmdline.isset("list-undefined-functions"))
569  {
571  return CPROVER_EXIT_SUCCESS;
572  }
573 
574  // experimental: print structs
575  if(cmdline.isset("show-struct-alignment"))
576  {
578  return CPROVER_EXIT_SUCCESS;
579  }
580 
581  if(cmdline.isset("show-locations"))
582  {
584  return CPROVER_EXIT_SUCCESS;
585  }
586 
587  if(cmdline.isset("dump-c") || cmdline.isset("dump-cpp"))
588  {
589  const bool is_cpp=cmdline.isset("dump-cpp");
590  const bool h_libc=!cmdline.isset("no-system-headers");
591  const bool h_all=cmdline.isset("use-all-headers");
592  const bool harness=cmdline.isset("harness");
594 
595  // restore RETURN instructions in case remove_returns had been
596  // applied
598 
599  if(cmdline.args.size()==2)
600  {
601  #ifdef _MSC_VER
602  std::ofstream out(widen(cmdline.args[1]));
603  #else
604  std::ofstream out(cmdline.args[1]);
605  #endif
606  if(!out)
607  {
608  error() << "failed to write to `" << cmdline.args[1] << "'";
610  }
611  (is_cpp ? dump_cpp : dump_c)(
613  h_libc,
614  h_all,
615  harness,
616  ns,
617  out);
618  }
619  else
620  (is_cpp ? dump_cpp : dump_c)(
622  h_libc,
623  h_all,
624  harness,
625  ns,
626  std::cout);
627 
628  return CPROVER_EXIT_SUCCESS;
629  }
630 
631  if(cmdline.isset("call-graph"))
632  {
634  call_grapht call_graph(goto_model);
635 
636  if(cmdline.isset("xml"))
637  call_graph.output_xml(std::cout);
638  else if(cmdline.isset("dot"))
639  call_graph.output_dot(std::cout);
640  else
641  call_graph.output(std::cout);
642 
643  return CPROVER_EXIT_SUCCESS;
644  }
645 
646  if(cmdline.isset("reachable-call-graph"))
647  {
649  call_grapht call_graph =
652  if(cmdline.isset("xml"))
653  call_graph.output_xml(std::cout);
654  else if(cmdline.isset("dot"))
655  call_graph.output_dot(std::cout);
656  else
657  call_graph.output(std::cout);
658 
659  return 0;
660  }
661 
662  if(cmdline.isset("show-class-hierarchy"))
663  {
664  class_hierarchyt hierarchy;
665  hierarchy(goto_model.symbol_table);
666  if(cmdline.isset("dot"))
667  hierarchy.output_dot(std::cout);
668  else
671 
672  return CPROVER_EXIT_SUCCESS;
673  }
674 
675  if(cmdline.isset("dot"))
676  {
678 
679  if(cmdline.args.size()==2)
680  {
681  #ifdef _MSC_VER
682  std::ofstream out(widen(cmdline.args[1]));
683  #else
684  std::ofstream out(cmdline.args[1]);
685  #endif
686  if(!out)
687  {
688  error() << "failed to write to " << cmdline.args[1] << "'";
690  }
691 
692  dot(goto_model, out);
693  }
694  else
695  dot(goto_model, std::cout);
696 
697  return CPROVER_EXIT_SUCCESS;
698  }
699 
700  if(cmdline.isset("accelerate"))
701  {
703 
705 
706  status() << "Performing full inlining" << eom;
708 
709  status() << "Removing calls to functions without a body" << eom;
710  remove_calls_no_bodyt remove_calls_no_body;
711  remove_calls_no_body(goto_model.goto_functions);
712 
713  status() << "Accelerating" << eom;
717  }
718 
719  if(cmdline.isset("horn-encoding"))
720  {
721  status() << "Horn-clause encoding" << eom;
723 
724  if(cmdline.args.size()==2)
725  {
726  #ifdef _MSC_VER
727  std::ofstream out(widen(cmdline.args[1]));
728  #else
729  std::ofstream out(cmdline.args[1]);
730  #endif
731 
732  if(!out)
733  {
734  error() << "Failed to open output file "
735  << cmdline.args[1] << eom;
737  }
738 
740  }
741  else
742  horn_encoding(goto_model, std::cout);
743 
744  return CPROVER_EXIT_SUCCESS;
745  }
746 
747  if(cmdline.isset("drop-unused-functions"))
748  {
750 
751  status() << "Removing unused functions" << eom;
753  }
754 
755  if(cmdline.isset("undefined-function-is-assume-false"))
756  {
759  }
760 
761  // write new binary?
762  if(cmdline.args.size()==2)
763  {
764  status() << "Writing GOTO program to `" << cmdline.args[1] << "'" << eom;
765 
769  else
770  return CPROVER_EXIT_SUCCESS;
771  }
772 
773  help();
775  }
776 
777  catch(const char *e)
778  {
779  error() << e << eom;
781  }
782 
783  catch(const std::string &e)
784  {
785  error() << e << eom;
787  }
788 
789  catch(int e)
790  {
791  error() << "Numeric exception : " << e << eom;
793  }
794 
795  catch(const std::bad_alloc &)
796  {
797  error() << "Out of memory" << eom;
799  }
800 // NOLINTNEXTLINE(readability/fn_size)
801 }
802 
804  bool force)
805 {
806  if(function_pointer_removal_done && !force)
807  return;
808 
810 
811  status() << "Function Pointer Removal" << eom;
814  goto_model,
815  cmdline.isset("pointer-check"));
816  status() << "Virtual function removal" << eom;
818  status() << "Cleaning inline assembler statements" << eom;
820 }
821 
826 {
827  // Don't bother if we've already done a full function pointer
828  // removal.
830  {
831  return;
832  }
833 
834  status() << "Removing const function pointers only" << eom;
837  goto_model,
838  cmdline.isset("pointer-check"),
839  true); // abort if we can't resolve via const pointers
840 }
841 
843 {
845  return;
846 
848 
849  if(!cmdline.isset("inline"))
850  {
851  status() << "Partial Inlining" << eom;
853  }
854 }
855 
857 {
859  return;
860 
861  remove_returns_done=true;
862 
863  status() << "Removing returns" << eom;
865 }
866 
868 {
869  status() << "Reading GOTO program from `" << cmdline.args[0] << "'" << eom;
870 
873  throw 0;
874 
875  config.set(cmdline);
876 }
877 
879 {
880  optionst options;
881 
882  // disable simplify when adding various checks?
883  if(cmdline.isset("no-simplify"))
884  options.set_option("simplify", false);
885  else
886  options.set_option("simplify", true);
887 
888  // use assumptions instead of assertions?
889  if(cmdline.isset("assert-to-assume"))
890  options.set_option("assert-to-assume", true);
891  else
892  options.set_option("assert-to-assume", false);
893 
894  // all checks supported by goto_check
896 
897  // check assertions
898  if(cmdline.isset("no-assertions"))
899  options.set_option("assertions", false);
900  else
901  options.set_option("assertions", true);
902 
903  // use assumptions
904  if(cmdline.isset("no-assumptions"))
905  options.set_option("assumptions", false);
906  else
907  options.set_option("assumptions", true);
908 
909  // magic error label
910  if(cmdline.isset("error-label"))
911  options.set_option("error-label", cmdline.get_value("error-label"));
912 
913  // unwind loops
914  if(cmdline.isset("unwind"))
915  {
916  status() << "Unwinding loops" << eom;
917  options.set_option("unwind", cmdline.get_value("unwind"));
918  }
919 
920  // skip over selected loops
921  if(cmdline.isset("skip-loops"))
922  {
923  status() << "Adding gotos to skip loops" << eom;
924  if(skip_loops(
925  goto_model,
926  cmdline.get_value("skip-loops"),
928  throw 0;
929  }
930 
932 
933  // initialize argv with valid pointers
934  if(cmdline.isset("model-argc-argv"))
935  {
936  unsigned max_argc=
937  safe_string2unsigned(cmdline.get_value("model-argc-argv"));
938 
939  status() << "Adding up to " << max_argc
940  << " command line arguments" << eom;
941  if(model_argc_argv(
942  goto_model,
943  max_argc,
945  throw 0;
946  }
947 
948  if(cmdline.isset("remove-function-body"))
949  {
951  goto_model,
952  cmdline.get_values("remove-function-body"),
954  }
955 
956  // we add the library in some cases, as some analyses benefit
957 
958  if(cmdline.isset("add-library") ||
959  cmdline.isset("mm"))
960  {
961  if(cmdline.isset("show-custom-bitvector-analysis") ||
962  cmdline.isset("custom-bitvector-analysis"))
963  config.ansi_c.defines.push_back("__CPROVER_CUSTOM_BITVECTOR_ANALYSIS");
964 
965  // add the library
966  status() << "Adding CPROVER library (" << config.ansi_c.arch << ")" << eom;
971  }
972 
973  // now do full inlining, if requested
974  if(cmdline.isset("inline"))
975  {
977 
978  if(cmdline.isset("show-custom-bitvector-analysis") ||
979  cmdline.isset("custom-bitvector-analysis"))
980  {
984  }
985 
986  status() << "Performing full inlining" << eom;
988  }
989 
990  if(cmdline.isset("show-custom-bitvector-analysis") ||
991  cmdline.isset("custom-bitvector-analysis"))
992  {
993  status() << "Propagating Constants" << eom;
994  constant_propagator_ait constant_propagator_ai(goto_model);
996  }
997 
998  if(cmdline.isset("escape-analysis"))
999  {
1003 
1004  // recalculate numbers, etc.
1006 
1007  status() << "Escape Analysis" << eom;
1008  escape_analysist escape_analysis;
1009  escape_analysis(goto_model);
1010  escape_analysis.instrument(goto_model);
1011 
1012  // inline added functions, they are often small
1014 
1015  // recalculate numbers, etc.
1017  }
1018 
1019  // verify and set invariants and pre/post-condition pairs
1020  if(cmdline.isset("apply-code-contracts"))
1021  {
1022  status() << "Applying Code Contracts" << eom;
1024  }
1025 
1026  // replace function pointers, if explicitly requested
1027  if(cmdline.isset("remove-function-pointers"))
1028  {
1030  }
1031  else if(cmdline.isset("remove-const-function-pointers"))
1032  {
1034  }
1035 
1036  if(cmdline.isset("function-inline"))
1037  {
1038  std::string function=cmdline.get_value("function-inline");
1039  PRECONDITION(!function.empty());
1040 
1041  bool caching=!cmdline.isset("no-caching");
1042 
1044 
1045  status() << "Inlining calls of function `" << function << "'" << eom;
1046 
1047  if(!cmdline.isset("log"))
1048  {
1050  goto_model,
1051  function,
1053  true,
1054  caching);
1055  }
1056  else
1057  {
1058  std::string filename=cmdline.get_value("log");
1059  bool have_file=!filename.empty() && filename!="-";
1060 
1061  jsont result=
1063  goto_model,
1064  function,
1066  true,
1067  caching);
1068 
1069  if(have_file)
1070  {
1071 #ifdef _MSC_VER
1072  std::ofstream of(widen(filename));
1073 #else
1074  std::ofstream of(filename);
1075 #endif
1076  if(!of)
1077  throw "failed to open file "+filename;
1078 
1079  of << result;
1080  of.close();
1081  }
1082  else
1083  {
1084  std::cout << result << '\n';
1085  }
1086  }
1087 
1090  }
1091 
1092  if(cmdline.isset("partial-inline"))
1093  {
1095 
1096  status() << "Partial inlining" << eom;
1098 
1101  }
1102 
1103  if(cmdline.isset("remove-calls-no-body"))
1104  {
1105  status() << "Removing calls to functions without a body" << eom;
1106 
1107  remove_calls_no_bodyt remove_calls_no_body;
1108  remove_calls_no_body(goto_model.goto_functions);
1109 
1112  }
1113 
1114  if(cmdline.isset("constant-propagator"))
1115  {
1117 
1118  status() << "Propagating Constants" << eom;
1119 
1120  constant_propagator_ait constant_propagator_ai(goto_model);
1122  }
1123 
1124  // add generic checks, if needed
1125  goto_check(options, goto_model);
1126 
1127  // check for uninitalized local variables
1128  if(cmdline.isset("uninitialized-check"))
1129  {
1130  status() << "Adding checks for uninitialized local variables" << eom;
1132  }
1133 
1134  // check for maximum call stack size
1135  if(cmdline.isset("stack-depth"))
1136  {
1137  status() << "Adding check for maximum call stack size" << eom;
1138  stack_depth(
1139  goto_model,
1140  unsafe_string2unsigned(cmdline.get_value("stack-depth")));
1141  }
1142 
1143  // ignore default/user-specified initialization of variables with static
1144  // lifetime
1145  if(cmdline.isset("nondet-static"))
1146  {
1147  status() << "Adding nondeterministic initialization of static/global "
1148  "variables" << eom;
1150  }
1151 
1152  if(cmdline.isset("slice-global-inits"))
1153  {
1154  status() << "Slicing away initializations of unused global variables"
1155  << eom;
1157  }
1158 
1159  if(cmdline.isset("string-abstraction"))
1160  {
1163 
1164  status() << "String Abstraction" << eom;
1166  goto_model,
1168  }
1169 
1170  // some analyses require function pointer removal and partial inlining
1171 
1172  if(cmdline.isset("remove-pointers") ||
1173  cmdline.isset("race-check") ||
1174  cmdline.isset("mm") ||
1175  cmdline.isset("isr") ||
1176  cmdline.isset("concurrency"))
1177  {
1179 
1180  status() << "Pointer Analysis" << eom;
1181  value_set_analysist value_set_analysis(ns);
1182  value_set_analysis(goto_model.goto_functions);
1183 
1184  if(cmdline.isset("remove-pointers"))
1185  {
1186  // removing pointers
1187  status() << "Removing Pointers" << eom;
1188  remove_pointers(goto_model, value_set_analysis);
1189  }
1190 
1191  if(cmdline.isset("race-check"))
1192  {
1193  status() << "Adding Race Checks" << eom;
1194  race_check(value_set_analysis, goto_model);
1195  }
1196 
1197  if(cmdline.isset("mm"))
1198  {
1199  std::string mm=cmdline.get_value("mm");
1200  memory_modelt model;
1201 
1202  // strategy of instrumentation
1203  instrumentation_strategyt inst_strategy;
1204  if(cmdline.isset("one-event-per-cycle"))
1205  inst_strategy=one_event_per_cycle;
1206  else if(cmdline.isset("minimum-interference"))
1207  inst_strategy=min_interference;
1208  else if(cmdline.isset("read-first"))
1209  inst_strategy=read_first;
1210  else if(cmdline.isset("write-first"))
1211  inst_strategy=write_first;
1212  else if(cmdline.isset("my-events"))
1213  inst_strategy=my_events;
1214  else
1215  /* default: instruments all unsafe pairs */
1216  inst_strategy=all;
1217 
1218  const unsigned unwind_loops=
1219  cmdline.isset("unwind")?
1221  const unsigned max_var=
1222  cmdline.isset("max-var")?
1224  const unsigned max_po_trans=
1225  cmdline.isset("max-po-trans")?
1226  unsafe_string2unsigned(cmdline.get_value("max-po-trans")):0;
1227 
1228  if(mm=="tso")
1229  {
1230  status() << "Adding weak memory (TSO) Instrumentation" << eom;
1231  model=TSO;
1232  }
1233  else if(mm=="pso")
1234  {
1235  status() << "Adding weak memory (PSO) Instrumentation" << eom;
1236  model=PSO;
1237  }
1238  else if(mm=="rmo")
1239  {
1240  status() << "Adding weak memory (RMO) Instrumentation" << eom;
1241  model=RMO;
1242  }
1243  else if(mm=="power")
1244  {
1245  status() << "Adding weak memory (Power) Instrumentation" << eom;
1246  model=Power;
1247  }
1248  else
1249  {
1250  error() << "Unknown weak memory model `" << mm << "'" << eom;
1251  model=Unknown;
1252  }
1253 
1255 
1256  if(cmdline.isset("force-loop-duplication"))
1257  loops=all_loops;
1258  if(cmdline.isset("no-loop-duplication"))
1259  loops=no_loop;
1260 
1261  if(model!=Unknown)
1262  weak_memory(
1263  model,
1264  value_set_analysis,
1265  goto_model,
1266  cmdline.isset("scc"),
1267  inst_strategy,
1268  unwind_loops,
1269  !cmdline.isset("cfg-kill"),
1270  cmdline.isset("no-dependencies"),
1271  loops,
1272  max_var,
1273  max_po_trans,
1274  !cmdline.isset("no-po-rendering"),
1275  cmdline.isset("render-cluster-file"),
1276  cmdline.isset("render-cluster-function"),
1277  cmdline.isset("cav11"),
1278  cmdline.isset("hide-internals"),
1280  cmdline.isset("ignore-arrays"));
1281  }
1282 
1283  // Interrupt handler
1284  if(cmdline.isset("isr"))
1285  {
1286  status() << "Instrumenting interrupt handler" << eom;
1287  interrupt(
1288  value_set_analysis,
1289  goto_model,
1290  cmdline.get_value("isr"));
1291  }
1292 
1293  // Memory-mapped I/O
1294  if(cmdline.isset("mmio"))
1295  {
1296  status() << "Instrumenting memory-mapped I/O" << eom;
1297  mmio(value_set_analysis, goto_model);
1298  }
1299 
1300  if(cmdline.isset("concurrency"))
1301  {
1302  status() << "Sequentializing concurrency" << eom;
1303  concurrency(value_set_analysis, goto_model);
1304  }
1305  }
1306 
1307  if(cmdline.isset("interval-analysis"))
1308  {
1309  status() << "Interval analysis" << eom;
1311  }
1312 
1313  if(cmdline.isset("havoc-loops"))
1314  {
1315  status() << "Havocking loops" << eom;
1317  }
1318 
1319  if(cmdline.isset("k-induction"))
1320  {
1321  bool base_case=cmdline.isset("base-case");
1322  bool step_case=cmdline.isset("step-case");
1323 
1324  if(step_case && base_case)
1325  throw "please specify only one of --step-case and --base-case";
1326  else if(!step_case && !base_case)
1327  throw "please specify one of --step-case and --base-case";
1328 
1329  unsigned k=unsafe_string2unsigned(cmdline.get_value("k-induction"));
1330 
1331  if(k==0)
1332  throw "please give k>=1";
1333 
1334  status() << "Instrumenting k-induction for k=" << k << ", "
1335  << (base_case?"base case":"step case") << eom;
1336 
1337  k_induction(goto_model, base_case, step_case, k);
1338  }
1339 
1340  if(cmdline.isset("function-enter"))
1341  {
1342  status() << "Function enter instrumentation" << eom;
1344  goto_model,
1345  cmdline.get_value("function-enter"));
1346  }
1347 
1348  if(cmdline.isset("function-exit"))
1349  {
1350  status() << "Function exit instrumentation" << eom;
1351  function_exit(
1352  goto_model,
1353  cmdline.get_value("function-exit"));
1354  }
1355 
1356  if(cmdline.isset("branch"))
1357  {
1358  status() << "Branch instrumentation" << eom;
1359  branch(
1360  goto_model,
1361  cmdline.get_value("branch"));
1362  }
1363 
1364  // add failed symbols
1366 
1367  // recalculate numbers, etc.
1369 
1370  // add loop ids
1372 
1373  // label the assertions
1375 
1376  // nondet volatile?
1377  if(cmdline.isset("nondet-volatile"))
1378  {
1379  status() << "Making volatile variables non-deterministic" << eom;
1381  }
1382 
1383  // reachability slice?
1384  if(cmdline.isset("reachability-slice"))
1385  {
1387 
1388  status() << "Performing a reachability slice" << eom;
1389  if(cmdline.isset("property"))
1391  else
1393  }
1394 
1395  // full slice?
1396  if(cmdline.isset("full-slice"))
1397  {
1400 
1401  status() << "Performing a full slice" << eom;
1402  if(cmdline.isset("property"))
1404  else
1406  }
1407 
1408  // splice option
1409  if(cmdline.isset("splice-call"))
1410  {
1411  status() << "Performing call splicing" << eom;
1412  std::string callercallee=cmdline.get_value("splice-call");
1413  if(splice_call(
1415  callercallee,
1418  throw 0;
1419  }
1420 
1421  if(cmdline.isset("generate-function-body"))
1422  {
1423  auto generate_implementation = generate_function_bodies_factory(
1424  cmdline.get_value("generate-function-body-options"),
1426  *message_handler);
1428  std::regex(cmdline.get_value("generate-function-body")),
1429  *generate_implementation,
1430  goto_model,
1431  *message_handler);
1432  }
1433 
1434  // recalculate numbers, etc.
1436 }
1437 
1440 {
1441  // clang-format off
1442  std::cout << '\n' << banner_string("Goto-Instrument", CBMC_VERSION) << '\n'
1443  <<
1444  "* * Copyright (C) 2008-2013 * *\n"
1445  "* * Daniel Kroening * *\n"
1446  "* * kroening@kroening.com * *\n"
1447  "\n"
1448  "Usage: Purpose:\n"
1449  "\n"
1450  " goto-instrument [-?] [-h] [--help] show help\n"
1451  " goto-instrument in out perform instrumentation\n"
1452  "\n"
1453  "Main options:\n"
1454  " --document-properties-html generate HTML property documentation\n"
1455  " --document-properties-latex generate Latex property documentation\n"
1456  " --dump-c generate C source\n"
1457  " --dump-cpp generate C++ source\n"
1458  " --dot generate CFG graph in DOT format\n"
1459  " --interpreter do concrete execution\n"
1460  "\n"
1461  "Diagnosis:\n"
1462  " --show-loops show the loops in the program\n"
1464  " --show-symbol-table show loaded symbol table\n"
1465  " --list-symbols list symbols with type information\n"
1468  " --drop-unused-functions drop functions trivially unreachable from main function\n" // NOLINT(*)
1469  " --print-internal-representation\n" // NOLINTNEXTLINE(*)
1470  " show verbose internal representation of the program\n"
1471  " --list-undefined-functions list functions without body\n"
1472  " --show-struct-alignment show struct members that might be concurrently accessed\n" // NOLINT(*)
1473  " --show-natural-loops show natural loop heads\n"
1474  // NOLINTNEXTLINE(whitespace/line_length)
1475  " --list-calls-args list all function calls with their arguments\n"
1476  " --call-graph show graph of function calls\n"
1477  // NOLINTNEXTLINE(whitespace/line_length)
1478  " --reachable-call-graph show graph of function calls potentially reachable from main function\n"
1480  // NOLINTNEXTLINE(whitespace/line_length)
1481  " --show-threaded show instructions that may be executed by more than one thread\n"
1482  "\n"
1483  "Safety checks:\n"
1484  " --no-assertions ignore user assertions\n"
1486  " --uninitialized-check add checks for uninitialized locals (experimental)\n" // NOLINT(*)
1487  " --error-label label check that label is unreachable\n"
1488  " --stack-depth n add check that call stack size of non-inlined functions never exceeds n\n" // NOLINT(*)
1489  " --race-check add floating-point data race checks\n"
1490  "\n"
1491  "Semantic transformations:\n"
1492  " --nondet-volatile makes reads from volatile variables non-deterministic\n" // NOLINT(*)
1493  " --unwind <n> unwinds the loops <n> times\n"
1494  " --unwindset L:B,... unwind loop L with a bound of B\n"
1495  " --unwindset-file <file> read unwindset from file\n"
1496  " --partial-loops permit paths with partial loops\n"
1497  " --unwinding-assertions generate unwinding assertions\n"
1498  " --continue-as-loops add loop for remaining iterations after unwound part\n" // NOLINT(*)
1499  " --isr <function> instruments an interrupt service routine\n"
1500  " --mmio instruments memory-mapped I/O\n"
1501  " --nondet-static add nondeterministic initialization of variables with static lifetime\n" // NOLINT(*)
1502  " --check-invariant function instruments invariant checking function\n"
1503  " --remove-pointers converts pointer arithmetic to base+offset expressions\n" // NOLINT(*)
1504  " --splice-call caller,callee prepends a call to callee in the body of caller\n" // NOLINT(*)
1505  " --undefined-function-is-assume-false\n"
1506  // NOLINTNEXTLINE(whitespace/line_length)
1507  " convert each call to an undefined function to assume(false)\n"
1509  "\n"
1510  "Loop transformations:\n"
1511  " --k-induction <k> check loops with k-induction\n"
1512  " --step-case k-induction: do step-case\n"
1513  " --base-case k-induction: do base-case\n"
1514  " --havoc-loops over-approximate all loops\n"
1515  " --accelerate add loop accelerators\n"
1516  " --skip-loops <loop-ids> add gotos to skip selected loops during execution\n" // NOLINT(*)
1517  "\n"
1518  "Memory model instrumentations:\n"
1519  " --mm <tso,pso,rmo,power> instruments a weak memory model\n"
1520  " --scc detects critical cycles per SCC (one thread per SCC)\n" // NOLINT(*)
1521  " --one-event-per-cycle only instruments one event per cycle\n"
1522  " --minimum-interference instruments an optimal number of events\n"
1523  " --my-events only instruments events whose ids appear in inst.evt\n" // NOLINT(*)
1524  " --cfg-kill enables symbolic execution used to reduce spurious cycles\n" // NOLINT(*)
1525  " --no-dependencies no dependency analysis\n"
1526  // NOLINTNEXTLINE(whitespace/line_length)
1527  " --no-po-rendering no representation of the threads in the dot\n"
1528  " --render-cluster-file clusterises the dot by files\n"
1529  " --render-cluster-function clusterises the dot by functions\n"
1530  "\n"
1531  "Slicing:\n"
1532  " --reachability-slice slice away instructions that can't reach assertions\n" // NOLINT(*)
1533  " --full-slice slice away instructions that don't affect assertions\n" // NOLINT(*)
1534  " --property id slice with respect to specific property only\n" // NOLINT(*)
1535  " --slice-global-inits slice away initializations of unused global variables\n" // NOLINT(*)
1536  "\n"
1537  "Further transformations:\n"
1538  " --constant-propagator propagate constants and simplify expressions\n" // NOLINT(*)
1539  " --inline perform full inlining\n"
1540  " --partial-inline perform partial inlining\n"
1541  " --function-inline <function> transitively inline all calls <function> makes\n" // NOLINT(*)
1542  " --no-caching disable caching of intermediate results during transitive function inlining\n" // NOLINT(*)
1543  " --log <file> log in json format which code segments were inlined, use with --function-inline\n" // NOLINT(*)
1544  " --remove-function-pointers replace function pointers by case statement over function calls\n" // NOLINT(*)
1547  " --add-library add models of C library functions\n"
1548  " --model-argc-argv <n> model up to <n> command line arguments\n"
1549  // NOLINTNEXTLINE(whitespace/line_length)
1550  " --remove-function-body <f> remove the implementation of function <f> (may be repeated)\n"
1551  "\n"
1552  "Other options:\n"
1553  " --no-system-headers with --dump-c/--dump-cpp: generate C source expanding libc includes\n" // NOLINT(*)
1554  " --use-all-headers with --dump-c/--dump-cpp: generate C source with all includes\n" // NOLINT(*)
1555  " --harness with --dump-c/--dump-cpp: include input generator in output\n" // NOLINT(*)
1556  " --version show version and exit\n"
1557  HELP_FLUSH
1558  " --xml-ui use XML-formatted output\n"
1559  " --json-ui use JSON-formatted output\n"
1561  "\n";
1562  // clang-format on
1563 }
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.
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:56
instrumentation_strategyt
Definition: wmm.h:26
void concurrency(value_setst &value_sets, goto_modelt &goto_model)
Remove Virtual Function (Method) Calls.
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:112
Definition: ai.h:377
Read Goto Programs.
#define HELP_SHOW_CLASS_HIERARCHY
Branch Instrumentation.
void weak_memory(memory_modelt model, value_setst &value_sets, goto_modelt &goto_model, bool SCC, instrumentation_strategyt event_strategy, unsigned unwinding_bound, 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)
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
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:92
bool set(const cmdlinet &cmdline)
Definition: config.cpp:737
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 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:647
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:276
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:249
void function_enter(goto_modelt &goto_model, const irep_idt &id)
Definition: function.cpp:80
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:230
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 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.
#define PARSE_OPTIONS_GOTO_CHECK(cmdline, options)
Definition: goto_check.h:56
void output_dot(std::ostream &out) const
Definition: graph.h:784
void remove_returns(symbol_table_baset &symbol_table, goto_functionst &goto_functions)
removes returns
void output(std::ostream &out) const
Definition: call_graph.cpp:266
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 show_natural_loops(const goto_modelt &goto_model, std::ostream &out)
Range-based reaching definitions analysis (following Field- Sensitive Program Dependence Analysis...
Verify and use annotated invariants and pre/post-conditions.
Show program locations.
static void list_calls_and_arguments(const namespacet &ns, const irep_idt &function, const goto_programt &goto_program)
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
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
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.
#define HELP_REPLACE_FUNCTION_BODY
void count_eloc(const goto_modelt &goto_model)
Definition: count_eloc.cpp:50
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
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.
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:106
#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:130
void print_global_state_size(const goto_modelt &goto_model)
Definition: count_eloc.cpp:149
void horn_encoding(const goto_modelt &, std::ostream &out)
void nondet_static(const namespacet &ns, goto_functionst &goto_functions, const irep_idt &fct_name)
void remove_asm(goto_functionst::goto_functiont &goto_function, symbol_tablet &symbol_table)
removes assembler
Definition: remove_asm.cpp:306
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