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  options.set_option("remove-returns", true);
392 
393  if(process_goto_program(options))
395 
396  if(cmdline.isset("validate-goto-model"))
397  {
399  }
400 
401  // show it?
402  if(cmdline.isset("show-symbol-table"))
403  {
405  return CPROVER_EXIT_SUCCESS;
406  }
407 
408  // show it?
409  if(
410  cmdline.isset("show-goto-functions") ||
411  cmdline.isset("list-goto-functions"))
412  {
414  goto_model, ui_message_handler, cmdline.isset("list-goto-functions"));
415  return CPROVER_EXIT_SUCCESS;
416  }
417 
418  return perform_analysis(options);
419 }
420 
423 {
424  if(options.get_bool_option("taint"))
425  {
426  std::string taint_file=cmdline.get_value("taint");
427 
428  if(cmdline.isset("show-taint"))
429  {
430  taint_analysis(goto_model, taint_file, ui_message_handler, true);
431  return CPROVER_EXIT_SUCCESS;
432  }
433  else
434  {
435  std::string json_file=cmdline.get_value("json");
436  bool result = taint_analysis(
437  goto_model, taint_file, ui_message_handler, false, json_file);
439  }
440  }
441 
442  // If no domain is given, this lightweight version of the analysis is used.
443  if(options.get_bool_option("unreachable-instructions") &&
444  options.get_bool_option("specific-analysis"))
445  {
446  const std::string json_file=cmdline.get_value("json");
447 
448  if(json_file.empty())
449  unreachable_instructions(goto_model, false, std::cout);
450  else if(json_file=="-")
451  unreachable_instructions(goto_model, true, std::cout);
452  else
453  {
454  std::ofstream ofs(json_file);
455  if(!ofs)
456  {
457  log.error() << "Failed to open json output '" << json_file << "'"
458  << messaget::eom;
460  }
461 
463  }
464 
465  return CPROVER_EXIT_SUCCESS;
466  }
467 
468  if(options.get_bool_option("unreachable-functions") &&
469  options.get_bool_option("specific-analysis"))
470  {
471  const std::string json_file=cmdline.get_value("json");
472 
473  if(json_file.empty())
474  unreachable_functions(goto_model, false, std::cout);
475  else if(json_file=="-")
476  unreachable_functions(goto_model, true, std::cout);
477  else
478  {
479  std::ofstream ofs(json_file);
480  if(!ofs)
481  {
482  log.error() << "Failed to open json output '" << json_file << "'"
483  << messaget::eom;
485  }
486 
487  unreachable_functions(goto_model, true, ofs);
488  }
489 
490  return CPROVER_EXIT_SUCCESS;
491  }
492 
493  if(options.get_bool_option("reachable-functions") &&
494  options.get_bool_option("specific-analysis"))
495  {
496  const std::string json_file=cmdline.get_value("json");
497 
498  if(json_file.empty())
499  reachable_functions(goto_model, false, std::cout);
500  else if(json_file=="-")
501  reachable_functions(goto_model, true, std::cout);
502  else
503  {
504  std::ofstream ofs(json_file);
505  if(!ofs)
506  {
507  log.error() << "Failed to open json output '" << json_file << "'"
508  << messaget::eom;
510  }
511 
512  reachable_functions(goto_model, true, ofs);
513  }
514 
515  return CPROVER_EXIT_SUCCESS;
516  }
517 
518  if(options.get_bool_option("show-local-may-alias"))
519  {
521 
522  for(const auto &gf_entry : goto_model.goto_functions.function_map)
523  {
524  std::cout << ">>>>\n";
525  std::cout << ">>>> " << gf_entry.first << '\n';
526  std::cout << ">>>>\n";
527  local_may_aliast local_may_alias(gf_entry.second);
528  local_may_alias.output(std::cout, gf_entry.second, ns);
529  std::cout << '\n';
530  }
531 
532  return CPROVER_EXIT_SUCCESS;
533  }
534 
536 
537  if(cmdline.isset("show-properties"))
538  {
540  return CPROVER_EXIT_SUCCESS;
541  }
542 
543  if(cmdline.isset("property"))
545 
546  if(options.get_bool_option("general-analysis"))
547  {
548  // Output file factory
549  const std::string outfile=options.get_option("outfile");
550 
551  std::ofstream output_stream;
552  if(outfile != "-" && !outfile.empty())
553  output_stream.open(outfile);
554 
555  std::ostream &out(
556  (outfile == "-" || outfile.empty()) ? std::cout : output_stream);
557 
558  if(!out)
559  {
560  log.error() << "Failed to open output file '" << outfile << "'"
561  << messaget::eom;
563  }
564 
565  // Build analyzer
566  log.status() << "Selecting abstract domain" << messaget::eom;
567  namespacet ns(goto_model.symbol_table); // Must live as long as the domain.
568  std::unique_ptr<ai_baset> analyzer;
569 
570  try
571  {
572  analyzer = build_analyzer(options, goto_model, ns, ui_message_handler);
573  }
575  {
576  log.error() << e.what() << messaget::eom;
578  }
579 
580  if(analyzer == nullptr)
581  {
582  log.status() << "Task / Interpreter combination not supported"
583  << messaget::eom;
585  }
586 
587  // Run
588  log.status() << "Computing abstract states" << messaget::eom;
589  (*analyzer)(goto_model);
590 
591  // Perform the task
592  log.status() << "Performing task" << messaget::eom;
593 
594  bool result = true;
595 
596  if(options.get_bool_option("show"))
597  {
598  static_show_domain(goto_model, *analyzer, options, out);
599  return CPROVER_EXIT_SUCCESS;
600  }
601  else if(options.get_bool_option("show-on-source"))
602  {
604  return CPROVER_EXIT_SUCCESS;
605  }
606  else if(options.get_bool_option("verify"))
607  {
608  result = static_verifier(
609  goto_model, *analyzer, options, ui_message_handler, out);
610  }
611  else if(options.get_bool_option("simplify"))
612  {
613  PRECONDITION(!outfile.empty() && outfile != "-");
614  output_stream.close();
615  output_stream.open(outfile, std::ios::binary);
616  result = static_simplifier(
617  goto_model, *analyzer, options, ui_message_handler, out);
618  }
619  else if(options.get_bool_option("unreachable-instructions"))
620  {
622  *analyzer,
623  options,
624  out);
625  }
626  else if(options.get_bool_option("unreachable-functions"))
627  {
629  *analyzer,
630  options,
631  out);
632  }
633  else if(options.get_bool_option("reachable-functions"))
634  {
636  *analyzer,
637  options,
638  out);
639  }
640  else
641  {
642  log.error() << "Unhandled task" << messaget::eom;
644  }
645 
646  return result ?
648  }
649 
650  // Final defensive error case
651  log.error() << "no analysis option given -- consider reading --help"
652  << messaget::eom;
654 }
655 
657  const optionst &options)
658 {
659  // Remove inline assembler; this needs to happen before
660  // adding the library.
662 
663  // add the library
664  log.status() << "Adding CPROVER library (" << config.ansi_c.arch << ")"
665  << messaget::eom;
668 
669  // Common removal of types and complex constructs
670  if(::process_goto_program(goto_model, options, log))
671  return true;
672 
673  return false;
674 }
675 
678 {
679  // clang-format off
680  std::cout << '\n' << banner_string("GOTO-ANALYZER", CBMC_VERSION) << '\n'
681  << align_center_with_border("Copyright (C) 2017-2018") << '\n'
682  << align_center_with_border("Daniel Kroening, Diffblue") << '\n'
683  << align_center_with_border("kroening@kroening.com") << '\n'
684  <<
685  "\n"
686  "Usage: Purpose:\n"
687  "\n"
688  " goto-analyzer [-h] [--help] show help\n"
689  " goto-analyzer file.c ... source file names\n"
690  "\n"
691  "Task options:\n"
692  " --show display the abstract states on the goto program\n" // NOLINT(*)
693  " --show-on-source display the abstract states on the source\n"
694  // NOLINTNEXTLINE(whitespace/line_length)
695  " --verify use the abstract domains to check assertions\n"
696  // NOLINTNEXTLINE(whitespace/line_length)
697  " --simplify file_name use the abstract domains to simplify the program\n"
698  " --unreachable-instructions list dead code\n"
699  // NOLINTNEXTLINE(whitespace/line_length)
700  " --unreachable-functions list functions unreachable from the entry point\n"
701  // NOLINTNEXTLINE(whitespace/line_length)
702  " --reachable-functions list functions reachable from the entry point\n"
703  "\n"
704  "Abstract interpreter options:\n"
705  // NOLINTNEXTLINE(whitespace/line_length)
706  " --recursive-interprocedural use recursion to handle interprocedural reasoning\n"
707  // NOLINTNEXTLINE(whitespace/line_length)
708  " --three-way-merge use VSD's three-way merge on return from function call\n"
709  // NOLINTNEXTLINE(whitespace/line_length)
710  " --legacy-ait recursion for function and one domain per location\n"
711  // NOLINTNEXTLINE(whitespace/line_length)
712  " --legacy-concurrent legacy-ait with an extended fixed-point for concurrency\n"
713  "\n"
714  "History options:\n"
715  // NOLINTNEXTLINE(whitespace/line_length)
716  " --ahistorical the most basic history, tracks locations only\n"
717  // NOLINTNEXTLINE(whitespace/line_length)
718  " --call-stack n track the calling location stack for each function\n"
719  // NOLINTNEXTLINE(whitespace/line_length)
720  " limiting to at most n recursive loops, 0 to disable\n"
721  // NOLINTNEXTLINE(whitespace/line_length)
722  " --loop-unwind n track the number of loop iterations within a function\n"
723  // NOLINTNEXTLINE(whitespace/line_length)
724  " limited to n histories per location, 0 is unlimited\n"
725  // NOLINTNEXTLINE(whitespace/line_length)
726  " --branching n track the forwards jumps (if, switch, etc.) within a function\n"
727  // NOLINTNEXTLINE(whitespace/line_length)
728  " limited to n histories per location, 0 is unlimited\n"
729  // NOLINTNEXTLINE(whitespace/line_length)
730  " --loop-unwind-and-branching n track all local control flow\n"
731  // NOLINTNEXTLINE(whitespace/line_length)
732  " limited to n histories per location, 0 is unlimited\n"
733  "\n"
734  "Domain options:\n"
735  " --constants a constant for each variable if possible\n"
736  " --intervals an interval for each variable\n"
737  " --non-null tracks which pointers are non-null\n"
738  " --dependence-graph data and control dependencies between instructions\n" // NOLINT(*)
739  " --vsd a configurable non-relational domain\n" // NOLINT(*)
740  " --dependence-graph-vs dependencies between instructions using VSD\n" // NOLINT(*)
741  "\n"
742  "Variable sensitivity domain (VSD) options:\n"
743  HELP_VSD
744  "\n"
745  "Storage options:\n"
746  // NOLINTNEXTLINE(whitespace/line_length)
747  " --one-domain-per-history stores a domain for each history object created\n"
748  " --one-domain-per-location stores a domain for each location reached\n"
749  "\n"
750  "Output options:\n"
751  " --text file_name output results in plain text to given file\n"
752  // NOLINTNEXTLINE(whitespace/line_length)
753  " --json file_name output results in JSON format to given file\n"
754  " --xml file_name output results in XML format to given file\n"
755  " --dot file_name output results in DOT format to given file\n"
756  "\n"
757  "Specific analyses:\n"
758  // NOLINTNEXTLINE(whitespace/line_length)
759  " --taint file_name perform taint analysis using rules in given file\n"
760  "\n"
761  "C/C++ frontend options:\n"
764  "\n"
765  "Platform options:\n"
767  "\n"
768  "Program representations:\n"
769  " --show-parse-tree show parse tree\n"
770  " --show-symbol-table show loaded symbol table\n"
773  "\n"
774  "Program instrumentation options:\n"
777  "\n"
778  "Other options:\n"
780  " --version show version and exit\n"
781  HELP_FLUSH
783  "\n";
784  // clang-format on
785 }
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:48
virtual bool isset(char option) const
Definition: cmdline.cpp:30
argst args
Definition: cmdline.h:145
const std::list< std::string > & get_values(const std::string &option) const
Definition: cmdline.cpp:109
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:62
#define HELP_CONFIG_PLATFORM
Definition: config.h:81
#define HELP_CONFIG_C_CPP
Definition: config.h:33
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_c.h:74
#define HELP_GOTO_CHECK
Definition: goto_check_c.h:53
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:206
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:512
Remove 'asm' statements by compiling them into suitable standard goto program instructions.
Replace function returns by assignments to global variables.
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:191
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