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>
20 
33 
36 #include <analyses/goto_check.h>
38 #include <analyses/is_threaded.h>
40 
45 
46 #include <langapi/language.h>
47 #include <langapi/mode.h>
48 
50 
51 #include <util/config.h>
52 #include <util/exit_codes.h>
53 #include <util/options.h>
54 #include <util/unicode.h>
55 #include <util/version.h>
56 
62 
66  argc,
67  argv,
68  std::string("JANALYZER ") + CBMC_VERSION)
69 {
70 }
71 
73 {
74  // Need ansi C language for __CPROVER_rounding_mode
77 }
78 
80 {
81  if(config.set(cmdline))
82  {
83  usage_error();
85  }
86 
87  if(cmdline.isset("function"))
88  options.set_option("function", cmdline.get_value("function"));
89 
91 
92  // check assertions
93  if(cmdline.isset("no-assertions"))
94  options.set_option("assertions", false);
95  else
96  options.set_option("assertions", true);
97 
98  // use assumptions
99  if(cmdline.isset("no-assumptions"))
100  options.set_option("assumptions", false);
101  else
102  options.set_option("assumptions", true);
103 
104  // magic error label
105  if(cmdline.isset("error-label"))
106  options.set_option("error-label", cmdline.get_values("error-label"));
107 
108  // Select a specific analysis
109  if(cmdline.isset("taint"))
110  {
111  options.set_option("taint", true);
112  options.set_option("specific-analysis", true);
113  }
114  // For backwards compatibility,
115  // these are first recognised as specific analyses
116  bool reachability_task = false;
117  if(cmdline.isset("unreachable-instructions"))
118  {
119  options.set_option("unreachable-instructions", true);
120  options.set_option("specific-analysis", true);
121  reachability_task = true;
122  }
123  if(cmdline.isset("unreachable-functions"))
124  {
125  options.set_option("unreachable-functions", true);
126  options.set_option("specific-analysis", true);
127  reachability_task = true;
128  }
129  if(cmdline.isset("reachable-functions"))
130  {
131  options.set_option("reachable-functions", true);
132  options.set_option("specific-analysis", true);
133  reachability_task = true;
134  }
135  if(cmdline.isset("show-local-may-alias"))
136  {
137  options.set_option("show-local-may-alias", true);
138  options.set_option("specific-analysis", true);
139  }
140 
141  // Output format choice
142  if(cmdline.isset("text"))
143  {
144  options.set_option("text", true);
145  options.set_option("outfile", cmdline.get_value("text"));
146  }
147  else if(cmdline.isset("json"))
148  {
149  options.set_option("json", true);
150  options.set_option("outfile", cmdline.get_value("json"));
151  }
152  else if(cmdline.isset("xml"))
153  {
154  options.set_option("xml", true);
155  options.set_option("outfile", cmdline.get_value("xml"));
156  }
157  else if(cmdline.isset("dot"))
158  {
159  options.set_option("dot", true);
160  options.set_option("outfile", cmdline.get_value("dot"));
161  }
162  else
163  {
164  options.set_option("text", true);
165  options.set_option("outfile", "-");
166  }
167 
168  // The use should either select:
169  // 1. a specific analysis, or
170  // 2. a triple of task / analyzer / domain, or
171  // 3. one of the general display options
172 
173  // Task options
174  if(cmdline.isset("show"))
175  {
176  options.set_option("show", true);
177  options.set_option("general-analysis", true);
178  }
179  else if(cmdline.isset("verify"))
180  {
181  options.set_option("verify", true);
182  options.set_option("general-analysis", true);
183  }
184  else if(cmdline.isset("simplify"))
185  {
186  options.set_option("simplify", true);
187  options.set_option("outfile", cmdline.get_value("simplify"));
188  options.set_option("general-analysis", true);
189 
190  // For development allow slicing to be disabled in the simplify task
191  options.set_option(
192  "simplify-slicing", !(cmdline.isset("no-simplify-slicing")));
193  }
194  else if(cmdline.isset("show-intervals"))
195  {
196  // For backwards compatibility
197  options.set_option("show", true);
198  options.set_option("general-analysis", true);
199  options.set_option("intervals", true);
200  options.set_option("domain set", true);
201  }
202  else if(cmdline.isset("(show-non-null)"))
203  {
204  // For backwards compatibility
205  options.set_option("show", true);
206  options.set_option("general-analysis", true);
207  options.set_option("non-null", true);
208  options.set_option("domain set", true);
209  }
210  else if(cmdline.isset("intervals") || cmdline.isset("non-null"))
211  {
212  // For backwards compatibility either of these on their own means show
213  options.set_option("show", true);
214  options.set_option("general-analysis", true);
215  }
216 
217  if(options.get_bool_option("general-analysis") || reachability_task)
218  {
219  // Abstract interpreter choice
220  if(cmdline.isset("location-sensitive"))
221  options.set_option("location-sensitive", true);
222  else if(cmdline.isset("concurrent"))
223  options.set_option("concurrent", true);
224  else
225  {
226  // Silently default to location-sensitive as it's the "default"
227  // view of abstract interpretation.
228  options.set_option("location-sensitive", true);
229  }
230 
231  // Domain choice
232  if(cmdline.isset("constants"))
233  {
234  options.set_option("constants", true);
235  options.set_option("domain set", true);
236  }
237  else if(cmdline.isset("dependence-graph"))
238  {
239  options.set_option("dependence-graph", true);
240  options.set_option("domain set", true);
241  }
242  else if(cmdline.isset("intervals"))
243  {
244  options.set_option("intervals", true);
245  options.set_option("domain set", true);
246  }
247  else if(cmdline.isset("non-null"))
248  {
249  options.set_option("non-null", true);
250  options.set_option("domain set", true);
251  }
252 
253  // Reachability questions, when given with a domain swap from specific
254  // to general tasks so that they can use the domain & parameterisations.
255  if(reachability_task)
256  {
257  if(options.get_bool_option("domain set"))
258  {
259  options.set_option("specific-analysis", false);
260  options.set_option("general-analysis", true);
261  }
262  }
263  else
264  {
265  if(!options.get_bool_option("domain set"))
266  {
267  // Default to constants as it is light-weight but useful
268  log.status() << "Domain not specified, defaulting to --constants"
269  << messaget::eom;
270  options.set_option("constants", true);
271  }
272  }
273  }
274 }
275 
280  goto_modelt &goto_model,
281  const optionst &options,
282  const namespacet &ns)
283 {
284  ai_baset *domain = nullptr;
285 
286  if(options.get_bool_option("location-sensitive"))
287  {
288  if(options.get_bool_option("constants"))
289  {
290  // constant_propagator_ait derives from ait<constant_propagator_domaint>
291  domain = new constant_propagator_ait(goto_model.goto_functions);
292  }
293  else if(options.get_bool_option("dependence-graph"))
294  {
295  domain = new dependence_grapht(ns);
296  }
297  else if(options.get_bool_option("intervals"))
298  {
299  domain = new ait<interval_domaint>();
300  }
301 #if 0
302  // Not actually implemented, despite the option...
303  else if(options.get_bool_option("non-null"))
304  {
305  domain=new ait<non_null_domaint>();
306  }
307 #endif
308  }
309  else if(options.get_bool_option("concurrent"))
310  {
311 #if 0
312  // Disabled until merge_shared is implemented for these
313  if(options.get_bool_option("constants"))
314  {
316  }
317  else if(options.get_bool_option("dependence-graph"))
318  {
319  domain=new dependence_grapht(ns);
320  }
321  else if(options.get_bool_option("intervals"))
322  {
324  }
325 #if 0
326  // Not actually implemented, despite the option...
327  else if(options.get_bool_option("non-null"))
328  {
330  }
331 #endif
332 #endif
333  }
334 
335  return domain;
336 }
337 
340 {
341  if(cmdline.isset("version"))
342  {
343  std::cout << CBMC_VERSION << '\n';
344  return CPROVER_EXIT_SUCCESS;
345  }
346 
347  //
348  // command line options
349  //
350 
351  optionst options;
352  get_command_line_options(options);
355 
356  //
357  // Print a banner
358  //
359  log.status() << "JANALYZER version " << CBMC_VERSION << " "
360  << sizeof(void *) * 8 << "-bit " << config.this_architecture()
362 
364 
365  if(!((cmdline.isset("jar") && cmdline.args.empty()) ||
366  (cmdline.isset("gb") && cmdline.args.empty()) ||
367  (!cmdline.isset("jar") && !cmdline.isset("gb") &&
368  (cmdline.args.size() == 1))))
369  {
370  log.error() << "Please give exactly one class name, "
371  << "and/or use -jar jarfile or --gb goto-binary"
372  << messaget::eom;
374  }
375 
376  if((cmdline.args.size() == 1) && !cmdline.isset("show-parse-tree"))
377  {
378  std::string main_class = cmdline.args[0];
379  // `java` accepts slashes and dots as package separators
380  std::replace(main_class.begin(), main_class.end(), '/', '.');
381  config.java.main_class = main_class;
382  cmdline.args.pop_back();
383  }
384 
385  if(cmdline.isset("jar"))
386  {
387  cmdline.args.push_back(cmdline.get_value("jar"));
388  }
389 
390  if(cmdline.isset("gb"))
391  {
392  cmdline.args.push_back(cmdline.get_value("gb"));
393  }
394 
395  // Shows the parse tree of the main class
396  if(cmdline.isset("show-parse-tree"))
397  {
398  std::unique_ptr<languaget> language = get_language_from_mode(ID_java);
399  CHECK_RETURN(language != nullptr);
400  language->set_language_options(options);
402 
403  log.status() << "Parsing ..." << messaget::eom;
404 
405  if(static_cast<java_bytecode_languaget *>(language.get())->parse())
406  {
407  log.error() << "PARSING ERROR" << messaget::eom;
409  }
410 
411  language->show_parse(std::cout);
412  return CPROVER_EXIT_SUCCESS;
413  }
414 
415  lazy_goto_modelt lazy_goto_model =
417  lazy_goto_model.initialize(cmdline.args, options);
418 
420  util_make_unique<class_hierarchyt>(lazy_goto_model.symbol_table);
421 
422  log.status() << "Generating GOTO Program" << messaget::eom;
423  lazy_goto_model.load_all_functions();
424 
425  std::unique_ptr<abstract_goto_modelt> goto_model_ptr =
427  std::move(lazy_goto_model));
428  if(goto_model_ptr == nullptr)
430 
431  goto_modelt &goto_model = dynamic_cast<goto_modelt &>(*goto_model_ptr);
432 
433  // show it?
434  if(cmdline.isset("show-symbol-table"))
435  {
437  return CPROVER_EXIT_SUCCESS;
438  }
439 
440  // show it?
441  if(
442  cmdline.isset("show-goto-functions") ||
443  cmdline.isset("list-goto-functions"))
444  {
446  goto_model, ui_message_handler, cmdline.isset("list-goto-functions"));
447  return CPROVER_EXIT_SUCCESS;
448  }
449 
450  return perform_analysis(goto_model, options);
451 }
452 
455  goto_modelt &goto_model,
456  const optionst &options)
457 {
458  if(options.get_bool_option("taint"))
459  {
460  std::string taint_file = cmdline.get_value("taint");
461 
462  if(cmdline.isset("show-taint"))
463  {
464  taint_analysis(goto_model, taint_file, ui_message_handler, true);
465  return CPROVER_EXIT_SUCCESS;
466  }
467  else
468  {
469  optionalt<std::string> json_file;
470  if(cmdline.isset("json"))
471  json_file = cmdline.get_value("json");
472  bool result = taint_analysis(
473  goto_model, taint_file, ui_message_handler, false, json_file);
475  }
476  }
477 
478  // If no domain is given, this lightweight version of the analysis is used.
479  if(
480  options.get_bool_option("unreachable-instructions") &&
481  options.get_bool_option("specific-analysis"))
482  {
483  const std::string json_file = cmdline.get_value("json");
484 
485  if(json_file.empty())
486  unreachable_instructions(goto_model, false, std::cout);
487  else if(json_file == "-")
488  unreachable_instructions(goto_model, true, std::cout);
489  else
490  {
491  std::ofstream ofs(json_file);
492  if(!ofs)
493  {
494  log.error() << "Failed to open json output '" << json_file << "'"
495  << messaget::eom;
497  }
498 
499  unreachable_instructions(goto_model, true, ofs);
500  }
501 
502  return CPROVER_EXIT_SUCCESS;
503  }
504 
505  if(
506  options.get_bool_option("unreachable-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  unreachable_functions(goto_model, false, std::cout);
513  else if(json_file == "-")
514  unreachable_functions(goto_model, true, std::cout);
515  else
516  {
517  std::ofstream ofs(json_file);
518  if(!ofs)
519  {
520  log.error() << "Failed to open json output '" << json_file << "'"
521  << messaget::eom;
523  }
524 
525  unreachable_functions(goto_model, true, ofs);
526  }
527 
528  return CPROVER_EXIT_SUCCESS;
529  }
530 
531  if(
532  options.get_bool_option("reachable-functions") &&
533  options.get_bool_option("specific-analysis"))
534  {
535  const std::string json_file = cmdline.get_value("json");
536 
537  if(json_file.empty())
538  reachable_functions(goto_model, false, std::cout);
539  else if(json_file == "-")
540  reachable_functions(goto_model, true, std::cout);
541  else
542  {
543  std::ofstream ofs(json_file);
544  if(!ofs)
545  {
546  log.error() << "Failed to open json output '" << json_file << "'"
547  << messaget::eom;
549  }
550 
551  reachable_functions(goto_model, true, ofs);
552  }
553 
554  return CPROVER_EXIT_SUCCESS;
555  }
556 
557  if(options.get_bool_option("show-local-may-alias"))
558  {
559  namespacet ns(goto_model.symbol_table);
560 
561  forall_goto_functions(it, goto_model.goto_functions)
562  {
563  std::cout << ">>>>\n";
564  std::cout << ">>>> " << it->first << '\n';
565  std::cout << ">>>>\n";
566  local_may_aliast local_may_alias(it->second);
567  local_may_alias.output(std::cout, it->second, ns);
568  std::cout << '\n';
569  }
570 
571  return CPROVER_EXIT_SUCCESS;
572  }
573 
574  label_properties(goto_model);
575 
576  if(cmdline.isset("show-properties"))
577  {
578  show_properties(goto_model, ui_message_handler);
579  return CPROVER_EXIT_SUCCESS;
580  }
581 
582  if(cmdline.isset("property"))
583  ::set_properties(goto_model, cmdline.get_values("property"));
584 
585  if(options.get_bool_option("general-analysis"))
586  {
587  // Output file factory
588  const std::string outfile = options.get_option("outfile");
589  std::ofstream output_stream;
590  if(!(outfile == "-"))
591  output_stream.open(outfile);
592 
593  std::ostream &out((outfile == "-") ? std::cout : output_stream);
594 
595  if(!out)
596  {
597  log.error() << "Failed to open output file '" << outfile << "'"
598  << messaget::eom;
600  }
601 
602  // Build analyzer
603  log.status() << "Selecting abstract domain" << messaget::eom;
604  namespacet ns(goto_model.symbol_table); // Must live as long as the domain.
605  std::unique_ptr<ai_baset> analyzer(build_analyzer(goto_model, options, ns));
606 
607  if(analyzer == nullptr)
608  {
609  log.status() << "Task / Interpreter / Domain combination not supported"
610  << messaget::eom;
612  }
613 
614  // Run
615  log.status() << "Computing abstract states" << messaget::eom;
616  (*analyzer)(goto_model);
617 
618  // Perform the task
619  log.status() << "Performing task" << messaget::eom;
620  bool result = true;
621  if(options.get_bool_option("show"))
622  {
623  static_show_domain(goto_model, *analyzer, options, out);
624  return CPROVER_EXIT_SUCCESS;
625  }
626  else if(options.get_bool_option("verify"))
627  {
628  result = static_verifier(
629  goto_model, *analyzer, options, ui_message_handler, out);
630  }
631  else if(options.get_bool_option("simplify"))
632  {
633  result = static_simplifier(
634  goto_model, *analyzer, options, ui_message_handler, out);
635  }
636  else if(options.get_bool_option("unreachable-instructions"))
637  {
639  goto_model, *analyzer, options, out);
640  }
641  else if(options.get_bool_option("unreachable-functions"))
642  {
644  goto_model, *analyzer, options, out);
645  }
646  else if(options.get_bool_option("reachable-functions"))
647  {
649  goto_model, *analyzer, options, out);
650  }
651  else
652  {
653  log.error() << "Unhandled task" << messaget::eom;
655  }
656 
657  return result ? CPROVER_EXIT_VERIFICATION_UNSAFE
659  }
660 
661  // Final defensive error case
662  log.error() << "no analysis option given -- consider reading --help"
663  << messaget::eom;
665 }
666 
668  goto_modelt &goto_model,
669  const optionst &options)
670 {
671  log.status() << "Running GOTO functions transformation passes"
672  << messaget::eom;
673 
674  // remove catch and throw
676 
677  // recalculate numbers, etc.
678  goto_model.goto_functions.update();
679 
680  // remove skips such that trivial GOTOs are deleted
681  remove_skip(goto_model);
682 
683  // label the assertions
684  // This must be done after adding assertions and
685  // before using the argument of the "property" option.
686  // Do not re-label after using the property slicer because
687  // this would cause the property identifiers to change.
688  label_properties(goto_model);
689 
690  return false;
691 }
692 
694  goto_model_functiont &function,
695  const abstract_goto_modelt &model,
696  const optionst &options)
697 {
698  journalling_symbol_tablet &symbol_table = function.get_symbol_table();
699  namespacet ns(symbol_table);
700  goto_functionst::goto_functiont &goto_function = function.get_goto_function();
701 
702  // Removal of RTTI inspection:
704  function.get_function_id(),
705  goto_function,
706  symbol_table,
709  // Java virtual functions -> explicit dispatch tables:
711 
712  auto function_is_stub = [&symbol_table, &model](const irep_idt &id) {
713  return symbol_table.lookup_ref(id).value.is_nil() &&
714  !model.can_produce_function(id);
715  };
716 
717  remove_returns(function, function_is_stub);
718 
719  // add generic checks
720  goto_check(
721  function.get_function_id(), function.get_goto_function(), ns, options);
722 }
723 
725 {
726  static const irep_idt initialize_id = INITIALIZE_FUNCTION;
727 
728  return name != goto_functionst::entry_point() && name != initialize_id;
729 }
730 
732  const irep_idt &function_name,
733  symbol_table_baset &symbol_table,
734  goto_functiont &function,
735  bool body_available)
736 {
737  return false;
738 }
739 
742 {
743  // clang-format off
744  std::cout << '\n' << banner_string("JANALYZER", CBMC_VERSION) << '\n'
745  << align_center_with_border("Copyright (C) 2016-2018") << '\n'
746  << align_center_with_border("Daniel Kroening, Diffblue") << '\n'
747  << align_center_with_border("kroening@kroening.com") << '\n'
748  <<
749  "\n"
750  "Usage: Purpose:\n"
751  "\n"
752  " janalyzer [-?] [-h] [--help] show help\n"
753  " janalyzer\n"
755  " janalyzer\n"
757  " janalyzer\n"
759  " janalyzer\n"
761  "\n"
764  "\n"
765  "Task options:\n"
766  " --show display the abstract domains\n"
767  // NOLINTNEXTLINE(whitespace/line_length)
768  " --verify use the abstract domains to check assertions\n"
769  // NOLINTNEXTLINE(whitespace/line_length)
770  " --simplify file_name use the abstract domains to simplify the program\n"
771  " --unreachable-instructions list dead code\n"
772  // NOLINTNEXTLINE(whitespace/line_length)
773  " --unreachable-functions list functions unreachable from the entry point\n"
774  // NOLINTNEXTLINE(whitespace/line_length)
775  " --reachable-functions list functions reachable from the entry point\n"
776  "\n"
777  "Abstract interpreter options:\n"
778  // NOLINTNEXTLINE(whitespace/line_length)
779  " --location-sensitive use location-sensitive abstract interpreter\n"
780  " --concurrent use concurrency-aware abstract interpreter\n"
781  "\n"
782  "Domain options:\n"
783  " --constants constant domain\n"
784  " --intervals interval domain\n"
785  " --non-null non-null domain\n"
786  " --dependence-graph data and control dependencies between instructions\n" // NOLINT(*)
787  "\n"
788  "Output options:\n"
789  " --text file_name output results in plain text to given file\n"
790  // NOLINTNEXTLINE(whitespace/line_length)
791  " --json file_name output results in JSON format to given file\n"
792  " --xml file_name output results in XML format to given file\n"
793  " --dot file_name output results in DOT format to given file\n"
794  "\n"
795  "Specific analyses:\n"
796  // NOLINTNEXTLINE(whitespace/line_length)
797  " --taint file_name perform taint analysis using rules in given file\n"
798  "\n"
799  "Java Bytecode frontend options:\n"
801  "\n"
802  "Program representations:\n"
803  " --show-parse-tree show parse tree\n"
804  " --show-symbol-table show loaded symbol table\n"
807  "\n"
808  "Program instrumentation options:\n"
810  "\n"
811  "Other options:\n"
812  " --version show version and exit\n"
814  "\n";
815  // clang-format on
816 }
cmdlinet::args
argst args
Definition: cmdline.h:91
abstract_goto_modelt::can_produce_function
virtual bool can_produce_function(const irep_idt &id) const =0
Determines if this model can produce a body for the given function.
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
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:469
lazy_goto_modelt::symbol_table
symbol_tablet & symbol_table
Reference to symbol_table in the internal goto_model.
Definition: lazy_goto_model.h:265
languaget::show_parse
virtual void show_parse(std::ostream &out)=0
symbol_table_baset::lookup_ref
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Definition: symbol_table_base.h:104
configt::javat::main_class
irep_idt main_class
Definition: config.h:168
parse_options_baset::ui_message_handler
ui_message_handlert ui_message_handler
Definition: parse_options.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:20
janalyzer_parse_optionst::class_hierarchy
std::unique_ptr< class_hierarchyt > class_hierarchy
Definition: janalyzer_parse_options.h:180
java_bytecode_language.h
JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP
#define JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP
Definition: java_bytecode_language.h:55
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:56
cmdlinet::isset
virtual bool isset(char option) const
Definition: cmdline.cpp:29
dependence_grapht
Definition: dependence_graph.h:217
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:198
goto_inline.h
Function Inlining.
optionst
Definition: options.h:23
static_simplifier.h
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
static_verifier
void static_verifier(const abstract_goto_modelt &abstract_goto_model, const ai_baset &ai, propertiest &properties)
Use the information from the abstract interpreter to fill out the statuses of the passed properties.
Definition: static_verifier.cpp:30
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
optionst::get_option
const std::string get_option(const std::string &option) const
Definition: options.cpp:67
messaget::M_STATISTICS
@ M_STATISTICS
Definition: message.h:171
messaget::status
mstreamt & status() const
Definition: message.h:414
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:47
HELP_FUNCTIONS
#define HELP_FUNCTIONS
Definition: rebuild_goto_start_function.h:27
static_verifier.h
lazy_goto_modelt::process_whole_model_and_freeze
static std::unique_ptr< goto_modelt > process_whole_model_and_freeze(lazy_goto_modelt &&model)
The model returned here has access to the functions we've already loaded but is frozen in the sense t...
Definition: lazy_goto_model.h:203
janalyzer_parse_optionst::register_languages
void register_languages()
Definition: janalyzer_parse_options.cpp:72
remove_skip
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:85
replace
void replace(const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)
Definition: string_constraint.cpp:67
new_java_bytecode_language
std::unique_ptr< languaget > new_java_bytecode_language()
Definition: java_bytecode_language.cpp:1522
get_language_from_mode
std::unique_ptr< languaget > get_language_from_mode(const irep_idt &mode)
Get the language corresponding to the given mode.
Definition: mode.cpp:50
taint_analysis.h
Taint Analysis.
remove_virtual_functions.h
Functions for replacing virtual function call with a static function calls in functions,...
constant_propagator.h
Constant propagation.
remove_virtual_functions
void remove_virtual_functions(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:723
ait
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition: ai.h:558
goto_modelt
Definition: goto_model.h:26
mode.h
options.h
Options.
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
goto_check
void goto_check(const irep_idt &function_identifier, goto_functionst::goto_functiont &goto_function, const namespacet &ns, const optionst &options)
Definition: goto_check.cpp:2231
optionst::set_option
void set_option(const std::string &option, const bool value)
Definition: options.cpp:28
HELP_JAVA_GOTO_BINARY
#define HELP_JAVA_GOTO_BINARY
Definition: java_bytecode_language.h:173
messaget::eom
static eomt eom
Definition: message.h:297
show_symbol_table
void show_symbol_table(const symbol_tablet &symbol_table, ui_message_handlert &ui)
Definition: show_symbol_table.cpp:268
version.h
lazy_goto_model.h
Author: Diffblue Ltd.
local_may_aliast
Definition: local_may_alias.h:26
label_properties
void label_properties(goto_modelt &goto_model)
Definition: set_properties.cpp:43
languaget::set_language_options
virtual void set_language_options(const optionst &)
Set language-specific options.
Definition: language.h:43
HELP_JAVA_JAR
#define HELP_JAVA_JAR
Definition: java_bytecode_language.h:161
remove_instanceof
void remove_instanceof(const irep_idt &function_identifier, 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:299
janalyzer_parse_optionst::help
virtual void help() override
display command line help
Definition: janalyzer_parse_options.cpp:741
parse_options_baset::usage_error
virtual void usage_error()
Definition: parse_options.cpp:47
reachable_functions
void reachable_functions(const goto_modelt &goto_model, const bool json, std::ostream &os)
Definition: unreachable_instructions.cpp:387
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
remove_complex.h
Remove the 'complex' data type by compilation into structs.
janalyzer_parse_optionst::janalyzer_parse_optionst
janalyzer_parse_optionst(int argc, const char **argv)
Definition: janalyzer_parse_options.cpp:63
set_properties.h
Set the properties to check.
lazy_goto_modelt::from_handler_object
static lazy_goto_modelt from_handler_object(THandler &handler, const optionst &options, message_handlert &message_handler)
Create a lazy_goto_modelt from a object that defines function/module pass handlers.
Definition: lazy_goto_model.h:153
janalyzer_parse_optionst::perform_analysis
virtual int perform_analysis(goto_modelt &goto_model, const optionst &options)
Depending on the command line mode, run one of the analysis tasks.
Definition: janalyzer_parse_options.cpp:454
CBMC_VERSION
const char * CBMC_VERSION
janalyzer_parse_optionst::doit
virtual int doit() override
invoke main modules
Definition: janalyzer_parse_options.cpp:339
unreachable_functions
void unreachable_functions(const goto_modelt &goto_model, const bool json, std::ostream &os)
Definition: unreachable_instructions.cpp:373
messaget::error
mstreamt & error() const
Definition: message.h:399
banner_string
std::string banner_string(const std::string &front_end, const std::string &version)
Definition: parse_options.cpp:163
local_may_alias.h
Field-insensitive, location-sensitive may-alias analysis.
lazy_goto_modelt
A GOTO model that produces function bodies on demand.
Definition: lazy_goto_model.h:43
remove_exceptions
void remove_exceptions(symbol_table_baset &symbol_table, goto_functionst &goto_functions, const class_hierarchyt &class_hierarchy, message_handlert &message_handler)
removes throws/CATCH-POP/CATCH-PUSH
Definition: remove_exceptions.cpp:697
symbol_table_baset
The symbol table base class interface.
Definition: symbol_table_base.h:22
show_properties.h
Show the properties.
is_threaded.h
Over-approximate Concurrency for Threaded Goto Programs.
INITIALIZE_FUNCTION
#define INITIALIZE_FUNCTION
Definition: static_lifetime_init.h:23
cmdlinet::get_value
std::string get_value(char option) const
Definition: cmdline.cpp:47
show_symbol_table.h
Show the symbol table.
language.h
Abstract interface to support a programming language.
messaget::set_message_handler
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:179
unreachable_instructions.h
List all unreachable instructions.
HELP_SHOW_PROPERTIES
#define HELP_SHOW_PROPERTIES
Definition: show_properties.h:29
HELP_JAVA_CLASS_NAME
#define HELP_JAVA_CLASS_NAME
Definition: java_bytecode_language.h:151
configt::this_operating_system
static irep_idt this_operating_system()
Definition: config.cpp:1402
java_bytecode_languaget::parse
virtual bool parse()
We set the main class (i.e. class to start the class loading analysis, see java_class_loadert) when w...
Definition: java_bytecode_language.cpp:367
show_goto_functions
void show_goto_functions(const namespacet &ns, ui_message_handlert &ui_message_handler, const goto_functionst &goto_functions, bool list_only)
Definition: show_goto_functions.cpp:26
irept::is_nil
bool is_nil() const
Definition: irep.h:398
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_functiont
A goto function, consisting of function type (see type), function body (see body),...
Definition: goto_function.h:28
lazy_goto_modelt::initialize
void initialize(const std::vector< std::string > &files, const optionst &options)
Performs initial symbol table and language_filest initialization from a given commandline and parsed ...
Definition: lazy_goto_model.cpp:111
goto_check.h
Program Transformation.
janalyzer_parse_optionst::process_goto_function
void process_goto_function(goto_model_functiont &function, const abstract_goto_modelt &model, const optionst &options)
Definition: janalyzer_parse_options.cpp:693
janalyzer_parse_optionst::process_goto_functions
bool process_goto_functions(goto_modelt &goto_model, const optionst &options)
Definition: janalyzer_parse_options.cpp:667
read_goto_binary.h
Read Goto Programs.
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
janalyzer_parse_options.h
JANALYZER Command Line Option Processing.
unreachable_instructions
static void unreachable_instructions(const goto_programt &goto_program, dead_mapt &dest)
Definition: unreachable_instructions.cpp:28
HELP_JAVA_METHOD_NAME
#define HELP_JAVA_METHOD_NAME
Definition: java_bytecode_language.h:146
remove_vector.h
Remove the 'vector' data type by compilation into arrays.
remove_returns.h
Replace function returns by assignments to global variables.
remove_exceptions.h
Remove function exceptional returns.
config
configt config
Definition: config.cpp:24
remove_instanceof.h
Remove Instance-of Operators.
goto_functionst::goto_functiont
::goto_functiont goto_functiont
Definition: goto_functions.h:25
parse_options_baset::log
messaget log
Definition: parse_options.h:43
configt::this_architecture
static irep_idt this_architecture()
Definition: config.cpp:1302
symbolt::value
exprt value
Initial value of symbol.
Definition: symbol.h:34
interval_domain.h
Interval Domain.
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
void get_command_line_options(optionst &options)
Definition: janalyzer_parse_options.cpp:79
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
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:435
ansi_c_language.h
HELP_GOTO_CHECK
#define HELP_GOTO_CHECK
Definition: goto_check.h:45
configt::set
bool set(const cmdlinet &cmdline)
Definition: config.cpp:798
HELP_JAVA_CLASSPATH
#define HELP_JAVA_CLASSPATH
Definition: java_bytecode_language.h:136
exit_codes.h
Document and give macros for the exit codes of CPROVER binaries.
optionst::get_bool_option
bool get_bool_option(const std::string &option) const
Definition: options.cpp:44
taint_analysis
bool taint_analysis(goto_modelt &goto_model, const std::string &taint_file_name, message_handlert &message_handler, bool show_full, const optionalt< std::string > &json_file_name)
Definition: taint_analysis.cpp:416
constant_propagator_ait
Definition: constant_propagator.h:171
concurrency_aware_ait
Base class for concurrency-aware abstract interpretation.
Definition: ai.h:642
remove_returns
void remove_returns(symbol_table_baset &symbol_table, goto_functionst &goto_functions)
removes returns
Definition: remove_returns.cpp:256
ai_baset
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:119
new_ansi_c_language
std::unique_ptr< languaget > new_ansi_c_language()
Definition: ansi_c_language.cpp:143
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
janalyzer_parse_optionst::generate_function_body
bool generate_function_body(const irep_idt &function_name, symbol_table_baset &symbol_table, goto_functiont &function, bool body_available)
Definition: janalyzer_parse_options.cpp:731
goto_functionst::update
void update()
Definition: goto_functions.h:81
configt::java
struct configt::javat java
unicode.h
janalyzer_parse_optionst::can_generate_function_body
bool can_generate_function_body(const irep_idt &name)
Definition: janalyzer_parse_options.cpp:724
config.h
forall_goto_functions
#define forall_goto_functions(it, functions)
Definition: goto_functions.h:122
abstract_goto_modelt
Abstract interface to eager or lazy GOTO models.
Definition: abstract_goto_model.h:21
lazy_goto_modelt::load_all_functions
void load_all_functions() const
Eagerly loads all functions from the symbol table.
Definition: lazy_goto_model.cpp:269
goto_functionst::entry_point
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
Definition: goto_functions.h:90
CPROVER_EXIT_INTERNAL_ERROR
#define CPROVER_EXIT_INTERNAL_ERROR
An error has been encountered during processing the requested analysis.
Definition: exit_codes.h:45
goto_convert_functions.h
Goto Programs with Functions.
static_lifetime_init.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:421
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:104
remove_skip.h
Program Transformation.
java_bytecode_languaget
Definition: java_bytecode_language.h:275
JANALYZER_OPTIONS
#define JANALYZER_OPTIONS
Definition: janalyzer_parse_options.h:123
janalyzer_parse_optionst::build_analyzer
ai_baset * build_analyzer(goto_modelt &goto_model, 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:279
cmdlinet::get_values
const std::list< std::string > & get_values(const std::string &option) const
Definition: cmdline.cpp:108
remove_function_pointers.h
Remove Indirect Function Calls.
parse_options_baset::cmdline
cmdlinet cmdline
Definition: parse_options.h:28
set_properties
void set_properties(goto_programt &goto_program, std::unordered_set< irep_idt > &property_set)
Definition: set_properties.cpp:19
journalling_symbol_tablet
A symbol table wrapper that records which entries have been updated/removedA caller can pass a journa...
Definition: journalling_symbol_table.h:36
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
align_center_with_border
std::string align_center_with_border(const std::string &text)
Utility for displaying help centered messages borderered by "* *".
Definition: parse_options.cpp:150
journalling_symbol_tablet::get_symbol_table
virtual const symbol_tablet & get_symbol_table() const override
Definition: journalling_symbol_table.h:75
goto_model_functiont
Interface providing access to a single function in a GOTO model, plus its associated symbol table.
Definition: goto_model.h:183
static_show_domain.h
dependence_graph.h
Field-Sensitive Program Dependence Analysis, Litvak et al., FSE 2010.
HELP_TIMESTAMP
#define HELP_TIMESTAMP
Definition: timestamper.h:14
CPROVER_EXIT_PARSE_ERROR
#define CPROVER_EXIT_PARSE_ERROR
An error during parsing of the input program.
Definition: exit_codes.h:37