cprover
goto_analyzer_parse_options.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Goto-Analyzer Command Line Option Processing
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
13 
14 #include <cstdlib> // exit()
15 #include <iostream>
16 #include <fstream>
17 #include <memory>
18 
19 #include <ansi-c/ansi_c_language.h>
20 #include <ansi-c/cprover_library.h>
21 
22 #include <assembler/remove_asm.h>
23 
24 #include <cpp/cpp_language.h>
25 #include <cpp/cprover_library.h>
26 
27 #include <jsil/jsil_language.h>
28 
44 
45 #include <analyses/is_threaded.h>
46 #include <analyses/goto_check.h>
51 
52 #include <langapi/mode.h>
53 #include <langapi/language.h>
54 
55 #include <util/config.h>
56 #include <util/exception_utils.h>
57 #include <util/exit_codes.h>
58 #include <util/options.h>
59 #include <util/unicode.h>
60 #include <util/version.h>
61 
62 #include "show_on_source.h"
63 #include "static_show_domain.h"
64 #include "static_simplifier.h"
65 #include "static_verifier.h"
66 #include "taint_analysis.h"
68 
70  int argc,
71  const char **argv)
74  argc,
75  argv,
76  std::string("GOTO-ANALYZER "))
77 {
78 }
79 
81 {
85 }
86 
88 {
89  if(config.set(cmdline))
90  {
91  usage_error();
93  }
94 
95  if(cmdline.isset("function"))
96  options.set_option("function", cmdline.get_value("function"));
97 
98 #if 0
99  if(cmdline.isset("c89"))
101 
102  if(cmdline.isset("c99"))
104 
105  if(cmdline.isset("c11"))
107 
108  if(cmdline.isset("cpp98"))
109  config.cpp.set_cpp98();
110 
111  if(cmdline.isset("cpp03"))
112  config.cpp.set_cpp03();
113 
114  if(cmdline.isset("cpp11"))
115  config.cpp.set_cpp11();
116 #endif
117 
118 #if 0
119  // check assertions
120  if(cmdline.isset("no-assertions"))
121  options.set_option("assertions", false);
122  else
123  options.set_option("assertions", true);
124 
125  // use assumptions
126  if(cmdline.isset("no-assumptions"))
127  options.set_option("assumptions", false);
128  else
129  options.set_option("assumptions", true);
130 
131  // magic error label
132  if(cmdline.isset("error-label"))
133  options.set_option("error-label", cmdline.get_values("error-label"));
134 #endif
135 
136  // The user should either select:
137  // 1. a specific analysis, or
138  // 2. a tuple of task / analyser options / outputs
139 
140  // Select a specific analysis
141  if(cmdline.isset("taint"))
142  {
143  options.set_option("taint", true);
144  options.set_option("specific-analysis", true);
145  }
146  // For backwards compatibility,
147  // these are first recognised as specific analyses
148  bool reachability_task = false;
149  if(cmdline.isset("unreachable-instructions"))
150  {
151  options.set_option("unreachable-instructions", true);
152  options.set_option("specific-analysis", true);
153  reachability_task = true;
154  }
155  if(cmdline.isset("unreachable-functions"))
156  {
157  options.set_option("unreachable-functions", true);
158  options.set_option("specific-analysis", true);
159  reachability_task = true;
160  }
161  if(cmdline.isset("reachable-functions"))
162  {
163  options.set_option("reachable-functions", true);
164  options.set_option("specific-analysis", true);
165  reachability_task = true;
166  }
167  if(cmdline.isset("show-local-may-alias"))
168  {
169  options.set_option("show-local-may-alias", true);
170  options.set_option("specific-analysis", true);
171  }
172 
173  // Output format choice
174  if(cmdline.isset("text"))
175  {
176  options.set_option("text", true);
177  options.set_option("outfile", cmdline.get_value("text"));
178  }
179  else if(cmdline.isset("json"))
180  {
181  options.set_option("json", true);
182  options.set_option("outfile", cmdline.get_value("json"));
183  }
184  else if(cmdline.isset("xml"))
185  {
186  options.set_option("xml", true);
187  options.set_option("outfile", cmdline.get_value("xml"));
188  }
189  else if(cmdline.isset("dot"))
190  {
191  options.set_option("dot", true);
192  options.set_option("outfile", cmdline.get_value("dot"));
193  }
194 
195  // Task options
196  if(cmdline.isset("show"))
197  {
198  options.set_option("show", true);
199  options.set_option("general-analysis", true);
200  }
201  else if(cmdline.isset("show-on-source"))
202  {
203  options.set_option("show-on-source", true);
204  options.set_option("general-analysis", true);
205  }
206  else if(cmdline.isset("verify"))
207  {
208  options.set_option("verify", true);
209  options.set_option("general-analysis", true);
210  }
211  else if(cmdline.isset("simplify"))
212  {
213  if(cmdline.get_value("simplify") == "-")
215  "cannot output goto binary to stdout", "--simplify");
216 
217  options.set_option("simplify", true);
218  options.set_option("outfile", cmdline.get_value("simplify"));
219  options.set_option("general-analysis", true);
220 
221  // For development allow slicing to be disabled in the simplify task
222  options.set_option(
223  "simplify-slicing",
224  !(cmdline.isset("no-simplify-slicing")));
225  }
226  else if(cmdline.isset("show-intervals"))
227  {
228  // For backwards compatibility
229  options.set_option("show", true);
230  options.set_option("general-analysis", true);
231  options.set_option("intervals", true);
232  options.set_option("domain set", true);
233  }
234  else if(cmdline.isset("show-non-null"))
235  {
236  // For backwards compatibility
237  options.set_option("show", true);
238  options.set_option("general-analysis", true);
239  options.set_option("non-null", true);
240  options.set_option("domain set", true);
241  }
242  else if(cmdline.isset("intervals") || cmdline.isset("non-null"))
243  {
244  // Partial backwards compatability, just giving these domains without
245  // a task will work. However it will use the general default of verify
246  // rather than their historical default of show.
247  options.set_option("verify", true);
248  options.set_option("general-analysis", true);
249  }
250 
251  if(options.get_bool_option("general-analysis") || reachability_task)
252  {
253  // Abstract interpreter choice
254  if(cmdline.isset("recursive-interprocedural"))
255  options.set_option("recursive-interprocedural", true);
256  else if(cmdline.isset("legacy-ait") || cmdline.isset("location-sensitive"))
257  {
258  options.set_option("legacy-ait", true);
259  // Fixes a number of other options as well
260  options.set_option("ahistorical", true);
261  options.set_option("history set", true);
262  options.set_option("one-domain-per-location", true);
263  options.set_option("storage set", true);
264  }
265  else if(cmdline.isset("legacy-concurrent") || cmdline.isset("concurrent"))
266  {
267  options.set_option("legacy-concurrent", true);
268  options.set_option("ahistorical", true);
269  options.set_option("history set", true);
270  options.set_option("one-domain-per-location", true);
271  options.set_option("storage set", true);
272  }
273  else
274  {
275  // Silently default to legacy-ait for backwards compatability
276  options.set_option("legacy-ait", true);
277  // Fixes a number of other options as well
278  options.set_option("ahistorical", true);
279  options.set_option("history set", true);
280  options.set_option("one-domain-per-location", true);
281  options.set_option("storage set", true);
282  }
283 
284  // History choice
285  if(cmdline.isset("ahistorical"))
286  {
287  options.set_option("ahistorical", true);
288  options.set_option("history set", true);
289  }
290  else if(cmdline.isset("call-stack"))
291  {
292  options.set_option("call-stack", true);
293  options.set_option(
294  "call-stack-recursion-limit", cmdline.get_value("call-stack"));
295  options.set_option("history set", true);
296  }
297 
298  if(!options.get_bool_option("history set"))
299  {
300  // Default to ahistorical as it is the expected for of analysis
301  log.status() << "History not specified, defaulting to --ahistorical"
302  << messaget::eom;
303  options.set_option("ahistorical", true);
304  options.set_option("history set", true);
305  }
306 
307  // Domain choice
308  if(cmdline.isset("constants"))
309  {
310  options.set_option("constants", true);
311  options.set_option("domain set", true);
312  }
313  else if(cmdline.isset("dependence-graph"))
314  {
315  options.set_option("dependence-graph", true);
316  options.set_option("domain set", true);
317  }
318  else if(cmdline.isset("intervals"))
319  {
320  options.set_option("intervals", true);
321  options.set_option("domain set", true);
322  }
323  else if(cmdline.isset("non-null"))
324  {
325  options.set_option("non-null", true);
326  options.set_option("domain set", true);
327  }
328 
329  // Reachability questions, when given with a domain swap from specific
330  // to general tasks so that they can use the domain & parameterisations.
331  if(reachability_task)
332  {
333  if(options.get_bool_option("domain set"))
334  {
335  options.set_option("specific-analysis", false);
336  options.set_option("general-analysis", true);
337  }
338  }
339  else
340  {
341  if(!options.get_bool_option("domain set"))
342  {
343  // Default to constants as it is light-weight but useful
344  log.status() << "Domain not specified, defaulting to --constants"
345  << messaget::eom;
346  options.set_option("constants", true);
347  }
348  }
349  }
350 
351  // Storage choice
352  if(cmdline.isset("one-domain-per-history"))
353  {
354  options.set_option("one-domain-per-history", true);
355  options.set_option("storage set", true);
356  }
357  else if(cmdline.isset("one-domain-per-location"))
358  {
359  options.set_option("one-domain-per-location", true);
360  options.set_option("storage set", true);
361  }
362 
363  if(!options.get_bool_option("storage set"))
364  {
365  // one-domain-per-location and one-domain-per-history are effectively
366  // the same when using ahistorical so we default to per-history so that
367  // more sophisticated history objects work as expected
368  log.status() << "Storage not specified,"
369  << " defaulting to --one-domain-per-history" << messaget::eom;
370  options.set_option("one-domain-per-history", true);
371  options.set_option("storage set", true);
372  }
373 
374  if(cmdline.isset("validate-goto-model"))
375  {
376  options.set_option("validate-goto-model", true);
377  }
378 }
379 
384  const optionst &options,
385  const namespacet &ns)
386 {
387  // These support all of the option categories
388  if(options.get_bool_option("recursive-interprocedural"))
389  {
390  // Build the history factory
391  std::unique_ptr<ai_history_factory_baset> hf = nullptr;
392  if(options.get_bool_option("ahistorical"))
393  {
394  hf = util_make_unique<
396  }
397  else if(options.get_bool_option("call-stack"))
398  {
399  hf = util_make_unique<call_stack_history_factoryt>(
400  options.get_unsigned_int_option("call-stack-recursion-limit"));
401  }
402 
403  // Build the domain factory
404  std::unique_ptr<ai_domain_factory_baset> df = nullptr;
405  if(options.get_bool_option("constants"))
406  {
407  df = util_make_unique<
409  }
410  else if(options.get_bool_option("intervals"))
411  {
412  df = util_make_unique<
414  }
415  // non-null is not fully supported, despite the historical options
416  // dependency-graph is quite heavily tied to the legacy-ait infrastructure
417 
418  // Build the storage object
419  std::unique_ptr<ai_storage_baset> st = nullptr;
420  if(options.get_bool_option("one-domain-per-history"))
421  {
422  st = util_make_unique<history_sensitive_storaget>();
423  }
424  else if(options.get_bool_option("one-domain-per-location"))
425  {
426  st = util_make_unique<location_sensitive_storaget>();
427  }
428 
429  // Only try to build the abstract interpreter if all the parts have been
430  // correctly specified and configured
431  if(hf != nullptr && df != nullptr && st != nullptr)
432  {
433  if(options.get_bool_option("recursive-interprocedural"))
434  {
436  std::move(hf), std::move(df), std::move(st));
437  }
438  UNREACHABLE;
439  }
440  }
441  else if(options.get_bool_option("legacy-ait"))
442  {
443  if(options.get_bool_option("constants"))
444  {
445  // constant_propagator_ait derives from ait<constant_propagator_domaint>
447  }
448  else if(options.get_bool_option("dependence-graph"))
449  {
450  return new dependence_grapht(ns);
451  }
452  else if(options.get_bool_option("intervals"))
453  {
454  return new ait<interval_domaint>();
455  }
456 #if 0
457  // Not actually implemented, despite the option...
458  else if(options.get_bool_option("non-null"))
459  {
460  return new ait<non_null_domaint>();
461  }
462 #endif
463  }
464  else if(options.get_bool_option("legacy-concurrent"))
465  {
466 #if 0
467  // Very few domains can work with this interpreter
468  // as it requires that changes to the domain are
469  // 'non-revertable' and it has merge shared
470  if(options.get_bool_option("dependence-graph"))
471  {
472  return new dependence_grapht(ns);
473  }
474 #endif
475  }
476 
477  // Construction failed due to configuration errors
478  return nullptr;
479 }
480 
483 {
484  if(cmdline.isset("version"))
485  {
486  std::cout << CBMC_VERSION << '\n';
487  return CPROVER_EXIT_SUCCESS;
488  }
489 
490  //
491  // command line options
492  //
493 
494  optionst options;
495  get_command_line_options(options);
498 
499  //
500  // Print a banner
501  //
502  log.status() << "GOTO-ANALYSER version " << CBMC_VERSION << " "
503  << sizeof(void *) * 8 << "-bit " << config.this_architecture()
505 
507 
509 
510  if(process_goto_program(options))
512 
513  if(cmdline.isset("validate-goto-model"))
514  {
516  }
517 
518  // show it?
519  if(cmdline.isset("show-symbol-table"))
520  {
522  return CPROVER_EXIT_SUCCESS;
523  }
524 
525  // show it?
526  if(
527  cmdline.isset("show-goto-functions") ||
528  cmdline.isset("list-goto-functions"))
529  {
531  goto_model, ui_message_handler, cmdline.isset("list-goto-functions"));
532  return CPROVER_EXIT_SUCCESS;
533  }
534 
535  return perform_analysis(options);
536 }
537 
538 
541 {
543  if(options.get_bool_option("taint"))
544  {
545  std::string taint_file=cmdline.get_value("taint");
546 
547  if(cmdline.isset("show-taint"))
548  {
549  taint_analysis(goto_model, taint_file, ui_message_handler, true);
550  return CPROVER_EXIT_SUCCESS;
551  }
552  else
553  {
554  std::string json_file=cmdline.get_value("json");
555  bool result = taint_analysis(
556  goto_model, taint_file, ui_message_handler, false, json_file);
558  }
559  }
560 
561  // If no domain is given, this lightweight version of the analysis is used.
562  if(options.get_bool_option("unreachable-instructions") &&
563  options.get_bool_option("specific-analysis"))
564  {
565  const std::string json_file=cmdline.get_value("json");
566 
567  if(json_file.empty())
568  unreachable_instructions(goto_model, false, std::cout);
569  else if(json_file=="-")
570  unreachable_instructions(goto_model, true, std::cout);
571  else
572  {
573  std::ofstream ofs(json_file);
574  if(!ofs)
575  {
576  log.error() << "Failed to open json output '" << json_file << "'"
577  << messaget::eom;
579  }
580 
582  }
583 
584  return CPROVER_EXIT_SUCCESS;
585  }
586 
587  if(options.get_bool_option("unreachable-functions") &&
588  options.get_bool_option("specific-analysis"))
589  {
590  const std::string json_file=cmdline.get_value("json");
591 
592  if(json_file.empty())
593  unreachable_functions(goto_model, false, std::cout);
594  else if(json_file=="-")
595  unreachable_functions(goto_model, true, std::cout);
596  else
597  {
598  std::ofstream ofs(json_file);
599  if(!ofs)
600  {
601  log.error() << "Failed to open json output '" << json_file << "'"
602  << messaget::eom;
604  }
605 
606  unreachable_functions(goto_model, true, ofs);
607  }
608 
609  return CPROVER_EXIT_SUCCESS;
610  }
611 
612  if(options.get_bool_option("reachable-functions") &&
613  options.get_bool_option("specific-analysis"))
614  {
615  const std::string json_file=cmdline.get_value("json");
616 
617  if(json_file.empty())
618  reachable_functions(goto_model, false, std::cout);
619  else if(json_file=="-")
620  reachable_functions(goto_model, true, std::cout);
621  else
622  {
623  std::ofstream ofs(json_file);
624  if(!ofs)
625  {
626  log.error() << "Failed to open json output '" << json_file << "'"
627  << messaget::eom;
629  }
630 
631  reachable_functions(goto_model, true, ofs);
632  }
633 
634  return CPROVER_EXIT_SUCCESS;
635  }
636 
637  if(options.get_bool_option("show-local-may-alias"))
638  {
640 
642  {
643  std::cout << ">>>>\n";
644  std::cout << ">>>> " << it->first << '\n';
645  std::cout << ">>>>\n";
646  local_may_aliast local_may_alias(it->second);
647  local_may_alias.output(std::cout, it->second, ns);
648  std::cout << '\n';
649  }
650 
651  return CPROVER_EXIT_SUCCESS;
652  }
653 
655 
656  if(cmdline.isset("show-properties"))
657  {
659  return CPROVER_EXIT_SUCCESS;
660  }
661 
662  if(cmdline.isset("property"))
664 
665  if(options.get_bool_option("general-analysis"))
666  {
667  // Output file factory
668  const std::string outfile=options.get_option("outfile");
669 
670  std::ofstream output_stream;
671  if(outfile != "-" && !outfile.empty())
672  output_stream.open(outfile);
673 
674  std::ostream &out(
675  (outfile == "-" || outfile.empty()) ? std::cout : output_stream);
676 
677  if(!out)
678  {
679  log.error() << "Failed to open output file '" << outfile << "'"
680  << messaget::eom;
682  }
683 
684  // Build analyzer
685  log.status() << "Selecting abstract domain" << messaget::eom;
686  namespacet ns(goto_model.symbol_table); // Must live as long as the domain.
687  std::unique_ptr<ai_baset> analyzer(build_analyzer(options, ns));
688 
689  if(analyzer == nullptr)
690  {
691  log.status() << "Task / Interpreter combination not supported"
692  << messaget::eom;
694  }
695 
696  // Run
697  log.status() << "Computing abstract states" << messaget::eom;
698  (*analyzer)(goto_model);
699 
700  // Perform the task
701  log.status() << "Performing task" << messaget::eom;
702 
703  bool result = true;
704 
705  if(options.get_bool_option("show"))
706  {
707  static_show_domain(goto_model, *analyzer, options, out);
708  return CPROVER_EXIT_SUCCESS;
709  }
710  else if(options.get_bool_option("show-on-source"))
711  {
713  return CPROVER_EXIT_SUCCESS;
714  }
715  else if(options.get_bool_option("verify"))
716  {
717  result = static_verifier(
718  goto_model, *analyzer, options, ui_message_handler, out);
719  }
720  else if(options.get_bool_option("simplify"))
721  {
722  PRECONDITION(!outfile.empty() && outfile != "-");
723  output_stream.close();
724  output_stream.open(outfile, std::ios::binary);
725  result = static_simplifier(
726  goto_model, *analyzer, options, ui_message_handler, out);
727  }
728  else if(options.get_bool_option("unreachable-instructions"))
729  {
731  *analyzer,
732  options,
733  out);
734  }
735  else if(options.get_bool_option("unreachable-functions"))
736  {
738  *analyzer,
739  options,
740  out);
741  }
742  else if(options.get_bool_option("reachable-functions"))
743  {
745  *analyzer,
746  options,
747  out);
748  }
749  else
750  {
751  log.error() << "Unhandled task" << messaget::eom;
753  }
754 
755  return result ?
757  }
758 
759 
760  // Final defensive error case
761  log.error() << "no analysis option given -- consider reading --help"
762  << messaget::eom;
764 }
765 
767  const optionst &options)
768 {
769  {
770  #if 0
771  // Remove inline assembler; this needs to happen before
772  // adding the library.
774 
775  // add the library
776  log.status() << "Adding CPROVER library (" << config.ansi_c.arch << ")" << messaget::eom;
780  #endif
781 
782  // remove function pointers
783  log.status() << "Removing function pointers and virtual functions"
784  << messaget::eom;
786  ui_message_handler, goto_model, cmdline.isset("pointer-check"));
787 
788  // do partial inlining
789  log.status() << "Partial Inlining" << messaget::eom;
791 
792  // remove returns, gcc vectors, complex
796 
797 #if 0
798  // add generic checks
799  log.status() << "Generic Property Instrumentation" << messaget::eom;
800  goto_check(options, goto_model);
801 #else
802  (void)options; // unused parameter
803 #endif
804 
805  // recalculate numbers, etc.
807 
808  // add loop ids
810  }
811  return false;
812 }
813 
816 {
817  // clang-format off
818  std::cout << '\n' << banner_string("GOTO-ANALYZER", CBMC_VERSION) << '\n'
819  << align_center_with_border("Copyright (C) 2017-2018") << '\n'
820  << align_center_with_border("Daniel Kroening, Diffblue") << '\n'
821  << align_center_with_border("kroening@kroening.com") << '\n'
822  <<
823  "\n"
824  "Usage: Purpose:\n"
825  "\n"
826  " goto-analyzer [-h] [--help] show help\n"
827  " goto-analyzer file.c ... source file names\n"
828  "\n"
829  "Task options:\n"
830  " --show display the abstract states on the goto program\n" // NOLINT(*)
831  " --show-on-source display the abstract states on the source\n"
832  // NOLINTNEXTLINE(whitespace/line_length)
833  " --verify use the abstract domains to check assertions\n"
834  // NOLINTNEXTLINE(whitespace/line_length)
835  " --simplify file_name use the abstract domains to simplify the program\n"
836  " --unreachable-instructions list dead code\n"
837  // NOLINTNEXTLINE(whitespace/line_length)
838  " --unreachable-functions list functions unreachable from the entry point\n"
839  // NOLINTNEXTLINE(whitespace/line_length)
840  " --reachable-functions list functions reachable from the entry point\n"
841  "\n"
842  "Abstract interpreter options:\n"
843  // NOLINTNEXTLINE(whitespace/line_length)
844  " --recursive-interprocedural use recursion to handle interprocedural reasoning\n"
845  // NOLINTNEXTLINE(whitespace/line_length)
846  " --legacy-ait recursion for function and one domain per location\n"
847  // NOLINTNEXTLINE(whitespace/line_length)
848  " --legacy-concurrent legacy-ait with an extended fixed-point for concurrency\n"
849  "\n"
850  "History options:\n"
851  // NOLINTNEXTLINE(whitespace/line_length)
852  " --ahistorical the most basic history, tracks locations only\n"
853  // NOLINTNEXTLINE(whitespace/line_length)
854  " --call-stack n track the calling location stack for each function\n"
855  // NOLINTNEXTLINE(whitespace/line_length)
856  " limiting to at most n recursive loops, 0 to disable\n"
857  "\n"
858  "Domain options:\n"
859  " --constants a constant for each variable if possible\n"
860  " --intervals an interval for each variable\n"
861  " --non-null tracks which pointers are non-null\n"
862  " --dependence-graph data and control dependencies between instructions\n" // NOLINT(*)
863  "\n"
864  "Storage options:\n"
865  // NOLINTNEXTLINE(whitespace/line_length)
866  " --one-domain-per-history stores a domain for each history object created\n"
867  " --one-domain-per-location stores a domain for each location reached\n"
868  "\n"
869  "Output options:\n"
870  " --text file_name output results in plain text to given file\n"
871  // NOLINTNEXTLINE(whitespace/line_length)
872  " --json file_name output results in JSON format to given file\n"
873  " --xml file_name output results in XML format to given file\n"
874  " --dot file_name output results in DOT format to given file\n"
875  "\n"
876  "Specific analyses:\n"
877  // NOLINTNEXTLINE(whitespace/line_length)
878  " --taint file_name perform taint analysis using rules in given file\n"
879  "\n"
880  "C/C++ frontend options:\n"
881  " -I path set include path (C/C++)\n"
882  " -D macro define preprocessor macro (C/C++)\n"
883  " --arch X set architecture (default: "
884  << configt::this_architecture() << ")\n"
885  " --os set operating system (default: "
886  << configt::this_operating_system() << ")\n"
887  " --c89/99/11 set C language standard (default: "
894  "c11":"") << ")\n"
895  " --cpp98/03/11 set C++ language standard (default: "
898  "cpp98":
901  "cpp03":
904  "cpp11":"") << ")\n"
905  #ifdef _WIN32
906  " --gcc use GCC as preprocessor\n"
907  #endif
908  " --no-library disable built-in abstract C library\n"
910  "\n"
911  "Program representations:\n"
912  " --show-parse-tree show parse tree\n"
913  " --show-symbol-table show loaded symbol table\n"
916  "\n"
917  "Program instrumentation options:\n"
919  "\n"
920  "Other options:\n"
922  " --version show version and exit\n"
923  HELP_FLUSH
925  "\n";
926  // clang-format on
927 }
cprover_library.h
cmdlinet::args
argst args
Definition: cmdline.h:85
CBMC_VERSION
const char * CBMC_VERSION
Definition: version.cpp:1
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
ai_domain_factory_default_constructort
Definition: ai_domain.h:243
exception_utils.h
configt::cppt::cpp_standardt::CPP98
@ CPP98
HELP_SHOW_GOTO_FUNCTIONS
#define HELP_SHOW_GOTO_FUNCTIONS
Definition: show_goto_functions.h:26
local_may_aliast::output
void output(std::ostream &out, const goto_functiont &goto_function, const namespacet &ns) const
Definition: local_may_alias.cpp:469
configt::ansi_ct::set_c99
void set_c99()
Definition: config.h:53
parse_options_baset::ui_message_handler
ui_message_handlert ui_message_handler
Definition: parse_options.h:42
CPROVER_EXIT_VERIFICATION_UNSAFE
#define CPROVER_EXIT_VERIFICATION_UNSAFE
Verification successful indicates the analysis has been performed without error AND the software is n...
Definition: exit_codes.h:25
parse_options_baset
Definition: parse_options.h:20
cmdlinet::isset
virtual bool isset(char option) const
Definition: cmdline.cpp:28
dependence_grapht
Definition: dependence_graph.h:217
static_unreachable_instructions
bool static_unreachable_instructions(const goto_modelt &goto_model, const ai_baset &ai, const optionst &options, std::ostream &out)
Definition: unreachable_instructions.cpp:198
goto_inline.h
optionst
Definition: options.h:23
static_simplifier.h
static_verifier
void static_verifier(const abstract_goto_modelt &abstract_goto_model, const ai_baset &ai, propertiest &properties)
Use the information from the abstract interpreter to fill out the statuses of the passed properties.
Definition: static_verifier.cpp:30
goto_analyzer_parse_optionst::get_command_line_options
virtual void get_command_line_options(optionst &options)
Definition: goto_analyzer_parse_options.cpp:87
ai_recursive_interproceduralt
Definition: ai.h:519
static_simplifier
bool static_simplifier(goto_modelt &goto_model, const ai_baset &ai, const optionst &options, message_handlert &message_handler, std::ostream &out)
Simplifies the program using the information in the abstract domain.
Definition: static_simplifier.cpp:29
optionst::get_option
const std::string get_option(const std::string &option) const
Definition: options.cpp:67
messaget::M_STATISTICS
@ M_STATISTICS
Definition: message.h:168
messaget::status
mstreamt & status() const
Definition: message.h:400
show_properties
void show_properties(const namespacet &ns, const irep_idt &identifier, message_handlert &message_handler, ui_message_handlert::uit ui, const goto_programt &goto_program)
Definition: show_properties.cpp:47
HELP_FUNCTIONS
#define HELP_FUNCTIONS
Definition: rebuild_goto_start_function.h:27
static_verifier.h
goto_partial_inline
void goto_partial_inline(goto_modelt &goto_model, message_handlert &message_handler, unsigned smallfunc_limit, bool adjust_function)
Inline all function calls to functions either marked as "inlined" or smaller than smallfunc_limit (by...
Definition: goto_inline.cpp:108
goto_analyzer_parse_options.h
configt::cppt::cpp_standardt::CPP03
@ CPP03
taint_analysis.h
remove_virtual_functions.h
remove_asm.h
constant_propagator.h
jsil_language.h
ait
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition: ai.h:553
mode.h
options.h
CPROVER_EXIT_VERIFICATION_SAFE
#define CPROVER_EXIT_VERIFICATION_SAFE
Verification successful indicates the analysis has been performed without error AND the software is s...
Definition: exit_codes.h:21
goto_check
void goto_check(const irep_idt &function_identifier, goto_functionst::goto_functiont &goto_function, const namespacet &ns, const optionst &options)
Definition: goto_check.cpp:2143
optionst::set_option
void set_option(const std::string &option, const bool value)
Definition: options.cpp:28
messaget::eom
static eomt eom
Definition: message.h:283
show_symbol_table
void show_symbol_table(const symbol_tablet &symbol_table, ui_message_handlert &ui)
Definition: show_symbol_table.cpp:268
configt::ansi_c
struct configt::ansi_ct ansi_c
version.h
goto_analyzer_parse_optionst::build_analyzer
ai_baset * build_analyzer(const optionst &, const namespacet &ns)
For the task, build the appropriate kind of analyzer Ideally this should be a pure function of option...
Definition: goto_analyzer_parse_options.cpp:383
goto_analyzer_parse_optionst::goto_analyzer_parse_optionst
goto_analyzer_parse_optionst(int argc, const char **argv)
Definition: goto_analyzer_parse_options.cpp:69
local_may_aliast
Definition: local_may_alias.h:26
label_properties
void label_properties(goto_modelt &goto_model)
Definition: set_properties.cpp:43
validate_goto_model.h
parse_options_baset::usage_error
virtual void usage_error()
Definition: parse_options.cpp:45
new_cpp_language
std::unique_ptr< languaget > new_cpp_language()
Definition: cpp_language.cpp:201
reachable_functions
void reachable_functions(const goto_modelt &goto_model, const bool json, std::ostream &os)
Definition: unreachable_instructions.cpp:387
remove_vector
static void remove_vector(typet &)
removes vector data type
Definition: remove_vector.cpp:166
configt::cppt::set_cpp98
void set_cpp98()
Definition: config.h:141
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
util_make_unique
std::unique_ptr< T > util_make_unique(Ts &&... ts)
Definition: make_unique.h:19
remove_complex.h
set_properties.h
configt::ansi_ct::c_standardt::C89
@ C89
unreachable_functions
void unreachable_functions(const goto_modelt &goto_model, const bool json, std::ostream &os)
Definition: unreachable_instructions.cpp:373
messaget::error
mstreamt & error() const
Definition: message.h:385
goto_analyzer_parse_optionst::process_goto_program
virtual bool process_goto_program(const optionst &options)
Definition: goto_analyzer_parse_options.cpp:766
initialize_goto_model.h
banner_string
std::string banner_string(const std::string &front_end, const std::string &version)
Definition: parse_options.cpp:146
local_may_alias.h
ai_history_factory_default_constructort
An easy factory implementation for histories that don't need parameters.
Definition: ai_history.h:329
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
show_properties.h
is_threaded.h
configt::cppt::set_cpp11
void set_cpp11()
Definition: config.h:143
cmdlinet::get_value
std::string get_value(char option) const
Definition: cmdline.cpp:46
show_symbol_table.h
goto_analyzer_parse_optionst::doit
virtual int doit() override
invoke main modules
Definition: goto_analyzer_parse_options.cpp:482
language.h
unreachable_instructions.h
HELP_SHOW_PROPERTIES
#define HELP_SHOW_PROPERTIES
Definition: show_properties.h:29
configt::this_operating_system
static irep_idt this_operating_system()
Definition: config.cpp:1375
configt::ansi_ct::arch
irep_idt arch
Definition: config.h:85
show_goto_functions
void show_goto_functions(const namespacet &ns, ui_message_handlert &ui_message_handler, const goto_functionst &goto_functions, bool list_only)
Definition: show_goto_functions.cpp:26
static_show_domain
void static_show_domain(const goto_modelt &goto_model, const ai_baset &ai, const optionst &options, std::ostream &out)
Runs the analyzer and then prints out the domain.
Definition: static_show_domain.cpp:20
goto_analyzer_parse_optionst::help
virtual void help() override
display command line help
Definition: goto_analyzer_parse_options.cpp:815
goto_check.h
goto_functionst::compute_loop_numbers
void compute_loop_numbers()
Definition: goto_functions.cpp:52
read_goto_binary.h
GOTO_ANALYSER_OPTIONS
#define GOTO_ANALYSER_OPTIONS
Definition: goto_analyzer_parse_options.h:143
unreachable_instructions
static void unreachable_instructions(const goto_programt &goto_program, dead_mapt &dest)
Definition: unreachable_instructions.cpp:28
optionst::get_unsigned_int_option
unsigned int get_unsigned_int_option(const std::string &option) const
Definition: options.cpp:56
configt::ansi_ct::default_c_standard
static c_standardt default_c_standard()
Definition: config.cpp:675
remove_vector.h
remove_complex
static void remove_complex(typet &)
removes complex data type
Definition: remove_complex.cpp:231
remove_returns.h
config
configt config
Definition: config.cpp:24
configt::ansi_ct::c_standardt::C99
@ C99
goto_analyzer_parse_optionst::register_languages
virtual void register_languages()
Definition: goto_analyzer_parse_options.cpp:80
parse_options_baset::log
messaget log
Definition: parse_options.h:43
configt::ansi_ct::set_c11
void set_c11()
Definition: config.h:54
configt::this_architecture
static irep_idt this_architecture()
Definition: config.cpp:1275
configt::ansi_ct::c_standardt::C11
@ C11
interval_domain.h
configt::ansi_ct::set_c89
void set_c89()
Definition: config.h:52
register_language
void register_language(language_factoryt factory)
Register a language Note: registering a language is required for using the functions in language_util...
Definition: mode.cpp:38
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
static_reachable_functions
bool static_reachable_functions(const goto_modelt &goto_model, const ai_baset &ai, const optionst &options, std::ostream &out)
Definition: unreachable_instructions.cpp:435
ansi_c_language.h
HELP_GOTO_CHECK
#define HELP_GOTO_CHECK
Definition: goto_check.h:44
cprover_c_library_factory
void cprover_c_library_factory(const std::set< irep_idt > &functions, symbol_tablet &symbol_table, message_handlert &message_handler)
Definition: cprover_library.cpp:77
configt::set
bool set(const cmdlinet &cmdline)
Definition: config.cpp:768
configt::cppt::default_cpp_standard
static cpp_standardt default_cpp_standard()
Definition: config.cpp:690
exit_codes.h
optionst::get_bool_option
bool get_bool_option(const std::string &option) const
Definition: options.cpp:44
taint_analysis
bool taint_analysis(goto_modelt &goto_model, const std::string &taint_file_name, message_handlert &message_handler, bool show_full, const optionalt< std::string > &json_file_name)
Definition: taint_analysis.cpp:416
constant_propagator_ait
Definition: constant_propagator.h:171
show_on_source.h
remove_returns
void remove_returns(symbol_table_baset &symbol_table, goto_functionst &goto_functions)
removes returns
Definition: remove_returns.cpp:256
ai_baset
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:119
new_ansi_c_language
std::unique_ptr< languaget > new_ansi_c_language()
Definition: ansi_c_language.cpp:143
CPROVER_EXIT_USAGE_ERROR
#define CPROVER_EXIT_USAGE_ERROR
A usage error is returned when the command line is invalid or conflicting.
Definition: exit_codes.h:33
goto_functionst::update
void update()
Definition: goto_functions.h:81
binary
static std::string binary(const constant_exprt &src)
Definition: json_expr.cpp:204
remove_asm
void remove_asm(goto_functionst &goto_functions, symbol_tablet &symbol_table)
Replaces inline assembly instructions in the goto program (i.e., instructions of kind OTHER with a co...
Definition: remove_asm.cpp:512
unicode.h
config.h
goto_modelt::validate
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
forall_goto_functions
#define forall_goto_functions(it, functions)
Definition: goto_functions.h:122
adjust_float_expressions
void adjust_float_expressions(exprt &expr, const exprt &rounding_mode)
Replaces arithmetic operations and typecasts involving floating point numbers with their equivalent f...
Definition: adjust_float_expressions.cpp:78
configt::cppt::cpp_standardt::CPP11
@ CPP11
CPROVER_EXIT_INTERNAL_ERROR
#define CPROVER_EXIT_INTERNAL_ERROR
An error has been encountered during processing the requested analysis.
Definition: exit_codes.h:45
initialize_goto_model
goto_modelt initialize_goto_model(const std::vector< std::string > &files, message_handlert &message_handler, const optionst &options)
Definition: initialize_goto_model.cpp:59
goto_convert_functions.h
static_unreachable_functions
bool static_unreachable_functions(const goto_modelt &goto_model, const ai_baset &ai, const optionst &options, std::ostream &out)
Definition: unreachable_instructions.cpp:421
configt::cpp
struct configt::cppt cpp
CPROVER_EXIT_SUCCESS
#define CPROVER_EXIT_SUCCESS
Success indicates the required analysis has been performed without error.
Definition: exit_codes.h:16
show_on_source
void show_on_source(const std::string &source_file, const goto_modelt &goto_model, const ai_baset &ai, message_handlert &message_handler)
output source code annotated with abstract states for given file
Definition: show_on_source.cpp:69
messaget::eval_verbosity
static unsigned eval_verbosity(const std::string &user_input, const message_levelt default_verbosity, message_handlert &dest)
Parse a (user-)provided string as a verbosity level and set it as the verbosity of dest.
Definition: message.cpp:99
goto_analyzer_parse_optionst::goto_model
goto_modelt goto_model
Definition: goto_analyzer_parse_options.h:181
adjust_float_expressions.h
remove_function_pointers
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)
Definition: remove_function_pointers.cpp:519
invalid_command_line_argument_exceptiont
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
Definition: exception_utils.h:38
cmdlinet::get_values
const std::list< std::string > & get_values(const std::string &option) const
Definition: cmdline.cpp:107
remove_function_pointers.h
parse_options_baset::cmdline
cmdlinet cmdline
Definition: parse_options.h:28
set_properties
void set_properties(goto_programt &goto_program, std::unordered_set< irep_idt > &property_set)
Definition: set_properties.cpp:19
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
align_center_with_border
std::string align_center_with_border(const std::string &text)
Utility for displaying help centered messages borderered by "* *".
Definition: parse_options.cpp:133
goto_analyzer_parse_optionst::perform_analysis
virtual int perform_analysis(const optionst &options)
Depending on the command line mode, run one of the analysis tasks.
Definition: goto_analyzer_parse_options.cpp:540
cprover_library.h
static_show_domain.h
dependence_graph.h
HELP_TIMESTAMP
#define HELP_TIMESTAMP
Definition: timestamper.h:14
HELP_FLUSH
#define HELP_FLUSH
Definition: ui_message.h:105
configt::cppt::set_cpp03
void set_cpp03()
Definition: config.h:142
cprover_cpp_library_factory
void cprover_cpp_library_factory(const std::set< irep_idt > &functions, symbol_tablet &symbol_table, message_handlert &message_handler)
Definition: cprover_library.cpp:38
new_jsil_language
std::unique_ptr< languaget > new_jsil_language()
Definition: jsil_language.cpp:102
HELP_VALIDATE
#define HELP_VALIDATE
Definition: validation_interface.h:16
cpp_language.h