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