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 <cpp/cpp_language.h>
23 #include <cpp/cprover_library.h>
24 
25 #include <jsil/jsil_language.h>
26 
42 
43 #include <analyses/is_threaded.h>
44 #include <analyses/goto_check.h>
49 
50 #include <langapi/mode.h>
51 #include <langapi/language.h>
52 
53 #include <util/config.h>
54 #include <util/exception_utils.h>
55 #include <util/exit_codes.h>
56 #include <util/options.h>
57 #include <util/unicode.h>
58 #include <util/version.h>
59 
60 #include "show_on_source.h"
61 #include "static_show_domain.h"
62 #include "static_simplifier.h"
63 #include "static_verifier.h"
64 #include "taint_analysis.h"
66 
68  int argc,
69  const char **argv)
71  messaget(ui_message_handler),
72  ui_message_handler(cmdline, std::string("GOTO-ANALYZER ") + CBMC_VERSION)
73 {
74 }
75 
77 {
81 }
82 
84 {
85  if(config.set(cmdline))
86  {
87  usage_error();
89  }
90 
91  if(cmdline.isset("function"))
92  options.set_option("function", cmdline.get_value("function"));
93 
94 #if 0
95  if(cmdline.isset("c89"))
97 
98  if(cmdline.isset("c99"))
100 
101  if(cmdline.isset("c11"))
103 
104  if(cmdline.isset("cpp98"))
105  config.cpp.set_cpp98();
106 
107  if(cmdline.isset("cpp03"))
108  config.cpp.set_cpp03();
109 
110  if(cmdline.isset("cpp11"))
111  config.cpp.set_cpp11();
112 #endif
113 
114 #if 0
115  // check assertions
116  if(cmdline.isset("no-assertions"))
117  options.set_option("assertions", false);
118  else
119  options.set_option("assertions", true);
120 
121  // use assumptions
122  if(cmdline.isset("no-assumptions"))
123  options.set_option("assumptions", false);
124  else
125  options.set_option("assumptions", true);
126 
127  // magic error label
128  if(cmdline.isset("error-label"))
129  options.set_option("error-label", cmdline.get_values("error-label"));
130 #endif
131 
132  // Select a specific analysis
133  if(cmdline.isset("taint"))
134  {
135  options.set_option("taint", true);
136  options.set_option("specific-analysis", true);
137  }
138  // For backwards compatibility,
139  // these are first recognised as specific analyses
140  bool reachability_task = false;
141  if(cmdline.isset("unreachable-instructions"))
142  {
143  options.set_option("unreachable-instructions", true);
144  options.set_option("specific-analysis", true);
145  reachability_task = true;
146  }
147  if(cmdline.isset("unreachable-functions"))
148  {
149  options.set_option("unreachable-functions", true);
150  options.set_option("specific-analysis", true);
151  reachability_task = true;
152  }
153  if(cmdline.isset("reachable-functions"))
154  {
155  options.set_option("reachable-functions", true);
156  options.set_option("specific-analysis", true);
157  reachability_task = true;
158  }
159  if(cmdline.isset("show-local-may-alias"))
160  {
161  options.set_option("show-local-may-alias", true);
162  options.set_option("specific-analysis", true);
163  }
164 
165  // Output format choice
166  if(cmdline.isset("text"))
167  {
168  options.set_option("text", true);
169  options.set_option("outfile", cmdline.get_value("text"));
170  }
171  else if(cmdline.isset("json"))
172  {
173  options.set_option("json", true);
174  options.set_option("outfile", cmdline.get_value("json"));
175  }
176  else if(cmdline.isset("xml"))
177  {
178  options.set_option("xml", true);
179  options.set_option("outfile", cmdline.get_value("xml"));
180  }
181  else if(cmdline.isset("dot"))
182  {
183  options.set_option("dot", true);
184  options.set_option("outfile", cmdline.get_value("dot"));
185  }
186 
187  // The use should either select:
188  // 1. a specific analysis, or
189  // 2. a triple of task / analyzer / domain, or
190  // 3. one of the general display options
191 
192  // Task options
193  if(cmdline.isset("show"))
194  {
195  options.set_option("show", true);
196  options.set_option("general-analysis", true);
197  }
198  else if(cmdline.isset("show-on-source"))
199  {
200  options.set_option("show-on-source", true);
201  options.set_option("general-analysis", true);
202  }
203  else if(cmdline.isset("verify"))
204  {
205  options.set_option("verify", true);
206  options.set_option("general-analysis", true);
207  }
208  else if(cmdline.isset("simplify"))
209  {
210  if(cmdline.get_value("simplify") == "-")
212  "cannot output goto binary to stdout", "--simplify");
213 
214  options.set_option("simplify", true);
215  options.set_option("outfile", cmdline.get_value("simplify"));
216  options.set_option("general-analysis", true);
217 
218  // For development allow slicing to be disabled in the simplify task
219  options.set_option(
220  "simplify-slicing",
221  !(cmdline.isset("no-simplify-slicing")));
222  }
223  else if(cmdline.isset("show-intervals"))
224  {
225  // For backwards compatibility
226  options.set_option("show", true);
227  options.set_option("general-analysis", true);
228  options.set_option("intervals", true);
229  options.set_option("domain set", true);
230  }
231  else if(cmdline.isset("show-non-null"))
232  {
233  // For backwards compatibility
234  options.set_option("show", true);
235  options.set_option("general-analysis", true);
236  options.set_option("non-null", true);
237  options.set_option("domain set", true);
238  }
239  else if(cmdline.isset("intervals") || cmdline.isset("non-null"))
240  {
241  // Partial backwards compatability, just giving these domains without
242  // a task will work. However it will use the general default of verify
243  // rather than their historical default of show.
244  options.set_option("verify", true);
245  options.set_option("general-analysis", true);
246  }
247 
248  if(options.get_bool_option("general-analysis") || reachability_task)
249  {
250  // Abstract interpreter choice
251  if(cmdline.isset("location-sensitive"))
252  options.set_option("location-sensitive", true);
253  else if(cmdline.isset("concurrent"))
254  options.set_option("concurrent", true);
255  else
256  {
257  // Silently default to location-sensitive as it's the "default"
258  // view of abstract interpretation.
259  options.set_option("location-sensitive", true);
260  }
261 
262  // Domain choice
263  if(cmdline.isset("constants"))
264  {
265  options.set_option("constants", true);
266  options.set_option("domain set", true);
267  }
268  else if(cmdline.isset("dependence-graph"))
269  {
270  options.set_option("dependence-graph", true);
271  options.set_option("domain set", true);
272  }
273  else if(cmdline.isset("intervals"))
274  {
275  options.set_option("intervals", true);
276  options.set_option("domain set", true);
277  }
278  else if(cmdline.isset("non-null"))
279  {
280  options.set_option("non-null", true);
281  options.set_option("domain set", true);
282  }
283 
284  // Reachability questions, when given with a domain swap from specific
285  // to general tasks so that they can use the domain & parameterisations.
286  if(reachability_task)
287  {
288  if(options.get_bool_option("domain set"))
289  {
290  options.set_option("specific-analysis", false);
291  options.set_option("general-analysis", true);
292  }
293  }
294  else
295  {
296  if(!options.get_bool_option("domain set"))
297  {
298  // Default to constants as it is light-weight but useful
299  status() << "Domain not specified, defaulting to --constants" << eom;
300  options.set_option("constants", true);
301  }
302  }
303  }
304 
305  if(cmdline.isset("validate-goto-model"))
306  {
307  options.set_option("validate-goto-model", true);
308  }
309 }
310 
315  const optionst &options,
316  const namespacet &ns)
317 {
318  ai_baset *domain = nullptr;
319 
320  if(options.get_bool_option("location-sensitive"))
321  {
322  if(options.get_bool_option("constants"))
323  {
324  // constant_propagator_ait derives from ait<constant_propagator_domaint>
326  }
327  else if(options.get_bool_option("dependence-graph"))
328  {
329  domain=new dependence_grapht(ns);
330  }
331  else if(options.get_bool_option("intervals"))
332  {
333  domain=new ait<interval_domaint>();
334  }
335 #if 0
336  // Not actually implemented, despite the option...
337  else if(options.get_bool_option("non-null"))
338  {
339  domain=new ait<non_null_domaint>();
340  }
341 #endif
342  }
343  else if(options.get_bool_option("concurrent"))
344  {
345 #if 0
346  // Disabled until merge_shared is implemented for these
347  if(options.get_bool_option("constants"))
348  {
350  }
351  else if(options.get_bool_option("dependence-graph"))
352  {
353  domain=new dependence_grapht(ns);
354  }
355  else if(options.get_bool_option("intervals"))
356  {
358  }
359 #if 0
360  // Not actually implemented, despite the option...
361  else if(options.get_bool_option("non-null"))
362  {
364  }
365 #endif
366 #endif
367  }
368 
369  return domain;
370 }
371 
374 {
375  if(cmdline.isset("version"))
376  {
377  std::cout << CBMC_VERSION << '\n';
378  return CPROVER_EXIT_SUCCESS;
379  }
380 
381  //
382  // command line options
383  //
384 
385  optionst options;
386  get_command_line_options(options);
389 
390  //
391  // Print a banner
392  //
393  status() << "GOTO-ANALYSER version " << CBMC_VERSION << " "
394  << sizeof(void *) * 8 << "-bit " << config.this_architecture() << " "
396 
398 
399  try
400  {
401  goto_model =
403  }
404 
405  catch(const char *e)
406  {
407  error() << e << eom;
408  return CPROVER_EXIT_EXCEPTION;
409  }
410 
411  catch(const std::string &e)
412  {
413  error() << e << eom;
414  return CPROVER_EXIT_EXCEPTION;
415  }
416 
417  catch(int e)
418  {
419  error() << "Numeric exception: " << e << eom;
420  return CPROVER_EXIT_EXCEPTION;
421  }
422 
423  if(process_goto_program(options))
425 
426  if(cmdline.isset("validate-goto-model"))
427  {
429  }
430 
431  // show it?
432  if(cmdline.isset("show-symbol-table"))
433  {
435  return CPROVER_EXIT_SUCCESS;
436  }
437 
438  // show it?
439  if(
440  cmdline.isset("show-goto-functions") ||
441  cmdline.isset("list-goto-functions"))
442  {
444  goto_model,
446  get_ui(),
447  cmdline.isset("list-goto-functions"));
448  return CPROVER_EXIT_SUCCESS;
449  }
450 
451  try
452  {
453  return perform_analysis(options);
454  }
455 
456  catch(const char *e)
457  {
458  error() << e << eom;
459  return CPROVER_EXIT_EXCEPTION;
460  }
461 
462  catch(const std::string &e)
463  {
464  error() << e << eom;
465  return CPROVER_EXIT_EXCEPTION;
466  }
467 
468  catch(int e)
469  {
470  error() << "Numeric exception: " << e << eom;
471  return CPROVER_EXIT_EXCEPTION;
472  }
473 
474  catch(const std::bad_alloc &)
475  {
476  error() << "Out of memory" << eom;
478  }
479 }
480 
481 
484 {
486  if(options.get_bool_option("taint"))
487  {
488  std::string taint_file=cmdline.get_value("taint");
489 
490  if(cmdline.isset("show-taint"))
491  {
492  taint_analysis(goto_model, taint_file, get_message_handler(), true, "");
493  return CPROVER_EXIT_SUCCESS;
494  }
495  else
496  {
497  std::string json_file=cmdline.get_value("json");
498  bool result=
500  goto_model, taint_file, get_message_handler(), false, json_file);
502  }
503  }
504 
505  // If no domain is given, this lightweight version of the analysis is used.
506  if(options.get_bool_option("unreachable-instructions") &&
507  options.get_bool_option("specific-analysis"))
508  {
509  const std::string json_file=cmdline.get_value("json");
510 
511  if(json_file.empty())
512  unreachable_instructions(goto_model, false, std::cout);
513  else if(json_file=="-")
514  unreachable_instructions(goto_model, true, std::cout);
515  else
516  {
517  std::ofstream ofs(json_file);
518  if(!ofs)
519  {
520  error() << "Failed to open json output `"
521  << json_file << "'" << eom;
523  }
524 
526  }
527 
528  return CPROVER_EXIT_SUCCESS;
529  }
530 
531  if(options.get_bool_option("unreachable-functions") &&
532  options.get_bool_option("specific-analysis"))
533  {
534  const std::string json_file=cmdline.get_value("json");
535 
536  if(json_file.empty())
537  unreachable_functions(goto_model, false, std::cout);
538  else if(json_file=="-")
539  unreachable_functions(goto_model, true, std::cout);
540  else
541  {
542  std::ofstream ofs(json_file);
543  if(!ofs)
544  {
545  error() << "Failed to open json output `"
546  << json_file << "'" << eom;
548  }
549 
550  unreachable_functions(goto_model, true, ofs);
551  }
552 
553  return CPROVER_EXIT_SUCCESS;
554  }
555 
556  if(options.get_bool_option("reachable-functions") &&
557  options.get_bool_option("specific-analysis"))
558  {
559  const std::string json_file=cmdline.get_value("json");
560 
561  if(json_file.empty())
562  reachable_functions(goto_model, false, std::cout);
563  else if(json_file=="-")
564  reachable_functions(goto_model, true, std::cout);
565  else
566  {
567  std::ofstream ofs(json_file);
568  if(!ofs)
569  {
570  error() << "Failed to open json output `"
571  << json_file << "'" << eom;
573  }
574 
575  reachable_functions(goto_model, true, ofs);
576  }
577 
578  return CPROVER_EXIT_SUCCESS;
579  }
580 
581  if(options.get_bool_option("show-local-may-alias"))
582  {
584 
586  {
587  std::cout << ">>>>\n";
588  std::cout << ">>>> " << it->first << '\n';
589  std::cout << ">>>>\n";
590  local_may_aliast local_may_alias(it->second);
591  local_may_alias.output(std::cout, it->second, ns);
592  std::cout << '\n';
593  }
594 
595  return CPROVER_EXIT_SUCCESS;
596  }
597 
599 
600  if(cmdline.isset("show-properties"))
601  {
603  return CPROVER_EXIT_SUCCESS;
604  }
605 
606  if(set_properties())
608 
609  if(options.get_bool_option("general-analysis"))
610  {
611  // Output file factory
612  const std::string outfile=options.get_option("outfile");
613 
614  std::ofstream output_stream;
615  if(outfile != "-" && !outfile.empty())
616  output_stream.open(outfile);
617 
618  std::ostream &out(
619  (outfile == "-" || outfile.empty()) ? std::cout : output_stream);
620 
621  if(!out)
622  {
623  error() << "Failed to open output file `"
624  << outfile << "'" << eom;
626  }
627 
628  // Build analyzer
629  status() << "Selecting abstract domain" << eom;
630  namespacet ns(goto_model.symbol_table); // Must live as long as the domain.
631  std::unique_ptr<ai_baset> analyzer(build_analyzer(options, ns));
632 
633  if(analyzer == nullptr)
634  {
635  status() << "Task / Interpreter / Domain combination not supported"
636  << messaget::eom;
638  }
639 
640  // Run
641  status() << "Computing abstract states" << eom;
642  (*analyzer)(goto_model);
643 
644  // Perform the task
645  status() << "Performing task" << eom;
646 
647  bool result = true;
648 
649  if(options.get_bool_option("show"))
650  {
651  static_show_domain(goto_model, *analyzer, options, out);
652  return CPROVER_EXIT_SUCCESS;
653  }
654  else if(options.get_bool_option("show-on-source"))
655  {
657  return CPROVER_EXIT_SUCCESS;
658  }
659  else if(options.get_bool_option("verify"))
660  {
662  *analyzer,
663  options,
665  out);
666  }
667  else if(options.get_bool_option("simplify"))
668  {
669  PRECONDITION(!outfile.empty() && outfile != "-");
670  output_stream.close();
671  output_stream.open(outfile, std::ios::binary);
673  *analyzer,
674  options,
676  out);
677  }
678  else if(options.get_bool_option("unreachable-instructions"))
679  {
681  *analyzer,
682  options,
683  out);
684  }
685  else if(options.get_bool_option("unreachable-functions"))
686  {
688  *analyzer,
689  options,
690  out);
691  }
692  else if(options.get_bool_option("reachable-functions"))
693  {
695  *analyzer,
696  options,
697  out);
698  }
699  else
700  {
701  error() << "Unhandled task" << eom;
703  }
704 
705  return result ?
707  }
708 
709 
710  // Final defensive error case
711  error() << "no analysis option given -- consider reading --help"
712  << eom;
714 }
715 
717 {
718  try
719  {
720  if(cmdline.isset("property"))
722  }
723 
724  catch(const char *e)
725  {
726  error() << e << eom;
727  return true;
728  }
729 
730  catch(const std::string &e)
731  {
732  error() << e << eom;
733  return true;
734  }
735 
736  catch(int)
737  {
738  return true;
739  }
740 
741  return false;
742 }
743 
745  const optionst &options)
746 {
747  try
748  {
749  #if 0
750  // Remove inline assembler; this needs to happen before
751  // adding the library.
753 
754  // add the library
755  status() << "Adding CPROVER library (" << config.ansi_c.arch << ")" << eom;
759  #endif
760 
761  // remove function pointers
762  status() << "Removing function pointers and virtual functions" << eom;
764  get_message_handler(), goto_model, cmdline.isset("pointer-check"));
765 
766  // do partial inlining
767  status() << "Partial Inlining" << eom;
769 
770  // remove returns, gcc vectors, complex
774 
775 #if 0
776  // add generic checks
777  status() << "Generic Property Instrumentation" << eom;
778  goto_check(options, goto_model);
779 #else
780  (void)options; // unused parameter
781 #endif
782 
783  // recalculate numbers, etc.
785 
786  // add loop ids
788  }
789 
790  catch(const char *e)
791  {
792  error() << e << eom;
793  return true;
794  }
795 
796  catch(const std::string &e)
797  {
798  error() << e << eom;
799  return true;
800  }
801 
802  catch(int)
803  {
804  return true;
805  }
806 
807  catch(const std::bad_alloc &)
808  {
809  error() << "Out of memory" << eom;
810  return true;
811  }
812 
813  return false;
814 }
815 
818 {
819  // clang-format off
820  std::cout << '\n' << banner_string("GOTO-ANALYZER", CBMC_VERSION) << '\n'
821  <<
822  "* * Copyright (C) 2017-2018 * *\n"
823  "* * Daniel Kroening, Diffblue * *\n"
824  "* * kroening@kroening.com * *\n"
825  "\n"
826  "Usage: Purpose:\n"
827  "\n"
828  " goto-analyzer [-h] [--help] show help\n"
829  " goto-analyzer file.c ... source file names\n"
830  "\n"
831  "Task options:\n"
832  " --show display the abstract states on the goto program\n" // NOLINT(*)
833  " --show-on-source display the abstract states on the source\n"
834  // NOLINTNEXTLINE(whitespace/line_length)
835  " --verify use the abstract domains to check assertions\n"
836  // NOLINTNEXTLINE(whitespace/line_length)
837  " --simplify file_name use the abstract domains to simplify the program\n"
838  " --unreachable-instructions list dead code\n"
839  // NOLINTNEXTLINE(whitespace/line_length)
840  " --unreachable-functions list functions unreachable from the entry point\n"
841  // NOLINTNEXTLINE(whitespace/line_length)
842  " --reachable-functions list functions reachable from the entry point\n"
843  "\n"
844  "Abstract interpreter options:\n"
845  // NOLINTNEXTLINE(whitespace/line_length)
846  " --location-sensitive use location-sensitive abstract interpreter\n"
847  " --concurrent use concurrency-aware abstract interpreter\n"
848  "\n"
849  "Domain options:\n"
850  " --constants constant domain\n"
851  " --intervals interval domain\n"
852  " --non-null non-null domain\n"
853  " --dependence-graph data and control dependencies between instructions\n" // NOLINT(*)
854  "\n"
855  "Output options:\n"
856  " --text file_name output results in plain text to given file\n"
857  // NOLINTNEXTLINE(whitespace/line_length)
858  " --json file_name output results in JSON format to given file\n"
859  " --xml file_name output results in XML format to given file\n"
860  " --dot file_name output results in DOT format to given file\n"
861  "\n"
862  "Specific analyses:\n"
863  // NOLINTNEXTLINE(whitespace/line_length)
864  " --taint file_name perform taint analysis using rules in given file\n"
865  "\n"
866  "C/C++ frontend options:\n"
867  " -I path set include path (C/C++)\n"
868  " -D macro define preprocessor macro (C/C++)\n"
869  " --arch X set architecture (default: "
870  << configt::this_architecture() << ")\n"
871  " --os set operating system (default: "
872  << configt::this_operating_system() << ")\n"
873  " --c89/99/11 set C language standard (default: "
880  "c11":"") << ")\n"
881  " --cpp98/03/11 set C++ language standard (default: "
884  "cpp98":
887  "cpp03":
890  "cpp11":"") << ")\n"
891  #ifdef _WIN32
892  " --gcc use GCC as preprocessor\n"
893  #endif
894  " --no-library disable built-in abstract C library\n"
895  "\n"
897  "\n"
898  "Program representations:\n"
899  " --show-parse-tree show parse tree\n"
900  " --show-symbol-table show loaded symbol table\n"
903  "\n"
904  "Program instrumentation options:\n"
906  "\n"
907  "Other options:\n"
909  " --version show version and exit\n"
910  HELP_FLUSH
912  "\n";
913  // clang-format on
914 }
taint_analysis
bool taint_analysis(goto_modelt &goto_model, const std::string &taint_file_name, message_handlert &message_handler, bool show_full, const std::string &json_file_name)
Definition: taint_analysis.cpp:414
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:144
cprover_library.h
cmdlinet::args
argst args
Definition: cmdline.h:44
CBMC_VERSION
const char * CBMC_VERSION
Definition: version.cpp:1
exception_utils.h
configt::cppt::cpp_standardt::CPP98
HELP_SHOW_GOTO_FUNCTIONS
#define HELP_SHOW_GOTO_FUNCTIONS
Definition: show_goto_functions.h:26
local_may_aliast::output
void output(std::ostream &out, const goto_functiont &goto_function, const namespacet &ns) const
Definition: local_may_alias.cpp:438
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
configt::ansi_ct::set_c99
void set_c99()
Definition: config.h:52
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:17
cmdlinet::isset
virtual bool isset(char option) const
Definition: cmdline.cpp:27
dependence_grapht
Definition: dependence_graph.h:217
static_unreachable_instructions
bool static_unreachable_instructions(const goto_modelt &goto_model, const ai_baset &ai, const optionst &options, std::ostream &out)
Definition: unreachable_instructions.cpp:204
goto_inline.h
optionst
Definition: options.h:22
static_simplifier.h
goto_analyzer_parse_optionst::get_command_line_options
virtual void get_command_line_options(optionst &options)
Definition: goto_analyzer_parse_options.cpp:83
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
CPROVER_EXIT_INTERNAL_OUT_OF_MEMORY
#define CPROVER_EXIT_INTERNAL_OUT_OF_MEMORY
Memory allocation has failed and this has been detected within the program.
Definition: exit_codes.h:53
optionst::get_option
const std::string get_option(const std::string &option) const
Definition: options.cpp:65
messaget::M_STATISTICS
Definition: message.h:161
messaget::status
mstreamt & status() const
Definition: message.h:401
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:49
HELP_FUNCTIONS
#define HELP_FUNCTIONS
Definition: rebuild_goto_start_function.h:24
static_verifier.h
goto_partial_inline
void goto_partial_inline(goto_modelt &goto_model, message_handlert &message_handler, unsigned smallfunc_limit, bool adjust_function)
Inline all function calls to functions either marked as "inlined" or smaller than smallfunc_limit (by...
Definition: goto_inline.cpp:109
goto_analyzer_parse_options.h
configt::cppt::cpp_standardt::CPP03
static_verifier
bool static_verifier(const goto_modelt &goto_model, const ai_baset &ai, const optionst &options, message_handlert &message_handler, std::ostream &out)
Runs the analyzer and then prints out the domain.
Definition: static_verifier.cpp:234
show_goto_functions
void show_goto_functions(const namespacet &ns, message_handlert &message_handler, ui_message_handlert::uit ui, const goto_functionst &goto_functions, bool list_only)
Definition: show_goto_functions.cpp:28
taint_analysis.h
remove_virtual_functions.h
remove_asm.h
constant_propagator.h
jsil_language.h
ait
Definition: ai.h:365
CPROVER_EXIT_EXCEPTION
#define CPROVER_EXIT_EXCEPTION
An (unanticipated) exception was thrown during computation.
Definition: exit_codes.h:41
mode.h
options.h
CPROVER_EXIT_VERIFICATION_SAFE
#define CPROVER_EXIT_VERIFICATION_SAFE
Verification successful indicates the analysis has been performed without error AND the software is s...
Definition: exit_codes.h:21
optionst::set_option
void set_option(const std::string &option, const bool value)
Definition: options.cpp:26
configt::ansi_c
struct configt::ansi_ct ansi_c
messaget::eom
static eomt eom
Definition: message.h:284
show_symbol_table
void show_symbol_table(const symbol_tablet &symbol_table, ui_message_handlert &ui)
Definition: show_symbol_table.cpp:283
version.h
goto_analyzer_parse_optionst::build_analyzer
ai_baset * build_analyzer(const optionst &, const namespacet &ns)
For the task, build the appropriate kind of analyzer Ideally this should be a pure function of option...
Definition: goto_analyzer_parse_options.cpp:314
goto_analyzer_parse_optionst::goto_analyzer_parse_optionst
goto_analyzer_parse_optionst(int argc, const char **argv)
Definition: goto_analyzer_parse_options.cpp:67
local_may_aliast
Definition: local_may_alias.h:25
label_properties
void label_properties(goto_modelt &goto_model)
Definition: set_properties.cpp:43
goto_modelt::validate
void validate(const validation_modet vm) const
Check that the goto model is well-formed.
Definition: goto_model.h:97
parse_options_baset::usage_error
virtual void usage_error()
Definition: parse_options.cpp:36
new_cpp_language
std::unique_ptr< languaget > new_cpp_language()
Definition: cpp_language.cpp:197
reachable_functions
void reachable_functions(const goto_modelt &goto_model, const bool json, std::ostream &os)
Definition: unreachable_instructions.cpp:392
remove_vector
static void remove_vector(typet &)
removes vector data type
Definition: remove_vector.cpp:167
configt::cppt::set_cpp98
void set_cpp98()
Definition: config.h:140
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
remove_complex.h
set_properties.h
configt::ansi_ct::c_standardt::C89
messaget::result
mstreamt & result() const
Definition: message.h:396
unreachable_functions
void unreachable_functions(const goto_modelt &goto_model, const bool json, std::ostream &os)
Definition: unreachable_instructions.cpp:378
messaget::error
mstreamt & error() const
Definition: message.h:386
goto_analyzer_parse_optionst::process_goto_program
virtual bool process_goto_program(const optionst &options)
Definition: goto_analyzer_parse_options.cpp:744
initialize_goto_model.h
banner_string
std::string banner_string(const std::string &front_end, const std::string &version)
Definition: parse_options.cpp:87
local_may_alias.h
remove_function_pointers
bool remove_function_pointers(message_handlert &_message_handler, symbol_tablet &symbol_table, const goto_functionst &goto_functions, goto_programt &goto_program, bool add_safety_assertion, bool only_remove_const_fps)
Definition: remove_function_pointers.cpp:520
goto_analyzer_parse_optionst::ui_message_handler
ui_message_handlert ui_message_handler
Definition: goto_analyzer_parse_options.h:167
show_properties.h
is_threaded.h
configt::cppt::set_cpp11
void set_cpp11()
Definition: config.h:142
cmdlinet::get_value
std::string get_value(char option) const
Definition: cmdline.cpp:45
show_symbol_table.h
goto_analyzer_parse_optionst::doit
virtual int doit() override
invoke main modules
Definition: goto_analyzer_parse_options.cpp:373
language.h
unreachable_instructions.h
HELP_SHOW_PROPERTIES
#define HELP_SHOW_PROPERTIES
Definition: show_properties.h:29
configt::this_operating_system
static irep_idt this_operating_system()
Definition: config.cpp:1368
goto_check
void goto_check(const namespacet &ns, const optionst &options, const irep_idt &mode, goto_functionst::goto_functiont &goto_function)
Definition: goto_check.cpp:1784
CPROVER_EXIT_SET_PROPERTIES_FAILED
#define CPROVER_EXIT_SET_PROPERTIES_FAILED
Failure to identify the properties to verify.
Definition: exit_codes.h:56
configt::ansi_ct::arch
irep_idt arch
Definition: config.h:84
static_show_domain
void static_show_domain(const goto_modelt &goto_model, const ai_baset &ai, const optionst &options, std::ostream &out)
Runs the analyzer and then prints out the domain.
Definition: static_show_domain.cpp:20
goto_analyzer_parse_optionst::help
virtual void help() override
display command line help
Definition: goto_analyzer_parse_options.cpp:817
goto_check.h
goto_functionst::compute_loop_numbers
void compute_loop_numbers()
Definition: goto_functions.cpp:52
read_goto_binary.h
GOTO_ANALYSER_OPTIONS
#define GOTO_ANALYSER_OPTIONS
Definition: goto_analyzer_parse_options.h:123
unreachable_instructions
static void unreachable_instructions(const goto_programt &goto_program, dead_mapt &dest)
Definition: unreachable_instructions.cpp:28
configt::ansi_ct::default_c_standard
static c_standardt default_c_standard()
Definition: config.cpp:675
remove_vector.h
remove_complex
static void remove_complex(typet &)
removes complex data type
Definition: remove_complex.cpp:240
remove_returns.h
config
configt config
Definition: config.cpp:24
configt::ansi_ct::c_standardt::C99
goto_analyzer_parse_optionst::register_languages
virtual void register_languages()
Definition: goto_analyzer_parse_options.cpp:76
configt::ansi_ct::set_c11
void set_c11()
Definition: config.h:53
configt::this_architecture
static irep_idt this_architecture()
Definition: config.cpp:1268
configt::ansi_ct::c_standardt::C11
messaget::get_message_handler
message_handlert & get_message_handler()
Definition: message.h:174
interval_domain.h
configt::ansi_ct::set_c89
void set_c89()
Definition: config.h:51
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:32
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:440
ansi_c_language.h
HELP_GOTO_CHECK
#define HELP_GOTO_CHECK
Definition: goto_check.h:43
cprover_c_library_factory
void cprover_c_library_factory(const std::set< irep_idt > &functions, symbol_tablet &symbol_table, message_handlert &message_handler)
Definition: cprover_library.cpp:77
goto_analyzer_parse_optionst::get_ui
ui_message_handlert::uit get_ui()
Definition: goto_analyzer_parse_options.h:181
configt::set
bool set(const cmdlinet &cmdline)
Definition: config.cpp:767
configt::cppt::default_cpp_standard
static cpp_standardt default_cpp_standard()
Definition: config.cpp:689
exit_codes.h
optionst::get_bool_option
bool get_bool_option(const std::string &option) const
Definition: options.cpp:42
constant_propagator_ait
Definition: constant_propagator.h:162
show_on_source.h
concurrency_aware_ait
Definition: ai.h:467
remove_returns
void remove_returns(symbol_table_baset &symbol_table, goto_functionst &goto_functions)
removes returns
Definition: remove_returns.cpp:261
ai_baset
The basic interface of an abstract interpreter.
Definition: ai.h:32
new_ansi_c_language
std::unique_ptr< languaget > new_ansi_c_language()
Definition: ansi_c_language.cpp:142
CPROVER_EXIT_USAGE_ERROR
#define CPROVER_EXIT_USAGE_ERROR
A usage error is returned when the command line is invalid or conflicting.
Definition: exit_codes.h:33
goto_functionst::update
void update()
Definition: goto_functions.h:91
binary
static std::string binary(const constant_exprt &src)
Definition: json_expr.cpp:224
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:516
unicode.h
config.h
forall_goto_functions
#define forall_goto_functions(it, functions)
Definition: goto_functions.h:149
adjust_float_expressions
void adjust_float_expressions(exprt &expr, const exprt &rounding_mode)
This adds the rounding mode to floating-point operations, including those in vectors and complex numb...
Definition: adjust_float_expressions.cpp:78
configt::cppt::cpp_standardt::CPP11
CPROVER_EXIT_INTERNAL_ERROR
#define CPROVER_EXIT_INTERNAL_ERROR
An error has been encountered during processing the requested analysis.
Definition: exit_codes.h:46
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:32
goto_convert_functions.h
configt::cpp
struct configt::cppt cpp
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:426
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:98
goto_analyzer_parse_optionst::goto_model
goto_modelt goto_model
Definition: goto_analyzer_parse_options.h:168
adjust_float_expressions.h
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:37
cmdlinet::get_values
const std::list< std::string > & get_values(const std::string &option) const
Definition: cmdline.cpp:110
remove_function_pointers.h
parse_options_baset::cmdline
cmdlinet cmdline
Definition: parse_options.h:23
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
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:483
cprover_library.h
static_show_domain.h
validation_modet::INVARIANT
dependence_graph.h
HELP_TIMESTAMP
#define HELP_TIMESTAMP
Definition: timestamper.h:14
HELP_FLUSH
#define HELP_FLUSH
Definition: ui_message.h:104
goto_analyzer_parse_optionst::set_properties
bool set_properties()
Definition: goto_analyzer_parse_options.cpp:716
configt::cppt::set_cpp03
void set_cpp03()
Definition: config.h:141
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