cprover
goto_instrument_parse_options.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Main Module
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
13 
14 #include <fstream>
15 #include <iostream>
16 #include <memory>
17 
18 #include <util/config.h>
19 #include <util/exception_utils.h>
20 #include <util/exit_codes.h>
21 #include <util/json.h>
22 #include <util/string2int.h>
23 #include <util/string_utils.h>
24 #include <util/version.h>
25 
26 #ifdef _MSC_VER
27 # include <util/unicode.h>
28 #endif
29 
36 #include <goto-programs/loop_ids.h>
53 
58 
59 #include <analyses/call_graph.h>
67 #include <analyses/is_threaded.h>
68 #include <analyses/lexical_loops.h>
71 #include <analyses/natural_loops.h>
73 #include <analyses/sese_regions.h>
74 
75 #include <ansi-c/ansi_c_language.h>
77 #include <ansi-c/cprover_library.h>
78 
79 #include <assembler/remove_asm.h>
80 
81 #include <cpp/cprover_library.h>
82 
83 #include "accelerate/accelerate.h"
84 #include "alignment_checks.h"
85 #include "branch.h"
86 #include "call_sequences.h"
87 #include "concurrency.h"
88 #include "document_properties.h"
89 #include "dot.h"
90 #include "dump_c.h"
91 #include "full_slicer.h"
92 #include "function.h"
93 #include "havoc_loops.h"
94 #include "horn_encoding.h"
96 #include "interrupt.h"
97 #include "k_induction.h"
98 #include "mmio.h"
99 #include "model_argc_argv.h"
100 #include "nondet_static.h"
101 #include "nondet_volatile.h"
102 #include "points_to.h"
103 #include "race_check.h"
104 #include "reachability_slicer.h"
105 #include "remove_function.h"
106 #include "rw_set.h"
107 #include "show_locations.h"
108 #include "skip_loops.h"
109 #include "splice_call.h"
110 #include "stack_depth.h"
111 #include "thread_instrumentation.h"
112 #include "undefined_functions.h"
113 #include "uninitialized.h"
114 #include "unwind.h"
115 #include "unwindset.h"
116 #include "value_set_fi_fp_removal.h"
117 #include "wmm/weak_memory.h"
118 
121 {
122  if(cmdline.isset("version"))
123  {
124  std::cout << CBMC_VERSION << '\n';
125  return CPROVER_EXIT_SUCCESS;
126  }
127 
128  if(cmdline.args.size()!=1 && cmdline.args.size()!=2)
129  {
130  help();
132  }
133 
136 
137  {
139 
141 
142  {
143  const bool validate_only = cmdline.isset("validate-goto-binary");
144 
145  if(validate_only || cmdline.isset("validate-goto-model"))
146  {
148 
149  if(validate_only)
150  {
151  return CPROVER_EXIT_SUCCESS;
152  }
153  }
154  }
155 
157 
158  if(cmdline.isset("validate-goto-model"))
159  {
161  }
162 
163  {
164  bool unwind_given=cmdline.isset("unwind");
165  bool unwindset_given=cmdline.isset("unwindset");
166  bool unwindset_file_given=cmdline.isset("unwindset-file");
167 
168  if(unwindset_given && unwindset_file_given)
169  throw "only one of --unwindset and --unwindset-file supported at a "
170  "time";
171 
172  if(unwind_given || unwindset_given || unwindset_file_given)
173  {
174  unwindsett unwindset;
175 
176  if(unwind_given)
177  unwindset.parse_unwind(cmdline.get_value("unwind"));
178 
179  if(unwindset_file_given)
180  unwindset.parse_unwindset_file(cmdline.get_value("unwindset-file"));
181 
182  if(unwindset_given)
183  unwindset.parse_unwindset(cmdline.get_values("unwindset"));
184 
185  bool unwinding_assertions=cmdline.isset("unwinding-assertions");
186  bool partial_loops=cmdline.isset("partial-loops");
187  bool continue_as_loops=cmdline.isset("continue-as-loops");
188 
189  if(unwinding_assertions+partial_loops+continue_as_loops>1)
190  throw "more than one of --unwinding-assertions,--partial-loops,"
191  "--continue-as-loops selected";
192 
193  goto_unwindt::unwind_strategyt unwind_strategy=
195 
196  if(unwinding_assertions)
197  {
199  }
200  else if(partial_loops)
201  {
203  }
204  else if(continue_as_loops)
205  {
207  }
208 
209  goto_unwindt goto_unwind;
210  goto_unwind(goto_model, unwindset, unwind_strategy);
211 
212  if(cmdline.isset("log"))
213  {
214  std::string filename=cmdline.get_value("log");
215  bool have_file=!filename.empty() && filename!="-";
216 
217  jsont result=goto_unwind.output_log_json();
218 
219  if(have_file)
220  {
221 #ifdef _MSC_VER
222  std::ofstream of(widen(filename));
223 #else
224  std::ofstream of(filename);
225 #endif
226  if(!of)
227  throw "failed to open file "+filename;
228 
229  of << result;
230  of.close();
231  }
232  else
233  {
234  std::cout << result << '\n';
235  }
236  }
237 
238  // goto_unwind holds references to instructions, only do remove_skip
239  // after having generated the log above
241  }
242  }
243 
244  if(cmdline.isset("show-threaded"))
245  {
247 
248  is_threadedt is_threaded(goto_model);
249 
250  for(const auto &gf_entry : goto_model.goto_functions.function_map)
251  {
252  std::cout << "////\n";
253  std::cout << "//// Function: " << gf_entry.first << '\n';
254  std::cout << "////\n\n";
255 
256  const goto_programt &goto_program = gf_entry.second.body;
257 
258  forall_goto_program_instructions(i_it, goto_program)
259  {
260  goto_program.output_instruction(ns, gf_entry.first, std::cout, *i_it);
261  std::cout << "Is threaded: " << (is_threaded(i_it)?"True":"False")
262  << "\n\n";
263  }
264  }
265 
266  return CPROVER_EXIT_SUCCESS;
267  }
268 
269  if(cmdline.isset("insert-final-assert-false"))
270  {
271  log.status() << "Inserting final assert false" << messaget::eom;
272  bool fail = insert_final_assert_false(
273  goto_model,
274  cmdline.get_value("insert-final-assert-false"),
276  if(fail)
277  {
279  }
280  // otherwise, fall-through to write new binary
281  }
282 
283  if(cmdline.isset("show-value-sets"))
284  {
286 
287  // recalculate numbers, etc.
289 
290  log.status() << "Pointer Analysis" << messaget::eom;
292  value_set_analysist value_set_analysis(ns);
293  value_set_analysis(goto_model.goto_functions);
295  ui_message_handler.get_ui(), goto_model, value_set_analysis);
296  return CPROVER_EXIT_SUCCESS;
297  }
298 
299  if(cmdline.isset("show-global-may-alias"))
300  {
304 
305  // recalculate numbers, etc.
307 
308  global_may_alias_analysist global_may_alias_analysis;
309  global_may_alias_analysis(goto_model);
310  global_may_alias_analysis.output(goto_model, std::cout);
311 
312  return CPROVER_EXIT_SUCCESS;
313  }
314 
315  if(cmdline.isset("show-local-bitvector-analysis"))
316  {
319 
320  // recalculate numbers, etc.
322 
324 
325  for(const auto &gf_entry : goto_model.goto_functions.function_map)
326  {
327  local_bitvector_analysist local_bitvector_analysis(gf_entry.second, ns);
328  std::cout << ">>>>\n";
329  std::cout << ">>>> " << gf_entry.first << '\n';
330  std::cout << ">>>>\n";
331  local_bitvector_analysis.output(std::cout, gf_entry.second, ns);
332  std::cout << '\n';
333  }
334 
335  return CPROVER_EXIT_SUCCESS;
336  }
337 
338  if(cmdline.isset("show-local-safe-pointers") ||
339  cmdline.isset("show-safe-dereferences"))
340  {
341  // Ensure location numbering is unique:
343 
345 
346  for(const auto &gf_entry : goto_model.goto_functions.function_map)
347  {
348  local_safe_pointerst local_safe_pointers;
349  local_safe_pointers(gf_entry.second.body);
350  std::cout << ">>>>\n";
351  std::cout << ">>>> " << gf_entry.first << '\n';
352  std::cout << ">>>>\n";
353  if(cmdline.isset("show-local-safe-pointers"))
354  local_safe_pointers.output(std::cout, gf_entry.second.body, ns);
355  else
356  {
357  local_safe_pointers.output_safe_dereferences(
358  std::cout, gf_entry.second.body, ns);
359  }
360  std::cout << '\n';
361  }
362 
363  return CPROVER_EXIT_SUCCESS;
364  }
365 
366  if(cmdline.isset("show-sese-regions"))
367  {
368  // Ensure location numbering is unique:
370 
372 
373  for(const auto &gf_entry : goto_model.goto_functions.function_map)
374  {
375  sese_region_analysist sese_region_analysis;
376  sese_region_analysis(gf_entry.second.body);
377  std::cout << ">>>>\n";
378  std::cout << ">>>> " << gf_entry.first << '\n';
379  std::cout << ">>>>\n";
380  sese_region_analysis.output(std::cout, gf_entry.second.body, ns);
381  std::cout << '\n';
382  }
383 
384  return CPROVER_EXIT_SUCCESS;
385  }
386 
387  if(cmdline.isset("show-custom-bitvector-analysis"))
388  {
392 
394 
395  if(!cmdline.isset("inline"))
396  {
399  }
400 
401  // recalculate numbers, etc.
403 
404  custom_bitvector_analysist custom_bitvector_analysis;
405  custom_bitvector_analysis(goto_model);
406  custom_bitvector_analysis.output(goto_model, std::cout);
407 
408  return CPROVER_EXIT_SUCCESS;
409  }
410 
411  if(cmdline.isset("show-escape-analysis"))
412  {
416 
417  // recalculate numbers, etc.
419 
420  escape_analysist escape_analysis;
421  escape_analysis(goto_model);
422  escape_analysis.output(goto_model, std::cout);
423 
424  return CPROVER_EXIT_SUCCESS;
425  }
426 
427  if(cmdline.isset("custom-bitvector-analysis"))
428  {
432 
434 
435  if(!cmdline.isset("inline"))
436  {
439  }
440 
441  // recalculate numbers, etc.
443 
445 
446  custom_bitvector_analysist custom_bitvector_analysis;
447  custom_bitvector_analysis(goto_model);
448  custom_bitvector_analysis.check(
449  goto_model,
450  cmdline.isset("xml-ui"),
451  std::cout);
452 
453  return CPROVER_EXIT_SUCCESS;
454  }
455 
456  if(cmdline.isset("show-points-to"))
457  {
459 
460  // recalculate numbers, etc.
462 
464 
465  log.status() << "Pointer Analysis" << messaget::eom;
466  points_tot points_to;
467  points_to(goto_model);
468  points_to.output(std::cout);
469  return CPROVER_EXIT_SUCCESS;
470  }
471 
472  if(cmdline.isset("show-intervals"))
473  {
475 
476  // recalculate numbers, etc.
478 
479  log.status() << "Interval Analysis" << messaget::eom;
483  interval_analysis.output(goto_model, std::cout);
484  return CPROVER_EXIT_SUCCESS;
485  }
486 
487  if(cmdline.isset("show-call-sequences"))
488  {
491  return CPROVER_EXIT_SUCCESS;
492  }
493 
494  if(cmdline.isset("check-call-sequence"))
495  {
498  return CPROVER_EXIT_SUCCESS;
499  }
500 
501  if(cmdline.isset("list-calls-args"))
502  {
504 
506 
507  return CPROVER_EXIT_SUCCESS;
508  }
509 
510  if(cmdline.isset("show-rw-set"))
511  {
513 
514  if(!cmdline.isset("inline"))
515  {
517 
518  // recalculate numbers, etc.
520  }
521 
522  log.status() << "Pointer Analysis" << messaget::eom;
523  value_set_analysist value_set_analysis(ns);
524  value_set_analysis(goto_model.goto_functions);
525 
526  const symbolt &symbol=ns.lookup(ID_main);
527  symbol_exprt main(symbol.name, symbol.type);
528 
529  std::cout <<
530  rw_set_functiont(value_set_analysis, goto_model, main);
531  return CPROVER_EXIT_SUCCESS;
532  }
533 
534  if(cmdline.isset("show-symbol-table"))
535  {
537  return CPROVER_EXIT_SUCCESS;
538  }
539 
540  if(cmdline.isset("show-reaching-definitions"))
541  {
543 
545  reaching_definitions_analysist rd_analysis(ns);
546  rd_analysis(goto_model);
547  rd_analysis.output(goto_model, std::cout);
548 
549  return CPROVER_EXIT_SUCCESS;
550  }
551 
552  if(cmdline.isset("show-dependence-graph"))
553  {
555 
557  dependence_grapht dependence_graph(ns);
558  dependence_graph(goto_model);
559  dependence_graph.output(goto_model, std::cout);
560  dependence_graph.output_dot(std::cout);
561 
562  return CPROVER_EXIT_SUCCESS;
563  }
564 
565  if(cmdline.isset("count-eloc"))
566  {
568  return CPROVER_EXIT_SUCCESS;
569  }
570 
571  if(cmdline.isset("list-eloc"))
572  {
574  return CPROVER_EXIT_SUCCESS;
575  }
576 
577  if(cmdline.isset("print-path-lengths"))
578  {
580  return CPROVER_EXIT_SUCCESS;
581  }
582 
583  if(cmdline.isset("print-global-state-size"))
584  {
586  return CPROVER_EXIT_SUCCESS;
587  }
588 
589  if(cmdline.isset("list-symbols"))
590  {
592  return CPROVER_EXIT_SUCCESS;
593  }
594 
595  if(cmdline.isset("show-uninitialized"))
596  {
597  show_uninitialized(goto_model, std::cout);
598  return CPROVER_EXIT_SUCCESS;
599  }
600 
601  if(cmdline.isset("interpreter"))
602  {
605 
606  log.status() << "Starting interpreter" << messaget::eom;
608  return CPROVER_EXIT_SUCCESS;
609  }
610 
611  if(cmdline.isset("show-claims") ||
612  cmdline.isset("show-properties"))
613  {
616  return CPROVER_EXIT_SUCCESS;
617  }
618 
619  if(cmdline.isset("document-claims-html") ||
620  cmdline.isset("document-properties-html"))
621  {
623  return CPROVER_EXIT_SUCCESS;
624  }
625 
626  if(cmdline.isset("document-claims-latex") ||
627  cmdline.isset("document-properties-latex"))
628  {
630  return CPROVER_EXIT_SUCCESS;
631  }
632 
633  if(cmdline.isset("show-loops"))
634  {
636  return CPROVER_EXIT_SUCCESS;
637  }
638 
639  if(cmdline.isset("show-natural-loops"))
640  {
641  show_natural_loops(goto_model, std::cout);
642  return CPROVER_EXIT_SUCCESS;
643  }
644 
645  if(cmdline.isset("show-lexical-loops"))
646  {
647  show_lexical_loops(goto_model, std::cout);
648  }
649 
650  if(cmdline.isset("print-internal-representation"))
651  {
652  for(auto const &pair : goto_model.goto_functions.function_map)
653  for(auto const &ins : pair.second.body.instructions)
654  {
655  if(ins.get_code().is_not_nil())
656  log.status() << ins.get_code().pretty() << messaget::eom;
657  if(ins.has_condition())
658  {
659  log.status() << "[guard] " << ins.get_condition().pretty()
660  << messaget::eom;
661  }
662  }
663  return CPROVER_EXIT_SUCCESS;
664  }
665 
666  if(
667  cmdline.isset("show-goto-functions") ||
668  cmdline.isset("list-goto-functions"))
669  {
671  goto_model, ui_message_handler, cmdline.isset("list-goto-functions"));
672  return CPROVER_EXIT_SUCCESS;
673  }
674 
675  if(cmdline.isset("list-undefined-functions"))
676  {
678  return CPROVER_EXIT_SUCCESS;
679  }
680 
681  // experimental: print structs
682  if(cmdline.isset("show-struct-alignment"))
683  {
685  return CPROVER_EXIT_SUCCESS;
686  }
687 
688  if(cmdline.isset("show-locations"))
689  {
691  return CPROVER_EXIT_SUCCESS;
692  }
693 
694  if(
695  cmdline.isset("dump-c") || cmdline.isset("dump-cpp") ||
696  cmdline.isset("dump-c-type-header"))
697  {
698  const bool is_cpp=cmdline.isset("dump-cpp");
699  const bool is_header = cmdline.isset("dump-c-type-header");
700  const bool h_libc=!cmdline.isset("no-system-headers");
701  const bool h_all=cmdline.isset("use-all-headers");
702  const bool harness=cmdline.isset("harness");
704 
705  // restore RETURN instructions in case remove_returns had been
706  // applied
708 
709  // dump_c (actually goto_program2code) requires valid instruction
710  // location numbers:
712 
713  if(cmdline.args.size()==2)
714  {
715  #ifdef _MSC_VER
716  std::ofstream out(widen(cmdline.args[1]));
717  #else
718  std::ofstream out(cmdline.args[1]);
719  #endif
720  if(!out)
721  {
722  log.error() << "failed to write to '" << cmdline.args[1] << "'";
724  }
725  if(is_header)
726  {
729  h_libc,
730  h_all,
731  harness,
732  ns,
733  cmdline.get_value("dump-c-type-header"),
734  out);
735  }
736  else
737  {
738  (is_cpp ? dump_cpp : dump_c)(
739  goto_model.goto_functions, h_libc, h_all, harness, ns, out);
740  }
741  }
742  else
743  {
744  if(is_header)
745  {
748  h_libc,
749  h_all,
750  harness,
751  ns,
752  cmdline.get_value("dump-c-type-header"),
753  std::cout);
754  }
755  else
756  {
757  (is_cpp ? dump_cpp : dump_c)(
758  goto_model.goto_functions, h_libc, h_all, harness, ns, std::cout);
759  }
760  }
761 
762  return CPROVER_EXIT_SUCCESS;
763  }
764 
765  if(cmdline.isset("call-graph"))
766  {
768  call_grapht call_graph(goto_model);
769 
770  if(cmdline.isset("xml"))
771  call_graph.output_xml(std::cout);
772  else if(cmdline.isset("dot"))
773  call_graph.output_dot(std::cout);
774  else
775  call_graph.output(std::cout);
776 
777  return CPROVER_EXIT_SUCCESS;
778  }
779 
780  if(cmdline.isset("reachable-call-graph"))
781  {
783  call_grapht call_graph =
786  if(cmdline.isset("xml"))
787  call_graph.output_xml(std::cout);
788  else if(cmdline.isset("dot"))
789  call_graph.output_dot(std::cout);
790  else
791  call_graph.output(std::cout);
792 
793  return 0;
794  }
795 
796  if(cmdline.isset("show-class-hierarchy"))
797  {
798  class_hierarchyt hierarchy;
799  hierarchy(goto_model.symbol_table);
800  if(cmdline.isset("dot"))
801  hierarchy.output_dot(std::cout);
802  else
804 
805  return CPROVER_EXIT_SUCCESS;
806  }
807 
808  if(cmdline.isset("dot"))
809  {
811 
812  if(cmdline.args.size()==2)
813  {
814  #ifdef _MSC_VER
815  std::ofstream out(widen(cmdline.args[1]));
816  #else
817  std::ofstream out(cmdline.args[1]);
818  #endif
819  if(!out)
820  {
821  log.error() << "failed to write to " << cmdline.args[1] << "'";
823  }
824 
825  dot(goto_model, out);
826  }
827  else
828  dot(goto_model, std::cout);
829 
830  return CPROVER_EXIT_SUCCESS;
831  }
832 
833  if(cmdline.isset("accelerate"))
834  {
836 
838 
839  log.status() << "Performing full inlining" << messaget::eom;
841 
842  log.status() << "Removing calls to functions without a body"
843  << messaget::eom;
844  remove_calls_no_bodyt remove_calls_no_body;
845  remove_calls_no_body(goto_model.goto_functions);
846 
847  log.status() << "Accelerating" << messaget::eom;
848  guard_managert guard_manager;
850  goto_model, ui_message_handler, cmdline.isset("z3"), guard_manager);
852  }
853 
854  if(cmdline.isset("horn-encoding"))
855  {
856  log.status() << "Horn-clause encoding" << messaget::eom;
858 
859  if(cmdline.args.size()==2)
860  {
861  #ifdef _MSC_VER
862  std::ofstream out(widen(cmdline.args[1]));
863  #else
864  std::ofstream out(cmdline.args[1]);
865  #endif
866 
867  if(!out)
868  {
869  log.error() << "Failed to open output file " << cmdline.args[1]
870  << messaget::eom;
872  }
873 
875  }
876  else
877  horn_encoding(goto_model, std::cout);
878 
879  return CPROVER_EXIT_SUCCESS;
880  }
881 
882  if(cmdline.isset("drop-unused-functions"))
883  {
885 
886  log.status() << "Removing unused functions" << messaget::eom;
888  }
889 
890  if(cmdline.isset("undefined-function-is-assume-false"))
891  {
894  }
895 
896  // write new binary?
897  if(cmdline.args.size()==2)
898  {
899  log.status() << "Writing GOTO program to '" << cmdline.args[1] << "'"
900  << messaget::eom;
901 
904  else
905  return CPROVER_EXIT_SUCCESS;
906  }
907  else if(cmdline.args.size() < 2)
908  {
910  "Invalid number of positional arguments passed",
911  "[in] [out]",
912  "goto-instrument needs one input and one output file, aside from other "
913  "flags");
914  }
915 
916  help();
918  }
919 // NOLINTNEXTLINE(readability/fn_size)
920 }
921 
923  bool force)
924 {
925  if(function_pointer_removal_done && !force)
926  return;
927 
929 
930  log.status() << "Function Pointer Removal" << messaget::eom;
932  ui_message_handler, goto_model, cmdline.isset("pointer-check"));
933  log.status() << "Virtual function removal" << messaget::eom;
935  log.status() << "Cleaning inline assembler statements" << messaget::eom;
937 }
938 
943 {
944  // Don't bother if we've already done a full function pointer
945  // removal.
947  {
948  return;
949  }
950 
951  log.status() << "Removing const function pointers only" << messaget::eom;
954  goto_model,
955  cmdline.isset("pointer-check"),
956  true); // abort if we can't resolve via const pointers
957 }
958 
960 {
962  return;
963 
965 
966  if(!cmdline.isset("inline"))
967  {
968  log.status() << "Partial Inlining" << messaget::eom;
970  }
971 }
972 
974 {
976  return;
977 
978  remove_returns_done=true;
979 
980  log.status() << "Removing returns" << messaget::eom;
982 }
983 
985 {
986  log.status() << "Reading GOTO program from '" << cmdline.args[0] << "'"
987  << messaget::eom;
988 
989  config.set(cmdline);
990 
991  auto result = read_goto_binary(cmdline.args[0], ui_message_handler);
992 
993  if(!result.has_value())
994  throw 0;
995 
996  goto_model = std::move(result.value());
997 
999 }
1000 
1002 {
1003  optionst options;
1004 
1006 
1007  // disable simplify when adding various checks?
1008  if(cmdline.isset("no-simplify"))
1009  options.set_option("simplify", false);
1010  else
1011  options.set_option("simplify", true);
1012 
1013  // all checks supported by goto_check
1015 
1016  // unwind loops
1017  if(cmdline.isset("unwind"))
1018  {
1019  log.status() << "Unwinding loops" << messaget::eom;
1020  options.set_option("unwind", cmdline.get_value("unwind"));
1021  }
1022 
1023  {
1025 
1026  if(
1030  {
1032 
1033  const auto function_pointer_restrictions =
1035  options, goto_model, log.get_message_handler());
1036 
1037  restrict_function_pointers(goto_model, function_pointer_restrictions);
1038  }
1039  }
1040 
1041  // skip over selected loops
1042  if(cmdline.isset("skip-loops"))
1043  {
1044  log.status() << "Adding gotos to skip loops" << messaget::eom;
1045  if(skip_loops(
1047  throw 0;
1048  }
1049 
1051 
1052  // initialize argv with valid pointers
1053  if(cmdline.isset("model-argc-argv"))
1054  {
1055  unsigned max_argc=
1056  safe_string2unsigned(cmdline.get_value("model-argc-argv"));
1057 
1058  log.status() << "Adding up to " << max_argc << " command line arguments"
1059  << messaget::eom;
1061  throw 0;
1062  }
1063 
1064  if(cmdline.isset("remove-function-body"))
1065  {
1067  goto_model,
1068  cmdline.get_values("remove-function-body"),
1070  }
1071 
1072  // we add the library in some cases, as some analyses benefit
1073 
1074  if(cmdline.isset("add-library") ||
1075  cmdline.isset("mm"))
1076  {
1077  if(cmdline.isset("show-custom-bitvector-analysis") ||
1078  cmdline.isset("custom-bitvector-analysis"))
1079  {
1080  config.ansi_c.defines.push_back(
1081  std::string(CPROVER_PREFIX) + "CUSTOM_BITVECTOR_ANALYSIS");
1082  }
1083 
1084  // add the library
1085  log.status() << "Adding CPROVER library (" << config.ansi_c.arch << ")"
1086  << messaget::eom;
1090  }
1091 
1092  // now do full inlining, if requested
1093  if(cmdline.isset("inline"))
1094  {
1096 
1097  if(cmdline.isset("show-custom-bitvector-analysis") ||
1098  cmdline.isset("custom-bitvector-analysis"))
1099  {
1103  }
1104 
1105  log.status() << "Performing full inlining" << messaget::eom;
1107  }
1108 
1109  if(cmdline.isset("show-custom-bitvector-analysis") ||
1110  cmdline.isset("custom-bitvector-analysis"))
1111  {
1112  log.status() << "Propagating Constants" << messaget::eom;
1113  constant_propagator_ait constant_propagator_ai(goto_model);
1115  }
1116 
1117  if(cmdline.isset("escape-analysis"))
1118  {
1122 
1123  // recalculate numbers, etc.
1125 
1126  log.status() << "Escape Analysis" << messaget::eom;
1127  escape_analysist escape_analysis;
1128  escape_analysis(goto_model);
1129  escape_analysis.instrument(goto_model);
1130 
1131  // inline added functions, they are often small
1133 
1134  // recalculate numbers, etc.
1136  }
1137 
1138  const std::list<std::pair<std::string, std::string>> contract_flags(
1141  for(const auto &pair : contract_flags)
1142  {
1143  if(cmdline.isset(pair.first.c_str()) && cmdline.isset(pair.second.c_str()))
1144  {
1145  log.error() << "Pass at most one of --" << pair.first << " and --"
1146  << pair.second << "." << messaget::eom;
1148  }
1149  }
1150 
1151  if(
1156  {
1158 
1160  {
1161  std::set<std::string> to_replace(
1164  if(cont.replace_calls(to_replace))
1166  }
1167 
1169  if(cont.replace_calls())
1171 
1173  {
1174  std::set<std::string> to_enforce(
1177  if(cont.enforce_contracts(to_enforce))
1179  }
1180 
1182  if(cont.enforce_contracts())
1184 
1186  cont.apply_loop_contracts();
1187  }
1188 
1189  if(cmdline.isset("value-set-fi-fp-removal"))
1190  {
1193  }
1194 
1195  // replace function pointers, if explicitly requested
1196  if(cmdline.isset("remove-function-pointers"))
1197  {
1199  }
1200  else if(cmdline.isset("remove-const-function-pointers"))
1201  {
1203  }
1204 
1205  if(cmdline.isset("replace-calls"))
1206  {
1208 
1209  replace_callst replace_calls;
1210  replace_calls(goto_model, cmdline.get_values("replace-calls"));
1211  }
1212 
1213  if(cmdline.isset("function-inline"))
1214  {
1215  std::string function=cmdline.get_value("function-inline");
1216  PRECONDITION(!function.empty());
1217 
1218  bool caching=!cmdline.isset("no-caching");
1219 
1221 
1222  log.status() << "Inlining calls of function '" << function << "'"
1223  << messaget::eom;
1224 
1225  if(!cmdline.isset("log"))
1226  {
1228  goto_model, function, ui_message_handler, true, caching);
1229  }
1230  else
1231  {
1232  std::string filename=cmdline.get_value("log");
1233  bool have_file=!filename.empty() && filename!="-";
1234 
1236  goto_model, function, ui_message_handler, true, caching);
1237 
1238  if(have_file)
1239  {
1240 #ifdef _MSC_VER
1241  std::ofstream of(widen(filename));
1242 #else
1243  std::ofstream of(filename);
1244 #endif
1245  if(!of)
1246  throw "failed to open file "+filename;
1247 
1248  of << result;
1249  of.close();
1250  }
1251  else
1252  {
1253  std::cout << result << '\n';
1254  }
1255  }
1256 
1259  }
1260 
1261  if(cmdline.isset("partial-inline"))
1262  {
1264 
1265  log.status() << "Partial inlining" << messaget::eom;
1267 
1270  }
1271 
1272  if(cmdline.isset("remove-calls-no-body"))
1273  {
1274  log.status() << "Removing calls to functions without a body"
1275  << messaget::eom;
1276 
1277  remove_calls_no_bodyt remove_calls_no_body;
1278  remove_calls_no_body(goto_model.goto_functions);
1279 
1282  }
1283 
1284  if(cmdline.isset("constant-propagator"))
1285  {
1287 
1288  log.status() << "Propagating Constants" << messaget::eom;
1289 
1290  constant_propagator_ait constant_propagator_ai(goto_model);
1292  }
1293 
1294  if(cmdline.isset("generate-function-body"))
1295  {
1296  optionst c_object_factory_options;
1297  parse_c_object_factory_options(cmdline, c_object_factory_options);
1298  c_object_factory_parameterst object_factory_parameters(
1299  c_object_factory_options);
1300 
1301  auto generate_implementation = generate_function_bodies_factory(
1302  cmdline.get_value("generate-function-body-options"),
1303  object_factory_parameters,
1307  std::regex(cmdline.get_value("generate-function-body")),
1308  *generate_implementation,
1309  goto_model,
1311  }
1312 
1313  if(cmdline.isset("generate-havocing-body"))
1314  {
1315  optionst c_object_factory_options;
1316  parse_c_object_factory_options(cmdline, c_object_factory_options);
1317  c_object_factory_parameterst object_factory_parameters(
1318  c_object_factory_options);
1319 
1320  auto options_split =
1321  split_string(cmdline.get_value("generate-havocing-body"), ',');
1322  if(options_split.size() < 2)
1324  "not enough arguments for this option", "--generate-havocing-body"};
1325 
1326  if(options_split.size() == 2)
1327  {
1328  auto generate_implementation = generate_function_bodies_factory(
1329  std::string{"havoc,"} + options_split.back(),
1330  object_factory_parameters,
1334  std::regex(options_split[0]),
1335  *generate_implementation,
1336  goto_model,
1338  }
1339  else
1340  {
1341  CHECK_RETURN(options_split.size() % 2 == 1);
1342  for(size_t i = 1; i + 1 < options_split.size(); i += 2)
1343  {
1344  auto generate_implementation = generate_function_bodies_factory(
1345  std::string{"havoc,"} + options_split[i + 1],
1346  object_factory_parameters,
1350  options_split[0],
1351  options_split[i],
1352  *generate_implementation,
1353  goto_model,
1355  }
1356  }
1357  }
1358 
1359  // add generic checks, if needed
1360  goto_check(options, goto_model);
1361 
1362  // check for uninitalized local variables
1363  if(cmdline.isset("uninitialized-check"))
1364  {
1365  log.status() << "Adding checks for uninitialized local variables"
1366  << messaget::eom;
1368  }
1369 
1370  // check for maximum call stack size
1371  if(cmdline.isset("stack-depth"))
1372  {
1373  log.status() << "Adding check for maximum call stack size" << messaget::eom;
1374  stack_depth(
1375  goto_model,
1376  safe_string2size_t(cmdline.get_value("stack-depth")));
1377  }
1378 
1379  // ignore default/user-specified initialization of variables with static
1380  // lifetime
1381  if(cmdline.isset("nondet-static-exclude"))
1382  {
1383  log.status() << "Adding nondeterministic initialization "
1384  "of static/global variables except for "
1385  "the specified ones."
1386  << messaget::eom;
1387 
1388  nondet_static(goto_model, cmdline.get_values("nondet-static-exclude"));
1389  }
1390  else if(cmdline.isset("nondet-static"))
1391  {
1392  log.status() << "Adding nondeterministic initialization "
1393  "of static/global variables"
1394  << messaget::eom;
1396  }
1397 
1398  if(cmdline.isset("slice-global-inits"))
1399  {
1400  log.status() << "Slicing away initializations of unused global variables"
1401  << messaget::eom;
1403  }
1404 
1405  if(cmdline.isset("string-abstraction"))
1406  {
1409 
1410  log.status() << "String Abstraction" << messaget::eom;
1412  }
1413 
1414  // some analyses require function pointer removal and partial inlining
1415 
1416  if(cmdline.isset("remove-pointers") ||
1417  cmdline.isset("race-check") ||
1418  cmdline.isset("mm") ||
1419  cmdline.isset("isr") ||
1420  cmdline.isset("concurrency"))
1421  {
1423 
1424  log.status() << "Pointer Analysis" << messaget::eom;
1425  value_set_analysist value_set_analysis(ns);
1426  value_set_analysis(goto_model.goto_functions);
1427 
1428  if(cmdline.isset("remove-pointers"))
1429  {
1430  // removing pointers
1431  log.status() << "Removing Pointers" << messaget::eom;
1432  remove_pointers(goto_model, value_set_analysis);
1433  }
1434 
1435  if(cmdline.isset("race-check"))
1436  {
1437  log.status() << "Adding Race Checks" << messaget::eom;
1438  race_check(value_set_analysis, goto_model);
1439  }
1440 
1441  if(cmdline.isset("mm"))
1442  {
1443  std::string mm=cmdline.get_value("mm");
1444  memory_modelt model;
1445 
1446  // strategy of instrumentation
1447  instrumentation_strategyt inst_strategy;
1448  if(cmdline.isset("one-event-per-cycle"))
1449  inst_strategy=one_event_per_cycle;
1450  else if(cmdline.isset("minimum-interference"))
1451  inst_strategy=min_interference;
1452  else if(cmdline.isset("read-first"))
1453  inst_strategy=read_first;
1454  else if(cmdline.isset("write-first"))
1455  inst_strategy=write_first;
1456  else if(cmdline.isset("my-events"))
1457  inst_strategy=my_events;
1458  else
1459  /* default: instruments all unsafe pairs */
1460  inst_strategy=all;
1461 
1462  const unsigned max_var=
1463  cmdline.isset("max-var")?
1465  const unsigned max_po_trans=
1466  cmdline.isset("max-po-trans")?
1467  unsafe_string2unsigned(cmdline.get_value("max-po-trans")):0;
1468 
1469  if(mm=="tso")
1470  {
1471  log.status() << "Adding weak memory (TSO) Instrumentation"
1472  << messaget::eom;
1473  model=TSO;
1474  }
1475  else if(mm=="pso")
1476  {
1477  log.status() << "Adding weak memory (PSO) Instrumentation"
1478  << messaget::eom;
1479  model=PSO;
1480  }
1481  else if(mm=="rmo")
1482  {
1483  log.status() << "Adding weak memory (RMO) Instrumentation"
1484  << messaget::eom;
1485  model=RMO;
1486  }
1487  else if(mm=="power")
1488  {
1489  log.status() << "Adding weak memory (Power) Instrumentation"
1490  << messaget::eom;
1491  model=Power;
1492  }
1493  else
1494  {
1495  log.error() << "Unknown weak memory model '" << mm << "'"
1496  << messaget::eom;
1497  model=Unknown;
1498  }
1499 
1501 
1502  if(cmdline.isset("force-loop-duplication"))
1503  loops=all_loops;
1504  if(cmdline.isset("no-loop-duplication"))
1505  loops=no_loop;
1506 
1507  if(model!=Unknown)
1508  weak_memory(
1509  model,
1510  value_set_analysis,
1511  goto_model,
1512  cmdline.isset("scc"),
1513  inst_strategy,
1514  !cmdline.isset("cfg-kill"),
1515  cmdline.isset("no-dependencies"),
1516  loops,
1517  max_var,
1518  max_po_trans,
1519  !cmdline.isset("no-po-rendering"),
1520  cmdline.isset("render-cluster-file"),
1521  cmdline.isset("render-cluster-function"),
1522  cmdline.isset("cav11"),
1523  cmdline.isset("hide-internals"),
1525  cmdline.isset("ignore-arrays"));
1526  }
1527 
1528  // Interrupt handler
1529  if(cmdline.isset("isr"))
1530  {
1531  log.status() << "Instrumenting interrupt handler" << messaget::eom;
1532  interrupt(
1533  value_set_analysis,
1534  goto_model,
1535  cmdline.get_value("isr"));
1536  }
1537 
1538  // Memory-mapped I/O
1539  if(cmdline.isset("mmio"))
1540  {
1541  log.status() << "Instrumenting memory-mapped I/O" << messaget::eom;
1542  mmio(value_set_analysis, goto_model);
1543  }
1544 
1545  if(cmdline.isset("concurrency"))
1546  {
1547  log.status() << "Sequentializing concurrency" << messaget::eom;
1548  concurrency(value_set_analysis, goto_model);
1549  }
1550  }
1551 
1552  if(cmdline.isset("interval-analysis"))
1553  {
1554  log.status() << "Interval analysis" << messaget::eom;
1556  }
1557 
1558  if(cmdline.isset("havoc-loops"))
1559  {
1560  log.status() << "Havocking loops" << messaget::eom;
1562  }
1563 
1564  if(cmdline.isset("k-induction"))
1565  {
1566  bool base_case=cmdline.isset("base-case");
1567  bool step_case=cmdline.isset("step-case");
1568 
1569  if(step_case && base_case)
1570  throw "please specify only one of --step-case and --base-case";
1571  else if(!step_case && !base_case)
1572  throw "please specify one of --step-case and --base-case";
1573 
1574  unsigned k=unsafe_string2unsigned(cmdline.get_value("k-induction"));
1575 
1576  if(k==0)
1577  throw "please give k>=1";
1578 
1579  log.status() << "Instrumenting k-induction for k=" << k << ", "
1580  << (base_case ? "base case" : "step case") << messaget::eom;
1581 
1582  k_induction(goto_model, base_case, step_case, k);
1583  }
1584 
1585  if(cmdline.isset("function-enter"))
1586  {
1587  log.status() << "Function enter instrumentation" << messaget::eom;
1589  goto_model,
1590  cmdline.get_value("function-enter"));
1591  }
1592 
1593  if(cmdline.isset("function-exit"))
1594  {
1595  log.status() << "Function exit instrumentation" << messaget::eom;
1596  function_exit(
1597  goto_model,
1598  cmdline.get_value("function-exit"));
1599  }
1600 
1601  if(cmdline.isset("branch"))
1602  {
1603  log.status() << "Branch instrumentation" << messaget::eom;
1604  branch(
1605  goto_model,
1606  cmdline.get_value("branch"));
1607  }
1608 
1609  // add failed symbols
1611 
1612  // recalculate numbers, etc.
1614 
1615  // add loop ids
1617 
1618  // label the assertions
1620 
1621  nondet_volatile(goto_model, options);
1622 
1623  // reachability slice?
1624  if(cmdline.isset("reachability-slice"))
1625  {
1627 
1628  log.status() << "Performing a reachability slice" << messaget::eom;
1629 
1630  // reachability_slicer requires that the model has unique location numbers:
1632 
1633  if(cmdline.isset("property"))
1635  else
1637  }
1638 
1639  if(cmdline.isset("fp-reachability-slice"))
1640  {
1642 
1643  log.status() << "Performing a function pointer reachability slice"
1644  << messaget::eom;
1646  goto_model, cmdline.get_comma_separated_values("fp-reachability-slice"));
1647  }
1648 
1649  // full slice?
1650  if(cmdline.isset("full-slice"))
1651  {
1654 
1655  log.status() << "Performing a full slice" << messaget::eom;
1656  if(cmdline.isset("property"))
1658  else
1659  {
1660  // full_slicer requires that the model has unique location numbers:
1663  }
1664  }
1665 
1666  // splice option
1667  if(cmdline.isset("splice-call"))
1668  {
1669  log.status() << "Performing call splicing" << messaget::eom;
1670  std::string callercallee=cmdline.get_value("splice-call");
1671  if(splice_call(
1673  callercallee,
1676  throw 0;
1677  }
1678 
1679  // aggressive slicer
1680  if(cmdline.isset("aggressive-slice"))
1681  {
1683 
1684  // reachability_slicer requires that the model has unique location numbers:
1686 
1687  log.status() << "Slicing away initializations of unused global variables"
1688  << messaget::eom;
1690 
1691  log.status() << "Performing an aggressive slice" << messaget::eom;
1692  aggressive_slicert aggressive_slicer(goto_model, ui_message_handler);
1693 
1694  if(cmdline.isset("aggressive-slice-call-depth"))
1695  aggressive_slicer.call_depth =
1696  safe_string2unsigned(cmdline.get_value("aggressive-slice-call-depth"));
1697 
1698  if(cmdline.isset("aggressive-slice-preserve-function"))
1699  aggressive_slicer.preserve_functions(
1700  cmdline.get_values("aggressive-slice-preserve-function"));
1701 
1702  if(cmdline.isset("property"))
1703  aggressive_slicer.user_specified_properties =
1704  cmdline.get_values("property");
1705 
1706  if(cmdline.isset("aggressive-slice-preserve-functions-containing"))
1707  aggressive_slicer.name_snippets =
1708  cmdline.get_values("aggressive-slice-preserve-functions-containing");
1709 
1710  aggressive_slicer.preserve_all_direct_paths =
1711  cmdline.isset("aggressive-slice-preserve-all-direct-paths");
1712 
1713  aggressive_slicer.doit();
1714 
1716 
1717  log.status() << "Performing a reachability slice" << messaget::eom;
1718  if(cmdline.isset("property"))
1720  else
1722  }
1723 
1724  if(cmdline.isset("ensure-one-backedge-per-target"))
1725  {
1726  log.status() << "Trying to force one backedge per target" << messaget::eom;
1728  }
1729 
1730  // recalculate numbers, etc.
1732 }
1733 
1736 {
1737  // clang-format off
1738  std::cout << '\n' << banner_string("Goto-Instrument", CBMC_VERSION) << '\n'
1739  << align_center_with_border("Copyright (C) 2008-2013") << '\n'
1740  << align_center_with_border("Daniel Kroening") << '\n'
1741  << align_center_with_border("kroening@kroening.com") << '\n'
1742  <<
1743  "\n"
1744  "Usage: Purpose:\n"
1745  "\n"
1746  " goto-instrument [-?] [-h] [--help] show help\n"
1747  " goto-instrument in out perform instrumentation\n"
1748  "\n"
1749  "Main options:\n"
1750  " --document-properties-html generate HTML property documentation\n"
1751  " --document-properties-latex generate Latex property documentation\n"
1752  " --dump-c generate C source\n"
1753  " --dump-c-type-header m generate a C header for types local in m\n"
1754  " --dump-cpp generate C++ source\n"
1755  " --dot generate CFG graph in DOT format\n"
1756  " --interpreter do concrete execution\n"
1757  "\n"
1758  "Diagnosis:\n"
1759  " --show-loops show the loops in the program\n"
1761  " --show-symbol-table show loaded symbol table\n"
1762  " --list-symbols list symbols with type information\n"
1765  " --drop-unused-functions drop functions trivially unreachable from main function\n" // NOLINT(*)
1766  " --print-internal-representation\n" // NOLINTNEXTLINE(*)
1767  " show verbose internal representation of the program\n"
1768  " --list-undefined-functions list functions without body\n"
1769  " --show-struct-alignment show struct members that might be concurrently accessed\n" // NOLINT(*)
1770  " --show-natural-loops show natural loop heads\n"
1771  // NOLINTNEXTLINE(whitespace/line_length)
1772  " --list-calls-args list all function calls with their arguments\n"
1773  " --call-graph show graph of function calls\n"
1774  // NOLINTNEXTLINE(whitespace/line_length)
1775  " --reachable-call-graph show graph of function calls potentially reachable from main function\n"
1777  // NOLINTNEXTLINE(whitespace/line_length)
1778  " --show-threaded show instructions that may be executed by more than one thread\n"
1779  " --show-local-safe-pointers show pointer expressions that are trivially dominated by a not-null check\n" // NOLINT(*)
1780  " --show-safe-dereferences show pointer expressions that are trivially dominated by a not-null check\n" // NOLINT(*)
1781  " *and* used as a dereference operand\n" // NOLINT(*)
1783  // NOLINTNEXTLINE(whitespace/line_length)
1784  " --validate-goto-binary check the well-formedness of the passed in goto\n"
1785  " binary and then exit\n"
1786  "\n"
1787  "Safety checks:\n"
1788  " --no-assertions ignore user assertions\n"
1790  " --uninitialized-check add checks for uninitialized locals (experimental)\n" // NOLINT(*)
1791  " --stack-depth n add check that call stack size of non-inlined functions never exceeds n\n" // NOLINT(*)
1792  " --race-check add floating-point data race checks\n"
1793  "\n"
1794  "Semantic transformations:\n"
1795  << HELP_NONDET_VOLATILE <<
1796  " --unwind <n> unwinds the loops <n> times\n"
1797  " --unwindset L:B,... unwind loop L with a bound of B\n"
1798  " --unwindset-file <file> read unwindset from file\n"
1799  " --partial-loops permit paths with partial loops\n"
1800  " --unwinding-assertions generate unwinding assertions\n"
1801  " --continue-as-loops add loop for remaining iterations after unwound part\n" // NOLINT(*)
1802  " --isr <function> instruments an interrupt service routine\n"
1803  " --mmio instruments memory-mapped I/O\n"
1804  " --nondet-static add nondeterministic initialization of variables with static lifetime\n" // NOLINT(*)
1805  " --nondet-static-exclude e same as nondet-static except for the variable e\n" //NOLINT(*)
1806  " (use multiple times if required)\n"
1807  " --check-invariant function instruments invariant checking function\n"
1808  " --remove-pointers converts pointer arithmetic to base+offset expressions\n" // NOLINT(*)
1809  " --splice-call caller,callee prepends a call to callee in the body of caller\n" // NOLINT(*)
1810  " --undefined-function-is-assume-false\n"
1811  // NOLINTNEXTLINE(whitespace/line_length)
1812  " convert each call to an undefined function to assume(false)\n"
1816  "\n"
1817  "Loop transformations:\n"
1818  " --k-induction <k> check loops with k-induction\n"
1819  " --step-case k-induction: do step-case\n"
1820  " --base-case k-induction: do base-case\n"
1821  " --havoc-loops over-approximate all loops\n"
1822  " --accelerate add loop accelerators\n"
1823  " --skip-loops <loop-ids> add gotos to skip selected loops during execution\n" // NOLINT(*)
1824  "\n"
1825  "Memory model instrumentations:\n"
1826  " --mm <tso,pso,rmo,power> instruments a weak memory model\n"
1827  " --scc detects critical cycles per SCC (one thread per SCC)\n" // NOLINT(*)
1828  " --one-event-per-cycle only instruments one event per cycle\n"
1829  " --minimum-interference instruments an optimal number of events\n"
1830  " --my-events only instruments events whose ids appear in inst.evt\n" // NOLINT(*)
1831  " --cfg-kill enables symbolic execution used to reduce spurious cycles\n" // NOLINT(*)
1832  " --no-dependencies no dependency analysis\n"
1833  // NOLINTNEXTLINE(whitespace/line_length)
1834  " --no-po-rendering no representation of the threads in the dot\n"
1835  " --render-cluster-file clusterises the dot by files\n"
1836  " --render-cluster-function clusterises the dot by functions\n"
1837  "\n"
1838  "Slicing:\n"
1840  " --full-slice slice away instructions that don't affect assertions\n" // NOLINT(*)
1841  " --property id slice with respect to specific property only\n" // NOLINT(*)
1842  " --slice-global-inits slice away initializations of unused global variables\n" // NOLINT(*)
1843  " --aggressive-slice remove bodies of any functions not on the shortest path between\n" // NOLINT(*)
1844  " the start function and the function containing the property(s)\n" // NOLINT(*)
1845  " --aggressive-slice-call-depth <n>\n"
1846  " used with aggressive-slice, preserves all functions within <n> function calls\n" // NOLINT(*)
1847  " of the functions on the shortest path\n"
1848  " --aggressive-slice-preserve-function <f>\n"
1849  " force the aggressive slicer to preserve function <f>\n" // NOLINT(*)
1850  " --aggressive-slice-preserve-function containing <f>\n"
1851  " force the aggressive slicer to preserve all functions with names containing <f>\n" // NOLINT(*)
1852  "--aggressive-slice-preserve-all-direct-paths \n"
1853  " force aggressive slicer to preserve all direct paths\n" // NOLINT(*)
1854  "\n"
1855  "Further transformations:\n"
1856  " --constant-propagator propagate constants and simplify expressions\n" // NOLINT(*)
1857  " --inline perform full inlining\n"
1858  " --partial-inline perform partial inlining\n"
1859  " --function-inline <function> transitively inline all calls <function> makes\n" // NOLINT(*)
1860  " --no-caching disable caching of intermediate results during transitive function inlining\n" // NOLINT(*)
1861  " --log <file> log in json format which code segments were inlined, use with --function-inline\n" // NOLINT(*)
1862  " --remove-function-pointers replace function pointers by case statement over function calls\n" // NOLINT(*)
1863  " --value-set-fi-fp-removal build flow-insensitive value set and replace function pointers by a case statement\n" // NOLINT(*)
1864  " over the possible assignments. If the set of possible assignments is empty the function pointer\n" // NOLINT(*)
1865  " is removed using the standard remove-function-pointers pass. \n" // NOLINT(*)
1869  " --add-library add models of C library functions\n"
1870  " --model-argc-argv <n> model up to <n> command line arguments\n"
1871  // NOLINTNEXTLINE(whitespace/line_length)
1872  " --remove-function-body <f> remove the implementation of function <f> (may be repeated)\n"
1874  "\n"
1875  "Code contracts:\n"
1881  "\n"
1882  "Other options:\n"
1883  " --no-system-headers with --dump-c/--dump-cpp: generate C source expanding libc includes\n" // NOLINT(*)
1884  " --use-all-headers with --dump-c/--dump-cpp: generate C source with all includes\n" // NOLINT(*)
1885  " --harness with --dump-c/--dump-cpp: include input generator in output\n" // NOLINT(*)
1886  " --version show version and exit\n"
1887  HELP_FLUSH
1888  " --xml-ui use XML-formatted output\n"
1889  " --json-ui use JSON-formatted output\n"
1891  "\n";
1892  // clang-format on
1893 }
void accelerate_functions(goto_modelt &goto_model, message_handlert &message_handler, bool use_z3, guard_managert &guard_manager)
Definition: accelerate.cpp:637
Loop Acceleration.
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....
Pointer Dereferencing.
void print_struct_alignment_problems(const symbol_tablet &symbol_table, std::ostream &out)
Alignment Checks.
void cprover_c_library_factory(const std::set< irep_idt > &functions, symbol_tablet &symbol_table, message_handlert &message_handler)
#define HELP_ANSI_C_LANGUAGE
void branch(goto_modelt &goto_model, const irep_idt &id)
Definition: branch.cpp:22
Branch Instrumentation.
void parse_c_object_factory_options(const cmdlinet &cmdline, optionst &options)
Parse the c object factory parameters from a given command line.
Function Call Graphs.
static void list_calls_and_arguments(const namespacet &ns, const goto_programt &goto_program)
void check_call_sequence(const goto_modelt &goto_model)
void show_call_sequences(const irep_idt &caller, const goto_programt &goto_program)
Memory-mapped I/O Instrumentation for Goto Programs.
void show_class_hierarchy(const class_hierarchyt &hierarchy, ui_message_handlert &message_handler, bool children_only)
Output the class hierarchy.
Class Hierarchy.
#define HELP_SHOW_CLASS_HIERARCHY
The aggressive slicer removes the body of all the functions except those on the shortest path,...
std::list< std::string > user_specified_properties
void doit()
Removes the body of all functions except those on the shortest path or functions that are reachable f...
std::list< std::string > name_snippets
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.
virtual void output(const namespacet &ns, const irep_idt &function_id, const goto_programt &goto_program, std::ostream &out) const
Output the abstract states for a single function.
Definition: ai.cpp:40
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition: ai.h:564
A call graph (https://en.wikipedia.org/wiki/Call_graph) for a GOTO model or GOTO functions collection...
Definition: call_graph.h:44
void output_dot(std::ostream &out) const
Definition: call_graph.cpp:255
void output(std::ostream &out) const
Definition: call_graph.cpp:272
static call_grapht create_from_root_function(const goto_modelt &model, const irep_idt &root, bool collect_callsites)
Definition: call_graph.h:53
void output_xml(std::ostream &out) const
Definition: call_graph.cpp:282
Non-graph-based representation of the class hierarchy.
void output_dot(std::ostream &) const
Output class hierarchy in Graphviz DOT format.
std::string get_value(char option) const
Definition: cmdline.cpp:47
virtual bool isset(char option) const
Definition: cmdline.cpp:29
std::list< std::string > get_comma_separated_values(const char *option) const
Definition: cmdline.cpp:120
argst args
Definition: cmdline.h:143
const std::list< std::string > & get_values(const std::string &option) const
Definition: cmdline.cpp:108
bool replace_calls(const std::set< std::string > &functions)
Replace all calls to each function in the list with that function's contract.
Definition: contracts.cpp:1195
void apply_loop_contracts()
Definition: contracts.cpp:1244
bool enforce_contracts(const std::set< std::string > &functions)
Turn requires & ensures into assumptions and assertions for each of the named functions.
Definition: contracts.cpp:1272
void set_from_symbol_table(const symbol_tablet &)
Definition: config.cpp:1231
bool set(const cmdlinet &cmdline)
Definition: config.cpp:798
struct configt::ansi_ct ansi_c
void check(const goto_modelt &, bool xml, std::ostream &)
void instrument(goto_modelt &)
static function_pointer_restrictionst from_options(const optionst &options, const goto_modelt &goto_model, message_handlert &message_handler)
Parse function pointer restrictions from command line.
This is a may analysis (i.e.
void compute_loop_numbers()
function_mapt function_map
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
void help() override
display command line help
void do_indirect_call_and_rtti_removal(bool force=false)
void do_remove_const_function_pointers_only()
Remove function pointers that can be resolved by analysing const variables (i.e.
int doit() override
invoke main modules
void validate(const validation_modet vm=validation_modet::INVARIANT, const goto_model_validation_optionst &goto_model_validation_options=goto_model_validation_optionst{}) const override
Check that the goto model is well-formed.
Definition: goto_model.h:98
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:71
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &instruction) const
Output a single instruction.
unwind_strategyt
Definition: unwind.h:24
jsont output_log_json() const
Definition: unwind.h:70
void output_dot(std::ostream &out) const
Definition: graph.h:990
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
Definition: json.h:27
void output(std::ostream &out, const goto_functiont &goto_function, const namespacet &ns) const
A very simple, cheap analysis to determine when dereference operations are trivially guarded by a che...
void output_safe_dereferences(std::ostream &stream, const goto_programt &program, const namespacet &ns)
Output safely dereferenced expressions per instruction in human-readable format.
void output(std::ostream &stream, const goto_programt &program, const namespacet &ns)
Output non-null expressions per instruction in human-readable format.
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:105
mstreamt & error() const
Definition: message.h:399
mstreamt & status() const
Definition: message.h:414
message_handlert & get_message_handler()
Definition: message.h:184
@ M_STATISTICS
Definition: message.h:171
static eomt eom
Definition: message.h:297
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
bool is_set(const std::string &option) const
N.B. opts.is_set("foo") does not imply opts.get_bool_option("foo")
Definition: options.cpp:62
void set_option(const std::string &option, const bool value)
Definition: options.cpp:28
virtual int main()
ui_message_handlert ui_message_handler
Definition: parse_options.h:45
void output(std::ostream &out) const
Definition: points_to.cpp:33
void output(std::ostream &out, const goto_programt &goto_program, const namespacet &ns) const
Expression to hold a symbol (variable)
Definition: std_expr.h:80
Symbol table entry.
Definition: symbol.h:28
typet type
Type of symbol.
Definition: symbol.h:31
irep_idt name
The unique identifier.
Definition: symbol.h:40
virtual uit get_ui() const
Definition: ui_message.h:33
void parse_unwind(const std::string &unwind)
Definition: unwindset.cpp:20
void parse_unwindset(const std::list< std::string > &unwindset)
Definition: unwindset.cpp:59
void parse_unwindset_file(const std::string &file_name)
Definition: unwindset.cpp:93
This template class implements a data-flow analysis which keeps track of what values different variab...
void concurrency(value_setst &value_sets, goto_modelt &goto_model)
Encoding for Threaded Goto Programs.
configt config
Definition: config.cpp:25
Constant propagation.
#define HELP_REPLACE_CALL
Definition: contracts.h:40
#define FLAG_REPLACE_ALL_CALLS
Definition: contracts.h:44
#define FLAG_REPLACE_CALL
Definition: contracts.h:39
#define FLAG_ENFORCE_CONTRACT
Definition: contracts.h:49
#define HELP_ENFORCE_ALL_CONTRACTS
Definition: contracts.h:54
#define HELP_LOOP_CONTRACTS
Definition: contracts.h:35
#define FLAG_LOOP_CONTRACTS
Definition: contracts.h:34
#define HELP_ENFORCE_CONTRACT
Definition: contracts.h:50
#define HELP_REPLACE_ALL_CALLS
Definition: contracts.h:45
#define FLAG_ENFORCE_ALL_CONTRACTS
Definition: contracts.h:53
void count_eloc(const goto_modelt &goto_model)
Definition: count_eloc.cpp:54
void print_global_state_size(const goto_modelt &goto_model)
Definition: count_eloc.cpp:158
void print_path_lengths(const goto_modelt &goto_model)
Definition: count_eloc.cpp:85
void list_eloc(const goto_modelt &goto_model)
Definition: count_eloc.cpp:68
#define HELP_GOTO_PROGRAM_STATS
Definition: count_eloc.h:30
void cprover_cpp_library_factory(const std::set< irep_idt > &functions, symbol_tablet &symbol_table, message_handlert &message_handler)
#define CPROVER_PREFIX
Field-insensitive, location-sensitive bitvector analysis.
Field-Sensitive Program Dependence Analysis, Litvak et al., FSE 2010.
void document_properties_latex(const goto_modelt &goto_model, std::ostream &out)
void document_properties_html(const goto_modelt &goto_model, std::ostream &out)
Documentation of Properties.
void dot(const goto_modelt &src, std::ostream &out)
Definition: dot.cpp:352
Dump Goto-Program as DOT Graph.
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:1592
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:1579
void dump_c_type_header(const goto_functionst &src, const bool use_system_headers, const bool use_all_headers, const bool include_harness, const namespacet &ns, const std::string module, std::ostream &out)
Definition: dump_c.cpp:1614
Dump C from Goto Program.
bool ensure_one_backedge_per_target(goto_programt::targett &it, goto_programt &goto_program)
Ensure one backedge per target.
Field-insensitive, location-sensitive, over-approximative escape analysis.
Document and give macros for the exit codes of CPROVER binaries.
#define CPROVER_EXIT_CONVERSION_FAILED
Failure to convert / write to another format.
Definition: exit_codes.h:62
#define CPROVER_EXIT_INTERNAL_ERROR
An error has been encountered during processing the requested analysis.
Definition: exit_codes.h:45
#define CPROVER_EXIT_USAGE_ERROR
A usage error is returned when the command line is invalid or conflicting.
Definition: exit_codes.h:33
#define CPROVER_EXIT_SUCCESS
Success indicates the required analysis has been performed without error.
Definition: exit_codes.h:16
void full_slicer(goto_functionst &goto_functions, const namespacet &ns, const slicing_criteriont &criterion)
void property_slicer(goto_functionst &goto_functions, const namespacet &ns, const std::list< std::string > &properties)
void function_exit(goto_modelt &goto_model, const irep_idt &id)
Definition: function.cpp:101
void function_enter(goto_modelt &goto_model, const irep_idt &id)
Definition: function.cpp:76
Function Entering and Exiting.
std::unique_ptr< generate_function_bodiest > generate_function_bodies_factory(const std::string &options, const c_object_factory_parameterst &object_factory_parameters, const symbol_tablet &symbol_table, message_handlert &message_handler)
Create the type that actually generates the functions.
void generate_function_bodies(const std::regex &functions_regex, const generate_function_bodiest &generate_function_body, goto_modelt &model, message_handlert &message_handler)
Generate function bodies with some default behavior: assert-false, assume-false, assert-false-assume-...
#define HELP_REPLACE_FUNCTION_BODY
Field-insensitive, location-sensitive, over-approximative escape analysis.
void goto_check(const irep_idt &function_identifier, goto_functionst::goto_functiont &goto_function, const namespacet &ns, const optionst &options)
#define PARSE_OPTIONS_GOTO_CHECK(cmdline, options)
Definition: goto_check.h:70
#define HELP_GOTO_CHECK
Definition: goto_check.h:49
void goto_inline(goto_modelt &goto_model, message_handlert &message_handler, bool adjust_function)
Inline every function call into the entry_point() function.
Definition: goto_inline.cpp:26
void goto_function_inline(goto_modelt &goto_model, const irep_idt function, message_handlert &message_handler, bool adjust_function, bool caching)
Transitively inline all function calls made from a particular function.
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...
jsont goto_function_inline_and_log(goto_modelt &goto_model, const irep_idt function, message_handlert &message_handler, bool adjust_function, bool caching)
Function Inlining This gives a number of different interfaces to the function inlining functionality ...
Command Line Parsing.
#define forall_goto_program_instructions(it, program)
void remove_pointers(goto_modelt &goto_model, value_setst &value_sets)
Remove dereferences in all expressions contained in the program goto_model.
void havoc_loops(goto_modelt &goto_model)
Havoc Loops.
void horn_encoding(const goto_modelt &, std::ostream &)
Horn-clause Encoding.
bool insert_final_assert_false(goto_modelt &goto_model, const std::string &function_to_instrument, message_handlert &message_handler)
Transform a goto program by inserting assert(false) at the end of a given function function_to_instru...
Insert final assert false into a function.
#define HELP_INSERT_FINAL_ASSERT_FALSE
void interpreter(const goto_modelt &goto_model, message_handlert &message_handler)
Interpreter for GOTO Programs.
static void interrupt(value_setst &value_sets, const symbol_tablet &symbol_table, const irep_idt &function_id, goto_programt &goto_program, const symbol_exprt &interrupt_handler, const rw_set_baset &isr_rw_set)
Definition: interrupt.cpp:57
Interrupt Instrumentation for Goto Programs.
void interval_analysis(goto_modelt &goto_model)
Initialises the abstract interpretation over interval domain and instruments instructions using inter...
Interval Analysis.
Interval Domain.
Over-approximate Concurrency for Threaded Goto Programs.
void k_induction(goto_modelt &goto_model, bool base_case, bool step_case, unsigned k)
k-induction
void label_function_pointer_call_sites(goto_modelt &goto_model)
This ensures that call instructions can be only one of two things:
Label function pointer call sites across a goto model.
Compute lexical loops in a goto_function.
void show_lexical_loops(const goto_modelt &goto_model, std::ostream &out)
Field-insensitive, location-sensitive bitvector analysis.
Local safe pointer analysis.
void show_loop_ids(ui_message_handlert::uit ui, const goto_modelt &goto_model)
Definition: loop_ids.cpp:21
Loop IDs.
static void mmio(value_setst &value_sets, const symbol_tablet &symbol_table, const irep_idt &function_id, goto_programt &goto_program)
Definition: mmio.cpp:24
Memory-mapped I/O Instrumentation for Goto Programs.
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.
Initialize command line arguments.
Compute natural loops in a goto_function.
void show_natural_loops(const goto_modelt &goto_model, std::ostream &out)
Definition: natural_loops.h:92
void nondet_static(const namespacet &ns, goto_functionst &goto_functions, const irep_idt &fct_name)
Nondeterministically initializes global scope variables in a goto-function.
Nondeterministically initializes global scope variables, except for constants (such as string literal...
void parse_nondet_volatile_options(const cmdlinet &cmdline, optionst &options)
void nondet_volatile(goto_modelt &goto_model, const optionst &options)
Havoc reads from volatile expressions, if enabled in the options.
Volatile Variables.
#define HELP_NONDET_VOLATILE
void parameter_assignments(symbol_tablet &symbol_table, goto_functionst &goto_functions)
removes returns
Add parameter assignments.
std::string align_center_with_border(const std::string &text)
Utility for displaying help centered messages borderered by "* *".
std::string banner_string(const std::string &front_end, const std::string &version)
Field-sensitive, location-insensitive points-to analysis.
static void race_check(value_setst &value_sets, symbol_tablet &symbol_table, const irep_idt &function_id, goto_programt &goto_program, w_guardst &w_guards)
Definition: race_check.cpp:161
Race Detection for Threaded Goto Programs.
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.
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.
#define HELP_REACHABILITY_SLICER
Range-based reaching definitions analysis (following Field- Sensitive Program Dependence Analysis,...
static bool read_goto_binary(const std::string &filename, symbol_tablet &, goto_functionst &, message_handlert &)
Read a goto binary from a file, but do not update config.
Read Goto Programs.
void remove_asm(goto_functionst &goto_functions, symbol_tablet &symbol_table)
Replaces inline assembly instructions in the goto program (i.e., instructions of kind OTHER with a co...
Definition: remove_asm.cpp:511
Remove 'asm' statements by compiling them into suitable standard goto program instructions.
Remove calls to functions without a body.
#define HELP_REMOVE_CALLS_NO_BODY
#define HELP_REMOVE_CONST_FUNCTION_POINTERS
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...
Remove function definition.
bool remove_function_pointers(message_handlert &_message_handler, symbol_tablet &symbol_table, const goto_functionst &goto_functions, goto_programt &goto_program, const irep_idt &function_id, bool add_safety_assertion, bool only_remove_const_fps)
Remove Indirect Function Calls.
void restore_returns(goto_modelt &goto_model)
restores return statements
void remove_returns(symbol_table_baset &symbol_table, goto_functionst &goto_functions)
removes returns
Replace function returns by assignments to global variables.
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:86
Program Transformation.
void remove_unused_functions(goto_modelt &goto_model, message_handlert &message_handler)
Unused function removal.
void remove_virtual_functions(symbol_table_baset &symbol_table, goto_functionst &goto_functions)
Remove virtual function calls from all functions in the specified list and replace them with their mo...
Functions for replacing virtual function call with a static function calls in functions,...
#define HELP_REPLACE_CALLS
Definition: replace_calls.h:58
void restrict_function_pointers(goto_modelt &goto_model, const function_pointer_restrictionst &restrictions)
Apply function pointer restrictions to a goto_model.
void parse_function_pointer_restriction_options_from_cmdline(const cmdlinet &cmdline, optionst &options)
Given goto functions and a list of function parameters or globals that are function pointers with lis...
#define RESTRICT_FUNCTION_POINTER_OPT
#define RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT
#define HELP_RESTRICT_FUNCTION_POINTER
#define RESTRICT_FUNCTION_POINTER_BY_NAME_OPT
void rewrite_union(exprt &expr)
We rewrite u.c for unions u into byte_extract(u, 0), and { .c = v } into byte_update(NIL,...
Symbolic Execution.
Race Detection for Threaded Goto Programs.
Single-entry, single-exit region analysis.
void label_properties(goto_modelt &goto_model)
Set the properties to check.
void show_goto_functions(const namespacet &ns, ui_message_handlert &ui_message_handler, const goto_functionst &goto_functions, bool list_only)
#define HELP_SHOW_GOTO_FUNCTIONS
void show_locations(ui_message_handlert::uit ui, const irep_idt function_id, const goto_programt &goto_program)
Show program locations.
void show_properties(const namespacet &ns, const irep_idt &identifier, message_handlert &message_handler, ui_message_handlert::uit ui, const goto_programt &goto_program)
Show the properties.
#define HELP_SHOW_PROPERTIES
void show_symbol_table(const symbol_tablet &symbol_table, ui_message_handlert &ui)
void show_symbol_table_brief(const symbol_tablet &symbol_table, ui_message_handlert &ui)
Show the symbol table.
void show_value_sets(ui_message_handlert::uit ui, const goto_modelt &goto_model, const value_set_analysist &value_set_analysis)
Show Value Sets.
static bool skip_loops(goto_programt &goto_program, const loop_idst &loop_ids, messaget &message)
Definition: skip_loops.cpp:24
Skip over selected loops by adding gotos.
void slice_global_inits(goto_modelt &goto_model)
Remove initializations of unused global variables.
bool splice_call(goto_functionst &goto_functions, const std::string &callercallee, const symbol_tablet &symbol_table, message_handlert &message_handler)
Definition: splice_call.cpp:34
Harnessing for goto functions.
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
void stack_depth(goto_programt &goto_program, const symbol_exprt &symbol, const std::size_t i_depth, const exprt &max_depth)
Definition: stack_depth.cpp:44
Stack depth checks.
unsigned safe_string2unsigned(const std::string &str, int base)
Definition: string2int.cpp:16
unsigned unsafe_string2unsigned(const std::string &str, int base)
Definition: string2int.cpp:35
std::size_t safe_string2size_t(const std::string &str, int base)
Definition: string2int.cpp:23
void string_abstraction(symbol_tablet &symbol_table, message_handlert &message_handler, goto_functionst &dest)
String Abstraction.
void split_string(const std::string &s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)
irep_idt arch
Definition: config.h:164
std::list< std::string > defines
Definition: config.h:201
This is unused by this implementation of guards, but can be used by other implementations of the same...
Definition: guard_expr.h:20
void thread_exit_instrumentation(goto_programt &goto_program)
void mutex_init_instrumentation(const symbol_tablet &symbol_table, goto_programt &goto_program, typet lock_type)
#define HELP_TIMESTAMP
Definition: timestamper.h:14
#define HELP_FLUSH
Definition: ui_message.h:108
void list_undefined_functions(const goto_modelt &goto_model, std::ostream &os)
void undefined_function_abort_path(goto_modelt &goto_model)
Handling of functions without body.
std::wstring widen(const char *s)
Definition: unicode.cpp:48
void add_uninitialized_locals_assertions(goto_modelt &goto_model)
void show_uninitialized(const goto_modelt &goto_model, std::ostream &out)
Detection for Uninitialized Local Variables.
Loop unwinding.
Loop unwinding.
#define HELP_VALIDATE
Value Set Propagation.
void value_set_fi_fp_removal(goto_modelt &goto_model, message_handlert &message_handler)
Builds the flow-insensitive value set for all function pointers and replaces function pointers with a...
flow insensitive value set function pointer removal
const char * CBMC_VERSION
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)
Weak Memory Instrumentation for Threaded Goto Programs.
memory_modelt
Definition: wmm.h:18
@ Unknown
Definition: wmm.h:19
@ TSO
Definition: wmm.h:20
@ RMO
Definition: wmm.h:22
@ PSO
Definition: wmm.h:21
@ Power
Definition: wmm.h:23
loop_strategyt
Definition: wmm.h:37
@ all_loops
Definition: wmm.h:39
@ arrays_only
Definition: wmm.h:38
@ no_loop
Definition: wmm.h:40
instrumentation_strategyt
Definition: wmm.h:27
@ my_events
Definition: wmm.h:32
@ one_event_per_cycle
Definition: wmm.h:33
@ min_interference
Definition: wmm.h:29
@ read_first
Definition: wmm.h:30
@ all
Definition: wmm.h:28
@ write_first
Definition: wmm.h:31
bool write_goto_binary(std::ostream &out, const symbol_tablet &symbol_table, const goto_functionst &goto_functions, irep_serializationt &irepconverter)
Writes a goto program to disc, using goto binary format.
Write GOTO binaries.