cprover
goto_instrument_parse_options.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Main Module
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
13 
14 #include <fstream>
15 #include <iostream>
16 #include <memory>
17 
18 #include <util/config.h>
19 #include <util/string2int.h>
20 #include <util/unicode.h>
21 #include <util/json.h>
22 
37 #include <goto-programs/loop_ids.h>
44 
49 
50 #include <analyses/natural_loops.h>
55 #include <analyses/call_graph.h>
61 #include <analyses/is_threaded.h>
62 
63 #include <cbmc/version.h>
64 
65 #include "document_properties.h"
66 #include "uninitialized.h"
67 #include "full_slicer.h"
68 #include "reachability_slicer.h"
69 #include "show_locations.h"
70 #include "points_to.h"
71 #include "alignment_checks.h"
72 #include "race_check.h"
73 #include "nondet_volatile.h"
74 #include "interrupt.h"
75 #include "mmio.h"
76 #include "stack_depth.h"
77 #include "nondet_static.h"
78 #include "rw_set.h"
79 #include "concurrency.h"
80 #include "dump_c.h"
81 #include "dot.h"
82 #include "havoc_loops.h"
83 #include "k_induction.h"
84 #include "function.h"
85 #include "branch.h"
86 #include "wmm/weak_memory.h"
87 #include "call_sequences.h"
88 #include "accelerate/accelerate.h"
89 #include "count_eloc.h"
90 #include "horn_encoding.h"
91 #include "thread_instrumentation.h"
92 #include "skip_loops.h"
93 #include "code_contracts.h"
94 #include "unwind.h"
95 #include "model_argc_argv.h"
96 #include "undefined_functions.h"
97 #include "remove_function.h"
98 
100 {
101  unsigned int v=8;
102 
103  if(cmdline.isset("verbosity"))
104  {
105  v=unsafe_string2unsigned(cmdline.get_value("verbosity"));
106  if(v>10)
107  v=10;
108  }
109 
111 }
112 
115 {
116  if(cmdline.isset("version"))
117  {
118  std::cout << CBMC_VERSION << '\n';
119  return 0;
120  }
121 
122  if(cmdline.args.size()!=1 && cmdline.args.size()!=2)
123  {
124  help();
125  return 0;
126  }
127 
128  eval_verbosity();
129 
130  try
131  {
133 
135 
137 
138  {
139  bool unwind=cmdline.isset("unwind");
140  bool unwindset=cmdline.isset("unwindset");
141  bool unwindset_file=cmdline.isset("unwindset-file");
142 
143  if(unwindset && unwindset_file)
144  throw "only one of --unwindset and --unwindset-file supported at a "
145  "time";
146 
147  if(unwind || unwindset || unwindset_file)
148  {
149  int k=-1;
150 
151  if(unwind)
152  k=std::stoi(cmdline.get_value("unwind"));
153 
154  unwind_sett unwind_set;
155 
156  if(unwindset_file)
157  {
158  std::string us;
159  std::string fn=cmdline.get_value("unwindset-file");
160 
161 #ifdef _MSC_VER
162  std::ifstream file(widen(fn));
163 #else
164  std::ifstream file(fn);
165 #endif
166  if(!file)
167  throw "cannot open file "+fn;
168 
169  std::stringstream buffer;
170  buffer << file.rdbuf();
171  us=buffer.str();
172  parse_unwindset(us, unwind_set);
173  }
174  else if(unwindset)
175  parse_unwindset(cmdline.get_value("unwindset"), unwind_set);
176 
177  bool unwinding_assertions=cmdline.isset("unwinding-assertions");
178  bool partial_loops=cmdline.isset("partial-loops");
179  bool continue_as_loops=cmdline.isset("continue-as-loops");
180 
181  if(unwinding_assertions+partial_loops+continue_as_loops>1)
182  throw "more than one of --unwinding-assertions,--partial-loops,"
183  "--continue-as-loops selected";
184 
185  goto_unwindt::unwind_strategyt unwind_strategy=
187 
188  if(unwinding_assertions)
189  {
191  }
192  else if(partial_loops)
193  {
195  }
196  else if(continue_as_loops)
197  {
199  }
200 
201  goto_unwindt goto_unwind;
202  goto_unwind(goto_functions, unwind_set, k, unwind_strategy);
203 
206 
207  if(cmdline.isset("log"))
208  {
209  std::string filename=cmdline.get_value("log");
210  bool have_file=!filename.empty() && filename!="-";
211 
212  jsont result=goto_unwind.output_log_json();
213 
214  if(have_file)
215  {
216 #ifdef _MSC_VER
217  std::ofstream of(widen(filename));
218 #else
219  std::ofstream of(filename);
220 #endif
221  if(!of)
222  throw "failed to open file "+filename;
223 
224  of << result;
225  of.close();
226  }
227  else
228  {
229  std::cout << result << '\n';
230  }
231  }
232  }
233  }
234 
235  if(cmdline.isset("show-threaded"))
236  {
238 
239  is_threadedt is_threaded(goto_functions);
240 
242  {
243  std::cout << "////\n";
244  std::cout << "//// Function: " << f_it->first << '\n';
245  std::cout << "////\n\n";
246 
247  const goto_programt &goto_program=f_it->second.body;
248 
249  forall_goto_program_instructions(i_it, goto_program)
250  {
251  goto_program.output_instruction(ns, "", std::cout, i_it);
252  std::cout << "Is threaded: " << (is_threaded(i_it)?"True":"False")
253  << "\n\n";
254  }
255  }
256  }
257 
258  if(cmdline.isset("show-value-sets"))
259  {
262 
263  // recalculate numbers, etc.
265 
266  status() << "Pointer Analysis" << eom;
268  value_set_analysist value_set_analysis(ns);
269  value_set_analysis(goto_functions);
270 
271  show_value_sets(get_ui(), goto_functions, value_set_analysis);
272  return 0;
273  }
274 
275  if(cmdline.isset("show-global-may-alias"))
276  {
281 
282  // recalculate numbers, etc.
284 
286  global_may_alias_analysist global_may_alias_analysis;
287  global_may_alias_analysis(goto_functions, ns);
288  global_may_alias_analysis.output(ns, goto_functions, std::cout);
289 
290  return 0;
291  }
292 
293  if(cmdline.isset("show-local-bitvector-analysis"))
294  {
298 
299  // recalculate numbers, etc.
301 
303 
305  {
306  local_bitvector_analysist local_bitvector_analysis(it->second);
307  std::cout << ">>>>\n";
308  std::cout << ">>>> " << it->first << '\n';
309  std::cout << ">>>>\n";
310  local_bitvector_analysis.output(std::cout, it->second, ns);
311  std::cout << '\n';
312  }
313 
314  return 0;
315  }
316 
317  if(cmdline.isset("show-custom-bitvector-analysis"))
318  {
323 
325 
326  if(!cmdline.isset("inline"))
327  {
330  }
331 
332  // recalculate numbers, etc.
334 
336  custom_bitvector_analysist custom_bitvector_analysis;
337  custom_bitvector_analysis(goto_functions, ns);
338  custom_bitvector_analysis.output(ns, goto_functions, std::cout);
339 
340  return 0;
341  }
342 
343  if(cmdline.isset("show-escape-analysis"))
344  {
349 
350  // recalculate numbers, etc.
352 
354 
355  escape_analysist escape_analysis;
356  escape_analysis(goto_functions, ns);
357 
358  escape_analysis.output(ns, goto_functions, std::cout);
359 
360  return 0;
361  }
362 
363  if(cmdline.isset("custom-bitvector-analysis"))
364  {
369 
371 
372  if(!cmdline.isset("inline"))
373  {
376  }
377 
378  // recalculate numbers, etc.
380 
382 
383  custom_bitvector_analysist custom_bitvector_analysis;
384  custom_bitvector_analysis(goto_functions, ns);
385  custom_bitvector_analysis.check(
386  ns,
388  cmdline.isset("xml-ui"),
389  std::cout);
390 
391  return 0;
392  }
393 
394  if(cmdline.isset("show-points-to"))
395  {
398 
399  // recalculate numbers, etc.
401 
403 
404  status() << "Pointer Analysis" << eom;
405  points_tot points_to;
406  points_to(goto_functions);
407  points_to.output(std::cout);
408  return 0;
409  }
410 
411  if(cmdline.isset("show-intervals"))
412  {
415 
416  // recalculate numbers, etc.
418 
419  status() << "Interval Analysis" << eom;
423 
424  interval_analysis.output(ns, goto_functions, std::cout);
425  return 0;
426  }
427 
428  if(cmdline.isset("show-call-sequences"))
429  {
431  return 0;
432  }
433 
434  if(cmdline.isset("check-call-sequence"))
435  {
438  return 0;
439  }
440 
441  if(cmdline.isset("list-calls-args"))
442  {
445 
448 
449  return 0;
450  }
451 
452  if(cmdline.isset("show-rw-set"))
453  {
455 
456  if(!cmdline.isset("inline"))
457  {
460 
461  // recalculate numbers, etc.
463  }
464 
465  status() << "Pointer Analysis" << eom;
466  value_set_analysist value_set_analysis(ns);
467  value_set_analysis(goto_functions);
468 
469  const symbolt &symbol=ns.lookup(ID_main);
470  symbol_exprt main(symbol.name, symbol.type);
471 
472  std::cout <<
473  rw_set_functiont(value_set_analysis, ns, goto_functions, main);
474  return 0;
475  }
476 
477  if(cmdline.isset("show-symbol-table"))
478  {
480  return 0;
481  }
482 
483  if(cmdline.isset("show-reaching-definitions"))
484  {
486 
487  const namespacet ns(symbol_table);
488  reaching_definitions_analysist rd_analysis(ns);
489  rd_analysis(goto_functions, ns);
490 
491  rd_analysis.output(ns, goto_functions, std::cout);
492 
493  return 0;
494  }
495 
496  if(cmdline.isset("show-dependence-graph"))
497  {
499 
500  const namespacet ns(symbol_table);
501  dependence_grapht dependence_graph(ns);
502  dependence_graph(goto_functions, ns);
503 
504  dependence_graph.output(ns, goto_functions, std::cout);
505  dependence_graph.output_dot(std::cout);
506 
507  return 0;
508  }
509 
510  if(cmdline.isset("count-eloc"))
511  {
513  return 0;
514  }
515 
516  if(cmdline.isset("list-eloc"))
517  {
519  return 0;
520  }
521 
522  if(cmdline.isset("print-path-lengths"))
523  {
525  return 0;
526  }
527 
528  if(cmdline.isset("list-symbols"))
529  {
530  show_symbol_table(true);
531  return 0;
532  }
533 
534  if(cmdline.isset("show-uninitialized"))
535  {
537  return 0;
538  }
539 
540  if(cmdline.isset("interpreter"))
541  {
542  status() << "Starting interpreter" << eom;
544  return 0;
545  }
546 
547  if(cmdline.isset("show-claims") ||
548  cmdline.isset("show-properties"))
549  {
550  const namespacet ns(symbol_table);
552  return 0;
553  }
554 
555  if(cmdline.isset("document-claims-html") ||
556  cmdline.isset("document-properties-html"))
557  {
559  return 0;
560  }
561 
562  if(cmdline.isset("document-claims-latex") ||
563  cmdline.isset("document-properties-latex"))
564  {
566  return 0;
567  }
568 
569  if(cmdline.isset("show-loops"))
570  {
572  return 0;
573  }
574 
575  if(cmdline.isset("show-natural-loops"))
576  {
577  const namespacet ns(symbol_table);
579  return 0;
580  }
581 
582  if(cmdline.isset("print-internal-representation"))
583  {
584  for(auto const &pair : goto_functions.function_map)
585  for(auto const &ins : pair.second.body.instructions)
586  {
587  if(ins.code.is_not_nil())
588  status() << ins.code.pretty() << eom;
589  if(ins.guard.is_not_nil())
590  status() << "[guard] " << ins.guard.pretty() << eom;
591  }
592  return 0;
593  }
594 
595  if(cmdline.isset("show-goto-functions"))
596  {
599  return 0;
600  }
601 
602  if(cmdline.isset("list-undefined-functions"))
603  {
604  const namespacet ns(symbol_table);
606  return 0;
607  }
608 
609  // experimental: print structs
610  if(cmdline.isset("show-struct-alignment"))
611  {
613  return 0;
614  }
615 
616  if(cmdline.isset("show-locations"))
617  {
619  return 0;
620  }
621 
622  if(cmdline.isset("dump-c") || cmdline.isset("dump-cpp"))
623  {
624  const bool is_cpp=cmdline.isset("dump-cpp");
625  const bool h_libc=!cmdline.isset("no-system-headers");
626  const bool h_all=cmdline.isset("use-all-headers");
628 
629  // restore RETURN instructions in case remove_returns had been
630  // applied
632 
633  if(cmdline.args.size()==2)
634  {
635  #ifdef _MSC_VER
636  std::ofstream out(widen(cmdline.args[1]));
637  #else
638  std::ofstream out(cmdline.args[1]);
639  #endif
640  if(!out)
641  {
642  error() << "failed to write to `" << cmdline.args[1] << "'";
643  return 10;
644  }
645  (is_cpp ? dump_cpp : dump_c)(goto_functions, h_libc, h_all, ns, out);
646  }
647  else
648  (is_cpp ? dump_cpp : dump_c)(
649  goto_functions, h_libc, h_all, ns, std::cout);
650 
651  return 0;
652  }
653 
654  if(cmdline.isset("call-graph"))
655  {
656  call_grapht call_graph(goto_functions);
657 
658  if(cmdline.isset("xml"))
659  call_graph.output_xml(std::cout);
660  else if(cmdline.isset("dot"))
661  call_graph.output_dot(std::cout);
662  else
663  call_graph.output(std::cout);
664 
665  return 0;
666  }
667 
668  if(cmdline.isset("dot"))
669  {
671 
672  if(cmdline.args.size()==2)
673  {
674  #ifdef _MSC_VER
675  std::ofstream out(widen(cmdline.args[1]));
676  #else
677  std::ofstream out(cmdline.args[1]);
678  #endif
679  if(!out)
680  {
681  error() << "failed to write to " << cmdline.args[1] << "'";
682  return 10;
683  }
684 
685  dot(goto_functions, ns, out);
686  }
687  else
688  dot(goto_functions, ns, std::cout);
689 
690  return 0;
691  }
692 
693  if(cmdline.isset("accelerate"))
694  {
696 
698 
699  status() << "Performing full inlining" << eom;
701 
702  status() << "Accelerating" << eom;
706  }
707 
708  if(cmdline.isset("horn-encoding"))
709  {
710  status() << "Horn-clause encoding" << eom;
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 
721  if(!out)
722  {
723  error() << "Failed to open output file "
724  << cmdline.args[1] << eom;
725  return 1;
726  }
727 
728  horn_encoding(goto_functions, ns, out);
729  }
730  else
731  horn_encoding(goto_functions, ns, std::cout);
732 
733  return 0;
734  }
735 
736  if(cmdline.isset("drop-unused-functions"))
737  {
739 
740  status() << "Removing unused functions" << eom;
742  }
743 
744  if(cmdline.isset("undefined-function-is-assume-false"))
745  {
747 
749  }
750 
751  // write new binary?
752  if(cmdline.args.size()==2)
753  {
754  status() << "Writing GOTO program to `" << cmdline.args[1] << "'" << eom;
755 
758  return 1;
759  else
760  return 0;
761  }
762 
763  help();
764  return 0;
765  }
766 
767  catch(const char *e)
768  {
769  error() << e << eom;
770  return 11;
771  }
772 
773  catch(const std::string e)
774  {
775  error() << e << eom;
776  return 11;
777  }
778 
779  catch(int)
780  {
781  return 11;
782  }
783 
784  catch(std::bad_alloc)
785  {
786  error() << "Out of memory" << eom;
787  return 11;
788  }
789 // NOLINTNEXTLINE(readability/fn_size)
790 }
791 
793  bool force)
794 {
795  if(function_pointer_removal_done && !force)
796  return;
797 
799 
800  status() << "Function Pointer Removal" << eom;
803  symbol_table,
805  cmdline.isset("pointer-check"));
806  status() << "Virtual function removal" << eom;
808  status() << "Catch and throw removal" << eom;
810  status() << "Java instanceof removal" << eom;
812 }
813 
818 {
819  // Don't bother if we've already done a full function pointer
820  // removal.
822  {
823  return;
824  }
825 
826  status() << "Removing const function pointers only" << eom;
829  symbol_table,
831  cmdline.isset("pointer-check"),
832  true); // abort if we can't resolve via const pointers
833 }
834 
836 {
838  return;
839 
841 
842  if(!cmdline.isset("inline"))
843  {
844  status() << "Partial Inlining" << eom;
845  const namespacet ns(symbol_table);
847  }
848 }
849 
851 {
853  return;
854 
855  remove_returns_done=true;
856 
857  status() << "Removing returns" << eom;
859 }
860 
862 {
863  status() << "Reading GOTO program from `" << cmdline.args[0] << "'" << eom;
864 
867  throw 0;
868 
869  config.set(cmdline);
871 }
872 
874 {
875  optionst options;
876 
877  // disable simplify when adding various checks?
878  if(cmdline.isset("no-simplify"))
879  options.set_option("simplify", false);
880  else
881  options.set_option("simplify", true);
882 
883  // use assumptions instead of assertions?
884  if(cmdline.isset("assert-to-assume"))
885  options.set_option("assert-to-assume", true);
886  else
887  options.set_option("assert-to-assume", false);
888 
889  // all checks supported by goto_check
891 
892  // check assertions
893  if(cmdline.isset("no-assertions"))
894  options.set_option("assertions", false);
895  else
896  options.set_option("assertions", true);
897 
898  // use assumptions
899  if(cmdline.isset("no-assumptions"))
900  options.set_option("assumptions", false);
901  else
902  options.set_option("assumptions", true);
903 
904  // magic error label
905  if(cmdline.isset("error-label"))
906  options.set_option("error-label", cmdline.get_value("error-label"));
907 
908  // unwind loops
909  if(cmdline.isset("unwind"))
910  {
911  status() << "Unwinding loops" << eom;
912  options.set_option("unwind", cmdline.get_value("unwind"));
913  }
914 
915  // skip over selected loops
916  if(cmdline.isset("skip-loops"))
917  {
918  status() << "Adding gotos to skip loops" << eom;
919  if(skip_loops(
921  cmdline.get_value("skip-loops"),
923  throw 0;
924  }
925 
927 
928  // initialize argv with valid pointers
929  if(cmdline.isset("model-argc-argv"))
930  {
931  unsigned max_argc=
932  safe_string2unsigned(cmdline.get_value("model-argc-argv"));
933 
934  status() << "Adding up to " << max_argc
935  << " command line arguments" << eom;
936  if(model_argc_argv(
937  symbol_table,
939  max_argc,
941  throw 0;
942  }
943 
944  if(cmdline.isset("remove-function-body"))
945  {
947  symbol_table,
949  cmdline.get_values("remove-function-body"),
951  }
952 
953  // we add the library in some cases, as some analyses benefit
954 
955  if(cmdline.isset("add-library") ||
956  cmdline.isset("mm"))
957  {
958  if(cmdline.isset("show-custom-bitvector-analysis") ||
959  cmdline.isset("custom-bitvector-analysis"))
960  config.ansi_c.defines.push_back("__CPROVER_CUSTOM_BITVECTOR_ANALYSIS");
961 
962  // add the library
964  }
965 
966  // now do full inlining, if requested
967  if(cmdline.isset("inline"))
968  {
970 
971  if(cmdline.isset("show-custom-bitvector-analysis") ||
972  cmdline.isset("custom-bitvector-analysis"))
973  {
977  }
978 
979  status() << "Performing full inlining" << eom;
981  }
982 
983  if(cmdline.isset("show-custom-bitvector-analysis") ||
984  cmdline.isset("custom-bitvector-analysis"))
985  {
987 
988  status() << "Propagating Constants" << eom;
989  constant_propagator_ait constant_propagator_ai(goto_functions, ns);
991  }
992 
993  if(cmdline.isset("escape-analysis"))
994  {
999 
1000  // recalculate numbers, etc.
1002 
1003  status() << "Escape Analysis" << eom;
1004  escape_analysist escape_analysis;
1005  escape_analysis(goto_functions, ns);
1006  escape_analysis.instrument(goto_functions, ns);
1007 
1008  // inline added functions, they are often small
1010 
1011  // recalculate numbers, etc.
1013  }
1014 
1015  // verify and set invariants and pre/post-condition pairs
1016  if(cmdline.isset("apply-code-contracts"))
1017  {
1018  status() << "Applying Code Contracts" << eom;
1020  }
1021 
1022  // replace function pointers, if explicitly requested
1023  if(cmdline.isset("remove-function-pointers"))
1024  {
1026  }
1027  else if(cmdline.isset("remove-const-function-pointers"))
1028  {
1030  }
1031 
1032  if(cmdline.isset("function-inline"))
1033  {
1034  std::string function=cmdline.get_value("function-inline");
1035  assert(!function.empty());
1036 
1037  bool caching=!cmdline.isset("no-caching");
1038 
1040 
1041  status() << "Inlining calls of function `" << function << "'" << eom;
1042 
1043  if(!cmdline.isset("log"))
1044  {
1047  function,
1048  ns,
1050  true,
1051  caching);
1052  }
1053  else
1054  {
1055  std::string filename=cmdline.get_value("log");
1056  bool have_file=!filename.empty() && filename!="-";
1057 
1058  jsont result=
1061  function,
1062  ns,
1064  true,
1065  caching);
1066 
1067  if(have_file)
1068  {
1069 #ifdef _MSC_VER
1070  std::ofstream of(widen(filename));
1071 #else
1072  std::ofstream of(filename);
1073 #endif
1074  if(!of)
1075  throw "failed to open file "+filename;
1076 
1077  of << result;
1078  of.close();
1079  }
1080  else
1081  {
1082  std::cout << result << '\n';
1083  }
1084  }
1085 
1088  }
1089 
1090  if(cmdline.isset("partial-inline"))
1091  {
1093 
1094  status() << "Partial inlining" << eom;
1096 
1099  }
1100 
1101  // now do full inlining, if requested
1102  if(cmdline.isset("inline"))
1103  {
1104  do_indirect_call_and_rtti_removal(/*force=*/true);
1105 
1106  if(cmdline.isset("show-custom-bitvector-analysis") ||
1107  cmdline.isset("custom-bitvector-analysis"))
1108  {
1112  }
1113 
1114  status() << "Performing full inlining" << eom;
1116  }
1117 
1118  if(cmdline.isset("constant-propagator"))
1119  {
1121 
1122  status() << "Propagating Constants" << eom;
1123 
1124  constant_propagator_ait constant_propagator_ai(goto_functions, ns);
1125 
1127  }
1128 
1129  // add generic checks, if needed
1130  goto_check(ns, options, goto_functions);
1131 
1132  // check for uninitalized local variables
1133  if(cmdline.isset("uninitialized-check"))
1134  {
1135  status() << "Adding checks for uninitialized local variables" << eom;
1137  }
1138 
1139  // check for maximum call stack size
1140  if(cmdline.isset("stack-depth"))
1141  {
1142  status() << "Adding check for maximum call stack size" << eom;
1143  stack_depth(
1144  symbol_table,
1146  unsafe_string2unsigned(cmdline.get_value("stack-depth")));
1147  }
1148 
1149  // ignore default/user-specified initialization of variables with static
1150  // lifetime
1151  if(cmdline.isset("nondet-static"))
1152  {
1153  status() << "Adding nondeterministic initialization of static/global "
1154  "variables" << eom;
1156  }
1157 
1158  if(cmdline.isset("slice-global-inits"))
1159  {
1160  status() << "Slicing away initializations of unused global variables"
1161  << eom;
1163  }
1164 
1165  if(cmdline.isset("string-abstraction"))
1166  {
1169 
1170  status() << "String Abstraction" << eom;
1172  symbol_table,
1174  goto_functions);
1175  }
1176 
1177  // some analyses require function pointer removal and partial inlining
1178 
1179  if(cmdline.isset("remove-pointers") ||
1180  cmdline.isset("race-check") ||
1181  cmdline.isset("mm") ||
1182  cmdline.isset("isr") ||
1183  cmdline.isset("concurrency"))
1184  {
1187 
1188  status() << "Pointer Analysis" << eom;
1189  value_set_analysist value_set_analysis(ns);
1190  value_set_analysis(goto_functions);
1191 
1192  if(cmdline.isset("remove-pointers"))
1193  {
1194  // removing pointers
1195  status() << "Removing Pointers" << eom;
1198  symbol_table,
1199  value_set_analysis);
1200  }
1201 
1202  if(cmdline.isset("race-check"))
1203  {
1204  status() << "Adding Race Checks" << eom;
1205  race_check(
1206  value_set_analysis,
1207  symbol_table,
1208  goto_functions);
1209  }
1210 
1211  if(cmdline.isset("mm"))
1212  {
1213  // TODO: move to wmm/weak_mem, and copy goto_functions AFTER some of the
1214  // modifications. Do the analysis on the copy, after remove_asm, and
1215  // instrument the original (without remove_asm)
1218 
1219  std::string mm=cmdline.get_value("mm");
1220  memory_modelt model;
1221 
1222  // strategy of instrumentation
1223  instrumentation_strategyt inst_strategy;
1224  if(cmdline.isset("one-event-per-cycle"))
1225  inst_strategy=one_event_per_cycle;
1226  else if(cmdline.isset("minimum-interference"))
1227  inst_strategy=min_interference;
1228  else if(cmdline.isset("read-first"))
1229  inst_strategy=read_first;
1230  else if(cmdline.isset("write-first"))
1231  inst_strategy=write_first;
1232  else if(cmdline.isset("my-events"))
1233  inst_strategy=my_events;
1234  else
1235  /* default: instruments all unsafe pairs */
1236  inst_strategy=all;
1237 
1238  const unsigned unwind_loops=
1239  cmdline.isset("unwind")?
1241  const unsigned max_var=
1242  cmdline.isset("max-var")?
1244  const unsigned max_po_trans=
1245  cmdline.isset("max-po-trans")?
1246  unsafe_string2unsigned(cmdline.get_value("max-po-trans")):0;
1247 
1248  if(mm=="tso")
1249  {
1250  status() << "Adding weak memory (TSO) Instrumentation" << eom;
1251  model=TSO;
1252  }
1253  else if(mm=="pso")
1254  {
1255  status() << "Adding weak memory (PSO) Instrumentation" << eom;
1256  model=PSO;
1257  }
1258  else if(mm=="rmo")
1259  {
1260  status() << "Adding weak memory (RMO) Instrumentation" << eom;
1261  model=RMO;
1262  }
1263  else if(mm=="power")
1264  {
1265  status() << "Adding weak memory (Power) Instrumentation" << eom;
1266  model=Power;
1267  }
1268  else
1269  {
1270  error() << "Unknown weak memory model `" << mm << "'" << eom;
1271  model=Unknown;
1272  }
1273 
1275 
1276  if(cmdline.isset("force-loop-duplication"))
1277  loops=all_loops;
1278  if(cmdline.isset("no-loop-duplication"))
1279  loops=no_loop;
1280 
1281  if(model!=Unknown)
1282  weak_memory(
1283  model,
1284  value_set_analysis,
1285  symbol_table,
1287  cmdline.isset("scc"),
1288  inst_strategy,
1289  unwind_loops,
1290  !cmdline.isset("cfg-kill"),
1291  cmdline.isset("no-dependencies"),
1292  loops,
1293  max_var,
1294  max_po_trans,
1295  !cmdline.isset("no-po-rendering"),
1296  cmdline.isset("render-cluster-file"),
1297  cmdline.isset("render-cluster-function"),
1298  cmdline.isset("cav11"),
1299  cmdline.isset("hide-internals"),
1301  cmdline.isset("ignore-arrays"));
1302  }
1303 
1304  // Interrupt handler
1305  if(cmdline.isset("isr"))
1306  {
1307  status() << "Instrumenting interrupt handler" << eom;
1308  interrupt(
1309  value_set_analysis,
1310  symbol_table,
1312  cmdline.get_value("isr"));
1313  }
1314 
1315  // Memory-mapped I/O
1316  if(cmdline.isset("mmio"))
1317  {
1318  status() << "Instrumenting memory-mapped I/O" << eom;
1319  mmio(
1320  value_set_analysis,
1321  symbol_table,
1322  goto_functions);
1323  }
1324 
1325  if(cmdline.isset("concurrency"))
1326  {
1327  status() << "Sequentializing concurrency" << eom;
1328  concurrency(
1329  value_set_analysis,
1330  symbol_table,
1331  goto_functions);
1332  }
1333  }
1334 
1335  if(cmdline.isset("interval-analysis"))
1336  {
1337  status() << "Interval analysis" << eom;
1339  }
1340 
1341  if(cmdline.isset("havoc-loops"))
1342  {
1343  status() << "Havocking loops" << eom;
1345  }
1346 
1347  if(cmdline.isset("k-induction"))
1348  {
1349  bool base_case=cmdline.isset("base-case");
1350  bool step_case=cmdline.isset("step-case");
1351 
1352  if(step_case && base_case)
1353  throw "please specify only one of --step-case and --base-case";
1354  else if(!step_case && !base_case)
1355  throw "please specify one of --step-case and --base-case";
1356 
1357  unsigned k=unsafe_string2unsigned(cmdline.get_value("k-induction"));
1358 
1359  if(k==0)
1360  throw "please give k>=1";
1361 
1362  status() << "Instrumenting k-induction for k=" << k << ", "
1363  << (base_case?"base case":"step case") << eom;
1364 
1365  k_induction(goto_functions, base_case, step_case, k);
1366  }
1367 
1368  if(cmdline.isset("function-enter"))
1369  {
1370  status() << "Function enter instrumentation" << eom;
1372  symbol_table,
1374  cmdline.get_value("function-enter"));
1375  }
1376 
1377  if(cmdline.isset("function-exit"))
1378  {
1379  status() << "Function exit instrumentation" << eom;
1380  function_exit(
1381  symbol_table,
1383  cmdline.get_value("function-exit"));
1384  }
1385 
1386  if(cmdline.isset("branch"))
1387  {
1388  status() << "Branch instrumentation" << eom;
1389  branch(
1390  symbol_table,
1392  cmdline.get_value("branch"));
1393  }
1394 
1395  // add failed symbols
1397 
1398  // recalculate numbers, etc.
1400 
1401  // add loop ids
1403 
1404  // label the assertions
1406 
1407  // nondet volatile?
1408  if(cmdline.isset("nondet-volatile"))
1409  {
1410  status() << "Making volatile variables non-deterministic" << eom;
1412  }
1413 
1414  // reachability slice?
1415  if(cmdline.isset("reachability-slice"))
1416  {
1417  status() << "Performing a reachability slice" << eom;
1418  if(cmdline.isset("property"))
1420  else
1422  }
1423 
1424  // full slice?
1425  if(cmdline.isset("full-slice"))
1426  {
1429 
1430  status() << "Performing a full slice" << eom;
1431  if(cmdline.isset("property"))
1433  else
1435  }
1436 
1437  // recalculate numbers, etc.
1439 }
1440 
1443 {
1444  std::cout <<
1445  "\n"
1446  "* * Goto-Instrument " CBMC_VERSION " - Copyright (C) 2008-2013 * *\n" // NOLINT(*)
1447  "* * Daniel Kroening * *\n"
1448  "* * kroening@kroening.com * *\n"
1449  "\n"
1450  "Usage: Purpose:\n"
1451  "\n"
1452  " goto-instrument [-?] [-h] [--help] show help\n"
1453  " goto-instrument in out perform instrumentation\n"
1454  "\n"
1455  "Main options:\n"
1456  " --document-properties-html generate HTML property documentation\n"
1457  " --document-properties-latex generate Latex property documentation\n"
1458  " --dump-c generate C source\n"
1459  " --dump-cpp generate C++ source\n"
1460  " --dot generate CFG graph in DOT format\n"
1461  " --interpreter do concrete execution\n"
1462  " --count-eloc count effective lines of code\n"
1463  " --list-eloc list full path names of lines containing code\n" // NOLINT(*)
1464  "\n"
1465  "Diagnosis:\n"
1466  " --show-loops show the loops in the program\n"
1467  " --show-properties show the properties\n"
1468  " --show-symbol-table show symbol table\n"
1469  " --list-symbols list symbols with type information\n"
1471  " --print-internal-representation\n" // NOLINTNEXTLINE(*)
1472  " show verbose internal representation of the program\n"
1473  " --list-undefined-functions list functions without body\n"
1474  " --show-struct-alignment show struct members that might be concurrently accessed\n" // NOLINT(*)
1475  " --show-natural-loops show natural loop heads\n"
1476  // NOLINTNEXTLINE(whitespace/line_length)
1477  " --list-calls-args list all function calls with their arguments\n"
1478  "\n"
1479  "Safety checks:\n"
1480  " --no-assertions ignore user assertions\n"
1482  " --uninitialized-check add checks for uninitialized locals (experimental)\n" // NOLINT(*)
1483  " --error-label label check that label is unreachable\n"
1484  " --stack-depth n add check that call stack size of non-inlined functions never exceeds n\n" // NOLINT(*)
1485  " --race-check add floating-point data race checks\n"
1486  "\n"
1487  "Semantic transformations:\n"
1488  " --nondet-volatile makes reads from volatile variables non-deterministic\n" // NOLINT(*)
1489  " --unwind <n> unwinds the loops <n> times\n"
1490  " --unwindset L:B,... unwind loop L with a bound of B\n"
1491  " --unwindset-file <file> read unwindset from file\n"
1492  " --partial-loops permit paths with partial loops\n"
1493  " --unwinding-assertions generate unwinding assertions\n"
1494  " --continue-as-loops add loop for remaining iterations after unwound part\n" // NOLINT(*)
1495  " --isr <function> instruments an interrupt service routine\n"
1496  " --mmio instruments memory-mapped I/O\n"
1497  " --nondet-static add nondeterministic initialization of variables with static lifetime\n" // NOLINT(*)
1498  " --check-invariant function instruments invariant checking function\n"
1499  " --remove-pointers converts pointer arithmetic to base+offset expressions\n" // NOLINT(*)
1500  // NOLINTNEXTLINE(whitespace/line_length)
1501  " --undefined-function-is-assume-false\n" // NOLINTNEXTLINE(whitespace/line_length)
1502  " convert each call to an undefined function to assume(false)\n"
1503  "\n"
1504  "Loop transformations:\n"
1505  " --k-induction <k> check loops with k-induction\n"
1506  " --step-case k-induction: do step-case\n"
1507  " --base-case k-induction: do base-case\n"
1508  " --havoc-loops over-approximate all loops\n"
1509  " --accelerate add loop accelerators\n"
1510  " --skip-loops <loop-ids> add gotos to skip selected loops during execution\n" // NOLINT(*)
1511  "\n"
1512  "Memory model instrumentations:\n"
1513  " --mm <tso,pso,rmo,power> instruments a weak memory model\n"
1514  " --scc detects critical cycles per SCC (one thread per SCC)\n" // NOLINT(*)
1515  " --one-event-per-cycle only instruments one event per cycle\n"
1516  " --minimum-interference instruments an optimal number of events\n"
1517  " --my-events only instruments events whose ids appear in inst.evt\n" // NOLINT(*)
1518  " --cfg-kill enables symbolic execution used to reduce spurious cycles\n" // NOLINT(*)
1519  " --no-dependencies no dependency analysis\n"
1520  // NOLINTNEXTLINE(whitespace/line_length)
1521  " --no-po-rendering no representation of the threads in the dot\n"
1522  " --render-cluster-file clusterises the dot by files\n"
1523  " --render-cluster-function clusterises the dot by functions\n"
1524  "\n"
1525  "Slicing:\n"
1526  " --reachability-slice slice away instructions that can't reach assertions\n" // NOLINT(*)
1527  " --full-slice slice away instructions that don't affect assertions\n" // NOLINT(*)
1528  " --property id slice with respect to specific property only\n" // NOLINT(*)
1529  " --slice-global-inits slice away initializations of unused global variables\n" // NOLINT(*)
1530  "\n"
1531  "Further transformations:\n"
1532  " --constant-propagator propagate constants and simplify expressions\n" // NOLINT(*)
1533  " --inline perform full inlining\n"
1534  " --partial-inline perform partial inlining\n"
1535  " --function-inline <function> transitively inline all calls <function> makes\n" // NOLINT(*)
1536  " --no-caching disable caching of intermediate results during transitive function inlining\n" // NOLINT(*)
1537  " --log <file> log in json format which code segments were inlined, use with --function-inline\n" // NOLINT(*)
1538  " --remove-function-pointers replace function pointers by case statement over function calls\n" // NOLINT(*)
1540  " --add-library add models of C library functions\n"
1541  " --model-argc-argv <n> model up to <n> command line arguments\n"
1542  // NOLINTNEXTLINE(whitespace/line_length)
1543  " --remove-function-body <f> remove the implementation of function <f> (may be repeated)\n"
1544  "\n"
1545  "Other options:\n"
1546  " --no-system-headers with --dump-c/--dump-cpp: generate C source expanding libc includes\n" // NOLINT(*)
1547  " --use-all-headers with --dump-c/--dump-cpp: generate C source with all includes\n" // NOLINT(*)
1548  " --version show version and exit\n"
1549  " --xml-ui use XML-formatted output\n"
1550  " --json-ui use JSON-formatted output\n"
1551  "\n";
1552 }
void do_indirect_call_and_rtti_removal(bool force=false)
symbol_tablet symbol_table
Definition: language_ui.h:24
irep_idt name
The unique identifier.
Definition: symbol.h:46
const std::list< std::string > & get_values(const std::string &option) const
Definition: cmdline.cpp:90
Loop Acceleration.
Detection for Uninitialized Local Variables.
mstreamt & result()
Definition: message.h:233
void show_loop_ids(ui_message_handlert::uit ui, const goto_modelt &goto_model)
Definition: loop_ids.cpp:21
struct configt::ansi_ct ansi_c
jsont output_log_json() const
Definition: unwind.h:76
Field-insensitive, location-sensitive bitvector analysis.
void string_abstraction(symbol_tablet &symbol_table, message_handlert &message_handler, goto_programt &dest)
Show Value Sets.
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
Definition: namespace.cpp:139
Function Entering and Exiting.
Over-approximate Concurrency for Threaded Goto Programs.
Skip over selected loops by adding gotos.
Remove function exceptional returns.
Interval Analysis.
Remove initializations of unused global variables.
Initialize command line arguments.
void mutex_init_instrumentation(const symbol_tablet &symbol_table, goto_programt &goto_program, typet lock_type)
Remove Instance-of Operators.
void remove_asm(symbol_tablet &symbol_table, goto_functionst &goto_functions)
removes assembler
Definition: remove_asm.cpp:317
void show_uninitialized(const class symbol_tablet &symbol_table, const goto_functionst &goto_functions, std::ostream &out)
Remove Indirect Function Calls.
std::wstring widen(const char *s)
Definition: unicode.cpp:56
instrumentation_strategyt
Definition: wmm.h:26
Remove Virtual Function (Method) Calls.
void parameter_assignments(symbol_tablet &symbol_table, goto_functionst &goto_functions)
removes returns
void remove_pointers(goto_programt &goto_program, symbol_tablet &symbol_table, value_setst &value_sets)
Command Line Parsing.
Field-Sensitive Program Dependence Analysis, Litvak et al., FSE 2010.
static bool skip_loops(goto_programt &goto_program, const loop_idst &loop_ids, messaget &message)
Definition: skip_loops.cpp:24
mstreamt & status()
Definition: message.h:238
virtual int main()
void remove_unused_functions(goto_functionst &functions, message_handlert &message_handler)
void goto_check(const namespacet &ns, const optionst &options, goto_functionst::goto_functiont &goto_function)
uit get_ui()
Definition: language_ui.h:47
Field-sensitive, location-insensitive points-to analysis.
unsigned unsafe_string2unsigned(const std::string &str, int base)
Definition: string2int.cpp:66
void parse_unwindset(const std::string &us, unwind_sett &unwind_set)
Definition: unwind.cpp:25
Definition: wmm.h:23
Definition: wmm.h:39
Remove function definition.
Definition: json.h:21
void print_struct_alignment_problems(const symbol_tablet &symbol_table, std::ostream &out)
std::list< std::string > defines
Definition: config.h:111
Read Goto Programs.
void undefined_function_abort_path(goto_functionst &goto_functions)
void restore_returns(symbol_tablet &symbol_table, goto_functionst &goto_functions)
restores return statements
void list_undefined_functions(const goto_functionst &goto_functions, const namespacet &ns, std::ostream &os)
Branch Instrumentation.
Function Call Graphs.
Dump C from Goto Program.
std::string get_value(char option) const
Definition: cmdline.cpp:46
void show_properties(const namespacet &ns, const irep_idt &identifier, ui_message_handlert::uit ui, const goto_programt &goto_program)
void code_contracts(symbol_tablet &symbol_table, goto_functionst &goto_functions)
void goto_function_inline(goto_modelt &goto_model, const irep_idt function, message_handlert &message_handler, bool adjust_function, bool caching)
Inline all function calls made from a particular function.
Definition: wmm.h:22
void check_call_sequence(const goto_functionst &goto_functions)
Race Detection for Threaded Goto Programs.
Field-insensitive, location-sensitive bitvector analysis.
virtual void show_symbol_table(bool brief=false)
Stack depth checks.
Memory-mapped I/O Instrumentation for Goto Programs.
void mmio(value_setst &value_sets, const symbol_tablet &symbol_table, goto_programt &goto_program)
Definition: mmio.cpp:36
Interpreter for GOTO Programs.
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
void function_exit(symbol_tablet &symbol_table, goto_functionst &goto_functions, const irep_idt &id)
Definition: function.cpp:108
Pointer Dereferencing.
Definition: wmm.h:30
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
Weak Memory Instrumentation for Threaded Goto Programs.
String Abstraction.
configt config
Definition: config.cpp:21
virtual int doit()
invoke main modules
Remove &#39;asm&#39; statements by compiling into suitable standard code.
void nondet_volatile(symbol_tablet &symbol_table, goto_programt &goto_program)
void remove_exceptions(symbol_tablet &symbol_table, goto_functionst &goto_functions)
removes throws/CATCH-POP/CATCH-PUSH
void concurrency(value_setst &value_sets, class symbol_tablet &symbol_table, goto_functionst &goto_functions)
loop_strategyt
Definition: wmm.h:36
Documentation of Properties.
k-induction
void remove_virtual_functions(const symbol_tablet &symbol_table, goto_functionst &goto_functions)
unwind_strategyt
Definition: unwind.h:30
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...
Set the properties to check.
#define HELP_GOTO_CHECK
Definition: goto_check.h:41
void add_uninitialized_locals_assertions(symbol_tablet &symbol_table, goto_functionst &goto_functions)
Unused function removal.
virtual void output(const namespacet &ns, const goto_functionst &goto_functions, std::ostream &out) const
Definition: ai.cpp:92
bool set(const cmdlinet &cmdline)
Definition: config.cpp:727
void show_natural_loops(const goto_functionst &goto_functions)
bool read_goto_binary(const std::string &filename, goto_modelt &dest, message_handlert &message_handler)
argst args
Definition: cmdline.h:35
virtual bool isset(char option) const
Definition: cmdline.cpp:30
memory_modelt
Definition: wmm.h:17
void remove_functions(symbol_tablet &symbol_table, goto_functionst &goto_functions, 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...
Value Set Propagation.
void remove_instanceof(symbol_tablet &symbol_table, goto_functionst &goto_functions)
See function above.
void check(const namespacet &, const goto_functionst &, bool xml, std::ostream &)
String Abstraction.
void output_xml(std::ostream &out) const
Definition: call_graph.cpp:75
Nondeterministic initialization of certain global scope variables.
void output_dot(std::ostream &out) const
Definition: call_graph.cpp:52
Dump Goto-Program as DOT Graph.
TO_BE_DOCUMENTED.
Definition: namespace.h:62
Function Inlining.
Loop IDs.
void print_path_lengths(const goto_functionst &goto_functions)
Definition: count_eloc.cpp:77
Definition: wmm.h:21
void k_induction(goto_functionst &goto_functions, bool base_case, bool step_case, unsigned k)
void horn_encoding(const goto_functionst &, const namespacet &, std::ostream &out)
bool remove_function_pointers(message_handlert &_message_handler, symbol_tablet &symbol_table, const goto_functionst &goto_functions, goto_programt &goto_program, bool add_safety_assertion, bool only_remove_const_fps)
Field-insensitive, location-sensitive, over-approximative escape analysis.
void output(std::ostream &out, const goto_functiont &goto_function, const namespacet &ns) const
void full_slicer(goto_functionst &goto_functions, const namespacet &ns, slicing_criteriont &criterion)
Volatile Variables.
void dump_cpp(const goto_functionst &src, const bool use_system_headers, const bool use_all_headers, const namespacet &ns, std::ostream &out)
Definition: dump_c.cpp:1656
void count_eloc(const goto_functionst &goto_functions)
Definition: count_eloc.cpp:46
Remove function returns.
void property_slicer(goto_functionst &goto_functions, const namespacet &ns, const std::list< std::string > &properties)
Havoc Loops.
Count effective lines of code.
void instrument(goto_functionst &, const namespacet &)
Loop unwinding.
jsont goto_function_inline_and_log(goto_functionst &goto_functions, const irep_idt function, const namespacet &ns, message_handlert &message_handler, bool adjust_function, bool caching)
#define PARSE_OPTIONS_GOTO_CHECK(cmdline, options)
Definition: goto_check.h:55
void output_dot(std::ostream &out) const
Definition: graph.h:656
void weak_memory(memory_modelt model, value_setst &value_sets, symbol_tablet &symbol_table, goto_functionst &goto_functions, bool SCC, instrumentation_strategyt event_strategy, unsigned unwinding_bound, bool no_cfg_kill, bool no_dependencies, loop_strategyt duplicate_body, unsigned input_max_var, unsigned input_max_po_trans, bool render_po, bool render_file, bool render_function, bool cav11_option, bool hide_internals, message_handlert &message_handler, bool ignore_arrays)
void output(std::ostream &out) const
Definition: call_graph.cpp:67
#define HELP_REMOVE_CONST_FUNCTION_POINTERS
void show_call_sequences(const irep_idt &function, const goto_programt &goto_program, const goto_programt::const_targett start)
void set_from_symbol_table(const symbol_tablet &)
Definition: config.cpp:1091
void reachability_slicer(goto_functionst &goto_functions)
Interrupt Instrumentation for Goto Programs.
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
void branch(symbol_tablet &symbol_table, goto_functionst &goto_functions, const irep_idt &id)
Definition: branch.cpp:19
Range-based reaching definitions analysis (following Field- Sensitive Program Dependence Analysis...
Verify and use annotated invariants and pre/post-conditions.
Show program locations.
static void list_calls_and_arguments(const namespacet &ns, const irep_idt &function, const goto_programt &goto_program)
void document_properties_latex(const goto_functionst &goto_functions, std::ostream &out)
Definition: wmm.h:32
unsigned safe_string2unsigned(const std::string &str, int base)
Definition: string2int.cpp:51
void output(std::ostream &out) const
Definition: points_to.cpp:36
Interval Domain.
typet type
Type of symbol.
Definition: symbol.h:37
void remove_skip(goto_programt &goto_program)
remove unnecessary skip statements
Definition: remove_skip.cpp:71
message_handlert & get_message_handler()
Definition: message.h:127
Goto Programs with Functions.
Definition: wmm.h:19
void list_eloc(const goto_functionst &goto_functions)
Definition: count_eloc.cpp:60
#define HELP_SHOW_GOTO_FUNCTIONS
virtual void help()
display command line help
void goto_inline(goto_modelt &goto_model, message_handlert &message_handler, bool adjust_function)
Definition: goto_inline.cpp:25
Constant propagation.
void havoc_loops(goto_functionst &goto_functions)
Definition: wmm.h:20
Slicing.
Handling of functions without body.
void dump_c(const goto_functionst &src, const bool use_system_headers, const bool use_all_headers, const namespacet &ns, std::ostream &out)
Definition: dump_c.cpp:1644
void interpreter(const symbol_tablet &symbol_table, const goto_functionst &goto_functions)
void remove_returns(symbol_tablet &symbol_table, goto_functionst &goto_functions)
removes returns
void accelerate_functions(goto_functionst &functions, symbol_tablet &symbol_table, bool use_z3)
Definition: accelerate.cpp:652
mstreamt & error()
Definition: message.h:223
void dot(const goto_functionst &src, const namespacet &ns, std::ostream &out)
Definition: dot.cpp:353
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:61
void race_check(value_setst &value_sets, symbol_tablet &symbol_table, goto_programt &goto_program, w_guardst &w_guards)
Definition: race_check.cpp:169
Alignment Checks.
void set_verbosity(unsigned _verbosity)
Definition: message.h:44
void function_enter(symbol_tablet &symbol_table, goto_functionst &goto_functions, const irep_idt &id)
Definition: function.cpp:81
#define CBMC_VERSION
Definition: version.h:4
std::map< irep_idt, std::map< unsigned, int > > unwind_sett
Definition: unwind.h:20
Expression to hold a symbol (variable)
Definition: std_expr.h:82
Horn-clause Encoding.
Show the properties.
void show_locations(ui_message_handlert::uit ui, const irep_idt function_id, const goto_programt &goto_program)
Definition: wmm.h:40
Compute natural loops in a goto_function.
void set_option(const std::string &option, const bool value)
Definition: options.cpp:24
void do_remove_const_function_pointers_only()
Remove function pointers that can be resolved by analysing const variables (i.e.
Memory-mapped I/O Instrumentation for Goto Programs.
void add_failed_symbols(symbol_tablet &symbol_table)
Encoding for Threaded Goto Programs.
bool write_goto_binary(std::ostream &out, const symbol_tablet &lsymbol_table, const goto_functionst &functions, int version)
Writes a goto program to disc.
void show_goto_functions(const namespacet &ns, ui_message_handlert::uit ui, const goto_functionst &goto_functions)
Program Transformation.
#define forall_goto_functions(it, functions)
Field-insensitive, location-sensitive, over-approximative escape analysis.
std::ostream & output_instruction(const class namespacet &ns, const irep_idt &identifier, std::ostream &out, instructionst::const_iterator it) const
See below.
void document_properties_html(const goto_functionst &goto_functions, std::ostream &out)
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:68
void slice_global_inits(const namespacet &ns, goto_functionst &goto_functions)
Add parameter assignments.
void label_properties(goto_modelt &goto_model)
Write GOTO binaries.
void nondet_static(const namespacet &ns, goto_functionst &goto_functions, const irep_idt &fct_name)
void interval_analysis(const namespacet &ns, goto_functionst &goto_functions)
bool model_argc_argv(symbol_tablet &symbol_table, goto_functionst &goto_functions, unsigned max_argc, message_handlert &message_handler)
void show_value_sets(ui_message_handlert::uit ui, const goto_functionst &goto_functions, const value_set_analysist &value_set_analysis)
void thread_exit_instrumentation(goto_programt &goto_program)
Definition: wmm.h:28
Race Detection for Threaded Goto Programs.
Definition: kdev_t.h:19
void stack_depth(goto_programt &goto_program, const symbol_exprt &symbol, const int i_depth, const exprt &max_depth)
Definition: stack_depth.cpp:45