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 
41 
42 #include <analyses/is_threaded.h>
43 #include <analyses/goto_check.h>
48 
49 #include <langapi/mode.h>
50 #include <langapi/language.h>
51 
52 #include <util/options.h>
53 #include <util/config.h>
54 #include <util/unicode.h>
55 #include <util/exit_codes.h>
56 
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, "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 "
379  << config.this_architecture() << " "
381 
383 
384  try
385  {
387  }
388 
389  catch(const char *e)
390  {
391  error() << e << eom;
392  return CPROVER_EXIT_EXCEPTION;
393  }
394 
395  catch(const std::string &e)
396  {
397  error() << e << eom;
398  return CPROVER_EXIT_EXCEPTION;
399  }
400 
401  catch(int e)
402  {
403  error() << "Numeric exception: " << e << eom;
404  return CPROVER_EXIT_EXCEPTION;
405  }
406 
407  if(process_goto_program(options))
409 
410  // show it?
411  if(cmdline.isset("show-symbol-table"))
412  {
414  return CPROVER_EXIT_SUCCESS;
415  }
416 
417  // show it?
418  if(
419  cmdline.isset("show-goto-functions") ||
420  cmdline.isset("list-goto-functions"))
421  {
423  goto_model,
425  get_ui(),
426  cmdline.isset("list-goto-functions"));
427  return CPROVER_EXIT_SUCCESS;
428  }
429 
430  try
431  {
432  return perform_analysis(options);
433  }
434 
435  catch(const char *e)
436  {
437  error() << e << eom;
438  return CPROVER_EXIT_EXCEPTION;
439  }
440 
441  catch(const std::string &e)
442  {
443  error() << e << eom;
444  return CPROVER_EXIT_EXCEPTION;
445  }
446 
447  catch(int e)
448  {
449  error() << "Numeric exception: " << e << eom;
450  return CPROVER_EXIT_EXCEPTION;
451  }
452 
453  catch(const std::bad_alloc &)
454  {
455  error() << "Out of memory" << eom;
457  }
458 }
459 
460 
463 {
465  if(options.get_bool_option("taint"))
466  {
467  std::string taint_file=cmdline.get_value("taint");
468 
469  if(cmdline.isset("show-taint"))
470  {
471  taint_analysis(goto_model, taint_file, get_message_handler(), true, "");
472  return CPROVER_EXIT_SUCCESS;
473  }
474  else
475  {
476  std::string json_file=cmdline.get_value("json");
477  bool result=
479  goto_model, taint_file, get_message_handler(), false, json_file);
481  }
482  }
483 
484  // If no domain is given, this lightweight version of the analysis is used.
485  if(options.get_bool_option("unreachable-instructions") &&
486  options.get_bool_option("specific-analysis"))
487  {
488  const std::string json_file=cmdline.get_value("json");
489 
490  if(json_file.empty())
491  unreachable_instructions(goto_model, false, std::cout);
492  else if(json_file=="-")
493  unreachable_instructions(goto_model, true, std::cout);
494  else
495  {
496  std::ofstream ofs(json_file);
497  if(!ofs)
498  {
499  error() << "Failed to open json output `"
500  << json_file << "'" << eom;
502  }
503 
505  }
506 
507  return CPROVER_EXIT_SUCCESS;
508  }
509 
510  if(options.get_bool_option("unreachable-functions") &&
511  options.get_bool_option("specific-analysis"))
512  {
513  const std::string json_file=cmdline.get_value("json");
514 
515  if(json_file.empty())
516  unreachable_functions(goto_model, false, std::cout);
517  else if(json_file=="-")
518  unreachable_functions(goto_model, true, std::cout);
519  else
520  {
521  std::ofstream ofs(json_file);
522  if(!ofs)
523  {
524  error() << "Failed to open json output `"
525  << json_file << "'" << eom;
527  }
528 
529  unreachable_functions(goto_model, true, ofs);
530  }
531 
532  return CPROVER_EXIT_SUCCESS;
533  }
534 
535  if(options.get_bool_option("reachable-functions") &&
536  options.get_bool_option("specific-analysis"))
537  {
538  const std::string json_file=cmdline.get_value("json");
539 
540  if(json_file.empty())
541  reachable_functions(goto_model, false, std::cout);
542  else if(json_file=="-")
543  reachable_functions(goto_model, true, std::cout);
544  else
545  {
546  std::ofstream ofs(json_file);
547  if(!ofs)
548  {
549  error() << "Failed to open json output `"
550  << json_file << "'" << eom;
552  }
553 
554  reachable_functions(goto_model, true, ofs);
555  }
556 
557  return CPROVER_EXIT_SUCCESS;
558  }
559 
560  if(options.get_bool_option("show-local-may-alias"))
561  {
563 
565  {
566  std::cout << ">>>>\n";
567  std::cout << ">>>> " << it->first << '\n';
568  std::cout << ">>>>\n";
569  local_may_aliast local_may_alias(it->second);
570  local_may_alias.output(std::cout, it->second, ns);
571  std::cout << '\n';
572  }
573 
574  return CPROVER_EXIT_SUCCESS;
575  }
576 
578 
579  if(cmdline.isset("show-properties"))
580  {
582  return CPROVER_EXIT_SUCCESS;
583  }
584 
585  if(set_properties())
587 
588  if(options.get_bool_option("general-analysis"))
589  {
590 
591  // Output file factory
592  const std::string outfile=options.get_option("outfile");
593  std::ofstream output_stream;
594  if(!(outfile=="-"))
595  output_stream.open(outfile);
596 
597  std::ostream &out((outfile=="-") ? std::cout : output_stream);
598 
599  if(!out)
600  {
601  error() << "Failed to open output file `"
602  << outfile << "'" << eom;
604  }
605 
606  // Build analyzer
607  status() << "Selecting abstract domain" << eom;
608  namespacet ns(goto_model.symbol_table); // Must live as long as the domain.
609  std::unique_ptr<ai_baset> analyzer(build_analyzer(options, ns));
610 
611  if(analyzer == nullptr)
612  {
613  status() << "Task / Interpreter / Domain combination not supported"
614  << messaget::eom;
616  }
617 
618 
619  // Run
620  status() << "Computing abstract states" << eom;
621  (*analyzer)(goto_model);
622 
623  // Perform the task
624  status() << "Performing task" << eom;
625  bool result = true;
626  if(options.get_bool_option("show"))
627  {
629  *analyzer,
630  options,
632  out);
633  }
634  else if(options.get_bool_option("verify"))
635  {
637  *analyzer,
638  options,
640  out);
641  }
642  else if(options.get_bool_option("simplify"))
643  {
645  *analyzer,
646  options,
648  out);
649  }
650  else if(options.get_bool_option("unreachable-instructions"))
651  {
653  *analyzer,
654  options,
656  out);
657  }
658  else if(options.get_bool_option("unreachable-functions"))
659  {
661  *analyzer,
662  options,
664  out);
665  }
666  else if(options.get_bool_option("reachable-functions"))
667  {
669  *analyzer,
670  options,
672  out);
673  }
674  else
675  {
676  error() << "Unhandled task" << eom;
678  }
679 
680  return result ?
682  }
683 
684 
685  // Final defensive error case
686  error() << "no analysis option given -- consider reading --help"
687  << eom;
689 }
690 
692 {
693  try
694  {
695  if(cmdline.isset("property"))
697  }
698 
699  catch(const char *e)
700  {
701  error() << e << eom;
702  return true;
703  }
704 
705  catch(const std::string &e)
706  {
707  error() << e << eom;
708  return true;
709  }
710 
711  catch(int)
712  {
713  return true;
714  }
715 
716  return false;
717 }
718 
720  const optionst &options)
721 {
722  try
723  {
724  #if 0
725  // Remove inline assembler; this needs to happen before
726  // adding the library.
728 
729  // add the library
730  status() << "Adding CPROVER library (" << config.ansi_c.arch << ")" << eom;
734  #endif
735 
736  // remove function pointers
737  status() << "Removing function pointers and virtual functions" << eom;
739  get_message_handler(), goto_model, cmdline.isset("pointer-check"));
740 
741  // do partial inlining
742  status() << "Partial Inlining" << eom;
744 
745  // remove returns, gcc vectors, complex
749 
750  #if 0
751  // add generic checks
752  status() << "Generic Property Instrumentation" << eom;
753  goto_check(options, goto_model);
754  #endif
755 
756  // recalculate numbers, etc.
758 
759  // add loop ids
761  }
762 
763  catch(const char *e)
764  {
765  error() << e << eom;
766  return true;
767  }
768 
769  catch(const std::string &e)
770  {
771  error() << e << eom;
772  return true;
773  }
774 
775  catch(int)
776  {
777  return true;
778  }
779 
780  catch(const std::bad_alloc &)
781  {
782  error() << "Out of memory" << eom;
783  return true;
784  }
785 
786  return false;
787 }
788 
791 {
792  // clang-format off
793  std::cout << '\n' << banner_string("GOTO-ANALYZER", CBMC_VERSION) << '\n'
794  <<
795  "* * Copyright (C) 2017-2018 * *\n"
796  "* * Daniel Kroening, DiffBlue * *\n"
797  "* * kroening@kroening.com * *\n"
798  "\n"
799  "Usage: Purpose:\n"
800  "\n"
801  " goto-analyzer [-h] [--help] show help\n"
802  " goto-analyzer file.c ... source file names\n"
803  "\n"
804  "Task options:\n"
805  " --show display the abstract domains\n"
806  // NOLINTNEXTLINE(whitespace/line_length)
807  " --verify use the abstract domains to check assertions\n"
808  // NOLINTNEXTLINE(whitespace/line_length)
809  " --simplify file_name use the abstract domains to simplify the program\n"
810  " --unreachable-instructions list dead code\n"
811  // NOLINTNEXTLINE(whitespace/line_length)
812  " --unreachable-functions list functions unreachable from the entry point\n"
813  // NOLINTNEXTLINE(whitespace/line_length)
814  " --reachable-functions list functions reachable from the entry point\n"
815  "\n"
816  "Abstract interpreter options:\n"
817  // NOLINTNEXTLINE(whitespace/line_length)
818  " --location-sensitive use location-sensitive abstract interpreter\n"
819  " --concurrent use concurrency-aware abstract interpreter\n"
820  "\n"
821  "Domain options:\n"
822  " --constants constant domain\n"
823  " --intervals interval domain\n"
824  " --non-null non-null domain\n"
825  " --dependence-graph data and control dependencies between instructions\n" // NOLINT(*)
826  "\n"
827  "Output options:\n"
828  " --text file_name output results in plain text to given file\n"
829  // NOLINTNEXTLINE(whitespace/line_length)
830  " --json file_name output results in JSON format to given file\n"
831  " --xml file_name output results in XML format to given file\n"
832  " --dot file_name output results in DOT format to given file\n"
833  "\n"
834  "Specific analyses:\n"
835  // NOLINTNEXTLINE(whitespace/line_length)
836  " --taint file_name perform taint analysis using rules in given file\n"
837  "\n"
838  "C/C++ frontend options:\n"
839  " -I path set include path (C/C++)\n"
840  " -D macro define preprocessor macro (C/C++)\n"
841  " --arch X set architecture (default: "
842  << configt::this_architecture() << ")\n"
843  " --os set operating system (default: "
844  << configt::this_operating_system() << ")\n"
845  " --c89/99/11 set C language standard (default: "
852  "c11":"") << ")\n"
853  " --cpp98/03/11 set C++ language standard (default: "
856  "cpp98":
859  "cpp03":
862  "cpp11":"") << ")\n"
863  #ifdef _WIN32
864  " --gcc use GCC as preprocessor\n"
865  #endif
866  " --no-library disable built-in abstract C library\n"
867  "\n"
869  "\n"
870  "Program representations:\n"
871  " --show-parse-tree show parse tree\n"
872  " --show-symbol-table show loaded symbol table\n"
875  "\n"
876  "Program instrumentation options:\n"
878  "\n"
879  "Other options:\n"
880  " --version show version and exit\n"
881  HELP_FLUSH
883  "\n";
884  // clang-format on
885 }
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)
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:377
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:131
bool static_show_domain(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.
bool static_reachable_functions(const goto_modelt &goto_model, const ai_baset &ai, const optionst &options, message_handlert &message_handler, std::ostream &out)
bool static_unreachable_functions(const goto_modelt &goto_model, const ai_baset &ai, const optionst &options, message_handlert &message_handler, std::ostream &out)
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)
#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:737
void set_c89()
Definition: config.h:51
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
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.
void adjust_float_expressions(exprt &expr, const namespacet &ns)
This adds the rounding mode to floating-point operations, including those in vectors and complex numb...
#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
static c_standardt default_c_standard()
Definition: config.cpp:647
virtual void get_command_line_options(optionst &options)
Interval Domain.
List all unreachable instructions.
static irep_idt this_operating_system()
Definition: config.cpp:1309
#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:133
bool static_unreachable_instructions(const goto_modelt &goto_model, const ai_baset &ai, const optionst &options, message_handlert &message_handler, std::ostream &out)
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
Definition: ai.h:128
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
static cpp_standardt default_cpp_standard()
Definition: config.cpp:661
void reachable_functions(const goto_modelt &goto_model, const bool json, std::ostream &os)
void set_cpp03()
Definition: config.h:132
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:1212
#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.
void remove_asm(goto_functionst::goto_functiont &goto_function, symbol_tablet &symbol_table)
removes assembler
Definition: remove_asm.cpp:306
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)