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/exit_codes.h>
55 #include <util/options.h>
56 #include <util/unicode.h>
57 #include <util/version.h>
58 
59 #include "taint_analysis.h"
61 #include "static_show_domain.h"
62 #include "static_simplifier.h"
63 #include "static_verifier.h"
64 
66  int argc,
67  const char **argv)
69  messaget(ui_message_handler),
70  ui_message_handler(cmdline, std::string("GOTO-ANALYZER ") + CBMC_VERSION)
71 {
72 }
73 
75 {
79 }
80 
82 {
83  if(config.set(cmdline))
84  {
85  usage_error();
87  }
88 
89  #if 0
90  if(cmdline.isset("c89"))
92 
93  if(cmdline.isset("c99"))
95 
96  if(cmdline.isset("c11"))
98 
99  if(cmdline.isset("cpp98"))
100  config.cpp.set_cpp98();
101 
102  if(cmdline.isset("cpp03"))
103  config.cpp.set_cpp03();
104 
105  if(cmdline.isset("cpp11"))
106  config.cpp.set_cpp11();
107  #endif
108 
109  #if 0
110  // check assertions
111  if(cmdline.isset("no-assertions"))
112  options.set_option("assertions", false);
113  else
114  options.set_option("assertions", true);
115 
116  // use assumptions
117  if(cmdline.isset("no-assumptions"))
118  options.set_option("assumptions", false);
119  else
120  options.set_option("assumptions", true);
121 
122  // magic error label
123  if(cmdline.isset("error-label"))
124  options.set_option("error-label", cmdline.get_values("error-label"));
125  #endif
126 
127  // Select a specific analysis
128  if(cmdline.isset("taint"))
129  {
130  options.set_option("taint", true);
131  options.set_option("specific-analysis", true);
132  }
133  // For backwards compatibility,
134  // these are first recognised as specific analyses
135  bool reachability_task = false;
136  if(cmdline.isset("unreachable-instructions"))
137  {
138  options.set_option("unreachable-instructions", true);
139  options.set_option("specific-analysis", true);
140  reachability_task = true;
141  }
142  if(cmdline.isset("unreachable-functions"))
143  {
144  options.set_option("unreachable-functions", true);
145  options.set_option("specific-analysis", true);
146  reachability_task = true;
147  }
148  if(cmdline.isset("reachable-functions"))
149  {
150  options.set_option("reachable-functions", true);
151  options.set_option("specific-analysis", true);
152  reachability_task = true;
153  }
154  if(cmdline.isset("show-local-may-alias"))
155  {
156  options.set_option("show-local-may-alias", true);
157  options.set_option("specific-analysis", true);
158  }
159 
160  // Output format choice
161  if(cmdline.isset("text"))
162  {
163  options.set_option("text", true);
164  options.set_option("outfile", cmdline.get_value("text"));
165  }
166  else if(cmdline.isset("json"))
167  {
168  options.set_option("json", true);
169  options.set_option("outfile", cmdline.get_value("json"));
170  }
171  else if(cmdline.isset("xml"))
172  {
173  options.set_option("xml", true);
174  options.set_option("outfile", cmdline.get_value("xml"));
175  }
176  else if(cmdline.isset("dot"))
177  {
178  options.set_option("dot", true);
179  options.set_option("outfile", cmdline.get_value("dot"));
180  }
181  else
182  {
183  options.set_option("text", true);
184  options.set_option("outfile", "-");
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("verify"))
199  {
200  options.set_option("verify", true);
201  options.set_option("general-analysis", true);
202  }
203  else if(cmdline.isset("simplify"))
204  {
205  options.set_option("simplify", true);
206  options.set_option("outfile", cmdline.get_value("simplify"));
207  options.set_option("general-analysis", true);
208 
209  // For development allow slicing to be disabled in the simplify task
210  options.set_option(
211  "simplify-slicing",
212  !(cmdline.isset("no-simplify-slicing")));
213  }
214  else if(cmdline.isset("show-intervals"))
215  {
216  // For backwards compatibility
217  options.set_option("show", true);
218  options.set_option("general-analysis", true);
219  options.set_option("intervals", true);
220  options.set_option("domain set", true);
221  }
222  else if(cmdline.isset("(show-non-null)"))
223  {
224  // For backwards compatibility
225  options.set_option("show", true);
226  options.set_option("general-analysis", true);
227  options.set_option("non-null", true);
228  options.set_option("domain set", true);
229  }
230  else if(cmdline.isset("intervals") || cmdline.isset("non-null"))
231  {
232  // For backwards compatibility either of these on their own means show
233  options.set_option("show", true);
234  options.set_option("general-analysis", true);
235  }
236 
237  if(options.get_bool_option("general-analysis") || reachability_task)
238  {
239  // Abstract interpreter choice
240  if(cmdline.isset("location-sensitive"))
241  options.set_option("location-sensitive", true);
242  else if(cmdline.isset("concurrent"))
243  options.set_option("concurrent", true);
244  else
245  {
246  // Silently default to location-sensitive as it's the "default"
247  // view of abstract interpretation.
248  options.set_option("location-sensitive", true);
249  }
250 
251  // Domain choice
252  if(cmdline.isset("constants"))
253  {
254  options.set_option("constants", true);
255  options.set_option("domain set", true);
256  }
257  else if(cmdline.isset("dependence-graph"))
258  {
259  options.set_option("dependence-graph", true);
260  options.set_option("domain set", true);
261  }
262  else if(cmdline.isset("intervals"))
263  {
264  options.set_option("intervals", true);
265  options.set_option("domain set", true);
266  }
267  else if(cmdline.isset("non-null"))
268  {
269  options.set_option("non-null", true);
270  options.set_option("domain set", true);
271  }
272 
273  // Reachability questions, when given with a domain swap from specific
274  // to general tasks so that they can use the domain & parameterisations.
275  if(reachability_task)
276  {
277  if(options.get_bool_option("domain set"))
278  {
279  options.set_option("specific-analysis", false);
280  options.set_option("general-analysis", true);
281  }
282  }
283  else
284  {
285  if(!options.get_bool_option("domain set"))
286  {
287  // Default to constants as it is light-weight but useful
288  status() << "Domain not specified, defaulting to --constants" << eom;
289  options.set_option("constants", true);
290  }
291  }
292  }
293 }
294 
299  const optionst &options,
300  const namespacet &ns)
301 {
302  ai_baset *domain = nullptr;
303 
304  if(options.get_bool_option("location-sensitive"))
305  {
306  if(options.get_bool_option("constants"))
307  {
308  // constant_propagator_ait derives from ait<constant_propagator_domaint>
310  }
311  else if(options.get_bool_option("dependence-graph"))
312  {
313  domain=new dependence_grapht(ns);
314  }
315  else if(options.get_bool_option("intervals"))
316  {
317  domain=new ait<interval_domaint>();
318  }
319 #if 0
320  // Not actually implemented, despite the option...
321  else if(options.get_bool_option("non-null"))
322  {
323  domain=new ait<non_null_domaint>();
324  }
325 #endif
326  }
327  else if(options.get_bool_option("concurrent"))
328  {
329 #if 0
330  // Disabled until merge_shared is implemented for these
331  if(options.get_bool_option("constants"))
332  {
334  }
335  else if(options.get_bool_option("dependence-graph"))
336  {
337  domain=new dependence_grapht(ns);
338  }
339  else if(options.get_bool_option("intervals"))
340  {
342  }
343 #if 0
344  // Not actually implemented, despite the option...
345  else if(options.get_bool_option("non-null"))
346  {
348  }
349 #endif
350 #endif
351  }
352 
353  return domain;
354 }
355 
358 {
359  if(cmdline.isset("version"))
360  {
361  std::cout << CBMC_VERSION << '\n';
362  return CPROVER_EXIT_SUCCESS;
363  }
364 
365  //
366  // command line options
367  //
368 
369  optionst options;
370  get_command_line_options(options);
373 
374  //
375  // Print a banner
376  //
377  status() << "GOTO-ANALYSER version " << CBMC_VERSION << " "
378  << sizeof(void *) * 8 << "-bit " << config.this_architecture() << " "
380 
382 
383  try
384  {
386  }
387 
388  catch(const char *e)
389  {
390  error() << e << eom;
391  return CPROVER_EXIT_EXCEPTION;
392  }
393 
394  catch(const std::string &e)
395  {
396  error() << e << eom;
397  return CPROVER_EXIT_EXCEPTION;
398  }
399 
400  catch(int e)
401  {
402  error() << "Numeric exception: " << e << eom;
403  return CPROVER_EXIT_EXCEPTION;
404  }
405 
406  if(process_goto_program(options))
408 
409  // show it?
410  if(cmdline.isset("show-symbol-table"))
411  {
413  return CPROVER_EXIT_SUCCESS;
414  }
415 
416  // show it?
417  if(
418  cmdline.isset("show-goto-functions") ||
419  cmdline.isset("list-goto-functions"))
420  {
422  goto_model,
424  get_ui(),
425  cmdline.isset("list-goto-functions"));
426  return CPROVER_EXIT_SUCCESS;
427  }
428 
429  try
430  {
431  return perform_analysis(options);
432  }
433 
434  catch(const char *e)
435  {
436  error() << e << eom;
437  return CPROVER_EXIT_EXCEPTION;
438  }
439 
440  catch(const std::string &e)
441  {
442  error() << e << eom;
443  return CPROVER_EXIT_EXCEPTION;
444  }
445 
446  catch(int e)
447  {
448  error() << "Numeric exception: " << e << eom;
449  return CPROVER_EXIT_EXCEPTION;
450  }
451 
452  catch(const std::bad_alloc &)
453  {
454  error() << "Out of memory" << eom;
456  }
457 }
458 
459 
462 {
464  if(options.get_bool_option("taint"))
465  {
466  std::string taint_file=cmdline.get_value("taint");
467 
468  if(cmdline.isset("show-taint"))
469  {
470  taint_analysis(goto_model, taint_file, get_message_handler(), true, "");
471  return CPROVER_EXIT_SUCCESS;
472  }
473  else
474  {
475  std::string json_file=cmdline.get_value("json");
476  bool result=
478  goto_model, taint_file, get_message_handler(), false, json_file);
480  }
481  }
482 
483  // If no domain is given, this lightweight version of the analysis is used.
484  if(options.get_bool_option("unreachable-instructions") &&
485  options.get_bool_option("specific-analysis"))
486  {
487  const std::string json_file=cmdline.get_value("json");
488 
489  if(json_file.empty())
490  unreachable_instructions(goto_model, false, std::cout);
491  else if(json_file=="-")
492  unreachable_instructions(goto_model, true, std::cout);
493  else
494  {
495  std::ofstream ofs(json_file);
496  if(!ofs)
497  {
498  error() << "Failed to open json output `"
499  << json_file << "'" << eom;
501  }
502 
504  }
505 
506  return CPROVER_EXIT_SUCCESS;
507  }
508 
509  if(options.get_bool_option("unreachable-functions") &&
510  options.get_bool_option("specific-analysis"))
511  {
512  const std::string json_file=cmdline.get_value("json");
513 
514  if(json_file.empty())
515  unreachable_functions(goto_model, false, std::cout);
516  else if(json_file=="-")
517  unreachable_functions(goto_model, true, std::cout);
518  else
519  {
520  std::ofstream ofs(json_file);
521  if(!ofs)
522  {
523  error() << "Failed to open json output `"
524  << json_file << "'" << eom;
526  }
527 
528  unreachable_functions(goto_model, true, ofs);
529  }
530 
531  return CPROVER_EXIT_SUCCESS;
532  }
533 
534  if(options.get_bool_option("reachable-functions") &&
535  options.get_bool_option("specific-analysis"))
536  {
537  const std::string json_file=cmdline.get_value("json");
538 
539  if(json_file.empty())
540  reachable_functions(goto_model, false, std::cout);
541  else if(json_file=="-")
542  reachable_functions(goto_model, true, std::cout);
543  else
544  {
545  std::ofstream ofs(json_file);
546  if(!ofs)
547  {
548  error() << "Failed to open json output `"
549  << json_file << "'" << eom;
551  }
552 
553  reachable_functions(goto_model, true, ofs);
554  }
555 
556  return CPROVER_EXIT_SUCCESS;
557  }
558 
559  if(options.get_bool_option("show-local-may-alias"))
560  {
562 
564  {
565  std::cout << ">>>>\n";
566  std::cout << ">>>> " << it->first << '\n';
567  std::cout << ">>>>\n";
568  local_may_aliast local_may_alias(it->second);
569  local_may_alias.output(std::cout, it->second, ns);
570  std::cout << '\n';
571  }
572 
573  return CPROVER_EXIT_SUCCESS;
574  }
575 
577 
578  if(cmdline.isset("show-properties"))
579  {
581  return CPROVER_EXIT_SUCCESS;
582  }
583 
584  if(set_properties())
586 
587  if(options.get_bool_option("general-analysis"))
588  {
589 
590  // Output file factory
591  const std::string outfile=options.get_option("outfile");
592  std::ofstream output_stream;
593  if(!(outfile=="-"))
594  output_stream.open(outfile);
595 
596  std::ostream &out((outfile=="-") ? std::cout : output_stream);
597 
598  if(!out)
599  {
600  error() << "Failed to open output file `"
601  << outfile << "'" << eom;
603  }
604 
605  // Build analyzer
606  status() << "Selecting abstract domain" << eom;
607  namespacet ns(goto_model.symbol_table); // Must live as long as the domain.
608  std::unique_ptr<ai_baset> analyzer(build_analyzer(options, ns));
609 
610  if(analyzer == nullptr)
611  {
612  status() << "Task / Interpreter / Domain combination not supported"
613  << messaget::eom;
615  }
616 
617 
618  // Run
619  status() << "Computing abstract states" << eom;
620  (*analyzer)(goto_model);
621 
622  // Perform the task
623  status() << "Performing task" << eom;
624  bool result = true;
625  if(options.get_bool_option("show"))
626  {
628  *analyzer,
629  options,
630  out);
631  }
632  else if(options.get_bool_option("verify"))
633  {
635  *analyzer,
636  options,
638  out);
639  }
640  else if(options.get_bool_option("simplify"))
641  {
643  *analyzer,
644  options,
646  out);
647  }
648  else if(options.get_bool_option("unreachable-instructions"))
649  {
651  *analyzer,
652  options,
653  out);
654  }
655  else if(options.get_bool_option("unreachable-functions"))
656  {
658  *analyzer,
659  options,
660  out);
661  }
662  else if(options.get_bool_option("reachable-functions"))
663  {
665  *analyzer,
666  options,
667  out);
668  }
669  else
670  {
671  error() << "Unhandled task" << eom;
673  }
674 
675  return result ?
677  }
678 
679 
680  // Final defensive error case
681  error() << "no analysis option given -- consider reading --help"
682  << eom;
684 }
685 
687 {
688  try
689  {
690  if(cmdline.isset("property"))
692  }
693 
694  catch(const char *e)
695  {
696  error() << e << eom;
697  return true;
698  }
699 
700  catch(const std::string &e)
701  {
702  error() << e << eom;
703  return true;
704  }
705 
706  catch(int)
707  {
708  return true;
709  }
710 
711  return false;
712 }
713 
715  const optionst &options)
716 {
717  try
718  {
719  #if 0
720  // Remove inline assembler; this needs to happen before
721  // adding the library.
723 
724  // add the library
725  status() << "Adding CPROVER library (" << config.ansi_c.arch << ")" << eom;
729  #endif
730 
731  // remove function pointers
732  status() << "Removing function pointers and virtual functions" << eom;
734  get_message_handler(), goto_model, cmdline.isset("pointer-check"));
735 
736  // do partial inlining
737  status() << "Partial Inlining" << eom;
739 
740  // remove returns, gcc vectors, complex
744 
745  #if 0
746  // add generic checks
747  status() << "Generic Property Instrumentation" << eom;
748  goto_check(options, goto_model);
749  #endif
750 
751  // recalculate numbers, etc.
753 
754  // add loop ids
756  }
757 
758  catch(const char *e)
759  {
760  error() << e << eom;
761  return true;
762  }
763 
764  catch(const std::string &e)
765  {
766  error() << e << eom;
767  return true;
768  }
769 
770  catch(int)
771  {
772  return true;
773  }
774 
775  catch(const std::bad_alloc &)
776  {
777  error() << "Out of memory" << eom;
778  return true;
779  }
780 
781  return false;
782 }
783 
786 {
787  // clang-format off
788  std::cout << '\n' << banner_string("GOTO-ANALYZER", CBMC_VERSION) << '\n'
789  <<
790  "* * Copyright (C) 2017-2018 * *\n"
791  "* * Daniel Kroening, DiffBlue * *\n"
792  "* * kroening@kroening.com * *\n"
793  "\n"
794  "Usage: Purpose:\n"
795  "\n"
796  " goto-analyzer [-h] [--help] show help\n"
797  " goto-analyzer file.c ... source file names\n"
798  "\n"
799  "Task options:\n"
800  " --show display the abstract domains\n"
801  // NOLINTNEXTLINE(whitespace/line_length)
802  " --verify use the abstract domains to check assertions\n"
803  // NOLINTNEXTLINE(whitespace/line_length)
804  " --simplify file_name use the abstract domains to simplify the program\n"
805  " --unreachable-instructions list dead code\n"
806  // NOLINTNEXTLINE(whitespace/line_length)
807  " --unreachable-functions list functions unreachable from the entry point\n"
808  // NOLINTNEXTLINE(whitespace/line_length)
809  " --reachable-functions list functions reachable from the entry point\n"
810  "\n"
811  "Abstract interpreter options:\n"
812  // NOLINTNEXTLINE(whitespace/line_length)
813  " --location-sensitive use location-sensitive abstract interpreter\n"
814  " --concurrent use concurrency-aware abstract interpreter\n"
815  "\n"
816  "Domain options:\n"
817  " --constants constant domain\n"
818  " --intervals interval domain\n"
819  " --non-null non-null domain\n"
820  " --dependence-graph data and control dependencies between instructions\n" // NOLINT(*)
821  "\n"
822  "Output options:\n"
823  " --text file_name output results in plain text to given file\n"
824  // NOLINTNEXTLINE(whitespace/line_length)
825  " --json file_name output results in JSON format to given file\n"
826  " --xml file_name output results in XML format to given file\n"
827  " --dot file_name output results in DOT format to given file\n"
828  "\n"
829  "Specific analyses:\n"
830  // NOLINTNEXTLINE(whitespace/line_length)
831  " --taint file_name perform taint analysis using rules in given file\n"
832  "\n"
833  "C/C++ frontend options:\n"
834  " -I path set include path (C/C++)\n"
835  " -D macro define preprocessor macro (C/C++)\n"
836  " --arch X set architecture (default: "
837  << configt::this_architecture() << ")\n"
838  " --os set operating system (default: "
839  << configt::this_operating_system() << ")\n"
840  " --c89/99/11 set C language standard (default: "
847  "c11":"") << ")\n"
848  " --cpp98/03/11 set C++ language standard (default: "
851  "cpp98":
854  "cpp03":
857  "cpp11":"") << ")\n"
858  #ifdef _WIN32
859  " --gcc use GCC as preprocessor\n"
860  #endif
861  " --no-library disable built-in abstract C library\n"
862  "\n"
864  "\n"
865  "Program representations:\n"
866  " --show-parse-tree show parse tree\n"
867  " --show-symbol-table show loaded symbol table\n"
870  "\n"
871  "Program instrumentation options:\n"
873  "\n"
874  "Other options:\n"
875  " --version show version and exit\n"
876  HELP_FLUSH
878  "\n";
879  // clang-format on
880 }
const std::list< std::string > & get_values(const std::string &option) const
Definition: cmdline.cpp:110
Symbolic Execution.
struct configt::ansi_ct ansi_c
Over-approximate Concurrency for Threaded Goto Programs.
std::unique_ptr< languaget > new_cpp_language()
std::unique_ptr< languaget > new_jsil_language()
Remove Indirect Function Calls.
Remove Virtual Function (Method) Calls.
Field-Sensitive Program Dependence Analysis, Litvak et al., FSE 2010.
goto_analyzer_parse_optionst(int argc, const char **argv)
bool static_unreachable_functions(const goto_modelt &goto_model, const ai_baset &ai, const optionst &options, std::ostream &out)
void compute_loop_numbers()
Show the symbol table.
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:78
Definition: ai.h:294
Read Goto Programs.
Remove the &#39;complex&#39; data type by compilation into structs.
Goto-Analyser Command Line Option Processing.
std::string get_value(char option) const
Definition: cmdline.cpp:45
void set_cpp98()
Definition: config.h:139
STL namespace.
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
#define CPROVER_EXIT_INTERNAL_ERROR
An error has been encountered during processing the requested analysis.
Definition: exit_codes.h:41
void show_goto_functions(const namespacet &ns, message_handlert &message_handler, ui_message_handlert::uit ui, const goto_functionst &goto_functions, bool list_only)
configt config
Definition: config.cpp:23
Remove &#39;asm&#39; statements by compiling into suitable standard code.
#define HELP_FUNCTIONS
void cprover_c_library_factory(const std::set< irep_idt > &functions, symbol_tablet &symbol_table, message_handlert &message_handler)
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...
#define CPROVER_EXIT_SUCCESS
Success indicates the required analysis has been performed without error.
Definition: exit_codes.h:16
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...
Set the properties to check.
#define HELP_GOTO_CHECK
Definition: goto_check.h:42
bool set(const cmdlinet &cmdline)
Definition: config.cpp:738
void set_c89()
Definition: config.h:51
bool 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 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)
#define HELP_TIMESTAMP
Definition: timestamper.h:14
void show_symbol_table(const symbol_tablet &symbol_table, ui_message_handlert::uit ui)
virtual bool isset(char option) const
Definition: cmdline.cpp:27
Initialize a Goto Program.
#define HELP_SHOW_PROPERTIES
const std::string get_option(const std::string &option) const
Definition: options.cpp:65
bool static_reachable_functions(const goto_modelt &goto_model, const ai_baset &ai, const optionst &options, std::ostream &out)
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...
#define HELP_FLUSH
Definition: ui_message.h:108
bool get_bool_option(const std::string &option) const
Definition: options.cpp:42
mstreamt & error() const
Definition: message.h:302
C++ Language Module.
irep_idt arch
Definition: config.h:84
TO_BE_DOCUMENTED.
Definition: namespace.h:74
Function Inlining.
Abstract interface to support a programming language.
virtual bool process_goto_program(const optionst &options)
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.
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)
Program Transformation.
virtual void help() override
display command line help
void cprover_cpp_library_factory(const std::set< irep_idt > &functions, symbol_tablet &symbol_table, message_handlert &message_handler)
Remove function returns.
#define GOTO_ANALYSER_OPTIONS
std::string banner_string(const std::string &front_end, const std::string &version)
void remove_returns(symbol_table_baset &symbol_table, goto_functionst &goto_functions)
removes returns
Jsil Language.
void goto_check(const namespacet &ns, const optionst &options, const irep_idt &mode, goto_functionst::goto_functiont &goto_function)
void set_c11()
Definition: config.h:53
#define CPROVER_EXIT_EXCEPTION
An (unanticipated) exception was thrown during computation.
Definition: exit_codes.h:36
void remove_asm(goto_functionst &goto_functions, symbol_tablet &symbol_table)
removes assembler
Definition: remove_asm.cpp:482
static c_standardt default_c_standard()
Definition: config.cpp:648
virtual void get_command_line_options(optionst &options)
Interval Domain.
List all unreachable instructions.
static irep_idt this_operating_system()
Definition: config.cpp:1310
#define CPROVER_EXIT_INTERNAL_OUT_OF_MEMORY
Memory allocation has failed and this has been detected within the program.
Definition: exit_codes.h:48
struct configt::cppt cpp
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.
void set_c99()
Definition: config.h:52
message_handlert & get_message_handler()
Definition: message.h:153
void set_cpp11()
Definition: config.h:141
Goto Programs with Functions.
Document and give macros for the exit codes of CPROVER binaries.
mstreamt & result() const
Definition: message.h:312
mstreamt & status() const
Definition: message.h:317
#define HELP_SHOW_GOTO_FUNCTIONS
const char * CBMC_VERSION
Definition: version.cpp:1
The basic interface of an abstract interpreter.
Definition: ai.h:32
Constant propagation.
#define CPROVER_EXIT_VERIFICATION_UNSAFE
Verification successful indiciates the analysis has been performed without error AND the software is ...
Definition: exit_codes.h:25
virtual int perform_analysis(const optionst &options)
Depending on the command line mode, run one of the analysis tasks.
static void unreachable_instructions(const goto_programt &goto_program, dead_mapt &dest)
goto_modelt initialize_goto_model(const cmdlinet &cmdline, message_handlert &message_handler)
void unreachable_functions(const goto_modelt &goto_model, const bool json, std::ostream &os)
std::unique_ptr< languaget > new_ansi_c_language()
Taint Analysis.
Remove the &#39;vector&#39; data type by compilation into arrays.
Options.
virtual void usage_error()
Show the properties.
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
#define CPROVER_EXIT_VERIFICATION_SAFE
Verification successful indiciates the analysis has been performed without error AND the software is ...
Definition: exit_codes.h:21
void set_option(const std::string &option, const bool value)
Definition: options.cpp:24
static void remove_complex(typet &)
removes complex data type
void output(std::ostream &out, const goto_functiont &goto_function, const namespacet &ns) const
#define forall_goto_functions(it, functions)
#define CPROVER_EXIT_USAGE_ERROR
A usage error is returned when the command line is invalid or conflicting.
Definition: exit_codes.h:28
bool static_unreachable_instructions(const goto_modelt &goto_model, const ai_baset &ai, const optionst &options, std::ostream &out)
static cpp_standardt default_cpp_standard()
Definition: config.cpp:662
void reachable_functions(const goto_modelt &goto_model, const bool json, std::ostream &os)
void set_cpp03()
Definition: config.h:140
void label_properties(goto_modelt &goto_model)
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
static void remove_vector(typet &)
removes vector data type
static irep_idt this_architecture()
Definition: config.cpp:1213
#define CPROVER_EXIT_SET_PROPERTIES_FAILED
Failure to identify the properties to verify.
Definition: exit_codes.h:51
Field-insensitive, location-sensitive may-alias analysis.
virtual int doit() override
invoke main modules
void show_properties(const namespacet &ns, const irep_idt &identifier, message_handlert &message_handler, ui_message_handlert::uit ui, const goto_programt &goto_program)