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