CBMC
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 <util/config.h>
15 #include <util/exit_codes.h>
16 #include <util/options.h>
17 #include <util/version.h>
18 
26 
31 #include <ansi-c/ansi_c_language.h>
41 #include <langapi/language.h>
42 #include <langapi/mode.h>
44 
45 #include <cstdlib> // exit()
46 #include <fstream>
47 #include <iostream>
48 #include <memory>
49 
53  argc,
54  argv,
55  std::string("JANALYZER ") + CBMC_VERSION)
56 {
57 }
58 
60 {
61  // Need ansi C language for __CPROVER_rounding_mode
64 }
65 
67 {
68  if(config.set(cmdline))
69  {
70  usage_error();
72  }
73 
74  if(cmdline.isset("function"))
75  options.set_option("function", cmdline.get_value("function"));
76 
78 
79  // check assertions
80  if(cmdline.isset("no-assertions"))
81  options.set_option("assertions", false);
82  else
83  options.set_option("assertions", true);
84 
85  // use assumptions
86  if(cmdline.isset("no-assumptions"))
87  options.set_option("assumptions", false);
88  else
89  options.set_option("assumptions", true);
90 
91  // Select a specific analysis
92  if(cmdline.isset("taint"))
93  {
94  options.set_option("taint", true);
95  options.set_option("specific-analysis", true);
96  }
97  // For backwards compatibility,
98  // these are first recognised as specific analyses
99  bool reachability_task = false;
100  if(cmdline.isset("unreachable-instructions"))
101  {
102  options.set_option("unreachable-instructions", true);
103  options.set_option("specific-analysis", true);
104  reachability_task = true;
105  }
106  if(cmdline.isset("unreachable-functions"))
107  {
108  options.set_option("unreachable-functions", true);
109  options.set_option("specific-analysis", true);
110  reachability_task = true;
111  }
112  if(cmdline.isset("reachable-functions"))
113  {
114  options.set_option("reachable-functions", true);
115  options.set_option("specific-analysis", true);
116  reachability_task = true;
117  }
118  if(cmdline.isset("show-local-may-alias"))
119  {
120  options.set_option("show-local-may-alias", true);
121  options.set_option("specific-analysis", true);
122  }
123 
124  // Output format choice
125  if(cmdline.isset("text"))
126  {
127  options.set_option("text", true);
128  options.set_option("outfile", cmdline.get_value("text"));
129  }
130  else if(cmdline.isset("json"))
131  {
132  options.set_option("json", true);
133  options.set_option("outfile", cmdline.get_value("json"));
134  }
135  else if(cmdline.isset("xml"))
136  {
137  options.set_option("xml", true);
138  options.set_option("outfile", cmdline.get_value("xml"));
139  }
140  else if(cmdline.isset("dot"))
141  {
142  options.set_option("dot", true);
143  options.set_option("outfile", cmdline.get_value("dot"));
144  }
145  else
146  {
147  options.set_option("text", true);
148  options.set_option("outfile", "-");
149  }
150 
151  // The use should either select:
152  // 1. a specific analysis, or
153  // 2. a triple of task / analyzer / domain, or
154  // 3. one of the general display options
155 
156  // Task options
157  if(cmdline.isset("show"))
158  {
159  options.set_option("show", true);
160  options.set_option("general-analysis", true);
161  }
162  else if(cmdline.isset("verify"))
163  {
164  options.set_option("verify", true);
165  options.set_option("general-analysis", true);
166  }
167  else if(cmdline.isset("simplify"))
168  {
169  options.set_option("simplify", true);
170  options.set_option("outfile", cmdline.get_value("simplify"));
171  options.set_option("general-analysis", true);
172 
173  // For development allow slicing to be disabled in the simplify task
174  options.set_option(
175  "simplify-slicing", !(cmdline.isset("no-simplify-slicing")));
176  }
177  else if(cmdline.isset("show-intervals"))
178  {
179  // For backwards compatibility
180  options.set_option("show", true);
181  options.set_option("general-analysis", true);
182  options.set_option("intervals", true);
183  options.set_option("domain set", true);
184  }
185  else if(cmdline.isset("(show-non-null)"))
186  {
187  // For backwards compatibility
188  options.set_option("show", true);
189  options.set_option("general-analysis", true);
190  options.set_option("non-null", true);
191  options.set_option("domain set", true);
192  }
193  else if(cmdline.isset("intervals") || cmdline.isset("non-null"))
194  {
195  // For backwards compatibility either of these on their own means show
196  options.set_option("show", true);
197  options.set_option("general-analysis", true);
198  }
199 
200  if(options.get_bool_option("general-analysis") || reachability_task)
201  {
202  // Abstract interpreter choice
203  if(cmdline.isset("location-sensitive"))
204  options.set_option("location-sensitive", true);
205  else if(cmdline.isset("concurrent"))
206  options.set_option("concurrent", true);
207  else
208  {
209  // Silently default to location-sensitive as it's the "default"
210  // view of abstract interpretation.
211  options.set_option("location-sensitive", true);
212  }
213 
214  // Domain choice
215  if(cmdline.isset("constants"))
216  {
217  options.set_option("constants", true);
218  options.set_option("domain set", true);
219  }
220  else if(cmdline.isset("dependence-graph"))
221  {
222  options.set_option("dependence-graph", true);
223  options.set_option("domain set", true);
224  }
225  else if(cmdline.isset("intervals"))
226  {
227  options.set_option("intervals", true);
228  options.set_option("domain set", true);
229  }
230  else if(cmdline.isset("non-null"))
231  {
232  options.set_option("non-null", true);
233  options.set_option("domain set", true);
234  }
235 
236  // Reachability questions, when given with a domain swap from specific
237  // to general tasks so that they can use the domain & parameterisations.
238  if(reachability_task)
239  {
240  if(options.get_bool_option("domain set"))
241  {
242  options.set_option("specific-analysis", false);
243  options.set_option("general-analysis", true);
244  }
245  }
246  else
247  {
248  if(!options.get_bool_option("domain set"))
249  {
250  // Default to constants as it is light-weight but useful
251  log.status() << "Domain not specified, defaulting to --constants"
252  << messaget::eom;
253  options.set_option("constants", true);
254  }
255  }
256  }
257 }
258 
263  goto_modelt &goto_model,
264  const optionst &options,
265  const namespacet &ns)
266 {
267  ai_baset *domain = nullptr;
268 
269  if(options.get_bool_option("location-sensitive"))
270  {
271  if(options.get_bool_option("constants"))
272  {
273  // constant_propagator_ait derives from ait<constant_propagator_domaint>
274  domain = new constant_propagator_ait(goto_model.goto_functions);
275  }
276  else if(options.get_bool_option("dependence-graph"))
277  {
278  domain = new dependence_grapht(ns);
279  }
280  else if(options.get_bool_option("intervals"))
281  {
282  domain = new ait<interval_domaint>();
283  }
284 #if 0
285  // Not actually implemented, despite the option...
286  else if(options.get_bool_option("non-null"))
287  {
288  domain=new ait<non_null_domaint>();
289  }
290 #endif
291  }
292  else if(options.get_bool_option("concurrent"))
293  {
294 #if 0
295  // Disabled until merge_shared is implemented for these
296  if(options.get_bool_option("constants"))
297  {
299  }
300  else if(options.get_bool_option("dependence-graph"))
301  {
302  domain=new dependence_grapht(ns);
303  }
304  else if(options.get_bool_option("intervals"))
305  {
307  }
308 #if 0
309  // Not actually implemented, despite the option...
310  else if(options.get_bool_option("non-null"))
311  {
313  }
314 #endif
315 #endif
316  }
317 
318  return domain;
319 }
320 
323 {
324  if(cmdline.isset("version"))
325  {
326  std::cout << CBMC_VERSION << '\n';
327  return CPROVER_EXIT_SUCCESS;
328  }
329 
330  //
331  // command line options
332  //
333 
334  optionst options;
335  get_command_line_options(options);
338 
339  log_version_and_architecture("JANALYZER");
340 
342 
343  if(!((cmdline.isset("jar") && cmdline.args.empty()) ||
344  (cmdline.isset("gb") && cmdline.args.empty()) ||
345  (!cmdline.isset("jar") && !cmdline.isset("gb") &&
346  (cmdline.args.size() == 1))))
347  {
348  log.error() << "Please give exactly one class name, "
349  << "and/or use -jar jarfile or --gb goto-binary"
350  << messaget::eom;
352  }
353 
354  if((cmdline.args.size() == 1) && !cmdline.isset("show-parse-tree"))
355  {
356  std::string main_class = cmdline.args[0];
357  // `java` accepts slashes and dots as package separators
358  std::replace(main_class.begin(), main_class.end(), '/', '.');
359  config.java.main_class = main_class;
360  cmdline.args.pop_back();
361  }
362 
363  if(cmdline.isset("jar"))
364  {
365  cmdline.args.push_back(cmdline.get_value("jar"));
366  }
367 
368  if(cmdline.isset("gb"))
369  {
370  cmdline.args.push_back(cmdline.get_value("gb"));
371  }
372 
373  // Shows the parse tree of the main class
374  if(cmdline.isset("show-parse-tree"))
375  {
376  std::unique_ptr<languaget> language = get_language_from_mode(ID_java);
377  CHECK_RETURN(language != nullptr);
378  language->set_language_options(options);
380 
381  log.status() << "Parsing ..." << messaget::eom;
382 
383  if(static_cast<java_bytecode_languaget *>(language.get())->parse())
384  {
385  log.error() << "PARSING ERROR" << messaget::eom;
387  }
388 
389  language->show_parse(std::cout);
390  return CPROVER_EXIT_SUCCESS;
391  }
392 
393  lazy_goto_modelt lazy_goto_model =
395  lazy_goto_model.initialize(cmdline.args, options);
396 
398  util_make_unique<class_hierarchyt>(lazy_goto_model.symbol_table);
399 
400  log.status() << "Generating GOTO Program" << messaget::eom;
401  lazy_goto_model.load_all_functions();
402 
403  std::unique_ptr<abstract_goto_modelt> goto_model_ptr =
405  std::move(lazy_goto_model));
406  if(goto_model_ptr == nullptr)
408 
409  goto_modelt &goto_model = dynamic_cast<goto_modelt &>(*goto_model_ptr);
410 
411  // show it?
412  if(cmdline.isset("show-symbol-table"))
413  {
415  return CPROVER_EXIT_SUCCESS;
416  }
417 
418  // show it?
419  if(
420  cmdline.isset("show-goto-functions") ||
421  cmdline.isset("list-goto-functions"))
422  {
424  goto_model, ui_message_handler, cmdline.isset("list-goto-functions"));
425  return CPROVER_EXIT_SUCCESS;
426  }
427 
428  return perform_analysis(goto_model, options);
429 }
430 
433  goto_modelt &goto_model,
434  const optionst &options)
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, ui_message_handler, true);
443  return CPROVER_EXIT_SUCCESS;
444  }
445  else
446  {
447  optionalt<std::string> json_file;
448  if(cmdline.isset("json"))
449  json_file = cmdline.get_value("json");
450  bool result = taint_analysis(
451  goto_model, taint_file, ui_message_handler, false, json_file);
453  }
454  }
455 
456  // If no domain is given, this lightweight version of the analysis is used.
457  if(
458  options.get_bool_option("unreachable-instructions") &&
459  options.get_bool_option("specific-analysis"))
460  {
461  const std::string json_file = cmdline.get_value("json");
462 
463  if(json_file.empty())
464  unreachable_instructions(goto_model, false, std::cout);
465  else if(json_file == "-")
466  unreachable_instructions(goto_model, true, std::cout);
467  else
468  {
469  std::ofstream ofs(json_file);
470  if(!ofs)
471  {
472  log.error() << "Failed to open json output '" << json_file << "'"
473  << messaget::eom;
475  }
476 
477  unreachable_instructions(goto_model, true, ofs);
478  }
479 
480  return CPROVER_EXIT_SUCCESS;
481  }
482 
483  if(
484  options.get_bool_option("unreachable-functions") &&
485  options.get_bool_option("specific-analysis"))
486  {
487  const std::string json_file = cmdline.get_value("json");
488 
489  if(json_file.empty())
490  unreachable_functions(goto_model, false, std::cout);
491  else if(json_file == "-")
492  unreachable_functions(goto_model, true, std::cout);
493  else
494  {
495  std::ofstream ofs(json_file);
496  if(!ofs)
497  {
498  log.error() << "Failed to open json output '" << json_file << "'"
499  << messaget::eom;
501  }
502 
503  unreachable_functions(goto_model, true, ofs);
504  }
505 
506  return CPROVER_EXIT_SUCCESS;
507  }
508 
509  if(
510  options.get_bool_option("reachable-functions") &&
511  options.get_bool_option("specific-analysis"))
512  {
513  const std::string json_file = cmdline.get_value("json");
514 
515  if(json_file.empty())
516  reachable_functions(goto_model, false, std::cout);
517  else if(json_file == "-")
518  reachable_functions(goto_model, true, std::cout);
519  else
520  {
521  std::ofstream ofs(json_file);
522  if(!ofs)
523  {
524  log.error() << "Failed to open json output '" << json_file << "'"
525  << messaget::eom;
527  }
528 
529  reachable_functions(goto_model, true, ofs);
530  }
531 
532  return CPROVER_EXIT_SUCCESS;
533  }
534 
535  if(options.get_bool_option("show-local-may-alias"))
536  {
537  namespacet ns(goto_model.symbol_table);
538 
539  for(const auto &gf_entry : goto_model.goto_functions.function_map)
540  {
541  std::cout << ">>>>\n";
542  std::cout << ">>>> " << gf_entry.first << '\n';
543  std::cout << ">>>>\n";
544  local_may_aliast local_may_alias(gf_entry.second);
545  local_may_alias.output(std::cout, gf_entry.second, ns);
546  std::cout << '\n';
547  }
548 
549  return CPROVER_EXIT_SUCCESS;
550  }
551 
552  label_properties(goto_model);
553 
554  if(cmdline.isset("show-properties"))
555  {
556  show_properties(goto_model, ui_message_handler);
557  return CPROVER_EXIT_SUCCESS;
558  }
559 
560  if(cmdline.isset("property"))
561  ::set_properties(goto_model, cmdline.get_values("property"));
562 
563  if(options.get_bool_option("general-analysis"))
564  {
565  // Output file factory
566  const std::string outfile = options.get_option("outfile");
567  std::ofstream output_stream;
568  if(!(outfile == "-"))
569  output_stream.open(outfile);
570 
571  std::ostream &out((outfile == "-") ? std::cout : output_stream);
572 
573  if(!out)
574  {
575  log.error() << "Failed to open output file '" << outfile << "'"
576  << messaget::eom;
578  }
579 
580  // Build analyzer
581  log.status() << "Selecting abstract domain" << messaget::eom;
582  namespacet ns(goto_model.symbol_table); // Must live as long as the domain.
583  std::unique_ptr<ai_baset> analyzer(build_analyzer(goto_model, options, ns));
584 
585  if(analyzer == nullptr)
586  {
587  log.status() << "Task / Interpreter / Domain combination not supported"
588  << messaget::eom;
590  }
591 
592  // Run
593  log.status() << "Computing abstract states" << messaget::eom;
594  (*analyzer)(goto_model);
595 
596  // Perform the task
597  log.status() << "Performing task" << messaget::eom;
598  bool result = true;
599  if(options.get_bool_option("show"))
600  {
601  static_show_domain(goto_model, *analyzer, options, out);
602  return CPROVER_EXIT_SUCCESS;
603  }
604  else if(options.get_bool_option("verify"))
605  {
606  result = static_verifier(
607  goto_model, *analyzer, options, ui_message_handler, out);
608  }
609  else if(options.get_bool_option("simplify"))
610  {
611  result = static_simplifier(
612  goto_model, *analyzer, options, ui_message_handler, out);
613  }
614  else if(options.get_bool_option("unreachable-instructions"))
615  {
617  goto_model, *analyzer, options, out);
618  }
619  else if(options.get_bool_option("unreachable-functions"))
620  {
622  goto_model, *analyzer, options, out);
623  }
624  else if(options.get_bool_option("reachable-functions"))
625  {
627  goto_model, *analyzer, options, out);
628  }
629  else
630  {
631  log.error() << "Unhandled task" << messaget::eom;
633  }
634 
635  return result ? CPROVER_EXIT_VERIFICATION_UNSAFE
637  }
638 
639  // Final defensive error case
640  log.error() << "no analysis option given -- consider reading --help"
641  << messaget::eom;
643 }
644 
646  goto_modelt &goto_model,
647  const optionst &options)
648 {
649  log.status() << "Running GOTO functions transformation passes"
650  << messaget::eom;
651 
652  // remove catch and throw
654 
655  // recalculate numbers, etc.
656  goto_model.goto_functions.update();
657 
658  // remove skips such that trivial GOTOs are deleted
659  remove_skip(goto_model);
660 
661  // label the assertions
662  // This must be done after adding assertions and
663  // before using the argument of the "property" option.
664  // Do not re-label after using the property slicer because
665  // this would cause the property identifiers to change.
666  label_properties(goto_model);
667 
668  return false;
669 }
670 
672  goto_model_functiont &function,
673  const abstract_goto_modelt &model,
674  const optionst &options)
675 {
676  journalling_symbol_tablet &symbol_table = function.get_symbol_table();
677  namespacet ns(symbol_table);
678  goto_functionst::goto_functiont &goto_function = function.get_goto_function();
679 
680  // Removal of RTTI inspection:
682  function.get_function_id(),
683  goto_function,
684  symbol_table,
687  // Java virtual functions -> explicit dispatch tables:
689 
690  auto function_is_stub = [&symbol_table, &model](const irep_idt &id) {
691  return symbol_table.lookup_ref(id).value.is_nil() &&
692  !model.can_produce_function(id);
693  };
694 
695  remove_returns(function, function_is_stub);
696 
697  transform_assertions_assumptions(options, function.get_goto_function().body);
698 }
699 
701 {
702  static const irep_idt initialize_id = INITIALIZE_FUNCTION;
703 
704  return name != goto_functionst::entry_point() && name != initialize_id;
705 }
706 
708  const irep_idt &function_name,
709  symbol_table_baset &symbol_table,
710  goto_functiont &function,
711  bool body_available)
712 {
713  return false;
714 }
715 
718 {
719  // clang-format off
720  std::cout << '\n' << banner_string("JANALYZER", CBMC_VERSION) << '\n'
721  << align_center_with_border("Copyright (C) 2016-2018") << '\n'
722  << align_center_with_border("Daniel Kroening, Diffblue") << '\n'
723  << align_center_with_border("kroening@kroening.com") << '\n'
724  <<
725  "\n"
726  "Usage: Purpose:\n"
727  "\n"
728  " janalyzer [-?] [-h] [--help] show help\n"
729  " janalyzer\n"
731  " janalyzer\n"
733  " janalyzer\n"
735  " janalyzer\n"
737  "\n"
740  "\n"
741  "Task options:\n"
742  " --show display the abstract domains\n"
743  // NOLINTNEXTLINE(whitespace/line_length)
744  " --verify use the abstract domains to check assertions\n"
745  // NOLINTNEXTLINE(whitespace/line_length)
746  " --simplify file_name use the abstract domains to simplify the program\n"
747  " --no-simplify-slicing do not remove instructions from which no\n"
748  " property can be reached (use with --simplify)\n" // NOLINT(*)
749  " --unreachable-instructions list dead code\n"
750  // NOLINTNEXTLINE(whitespace/line_length)
751  " --unreachable-functions list functions unreachable from the entry point\n"
752  // NOLINTNEXTLINE(whitespace/line_length)
753  " --reachable-functions list functions reachable from the entry point\n"
754  "\n"
755  "Abstract interpreter options:\n"
756  // NOLINTNEXTLINE(whitespace/line_length)
757  " --location-sensitive use location-sensitive abstract interpreter\n"
758  " --concurrent use concurrency-aware abstract interpreter\n"
759  "\n"
760  "Domain options:\n"
761  " --constants constant domain\n"
762  " --intervals interval domain\n"
763  " --non-null non-null domain\n"
764  " --dependence-graph data and control dependencies between instructions\n" // NOLINT(*)
765  "\n"
766  "Output options:\n"
767  " --text file_name output results in plain text to given file\n"
768  // NOLINTNEXTLINE(whitespace/line_length)
769  " --json file_name output results in JSON format to given file\n"
770  " --xml file_name output results in XML format to given file\n"
771  " --dot file_name output results in DOT format to given file\n"
772  "\n"
773  "Specific analyses:\n"
774  // NOLINTNEXTLINE(whitespace/line_length)
775  " --taint file_name perform taint analysis using rules in given file\n"
776  " --show-taint print taint analysis results on stdout\n"
777  " --show-local-may-alias perform procedure-local may alias analysis\n"
778  "\n"
779  "Java Bytecode frontend options:\n"
781  "\n"
782  "Platform options:\n"
784  "\n"
785  "Program representations:\n"
786  " --show-parse-tree show parse tree\n"
787  " --show-symbol-table show loaded symbol table\n"
790  "\n"
791  "Program instrumentation options:\n"
792  " --no-assertions ignore user assertions\n"
793  " --no-assumptions ignore user assumptions\n"
794  " --property id enable selected properties only\n"
795  "\n"
796  "Other options:\n"
797  " --version show version and exit\n"
798  " --verbosity # verbosity level\n"
800  "\n";
801  // clang-format on
802 }
cmdlinet::args
argst args
Definition: cmdline.h:145
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:36
HELP_SHOW_GOTO_FUNCTIONS
#define HELP_SHOW_GOTO_FUNCTIONS
Definition: show_goto_functions.h:25
local_may_aliast::output
void output(std::ostream &out, const goto_functiont &goto_function, const namespacet &ns) const
Definition: local_may_alias.cpp:465
lazy_goto_modelt::symbol_table
symbol_tablet & symbol_table
Reference to symbol_table in the internal goto_model.
Definition: lazy_goto_model.h:260
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:328
parse_options_baset::ui_message_handler
ui_message_handlert ui_message_handler
Definition: parse_options.h:45
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:19
janalyzer_parse_optionst::class_hierarchy
std::unique_ptr< class_hierarchyt > class_hierarchy
Definition: janalyzer_parse_options.h:176
java_bytecode_language.h
JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP
#define JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP
Definition: java_bytecode_language.h:53
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:55
cmdlinet::isset
virtual bool isset(char option) const
Definition: cmdline.cpp:30
dependence_grapht
Definition: dependence_graph.h:211
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
optionst
Definition: options.h:22
static_simplifier.h
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
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:229
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:44
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:198
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:87
HELP_CONFIG_PLATFORM
#define HELP_CONFIG_PLATFORM
Definition: config.h:84
replace
void replace(const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)
Definition: string_constraint.cpp:70
new_java_bytecode_language
std::unique_ptr< languaget > new_java_bytecode_language()
Definition: java_bytecode_language.cpp:1524
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:51
taint_analysis.h
remove_virtual_functions.h
constant_propagator.h
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:728
ait
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition: ai.h:563
goto_modelt
Definition: goto_model.h:25
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:28
HELP_JAVA_GOTO_BINARY
#define HELP_JAVA_GOTO_BINARY
Definition: java_bytecode_language.h:173
parse_options_baset::log_version_and_architecture
void log_version_and_architecture(const std::string &front_end)
Write version and system architecture to log.status().
Definition: parse_options.cpp:152
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:242
janalyzer_parse_optionst::register_languages
void register_languages() override
Definition: janalyzer_parse_options.cpp:59
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:29
version.h
lazy_goto_model.h
Author: Diffblue Ltd.
local_may_aliast
Definition: local_may_alias.h:25
label_properties
void label_properties(goto_modelt &goto_model)
Definition: set_properties.cpp:45
languaget::set_language_options
virtual void set_language_options(const optionst &)
Set language-specific options.
Definition: language.h:41
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:306
janalyzer_parse_optionst::help
void help() override
display command line help
Definition: janalyzer_parse_options.cpp:717
parse_options_baset::usage_error
virtual void usage_error()
Definition: parse_options.cpp:49
reachable_functions
void reachable_functions(const goto_modelt &goto_model, const bool json, std::ostream &os)
Definition: unreachable_instructions.cpp:403
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:90
janalyzer_parse_optionst::janalyzer_parse_optionst
janalyzer_parse_optionst(int argc, const char **argv)
Definition: janalyzer_parse_options.cpp:50
set_properties.h
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:432
CBMC_VERSION
const char * CBMC_VERSION
janalyzer_parse_optionst::doit
int doit() override
invoke main modules
Definition: janalyzer_parse_options.cpp:322
unreachable_functions
void unreachable_functions(const goto_modelt &goto_model, const bool json, std::ostream &os)
Definition: unreachable_instructions.cpp:389
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:174
local_may_alias.h
lazy_goto_modelt
A GOTO model that produces function bodies on demand.
Definition: lazy_goto_model.h:42
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:691
symbol_table_baset
The symbol table base class interface.
Definition: symbol_table_base.h:21
show_properties.h
INITIALIZE_FUNCTION
#define INITIALIZE_FUNCTION
Definition: static_lifetime_init.h:22
cmdlinet::get_value
std::string get_value(char option) const
Definition: cmdline.cpp:48
show_symbol_table.h
language.h
messaget::set_message_handler
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:179
unreachable_instructions.h
HELP_SHOW_PROPERTIES
#define HELP_SHOW_PROPERTIES
Definition: show_properties.h:30
HELP_JAVA_CLASS_NAME
#define HELP_JAVA_CLASS_NAME
Definition: java_bytecode_language.h:151
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:369
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:20
transform_assertions_assumptions
static void transform_assertions_assumptions(goto_programt &goto_program, bool enable_assertions, bool enable_built_in_assertions, bool enable_assumptions)
Definition: goto_check.cpp:19
irept::is_nil
bool is_nil() const
Definition: irep.h:376
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:21
goto_functiont
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
Definition: goto_function.h:23
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:114
goto_check.h
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:671
janalyzer_parse_optionst::process_goto_functions
bool process_goto_functions(goto_modelt &goto_model, const optionst &options)
Definition: janalyzer_parse_options.cpp:645
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
janalyzer_parse_options.h
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_returns.h
remove_exceptions.h
config
configt config
Definition: config.cpp:25
remove_instanceof.h
goto_functionst::goto_functiont
::goto_functiont goto_functiont
Definition: goto_functions.h:27
parse_options_baset::log
messaget log
Definition: parse_options.h:46
symbolt::value
exprt value
Initial value of symbol.
Definition: symbol.h:34
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:39
janalyzer_parse_optionst::get_command_line_options
void get_command_line_options(optionst &options)
Definition: janalyzer_parse_options.cpp:66
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:451
ansi_c_language.h
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
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:418
constant_propagator_ait
Definition: constant_propagator.h:170
concurrency_aware_ait
Base class for concurrency-aware abstract interpretation.
Definition: ai.h:652
remove_returns
void remove_returns(symbol_table_baset &symbol_table, goto_functionst &goto_functions)
removes returns
Definition: remove_returns.cpp:255
ai_baset
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:118
new_ansi_c_language
std::unique_ptr< languaget > new_ansi_c_language()
Definition: ansi_c_language.cpp:150
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:707
goto_functionst::update
void update()
Definition: goto_functions.h:83
configt::java
struct configt::javat java
janalyzer_parse_optionst::can_generate_function_body
bool can_generate_function_body(const irep_idt &name)
Definition: janalyzer_parse_options.cpp:700
config.h
abstract_goto_modelt
Abstract interface to eager or lazy GOTO models.
Definition: abstract_goto_model.h:20
lazy_goto_modelt::load_all_functions
void load_all_functions() const
Eagerly loads all functions from the symbol table.
Definition: lazy_goto_model.cpp:187
goto_functionst::entry_point
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
Definition: goto_functions.h:92
CPROVER_EXIT_INTERNAL_ERROR
#define CPROVER_EXIT_INTERNAL_ERROR
An error has been encountered during processing the requested analysis.
Definition: exit_codes.h:45
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:437
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:105
remove_skip.h
java_bytecode_languaget
Definition: java_bytecode_language.h:274
JANALYZER_OPTIONS
#define JANALYZER_OPTIONS
Definition: janalyzer_parse_options.h:120
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:262
cmdlinet::get_values
const std::list< std::string > & get_values(const std::string &option) const
Definition: cmdline.cpp:109
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:21
journalling_symbol_tablet
A symbol table wrapper that records which entries have been updated/removed.
Definition: journalling_symbol_table.h:35
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:161
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:182
static_show_domain.h
dependence_graph.h
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