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 <fstream>
16 #include <iostream>
17 #include <memory>
18 
19 #include <ansi-c/cprover_library.h>
20 
21 #include <assembler/remove_asm.h>
22 
23 #include <cpp/cprover_library.h>
24 
32 
33 #include <analyses/ai.h>
35 
36 #include <util/config.h>
37 #include <util/exception_utils.h>
38 #include <util/exit_codes.h>
39 #include <util/options.h>
40 #include <util/version.h>
41 
42 #include "build_analyzer.h"
43 #include "show_on_source.h"
44 #include "static_show_domain.h"
45 #include "static_simplifier.h"
46 #include "static_verifier.h"
47 #include "taint_analysis.h"
49 
51  int argc,
52  const char **argv)
55  argc,
56  argv,
57  std::string("GOTO-ANALYZER "))
58 {
59 }
60 
62 {
63  if(config.set(cmdline))
64  {
65  usage_error();
67  }
68 
69  if(cmdline.isset("function"))
70  options.set_option("function", cmdline.get_value("function"));
71 
72  // all checks supported by goto_check
74 
75  // The user should either select:
76  // 1. a specific analysis, or
77  // 2. a tuple of task / analyser options / outputs
78 
79  // Select a specific analysis
80  if(cmdline.isset("taint"))
81  {
82  options.set_option("taint", true);
83  options.set_option("specific-analysis", true);
84  }
85  // For backwards compatibility,
86  // these are first recognised as specific analyses
87  bool reachability_task = false;
88  if(cmdline.isset("unreachable-instructions"))
89  {
90  options.set_option("unreachable-instructions", true);
91  options.set_option("specific-analysis", true);
92  reachability_task = true;
93  }
94  if(cmdline.isset("unreachable-functions"))
95  {
96  options.set_option("unreachable-functions", true);
97  options.set_option("specific-analysis", true);
98  reachability_task = true;
99  }
100  if(cmdline.isset("reachable-functions"))
101  {
102  options.set_option("reachable-functions", true);
103  options.set_option("specific-analysis", true);
104  reachability_task = true;
105  }
106  if(cmdline.isset("show-local-may-alias"))
107  {
108  options.set_option("show-local-may-alias", true);
109  options.set_option("specific-analysis", true);
110  }
111 
112  // Output format choice
113  if(cmdline.isset("text"))
114  {
115  options.set_option("text", true);
116  options.set_option("outfile", cmdline.get_value("text"));
117  }
118  else if(cmdline.isset("json"))
119  {
120  options.set_option("json", true);
121  options.set_option("outfile", cmdline.get_value("json"));
122  }
123  else if(cmdline.isset("xml"))
124  {
125  options.set_option("xml", true);
126  options.set_option("outfile", cmdline.get_value("xml"));
127  }
128  else if(cmdline.isset("dot"))
129  {
130  options.set_option("dot", true);
131  options.set_option("outfile", cmdline.get_value("dot"));
132  }
133 
134  // Task options
135  if(cmdline.isset("show"))
136  {
137  options.set_option("show", true);
138  options.set_option("general-analysis", true);
139  }
140  else if(cmdline.isset("show-on-source"))
141  {
142  options.set_option("show-on-source", true);
143  options.set_option("general-analysis", true);
144  }
145  else if(cmdline.isset("verify"))
146  {
147  options.set_option("verify", true);
148  options.set_option("general-analysis", true);
149  }
150  else if(cmdline.isset("simplify"))
151  {
152  if(cmdline.get_value("simplify") == "-")
154  "cannot output goto binary to stdout", "--simplify");
155 
156  options.set_option("simplify", true);
157  options.set_option("outfile", cmdline.get_value("simplify"));
158  options.set_option("general-analysis", true);
159 
160  // For development allow slicing to be disabled in the simplify task
161  options.set_option(
162  "simplify-slicing",
163  !(cmdline.isset("no-simplify-slicing")));
164  }
165  else if(cmdline.isset("show-intervals"))
166  {
167  // For backwards compatibility
168  options.set_option("show", true);
169  options.set_option("general-analysis", true);
170  options.set_option("intervals", true);
171  options.set_option("domain set", true);
172  }
173  else if(cmdline.isset("show-non-null"))
174  {
175  // For backwards compatibility
176  options.set_option("show", true);
177  options.set_option("general-analysis", true);
178  options.set_option("non-null", true);
179  options.set_option("domain set", true);
180  }
181  else if(cmdline.isset("intervals") || cmdline.isset("non-null"))
182  {
183  // Partial backwards compatability, just giving these domains without
184  // a task will work. However it will use the general default of verify
185  // rather than their historical default of show.
186  options.set_option("verify", true);
187  options.set_option("general-analysis", true);
188  }
189 
190  if(options.get_bool_option("general-analysis") || reachability_task)
191  {
192  // Abstract interpreter choice
193  if(cmdline.isset("recursive-interprocedural"))
194  options.set_option("recursive-interprocedural", true);
195  else if(cmdline.isset("three-way-merge"))
196  options.set_option("three-way-merge", true);
197  else if(cmdline.isset("legacy-ait") || cmdline.isset("location-sensitive"))
198  {
199  options.set_option("legacy-ait", true);
200  // Fixes a number of other options as well
201  options.set_option("ahistorical", true);
202  options.set_option("history set", true);
203  options.set_option("one-domain-per-location", true);
204  options.set_option("storage set", true);
205  }
206  else if(cmdline.isset("legacy-concurrent") || cmdline.isset("concurrent"))
207  {
208  options.set_option("legacy-concurrent", true);
209  options.set_option("ahistorical", true);
210  options.set_option("history set", true);
211  options.set_option("one-domain-per-location", true);
212  options.set_option("storage set", true);
213  }
214  else
215  {
216  // Silently default to legacy-ait for backwards compatability
217  options.set_option("legacy-ait", true);
218  // Fixes a number of other options as well
219  options.set_option("ahistorical", true);
220  options.set_option("history set", true);
221  options.set_option("one-domain-per-location", true);
222  options.set_option("storage set", true);
223  }
224 
225  // History choice
226  if(cmdline.isset("ahistorical"))
227  {
228  options.set_option("ahistorical", true);
229  options.set_option("history set", true);
230  }
231  else if(cmdline.isset("call-stack"))
232  {
233  options.set_option("call-stack", true);
234  options.set_option(
235  "call-stack-recursion-limit", cmdline.get_value("call-stack"));
236  options.set_option("history set", true);
237  }
238  else if(cmdline.isset("loop-unwind"))
239  {
240  options.set_option("local-control-flow-history", true);
241  options.set_option("local-control-flow-history-forward", false);
242  options.set_option("local-control-flow-history-backward", true);
243  options.set_option(
244  "local-control-flow-history-limit", cmdline.get_value("loop-unwind"));
245  options.set_option("history set", true);
246  }
247  else if(cmdline.isset("branching"))
248  {
249  options.set_option("local-control-flow-history", true);
250  options.set_option("local-control-flow-history-forward", true);
251  options.set_option("local-control-flow-history-backward", false);
252  options.set_option(
253  "local-control-flow-history-limit", cmdline.get_value("branching"));
254  options.set_option("history set", true);
255  }
256  else if(cmdline.isset("loop-unwind-and-branching"))
257  {
258  options.set_option("local-control-flow-history", true);
259  options.set_option("local-control-flow-history-forward", true);
260  options.set_option("local-control-flow-history-backward", true);
261  options.set_option(
262  "local-control-flow-history-limit",
263  cmdline.get_value("loop-unwind-and-branching"));
264  options.set_option("history set", true);
265  }
266 
267  if(!options.get_bool_option("history set"))
268  {
269  // Default to ahistorical as it is the expected for of analysis
270  log.status() << "History not specified, defaulting to --ahistorical"
271  << messaget::eom;
272  options.set_option("ahistorical", true);
273  options.set_option("history set", true);
274  }
275 
276  // Domain choice
277  if(cmdline.isset("constants"))
278  {
279  options.set_option("constants", true);
280  options.set_option("domain set", true);
281  }
282  else if(cmdline.isset("dependence-graph"))
283  {
284  options.set_option("dependence-graph", true);
285  options.set_option("domain set", true);
286  }
287  else if(cmdline.isset("intervals"))
288  {
289  options.set_option("intervals", true);
290  options.set_option("domain set", true);
291  }
292  else if(cmdline.isset("non-null"))
293  {
294  options.set_option("non-null", true);
295  options.set_option("domain set", true);
296  }
297  else if(cmdline.isset("vsd") || cmdline.isset("variable-sensitivity"))
298  {
299  options.set_option("vsd", true);
300  options.set_option("domain set", true);
301 
302  PARSE_OPTIONS_VSD(cmdline, options);
303  }
304  else if(cmdline.isset("dependence-graph-vs"))
305  {
306  options.set_option("dependence-graph-vs", true);
307  options.set_option("domain set", true);
308 
309  PARSE_OPTIONS_VSD(cmdline, options);
310  options.set_option("data-dependencies", true); // Always set
311  }
312 
313  // Reachability questions, when given with a domain swap from specific
314  // to general tasks so that they can use the domain & parameterisations.
315  if(reachability_task)
316  {
317  if(options.get_bool_option("domain set"))
318  {
319  options.set_option("specific-analysis", false);
320  options.set_option("general-analysis", true);
321  }
322  }
323  else
324  {
325  if(!options.get_bool_option("domain set"))
326  {
327  // Default to constants as it is light-weight but useful
328  log.status() << "Domain not specified, defaulting to --constants"
329  << messaget::eom;
330  options.set_option("constants", true);
331  }
332  }
333  }
334 
335  // Storage choice
336  if(cmdline.isset("one-domain-per-history"))
337  {
338  options.set_option("one-domain-per-history", true);
339  options.set_option("storage set", true);
340  }
341  else if(cmdline.isset("one-domain-per-location"))
342  {
343  options.set_option("one-domain-per-location", true);
344  options.set_option("storage set", true);
345  }
346 
347  if(!options.get_bool_option("storage set"))
348  {
349  // one-domain-per-location and one-domain-per-history are effectively
350  // the same when using ahistorical so we default to per-history so that
351  // more sophisticated history objects work as expected
352  log.status() << "Storage not specified,"
353  << " defaulting to --one-domain-per-history" << messaget::eom;
354  options.set_option("one-domain-per-history", true);
355  options.set_option("storage set", true);
356  }
357 
358  if(cmdline.isset("validate-goto-model"))
359  {
360  options.set_option("validate-goto-model", true);
361  }
362 }
363 
366 {
367  if(cmdline.isset("version"))
368  {
369  std::cout << CBMC_VERSION << '\n';
370  return CPROVER_EXIT_SUCCESS;
371  }
372 
373  //
374  // command line options
375  //
376 
377  optionst options;
378  get_command_line_options(options);
381 
382  log_version_and_architecture("GOTO-ANALYZER");
383 
385 
387 
388  // Preserve backwards compatibility in processing
389  options.set_option("partial-inline", true);
390  options.set_option("rewrite-union", false);
391 
392  if(process_goto_program(options))
394 
395  if(cmdline.isset("validate-goto-model"))
396  {
398  }
399 
400  // show it?
401  if(cmdline.isset("show-symbol-table"))
402  {
404  return CPROVER_EXIT_SUCCESS;
405  }
406 
407  // show it?
408  if(
409  cmdline.isset("show-goto-functions") ||
410  cmdline.isset("list-goto-functions"))
411  {
413  goto_model, ui_message_handler, cmdline.isset("list-goto-functions"));
414  return CPROVER_EXIT_SUCCESS;
415  }
416 
417  return perform_analysis(options);
418 }
419 
422 {
423  if(options.get_bool_option("taint"))
424  {
425  std::string taint_file=cmdline.get_value("taint");
426 
427  if(cmdline.isset("show-taint"))
428  {
429  taint_analysis(goto_model, taint_file, ui_message_handler, true);
430  return CPROVER_EXIT_SUCCESS;
431  }
432  else
433  {
434  std::string json_file=cmdline.get_value("json");
435  bool result = taint_analysis(
436  goto_model, taint_file, ui_message_handler, false, json_file);
438  }
439  }
440 
441  // If no domain is given, this lightweight version of the analysis is used.
442  if(options.get_bool_option("unreachable-instructions") &&
443  options.get_bool_option("specific-analysis"))
444  {
445  const std::string json_file=cmdline.get_value("json");
446 
447  if(json_file.empty())
448  unreachable_instructions(goto_model, false, std::cout);
449  else if(json_file=="-")
450  unreachable_instructions(goto_model, true, std::cout);
451  else
452  {
453  std::ofstream ofs(json_file);
454  if(!ofs)
455  {
456  log.error() << "Failed to open json output '" << json_file << "'"
457  << messaget::eom;
459  }
460 
462  }
463 
464  return CPROVER_EXIT_SUCCESS;
465  }
466 
467  if(options.get_bool_option("unreachable-functions") &&
468  options.get_bool_option("specific-analysis"))
469  {
470  const std::string json_file=cmdline.get_value("json");
471 
472  if(json_file.empty())
473  unreachable_functions(goto_model, false, std::cout);
474  else if(json_file=="-")
475  unreachable_functions(goto_model, true, std::cout);
476  else
477  {
478  std::ofstream ofs(json_file);
479  if(!ofs)
480  {
481  log.error() << "Failed to open json output '" << json_file << "'"
482  << messaget::eom;
484  }
485 
486  unreachable_functions(goto_model, true, ofs);
487  }
488 
489  return CPROVER_EXIT_SUCCESS;
490  }
491 
492  if(options.get_bool_option("reachable-functions") &&
493  options.get_bool_option("specific-analysis"))
494  {
495  const std::string json_file=cmdline.get_value("json");
496 
497  if(json_file.empty())
498  reachable_functions(goto_model, false, std::cout);
499  else if(json_file=="-")
500  reachable_functions(goto_model, true, std::cout);
501  else
502  {
503  std::ofstream ofs(json_file);
504  if(!ofs)
505  {
506  log.error() << "Failed to open json output '" << json_file << "'"
507  << messaget::eom;
509  }
510 
511  reachable_functions(goto_model, true, ofs);
512  }
513 
514  return CPROVER_EXIT_SUCCESS;
515  }
516 
517  if(options.get_bool_option("show-local-may-alias"))
518  {
520 
521  for(const auto &gf_entry : goto_model.goto_functions.function_map)
522  {
523  std::cout << ">>>>\n";
524  std::cout << ">>>> " << gf_entry.first << '\n';
525  std::cout << ">>>>\n";
526  local_may_aliast local_may_alias(gf_entry.second);
527  local_may_alias.output(std::cout, gf_entry.second, ns);
528  std::cout << '\n';
529  }
530 
531  return CPROVER_EXIT_SUCCESS;
532  }
533 
535 
536  if(cmdline.isset("show-properties"))
537  {
539  return CPROVER_EXIT_SUCCESS;
540  }
541 
542  if(cmdline.isset("property"))
544 
545  if(options.get_bool_option("general-analysis"))
546  {
547  // Output file factory
548  const std::string outfile=options.get_option("outfile");
549 
550  std::ofstream output_stream;
551  if(outfile != "-" && !outfile.empty())
552  output_stream.open(outfile);
553 
554  std::ostream &out(
555  (outfile == "-" || outfile.empty()) ? std::cout : output_stream);
556 
557  if(!out)
558  {
559  log.error() << "Failed to open output file '" << outfile << "'"
560  << messaget::eom;
562  }
563 
564  // Build analyzer
565  log.status() << "Selecting abstract domain" << messaget::eom;
566  namespacet ns(goto_model.symbol_table); // Must live as long as the domain.
567  std::unique_ptr<ai_baset> analyzer;
568 
569  try
570  {
571  analyzer = build_analyzer(options, goto_model, ns, ui_message_handler);
572  }
574  {
575  log.error() << e.what() << messaget::eom;
577  }
578 
579  if(analyzer == nullptr)
580  {
581  log.status() << "Task / Interpreter combination not supported"
582  << messaget::eom;
584  }
585 
586  // Run
587  log.status() << "Computing abstract states" << messaget::eom;
588  (*analyzer)(goto_model);
589 
590  // Perform the task
591  log.status() << "Performing task" << messaget::eom;
592 
593  bool result = true;
594 
595  if(options.get_bool_option("show"))
596  {
597  static_show_domain(goto_model, *analyzer, options, out);
598  return CPROVER_EXIT_SUCCESS;
599  }
600  else if(options.get_bool_option("show-on-source"))
601  {
603  return CPROVER_EXIT_SUCCESS;
604  }
605  else if(options.get_bool_option("verify"))
606  {
607  result = static_verifier(
608  goto_model, *analyzer, options, ui_message_handler, out);
609  }
610  else if(options.get_bool_option("simplify"))
611  {
612  PRECONDITION(!outfile.empty() && outfile != "-");
613  output_stream.close();
614  output_stream.open(outfile, std::ios::binary);
615  result = static_simplifier(
616  goto_model, *analyzer, options, ui_message_handler, out);
617  }
618  else if(options.get_bool_option("unreachable-instructions"))
619  {
621  *analyzer,
622  options,
623  out);
624  }
625  else if(options.get_bool_option("unreachable-functions"))
626  {
628  *analyzer,
629  options,
630  out);
631  }
632  else if(options.get_bool_option("reachable-functions"))
633  {
635  *analyzer,
636  options,
637  out);
638  }
639  else
640  {
641  log.error() << "Unhandled task" << messaget::eom;
643  }
644 
645  return result ?
647  }
648 
649  // Final defensive error case
650  log.error() << "no analysis option given -- consider reading --help"
651  << messaget::eom;
653 }
654 
656  const optionst &options)
657 {
658  // Remove inline assembler; this needs to happen before
659  // adding the library.
661 
662  // add the library
663  log.status() << "Adding CPROVER library (" << config.ansi_c.arch << ")"
664  << messaget::eom;
667 
669 
670  // Common removal of types and complex constructs
671  if(::process_goto_program(goto_model, options, log))
672  return true;
673 
674  return false;
675 }
676 
679 {
680  // clang-format off
681  std::cout << '\n' << banner_string("GOTO-ANALYZER", CBMC_VERSION) << '\n'
682  << align_center_with_border("Copyright (C) 2017-2018") << '\n'
683  << align_center_with_border("Daniel Kroening, Diffblue") << '\n'
684  << align_center_with_border("kroening@kroening.com") << '\n'
685  <<
686  "\n"
687  "Usage: Purpose:\n"
688  "\n"
689  " goto-analyzer [-h] [--help] show help\n"
690  " goto-analyzer file.c ... source file names\n"
691  "\n"
692  "Task options:\n"
693  " --show display the abstract states on the goto program\n" // NOLINT(*)
694  " --show-on-source display the abstract states on the source\n"
695  // NOLINTNEXTLINE(whitespace/line_length)
696  " --verify use the abstract domains to check assertions\n"
697  // NOLINTNEXTLINE(whitespace/line_length)
698  " --simplify file_name use the abstract domains to simplify the program\n"
699  " --unreachable-instructions list dead code\n"
700  // NOLINTNEXTLINE(whitespace/line_length)
701  " --unreachable-functions list functions unreachable from the entry point\n"
702  // NOLINTNEXTLINE(whitespace/line_length)
703  " --reachable-functions list functions reachable from the entry point\n"
704  "\n"
705  "Abstract interpreter options:\n"
706  // NOLINTNEXTLINE(whitespace/line_length)
707  " --recursive-interprocedural use recursion to handle interprocedural reasoning\n"
708  // NOLINTNEXTLINE(whitespace/line_length)
709  " --three-way-merge use VSD's three-way merge on return from function call\n"
710  // NOLINTNEXTLINE(whitespace/line_length)
711  " --legacy-ait recursion for function and one domain per location\n"
712  // NOLINTNEXTLINE(whitespace/line_length)
713  " --legacy-concurrent legacy-ait with an extended fixed-point for concurrency\n"
714  "\n"
715  "History options:\n"
716  // NOLINTNEXTLINE(whitespace/line_length)
717  " --ahistorical the most basic history, tracks locations only\n"
718  // NOLINTNEXTLINE(whitespace/line_length)
719  " --call-stack n track the calling location stack for each function\n"
720  // NOLINTNEXTLINE(whitespace/line_length)
721  " limiting to at most n recursive loops, 0 to disable\n"
722  // NOLINTNEXTLINE(whitespace/line_length)
723  " --loop-unwind n track the number of loop iterations within a function\n"
724  // NOLINTNEXTLINE(whitespace/line_length)
725  " limited to n histories per location, 0 is unlimited\n"
726  // NOLINTNEXTLINE(whitespace/line_length)
727  " --branching n track the forwards jumps (if, switch, etc.) within a function\n"
728  // NOLINTNEXTLINE(whitespace/line_length)
729  " limited to n histories per location, 0 is unlimited\n"
730  // NOLINTNEXTLINE(whitespace/line_length)
731  " --loop-unwind-and-branching n track all local control flow\n"
732  // NOLINTNEXTLINE(whitespace/line_length)
733  " limited to n histories per location, 0 is unlimited\n"
734  "\n"
735  "Domain options:\n"
736  " --constants a constant for each variable if possible\n"
737  " --intervals an interval for each variable\n"
738  " --non-null tracks which pointers are non-null\n"
739  " --dependence-graph data and control dependencies between instructions\n" // NOLINT(*)
740  " --vsd a configurable non-relational domain\n" // NOLINT(*)
741  " --dependence-graph-vs dependencies between instructions using VSD\n" // NOLINT(*)
742  "\n"
743  "Variable sensitivity domain (VSD) options:\n"
744  HELP_VSD
745  "\n"
746  "Storage options:\n"
747  // NOLINTNEXTLINE(whitespace/line_length)
748  " --one-domain-per-history stores a domain for each history object created\n"
749  " --one-domain-per-location stores a domain for each location reached\n"
750  "\n"
751  "Output options:\n"
752  " --text file_name output results in plain text to given file\n"
753  // NOLINTNEXTLINE(whitespace/line_length)
754  " --json file_name output results in JSON format to given file\n"
755  " --xml file_name output results in XML format to given file\n"
756  " --dot file_name output results in DOT format to given file\n"
757  "\n"
758  "Specific analyses:\n"
759  // NOLINTNEXTLINE(whitespace/line_length)
760  " --taint file_name perform taint analysis using rules in given file\n"
761  "\n"
762  "C/C++ frontend options:\n"
765  "\n"
766  "Platform options:\n"
768  "\n"
769  "Program representations:\n"
770  " --show-parse-tree show parse tree\n"
771  " --show-symbol-table show loaded symbol table\n"
774  "\n"
775  "Program instrumentation options:\n"
778  "\n"
779  "Other options:\n"
781  " --version show version and exit\n"
782  HELP_FLUSH
784  "\n";
785  // clang-format on
786 }
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 ...
Abstract Interpretation.
void cprover_c_library_factory(const std::set< irep_idt > &functions, symbol_tablet &symbol_table, message_handlert &message_handler)
std::unique_ptr< ai_baset > build_analyzer(const optionst &options, const goto_modelt &goto_model, const namespacet &ns, message_handlert &mh)
Ideally this should be a pure function of options.
std::string get_value(char option) const
Definition: cmdline.cpp:47
virtual bool isset(char option) const
Definition: cmdline.cpp:29
argst args
Definition: cmdline.h:143
const std::list< std::string > & get_values(const std::string &option) const
Definition: cmdline.cpp:108
bool set(const cmdlinet &cmdline)
Definition: config.cpp:798
struct configt::ansi_ct ansi_c
virtual int doit() override
invoke main modules
virtual void get_command_line_options(optionst &options)
goto_analyzer_parse_optionst(int argc, const char **argv)
virtual bool process_goto_program(const optionst &options)
virtual int perform_analysis(const optionst &options)
Depending on the command line mode, run one of the analysis tasks.
virtual void help() override
display command line help
function_mapt function_map
void validate(const validation_modet vm=validation_modet::INVARIANT, const goto_model_validation_optionst &goto_model_validation_options=goto_model_validation_optionst{}) const override
Check that the goto model is well-formed.
Definition: goto_model.h:98
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
std::string what() const override
A human readable description of what went wrong.
void output(std::ostream &out, const goto_functiont &goto_function, const namespacet &ns) const
static unsigned eval_verbosity(const std::string &user_input, const message_levelt default_verbosity, message_handlert &dest)
Parse a (user-)provided string as a verbosity level and set it as the verbosity of dest.
Definition: message.cpp:105
mstreamt & error() const
Definition: message.h:399
mstreamt & status() const
Definition: message.h:414
@ M_STATISTICS
Definition: message.h:171
static eomt eom
Definition: message.h:297
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
bool get_bool_option(const std::string &option) const
Definition: options.cpp:44
void set_option(const std::string &option, const bool value)
Definition: options.cpp:28
const std::string get_option(const std::string &option) const
Definition: options.cpp:67
virtual void usage_error()
void log_version_and_architecture(const std::string &front_end)
Write version and system architecture to log.status().
ui_message_handlert ui_message_handler
Definition: parse_options.h:45
configt config
Definition: config.cpp:25
#define HELP_CONFIG_LIBRARY
Definition: config.h:63
#define HELP_CONFIG_PLATFORM
Definition: config.h:82
#define HELP_CONFIG_C_CPP
Definition: config.h:34
void cprover_cpp_library_factory(const std::set< irep_idt > &functions, symbol_tablet &symbol_table, message_handlert &message_handler)
Document and give macros for the exit codes of CPROVER binaries.
#define CPROVER_EXIT_INTERNAL_ERROR
An error has been encountered during processing the requested analysis.
Definition: exit_codes.h:45
#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
#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
#define CPROVER_EXIT_USAGE_ERROR
A usage error is returned when the command line is invalid or conflicting.
Definition: exit_codes.h:33
#define CPROVER_EXIT_SUCCESS
Success indicates the required analysis has been performed without error.
Definition: exit_codes.h:16
Goto-Analyser Command Line Option Processing.
#define GOTO_ANALYSER_OPTIONS
#define PARSE_OPTIONS_GOTO_CHECK(cmdline, options)
Definition: goto_check.h:70
#define HELP_GOTO_CHECK
Definition: goto_check.h:49
goto_modelt initialize_goto_model(const std::vector< std::string > &files, message_handlert &message_handler, const optionst &options)
Initialize a Goto Program.
static std::string binary(const constant_exprt &src)
Definition: json_expr.cpp:205
Field-insensitive, location-sensitive may-alias analysis.
Options.
std::string align_center_with_border(const std::string &text)
Utility for displaying help centered messages borderered by "* *".
std::string banner_string(const std::string &front_end, const std::string &version)
#define HELP_FUNCTIONS
void remove_asm(goto_functionst &goto_functions, symbol_tablet &symbol_table)
Replaces inline assembly instructions in the goto program (i.e., instructions of kind OTHER with a co...
Definition: remove_asm.cpp:511
Remove 'asm' statements by compiling them into suitable standard goto program instructions.
void set_properties(goto_programt &goto_program, std::unordered_set< irep_idt > &property_set)
void label_properties(goto_modelt &goto_model)
Set the properties to check.
void show_goto_functions(const namespacet &ns, ui_message_handlert &ui_message_handler, const goto_functionst &goto_functions, bool list_only)
#define HELP_SHOW_GOTO_FUNCTIONS
void show_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
void show_properties(const namespacet &ns, const irep_idt &identifier, message_handlert &message_handler, ui_message_handlert::uit ui, const goto_programt &goto_program)
Show the properties.
#define HELP_SHOW_PROPERTIES
void show_symbol_table(const symbol_tablet &symbol_table, ui_message_handlert &ui)
Show the symbol table.
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
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.
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.
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.
irep_idt arch
Definition: config.h:164
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)
Taint Analysis.
#define HELP_TIMESTAMP
Definition: timestamper.h:14
#define HELP_FLUSH
Definition: ui_message.h:108
bool static_unreachable_functions(const goto_modelt &goto_model, const ai_baset &ai, const optionst &options, std::ostream &out)
bool static_unreachable_instructions(const goto_modelt &goto_model, const ai_baset &ai, const optionst &options, std::ostream &out)
bool static_reachable_functions(const goto_modelt &goto_model, const ai_baset &ai, const optionst &options, std::ostream &out)
void unreachable_functions(const goto_modelt &goto_model, const bool json, std::ostream &os)
static void unreachable_instructions(const goto_programt &goto_program, dead_mapt &dest)
void reachable_functions(const goto_modelt &goto_model, const bool json, std::ostream &os)
List all unreachable instructions.
#define HELP_VALIDATE
#define HELP_VSD
#define PARSE_OPTIONS_VSD(cmdline, options)
const char * CBMC_VERSION