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