cprover
janalyzer_parse_options.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: JANALYZER Command Line Option Processing
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
13 
14 #include <cstdlib> // exit()
15 #include <fstream>
16 #include <iostream>
17 #include <memory>
18 
19 #include <ansi-c/ansi_c_language.h>
21 
34 
37 #include <analyses/goto_check.h>
39 #include <analyses/is_threaded.h>
41 
44 
45 #include <langapi/language.h>
46 #include <langapi/mode.h>
47 
48 #include <util/config.h>
49 #include <util/exit_codes.h>
50 #include <util/options.h>
51 #include <util/unicode.h>
52 
58 
61  messaget(ui_message_handler),
62  ui_message_handler(cmdline, "JANALYZER " CBMC_VERSION)
63 {
64 }
65 
67 {
69 }
70 
72 {
73  if(config.set(cmdline))
74  {
75  usage_error();
77  }
78 
79  // check assertions
80  if(cmdline.isset("no-assertions"))
81  options.set_option("assertions", false);
82  else
83  options.set_option("assertions", true);
84 
85  // use assumptions
86  if(cmdline.isset("no-assumptions"))
87  options.set_option("assumptions", false);
88  else
89  options.set_option("assumptions", true);
90 
91  // magic error label
92  if(cmdline.isset("error-label"))
93  options.set_option("error-label", cmdline.get_values("error-label"));
94 
95  // Select a specific analysis
96  if(cmdline.isset("taint"))
97  {
98  options.set_option("taint", true);
99  options.set_option("specific-analysis", true);
100  }
101  // For backwards compatibility,
102  // these are first recognised as specific analyses
103  bool reachability_task = false;
104  if(cmdline.isset("unreachable-instructions"))
105  {
106  options.set_option("unreachable-instructions", true);
107  options.set_option("specific-analysis", true);
108  reachability_task = true;
109  }
110  if(cmdline.isset("unreachable-functions"))
111  {
112  options.set_option("unreachable-functions", true);
113  options.set_option("specific-analysis", true);
114  reachability_task = true;
115  }
116  if(cmdline.isset("reachable-functions"))
117  {
118  options.set_option("reachable-functions", true);
119  options.set_option("specific-analysis", true);
120  reachability_task = true;
121  }
122  if(cmdline.isset("show-local-may-alias"))
123  {
124  options.set_option("show-local-may-alias", true);
125  options.set_option("specific-analysis", true);
126  }
127 
128  // Output format choice
129  if(cmdline.isset("text"))
130  {
131  options.set_option("text", true);
132  options.set_option("outfile", cmdline.get_value("text"));
133  }
134  else if(cmdline.isset("json"))
135  {
136  options.set_option("json", true);
137  options.set_option("outfile", cmdline.get_value("json"));
138  }
139  else if(cmdline.isset("xml"))
140  {
141  options.set_option("xml", true);
142  options.set_option("outfile", cmdline.get_value("xml"));
143  }
144  else if(cmdline.isset("dot"))
145  {
146  options.set_option("dot", true);
147  options.set_option("outfile", cmdline.get_value("dot"));
148  }
149  else
150  {
151  options.set_option("text", true);
152  options.set_option("outfile", "-");
153  }
154 
155  // The use should either select:
156  // 1. a specific analysis, or
157  // 2. a triple of task / analyzer / domain, or
158  // 3. one of the general display options
159 
160  // Task options
161  if(cmdline.isset("show"))
162  {
163  options.set_option("show", true);
164  options.set_option("general-analysis", true);
165  }
166  else if(cmdline.isset("verify"))
167  {
168  options.set_option("verify", true);
169  options.set_option("general-analysis", true);
170  }
171  else if(cmdline.isset("simplify"))
172  {
173  options.set_option("simplify", true);
174  options.set_option("outfile", cmdline.get_value("simplify"));
175  options.set_option("general-analysis", true);
176 
177  // For development allow slicing to be disabled in the simplify task
178  options.set_option(
179  "simplify-slicing", !(cmdline.isset("no-simplify-slicing")));
180  }
181  else if(cmdline.isset("show-intervals"))
182  {
183  // For backwards compatibility
184  options.set_option("show", true);
185  options.set_option("general-analysis", true);
186  options.set_option("intervals", true);
187  options.set_option("domain set", true);
188  }
189  else if(cmdline.isset("(show-non-null)"))
190  {
191  // For backwards compatibility
192  options.set_option("show", true);
193  options.set_option("general-analysis", true);
194  options.set_option("non-null", true);
195  options.set_option("domain set", true);
196  }
197  else if(cmdline.isset("intervals") || cmdline.isset("non-null"))
198  {
199  // For backwards compatibility either of these on their own means show
200  options.set_option("show", true);
201  options.set_option("general-analysis", true);
202  }
203 
204  if(options.get_bool_option("general-analysis") || reachability_task)
205  {
206  // Abstract interpreter choice
207  if(cmdline.isset("location-sensitive"))
208  options.set_option("location-sensitive", true);
209  else if(cmdline.isset("concurrent"))
210  options.set_option("concurrent", true);
211  else
212  {
213  // Silently default to location-sensitive as it's the "default"
214  // view of abstract interpretation.
215  options.set_option("location-sensitive", true);
216  }
217 
218  // Domain choice
219  if(cmdline.isset("constants"))
220  {
221  options.set_option("constants", true);
222  options.set_option("domain set", true);
223  }
224  else if(cmdline.isset("dependence-graph"))
225  {
226  options.set_option("dependence-graph", true);
227  options.set_option("domain set", true);
228  }
229  else if(cmdline.isset("intervals"))
230  {
231  options.set_option("intervals", true);
232  options.set_option("domain set", true);
233  }
234  else if(cmdline.isset("non-null"))
235  {
236  options.set_option("non-null", true);
237  options.set_option("domain set", true);
238  }
239 
240  // Reachability questions, when given with a domain swap from specific
241  // to general tasks so that they can use the domain & parameterisations.
242  if(reachability_task)
243  {
244  if(options.get_bool_option("domain set"))
245  {
246  options.set_option("specific-analysis", false);
247  options.set_option("general-analysis", true);
248  }
249  }
250  else
251  {
252  if(!options.get_bool_option("domain set"))
253  {
254  // Default to constants as it is light-weight but useful
255  status() << "Domain not specified, defaulting to --constants" << eom;
256  options.set_option("constants", true);
257  }
258  }
259  }
260 }
261 
266  const optionst &options,
267  const namespacet &ns)
268 {
269  ai_baset *domain = nullptr;
270 
271  if(options.get_bool_option("location-sensitive"))
272  {
273  if(options.get_bool_option("constants"))
274  {
275  // constant_propagator_ait derives from ait<constant_propagator_domaint>
277  }
278  else if(options.get_bool_option("dependence-graph"))
279  {
280  domain = new dependence_grapht(ns);
281  }
282  else if(options.get_bool_option("intervals"))
283  {
284  domain = new ait<interval_domaint>();
285  }
286 #if 0
287  // Not actually implemented, despite the option...
288  else if(options.get_bool_option("non-null"))
289  {
290  domain=new ait<non_null_domaint>();
291  }
292 #endif
293  }
294  else if(options.get_bool_option("concurrent"))
295  {
296 #if 0
297  // Disabled until merge_shared is implemented for these
298  if(options.get_bool_option("constants"))
299  {
301  }
302  else if(options.get_bool_option("dependence-graph"))
303  {
304  domain=new dependence_grapht(ns);
305  }
306  else if(options.get_bool_option("intervals"))
307  {
309  }
310 #if 0
311  // Not actually implemented, despite the option...
312  else if(options.get_bool_option("non-null"))
313  {
315  }
316 #endif
317 #endif
318  }
319 
320  return domain;
321 }
322 
325 {
326  if(cmdline.isset("version"))
327  {
328  std::cout << CBMC_VERSION << '\n';
329  return CPROVER_EXIT_SUCCESS;
330  }
331 
332  //
333  // command line options
334  //
335 
336  optionst options;
337  get_command_line_options(options);
340 
341  //
342  // Print a banner
343  //
344  status() << "JANALYZER version " CBMC_VERSION " " << sizeof(void *) * 8
345  << "-bit " << config.this_architecture() << " "
347 
349 
350  try
351  {
353  }
354 
355  catch(const char *e)
356  {
357  error() << e << eom;
358  return CPROVER_EXIT_EXCEPTION;
359  }
360 
361  catch(const std::string &e)
362  {
363  error() << e << eom;
364  return CPROVER_EXIT_EXCEPTION;
365  }
366 
367  catch(int e)
368  {
369  error() << "Numeric exception: " << e << eom;
370  return CPROVER_EXIT_EXCEPTION;
371  }
372 
373  if(process_goto_program(options))
375 
376  // show it?
377  if(cmdline.isset("show-symbol-table"))
378  {
380  return CPROVER_EXIT_SUCCESS;
381  }
382 
383  // show it?
384  if(
385  cmdline.isset("show-goto-functions") ||
386  cmdline.isset("list-goto-functions"))
387  {
389  goto_model,
391  get_ui(),
392  cmdline.isset("list-goto-functions"));
393  return CPROVER_EXIT_SUCCESS;
394  }
395 
396  try
397  {
398  return perform_analysis(options);
399  }
400 
401  catch(const char *e)
402  {
403  error() << e << eom;
404  return CPROVER_EXIT_EXCEPTION;
405  }
406 
407  catch(const std::string &e)
408  {
409  error() << e << eom;
410  return CPROVER_EXIT_EXCEPTION;
411  }
412 
413  catch(int e)
414  {
415  error() << "Numeric exception: " << e << eom;
416  return CPROVER_EXIT_EXCEPTION;
417  }
418 
419  catch(const std::bad_alloc &)
420  {
421  error() << "Out of memory" << eom;
423  }
424 }
425 
428 {
429  if(options.get_bool_option("taint"))
430  {
431  std::string taint_file = cmdline.get_value("taint");
432 
433  if(cmdline.isset("show-taint"))
434  {
435  taint_analysis(goto_model, taint_file, get_message_handler(), true, "");
436  return CPROVER_EXIT_SUCCESS;
437  }
438  else
439  {
440  std::string json_file = cmdline.get_value("json");
441  bool result = taint_analysis(
442  goto_model, taint_file, get_message_handler(), false, json_file);
444  }
445  }
446 
447  // If no domain is given, this lightweight version of the analysis is used.
448  if(
449  options.get_bool_option("unreachable-instructions") &&
450  options.get_bool_option("specific-analysis"))
451  {
452  const std::string json_file = cmdline.get_value("json");
453 
454  if(json_file.empty())
455  unreachable_instructions(goto_model, false, std::cout);
456  else if(json_file == "-")
457  unreachable_instructions(goto_model, true, std::cout);
458  else
459  {
460  std::ofstream ofs(json_file);
461  if(!ofs)
462  {
463  error() << "Failed to open json output `" << json_file << "'" << eom;
465  }
466 
468  }
469 
470  return CPROVER_EXIT_SUCCESS;
471  }
472 
473  if(
474  options.get_bool_option("unreachable-functions") &&
475  options.get_bool_option("specific-analysis"))
476  {
477  const std::string json_file = cmdline.get_value("json");
478 
479  if(json_file.empty())
480  unreachable_functions(goto_model, false, std::cout);
481  else if(json_file == "-")
482  unreachable_functions(goto_model, true, std::cout);
483  else
484  {
485  std::ofstream ofs(json_file);
486  if(!ofs)
487  {
488  error() << "Failed to open json output `" << json_file << "'" << eom;
490  }
491 
492  unreachable_functions(goto_model, true, ofs);
493  }
494 
495  return CPROVER_EXIT_SUCCESS;
496  }
497 
498  if(
499  options.get_bool_option("reachable-functions") &&
500  options.get_bool_option("specific-analysis"))
501  {
502  const std::string json_file = cmdline.get_value("json");
503 
504  if(json_file.empty())
505  reachable_functions(goto_model, false, std::cout);
506  else if(json_file == "-")
507  reachable_functions(goto_model, true, std::cout);
508  else
509  {
510  std::ofstream ofs(json_file);
511  if(!ofs)
512  {
513  error() << "Failed to open json output `" << json_file << "'" << eom;
515  }
516 
517  reachable_functions(goto_model, true, ofs);
518  }
519 
520  return CPROVER_EXIT_SUCCESS;
521  }
522 
523  if(options.get_bool_option("show-local-may-alias"))
524  {
526 
528  {
529  std::cout << ">>>>\n";
530  std::cout << ">>>> " << it->first << '\n';
531  std::cout << ">>>>\n";
532  local_may_aliast local_may_alias(it->second);
533  local_may_alias.output(std::cout, it->second, ns);
534  std::cout << '\n';
535  }
536 
537  return CPROVER_EXIT_SUCCESS;
538  }
539 
541 
542  if(cmdline.isset("show-properties"))
543  {
545  return CPROVER_EXIT_SUCCESS;
546  }
547 
548  if(set_properties())
550 
551  if(options.get_bool_option("general-analysis"))
552  {
553  // Output file factory
554  const std::string outfile = options.get_option("outfile");
555  std::ofstream output_stream;
556  if(!(outfile == "-"))
557  output_stream.open(outfile);
558 
559  std::ostream &out((outfile == "-") ? std::cout : output_stream);
560 
561  if(!out)
562  {
563  error() << "Failed to open output file `" << outfile << "'" << eom;
565  }
566 
567  // Build analyzer
568  status() << "Selecting abstract domain" << eom;
569  namespacet ns(goto_model.symbol_table); // Must live as long as the domain.
570  std::unique_ptr<ai_baset> analyzer(build_analyzer(options, ns));
571 
572  if(analyzer == nullptr)
573  {
574  status() << "Task / Interpreter / Domain combination not supported"
575  << messaget::eom;
577  }
578 
579  // Run
580  status() << "Computing abstract states" << eom;
581  (*analyzer)(goto_model);
582 
583  // Perform the task
584  status() << "Performing task" << eom;
585  bool result = true;
586  if(options.get_bool_option("show"))
587  {
589  goto_model, *analyzer, options, get_message_handler(), out);
590  }
591  else if(options.get_bool_option("verify"))
592  {
594  goto_model, *analyzer, options, get_message_handler(), out);
595  }
596  else if(options.get_bool_option("simplify"))
597  {
599  goto_model, *analyzer, options, get_message_handler(), out);
600  }
601  else if(options.get_bool_option("unreachable-instructions"))
602  {
604  goto_model, *analyzer, options, get_message_handler(), out);
605  }
606  else if(options.get_bool_option("unreachable-functions"))
607  {
609  goto_model, *analyzer, options, get_message_handler(), out);
610  }
611  else if(options.get_bool_option("reachable-functions"))
612  {
614  goto_model, *analyzer, options, get_message_handler(), out);
615  }
616  else
617  {
618  error() << "Unhandled task" << eom;
620  }
621 
624  }
625 
626  // Final defensive error case
627  error() << "no analysis option given -- consider reading --help" << eom;
629 }
630 
632 {
633  try
634  {
635  if(cmdline.isset("property"))
637  }
638 
639  catch(const char *e)
640  {
641  error() << e << eom;
642  return true;
643  }
644 
645  catch(const std::string &e)
646  {
647  error() << e << eom;
648  return true;
649  }
650 
651  catch(int)
652  {
653  return true;
654  }
655 
656  return false;
657 }
658 
660 {
661  try
662  {
663  // remove function pointers
664  status() << "Removing function pointers and virtual functions" << eom;
666  get_message_handler(), goto_model, cmdline.isset("pointer-check"));
667  // Java virtual functions -> explicit dispatch tables:
669  // remove Java throw and catch
670  // This introduces instanceof, so order is important:
672  // remove rtti
674 
675  // do partial inlining
676  status() << "Partial Inlining" << eom;
678 
679  // remove returns, gcc vectors, complex
683 
684  // add generic checks
685  status() << "Generic Property Instrumentation" << eom;
686  goto_check(options, goto_model);
687 
688  // recalculate numbers, etc.
690 
691  // add loop ids
693  }
694 
695  catch(const char *e)
696  {
697  error() << e << eom;
698  return true;
699  }
700 
701  catch(const std::string &e)
702  {
703  error() << e << eom;
704  return true;
705  }
706 
707  catch(int)
708  {
709  return true;
710  }
711 
712  catch(const std::bad_alloc &)
713  {
714  error() << "Out of memory" << eom;
715  return true;
716  }
717 
718  return false;
719 }
720 
723 {
724  // clang-format off
725  std::cout << '\n' << banner_string("JANALYZER", CBMC_VERSION) << '\n'
726  <<
727  /* NOLINTNEXTLINE(whitespace/line_length) */
728  "* * Copyright (C) 2016-2018 * *\n"
729  "* * Daniel Kroening, Diffblue * *\n"
730  "* * kroening@kroening.com * *\n"
731  "\n"
732  "Usage: Purpose:\n"
733  "\n"
734  " janalyzer [-?] [-h] [--help] show help\n"
735  " janalyzer class name of class to be checked\n"
736  "\n"
737  "Task options:\n"
738  " --show display the abstract domains\n"
739  // NOLINTNEXTLINE(whitespace/line_length)
740  " --verify use the abstract domains to check assertions\n"
741  // NOLINTNEXTLINE(whitespace/line_length)
742  " --simplify file_name use the abstract domains to simplify the program\n"
743  " --unreachable-instructions list dead code\n"
744  // NOLINTNEXTLINE(whitespace/line_length)
745  " --unreachable-functions list functions unreachable from the entry point\n"
746  // NOLINTNEXTLINE(whitespace/line_length)
747  " --reachable-functions list functions reachable from the entry point\n"
748  "\n"
749  "Abstract interpreter options:\n"
750  // NOLINTNEXTLINE(whitespace/line_length)
751  " --location-sensitive use location-sensitive abstract interpreter\n"
752  " --concurrent use concurrency-aware abstract interpreter\n"
753  "\n"
754  "Domain options:\n"
755  " --constants constant domain\n"
756  " --intervals interval domain\n"
757  " --non-null non-null domain\n"
758  " --dependence-graph data and control dependencies between instructions\n" // NOLINT(*)
759  "\n"
760  "Output options:\n"
761  " --text file_name output results in plain text to given file\n"
762  // NOLINTNEXTLINE(whitespace/line_length)
763  " --json file_name output results in JSON format to given file\n"
764  " --xml file_name output results in XML format to given file\n"
765  " --dot file_name output results in DOT format to given file\n"
766  "\n"
767  "Specific analyses:\n"
768  // NOLINTNEXTLINE(whitespace/line_length)
769  " --taint file_name perform taint analysis using rules in given file\n"
770  "\n"
771  "Java Bytecode frontend options:\n"
772  " --classpath dir/jar set the classpath\n"
773  " --main-class class-name set the name of the main class\n"
776  "\n"
777  "Program representations:\n"
778  " --show-parse-tree show parse tree\n"
779  " --show-symbol-table show loaded symbol table\n"
782  "\n"
783  "Program instrumentation options:\n"
785  "\n"
786  "Other options:\n"
787  " --version show version and exit\n"
789  "\n";
790  // clang-format on
791 }
const std::list< std::string > & get_values(const std::string &option) const
Definition: cmdline.cpp:110
Over-approximate Concurrency for Threaded Goto Programs.
Remove function exceptional returns.
janalyzer_parse_optionst(int argc, const char **argv)
Remove Instance-of Operators.
Remove Indirect Function Calls.
Remove Virtual Function (Method) Calls.
Field-Sensitive Program Dependence Analysis, Litvak et al., FSE 2010.
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.
std::string get_value(char option) const
Definition: cmdline.cpp:45
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
void remove_virtual_functions(const symbol_table_baset &symbol_table, goto_functionst &goto_functions)
#define HELP_FUNCTIONS
#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
virtual int perform_analysis(const optionst &options)
Depending on the command line mode, run one of the analysis tasks.
bool set(const cmdlinet &cmdline)
Definition: config.cpp:737
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)
void remove_instanceof(goto_programt::targett target, goto_programt &goto_program, symbol_table_baset &symbol_table)
Replace an instanceof in the expression or guard of the passed instruction of the given function body...
#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
void remove_exceptions(symbol_table_baset &symbol_table, goto_functionst &goto_functions, remove_exceptions_typest type)
removes throws/CATCH-POP/CATCH-PUSH
const std::string get_option(const std::string &option) const
Definition: options.cpp:65
bool get_bool_option(const std::string &option) const
Definition: options.cpp:42
mstreamt & error() const
Definition: message.h:302
virtual int doit() override
invoke main modules
TO_BE_DOCUMENTED.
Definition: namespace.h:74
Function Inlining.
Abstract interface to support a programming language.
std::unique_ptr< languaget > new_java_bytecode_language()
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.
Remove function returns.
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
void goto_check(const namespacet &ns, const optionst &options, const irep_idt &mode, goto_functionst::goto_functiont &goto_function)
#define CPROVER_EXIT_EXCEPTION
An (unanticipated) exception was thrown during computation.
Definition: exit_codes.h:36
virtual bool process_goto_program(const 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
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.
virtual void get_command_line_options(optionst &options)
ui_message_handlert::uit get_ui()
message_handlert & get_message_handler()
Definition: message.h:153
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 JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP
#define HELP_SHOW_GOTO_FUNCTIONS
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: 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
JANALYZER Command Line Option Processing.
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)
Taint Analysis.
Remove the &#39;vector&#39; data type by compilation into arrays.
#define JANALYZER_OPTIONS
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
virtual void help() override
display command line help
#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
void reachable_functions(const goto_modelt &goto_model, const bool json, std::ostream &os)
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
ui_message_handlert ui_message_handler
Field-insensitive, location-sensitive may-alias analysis.
void show_properties(const namespacet &ns, const irep_idt &identifier, message_handlert &message_handler, ui_message_handlert::uit ui, const goto_programt &goto_program)