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 
45 
49 #include <analyses/goto_check.h>
51 #include <analyses/is_threaded.h>
54 
55 #include <langapi/mode.h>
56 #include <langapi/language.h>
57 
58 #include <util/config.h>
59 #include <util/exception_utils.h>
60 #include <util/exit_codes.h>
61 #include <util/options.h>
62 #include <util/unicode.h>
63 #include <util/version.h>
64 
65 #include "show_on_source.h"
66 #include "static_show_domain.h"
67 #include "static_simplifier.h"
68 #include "static_verifier.h"
69 #include "taint_analysis.h"
71 
73  int argc,
74  const char **argv)
77  argc,
78  argv,
79  std::string("GOTO-ANALYZER "))
80 {
81 }
82 
84 {
88 }
89 
91 {
92  if(config.set(cmdline))
93  {
94  usage_error();
96  }
97 
98  if(cmdline.isset("function"))
99  options.set_option("function", cmdline.get_value("function"));
100 
101 #if 0
102  if(cmdline.isset("c89"))
104 
105  if(cmdline.isset("c99"))
107 
108  if(cmdline.isset("c11"))
110 
111  if(cmdline.isset("cpp98"))
112  config.cpp.set_cpp98();
113 
114  if(cmdline.isset("cpp03"))
115  config.cpp.set_cpp03();
116 
117  if(cmdline.isset("cpp11"))
118  config.cpp.set_cpp11();
119 #endif
120 
121 #if 0
122  // check assertions
123  if(cmdline.isset("no-assertions"))
124  options.set_option("assertions", false);
125  else
126  options.set_option("assertions", true);
127 
128  // use assumptions
129  if(cmdline.isset("no-assumptions"))
130  options.set_option("assumptions", false);
131  else
132  options.set_option("assumptions", true);
133 
134  // magic error label
135  if(cmdline.isset("error-label"))
136  options.set_option("error-label", cmdline.get_values("error-label"));
137 #endif
138 
139  // The user should either select:
140  // 1. a specific analysis, or
141  // 2. a tuple of task / analyser options / outputs
142 
143  // Select a specific analysis
144  if(cmdline.isset("taint"))
145  {
146  options.set_option("taint", true);
147  options.set_option("specific-analysis", true);
148  }
149  // For backwards compatibility,
150  // these are first recognised as specific analyses
151  bool reachability_task = false;
152  if(cmdline.isset("unreachable-instructions"))
153  {
154  options.set_option("unreachable-instructions", true);
155  options.set_option("specific-analysis", true);
156  reachability_task = true;
157  }
158  if(cmdline.isset("unreachable-functions"))
159  {
160  options.set_option("unreachable-functions", true);
161  options.set_option("specific-analysis", true);
162  reachability_task = true;
163  }
164  if(cmdline.isset("reachable-functions"))
165  {
166  options.set_option("reachable-functions", true);
167  options.set_option("specific-analysis", true);
168  reachability_task = true;
169  }
170  if(cmdline.isset("show-local-may-alias"))
171  {
172  options.set_option("show-local-may-alias", true);
173  options.set_option("specific-analysis", true);
174  }
175 
176  // Output format choice
177  if(cmdline.isset("text"))
178  {
179  options.set_option("text", true);
180  options.set_option("outfile", cmdline.get_value("text"));
181  }
182  else if(cmdline.isset("json"))
183  {
184  options.set_option("json", true);
185  options.set_option("outfile", cmdline.get_value("json"));
186  }
187  else if(cmdline.isset("xml"))
188  {
189  options.set_option("xml", true);
190  options.set_option("outfile", cmdline.get_value("xml"));
191  }
192  else if(cmdline.isset("dot"))
193  {
194  options.set_option("dot", true);
195  options.set_option("outfile", cmdline.get_value("dot"));
196  }
197 
198  // Task options
199  if(cmdline.isset("show"))
200  {
201  options.set_option("show", true);
202  options.set_option("general-analysis", true);
203  }
204  else if(cmdline.isset("show-on-source"))
205  {
206  options.set_option("show-on-source", true);
207  options.set_option("general-analysis", true);
208  }
209  else if(cmdline.isset("verify"))
210  {
211  options.set_option("verify", true);
212  options.set_option("general-analysis", true);
213  }
214  else if(cmdline.isset("simplify"))
215  {
216  if(cmdline.get_value("simplify") == "-")
218  "cannot output goto binary to stdout", "--simplify");
219 
220  options.set_option("simplify", true);
221  options.set_option("outfile", cmdline.get_value("simplify"));
222  options.set_option("general-analysis", true);
223 
224  // For development allow slicing to be disabled in the simplify task
225  options.set_option(
226  "simplify-slicing",
227  !(cmdline.isset("no-simplify-slicing")));
228  }
229  else if(cmdline.isset("show-intervals"))
230  {
231  // For backwards compatibility
232  options.set_option("show", true);
233  options.set_option("general-analysis", true);
234  options.set_option("intervals", true);
235  options.set_option("domain set", true);
236  }
237  else if(cmdline.isset("show-non-null"))
238  {
239  // For backwards compatibility
240  options.set_option("show", true);
241  options.set_option("general-analysis", true);
242  options.set_option("non-null", true);
243  options.set_option("domain set", true);
244  }
245  else if(cmdline.isset("intervals") || cmdline.isset("non-null"))
246  {
247  // Partial backwards compatability, just giving these domains without
248  // a task will work. However it will use the general default of verify
249  // rather than their historical default of show.
250  options.set_option("verify", true);
251  options.set_option("general-analysis", true);
252  }
253 
254  if(options.get_bool_option("general-analysis") || reachability_task)
255  {
256  // Abstract interpreter choice
257  if(cmdline.isset("recursive-interprocedural"))
258  options.set_option("recursive-interprocedural", true);
259  else if(cmdline.isset("legacy-ait") || cmdline.isset("location-sensitive"))
260  {
261  options.set_option("legacy-ait", true);
262  // Fixes a number of other options as well
263  options.set_option("ahistorical", true);
264  options.set_option("history set", true);
265  options.set_option("one-domain-per-location", true);
266  options.set_option("storage set", true);
267  }
268  else if(cmdline.isset("legacy-concurrent") || cmdline.isset("concurrent"))
269  {
270  options.set_option("legacy-concurrent", true);
271  options.set_option("ahistorical", true);
272  options.set_option("history set", true);
273  options.set_option("one-domain-per-location", true);
274  options.set_option("storage set", true);
275  }
276  else
277  {
278  // Silently default to legacy-ait for backwards compatability
279  options.set_option("legacy-ait", true);
280  // Fixes a number of other options as well
281  options.set_option("ahistorical", true);
282  options.set_option("history set", true);
283  options.set_option("one-domain-per-location", true);
284  options.set_option("storage set", true);
285  }
286 
287  // History choice
288  if(cmdline.isset("ahistorical"))
289  {
290  options.set_option("ahistorical", true);
291  options.set_option("history set", true);
292  }
293  else if(cmdline.isset("call-stack"))
294  {
295  options.set_option("call-stack", true);
296  options.set_option(
297  "call-stack-recursion-limit", cmdline.get_value("call-stack"));
298  options.set_option("history set", true);
299  }
300  else if(cmdline.isset("loop-unwind"))
301  {
302  options.set_option("local-control-flow-history", true);
303  options.set_option("local-control-flow-history-forward", false);
304  options.set_option("local-control-flow-history-backward", true);
305  options.set_option(
306  "local-control-flow-history-limit", cmdline.get_value("loop-unwind"));
307  options.set_option("history set", true);
308  }
309  else if(cmdline.isset("branching"))
310  {
311  options.set_option("local-control-flow-history", true);
312  options.set_option("local-control-flow-history-forward", true);
313  options.set_option("local-control-flow-history-backward", false);
314  options.set_option(
315  "local-control-flow-history-limit", cmdline.get_value("branching"));
316  options.set_option("history set", true);
317  }
318  else if(cmdline.isset("loop-unwind-and-branching"))
319  {
320  options.set_option("local-control-flow-history", true);
321  options.set_option("local-control-flow-history-forward", true);
322  options.set_option("local-control-flow-history-backward", true);
323  options.set_option(
324  "local-control-flow-history-limit",
325  cmdline.get_value("loop-unwind-and-branching"));
326  options.set_option("history set", true);
327  }
328 
329  if(!options.get_bool_option("history set"))
330  {
331  // Default to ahistorical as it is the expected for of analysis
332  log.status() << "History not specified, defaulting to --ahistorical"
333  << messaget::eom;
334  options.set_option("ahistorical", true);
335  options.set_option("history set", true);
336  }
337 
338  // Domain choice
339  if(cmdline.isset("constants"))
340  {
341  options.set_option("constants", true);
342  options.set_option("domain set", true);
343  }
344  else if(cmdline.isset("dependence-graph"))
345  {
346  options.set_option("dependence-graph", true);
347  options.set_option("domain set", true);
348  }
349  else if(cmdline.isset("intervals"))
350  {
351  options.set_option("intervals", true);
352  options.set_option("domain set", true);
353  }
354  else if(cmdline.isset("non-null"))
355  {
356  options.set_option("non-null", true);
357  options.set_option("domain set", true);
358  }
359 
360  // Reachability questions, when given with a domain swap from specific
361  // to general tasks so that they can use the domain & parameterisations.
362  if(reachability_task)
363  {
364  if(options.get_bool_option("domain set"))
365  {
366  options.set_option("specific-analysis", false);
367  options.set_option("general-analysis", true);
368  }
369  }
370  else
371  {
372  if(!options.get_bool_option("domain set"))
373  {
374  // Default to constants as it is light-weight but useful
375  log.status() << "Domain not specified, defaulting to --constants"
376  << messaget::eom;
377  options.set_option("constants", true);
378  }
379  }
380  }
381 
382  // Storage choice
383  if(cmdline.isset("one-domain-per-history"))
384  {
385  options.set_option("one-domain-per-history", true);
386  options.set_option("storage set", true);
387  }
388  else if(cmdline.isset("one-domain-per-location"))
389  {
390  options.set_option("one-domain-per-location", true);
391  options.set_option("storage set", true);
392  }
393 
394  if(!options.get_bool_option("storage set"))
395  {
396  // one-domain-per-location and one-domain-per-history are effectively
397  // the same when using ahistorical so we default to per-history so that
398  // more sophisticated history objects work as expected
399  log.status() << "Storage not specified,"
400  << " defaulting to --one-domain-per-history" << messaget::eom;
401  options.set_option("one-domain-per-history", true);
402  options.set_option("storage set", true);
403  }
404 
405  if(cmdline.isset("validate-goto-model"))
406  {
407  options.set_option("validate-goto-model", true);
408  }
409 }
410 
415  const optionst &options,
416  const namespacet &ns)
417 {
418  // These support all of the option categories
419  if(options.get_bool_option("recursive-interprocedural"))
420  {
421  // Build the history factory
422  std::unique_ptr<ai_history_factory_baset> hf = nullptr;
423  if(options.get_bool_option("ahistorical"))
424  {
425  hf = util_make_unique<
427  }
428  else if(options.get_bool_option("call-stack"))
429  {
430  hf = util_make_unique<call_stack_history_factoryt>(
431  options.get_unsigned_int_option("call-stack-recursion-limit"));
432  }
433  else if(options.get_bool_option("local-control-flow-history"))
434  {
435  hf = util_make_unique<local_control_flow_history_factoryt>(
436  options.get_bool_option("local-control-flow-history-forward"),
437  options.get_bool_option("local-control-flow-history-backward"),
438  options.get_unsigned_int_option("local-control-flow-history-limit"));
439  }
440 
441  // Build the domain factory
442  std::unique_ptr<ai_domain_factory_baset> df = nullptr;
443  if(options.get_bool_option("constants"))
444  {
445  df = util_make_unique<
447  }
448  else if(options.get_bool_option("intervals"))
449  {
450  df = util_make_unique<
452  }
453  // non-null is not fully supported, despite the historical options
454  // dependency-graph is quite heavily tied to the legacy-ait infrastructure
455 
456  // Build the storage object
457  std::unique_ptr<ai_storage_baset> st = nullptr;
458  if(options.get_bool_option("one-domain-per-history"))
459  {
460  st = util_make_unique<history_sensitive_storaget>();
461  }
462  else if(options.get_bool_option("one-domain-per-location"))
463  {
464  st = util_make_unique<location_sensitive_storaget>();
465  }
466 
467  // Only try to build the abstract interpreter if all the parts have been
468  // correctly specified and configured
469  if(hf != nullptr && df != nullptr && st != nullptr)
470  {
471  if(options.get_bool_option("recursive-interprocedural"))
472  {
474  std::move(hf), std::move(df), std::move(st));
475  }
476  UNREACHABLE;
477  }
478  }
479  else if(options.get_bool_option("legacy-ait"))
480  {
481  if(options.get_bool_option("constants"))
482  {
483  // constant_propagator_ait derives from ait<constant_propagator_domaint>
485  }
486  else if(options.get_bool_option("dependence-graph"))
487  {
488  return new dependence_grapht(ns);
489  }
490  else if(options.get_bool_option("intervals"))
491  {
492  return new ait<interval_domaint>();
493  }
494 #if 0
495  // Not actually implemented, despite the option...
496  else if(options.get_bool_option("non-null"))
497  {
498  return new ait<non_null_domaint>();
499  }
500 #endif
501  }
502  else if(options.get_bool_option("legacy-concurrent"))
503  {
504 #if 0
505  // Very few domains can work with this interpreter
506  // as it requires that changes to the domain are
507  // 'non-revertable' and it has merge shared
508  if(options.get_bool_option("dependence-graph"))
509  {
510  return new dependence_grapht(ns);
511  }
512 #endif
513  }
514 
515  // Construction failed due to configuration errors
516  return nullptr;
517 }
518 
521 {
522  if(cmdline.isset("version"))
523  {
524  std::cout << CBMC_VERSION << '\n';
525  return CPROVER_EXIT_SUCCESS;
526  }
527 
528  //
529  // command line options
530  //
531 
532  optionst options;
533  get_command_line_options(options);
536 
537  //
538  // Print a banner
539  //
540  log.status() << "GOTO-ANALYSER version " << CBMC_VERSION << " "
541  << sizeof(void *) * 8 << "-bit " << config.this_architecture()
543 
545 
547 
548  if(process_goto_program(options))
550 
551  if(cmdline.isset("validate-goto-model"))
552  {
554  }
555 
556  // show it?
557  if(cmdline.isset("show-symbol-table"))
558  {
560  return CPROVER_EXIT_SUCCESS;
561  }
562 
563  // show it?
564  if(
565  cmdline.isset("show-goto-functions") ||
566  cmdline.isset("list-goto-functions"))
567  {
569  goto_model, ui_message_handler, cmdline.isset("list-goto-functions"));
570  return CPROVER_EXIT_SUCCESS;
571  }
572 
573  return perform_analysis(options);
574 }
575 
576 
579 {
581  if(options.get_bool_option("taint"))
582  {
583  std::string taint_file=cmdline.get_value("taint");
584 
585  if(cmdline.isset("show-taint"))
586  {
587  taint_analysis(goto_model, taint_file, ui_message_handler, true);
588  return CPROVER_EXIT_SUCCESS;
589  }
590  else
591  {
592  std::string json_file=cmdline.get_value("json");
593  bool result = taint_analysis(
594  goto_model, taint_file, ui_message_handler, false, json_file);
596  }
597  }
598 
599  // If no domain is given, this lightweight version of the analysis is used.
600  if(options.get_bool_option("unreachable-instructions") &&
601  options.get_bool_option("specific-analysis"))
602  {
603  const std::string json_file=cmdline.get_value("json");
604 
605  if(json_file.empty())
606  unreachable_instructions(goto_model, false, std::cout);
607  else if(json_file=="-")
608  unreachable_instructions(goto_model, true, std::cout);
609  else
610  {
611  std::ofstream ofs(json_file);
612  if(!ofs)
613  {
614  log.error() << "Failed to open json output '" << json_file << "'"
615  << messaget::eom;
617  }
618 
620  }
621 
622  return CPROVER_EXIT_SUCCESS;
623  }
624 
625  if(options.get_bool_option("unreachable-functions") &&
626  options.get_bool_option("specific-analysis"))
627  {
628  const std::string json_file=cmdline.get_value("json");
629 
630  if(json_file.empty())
631  unreachable_functions(goto_model, false, std::cout);
632  else if(json_file=="-")
633  unreachable_functions(goto_model, true, std::cout);
634  else
635  {
636  std::ofstream ofs(json_file);
637  if(!ofs)
638  {
639  log.error() << "Failed to open json output '" << json_file << "'"
640  << messaget::eom;
642  }
643 
644  unreachable_functions(goto_model, true, ofs);
645  }
646 
647  return CPROVER_EXIT_SUCCESS;
648  }
649 
650  if(options.get_bool_option("reachable-functions") &&
651  options.get_bool_option("specific-analysis"))
652  {
653  const std::string json_file=cmdline.get_value("json");
654 
655  if(json_file.empty())
656  reachable_functions(goto_model, false, std::cout);
657  else if(json_file=="-")
658  reachable_functions(goto_model, true, std::cout);
659  else
660  {
661  std::ofstream ofs(json_file);
662  if(!ofs)
663  {
664  log.error() << "Failed to open json output '" << json_file << "'"
665  << messaget::eom;
667  }
668 
669  reachable_functions(goto_model, true, ofs);
670  }
671 
672  return CPROVER_EXIT_SUCCESS;
673  }
674 
675  if(options.get_bool_option("show-local-may-alias"))
676  {
678 
680  {
681  std::cout << ">>>>\n";
682  std::cout << ">>>> " << it->first << '\n';
683  std::cout << ">>>>\n";
684  local_may_aliast local_may_alias(it->second);
685  local_may_alias.output(std::cout, it->second, ns);
686  std::cout << '\n';
687  }
688 
689  return CPROVER_EXIT_SUCCESS;
690  }
691 
693 
694  if(cmdline.isset("show-properties"))
695  {
697  return CPROVER_EXIT_SUCCESS;
698  }
699 
700  if(cmdline.isset("property"))
702 
703  if(options.get_bool_option("general-analysis"))
704  {
705  // Output file factory
706  const std::string outfile=options.get_option("outfile");
707 
708  std::ofstream output_stream;
709  if(outfile != "-" && !outfile.empty())
710  output_stream.open(outfile);
711 
712  std::ostream &out(
713  (outfile == "-" || outfile.empty()) ? std::cout : output_stream);
714 
715  if(!out)
716  {
717  log.error() << "Failed to open output file '" << outfile << "'"
718  << messaget::eom;
720  }
721 
722  // Build analyzer
723  log.status() << "Selecting abstract domain" << messaget::eom;
724  namespacet ns(goto_model.symbol_table); // Must live as long as the domain.
725  std::unique_ptr<ai_baset> analyzer(build_analyzer(options, ns));
726 
727  if(analyzer == nullptr)
728  {
729  log.status() << "Task / Interpreter combination not supported"
730  << messaget::eom;
732  }
733 
734  // Run
735  log.status() << "Computing abstract states" << messaget::eom;
736  (*analyzer)(goto_model);
737 
738  // Perform the task
739  log.status() << "Performing task" << messaget::eom;
740 
741  bool result = true;
742 
743  if(options.get_bool_option("show"))
744  {
745  static_show_domain(goto_model, *analyzer, options, out);
746  return CPROVER_EXIT_SUCCESS;
747  }
748  else if(options.get_bool_option("show-on-source"))
749  {
751  return CPROVER_EXIT_SUCCESS;
752  }
753  else if(options.get_bool_option("verify"))
754  {
755  result = static_verifier(
756  goto_model, *analyzer, options, ui_message_handler, out);
757  }
758  else if(options.get_bool_option("simplify"))
759  {
760  PRECONDITION(!outfile.empty() && outfile != "-");
761  output_stream.close();
762  output_stream.open(outfile, std::ios::binary);
763  result = static_simplifier(
764  goto_model, *analyzer, options, ui_message_handler, out);
765  }
766  else if(options.get_bool_option("unreachable-instructions"))
767  {
769  *analyzer,
770  options,
771  out);
772  }
773  else if(options.get_bool_option("unreachable-functions"))
774  {
776  *analyzer,
777  options,
778  out);
779  }
780  else if(options.get_bool_option("reachable-functions"))
781  {
783  *analyzer,
784  options,
785  out);
786  }
787  else
788  {
789  log.error() << "Unhandled task" << messaget::eom;
791  }
792 
793  return result ?
795  }
796 
797 
798  // Final defensive error case
799  log.error() << "no analysis option given -- consider reading --help"
800  << messaget::eom;
802 }
803 
805  const optionst &options)
806 {
807  {
808  #if 0
809  // Remove inline assembler; this needs to happen before
810  // adding the library.
812 
813  // add the library
814  log.status() << "Adding CPROVER library (" << config.ansi_c.arch << ")" << messaget::eom;
818 
819  // these are commented out as well because without the library
820  // this initialization code doesn’t make any sense
822 
823 #endif
824 
825  // remove function pointers
826  log.status() << "Removing function pointers and virtual functions"
827  << messaget::eom;
829  ui_message_handler, goto_model, cmdline.isset("pointer-check"));
830 
831  // do partial inlining
832  log.status() << "Partial Inlining" << messaget::eom;
834 
835  // remove returns, gcc vectors, complex
839 
840 #if 0
841  // add generic checks
842  log.status() << "Generic Property Instrumentation" << messaget::eom;
843  goto_check(options, goto_model);
844 #else
845  (void)options; // unused parameter
846 #endif
847 
848  // recalculate numbers, etc.
850 
851  // add loop ids
853  }
854  return false;
855 }
856 
859 {
860  // clang-format off
861  std::cout << '\n' << banner_string("GOTO-ANALYZER", CBMC_VERSION) << '\n'
862  << align_center_with_border("Copyright (C) 2017-2018") << '\n'
863  << align_center_with_border("Daniel Kroening, Diffblue") << '\n'
864  << align_center_with_border("kroening@kroening.com") << '\n'
865  <<
866  "\n"
867  "Usage: Purpose:\n"
868  "\n"
869  " goto-analyzer [-h] [--help] show help\n"
870  " goto-analyzer file.c ... source file names\n"
871  "\n"
872  "Task options:\n"
873  " --show display the abstract states on the goto program\n" // NOLINT(*)
874  " --show-on-source display the abstract states on the source\n"
875  // NOLINTNEXTLINE(whitespace/line_length)
876  " --verify use the abstract domains to check assertions\n"
877  // NOLINTNEXTLINE(whitespace/line_length)
878  " --simplify file_name use the abstract domains to simplify the program\n"
879  " --unreachable-instructions list dead code\n"
880  // NOLINTNEXTLINE(whitespace/line_length)
881  " --unreachable-functions list functions unreachable from the entry point\n"
882  // NOLINTNEXTLINE(whitespace/line_length)
883  " --reachable-functions list functions reachable from the entry point\n"
884  "\n"
885  "Abstract interpreter options:\n"
886  // NOLINTNEXTLINE(whitespace/line_length)
887  " --recursive-interprocedural use recursion to handle interprocedural reasoning\n"
888  // NOLINTNEXTLINE(whitespace/line_length)
889  " --legacy-ait recursion for function and one domain per location\n"
890  // NOLINTNEXTLINE(whitespace/line_length)
891  " --legacy-concurrent legacy-ait with an extended fixed-point for concurrency\n"
892  "\n"
893  "History options:\n"
894  // NOLINTNEXTLINE(whitespace/line_length)
895  " --ahistorical the most basic history, tracks locations only\n"
896  // NOLINTNEXTLINE(whitespace/line_length)
897  " --call-stack n track the calling location stack for each function\n"
898  // NOLINTNEXTLINE(whitespace/line_length)
899  " limiting to at most n recursive loops, 0 to disable\n"
900  // NOLINTNEXTLINE(whitespace/line_length)
901  " --loop-unwind n track the number of loop iterations within a function\n"
902  // NOLINTNEXTLINE(whitespace/line_length)
903  " limited to n histories per location, 0 is unlimited\n"
904  // NOLINTNEXTLINE(whitespace/line_length)
905  " --branching n track the forwards jumps (if, switch, etc.) within a function\n"
906  // NOLINTNEXTLINE(whitespace/line_length)
907  " limited to n histories per location, 0 is unlimited\n"
908  // NOLINTNEXTLINE(whitespace/line_length)
909  " --loop-unwind-and-branching n track all local control flow\n"
910  // NOLINTNEXTLINE(whitespace/line_length)
911  " limited to n histories per location, 0 is unlimited\n"
912  "\n"
913  "Domain options:\n"
914  " --constants a constant for each variable if possible\n"
915  " --intervals an interval for each variable\n"
916  " --non-null tracks which pointers are non-null\n"
917  " --dependence-graph data and control dependencies between instructions\n" // NOLINT(*)
918  "\n"
919  "Storage options:\n"
920  // NOLINTNEXTLINE(whitespace/line_length)
921  " --one-domain-per-history stores a domain for each history object created\n"
922  " --one-domain-per-location stores a domain for each location reached\n"
923  "\n"
924  "Output options:\n"
925  " --text file_name output results in plain text to given file\n"
926  // NOLINTNEXTLINE(whitespace/line_length)
927  " --json file_name output results in JSON format to given file\n"
928  " --xml file_name output results in XML format to given file\n"
929  " --dot file_name output results in DOT format to given file\n"
930  "\n"
931  "Specific analyses:\n"
932  // NOLINTNEXTLINE(whitespace/line_length)
933  " --taint file_name perform taint analysis using rules in given file\n"
934  "\n"
935  "C/C++ frontend options:\n"
936  " -I path set include path (C/C++)\n"
937  " -D macro define preprocessor macro (C/C++)\n"
938  " --arch X set architecture (default: "
939  << configt::this_architecture() << ")\n"
940  " --os set operating system (default: "
941  << configt::this_operating_system() << ")\n"
942  " --c89/99/11 set C language standard (default: "
949  "c11":"") << ")\n"
950  " --cpp98/03/11 set C++ language standard (default: "
953  "cpp98":
956  "cpp03":
959  "cpp11":"") << ")\n"
960  #ifdef _WIN32
961  " --gcc use GCC as preprocessor\n"
962  #endif
963  " --no-library disable built-in abstract C library\n"
965  "\n"
966  "Program representations:\n"
967  " --show-parse-tree show parse tree\n"
968  " --show-symbol-table show loaded symbol table\n"
971  "\n"
972  "Program instrumentation options:\n"
974  "\n"
975  "Other options:\n"
977  " --version show version and exit\n"
978  HELP_FLUSH
980  "\n";
981  // clang-format on
982 }
cprover_library.h
cmdlinet::args
argst args
Definition: cmdline.h:91
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
add_malloc_may_fail_variable_initializations.h
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:29
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
Function Inlining.
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:90
ai_recursive_interproceduralt
Definition: ai.h:524
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
local_control_flow_history.h
Track function-local control flow for loop unwinding and path senstivity.
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:171
messaget::status
mstreamt & status() const
Definition: message.h:414
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
Goto-Analyser Command Line Option Processing.
configt::cppt::cpp_standardt::CPP03
@ CPP03
taint_analysis.h
Taint Analysis.
remove_virtual_functions.h
Functions for replacing virtual function call with a static function calls in functions,...
remove_asm.h
Remove 'asm' statements by compiling them into suitable standard goto program instructions.
constant_propagator.h
Constant propagation.
jsil_language.h
Jsil Language.
ait
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition: ai.h:558
mode.h
options.h
Options.
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:2231
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:297
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:414
goto_analyzer_parse_optionst::goto_analyzer_parse_optionst
goto_analyzer_parse_optionst(int argc, const char **argv)
Definition: goto_analyzer_parse_options.cpp:72
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:47
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:151
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
Remove the 'complex' data type by compilation into structs.
set_properties.h
Set the properties to check.
configt::ansi_ct::c_standardt::C89
@ C89
CBMC_VERSION
const char * CBMC_VERSION
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:399
goto_analyzer_parse_optionst::process_goto_program
virtual bool process_goto_program(const optionst &options)
Definition: goto_analyzer_parse_options.cpp:804
initialize_goto_model.h
Initialize a Goto Program.
banner_string
std::string banner_string(const std::string &front_end, const std::string &version)
Definition: parse_options.cpp:163
local_may_alias.h
Field-insensitive, location-sensitive may-alias analysis.
ai_history_factory_default_constructort
An easy factory implementation for histories that don't need parameters.
Definition: ai_history.h:255
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
show_properties.h
Show the properties.
is_threaded.h
Over-approximate Concurrency for Threaded Goto Programs.
configt::cppt::set_cpp11
void set_cpp11()
Definition: config.h:153
cmdlinet::get_value
std::string get_value(char option) const
Definition: cmdline.cpp:47
show_symbol_table.h
Show the symbol table.
goto_analyzer_parse_optionst::doit
virtual int doit() override
invoke main modules
Definition: goto_analyzer_parse_options.cpp:520
language.h
Abstract interface to support a programming language.
unreachable_instructions.h
List all unreachable instructions.
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:1402
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:858
goto_check.h
Program Transformation.
goto_functionst::compute_loop_numbers
void compute_loop_numbers()
Definition: goto_functions.cpp:52
read_goto_binary.h
Read Goto Programs.
GOTO_ANALYSER_OPTIONS
#define GOTO_ANALYSER_OPTIONS
Definition: goto_analyzer_parse_options.h:146
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
add_malloc_may_fail_variable_initializations
void add_malloc_may_fail_variable_initializations(goto_modelt &goto_model)
Some variables have different initial values based on what flags are being passed to cbmc; since the ...
Definition: add_malloc_may_fail_variable_initializations.cpp:22
remove_vector.h
Remove the 'vector' data type by compilation into arrays.
remove_complex
static void remove_complex(typet &)
removes complex data type
Definition: remove_complex.cpp:231
remove_returns.h
Replace function returns by assignments to global variables.
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:83
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:1302
configt::ansi_ct::c_standardt::C11
@ C11
interval_domain.h
Interval Domain.
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:45
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:79
configt::set
bool set(const cmdlinet &cmdline)
Definition: config.cpp:798
configt::cppt::default_cpp_standard
static cpp_standardt default_cpp_standard()
Definition: config.cpp:690
exit_codes.h
Document and give macros for the exit codes of CPROVER binaries.
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
Goto Programs with Functions.
call_stack_history.h
History for tracking the call stack and performing interprocedural analysis.
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:104
goto_analyzer_parse_optionst::goto_model
goto_modelt goto_model
Definition: goto_analyzer_parse_options.h:184
adjust_float_expressions.h
Symbolic Execution.
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:108
remove_function_pointers.h
Remove Indirect Function Calls.
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:150
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:578
cprover_library.h
static_show_domain.h
dependence_graph.h
Field-Sensitive Program Dependence Analysis, Litvak et al., FSE 2010.
HELP_TIMESTAMP
#define HELP_TIMESTAMP
Definition: timestamper.h:14
HELP_FLUSH
#define HELP_FLUSH
Definition: ui_message.h:106
configt::cppt::set_cpp03
void set_cpp03()
Definition: config.h:152
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
C++ Language Module.