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 
128  {
129  const bool validate_only = cmdline.isset("validate-goto-binary");
130 
131  if(validate_only || cmdline.isset("validate-goto-model"))
132  {
134 
135  if(validate_only)
136  {
137  return CPROVER_EXIT_SUCCESS;
138  }
139  }
140  }
141 
143 
144  if(cmdline.isset("validate-goto-model"))
145  {
147  }
148 
149  {
150  bool unwind_given=cmdline.isset("unwind");
151  bool unwindset_given=cmdline.isset("unwindset");
152  bool unwindset_file_given=cmdline.isset("unwindset-file");
153 
154  if(unwindset_given && unwindset_file_given)
155  throw "only one of --unwindset and --unwindset-file supported at a "
156  "time";
157 
158  if(unwind_given || unwindset_given || unwindset_file_given)
159  {
160  unwindsett unwindset;
161 
162  if(unwind_given)
163  unwindset.parse_unwind(cmdline.get_value("unwind"));
164 
165  if(unwindset_file_given)
166  unwindset.parse_unwindset_file(cmdline.get_value("unwindset-file"));
167 
168  if(unwindset_given)
169  unwindset.parse_unwindset(cmdline.get_value("unwindset"));
170 
171  bool unwinding_assertions=cmdline.isset("unwinding-assertions");
172  bool partial_loops=cmdline.isset("partial-loops");
173  bool continue_as_loops=cmdline.isset("continue-as-loops");
174 
175  if(unwinding_assertions+partial_loops+continue_as_loops>1)
176  throw "more than one of --unwinding-assertions,--partial-loops,"
177  "--continue-as-loops selected";
178 
179  goto_unwindt::unwind_strategyt unwind_strategy=
181 
182  if(unwinding_assertions)
183  {
185  }
186  else if(partial_loops)
187  {
189  }
190  else if(continue_as_loops)
191  {
193  }
194 
195  goto_unwindt goto_unwind;
196  goto_unwind(goto_model, unwindset, unwind_strategy);
197 
198  if(cmdline.isset("log"))
199  {
200  std::string filename=cmdline.get_value("log");
201  bool have_file=!filename.empty() && filename!="-";
202 
203  jsont result=goto_unwind.output_log_json();
204 
205  if(have_file)
206  {
207 #ifdef _MSC_VER
208  std::ofstream of(widen(filename));
209 #else
210  std::ofstream of(filename);
211 #endif
212  if(!of)
213  throw "failed to open file "+filename;
214 
215  of << result;
216  of.close();
217  }
218  else
219  {
220  std::cout << result << '\n';
221  }
222  }
223 
224  // goto_unwind holds references to instructions, only do remove_skip
225  // after having generated the log above
227  }
228  }
229 
230  if(cmdline.isset("show-threaded"))
231  {
233 
234  is_threadedt is_threaded(goto_model);
235 
237  {
238  std::cout << "////\n";
239  std::cout << "//// Function: " << f_it->first << '\n';
240  std::cout << "////\n\n";
241 
242  const goto_programt &goto_program=f_it->second.body;
243 
244  forall_goto_program_instructions(i_it, goto_program)
245  {
246  goto_program.output_instruction(ns, "", std::cout, *i_it);
247  std::cout << "Is threaded: " << (is_threaded(i_it)?"True":"False")
248  << "\n\n";
249  }
250  }
251 
252  return CPROVER_EXIT_SUCCESS;
253  }
254 
255  if(cmdline.isset("show-value-sets"))
256  {
258 
259  // recalculate numbers, etc.
261 
262  status() << "Pointer Analysis" << eom;
264  value_set_analysist value_set_analysis(ns);
265  value_set_analysis(goto_model.goto_functions);
266  show_value_sets(get_ui(), goto_model, value_set_analysis);
267  return CPROVER_EXIT_SUCCESS;
268  }
269 
270  if(cmdline.isset("show-global-may-alias"))
271  {
275 
276  // recalculate numbers, etc.
278 
279  global_may_alias_analysist global_may_alias_analysis;
280  global_may_alias_analysis(goto_model);
281  global_may_alias_analysis.output(goto_model, std::cout);
282 
283  return CPROVER_EXIT_SUCCESS;
284  }
285 
286  if(cmdline.isset("show-local-bitvector-analysis"))
287  {
290 
291  // recalculate numbers, etc.
293 
295 
297  {
298  local_bitvector_analysist local_bitvector_analysis(it->second);
299  std::cout << ">>>>\n";
300  std::cout << ">>>> " << it->first << '\n';
301  std::cout << ">>>>\n";
302  local_bitvector_analysis.output(std::cout, it->second, ns);
303  std::cout << '\n';
304  }
305 
306  return CPROVER_EXIT_SUCCESS;
307  }
308 
309  if(cmdline.isset("show-local-safe-pointers") ||
310  cmdline.isset("show-safe-dereferences"))
311  {
312  // Ensure location numbering is unique:
314 
316 
318  {
319  local_safe_pointerst local_safe_pointers(ns);
320  local_safe_pointers(it->second.body);
321  std::cout << ">>>>\n";
322  std::cout << ">>>> " << it->first << '\n';
323  std::cout << ">>>>\n";
324  if(cmdline.isset("show-local-safe-pointers"))
325  local_safe_pointers.output(std::cout, it->second.body);
326  else
327  {
328  local_safe_pointers.output_safe_dereferences(
329  std::cout, it->second.body);
330  }
331  std::cout << '\n';
332  }
333 
334  return CPROVER_EXIT_SUCCESS;
335  }
336 
337  if(cmdline.isset("show-custom-bitvector-analysis"))
338  {
342 
344 
345  if(!cmdline.isset("inline"))
346  {
349  }
350 
351  // recalculate numbers, etc.
353 
354  custom_bitvector_analysist custom_bitvector_analysis;
355  custom_bitvector_analysis(goto_model);
356  custom_bitvector_analysis.output(goto_model, std::cout);
357 
358  return CPROVER_EXIT_SUCCESS;
359  }
360 
361  if(cmdline.isset("show-escape-analysis"))
362  {
366 
367  // recalculate numbers, etc.
369 
370  escape_analysist escape_analysis;
371  escape_analysis(goto_model);
372  escape_analysis.output(goto_model, std::cout);
373 
374  return CPROVER_EXIT_SUCCESS;
375  }
376 
377  if(cmdline.isset("custom-bitvector-analysis"))
378  {
382 
384 
385  if(!cmdline.isset("inline"))
386  {
389  }
390 
391  // recalculate numbers, etc.
393 
395 
396  custom_bitvector_analysist custom_bitvector_analysis;
397  custom_bitvector_analysis(goto_model);
398  custom_bitvector_analysis.check(
399  goto_model,
400  cmdline.isset("xml-ui"),
401  std::cout);
402 
403  return CPROVER_EXIT_SUCCESS;
404  }
405 
406  if(cmdline.isset("show-points-to"))
407  {
409 
410  // recalculate numbers, etc.
412 
414 
415  status() << "Pointer Analysis" << eom;
416  points_tot points_to;
417  points_to(goto_model);
418  points_to.output(std::cout);
419  return CPROVER_EXIT_SUCCESS;
420  }
421 
422  if(cmdline.isset("show-intervals"))
423  {
425 
426  // recalculate numbers, etc.
428 
429  status() << "Interval Analysis" << eom;
433  interval_analysis.output(goto_model, std::cout);
434  return CPROVER_EXIT_SUCCESS;
435  }
436 
437  if(cmdline.isset("show-call-sequences"))
438  {
441  return CPROVER_EXIT_SUCCESS;
442  }
443 
444  if(cmdline.isset("check-call-sequence"))
445  {
448  return CPROVER_EXIT_SUCCESS;
449  }
450 
451  if(cmdline.isset("list-calls-args"))
452  {
454 
456 
457  return CPROVER_EXIT_SUCCESS;
458  }
459 
460  if(cmdline.isset("show-rw-set"))
461  {
463 
464  if(!cmdline.isset("inline"))
465  {
467 
468  // recalculate numbers, etc.
470  }
471 
472  status() << "Pointer Analysis" << eom;
473  value_set_analysist value_set_analysis(ns);
474  value_set_analysis(goto_model.goto_functions);
475 
476  const symbolt &symbol=ns.lookup(ID_main);
477  symbol_exprt main(symbol.name, symbol.type);
478 
479  std::cout <<
480  rw_set_functiont(value_set_analysis, goto_model, main);
481  return CPROVER_EXIT_SUCCESS;
482  }
483 
484  if(cmdline.isset("show-symbol-table"))
485  {
487  return CPROVER_EXIT_SUCCESS;
488  }
489 
490  if(cmdline.isset("show-reaching-definitions"))
491  {
493 
495  reaching_definitions_analysist rd_analysis(ns);
496  rd_analysis(goto_model);
497  rd_analysis.output(goto_model, std::cout);
498 
499  return CPROVER_EXIT_SUCCESS;
500  }
501 
502  if(cmdline.isset("show-dependence-graph"))
503  {
505 
507  dependence_grapht dependence_graph(ns);
508  dependence_graph(goto_model);
509  dependence_graph.output(goto_model, std::cout);
510  dependence_graph.output_dot(std::cout);
511 
512  return CPROVER_EXIT_SUCCESS;
513  }
514 
515  if(cmdline.isset("count-eloc"))
516  {
518  return CPROVER_EXIT_SUCCESS;
519  }
520 
521  if(cmdline.isset("list-eloc"))
522  {
524  return CPROVER_EXIT_SUCCESS;
525  }
526 
527  if(cmdline.isset("print-path-lengths"))
528  {
530  return CPROVER_EXIT_SUCCESS;
531  }
532 
533  if(cmdline.isset("print-global-state-size"))
534  {
536  return CPROVER_EXIT_SUCCESS;
537  }
538 
539  if(cmdline.isset("list-symbols"))
540  {
542  return CPROVER_EXIT_SUCCESS;
543  }
544 
545  if(cmdline.isset("show-uninitialized"))
546  {
547  show_uninitialized(goto_model, std::cout);
548  return CPROVER_EXIT_SUCCESS;
549  }
550 
551  if(cmdline.isset("interpreter"))
552  {
553  status() << "Starting interpreter" << eom;
555  return CPROVER_EXIT_SUCCESS;
556  }
557 
558  if(cmdline.isset("show-claims") ||
559  cmdline.isset("show-properties"))
560  {
563  return CPROVER_EXIT_SUCCESS;
564  }
565 
566  if(cmdline.isset("document-claims-html") ||
567  cmdline.isset("document-properties-html"))
568  {
570  return CPROVER_EXIT_SUCCESS;
571  }
572 
573  if(cmdline.isset("document-claims-latex") ||
574  cmdline.isset("document-properties-latex"))
575  {
577  return CPROVER_EXIT_SUCCESS;
578  }
579 
580  if(cmdline.isset("show-loops"))
581  {
583  return CPROVER_EXIT_SUCCESS;
584  }
585 
586  if(cmdline.isset("show-natural-loops"))
587  {
588  show_natural_loops(goto_model, std::cout);
589  return CPROVER_EXIT_SUCCESS;
590  }
591 
592  if(cmdline.isset("print-internal-representation"))
593  {
594  for(auto const &pair : goto_model.goto_functions.function_map)
595  for(auto const &ins : pair.second.body.instructions)
596  {
597  if(ins.code.is_not_nil())
598  status() << ins.code.pretty() << eom;
599  if(ins.guard.is_not_nil())
600  status() << "[guard] " << ins.guard.pretty() << eom;
601  }
602  return CPROVER_EXIT_SUCCESS;
603  }
604 
605  if(
606  cmdline.isset("show-goto-functions") ||
607  cmdline.isset("list-goto-functions"))
608  {
610  goto_model,
613  cmdline.isset("list-goto-functions"));
614  return CPROVER_EXIT_SUCCESS;
615  }
616 
617  if(cmdline.isset("list-undefined-functions"))
618  {
620  return CPROVER_EXIT_SUCCESS;
621  }
622 
623  // experimental: print structs
624  if(cmdline.isset("show-struct-alignment"))
625  {
627  return CPROVER_EXIT_SUCCESS;
628  }
629 
630  if(cmdline.isset("show-locations"))
631  {
633  return CPROVER_EXIT_SUCCESS;
634  }
635 
636  if(cmdline.isset("dump-c") || cmdline.isset("dump-cpp"))
637  {
638  const bool is_cpp=cmdline.isset("dump-cpp");
639  const bool h_libc=!cmdline.isset("no-system-headers");
640  const bool h_all=cmdline.isset("use-all-headers");
641  const bool harness=cmdline.isset("harness");
643 
644  // restore RETURN instructions in case remove_returns had been
645  // applied
647 
648  if(cmdline.args.size()==2)
649  {
650  #ifdef _MSC_VER
651  std::ofstream out(widen(cmdline.args[1]));
652  #else
653  std::ofstream out(cmdline.args[1]);
654  #endif
655  if(!out)
656  {
657  error() << "failed to write to `" << cmdline.args[1] << "'";
659  }
660  (is_cpp ? dump_cpp : dump_c)(
662  h_libc,
663  h_all,
664  harness,
665  ns,
666  out);
667  }
668  else
669  (is_cpp ? dump_cpp : dump_c)(
671  h_libc,
672  h_all,
673  harness,
674  ns,
675  std::cout);
676 
677  return CPROVER_EXIT_SUCCESS;
678  }
679 
680  if(cmdline.isset("call-graph"))
681  {
683  call_grapht call_graph(goto_model);
684 
685  if(cmdline.isset("xml"))
686  call_graph.output_xml(std::cout);
687  else if(cmdline.isset("dot"))
688  call_graph.output_dot(std::cout);
689  else
690  call_graph.output(std::cout);
691 
692  return CPROVER_EXIT_SUCCESS;
693  }
694 
695  if(cmdline.isset("reachable-call-graph"))
696  {
698  call_grapht call_graph =
701  if(cmdline.isset("xml"))
702  call_graph.output_xml(std::cout);
703  else if(cmdline.isset("dot"))
704  call_graph.output_dot(std::cout);
705  else
706  call_graph.output(std::cout);
707 
708  return 0;
709  }
710 
711  if(cmdline.isset("show-class-hierarchy"))
712  {
713  class_hierarchyt hierarchy;
714  hierarchy(goto_model.symbol_table);
715  if(cmdline.isset("dot"))
716  hierarchy.output_dot(std::cout);
717  else
719 
720  return CPROVER_EXIT_SUCCESS;
721  }
722 
723  if(cmdline.isset("dot"))
724  {
726 
727  if(cmdline.args.size()==2)
728  {
729  #ifdef _MSC_VER
730  std::ofstream out(widen(cmdline.args[1]));
731  #else
732  std::ofstream out(cmdline.args[1]);
733  #endif
734  if(!out)
735  {
736  error() << "failed to write to " << cmdline.args[1] << "'";
738  }
739 
740  dot(goto_model, out);
741  }
742  else
743  dot(goto_model, std::cout);
744 
745  return CPROVER_EXIT_SUCCESS;
746  }
747 
748  if(cmdline.isset("accelerate"))
749  {
751 
753 
754  status() << "Performing full inlining" << eom;
756 
757  status() << "Removing calls to functions without a body" << eom;
758  remove_calls_no_bodyt remove_calls_no_body;
759  remove_calls_no_body(goto_model.goto_functions);
760 
761  status() << "Accelerating" << eom;
765  }
766 
767  if(cmdline.isset("horn-encoding"))
768  {
769  status() << "Horn-clause encoding" << eom;
771 
772  if(cmdline.args.size()==2)
773  {
774  #ifdef _MSC_VER
775  std::ofstream out(widen(cmdline.args[1]));
776  #else
777  std::ofstream out(cmdline.args[1]);
778  #endif
779 
780  if(!out)
781  {
782  error() << "Failed to open output file "
783  << cmdline.args[1] << eom;
785  }
786 
788  }
789  else
790  horn_encoding(goto_model, std::cout);
791 
792  return CPROVER_EXIT_SUCCESS;
793  }
794 
795  if(cmdline.isset("drop-unused-functions"))
796  {
798 
799  status() << "Removing unused functions" << eom;
801  }
802 
803  if(cmdline.isset("undefined-function-is-assume-false"))
804  {
807  }
808 
809  // write new binary?
810  if(cmdline.args.size()==2)
811  {
812  status() << "Writing GOTO program to `" << cmdline.args[1] << "'" << eom;
813 
817  else
818  return CPROVER_EXIT_SUCCESS;
819  }
820 
821  help();
823  }
824 
825  catch(const char *e)
826  {
827  error() << e << eom;
829  }
830 
831  catch(const std::string &e)
832  {
833  error() << e << eom;
835  }
836 
837  catch(int e)
838  {
839  error() << "Numeric exception : " << e << eom;
841  }
842 
843  catch(const std::bad_alloc &)
844  {
845  error() << "Out of memory" << eom;
847  }
848 // NOLINTNEXTLINE(readability/fn_size)
849 }
850 
852  bool force)
853 {
854  if(function_pointer_removal_done && !force)
855  return;
856 
858 
859  status() << "Function Pointer Removal" << eom;
862  goto_model,
863  cmdline.isset("pointer-check"));
864  status() << "Virtual function removal" << eom;
866  status() << "Cleaning inline assembler statements" << eom;
868 }
869 
874 {
875  // Don't bother if we've already done a full function pointer
876  // removal.
878  {
879  return;
880  }
881 
882  status() << "Removing const function pointers only" << eom;
885  goto_model,
886  cmdline.isset("pointer-check"),
887  true); // abort if we can't resolve via const pointers
888 }
889 
891 {
893  return;
894 
896 
897  if(!cmdline.isset("inline"))
898  {
899  status() << "Partial Inlining" << eom;
901  }
902 }
903 
905 {
907  return;
908 
909  remove_returns_done=true;
910 
911  status() << "Removing returns" << eom;
913 }
914 
916 {
917  status() << "Reading GOTO program from `" << cmdline.args[0] << "'" << eom;
918 
919  config.set(cmdline);
920 
922 
923  if(!result.has_value())
924  throw 0;
925 
926  goto_model = std::move(result.value());
927 
929 }
930 
932 {
933  optionst options;
934 
935  // disable simplify when adding various checks?
936  if(cmdline.isset("no-simplify"))
937  options.set_option("simplify", false);
938  else
939  options.set_option("simplify", true);
940 
941  // use assumptions instead of assertions?
942  if(cmdline.isset("assert-to-assume"))
943  options.set_option("assert-to-assume", true);
944  else
945  options.set_option("assert-to-assume", false);
946 
947  // all checks supported by goto_check
949 
950  // check assertions
951  if(cmdline.isset("no-assertions"))
952  options.set_option("assertions", false);
953  else
954  options.set_option("assertions", true);
955 
956  // use assumptions
957  if(cmdline.isset("no-assumptions"))
958  options.set_option("assumptions", false);
959  else
960  options.set_option("assumptions", true);
961 
962  // magic error label
963  if(cmdline.isset("error-label"))
964  options.set_option("error-label", cmdline.get_value("error-label"));
965 
966  // unwind loops
967  if(cmdline.isset("unwind"))
968  {
969  status() << "Unwinding loops" << eom;
970  options.set_option("unwind", cmdline.get_value("unwind"));
971  }
972 
973  // skip over selected loops
974  if(cmdline.isset("skip-loops"))
975  {
976  status() << "Adding gotos to skip loops" << eom;
977  if(skip_loops(
978  goto_model,
979  cmdline.get_value("skip-loops"),
981  throw 0;
982  }
983 
985 
986  // initialize argv with valid pointers
987  if(cmdline.isset("model-argc-argv"))
988  {
989  unsigned max_argc=
990  safe_string2unsigned(cmdline.get_value("model-argc-argv"));
991 
992  status() << "Adding up to " << max_argc
993  << " command line arguments" << eom;
994  if(model_argc_argv(
995  goto_model,
996  max_argc,
998  throw 0;
999  }
1000 
1001  if(cmdline.isset("remove-function-body"))
1002  {
1004  goto_model,
1005  cmdline.get_values("remove-function-body"),
1007  }
1008 
1009  // we add the library in some cases, as some analyses benefit
1010 
1011  if(cmdline.isset("add-library") ||
1012  cmdline.isset("mm"))
1013  {
1014  if(cmdline.isset("show-custom-bitvector-analysis") ||
1015  cmdline.isset("custom-bitvector-analysis"))
1016  {
1017  config.ansi_c.defines.push_back(
1018  std::string(CPROVER_PREFIX) + "CUSTOM_BITVECTOR_ANALYSIS");
1019  }
1020 
1021  // add the library
1022  status() << "Adding CPROVER library (" << config.ansi_c.arch << ")" << eom;
1027  }
1028 
1029  // now do full inlining, if requested
1030  if(cmdline.isset("inline"))
1031  {
1033 
1034  if(cmdline.isset("show-custom-bitvector-analysis") ||
1035  cmdline.isset("custom-bitvector-analysis"))
1036  {
1040  }
1041 
1042  status() << "Performing full inlining" << eom;
1044  }
1045 
1046  if(cmdline.isset("show-custom-bitvector-analysis") ||
1047  cmdline.isset("custom-bitvector-analysis"))
1048  {
1049  status() << "Propagating Constants" << eom;
1050  constant_propagator_ait constant_propagator_ai(goto_model);
1052  }
1053 
1054  if(cmdline.isset("escape-analysis"))
1055  {
1059 
1060  // recalculate numbers, etc.
1062 
1063  status() << "Escape Analysis" << eom;
1064  escape_analysist escape_analysis;
1065  escape_analysis(goto_model);
1066  escape_analysis.instrument(goto_model);
1067 
1068  // inline added functions, they are often small
1070 
1071  // recalculate numbers, etc.
1073  }
1074 
1075  // verify and set invariants and pre/post-condition pairs
1076  if(cmdline.isset("apply-code-contracts"))
1077  {
1078  status() << "Applying Code Contracts" << eom;
1080  }
1081 
1082  // replace function pointers, if explicitly requested
1083  if(cmdline.isset("remove-function-pointers"))
1084  {
1086  }
1087  else if(cmdline.isset("remove-const-function-pointers"))
1088  {
1090  }
1091 
1092  if(cmdline.isset("replace-calls"))
1093  {
1095 
1096  replace_callst replace_calls;
1097  replace_calls(goto_model, cmdline.get_values("replace-calls"));
1098  }
1099 
1100  if(cmdline.isset("function-inline"))
1101  {
1102  std::string function=cmdline.get_value("function-inline");
1103  PRECONDITION(!function.empty());
1104 
1105  bool caching=!cmdline.isset("no-caching");
1106 
1108 
1109  status() << "Inlining calls of function `" << function << "'" << eom;
1110 
1111  if(!cmdline.isset("log"))
1112  {
1114  goto_model,
1115  function,
1117  true,
1118  caching);
1119  }
1120  else
1121  {
1122  std::string filename=cmdline.get_value("log");
1123  bool have_file=!filename.empty() && filename!="-";
1124 
1125  jsont result=
1127  goto_model,
1128  function,
1130  true,
1131  caching);
1132 
1133  if(have_file)
1134  {
1135 #ifdef _MSC_VER
1136  std::ofstream of(widen(filename));
1137 #else
1138  std::ofstream of(filename);
1139 #endif
1140  if(!of)
1141  throw "failed to open file "+filename;
1142 
1143  of << result;
1144  of.close();
1145  }
1146  else
1147  {
1148  std::cout << result << '\n';
1149  }
1150  }
1151 
1154  }
1155 
1156  if(cmdline.isset("partial-inline"))
1157  {
1159 
1160  status() << "Partial inlining" << eom;
1162 
1165  }
1166 
1167  if(cmdline.isset("remove-calls-no-body"))
1168  {
1169  status() << "Removing calls to functions without a body" << eom;
1170 
1171  remove_calls_no_bodyt remove_calls_no_body;
1172  remove_calls_no_body(goto_model.goto_functions);
1173 
1176  }
1177 
1178  if(cmdline.isset("constant-propagator"))
1179  {
1181 
1182  status() << "Propagating Constants" << eom;
1183 
1184  constant_propagator_ait constant_propagator_ai(goto_model);
1186  }
1187 
1188  // add generic checks, if needed
1189  goto_check(options, goto_model);
1190 
1191  // check for uninitalized local variables
1192  if(cmdline.isset("uninitialized-check"))
1193  {
1194  status() << "Adding checks for uninitialized local variables" << eom;
1196  }
1197 
1198  // check for maximum call stack size
1199  if(cmdline.isset("stack-depth"))
1200  {
1201  status() << "Adding check for maximum call stack size" << eom;
1202  stack_depth(
1203  goto_model,
1204  safe_string2size_t(cmdline.get_value("stack-depth")));
1205  }
1206 
1207  // ignore default/user-specified initialization of variables with static
1208  // lifetime
1209  if(cmdline.isset("nondet-static"))
1210  {
1211  status() << "Adding nondeterministic initialization of static/global "
1212  "variables" << eom;
1214  }
1215 
1216  if(cmdline.isset("slice-global-inits"))
1217  {
1218  status() << "Slicing away initializations of unused global variables"
1219  << eom;
1221  }
1222 
1223  if(cmdline.isset("string-abstraction"))
1224  {
1227 
1228  status() << "String Abstraction" << eom;
1230  goto_model,
1232  }
1233 
1234  // some analyses require function pointer removal and partial inlining
1235 
1236  if(cmdline.isset("remove-pointers") ||
1237  cmdline.isset("race-check") ||
1238  cmdline.isset("mm") ||
1239  cmdline.isset("isr") ||
1240  cmdline.isset("concurrency"))
1241  {
1243 
1244  status() << "Pointer Analysis" << eom;
1245  value_set_analysist value_set_analysis(ns);
1246  value_set_analysis(goto_model.goto_functions);
1247 
1248  if(cmdline.isset("remove-pointers"))
1249  {
1250  // removing pointers
1251  status() << "Removing Pointers" << eom;
1252  remove_pointers(goto_model, value_set_analysis);
1253  }
1254 
1255  if(cmdline.isset("race-check"))
1256  {
1257  status() << "Adding Race Checks" << eom;
1258  race_check(value_set_analysis, goto_model);
1259  }
1260 
1261  if(cmdline.isset("mm"))
1262  {
1263  std::string mm=cmdline.get_value("mm");
1264  memory_modelt model;
1265 
1266  // strategy of instrumentation
1267  instrumentation_strategyt inst_strategy;
1268  if(cmdline.isset("one-event-per-cycle"))
1269  inst_strategy=one_event_per_cycle;
1270  else if(cmdline.isset("minimum-interference"))
1271  inst_strategy=min_interference;
1272  else if(cmdline.isset("read-first"))
1273  inst_strategy=read_first;
1274  else if(cmdline.isset("write-first"))
1275  inst_strategy=write_first;
1276  else if(cmdline.isset("my-events"))
1277  inst_strategy=my_events;
1278  else
1279  /* default: instruments all unsafe pairs */
1280  inst_strategy=all;
1281 
1282  const unsigned max_var=
1283  cmdline.isset("max-var")?
1285  const unsigned max_po_trans=
1286  cmdline.isset("max-po-trans")?
1287  unsafe_string2unsigned(cmdline.get_value("max-po-trans")):0;
1288 
1289  if(mm=="tso")
1290  {
1291  status() << "Adding weak memory (TSO) Instrumentation" << eom;
1292  model=TSO;
1293  }
1294  else if(mm=="pso")
1295  {
1296  status() << "Adding weak memory (PSO) Instrumentation" << eom;
1297  model=PSO;
1298  }
1299  else if(mm=="rmo")
1300  {
1301  status() << "Adding weak memory (RMO) Instrumentation" << eom;
1302  model=RMO;
1303  }
1304  else if(mm=="power")
1305  {
1306  status() << "Adding weak memory (Power) Instrumentation" << eom;
1307  model=Power;
1308  }
1309  else
1310  {
1311  error() << "Unknown weak memory model `" << mm << "'" << eom;
1312  model=Unknown;
1313  }
1314 
1316 
1317  if(cmdline.isset("force-loop-duplication"))
1318  loops=all_loops;
1319  if(cmdline.isset("no-loop-duplication"))
1320  loops=no_loop;
1321 
1322  if(model!=Unknown)
1323  weak_memory(
1324  model,
1325  value_set_analysis,
1326  goto_model,
1327  cmdline.isset("scc"),
1328  inst_strategy,
1329  !cmdline.isset("cfg-kill"),
1330  cmdline.isset("no-dependencies"),
1331  loops,
1332  max_var,
1333  max_po_trans,
1334  !cmdline.isset("no-po-rendering"),
1335  cmdline.isset("render-cluster-file"),
1336  cmdline.isset("render-cluster-function"),
1337  cmdline.isset("cav11"),
1338  cmdline.isset("hide-internals"),
1340  cmdline.isset("ignore-arrays"));
1341  }
1342 
1343  // Interrupt handler
1344  if(cmdline.isset("isr"))
1345  {
1346  status() << "Instrumenting interrupt handler" << eom;
1347  interrupt(
1348  value_set_analysis,
1349  goto_model,
1350  cmdline.get_value("isr"));
1351  }
1352 
1353  // Memory-mapped I/O
1354  if(cmdline.isset("mmio"))
1355  {
1356  status() << "Instrumenting memory-mapped I/O" << eom;
1357  mmio(value_set_analysis, goto_model);
1358  }
1359 
1360  if(cmdline.isset("concurrency"))
1361  {
1362  status() << "Sequentializing concurrency" << eom;
1363  concurrency(value_set_analysis, goto_model);
1364  }
1365  }
1366 
1367  if(cmdline.isset("interval-analysis"))
1368  {
1369  status() << "Interval analysis" << eom;
1371  }
1372 
1373  if(cmdline.isset("havoc-loops"))
1374  {
1375  status() << "Havocking loops" << eom;
1377  }
1378 
1379  if(cmdline.isset("k-induction"))
1380  {
1381  bool base_case=cmdline.isset("base-case");
1382  bool step_case=cmdline.isset("step-case");
1383 
1384  if(step_case && base_case)
1385  throw "please specify only one of --step-case and --base-case";
1386  else if(!step_case && !base_case)
1387  throw "please specify one of --step-case and --base-case";
1388 
1389  unsigned k=unsafe_string2unsigned(cmdline.get_value("k-induction"));
1390 
1391  if(k==0)
1392  throw "please give k>=1";
1393 
1394  status() << "Instrumenting k-induction for k=" << k << ", "
1395  << (base_case?"base case":"step case") << eom;
1396 
1397  k_induction(goto_model, base_case, step_case, k);
1398  }
1399 
1400  if(cmdline.isset("function-enter"))
1401  {
1402  status() << "Function enter instrumentation" << eom;
1404  goto_model,
1405  cmdline.get_value("function-enter"));
1406  }
1407 
1408  if(cmdline.isset("function-exit"))
1409  {
1410  status() << "Function exit instrumentation" << eom;
1411  function_exit(
1412  goto_model,
1413  cmdline.get_value("function-exit"));
1414  }
1415 
1416  if(cmdline.isset("branch"))
1417  {
1418  status() << "Branch instrumentation" << eom;
1419  branch(
1420  goto_model,
1421  cmdline.get_value("branch"));
1422  }
1423 
1424  // add failed symbols
1426 
1427  // recalculate numbers, etc.
1429 
1430  // add loop ids
1432 
1433  // label the assertions
1435 
1436  // nondet volatile?
1437  if(cmdline.isset("nondet-volatile"))
1438  {
1439  status() << "Making volatile variables non-deterministic" << eom;
1441  }
1442 
1443  // reachability slice?
1444  if(cmdline.isset("reachability-slice"))
1445  {
1447 
1448  status() << "Performing a reachability slice" << eom;
1449  if(cmdline.isset("property"))
1451  else
1453  }
1454 
1455  if(cmdline.isset("fp-reachability-slice"))
1456  {
1458 
1459  status() << "Performing a function pointer reachability slice" << eom;
1461  goto_model, cmdline.get_comma_separated_values("fp-reachability-slice"));
1462  }
1463 
1464  // full slice?
1465  if(cmdline.isset("full-slice"))
1466  {
1469 
1470  status() << "Performing a full slice" << eom;
1471  if(cmdline.isset("property"))
1473  else
1475  }
1476 
1477  // splice option
1478  if(cmdline.isset("splice-call"))
1479  {
1480  status() << "Performing call splicing" << eom;
1481  std::string callercallee=cmdline.get_value("splice-call");
1482  if(splice_call(
1484  callercallee,
1487  throw 0;
1488  }
1489 
1490  if(cmdline.isset("generate-function-body"))
1491  {
1492  auto generate_implementation = generate_function_bodies_factory(
1493  cmdline.get_value("generate-function-body-options"),
1495  *message_handler);
1497  std::regex(cmdline.get_value("generate-function-body")),
1498  *generate_implementation,
1499  goto_model,
1500  *message_handler);
1501  }
1502 
1503  // aggressive slicer
1504  if(cmdline.isset("aggressive-slice"))
1505  {
1507 
1508  status() << "Slicing away initializations of unused global variables"
1509  << eom;
1511 
1512  status() << "Performing an aggressive slice" << eom;
1513  aggressive_slicert aggressive_slicer(goto_model, get_message_handler());
1514 
1515  if(cmdline.isset("aggressive-slice-call-depth"))
1516  aggressive_slicer.call_depth =
1517  safe_string2unsigned(cmdline.get_value("aggressive-slice-call-depth"));
1518 
1519  if(cmdline.isset("aggressive-slice-preserve-function"))
1520  aggressive_slicer.preserve_functions(
1521  cmdline.get_values("aggressive-slice-preserve-function"));
1522 
1523  if(cmdline.isset("property"))
1524  aggressive_slicer.user_specified_properties =
1525  cmdline.get_values("property");
1526 
1527  if(cmdline.isset("aggressive-slice-preserve-functions-containing"))
1528  aggressive_slicer.name_snippets =
1529  cmdline.get_values("aggressive-slice-preserve-functions-containing");
1530 
1531  aggressive_slicer.preserve_all_direct_paths =
1532  cmdline.isset("aggressive-slice-preserve-all-direct-paths");
1533 
1534  aggressive_slicer.doit();
1535 
1536  status() << "Performing a reachability slice" << eom;
1537  if(cmdline.isset("property"))
1539  else
1541  }
1542 
1543  // recalculate numbers, etc.
1545 }
1546 
1549 {
1550  // clang-format off
1551  std::cout << '\n' << banner_string("Goto-Instrument", CBMC_VERSION) << '\n'
1552  <<
1553  "* * Copyright (C) 2008-2013 * *\n"
1554  "* * Daniel Kroening * *\n"
1555  "* * kroening@kroening.com * *\n"
1556  "\n"
1557  "Usage: Purpose:\n"
1558  "\n"
1559  " goto-instrument [-?] [-h] [--help] show help\n"
1560  " goto-instrument in out perform instrumentation\n"
1561  "\n"
1562  "Main options:\n"
1563  " --document-properties-html generate HTML property documentation\n"
1564  " --document-properties-latex generate Latex property documentation\n"
1565  " --dump-c generate C source\n"
1566  " --dump-cpp generate C++ source\n"
1567  " --dot generate CFG graph in DOT format\n"
1568  " --interpreter do concrete execution\n"
1569  "\n"
1570  "Diagnosis:\n"
1571  " --show-loops show the loops in the program\n"
1573  " --show-symbol-table show loaded symbol table\n"
1574  " --list-symbols list symbols with type information\n"
1577  " --drop-unused-functions drop functions trivially unreachable from main function\n" // NOLINT(*)
1578  " --print-internal-representation\n" // NOLINTNEXTLINE(*)
1579  " show verbose internal representation of the program\n"
1580  " --list-undefined-functions list functions without body\n"
1581  " --show-struct-alignment show struct members that might be concurrently accessed\n" // NOLINT(*)
1582  " --show-natural-loops show natural loop heads\n"
1583  // NOLINTNEXTLINE(whitespace/line_length)
1584  " --list-calls-args list all function calls with their arguments\n"
1585  " --call-graph show graph of function calls\n"
1586  // NOLINTNEXTLINE(whitespace/line_length)
1587  " --reachable-call-graph show graph of function calls potentially reachable from main function\n"
1589  // NOLINTNEXTLINE(whitespace/line_length)
1590  " --show-threaded show instructions that may be executed by more than one thread\n"
1591  " --show-local-safe-pointers show pointer expressions that are trivially dominated by a not-null check\n" // NOLINT(*)
1592  " --show-safe-dereferences show pointer expressions that are trivially dominated by a not-null check\n" // NOLINT(*)
1593  " *and* used as a dereference operand\n" // NOLINT(*)
1595  // NOLINTNEXTLINE(whitespace/line_length)
1596  " --validate-goto-binary check the well-formedness of the passed in goto\n"
1597  " binary and then exit\n"
1598  "\n"
1599  "Safety checks:\n"
1600  " --no-assertions ignore user assertions\n"
1602  " --uninitialized-check add checks for uninitialized locals (experimental)\n" // NOLINT(*)
1603  " --error-label label check that label is unreachable\n"
1604  " --stack-depth n add check that call stack size of non-inlined functions never exceeds n\n" // NOLINT(*)
1605  " --race-check add floating-point data race checks\n"
1606  "\n"
1607  "Semantic transformations:\n"
1608  " --nondet-volatile makes reads from volatile variables non-deterministic\n" // NOLINT(*)
1609  " --unwind <n> unwinds the loops <n> times\n"
1610  " --unwindset L:B,... unwind loop L with a bound of B\n"
1611  " --unwindset-file <file> read unwindset from file\n"
1612  " --partial-loops permit paths with partial loops\n"
1613  " --unwinding-assertions generate unwinding assertions\n"
1614  " --continue-as-loops add loop for remaining iterations after unwound part\n" // NOLINT(*)
1615  " --isr <function> instruments an interrupt service routine\n"
1616  " --mmio instruments memory-mapped I/O\n"
1617  " --nondet-static add nondeterministic initialization of variables with static lifetime\n" // NOLINT(*)
1618  " --check-invariant function instruments invariant checking function\n"
1619  " --remove-pointers converts pointer arithmetic to base+offset expressions\n" // NOLINT(*)
1620  " --splice-call caller,callee prepends a call to callee in the body of caller\n" // NOLINT(*)
1621  " --undefined-function-is-assume-false\n"
1622  // NOLINTNEXTLINE(whitespace/line_length)
1623  " convert each call to an undefined function to assume(false)\n"
1625  "\n"
1626  "Loop transformations:\n"
1627  " --k-induction <k> check loops with k-induction\n"
1628  " --step-case k-induction: do step-case\n"
1629  " --base-case k-induction: do base-case\n"
1630  " --havoc-loops over-approximate all loops\n"
1631  " --accelerate add loop accelerators\n"
1632  " --skip-loops <loop-ids> add gotos to skip selected loops during execution\n" // NOLINT(*)
1633  "\n"
1634  "Memory model instrumentations:\n"
1635  " --mm <tso,pso,rmo,power> instruments a weak memory model\n"
1636  " --scc detects critical cycles per SCC (one thread per SCC)\n" // NOLINT(*)
1637  " --one-event-per-cycle only instruments one event per cycle\n"
1638  " --minimum-interference instruments an optimal number of events\n"
1639  " --my-events only instruments events whose ids appear in inst.evt\n" // NOLINT(*)
1640  " --cfg-kill enables symbolic execution used to reduce spurious cycles\n" // NOLINT(*)
1641  " --no-dependencies no dependency analysis\n"
1642  // NOLINTNEXTLINE(whitespace/line_length)
1643  " --no-po-rendering no representation of the threads in the dot\n"
1644  " --render-cluster-file clusterises the dot by files\n"
1645  " --render-cluster-function clusterises the dot by functions\n"
1646  "\n"
1647  "Slicing:\n"
1649  " --full-slice slice away instructions that don't affect assertions\n" // NOLINT(*)
1650  " --property id slice with respect to specific property only\n" // NOLINT(*)
1651  " --slice-global-inits slice away initializations of unused global variables\n" // NOLINT(*)
1652  " --aggressive-slice remove bodies of any functions not on the shortest path between\n" // NOLINT(*)
1653  " the start function and the function containing the property(s)\n" // NOLINT(*)
1654  " --aggressive-slice-call-depth <n>\n"
1655  " used with aggressive-slice, preserves all functions within <n> function calls\n" // NOLINT(*)
1656  " of the functions on the shortest path\n"
1657  " --aggressive-slice-preserve-function <f>\n"
1658  " force the aggressive slicer to preserve function <f>\n" // NOLINT(*)
1659  " --aggressive-slice-preserve-function containing <f>\n"
1660  " force the aggressive slicer to preserve all functions with names containing <f>\n" // NOLINT(*)
1661  "--aggressive-slice-preserve-all-direct-paths \n"
1662  " force aggressive slicer to preserve all direct paths\n" // NOLINT(*)
1663  "\n"
1664  "Further transformations:\n"
1665  " --constant-propagator propagate constants and simplify expressions\n" // NOLINT(*)
1666  " --inline perform full inlining\n"
1667  " --partial-inline perform partial inlining\n"
1668  " --function-inline <function> transitively inline all calls <function> makes\n" // NOLINT(*)
1669  " --no-caching disable caching of intermediate results during transitive function inlining\n" // NOLINT(*)
1670  " --log <file> log in json format which code segments were inlined, use with --function-inline\n" // NOLINT(*)
1671  " --remove-function-pointers replace function pointers by case statement over function calls\n" // NOLINT(*)
1674  " --add-library add models of C library functions\n"
1675  " --model-argc-argv <n> model up to <n> command line arguments\n"
1676  // NOLINTNEXTLINE(whitespace/line_length)
1677  " --remove-function-body <f> remove the implementation of function <f> (may be repeated)\n"
1679  "\n"
1680  "Other options:\n"
1681  " --no-system-headers with --dump-c/--dump-cpp: generate C source expanding libc includes\n" // NOLINT(*)
1682  " --use-all-headers with --dump-c/--dump-cpp: generate C source with all includes\n" // NOLINT(*)
1683  " --harness with --dump-c/--dump-cpp: include input generator in output\n" // NOLINT(*)
1684  " --version show version and exit\n"
1685  HELP_FLUSH
1686  " --xml-ui use XML-formatted output\n"
1687  " --json-ui use JSON-formatted output\n"
1689  "\n";
1690  // clang-format on
1691 }
cprover_library.h
cmdlinet::args
argst args
Definition: cmdline.h:44
CBMC_VERSION
const char * CBMC_VERSION
Definition: version.cpp:1
Unknown
@ Unknown
Definition: wmm.h:19
HELP_REACHABILITY_SLICER
#define HELP_REACHABILITY_SLICER
Definition: reachability_slicer.h:43
configt::ansi_ct::defines
std::list< std::string > defines
Definition: config.h:121
HELP_SHOW_GOTO_FUNCTIONS
#define HELP_SHOW_GOTO_FUNCTIONS
Definition: show_goto_functions.h:26
no_loop
@ no_loop
Definition: wmm.h:40
TSO
@ TSO
Definition: wmm.h:20
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
string_abstraction.h
concurrency.h
horn_encoding
void horn_encoding(const goto_modelt &, std::ostream &)
Definition: horn_encoding.cpp:18
havoc_loops.h
PARSE_OPTIONS_GOTO_CHECK
#define PARSE_OPTIONS_GOTO_CHECK(cmdline, options)
Definition: goto_check.h:58
class_hierarchyt
Non-graph-based representation of the class hierarchy.
Definition: class_hierarchy.h:42
horn_encoding.h
unwindsett::parse_unwindset_file
void parse_unwindset_file(const std::string &file_name)
Definition: unwindset.cpp:85
goto_unwindt::unwind_strategyt
unwind_strategyt
Definition: unwind.h:27
local_bitvector_analysis.h
cmdlinet::isset
virtual bool isset(char option) const
Definition: cmdline.cpp:27
dependence_grapht
Definition: dependence_graph.h:217
print_global_state_size
void print_global_state_size(const goto_modelt &goto_model)
Definition: count_eloc.cpp:149
goto_instrument_parse_optionst::do_remove_returns
void do_remove_returns()
Definition: goto_instrument_parse_options.cpp:904
goto_instrument_parse_optionst::help
virtual void help()
display command line help
Definition: goto_instrument_parse_options.cpp:1548
stack_depth
void stack_depth(goto_programt &goto_program, const symbol_exprt &symbol, const std::size_t i_depth, const exprt &max_depth)
Definition: stack_depth.cpp:43
RMO
@ RMO
Definition: wmm.h:22
goto_instrument_parse_optionst::do_partial_inlining
void do_partial_inlining()
Definition: goto_instrument_parse_options.cpp:890
goto_inline.h
optionst
Definition: options.h:22
goto_instrument_parse_optionst::function_pointer_removal_done
bool function_pointer_removal_done
Definition: goto_instrument_parse_options.h:141
mutex_init_instrumentation
void mutex_init_instrumentation(const symbol_tablet &symbol_table, goto_programt &goto_program, typet lock_type)
Definition: thread_instrumentation.cpp:85
skip_loops.h
show_class_hierarchy
void show_class_hierarchy(const class_hierarchyt &hierarchy, ui_message_handlert &message_handler, bool children_only)
Output the class hierarchy.
Definition: class_hierarchy.cpp:261
messaget::M_STATISTICS
@ M_STATISTICS
Definition: message.h:161
read_goto_binary
bool read_goto_binary(const std::string &filename, goto_modelt &dest, message_handlert &message_handler)
Read a goto binary from a file, but do not update config.
Definition: read_goto_binary.cpp:36
messaget::status
mstreamt & status() const
Definition: message.h:401
show_properties
void show_properties(const namespacet &ns, const irep_idt &identifier, message_handlert &message_handler, ui_message_handlert::uit ui, const goto_programt &goto_program)
Definition: show_properties.cpp:49
custom_bitvector_analysis.h
goto_function_inline_and_log
jsont goto_function_inline_and_log(goto_modelt &goto_model, const irep_idt function, message_handlert &message_handler, bool adjust_function, bool caching)
Definition: goto_inline.cpp:286
goto_partial_inline
void goto_partial_inline(goto_modelt &goto_model, message_handlert &message_handler, unsigned smallfunc_limit, bool adjust_function)
Inline all function calls to functions either marked as "inlined" or smaller than smallfunc_limit (by...
Definition: goto_inline.cpp:109
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
concurrency
void concurrency(value_setst &value_sets, goto_modelt &goto_model)
Definition: concurrency.cpp:222
remove_virtual_functions
void remove_virtual_functions(const symbol_table_baset &symbol_table, goto_functionst &goto_functions)
Remove virtual function calls from all functions in the specified list and replace them with their mo...
Definition: remove_virtual_functions.cpp:568
dot
void dot(const goto_modelt &src, std::ostream &out)
Definition: dot.cpp:352
remove_skip
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:86
local_safe_pointerst
A very simple, cheap analysis to determine when dereference operations are trivially guarded by a che...
Definition: local_safe_pointers.h:24
model_argc_argv
bool model_argc_argv(goto_modelt &goto_model, unsigned max_argc, message_handlert &message_handler)
Set up argv with up to max_argc pointers into an array of 4096 bytes.
Definition: model_argc_argv.cpp:39
parameter_assignments
void parameter_assignments(symbol_tablet &symbol_table, goto_functionst &goto_functions)
removes returns
Definition: parameter_assignments.cpp:98
unwindsett::parse_unwindset
void parse_unwindset(const std::string &unwindset)
Definition: unwindset.cpp:24
splice_call
bool splice_call(goto_functionst &goto_functions, const std::string &callercallee, const symbol_tablet &symbol_table, message_handlert &message_handler)
Definition: splice_call.cpp:38
skip_loops
static bool skip_loops(goto_programt &goto_program, const loop_idst &loop_ids, messaget &message)
Definition: skip_loops.cpp:24
show_goto_functions
void show_goto_functions(const namespacet &ns, message_handlert &message_handler, ui_message_handlert::uit ui, const goto_functionst &goto_functions, bool list_only)
Definition: show_goto_functions.cpp:28
remove_virtual_functions.h
remove_asm.h
HELP_SHOW_CLASS_HIERARCHY
#define HELP_SHOW_CLASS_HIERARCHY
Definition: class_hierarchy.h:29
constant_propagator.h
reachability_slicer
void reachability_slicer(goto_modelt &goto_model, const bool include_forward_reachability)
Perform reachability slicing on goto_model, with respect to the criterion given by all properties.
Definition: reachability_slicer.cpp:351
PSO
@ PSO
Definition: wmm.h:21
value_set_analysis_templatet
Definition: value_set_analysis.h:30
interpreter.h
show_uninitialized
void show_uninitialized(const goto_modelt &goto_model, std::ostream &out)
Definition: uninitialized.cpp:211
goto_unwindt::unwind_strategyt::CONTINUE
@ CONTINUE
add_uninitialized_locals_assertions
void add_uninitialized_locals_assertions(goto_modelt &goto_model)
Definition: uninitialized.cpp:201
ait
Definition: ai.h:365
remove_calls_no_body.h
goto_instrument_parse_optionst::do_remove_const_function_pointers_only
void do_remove_const_function_pointers_only()
Remove function pointers that can be resolved by analysing const variables (i.e.
Definition: goto_instrument_parse_options.cpp:873
Power
@ Power
Definition: wmm.h:23
mmio.h
show_loop_ids
void show_loop_ids(ui_message_handlert::uit ui, const goto_modelt &goto_model)
Definition: loop_ids.cpp:21
generate_function_bodies
void generate_function_bodies(const std::regex &functions_regex, const generate_function_bodiest &generate_function_body, goto_modelt &model, message_handlert &message_handler)
Generate function bodies with some default behavior A list of currently accepted command line argumen...
Definition: generate_function_bodies.cpp:454
goto_unwindt::unwind_strategyt::ASSERT
@ ASSERT
aggressive_slicert::preserve_all_direct_paths
bool preserve_all_direct_paths
Definition: aggressive_slicer.h:70
optionst::set_option
void set_option(const std::string &option, const bool value)
Definition: options.cpp:26
call_graph.h
weak_memory.h
k_induction.h
messaget::eom
static eomt eom
Definition: message.h:284
string_abstraction
void string_abstraction(symbol_tablet &symbol_table, message_handlert &message_handler, goto_programt &dest)
Definition: string_abstraction.cpp:65
show_symbol_table
void show_symbol_table(const symbol_tablet &symbol_table, ui_message_handlert &ui)
Definition: show_symbol_table.cpp:283
configt::ansi_c
struct configt::ansi_ct ansi_c
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:27
version.h
remove_unused_functions
void remove_unused_functions(goto_modelt &goto_model, message_handlert &message_handler)
Definition: remove_unused_functions.cpp:18
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:143
call_grapht::output_xml
void output_xml(std::ostream &out) const
Definition: call_graph.cpp:281
race_check.h
nondet_static.h
jsont
Definition: json.h:23
document_properties.h
nondet_volatile
void nondet_volatile(symbol_tablet &symbol_table, goto_programt &goto_program)
Definition: nondet_volatile.cpp:80
string_instrumentation.h
write_first
@ write_first
Definition: wmm.h:31
loop_strategyt
loop_strategyt
Definition: wmm.h:36
local_safe_pointerst::output
void output(std::ostream &stream, const goto_programt &program)
Output non-null expressions per instruction in human-readable format.
Definition: local_safe_pointers.cpp:180
call_grapht::output_dot
void output_dot(std::ostream &out) const
Definition: call_graph.cpp:254
interpreter
void interpreter(const goto_modelt &goto_model, message_handlert &message_handler)
Definition: interpreter.cpp:1079
safe_string2size_t
std::size_t safe_string2size_t(const std::string &str, int base)
Definition: string2int.cpp:59
show_value_sets
void show_value_sets(ui_message_handlert::uit ui, const goto_modelt &goto_model, const value_set_analysist &value_set_analysis)
Definition: show_value_sets.cpp:21
label_properties
void label_properties(goto_modelt &goto_model)
Definition: set_properties.cpp:43
goto_modelt::validate
void validate(const validation_modet vm) const
Check that the goto model is well-formed.
Definition: goto_model.h:97
print_struct_alignment_problems
void print_struct_alignment_problems(const symbol_tablet &symbol_table, std::ostream &out)
Definition: alignment_checks.cpp:21
reaching_definitions_analysist
Definition: reaching_definitions.h:340
nondet_static
void nondet_static(const namespacet &ns, goto_functionst &goto_functions, const irep_idt &fct_name)
Nondeterministically initializes global scope variables in a goto-function.
Definition: nondet_static.cpp:71
write_goto_binary.h
list_undefined_functions
void list_undefined_functions(const goto_modelt &goto_model, std::ostream &os)
Definition: undefined_functions.cpp:22
cmdlinet::get_comma_separated_values
std::list< std::string > get_comma_separated_values(const char *option) const
Definition: cmdline.cpp:122
call_grapht::create_from_root_function
static call_grapht create_from_root_function(const goto_modelt &model, const irep_idt &root, bool collect_callsites)
Definition: call_graph.h:48
thread_instrumentation.h
splice_call.h
unwindsett::parse_unwind
void parse_unwind(const std::string &unwind)
Definition: unwindset.cpp:18
goto_unwindt::unwind_strategyt::PARTIAL
@ PARTIAL
is_threadedt
Definition: is_threaded.h:21
goto_unwindt::unwind_strategyt::ASSUME
@ ASSUME
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
show_natural_loops
void show_natural_loops(const goto_modelt &goto_model, std::ostream &out)
Definition: natural_loops.cpp:14
string2int.h
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:166
set_properties.h
show_call_sequences
void show_call_sequences(const irep_idt &caller, const goto_programt &goto_program)
Definition: call_sequences.cpp:27
mmio
void mmio(value_setst &value_sets, const symbol_tablet &symbol_table, goto_programt &goto_program)
Definition: mmio.cpp:24
aggressive_slicert::doit
void doit()
Removes the body of all functions except those on the shortest path or functions that are reachable f...
Definition: aggressive_slicer.cpp:68
full_slicer
void full_slicer(goto_functionst &goto_functions, const namespacet &ns, const slicing_criteriont &criterion)
Definition: full_slicer.cpp:367
dot.h
interrupt.h
escape_analysist
Definition: escape_analysis.h:113
messaget::result
mstreamt & result() const
Definition: message.h:396
show_symbol_table_brief
void show_symbol_table_brief(const symbol_tablet &symbol_table, ui_message_handlert &ui)
Definition: show_symbol_table.cpp:312
messaget::error
mstreamt & error() const
Definition: message.h:386
banner_string
std::string banner_string(const std::string &front_end, const std::string &version)
Definition: parse_options.cpp:87
goto_instrument_parse_optionst::doit
virtual int doit()
invoke main modules
Definition: goto_instrument_parse_options.cpp:105
goto_programt::output_instruction
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &instruction) const
Output a single instruction.
Definition: goto_program.cpp:37
all_loops
@ all_loops
Definition: wmm.h:39
unwindsett
Definition: unwindset.h:21
ai_baset::output
virtual void output(const namespacet &ns, const goto_functionst &goto_functions, std::ostream &out) const
Output the abstract states for a whole program.
Definition: ai.cpp:24
branch
void branch(goto_modelt &goto_model, const irep_idt &id)
Definition: branch.cpp:20
goto_instrument_parse_optionst::do_indirect_call_and_rtti_removal
void do_indirect_call_and_rtti_removal(bool force=false)
Definition: goto_instrument_parse_options.cpp:851
goto_instrument_parse_optionst::get_goto_program
void get_goto_program()
Definition: goto_instrument_parse_options.cpp:915
check_call_sequence
void check_call_sequence(const goto_modelt &goto_model)
Definition: call_sequences.cpp:252
remove_function_pointers
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)
Definition: remove_function_pointers.cpp:520
HELP_GOTO_PROGRAM_STATS
#define HELP_GOTO_PROGRAM_STATS
Definition: count_eloc.h:30
points_tot
Definition: points_to.h:22
dump_c
void dump_c(const goto_functionst &src, const bool use_system_headers, const bool use_all_headers, const bool include_harness, const namespacet &ns, std::ostream &out)
Definition: dump_c.cpp:1403
undefined_function_abort_path
void undefined_function_abort_path(goto_modelt &goto_model)
Definition: undefined_functions.cpp:34
unwind.h
document_properties_latex
void document_properties_latex(const goto_modelt &goto_model, std::ostream &out)
Definition: document_properties.cpp:372
property_slicer
void property_slicer(goto_functionst &goto_functions, const namespacet &ns, const std::list< std::string > &properties)
Definition: full_slicer.cpp:390
show_properties.h
is_threaded.h
goto_instrument_parse_optionst::instrument_goto_program
void instrument_goto_program()
Definition: goto_instrument_parse_options.cpp:931
goto_unwindt
Definition: unwind.h:24
HELP_REMOVE_CALLS_NO_BODY
#define HELP_REMOVE_CALLS_NO_BODY
Definition: remove_calls_no_body.h:42
cmdlinet::get_value
std::string get_value(char option) const
Definition: cmdline.cpp:45
show_symbol_table.h
remove_function.h
HELP_SHOW_PROPERTIES
#define HELP_SHOW_PROPERTIES
Definition: show_properties.h:29
CPROVER_EXIT_EXCEPTION_GOTO_INSTRUMENT
#define CPROVER_EXIT_EXCEPTION_GOTO_INSTRUMENT
Definition: exit_codes.h:43
k_induction
void k_induction(goto_modelt &goto_model, bool base_case, bool step_case, unsigned k)
Definition: k_induction.cpp:152
custom_bitvector_analysist
Definition: custom_bitvector_analysis.h:151
goto_check
void goto_check(const namespacet &ns, const optionst &options, const irep_idt &mode, goto_functionst::goto_functiont &goto_function)
Definition: goto_check.cpp:1784
HELP_REMOVE_CONST_FUNCTION_POINTERS
#define HELP_REMOVE_CONST_FUNCTION_POINTERS
Definition: remove_const_function_pointers.h:111
count_eloc
void count_eloc(const goto_modelt &goto_model)
Definition: count_eloc.cpp:50
accelerate.h
configt::ansi_ct::arch
irep_idt arch
Definition: config.h:84
aggressive_slicert::call_depth
std::size_t call_depth
Definition: aggressive_slicer.h:68
function_enter
void function_enter(goto_modelt &goto_model, const irep_idt &id)
Definition: function.cpp:72
local_safe_pointers.h
reaching_definitions.h
escape_analysist::instrument
void instrument(goto_modelt &)
Definition: escape_analysis.cpp:434
slice_global_inits
void slice_global_inits(goto_modelt &goto_model)
Definition: slice_global_inits.cpp:31
configt::set_from_symbol_table
void set_from_symbol_table(const symbol_tablet &)
Definition: config.cpp:1171
code_contracts
void code_contracts(goto_modelt &goto_model)
Definition: code_contracts.cpp:412
accelerate_functions
void accelerate_functions(goto_modelt &goto_model, message_handlert &message_handler, bool use_z3)
Definition: accelerate.cpp:652
goto_function_inline
void goto_function_inline(goto_modelt &goto_model, const irep_idt function, message_handlert &message_handler, bool adjust_function, bool caching)
Inline all function calls made from a particular function.
Definition: goto_inline.cpp:218
goto_instrument_parse_optionst::register_languages
virtual void register_languages()
Definition: goto_instrument_languages.cpp:19
goto_functionst::compute_loop_numbers
void compute_loop_numbers()
Definition: goto_functions.cpp:52
CPROVER_EXIT_CONVERSION_FAILED
#define CPROVER_EXIT_CONVERSION_FAILED
Failure to convert / write to another format.
Definition: exit_codes.h:63
widen
std::wstring widen(const char *s)
Definition: unicode.cpp:52
HELP_REPLACE_FUNCTION_BODY
#define HELP_REPLACE_FUNCTION_BODY
Definition: generate_function_bodies.h:76
branch.h
read_goto_binary.h
local_bitvector_analysist::output
void output(std::ostream &out, const goto_functiont &goto_function, const namespacet &ns) const
Definition: local_bitvector_analysis.cpp:327
weak_memory
void weak_memory(memory_modelt model, value_setst &value_sets, goto_modelt &goto_model, bool SCC, instrumentation_strategyt event_strategy, bool no_cfg_kill, bool no_dependencies, loop_strategyt duplicate_body, unsigned input_max_var, unsigned input_max_po_trans, bool render_po, bool render_file, bool render_function, bool cav11_option, bool hide_internals, message_handlert &message_handler, bool ignore_arrays)
Definition: weak_memory.cpp:104
full_slicer.h
goto_instrument_parse_optionst::partial_inlining_done
bool partial_inlining_done
Definition: goto_instrument_parse_options.h:142
memory_modelt
memory_modelt
Definition: wmm.h:17
local_safe_pointerst::output_safe_dereferences
void output_safe_dereferences(std::ostream &stream, const goto_programt &program)
Output safely dereferenced expressions per instruction in human-readable format.
Definition: local_safe_pointers.cpp:221
my_events
@ my_events
Definition: wmm.h:32
safe_string2unsigned
unsigned safe_string2unsigned(const std::string &str, int base)
Definition: string2int.cpp:54
parse_options_baset::main
virtual int main()
Definition: parse_options.cpp:50
read_first
@ read_first
Definition: wmm.h:30
aggressive_slicert::user_specified_properties
std::list< std::string > user_specified_properties
Definition: aggressive_slicer.h:65
global_may_alias_analysist
This is a may analysis (i.e.
Definition: global_may_alias.h:106
function_path_reachability_slicer
void function_path_reachability_slicer(goto_modelt &goto_model, const std::list< std::string > &functions_list)
Perform reachability slicing on goto_model for selected functions.
Definition: reachability_slicer.cpp:382
remove_returns.h
remove_unused_functions.h
config
configt config
Definition: config.cpp:24
remove_functions
void remove_functions(goto_modelt &goto_model, const std::list< std::string > &names, message_handlert &message_handler)
Remove the body of all functions listed in "names" such that an analysis will treat it as a side-effe...
Definition: remove_function.cpp:67
local_bitvector_analysist
Definition: local_bitvector_analysis.h:23
ui_message_handlert::get_ui
uit get_ui() const
Definition: ui_message.h:30
function.h
call_grapht
A call graph (https://en.wikipedia.org/wiki/Call_graph) for a GOTO model or GOTO functions collection...
Definition: call_graph.h:38
uninitialized.h
points_to.h
messaget::get_message_handler
message_handlert & get_message_handler()
Definition: message.h:174
goto_instrument_parse_optionst::remove_returns_done
bool remove_returns_done
Definition: goto_instrument_parse_options.h:143
class_hierarchy.h
interval_domain.h
stack_depth.h
show_locations.h
interrupt
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
show_locations
void show_locations(ui_message_handlert::uit ui, const irep_idt function_id, const goto_programt &goto_program)
Definition: show_locations.cpp:23
messaget::message_handler
message_handlert * message_handler
Definition: message.h:426
aggressive_slicert
The aggressive slicer removes the body of all the functions except those on the shortest path,...
Definition: aggressive_slicer.h:36
undefined_functions.h
min_interference
@ min_interference
Definition: wmm.h:29
arrays_only
@ arrays_only
Definition: wmm.h:38
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
validation_modet::EXCEPTION
@ EXCEPTION
generate_function_bodies_factory
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.
Definition: generate_function_bodies.cpp:335
HELP_GOTO_CHECK
#define HELP_GOTO_CHECK
Definition: goto_check.h:43
cprover_c_library_factory
void cprover_c_library_factory(const std::set< irep_idt > &functions, symbol_tablet &symbol_table, message_handlert &message_handler)
Definition: cprover_library.cpp:77
call_sequences.h
goto_instrument_parse_optionst::get_ui
ui_message_handlert::uit get_ui()
Definition: goto_instrument_parse_options.h:147
remove_calls_no_bodyt
Definition: remove_calls_no_body.h:19
symbolt
Symbol table entry.
Definition: symbol.h:27
configt::set
bool set(const cmdlinet &cmdline)
Definition: config.cpp:767
rw_set.h
exit_codes.h
call_grapht::output
void output(std::ostream &out) const
Definition: call_graph.cpp:271
natural_loops.h
constant_propagator_ait
Definition: constant_propagator.h:162
goto_program_dereference.h
one_event_per_cycle
@ one_event_per_cycle
Definition: wmm.h:33
remove_returns
void remove_returns(symbol_table_baset &symbol_table, goto_functionst &goto_functions)
removes returns
Definition: remove_returns.cpp:261
show_value_sets.h
aggressive_slicert::name_snippets
std::list< std::string > name_snippets
Definition: aggressive_slicer.h:69
CPROVER_EXIT_USAGE_ERROR
#define CPROVER_EXIT_USAGE_ERROR
A usage error is returned when the command line is invalid or conflicting.
Definition: exit_codes.h:33
nondet_volatile.h
CPROVER_PREFIX
#define CPROVER_PREFIX
Definition: cprover_prefix.h:14
replace_callst
Definition: replace_calls.h:18
unsafe_string2unsigned
unsigned unsafe_string2unsigned(const std::string &str, int base)
Definition: string2int.cpp:69
goto_functionst::update
void update()
Definition: goto_functions.h:91
json.h
remove_asm
void remove_asm(goto_functionst &goto_functions, symbol_tablet &symbol_table)
Replaces inline assembly instructions in the goto program (i.e., instructions of kind OTHER with a co...
Definition: remove_asm.cpp:516
unicode.h
parameter_assignments.h
aggressive_slicert::preserve_functions
void preserve_functions(const std::list< std::string > &function_list)
Adds a list of functions to the set of functions for the aggressive slicer to preserve.
Definition: aggressive_slicer.h:61
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
grapht::output_dot
void output_dot(std::ostream &out) const
Definition: graph.h:961
class_hierarchyt::output_dot
void output_dot(std::ostream &) const
Output class hierarchy in Graphviz DOT format.
Definition: class_hierarchy.cpp:217
custom_bitvector_analysist::check
void check(const goto_modelt &, bool xml, std::ostream &)
Definition: custom_bitvector_analysis.cpp:754
config.h
points_tot::output
void output(std::ostream &out) const
Definition: points_to.cpp:36
loop_ids.h
forall_goto_functions
#define forall_goto_functions(it, functions)
Definition: goto_functions.h:149
reachability_slicer.h
goto_instrument_parse_optionst::goto_model
goto_modelt goto_model
Definition: goto_instrument_parse_options.h:145
goto_instrument_parse_optionst::ui_message_handler
ui_message_handlert ui_message_handler
Definition: goto_instrument_parse_options.h:130
model_argc_argv.h
function_exit
void function_exit(goto_modelt &goto_model, const irep_idt &id)
Definition: function.cpp:98
instrumentation_strategyt
instrumentation_strategyt
Definition: wmm.h:26
slice_global_inits.h
add_failed_symbols.h
goto_functionst::entry_point
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
Definition: goto_functions.h:101
race_check
void race_check(value_setst &value_sets, symbol_tablet &symbol_table, goto_programt &goto_program, w_guardst &w_guards)
Definition: race_check.cpp:161
goto_convert_functions.h
document_properties_html
void document_properties_html(const goto_modelt &goto_model, std::ostream &out)
Definition: document_properties.cpp:365
add_failed_symbols
void add_failed_symbols(symbol_table_baset &symbol_table)
Create a failed-dereference symbol for all symbols in the given table that need one (i....
Definition: add_failed_symbols.cpp:76
global_may_alias.h
havoc_loops
void havoc_loops(goto_modelt &goto_model)
Definition: havoc_loops.cpp:188
alignment_checks.h
write_goto_binary
bool write_goto_binary(std::ostream &out, const goto_modelt &goto_model, int version)
Writes a goto program to disc.
Definition: write_goto_binary.cpp:127
CPROVER_EXIT_SUCCESS
#define CPROVER_EXIT_SUCCESS
Success indicates the required analysis has been performed without error.
Definition: exit_codes.h:16
value_set_analysis.h
HELP_REPLACE_CALLS
#define HELP_REPLACE_CALLS
Definition: replace_calls.h:50
messaget::eval_verbosity
static unsigned eval_verbosity(const std::string &user_input, const message_levelt default_verbosity, message_handlert &dest)
Parse a (user-)provided string as a verbosity level and set it as the verbosity of dest.
Definition: message.cpp:98
remove_skip.h
list_eloc
void list_eloc(const goto_modelt &goto_model)
Definition: count_eloc.cpp:64
remove_pointers
void remove_pointers(goto_programt &goto_program, symbol_tablet &symbol_table, value_setst &value_sets)
Definition: goto_program_dereference.cpp:400
all
@ all
Definition: wmm.h:28
dump_c.h
thread_exit_instrumentation
void thread_exit_instrumentation(goto_programt &goto_program)
Definition: thread_instrumentation.cpp:25
cmdlinet::get_values
const std::list< std::string > & get_values(const std::string &option) const
Definition: cmdline.cpp:110
remove_function_pointers.h
parse_options_baset::cmdline
cmdlinet cmdline
Definition: parse_options.h:23
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
rw_set_functiont
Definition: rw_set.h:200
print_path_lengths
void print_path_lengths(const goto_modelt &goto_model)
Definition: count_eloc.cpp:81
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
cprover_library.h
restore_returns
void restore_returns(goto_modelt &goto_model)
restores return statements
Definition: remove_returns.cpp:449
dump_cpp
void dump_cpp(const goto_functionst &src, const bool use_system_headers, const bool use_all_headers, const bool include_harness, const namespacet &ns, std::ostream &out)
Definition: dump_c.cpp:1421
forall_goto_program_instructions
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:804
code_contracts.h
interval_analysis.h
list_calls_and_arguments
static void list_calls_and_arguments(const namespacet &ns, const goto_programt &goto_program)
Definition: call_sequences.cpp:271
validation_modet::INVARIANT
@ INVARIANT
dependence_graph.h
goto_unwindt::output_log_json
jsont output_log_json() const
Definition: unwind.h:70
HELP_TIMESTAMP
#define HELP_TIMESTAMP
Definition: timestamper.h:14
goto_instrument_parse_options.h
HELP_FLUSH
#define HELP_FLUSH
Definition: ui_message.h:104
interval_analysis
void interval_analysis(goto_modelt &goto_model)
Initialises the abstract interpretation over interval domain and instruments instructions using inter...
Definition: interval_analysis.cpp:93
cprover_cpp_library_factory
void cprover_cpp_library_factory(const std::set< irep_idt > &functions, symbol_tablet &symbol_table, message_handlert &message_handler)
Definition: cprover_library.cpp:38
goto_inline
void goto_inline(goto_modelt &goto_model, message_handlert &message_handler, bool adjust_function)
Definition: goto_inline.cpp:24
escape_analysis.h
HELP_VALIDATE
#define HELP_VALIDATE
Definition: validation_interface.h:16