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