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  if(cmdline.isset("function"))
81  options.set_option("function", cmdline.get_value("function"));
82 
84 
85  // check assertions
86  if(cmdline.isset("no-assertions"))
87  options.set_option("assertions", false);
88  else
89  options.set_option("assertions", true);
90 
91  // use assumptions
92  if(cmdline.isset("no-assumptions"))
93  options.set_option("assumptions", false);
94  else
95  options.set_option("assumptions", true);
96 
97  // magic error label
98  if(cmdline.isset("error-label"))
99  options.set_option("error-label", cmdline.get_values("error-label"));
100 
101  // Select a specific analysis
102  if(cmdline.isset("taint"))
103  {
104  options.set_option("taint", true);
105  options.set_option("specific-analysis", true);
106  }
107  // For backwards compatibility,
108  // these are first recognised as specific analyses
109  bool reachability_task = false;
110  if(cmdline.isset("unreachable-instructions"))
111  {
112  options.set_option("unreachable-instructions", true);
113  options.set_option("specific-analysis", true);
114  reachability_task = true;
115  }
116  if(cmdline.isset("unreachable-functions"))
117  {
118  options.set_option("unreachable-functions", true);
119  options.set_option("specific-analysis", true);
120  reachability_task = true;
121  }
122  if(cmdline.isset("reachable-functions"))
123  {
124  options.set_option("reachable-functions", true);
125  options.set_option("specific-analysis", true);
126  reachability_task = true;
127  }
128  if(cmdline.isset("show-local-may-alias"))
129  {
130  options.set_option("show-local-may-alias", true);
131  options.set_option("specific-analysis", true);
132  }
133 
134  // Output format choice
135  if(cmdline.isset("text"))
136  {
137  options.set_option("text", true);
138  options.set_option("outfile", cmdline.get_value("text"));
139  }
140  else if(cmdline.isset("json"))
141  {
142  options.set_option("json", true);
143  options.set_option("outfile", cmdline.get_value("json"));
144  }
145  else if(cmdline.isset("xml"))
146  {
147  options.set_option("xml", true);
148  options.set_option("outfile", cmdline.get_value("xml"));
149  }
150  else if(cmdline.isset("dot"))
151  {
152  options.set_option("dot", true);
153  options.set_option("outfile", cmdline.get_value("dot"));
154  }
155  else
156  {
157  options.set_option("text", true);
158  options.set_option("outfile", "-");
159  }
160 
161  // The use should either select:
162  // 1. a specific analysis, or
163  // 2. a triple of task / analyzer / domain, or
164  // 3. one of the general display options
165 
166  // Task options
167  if(cmdline.isset("show"))
168  {
169  options.set_option("show", true);
170  options.set_option("general-analysis", true);
171  }
172  else if(cmdline.isset("verify"))
173  {
174  options.set_option("verify", true);
175  options.set_option("general-analysis", true);
176  }
177  else if(cmdline.isset("simplify"))
178  {
179  options.set_option("simplify", true);
180  options.set_option("outfile", cmdline.get_value("simplify"));
181  options.set_option("general-analysis", true);
182 
183  // For development allow slicing to be disabled in the simplify task
184  options.set_option(
185  "simplify-slicing", !(cmdline.isset("no-simplify-slicing")));
186  }
187  else if(cmdline.isset("show-intervals"))
188  {
189  // For backwards compatibility
190  options.set_option("show", true);
191  options.set_option("general-analysis", true);
192  options.set_option("intervals", true);
193  options.set_option("domain set", true);
194  }
195  else if(cmdline.isset("(show-non-null)"))
196  {
197  // For backwards compatibility
198  options.set_option("show", true);
199  options.set_option("general-analysis", true);
200  options.set_option("non-null", true);
201  options.set_option("domain set", true);
202  }
203  else if(cmdline.isset("intervals") || cmdline.isset("non-null"))
204  {
205  // For backwards compatibility either of these on their own means show
206  options.set_option("show", true);
207  options.set_option("general-analysis", true);
208  }
209 
210  if(options.get_bool_option("general-analysis") || reachability_task)
211  {
212  // Abstract interpreter choice
213  if(cmdline.isset("location-sensitive"))
214  options.set_option("location-sensitive", true);
215  else if(cmdline.isset("concurrent"))
216  options.set_option("concurrent", true);
217  else
218  {
219  // Silently default to location-sensitive as it's the "default"
220  // view of abstract interpretation.
221  options.set_option("location-sensitive", true);
222  }
223 
224  // Domain choice
225  if(cmdline.isset("constants"))
226  {
227  options.set_option("constants", true);
228  options.set_option("domain set", true);
229  }
230  else if(cmdline.isset("dependence-graph"))
231  {
232  options.set_option("dependence-graph", true);
233  options.set_option("domain set", true);
234  }
235  else if(cmdline.isset("intervals"))
236  {
237  options.set_option("intervals", true);
238  options.set_option("domain set", true);
239  }
240  else if(cmdline.isset("non-null"))
241  {
242  options.set_option("non-null", true);
243  options.set_option("domain set", true);
244  }
245 
246  // Reachability questions, when given with a domain swap from specific
247  // to general tasks so that they can use the domain & parameterisations.
248  if(reachability_task)
249  {
250  if(options.get_bool_option("domain set"))
251  {
252  options.set_option("specific-analysis", false);
253  options.set_option("general-analysis", true);
254  }
255  }
256  else
257  {
258  if(!options.get_bool_option("domain set"))
259  {
260  // Default to constants as it is light-weight but useful
261  status() << "Domain not specified, defaulting to --constants" << eom;
262  options.set_option("constants", true);
263  }
264  }
265  }
266 }
267 
272  const optionst &options,
273  const namespacet &ns)
274 {
275  ai_baset *domain = nullptr;
276 
277  if(options.get_bool_option("location-sensitive"))
278  {
279  if(options.get_bool_option("constants"))
280  {
281  // constant_propagator_ait derives from ait<constant_propagator_domaint>
283  }
284  else if(options.get_bool_option("dependence-graph"))
285  {
286  domain = new dependence_grapht(ns);
287  }
288  else if(options.get_bool_option("intervals"))
289  {
290  domain = new ait<interval_domaint>();
291  }
292 #if 0
293  // Not actually implemented, despite the option...
294  else if(options.get_bool_option("non-null"))
295  {
296  domain=new ait<non_null_domaint>();
297  }
298 #endif
299  }
300  else if(options.get_bool_option("concurrent"))
301  {
302 #if 0
303  // Disabled until merge_shared is implemented for these
304  if(options.get_bool_option("constants"))
305  {
307  }
308  else if(options.get_bool_option("dependence-graph"))
309  {
310  domain=new dependence_grapht(ns);
311  }
312  else if(options.get_bool_option("intervals"))
313  {
315  }
316 #if 0
317  // Not actually implemented, despite the option...
318  else if(options.get_bool_option("non-null"))
319  {
321  }
322 #endif
323 #endif
324  }
325 
326  return domain;
327 }
328 
331 {
332  if(cmdline.isset("version"))
333  {
334  std::cout << CBMC_VERSION << '\n';
335  return CPROVER_EXIT_SUCCESS;
336  }
337 
338  //
339  // command line options
340  //
341 
342  optionst options;
343  get_command_line_options(options);
346 
347  //
348  // Print a banner
349  //
350  status() << "JANALYZER version " << CBMC_VERSION << " " << sizeof(void *) * 8
351  << "-bit " << config.this_architecture() << " "
353 
355 
356  try
357  {
358  goto_model =
360  }
361 
362  catch(const char *e)
363  {
364  error() << e << eom;
365  return CPROVER_EXIT_EXCEPTION;
366  }
367 
368  catch(const std::string &e)
369  {
370  error() << e << eom;
371  return CPROVER_EXIT_EXCEPTION;
372  }
373 
374  catch(int e)
375  {
376  error() << "Numeric exception: " << e << eom;
377  return CPROVER_EXIT_EXCEPTION;
378  }
379 
380  if(process_goto_program(options))
382 
383  // show it?
384  if(cmdline.isset("show-symbol-table"))
385  {
387  return CPROVER_EXIT_SUCCESS;
388  }
389 
390  // show it?
391  if(
392  cmdline.isset("show-goto-functions") ||
393  cmdline.isset("list-goto-functions"))
394  {
396  goto_model,
398  get_ui(),
399  cmdline.isset("list-goto-functions"));
400  return CPROVER_EXIT_SUCCESS;
401  }
402 
403  try
404  {
405  return perform_analysis(options);
406  }
407 
408  catch(const char *e)
409  {
410  error() << e << eom;
411  return CPROVER_EXIT_EXCEPTION;
412  }
413 
414  catch(const std::string &e)
415  {
416  error() << e << eom;
417  return CPROVER_EXIT_EXCEPTION;
418  }
419 
420  catch(int e)
421  {
422  error() << "Numeric exception: " << e << eom;
423  return CPROVER_EXIT_EXCEPTION;
424  }
425 
426  catch(const std::bad_alloc &)
427  {
428  error() << "Out of memory" << eom;
430  }
431 }
432 
435 {
436  if(options.get_bool_option("taint"))
437  {
438  std::string taint_file = cmdline.get_value("taint");
439 
440  if(cmdline.isset("show-taint"))
441  {
442  taint_analysis(goto_model, taint_file, get_message_handler(), true, "");
443  return CPROVER_EXIT_SUCCESS;
444  }
445  else
446  {
447  std::string json_file = cmdline.get_value("json");
448  bool result = taint_analysis(
449  goto_model, taint_file, get_message_handler(), false, json_file);
451  }
452  }
453 
454  // If no domain is given, this lightweight version of the analysis is used.
455  if(
456  options.get_bool_option("unreachable-instructions") &&
457  options.get_bool_option("specific-analysis"))
458  {
459  const std::string json_file = cmdline.get_value("json");
460 
461  if(json_file.empty())
462  unreachable_instructions(goto_model, false, std::cout);
463  else if(json_file == "-")
464  unreachable_instructions(goto_model, true, std::cout);
465  else
466  {
467  std::ofstream ofs(json_file);
468  if(!ofs)
469  {
470  error() << "Failed to open json output `" << json_file << "'" << eom;
472  }
473 
475  }
476 
477  return CPROVER_EXIT_SUCCESS;
478  }
479 
480  if(
481  options.get_bool_option("unreachable-functions") &&
482  options.get_bool_option("specific-analysis"))
483  {
484  const std::string json_file = cmdline.get_value("json");
485 
486  if(json_file.empty())
487  unreachable_functions(goto_model, false, std::cout);
488  else if(json_file == "-")
489  unreachable_functions(goto_model, true, std::cout);
490  else
491  {
492  std::ofstream ofs(json_file);
493  if(!ofs)
494  {
495  error() << "Failed to open json output `" << json_file << "'" << eom;
497  }
498 
499  unreachable_functions(goto_model, true, ofs);
500  }
501 
502  return CPROVER_EXIT_SUCCESS;
503  }
504 
505  if(
506  options.get_bool_option("reachable-functions") &&
507  options.get_bool_option("specific-analysis"))
508  {
509  const std::string json_file = cmdline.get_value("json");
510 
511  if(json_file.empty())
512  reachable_functions(goto_model, false, std::cout);
513  else if(json_file == "-")
514  reachable_functions(goto_model, true, std::cout);
515  else
516  {
517  std::ofstream ofs(json_file);
518  if(!ofs)
519  {
520  error() << "Failed to open json output `" << json_file << "'" << eom;
522  }
523 
524  reachable_functions(goto_model, true, ofs);
525  }
526 
527  return CPROVER_EXIT_SUCCESS;
528  }
529 
530  if(options.get_bool_option("show-local-may-alias"))
531  {
533 
535  {
536  std::cout << ">>>>\n";
537  std::cout << ">>>> " << it->first << '\n';
538  std::cout << ">>>>\n";
539  local_may_aliast local_may_alias(it->second);
540  local_may_alias.output(std::cout, it->second, ns);
541  std::cout << '\n';
542  }
543 
544  return CPROVER_EXIT_SUCCESS;
545  }
546 
548 
549  if(cmdline.isset("show-properties"))
550  {
552  return CPROVER_EXIT_SUCCESS;
553  }
554 
555  if(set_properties())
557 
558  if(options.get_bool_option("general-analysis"))
559  {
560  // Output file factory
561  const std::string outfile = options.get_option("outfile");
562  std::ofstream output_stream;
563  if(!(outfile == "-"))
564  output_stream.open(outfile);
565 
566  std::ostream &out((outfile == "-") ? std::cout : output_stream);
567 
568  if(!out)
569  {
570  error() << "Failed to open output file `" << outfile << "'" << eom;
572  }
573 
574  // Build analyzer
575  status() << "Selecting abstract domain" << eom;
576  namespacet ns(goto_model.symbol_table); // Must live as long as the domain.
577  std::unique_ptr<ai_baset> analyzer(build_analyzer(options, ns));
578 
579  if(analyzer == nullptr)
580  {
581  status() << "Task / Interpreter / Domain combination not supported"
582  << messaget::eom;
584  }
585 
586  // Run
587  status() << "Computing abstract states" << eom;
588  (*analyzer)(goto_model);
589 
590  // Perform the task
591  status() << "Performing task" << eom;
592  bool result = true;
593  if(options.get_bool_option("show"))
594  {
595  static_show_domain(goto_model, *analyzer, options, out);
596  return CPROVER_EXIT_SUCCESS;
597  }
598  else if(options.get_bool_option("verify"))
599  {
601  goto_model, *analyzer, options, get_message_handler(), out);
602  }
603  else if(options.get_bool_option("simplify"))
604  {
606  goto_model, *analyzer, options, get_message_handler(), out);
607  }
608  else if(options.get_bool_option("unreachable-instructions"))
609  {
611  goto_model, *analyzer, options, out);
612  }
613  else if(options.get_bool_option("unreachable-functions"))
614  {
616  goto_model, *analyzer, options, out);
617  }
618  else if(options.get_bool_option("reachable-functions"))
619  {
621  goto_model, *analyzer, options, out);
622  }
623  else
624  {
625  error() << "Unhandled task" << eom;
627  }
628 
631  }
632 
633  // Final defensive error case
634  error() << "no analysis option given -- consider reading --help" << eom;
636 }
637 
639 {
640  try
641  {
642  if(cmdline.isset("property"))
644  }
645 
646  catch(const char *e)
647  {
648  error() << e << eom;
649  return true;
650  }
651 
652  catch(const std::string &e)
653  {
654  error() << e << eom;
655  return true;
656  }
657 
658  catch(int)
659  {
660  return true;
661  }
662 
663  return false;
664 }
665 
667 {
668  try
669  {
670  // remove function pointers
671  status() << "Removing function pointers and virtual functions" << eom;
673  get_message_handler(), goto_model, cmdline.isset("pointer-check"));
674 
675  // Java virtual functions -> explicit dispatch tables:
677 
678  // remove Java throw and catch
679  // This introduces instanceof, so order is important:
681 
682  // Java instanceof -> clsid comparison:
683  class_hierarchyt class_hierarchy(goto_model.symbol_table);
684  remove_instanceof(goto_model, class_hierarchy, get_message_handler());
685 
686  // do partial inlining
687  status() << "Partial Inlining" << eom;
689 
690  // remove returns, gcc vectors, complex
694 
695  // add generic checks
696  status() << "Generic Property Instrumentation" << eom;
697  goto_check(options, goto_model);
698 
699  // recalculate numbers, etc.
701 
702  // add loop ids
704  }
705 
706  catch(const char *e)
707  {
708  error() << e << eom;
709  return true;
710  }
711 
712  catch(const std::string &e)
713  {
714  error() << e << eom;
715  return true;
716  }
717 
718  catch(int)
719  {
720  return true;
721  }
722 
723  catch(const std::bad_alloc &)
724  {
725  error() << "Out of memory" << eom;
726  return true;
727  }
728 
729  return false;
730 }
731 
734 {
735  // clang-format off
736  std::cout << '\n' << banner_string("JANALYZER", CBMC_VERSION) << '\n'
737  <<
738  /* NOLINTNEXTLINE(whitespace/line_length) */
739  "* * Copyright (C) 2016-2018 * *\n"
740  "* * Daniel Kroening, Diffblue * *\n"
741  "* * kroening@kroening.com * *\n"
742  "\n"
743  "Usage: Purpose:\n"
744  "\n"
745  " janalyzer [-?] [-h] [--help] show help\n"
746  " janalyzer class name of class or JAR file to be checked\n"
747  " In the case of a JAR file, if a main class can be\n" // NOLINT(*)
748  " inferred from --main-class, --function, or the JAR\n" // NOLINT(*)
749  " manifest (checked in this order), the behavior is\n" // NOLINT(*)
750  " the same as running janalyzer on the corresponding\n" // NOLINT(*)
751  " class file."
752  "\n"
753  "Task options:\n"
754  " --show display the abstract domains\n"
755  // NOLINTNEXTLINE(whitespace/line_length)
756  " --verify use the abstract domains to check assertions\n"
757  // NOLINTNEXTLINE(whitespace/line_length)
758  " --simplify file_name use the abstract domains to simplify the program\n"
759  " --unreachable-instructions list dead code\n"
760  // NOLINTNEXTLINE(whitespace/line_length)
761  " --unreachable-functions list functions unreachable from the entry point\n"
762  // NOLINTNEXTLINE(whitespace/line_length)
763  " --reachable-functions list functions reachable from the entry point\n"
764  "\n"
765  "Abstract interpreter options:\n"
766  // NOLINTNEXTLINE(whitespace/line_length)
767  " --location-sensitive use location-sensitive abstract interpreter\n"
768  " --concurrent use concurrency-aware abstract interpreter\n"
769  "\n"
770  "Domain options:\n"
771  " --constants constant domain\n"
772  " --intervals interval domain\n"
773  " --non-null non-null domain\n"
774  " --dependence-graph data and control dependencies between instructions\n" // NOLINT(*)
775  "\n"
776  "Output options:\n"
777  " --text file_name output results in plain text to given file\n"
778  // NOLINTNEXTLINE(whitespace/line_length)
779  " --json file_name output results in JSON format to given file\n"
780  " --xml file_name output results in XML format to given file\n"
781  " --dot file_name output results in DOT format to given file\n"
782  "\n"
783  "Specific analyses:\n"
784  // NOLINTNEXTLINE(whitespace/line_length)
785  " --taint file_name perform taint analysis using rules in given file\n"
786  "\n"
787  "Java Bytecode frontend options:\n"
788  " --classpath dir/jar set the classpath\n"
789  " --main-class class-name set the name of the main class\n"
792  "\n"
793  "Program representations:\n"
794  " --show-parse-tree show parse tree\n"
795  " --show-symbol-table show loaded symbol table\n"
798  "\n"
799  "Program instrumentation options:\n"
801  "\n"
802  "Other options:\n"
803  " --version show version and exit\n"
805  "\n";
806  // clang-format on
807 }
taint_analysis
bool taint_analysis(goto_modelt &goto_model, const std::string &taint_file_name, message_handlert &message_handler, bool show_full, const std::string &json_file_name)
Definition: taint_analysis.cpp:414
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:144
cmdlinet::args
argst args
Definition: cmdline.h:44
CBMC_VERSION
const char * CBMC_VERSION
Definition: version.cpp:1
HELP_SHOW_GOTO_FUNCTIONS
#define HELP_SHOW_GOTO_FUNCTIONS
Definition: show_goto_functions.h:26
local_may_aliast::output
void output(std::ostream &out, const goto_functiont &goto_function, const namespacet &ns) const
Definition: local_may_alias.cpp:438
class_hierarchyt
Non-graph-based representation of the class hierarchy.
Definition: class_hierarchy.h:42
CPROVER_EXIT_VERIFICATION_UNSAFE
#define CPROVER_EXIT_VERIFICATION_UNSAFE
Verification successful indicates the analysis has been performed without error AND the software is n...
Definition: exit_codes.h:25
parse_options_baset
Definition: parse_options.h:17
janalyzer_parse_optionst::build_analyzer
ai_baset * build_analyzer(const optionst &, const namespacet &ns)
For the task, build the appropriate kind of analyzer Ideally this should be a pure function of option...
Definition: janalyzer_parse_options.cpp:271
java_bytecode_language.h
JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP
#define JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP
Definition: java_bytecode_language.h:44
parse_java_language_options
void parse_java_language_options(const cmdlinet &cmd, optionst &options)
Parse options that are java bytecode specific.
Definition: java_bytecode_language.cpp:48
remove_exceptions_using_instanceof
void remove_exceptions_using_instanceof(symbol_table_baset &symbol_table, goto_functionst &goto_functions, message_handlert &message_handler)
removes throws/CATCH-POP/CATCH-PUSH
Definition: remove_exceptions.cpp:594
cmdlinet::isset
virtual bool isset(char option) const
Definition: cmdline.cpp:27
dependence_grapht
Definition: dependence_graph.h:217
janalyzer_parse_optionst::set_properties
bool set_properties()
Definition: janalyzer_parse_options.cpp:638
static_unreachable_instructions
bool static_unreachable_instructions(const goto_modelt &goto_model, const ai_baset &ai, const optionst &options, std::ostream &out)
Definition: unreachable_instructions.cpp:204
goto_inline.h
optionst
Definition: options.h:22
static_simplifier.h
janalyzer_parse_optionst::process_goto_program
virtual bool process_goto_program(const optionst &options)
Definition: janalyzer_parse_options.cpp:666
static_simplifier
bool static_simplifier(goto_modelt &goto_model, const ai_baset &ai, const optionst &options, message_handlert &message_handler, std::ostream &out)
Simplifies the program using the information in the abstract domain.
Definition: static_simplifier.cpp:29
CPROVER_EXIT_INTERNAL_OUT_OF_MEMORY
#define CPROVER_EXIT_INTERNAL_OUT_OF_MEMORY
Memory allocation has failed and this has been detected within the program.
Definition: exit_codes.h:53
optionst::get_option
const std::string get_option(const std::string &option) const
Definition: options.cpp:65
messaget::M_STATISTICS
Definition: message.h:161
messaget::status
mstreamt & status() const
Definition: message.h:401
show_properties
void show_properties(const namespacet &ns, const irep_idt &identifier, message_handlert &message_handler, ui_message_handlert::uit ui, const goto_programt &goto_program)
Definition: show_properties.cpp:49
HELP_FUNCTIONS
#define HELP_FUNCTIONS
Definition: rebuild_goto_start_function.h:24
static_verifier.h
goto_partial_inline
void goto_partial_inline(goto_modelt &goto_model, message_handlert &message_handler, unsigned smallfunc_limit, bool adjust_function)
Inline all function calls to functions either marked as "inlined" or smaller than smallfunc_limit (by...
Definition: goto_inline.cpp:109
remove_virtual_functions
void remove_virtual_functions(const symbol_table_baset &symbol_table, goto_functionst &goto_functions)
Remove virtual function calls from all functions in the specified list and replace them with their mo...
Definition: remove_virtual_functions.cpp:568
janalyzer_parse_optionst::register_languages
virtual void register_languages()
Definition: janalyzer_parse_options.cpp:67
new_java_bytecode_language
std::unique_ptr< languaget > new_java_bytecode_language()
Definition: java_bytecode_language.cpp:1183
static_verifier
bool static_verifier(const goto_modelt &goto_model, const ai_baset &ai, const optionst &options, message_handlert &message_handler, std::ostream &out)
Runs the analyzer and then prints out the domain.
Definition: static_verifier.cpp:234
show_goto_functions
void show_goto_functions(const namespacet &ns, message_handlert &message_handler, ui_message_handlert::uit ui, const goto_functionst &goto_functions, bool list_only)
Definition: show_goto_functions.cpp:28
taint_analysis.h
remove_virtual_functions.h
constant_propagator.h
ait
Definition: ai.h:365
CPROVER_EXIT_EXCEPTION
#define CPROVER_EXIT_EXCEPTION
An (unanticipated) exception was thrown during computation.
Definition: exit_codes.h:41
mode.h
options.h
CPROVER_EXIT_VERIFICATION_SAFE
#define CPROVER_EXIT_VERIFICATION_SAFE
Verification successful indicates the analysis has been performed without error AND the software is s...
Definition: exit_codes.h:21
optionst::set_option
void set_option(const std::string &option, const bool value)
Definition: options.cpp:26
messaget::eom
static eomt eom
Definition: message.h:284
show_symbol_table
void show_symbol_table(const symbol_tablet &symbol_table, ui_message_handlert &ui)
Definition: show_symbol_table.cpp:283
version.h
local_may_aliast
Definition: local_may_alias.h:25
label_properties
void label_properties(goto_modelt &goto_model)
Definition: set_properties.cpp:43
janalyzer_parse_optionst::help
virtual void help() override
display command line help
Definition: janalyzer_parse_options.cpp:733
parse_options_baset::usage_error
virtual void usage_error()
Definition: parse_options.cpp:36
reachable_functions
void reachable_functions(const goto_modelt &goto_model, const bool json, std::ostream &os)
Definition: unreachable_instructions.cpp:392
remove_vector
static void remove_vector(typet &)
removes vector data type
Definition: remove_vector.cpp:167
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
remove_complex.h
janalyzer_parse_optionst::janalyzer_parse_optionst
janalyzer_parse_optionst(int argc, const char **argv)
Definition: janalyzer_parse_options.cpp:60
set_properties.h
janalyzer_parse_optionst::doit
virtual int doit() override
invoke main modules
Definition: janalyzer_parse_options.cpp:330
messaget::result
mstreamt & result() const
Definition: message.h:396
unreachable_functions
void unreachable_functions(const goto_modelt &goto_model, const bool json, std::ostream &os)
Definition: unreachable_instructions.cpp:378
messaget::error
mstreamt & error() const
Definition: message.h:386
initialize_goto_model.h
banner_string
std::string banner_string(const std::string &front_end, const std::string &version)
Definition: parse_options.cpp:87
local_may_alias.h
remove_function_pointers
bool remove_function_pointers(message_handlert &_message_handler, symbol_tablet &symbol_table, const goto_functionst &goto_functions, goto_programt &goto_program, bool add_safety_assertion, bool only_remove_const_fps)
Definition: remove_function_pointers.cpp:520
janalyzer_parse_optionst::ui_message_handler
ui_message_handlert ui_message_handler
Definition: janalyzer_parse_options.h:162
show_properties.h
is_threaded.h
cmdlinet::get_value
std::string get_value(char option) const
Definition: cmdline.cpp:45
show_symbol_table.h
language.h
unreachable_instructions.h
HELP_SHOW_PROPERTIES
#define HELP_SHOW_PROPERTIES
Definition: show_properties.h:29
configt::this_operating_system
static irep_idt this_operating_system()
Definition: config.cpp:1368
goto_check
void goto_check(const namespacet &ns, const optionst &options, const irep_idt &mode, goto_functionst::goto_functiont &goto_function)
Definition: goto_check.cpp:1784
CPROVER_EXIT_SET_PROPERTIES_FAILED
#define CPROVER_EXIT_SET_PROPERTIES_FAILED
Failure to identify the properties to verify.
Definition: exit_codes.h:56
static_show_domain
void static_show_domain(const goto_modelt &goto_model, const ai_baset &ai, const optionst &options, std::ostream &out)
Runs the analyzer and then prints out the domain.
Definition: static_show_domain.cpp:20
goto_check.h
goto_functionst::compute_loop_numbers
void compute_loop_numbers()
Definition: goto_functions.cpp:52
read_goto_binary.h
janalyzer_parse_options.h
janalyzer_parse_optionst::get_ui
ui_message_handlert::uit get_ui()
Definition: janalyzer_parse_options.h:176
unreachable_instructions
static void unreachable_instructions(const goto_programt &goto_program, dead_mapt &dest)
Definition: unreachable_instructions.cpp:28
remove_vector.h
remove_complex
static void remove_complex(typet &)
removes complex data type
Definition: remove_complex.cpp:240
remove_returns.h
remove_exceptions.h
config
configt config
Definition: config.cpp:24
remove_instanceof.h
configt::this_architecture
static irep_idt this_architecture()
Definition: config.cpp:1268
remove_instanceof
void remove_instanceof(goto_programt::targett target, goto_programt &goto_program, symbol_table_baset &symbol_table, const class_hierarchyt &class_hierarchy, message_handlert &message_handler)
Replace an instanceof in the expression or guard of the passed instruction of the given function body...
Definition: remove_instanceof.cpp:243
messaget::get_message_handler
message_handlert & get_message_handler()
Definition: message.h:174
interval_domain.h
register_language
void register_language(language_factoryt factory)
Register a language Note: registering a language is required for using the functions in language_util...
Definition: mode.cpp:38
janalyzer_parse_optionst::get_command_line_options
virtual void get_command_line_options(optionst &options)
Definition: janalyzer_parse_options.cpp:72
janalyzer_parse_optionst::perform_analysis
virtual int perform_analysis(const optionst &options)
Depending on the command line mode, run one of the analysis tasks.
Definition: janalyzer_parse_options.cpp:434
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
static_reachable_functions
bool static_reachable_functions(const goto_modelt &goto_model, const ai_baset &ai, const optionst &options, std::ostream &out)
Definition: unreachable_instructions.cpp:440
ansi_c_language.h
HELP_GOTO_CHECK
#define HELP_GOTO_CHECK
Definition: goto_check.h:43
configt::set
bool set(const cmdlinet &cmdline)
Definition: config.cpp:767
exit_codes.h
optionst::get_bool_option
bool get_bool_option(const std::string &option) const
Definition: options.cpp:42
constant_propagator_ait
Definition: constant_propagator.h:162
concurrency_aware_ait
Definition: ai.h:467
remove_returns
void remove_returns(symbol_table_baset &symbol_table, goto_functionst &goto_functions)
removes returns
Definition: remove_returns.cpp:261
ai_baset
The basic interface of an abstract interpreter.
Definition: ai.h:32
CPROVER_EXIT_USAGE_ERROR
#define CPROVER_EXIT_USAGE_ERROR
A usage error is returned when the command line is invalid or conflicting.
Definition: exit_codes.h:33
goto_functionst::update
void update()
Definition: goto_functions.h:91
unicode.h
config.h
forall_goto_functions
#define forall_goto_functions(it, functions)
Definition: goto_functions.h:149
CPROVER_EXIT_INTERNAL_ERROR
#define CPROVER_EXIT_INTERNAL_ERROR
An error has been encountered during processing the requested analysis.
Definition: exit_codes.h:46
initialize_goto_model
goto_modelt initialize_goto_model(const std::vector< std::string > &files, message_handlert &message_handler, const optionst &options)
Definition: initialize_goto_model.cpp:32
goto_convert_functions.h
static_unreachable_functions
bool static_unreachable_functions(const goto_modelt &goto_model, const ai_baset &ai, const optionst &options, std::ostream &out)
Definition: unreachable_instructions.cpp:426
CPROVER_EXIT_SUCCESS
#define CPROVER_EXIT_SUCCESS
Success indicates the required analysis has been performed without error.
Definition: exit_codes.h:16
messaget::eval_verbosity
static unsigned eval_verbosity(const std::string &user_input, const message_levelt default_verbosity, message_handlert &dest)
Parse a (user-)provided string as a verbosity level and set it as the verbosity of dest.
Definition: message.cpp:98
JANALYZER_OPTIONS
#define JANALYZER_OPTIONS
Definition: janalyzer_parse_options.h:123
cmdlinet::get_values
const std::list< std::string > & get_values(const std::string &option) const
Definition: cmdline.cpp:110
remove_function_pointers.h
parse_options_baset::cmdline
cmdlinet cmdline
Definition: parse_options.h:23
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
static_show_domain.h
dependence_graph.h
janalyzer_parse_optionst::goto_model
goto_modelt goto_model
Definition: janalyzer_parse_options.h:163
HELP_TIMESTAMP
#define HELP_TIMESTAMP
Definition: timestamper.h:14