cprover
janalyzer_parse_options.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: JANALYZER Command Line Option Processing
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
13
14#include <cstdlib> // exit()
15#include <fstream>
16#include <iostream>
17#include <memory>
18
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 {
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';
337 }
338
339 //
340 // command line options
341 //
342
343 optionst 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);
388 language->set_message_handler(ui_message_handler);
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);
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 {
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"));
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);
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
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
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
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
559 }
560
561 label_properties(goto_model);
562
563 if(cmdline.isset("show-properties"))
564 {
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);
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
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
708 function.get_function_id(),
709 function.get_goto_function(),
710 ns,
711 options,
713}
714
716{
717 static const irep_idt initialize_id = INITIALIZE_FUNCTION;
718
719 return name != goto_functionst::entry_point() && name != initialize_id;
720}
721
723 const irep_idt &function_name,
724 symbol_table_baset &symbol_table,
725 goto_functiont &function,
726 bool body_available)
727{
728 return false;
729}
730
733{
734 // clang-format off
735 std::cout << '\n' << banner_string("JANALYZER", CBMC_VERSION) << '\n'
736 << align_center_with_border("Copyright (C) 2016-2018") << '\n'
737 << align_center_with_border("Daniel Kroening, Diffblue") << '\n'
738 << align_center_with_border("kroening@kroening.com") << '\n'
739 <<
740 "\n"
741 "Usage: Purpose:\n"
742 "\n"
743 " janalyzer [-?] [-h] [--help] show help\n"
744 " janalyzer\n"
746 " janalyzer\n"
748 " janalyzer\n"
750 " janalyzer\n"
752 "\n"
755 "\n"
756 "Task options:\n"
757 " --show display the abstract domains\n"
758 // NOLINTNEXTLINE(whitespace/line_length)
759 " --verify use the abstract domains to check assertions\n"
760 // NOLINTNEXTLINE(whitespace/line_length)
761 " --simplify file_name use the abstract domains to simplify the program\n"
762 " --unreachable-instructions list dead code\n"
763 // NOLINTNEXTLINE(whitespace/line_length)
764 " --unreachable-functions list functions unreachable from the entry point\n"
765 // NOLINTNEXTLINE(whitespace/line_length)
766 " --reachable-functions list functions reachable from the entry point\n"
767 "\n"
768 "Abstract interpreter options:\n"
769 // NOLINTNEXTLINE(whitespace/line_length)
770 " --location-sensitive use location-sensitive abstract interpreter\n"
771 " --concurrent use concurrency-aware abstract interpreter\n"
772 "\n"
773 "Domain options:\n"
774 " --constants constant domain\n"
775 " --intervals interval domain\n"
776 " --non-null non-null domain\n"
777 " --dependence-graph data and control dependencies between instructions\n" // NOLINT(*)
778 "\n"
779 "Output options:\n"
780 " --text file_name output results in plain text to given file\n"
781 // NOLINTNEXTLINE(whitespace/line_length)
782 " --json file_name output results in JSON format to given file\n"
783 " --xml file_name output results in XML format to given file\n"
784 " --dot file_name output results in DOT format to given file\n"
785 "\n"
786 "Specific analyses:\n"
787 // NOLINTNEXTLINE(whitespace/line_length)
788 " --taint file_name perform taint analysis using rules in given file\n"
789 "\n"
790 "Java Bytecode frontend options:\n"
792 "\n"
793 "Program representations:\n"
794 " --show-parse-tree show parse tree\n"
795 " --show-symbol-table show loaded symbol table\n"
798 "\n"
799 "Program instrumentation options:\n"
801 "\n"
802 "Other options:\n"
803 " --version show version and exit\n"
805 "\n";
806 // clang-format on
807}
std::unique_ptr< languaget > new_ansi_c_language()
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:119
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition: ai.h:564
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:145
const std::list< std::string > & get_values(const std::string &option) const
Definition: cmdline.cpp:109
Base class for concurrency-aware abstract interpretation.
Definition: ai.h:653
bool set(const cmdlinet &cmdline)
Definition: config.cpp:798
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:37
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:183
const irep_idt & get_function_id()
Get function id.
Definition: goto_model.h:232
goto_functionst::goto_functiont & get_goto_function()
Get GOTO function.
Definition: goto_model.h:225
journalling_symbol_tablet & get_symbol_table()
Get symbol table.
Definition: goto_model.h:218
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
bool is_nil() const
Definition: irep.h:376
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)
virtual bool parse()
We set the main class (i.e. class to start the class loading analysis, see java_class_loadert) when w...
A symbol table wrapper that records which entries have been updated/removedA caller can pass a journa...
A GOTO model that produces function bodies on demand.
void load_all_functions() const
Eagerly loads all functions from the symbol table.
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...
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.
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:399
@ M_STATISTICS
Definition: message.h:171
static eomt eom
Definition: message.h:297
mstreamt & status() const
Definition: message.h:414
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
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
configt config
Definition: config.cpp:25
Constant propagation.
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
void goto_check(const irep_idt &function_identifier, goto_functionst::goto_functiont &goto_function, const namespacet &ns, const optionst &options, message_handlert &message_handler)
Definition: goto_check.cpp:18
Checks for Errors in C and Java Programs.
#define HELP_GOTO_CHECK_JAVA
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.
Author: Diffblue Ltd.
Field-insensitive, location-sensitive may-alias analysis.
std::unique_ptr< languaget > get_language_from_mode(const irep_idt &mode)
Get the language corresponding to the given mode.
Definition: mode.cpp:51
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
STL namespace.
nonstd::optional< T > optionalt
Definition: optional.h:35
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)
#define HELP_FUNCTIONS
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:88
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.
void show_goto_functions(const namespacet &ns, ui_message_handlert &ui_message_handler, const goto_functionst &goto_functions, bool list_only)
#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_tablet &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 replace(const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)
irep_idt main_class
Definition: config.h:313
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)
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