cprover
Loading...
Searching...
No Matches
goto_analyzer_parse_options.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Goto-Analyzer Command Line Option Processing
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
13
14#include <util/config.h>
16#include <util/exit_codes.h>
17#include <util/help_formatter.h>
18#include <util/options.h>
19#include <util/version.h>
20
27
28#include <analyses/ai.h>
31#include <ansi-c/gcc_version.h>
33#include <cpp/cprover_library.h>
34
35#include "build_analyzer.h"
36#include "show_on_source.h"
37#include "static_show_domain.h"
38#include "static_simplifier.h"
39#include "static_verifier.h"
40#include "taint_analysis.h"
42
43#include <cstdlib> // exit()
44#include <fstream> // IWYU pragma: keep
45#include <iostream>
46#include <memory>
47
49 int argc,
50 const char **argv)
53 argc,
54 argv,
55 std::string("GOTO-ANALYZER "))
56{
57}
58
60{
61 if(config.set(cmdline))
62 {
65 }
66
67 if(cmdline.isset("function"))
68 options.set_option("function", cmdline.get_value("function"));
69
70 // all checks supported by goto_check
72
73 // The user should either select:
74 // 1. a specific analysis, or
75 // 2. a tuple of task / analyser options / outputs
76
77 // Select a specific analysis
78 if(cmdline.isset("taint"))
79 {
80 options.set_option("taint", true);
81 options.set_option("specific-analysis", true);
82 }
83 // For backwards compatibility,
84 // these are first recognised as specific analyses
85 bool reachability_task = false;
86 if(cmdline.isset("unreachable-instructions"))
87 {
88 options.set_option("unreachable-instructions", true);
89 options.set_option("specific-analysis", true);
90 reachability_task = true;
91 }
92 if(cmdline.isset("unreachable-functions"))
93 {
94 options.set_option("unreachable-functions", true);
95 options.set_option("specific-analysis", true);
96 reachability_task = true;
97 }
98 if(cmdline.isset("reachable-functions"))
99 {
100 options.set_option("reachable-functions", true);
101 options.set_option("specific-analysis", true);
102 reachability_task = true;
103 }
104 if(cmdline.isset("show-local-may-alias"))
105 {
106 options.set_option("show-local-may-alias", true);
107 options.set_option("specific-analysis", true);
108 }
109
110 // Output format choice
111 if(cmdline.isset("text"))
112 {
113 options.set_option("text", true);
114 options.set_option("outfile", cmdline.get_value("text"));
115 }
116 else if(cmdline.isset("json"))
117 {
118 options.set_option("json", true);
119 options.set_option("outfile", cmdline.get_value("json"));
120 }
121 else if(cmdline.isset("xml"))
122 {
123 options.set_option("xml", true);
124 options.set_option("outfile", cmdline.get_value("xml"));
125 }
126 else if(cmdline.isset("dot"))
127 {
128 options.set_option("dot", true);
129 options.set_option("outfile", cmdline.get_value("dot"));
130 }
131
132 // Task options
133 if(cmdline.isset("show"))
134 {
135 options.set_option("show", true);
136 options.set_option("general-analysis", true);
137 }
138 else if(cmdline.isset("show-on-source"))
139 {
140 options.set_option("show-on-source", true);
141 options.set_option("general-analysis", true);
142 }
143 else if(cmdline.isset("verify"))
144 {
145 options.set_option("verify", true);
146 options.set_option("general-analysis", true);
147 }
148 else if(cmdline.isset("simplify"))
149 {
150 if(cmdline.get_value("simplify") == "-")
152 "cannot output goto binary to stdout", "--simplify");
153
154 options.set_option("simplify", true);
155 options.set_option("outfile", cmdline.get_value("simplify"));
156 options.set_option("general-analysis", true);
157
158 // For development allow slicing to be disabled in the simplify task
159 options.set_option(
160 "simplify-slicing",
161 !(cmdline.isset("no-simplify-slicing")));
162 }
163 else if(cmdline.isset("show-intervals"))
164 {
165 // For backwards compatibility
166 options.set_option("show", true);
167 options.set_option("general-analysis", true);
168 options.set_option("intervals", true);
169 options.set_option("domain set", true);
170 }
171 else if(cmdline.isset("show-non-null"))
172 {
173 // For backwards compatibility
174 options.set_option("show", true);
175 options.set_option("general-analysis", true);
176 options.set_option("non-null", true);
177 options.set_option("domain set", true);
178 }
179 else if(cmdline.isset("intervals") || cmdline.isset("non-null"))
180 {
181 // Partial backwards compatability, just giving these domains without
182 // a task will work. However it will use the general default of verify
183 // rather than their historical default of show.
184 options.set_option("verify", true);
185 options.set_option("general-analysis", true);
186 }
187
188 if(options.get_bool_option("general-analysis") || reachability_task)
189 {
190 // Abstract interpreter choice
191 if(cmdline.isset("recursive-interprocedural"))
192 options.set_option("recursive-interprocedural", true);
193 else if(cmdline.isset("three-way-merge"))
194 options.set_option("three-way-merge", true);
195 else if(cmdline.isset("legacy-ait") || cmdline.isset("location-sensitive"))
196 {
197 options.set_option("legacy-ait", true);
198 // Fixes a number of other options as well
199 options.set_option("ahistorical", true);
200 options.set_option("history set", true);
201 options.set_option("one-domain-per-location", true);
202 options.set_option("storage set", true);
203 }
204 else if(cmdline.isset("legacy-concurrent") || cmdline.isset("concurrent"))
205 {
206 options.set_option("legacy-concurrent", true);
207 options.set_option("ahistorical", true);
208 options.set_option("history set", true);
209 options.set_option("one-domain-per-location", true);
210 options.set_option("storage set", true);
211 }
212 else
213 {
214 // Silently default to legacy-ait for backwards compatability
215 options.set_option("legacy-ait", true);
216 // Fixes a number of other options as well
217 options.set_option("ahistorical", true);
218 options.set_option("history set", true);
219 options.set_option("one-domain-per-location", true);
220 options.set_option("storage set", true);
221 }
222
223 // History choice
224 if(cmdline.isset("ahistorical"))
225 {
226 options.set_option("ahistorical", true);
227 options.set_option("history set", true);
228 }
229 else if(cmdline.isset("call-stack"))
230 {
231 options.set_option("call-stack", true);
232 options.set_option(
233 "call-stack-recursion-limit", cmdline.get_value("call-stack"));
234 options.set_option("history set", true);
235 }
236 else if(cmdline.isset("loop-unwind"))
237 {
238 options.set_option("local-control-flow-history", true);
239 options.set_option("local-control-flow-history-forward", false);
240 options.set_option("local-control-flow-history-backward", true);
241 options.set_option(
242 "local-control-flow-history-limit", cmdline.get_value("loop-unwind"));
243 options.set_option("history set", true);
244 }
245 else if(cmdline.isset("branching"))
246 {
247 options.set_option("local-control-flow-history", true);
248 options.set_option("local-control-flow-history-forward", true);
249 options.set_option("local-control-flow-history-backward", false);
250 options.set_option(
251 "local-control-flow-history-limit", cmdline.get_value("branching"));
252 options.set_option("history set", true);
253 }
254 else if(cmdline.isset("loop-unwind-and-branching"))
255 {
256 options.set_option("local-control-flow-history", true);
257 options.set_option("local-control-flow-history-forward", true);
258 options.set_option("local-control-flow-history-backward", true);
259 options.set_option(
260 "local-control-flow-history-limit",
261 cmdline.get_value("loop-unwind-and-branching"));
262 options.set_option("history set", true);
263 }
264
265 if(!options.get_bool_option("history set"))
266 {
267 // Default to ahistorical as it is the expected for of analysis
268 log.status() << "History not specified, defaulting to --ahistorical"
269 << messaget::eom;
270 options.set_option("ahistorical", true);
271 options.set_option("history set", true);
272 }
273
274 // Domain choice
275 if(cmdline.isset("constants"))
276 {
277 options.set_option("constants", true);
278 options.set_option("domain set", true);
279 }
280 else if(cmdline.isset("dependence-graph"))
281 {
282 options.set_option("dependence-graph", true);
283 options.set_option("domain set", true);
284 }
285 else if(cmdline.isset("intervals"))
286 {
287 options.set_option("intervals", true);
288 options.set_option("domain set", true);
289 }
290 else if(cmdline.isset("non-null"))
291 {
292 options.set_option("non-null", true);
293 options.set_option("domain set", true);
294 }
295 else if(cmdline.isset("vsd") || cmdline.isset("variable-sensitivity"))
296 {
297 options.set_option("vsd", true);
298 options.set_option("domain set", true);
299
300 PARSE_OPTIONS_VSD(cmdline, options);
301 }
302 else if(cmdline.isset("dependence-graph-vs"))
303 {
304 options.set_option("dependence-graph-vs", true);
305 options.set_option("domain set", true);
306
307 PARSE_OPTIONS_VSD(cmdline, options);
308 options.set_option("data-dependencies", true); // Always set
309 }
310
311 // Reachability questions, when given with a domain swap from specific
312 // to general tasks so that they can use the domain & parameterisations.
314 {
315 if(options.get_bool_option("domain set"))
316 {
317 options.set_option("specific-analysis", false);
318 options.set_option("general-analysis", true);
319 }
320 }
321 else
322 {
323 if(!options.get_bool_option("domain set"))
324 {
325 // Default to constants as it is light-weight but useful
326 log.status() << "Domain not specified, defaulting to --constants"
327 << messaget::eom;
328 options.set_option("constants", true);
329 }
330 }
331 }
332
333 // Storage choice
334 if(cmdline.isset("one-domain-per-history"))
335 {
336 options.set_option("one-domain-per-history", true);
337 options.set_option("storage set", true);
338 }
339 else if(cmdline.isset("one-domain-per-location"))
340 {
341 options.set_option("one-domain-per-location", true);
342 options.set_option("storage set", true);
343 }
344
345 if(!options.get_bool_option("storage set"))
346 {
347 // one-domain-per-location and one-domain-per-history are effectively
348 // the same when using ahistorical so we default to per-history so that
349 // more sophisticated history objects work as expected
350 log.status() << "Storage not specified,"
351 << " defaulting to --one-domain-per-history" << messaget::eom;
352 options.set_option("one-domain-per-history", true);
353 options.set_option("storage set", true);
354 }
355
356 if(cmdline.isset("validate-goto-model"))
357 {
358 options.set_option("validate-goto-model", true);
359 }
360}
361
364{
365 if(cmdline.isset("version"))
366 {
367 std::cout << CBMC_VERSION << '\n';
369 }
370
371 //
372 // command line options
373 //
374
375 optionst options;
379
380 log_version_and_architecture("GOTO-ANALYZER");
381
383
384 // configure gcc, if required
386 {
387 gcc_versiont gcc_version;
388 gcc_version.get("gcc");
389 configure_gcc(gcc_version);
390 }
391
393
394 // Preserve backwards compatibility in processing
395 options.set_option("partial-inline", true);
396 options.set_option("rewrite-rw-ok", false);
397 options.set_option("rewrite-union", false);
398 options.set_option("remove-returns", true);
399
400 if(process_goto_program(options))
402
403 if(cmdline.isset("validate-goto-model"))
404 {
406 }
407
408 // show it?
409 if(cmdline.isset("show-symbol-table"))
410 {
413 }
414
415 // show it?
416 if(
417 cmdline.isset("show-goto-functions") ||
418 cmdline.isset("list-goto-functions"))
419 {
421 goto_model, ui_message_handler, cmdline.isset("list-goto-functions"));
423 }
424
425 return perform_analysis(options);
426}
427
430{
431 if(options.get_bool_option("taint"))
432 {
433 std::string taint_file=cmdline.get_value("taint");
434
435 if(cmdline.isset("show-taint"))
436 {
439 }
440 else
441 {
442 std::string json_file=cmdline.get_value("json");
443 bool result = taint_analysis(
446 }
447 }
448
449 // If no domain is given, this lightweight version of the analysis is used.
450 if(options.get_bool_option("unreachable-instructions") &&
451 options.get_bool_option("specific-analysis"))
452 {
453 const std::string json_file=cmdline.get_value("json");
454
455 if(json_file.empty())
456 unreachable_instructions(goto_model, false, std::cout);
457 else if(json_file=="-")
458 unreachable_instructions(goto_model, true, std::cout);
459 else
460 {
461 std::ofstream ofs(json_file);
462 if(!ofs)
463 {
464 log.error() << "Failed to open json output '" << json_file << "'"
465 << messaget::eom;
467 }
468
470 }
471
473 }
474
475 if(options.get_bool_option("unreachable-functions") &&
476 options.get_bool_option("specific-analysis"))
477 {
478 const std::string json_file=cmdline.get_value("json");
479
480 if(json_file.empty())
481 unreachable_functions(goto_model, false, std::cout);
482 else if(json_file=="-")
483 unreachable_functions(goto_model, true, std::cout);
484 else
485 {
486 std::ofstream ofs(json_file);
487 if(!ofs)
488 {
489 log.error() << "Failed to open json output '" << json_file << "'"
490 << messaget::eom;
492 }
493
495 }
496
498 }
499
500 if(options.get_bool_option("reachable-functions") &&
501 options.get_bool_option("specific-analysis"))
502 {
503 const std::string json_file=cmdline.get_value("json");
504
505 if(json_file.empty())
506 reachable_functions(goto_model, false, std::cout);
507 else if(json_file=="-")
508 reachable_functions(goto_model, true, std::cout);
509 else
510 {
511 std::ofstream ofs(json_file);
512 if(!ofs)
513 {
514 log.error() << "Failed to open json output '" << json_file << "'"
515 << messaget::eom;
517 }
518
520 }
521
523 }
524
525 if(options.get_bool_option("show-local-may-alias"))
526 {
528
530 {
531 std::cout << ">>>>\n";
532 std::cout << ">>>> " << gf_entry.first << '\n';
533 std::cout << ">>>>\n";
534 local_may_aliast local_may_alias(gf_entry.second);
535 local_may_alias.output(std::cout, gf_entry.second, ns);
536 std::cout << '\n';
537 }
538
540 }
541
543
544 if(cmdline.isset("show-properties"))
545 {
548 }
549
550 if(cmdline.isset("property"))
552
553 if(options.get_bool_option("general-analysis"))
554 {
555 // Output file factory
556 const std::string outfile=options.get_option("outfile");
557
558 std::ofstream output_stream;
559 if(outfile != "-" && !outfile.empty())
560 output_stream.open(outfile);
561
562 std::ostream &out(
563 (outfile == "-" || outfile.empty()) ? std::cout : output_stream);
564
565 if(!out)
566 {
567 log.error() << "Failed to open output file '" << outfile << "'"
568 << messaget::eom;
570 }
571
572 // Build analyzer
573 log.status() << "Selecting abstract domain" << messaget::eom;
574 namespacet ns(goto_model.symbol_table); // Must live as long as the domain.
575 std::unique_ptr<ai_baset> analyzer;
576
577 try
578 {
580 }
582 {
583 log.error() << e.what() << messaget::eom;
585 }
586
587 if(analyzer == nullptr)
588 {
589 log.status() << "Task / Interpreter combination not supported"
590 << messaget::eom;
592 }
593
594 // Run
595 log.status() << "Computing abstract states" << messaget::eom;
596 (*analyzer)(goto_model);
597
598 // Perform the task
599 log.status() << "Performing task" << messaget::eom;
600
601 bool result = true;
602
603 if(options.get_bool_option("show"))
604 {
605 static_show_domain(goto_model, *analyzer, options, out);
607 }
608 else if(options.get_bool_option("show-on-source"))
609 {
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 PRECONDITION(!outfile.empty() && outfile != "-");
621 output_stream.close();
622 output_stream.open(outfile, std::ios::binary);
623 result = static_simplifier(
624 goto_model, *analyzer, options, ui_message_handler, out);
625 }
626 else if(options.get_bool_option("unreachable-instructions"))
627 {
629 *analyzer,
630 options,
631 out);
632 }
633 else if(options.get_bool_option("unreachable-functions"))
634 {
636 *analyzer,
637 options,
638 out);
639 }
640 else if(options.get_bool_option("reachable-functions"))
641 {
643 *analyzer,
644 options,
645 out);
646 }
647 else
648 {
649 log.error() << "Unhandled task" << messaget::eom;
651 }
652
653 return result ?
655 }
656
657 // Final defensive error case
658 log.error() << "no analysis option given -- consider reading --help"
659 << messaget::eom;
661}
662
664 const optionst &options)
665{
666 // Remove inline assembler; this needs to happen before
667 // adding the library.
669
670 // add the library
671 log.status() << "Adding CPROVER library (" << config.ansi_c.arch << ")"
672 << messaget::eom;
675
676 // Common removal of types and complex constructs
678 return true;
679
680 return false;
681}
682
685{
686 std::cout << '\n'
687 << banner_string("GOTO-ANALYZER", CBMC_VERSION) << '\n'
688 << align_center_with_border("Copyright (C) 2017-2018") << '\n'
689 << align_center_with_border("Daniel Kroening, Diffblue") << '\n'
690 << align_center_with_border("kroening@kroening.com") << '\n';
691
692 // clang-format off
693 std::cout << help_formatter(
694 "\n"
695 "Usage: \tPurpose:\n"
696 "\n"
697 " {bgoto-analyzer} [{y-?}|{y-h}|{y--help}] \t show this help\n"
698 " {bgoto-analyzer} {ufile.c...} \t source file names\n"
699 "\n"
700 "Task options:\n"
701 " {y--show} \t display the abstract states on the goto program\n"
702 " {y--show-on-source} \t display the abstract states on the source\n"
703 " {y--verify} \t use the abstract domains to check assertions\n"
704 " {y--simplify} {ufile_name} \t use the abstract domains to simplify the"
705 " program\n"
706 " {y--no-simplify-slicing} \t do not remove instructions from which no"
707 " property can be reached (use with {y--simplify})\n"
708 " {y--unreachable-instructions} \t list dead code\n"
709 " {y--unreachable-functions} \t list functions unreachable from the entry"
710 " point\n"
711 " {y--reachable-functions} \t list functions reachable from the entry"
712 " point\n"
713 "\n"
714 "Abstract interpreter options:\n"
715 " {y--legacy-ait} \t recursion for function and one domain per location\n"
716 " {y--recursive-interprocedural} \t use recursion to handle interprocedural"
717 " reasoning\n"
718 " {y--three-way-merge} \t use VSD's three-way merge on return from function"
719 " call\n"
720 " {y--legacy-concurrent} \t legacy-ait with an extended fixed-point for"
721 " concurrency\n"
722 " {y--location-sensitive} \t use location-sensitive abstract interpreter\n"
723 "\n"
724 "History options:\n"
725 " {y--ahistorical} \t the most basic history, tracks locations only\n"
726 " {y--call-stack} {un} \t track the calling location stack for each"
727 " function limiting to at most {un} recursive loops, 0 to disable\n"
728 " {y--loop-unwind} {un} \t track the number of loop iterations within a"
729 " function limited to {un} histories per location, 0 is unlimited\n"
730 " {y--branching} {un} \t track the forwards jumps (if, switch, etc.) within"
731 " a function limited to {un} histories per location, 0 is unlimited\n"
732 " {y--loop-unwind-and-branching} {un} \t track all local control flow"
733 " limited to {un} histories per location, 0 is unlimited\n"
734 "\n"
735 "Domain options:\n"
736 " {y--constants} \t a constant for each variable if possible\n"
737 " {y--intervals} \t an interval for each variable\n"
738 " {y--non-null} \t tracks which pointers are non-null\n"
739 " {y--dependence-graph} \t data and control dependencies between"
740 " instructions\n"
741 " {y--vsd}, {y--variable-sensitivity} \t a configurable non-relational"
742 " domain\n"
743 " {y--dependence-graph-vs} \t dependencies between instructions using VSD\n"
744 "\n"
745 "Variable sensitivity domain (VSD) options:\n"
747 "\n"
748 "Storage options:\n"
749 " {y--one-domain-per-location} \t stores a domain for each location"
750 " reached\n"
751 " {y--one-domain-per-history} \t stores a domain for each history object"
752 " created\n"
753 "\n"
754 "Output options:\n"
755 " {y--text} {ufile_name} \t output results in plain text to given file\n"
756 " {y--json} {ufile_name} \t output results in JSON format to given file\n"
757 " {y--xml} {ufile_name} \t output results in XML format to given file\n"
758 " {y--dot} {ufile_name} \t output results in DOT format to given file\n"
759 "\n"
760 "Specific analyses:\n"
761 " {y--taint} {ufile_name} \t perform taint analysis using rules in given"
762 " file\n"
763 " {y--show-taint} \t print taint analysis results on stdout\n"
764 " {y--show-local-may-alias} \t perform procedure-local may alias analysis\n"
765 "\n"
766 "C/C++ frontend options:\n"
769 "\n"
770 "Platform options:\n"
772 "\n"
773 "Program representations:\n"
774 " {y--show-parse-tree} \t show parse tree\n"
775 " {y--show-symbol-table} \t show loaded symbol table\n"
778 "\n"
779 "Program instrumentation options:\n"
780 " {y--property} {uid} \t enable selected properties only\n"
783 "\n"
784 "Other options:\n"
786 " {y--version} \t show version and exit\n"
788 " {y--verbosity} {u#} \t verbosity level\n"
790 "\n");
791 // clang-format on
792}
Abstract Interpretation.
void cprover_c_library_factory(const std::set< irep_idt > &functions, const symbol_table_baset &symbol_table, symbol_table_baset &dest_symbol_table, message_handlert &message_handler)
configt config
Definition config.cpp:25
std::unique_ptr< ai_baset > build_analyzer(const optionst &options, const goto_modelt &goto_model, const namespacet &ns, message_handlert &mh)
Ideally this should be a pure function of options.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
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
bool set(const cmdlinet &cmdline)
Definition config.cpp:798
struct configt::ansi_ct ansi_c
void get(const std::string &executable)
virtual int doit() override
invoke main modules
virtual void get_command_line_options(optionst &options)
goto_analyzer_parse_optionst(int argc, const char **argv)
virtual bool process_goto_program(const optionst &options)
virtual int perform_analysis(const optionst &options)
Depending on the command line mode, run one of the analysis tasks.
virtual void help() override
display command line help
function_mapt function_map
void validate(const validation_modet vm=validation_modet::INVARIANT, const goto_model_validation_optionst &goto_model_validation_options=goto_model_validation_optionst{}) const override
Check that the goto model is well-formed.
Definition goto_model.h:105
symbol_tablet symbol_table
Symbol table.
Definition goto_model.h:31
goto_functionst goto_functions
GOTO functions.
Definition goto_model.h:34
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
std::string what() const override
A human readable description of what went wrong.
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
#define HELP_CONFIG_LIBRARY
Definition config.h:76
#define HELP_CONFIG_PLATFORM
Definition config.h:94
#define HELP_CONFIG_C_CPP
Definition config.h:32
void cprover_cpp_library_factory(const std::set< irep_idt > &functions, const symbol_table_baset &symbol_table, symbol_table_baset &dest_symbol_table, message_handlert &message_handler)
static void show_goto_functions(const goto_modelt &goto_model)
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_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 configure_gcc(const gcc_versiont &gcc_version)
Goto-Analyser Command Line Option Processing.
#define GOTO_ANALYSER_OPTIONS
#define PARSE_OPTIONS_GOTO_CHECK(cmdline, options)
#define HELP_GOTO_CHECK
Help Formatter.
static help_formattert help_formatter(const std::string &s)
goto_modelt initialize_goto_model(const std::vector< std::string > &files, message_handlert &message_handler, const optionst &options)
Initialize a Goto Program.
#define HELP_FUNCTIONS
Definition language.h:33
Field-insensitive, location-sensitive may-alias analysis.
STL namespace.
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_asm(goto_functionst &goto_functions, symbol_tablet &symbol_table)
Replaces inline assembly instructions in the goto program (i.e., instructions of kind OTHER with a co...
Remove 'asm' statements by compiling them into suitable standard goto program instructions.
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_on_source(const std::string &source_file, const goto_modelt &goto_model, const ai_baset &ai, message_handlert &message_handler)
output source code annotated with abstract states for given file
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 PRECONDITION(CONDITION)
Definition invariant.h:463
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.
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
#define HELP_FLUSH
Definition ui_message.h:108
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.
#define HELP_VALIDATE
#define HELP_VSD
#define PARSE_OPTIONS_VSD(cmdline, options)
const char * CBMC_VERSION