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 <cstdlib> // exit()
15#include <fstream>
16#include <iostream>
17#include <memory>
18
20
22
23#include <cpp/cprover_library.h>
24
32
33#include <analyses/ai.h>
35
36#include <util/config.h>
38#include <util/exit_codes.h>
39#include <util/options.h>
40#include <util/version.h>
41
42#include "build_analyzer.h"
43#include "show_on_source.h"
44#include "static_show_domain.h"
45#include "static_simplifier.h"
46#include "static_verifier.h"
47#include "taint_analysis.h"
49
51 int argc,
52 const char **argv)
55 argc,
56 argv,
57 std::string("GOTO-ANALYZER "))
58{
59}
60
62{
63 if(config.set(cmdline))
64 {
67 }
68
69 if(cmdline.isset("function"))
70 options.set_option("function", cmdline.get_value("function"));
71
72 // all checks supported by goto_check
74
75 // The user should either select:
76 // 1. a specific analysis, or
77 // 2. a tuple of task / analyser options / outputs
78
79 // Select a specific analysis
80 if(cmdline.isset("taint"))
81 {
82 options.set_option("taint", true);
83 options.set_option("specific-analysis", true);
84 }
85 // For backwards compatibility,
86 // these are first recognised as specific analyses
87 bool reachability_task = false;
88 if(cmdline.isset("unreachable-instructions"))
89 {
90 options.set_option("unreachable-instructions", true);
91 options.set_option("specific-analysis", true);
92 reachability_task = true;
93 }
94 if(cmdline.isset("unreachable-functions"))
95 {
96 options.set_option("unreachable-functions", true);
97 options.set_option("specific-analysis", true);
98 reachability_task = true;
99 }
100 if(cmdline.isset("reachable-functions"))
101 {
102 options.set_option("reachable-functions", true);
103 options.set_option("specific-analysis", true);
104 reachability_task = true;
105 }
106 if(cmdline.isset("show-local-may-alias"))
107 {
108 options.set_option("show-local-may-alias", true);
109 options.set_option("specific-analysis", true);
110 }
111
112 // Output format choice
113 if(cmdline.isset("text"))
114 {
115 options.set_option("text", true);
116 options.set_option("outfile", cmdline.get_value("text"));
117 }
118 else if(cmdline.isset("json"))
119 {
120 options.set_option("json", true);
121 options.set_option("outfile", cmdline.get_value("json"));
122 }
123 else if(cmdline.isset("xml"))
124 {
125 options.set_option("xml", true);
126 options.set_option("outfile", cmdline.get_value("xml"));
127 }
128 else if(cmdline.isset("dot"))
129 {
130 options.set_option("dot", true);
131 options.set_option("outfile", cmdline.get_value("dot"));
132 }
133
134 // Task options
135 if(cmdline.isset("show"))
136 {
137 options.set_option("show", true);
138 options.set_option("general-analysis", true);
139 }
140 else if(cmdline.isset("show-on-source"))
141 {
142 options.set_option("show-on-source", true);
143 options.set_option("general-analysis", true);
144 }
145 else if(cmdline.isset("verify"))
146 {
147 options.set_option("verify", true);
148 options.set_option("general-analysis", true);
149 }
150 else if(cmdline.isset("simplify"))
151 {
152 if(cmdline.get_value("simplify") == "-")
154 "cannot output goto binary to stdout", "--simplify");
155
156 options.set_option("simplify", true);
157 options.set_option("outfile", cmdline.get_value("simplify"));
158 options.set_option("general-analysis", true);
159
160 // For development allow slicing to be disabled in the simplify task
161 options.set_option(
162 "simplify-slicing",
163 !(cmdline.isset("no-simplify-slicing")));
164 }
165 else if(cmdline.isset("show-intervals"))
166 {
167 // For backwards compatibility
168 options.set_option("show", true);
169 options.set_option("general-analysis", true);
170 options.set_option("intervals", true);
171 options.set_option("domain set", true);
172 }
173 else if(cmdline.isset("show-non-null"))
174 {
175 // For backwards compatibility
176 options.set_option("show", true);
177 options.set_option("general-analysis", true);
178 options.set_option("non-null", true);
179 options.set_option("domain set", true);
180 }
181 else if(cmdline.isset("intervals") || cmdline.isset("non-null"))
182 {
183 // Partial backwards compatability, just giving these domains without
184 // a task will work. However it will use the general default of verify
185 // rather than their historical default of show.
186 options.set_option("verify", true);
187 options.set_option("general-analysis", true);
188 }
189
190 if(options.get_bool_option("general-analysis") || reachability_task)
191 {
192 // Abstract interpreter choice
193 if(cmdline.isset("recursive-interprocedural"))
194 options.set_option("recursive-interprocedural", true);
195 else if(cmdline.isset("three-way-merge"))
196 options.set_option("three-way-merge", true);
197 else if(cmdline.isset("legacy-ait") || cmdline.isset("location-sensitive"))
198 {
199 options.set_option("legacy-ait", true);
200 // Fixes a number of other options as well
201 options.set_option("ahistorical", true);
202 options.set_option("history set", true);
203 options.set_option("one-domain-per-location", true);
204 options.set_option("storage set", true);
205 }
206 else if(cmdline.isset("legacy-concurrent") || cmdline.isset("concurrent"))
207 {
208 options.set_option("legacy-concurrent", true);
209 options.set_option("ahistorical", true);
210 options.set_option("history set", true);
211 options.set_option("one-domain-per-location", true);
212 options.set_option("storage set", true);
213 }
214 else
215 {
216 // Silently default to legacy-ait for backwards compatability
217 options.set_option("legacy-ait", true);
218 // Fixes a number of other options as well
219 options.set_option("ahistorical", true);
220 options.set_option("history set", true);
221 options.set_option("one-domain-per-location", true);
222 options.set_option("storage set", true);
223 }
224
225 // History choice
226 if(cmdline.isset("ahistorical"))
227 {
228 options.set_option("ahistorical", true);
229 options.set_option("history set", true);
230 }
231 else if(cmdline.isset("call-stack"))
232 {
233 options.set_option("call-stack", true);
234 options.set_option(
235 "call-stack-recursion-limit", cmdline.get_value("call-stack"));
236 options.set_option("history set", true);
237 }
238 else if(cmdline.isset("loop-unwind"))
239 {
240 options.set_option("local-control-flow-history", true);
241 options.set_option("local-control-flow-history-forward", false);
242 options.set_option("local-control-flow-history-backward", true);
243 options.set_option(
244 "local-control-flow-history-limit", cmdline.get_value("loop-unwind"));
245 options.set_option("history set", true);
246 }
247 else if(cmdline.isset("branching"))
248 {
249 options.set_option("local-control-flow-history", true);
250 options.set_option("local-control-flow-history-forward", true);
251 options.set_option("local-control-flow-history-backward", false);
252 options.set_option(
253 "local-control-flow-history-limit", cmdline.get_value("branching"));
254 options.set_option("history set", true);
255 }
256 else if(cmdline.isset("loop-unwind-and-branching"))
257 {
258 options.set_option("local-control-flow-history", true);
259 options.set_option("local-control-flow-history-forward", true);
260 options.set_option("local-control-flow-history-backward", true);
261 options.set_option(
262 "local-control-flow-history-limit",
263 cmdline.get_value("loop-unwind-and-branching"));
264 options.set_option("history set", true);
265 }
266
267 if(!options.get_bool_option("history set"))
268 {
269 // Default to ahistorical as it is the expected for of analysis
270 log.status() << "History not specified, defaulting to --ahistorical"
271 << messaget::eom;
272 options.set_option("ahistorical", true);
273 options.set_option("history set", true);
274 }
275
276 // Domain choice
277 if(cmdline.isset("constants"))
278 {
279 options.set_option("constants", true);
280 options.set_option("domain set", true);
281 }
282 else if(cmdline.isset("dependence-graph"))
283 {
284 options.set_option("dependence-graph", true);
285 options.set_option("domain set", true);
286 }
287 else if(cmdline.isset("intervals"))
288 {
289 options.set_option("intervals", true);
290 options.set_option("domain set", true);
291 }
292 else if(cmdline.isset("non-null"))
293 {
294 options.set_option("non-null", true);
295 options.set_option("domain set", true);
296 }
297 else if(cmdline.isset("vsd") || cmdline.isset("variable-sensitivity"))
298 {
299 options.set_option("vsd", true);
300 options.set_option("domain set", true);
301
302 PARSE_OPTIONS_VSD(cmdline, options);
303 }
304 else if(cmdline.isset("dependence-graph-vs"))
305 {
306 options.set_option("dependence-graph-vs", true);
307 options.set_option("domain set", true);
308
309 PARSE_OPTIONS_VSD(cmdline, options);
310 options.set_option("data-dependencies", true); // Always set
311 }
312
313 // Reachability questions, when given with a domain swap from specific
314 // to general tasks so that they can use the domain & parameterisations.
316 {
317 if(options.get_bool_option("domain set"))
318 {
319 options.set_option("specific-analysis", false);
320 options.set_option("general-analysis", true);
321 }
322 }
323 else
324 {
325 if(!options.get_bool_option("domain set"))
326 {
327 // Default to constants as it is light-weight but useful
328 log.status() << "Domain not specified, defaulting to --constants"
329 << messaget::eom;
330 options.set_option("constants", true);
331 }
332 }
333 }
334
335 // Storage choice
336 if(cmdline.isset("one-domain-per-history"))
337 {
338 options.set_option("one-domain-per-history", true);
339 options.set_option("storage set", true);
340 }
341 else if(cmdline.isset("one-domain-per-location"))
342 {
343 options.set_option("one-domain-per-location", true);
344 options.set_option("storage set", true);
345 }
346
347 if(!options.get_bool_option("storage set"))
348 {
349 // one-domain-per-location and one-domain-per-history are effectively
350 // the same when using ahistorical so we default to per-history so that
351 // more sophisticated history objects work as expected
352 log.status() << "Storage not specified,"
353 << " defaulting to --one-domain-per-history" << messaget::eom;
354 options.set_option("one-domain-per-history", true);
355 options.set_option("storage set", true);
356 }
357
358 if(cmdline.isset("validate-goto-model"))
359 {
360 options.set_option("validate-goto-model", true);
361 }
362}
363
366{
367 if(cmdline.isset("version"))
368 {
369 std::cout << CBMC_VERSION << '\n';
371 }
372
373 //
374 // command line options
375 //
376
377 optionst options;
381
382 log_version_and_architecture("GOTO-ANALYZER");
383
385
387
388 // Preserve backwards compatibility in processing
389 options.set_option("partial-inline", true);
390 options.set_option("rewrite-union", false);
391 options.set_option("remove-returns", true);
392
393 if(process_goto_program(options))
395
396 if(cmdline.isset("validate-goto-model"))
397 {
399 }
400
401 // show it?
402 if(cmdline.isset("show-symbol-table"))
403 {
406 }
407
408 // show it?
409 if(
410 cmdline.isset("show-goto-functions") ||
411 cmdline.isset("list-goto-functions"))
412 {
414 goto_model, ui_message_handler, cmdline.isset("list-goto-functions"));
416 }
417
418 return perform_analysis(options);
419}
420
423{
424 if(options.get_bool_option("taint"))
425 {
426 std::string taint_file=cmdline.get_value("taint");
427
428 if(cmdline.isset("show-taint"))
429 {
432 }
433 else
434 {
435 std::string json_file=cmdline.get_value("json");
436 bool result = taint_analysis(
439 }
440 }
441
442 // If no domain is given, this lightweight version of the analysis is used.
443 if(options.get_bool_option("unreachable-instructions") &&
444 options.get_bool_option("specific-analysis"))
445 {
446 const std::string json_file=cmdline.get_value("json");
447
448 if(json_file.empty())
449 unreachable_instructions(goto_model, false, std::cout);
450 else if(json_file=="-")
451 unreachable_instructions(goto_model, true, std::cout);
452 else
453 {
454 std::ofstream ofs(json_file);
455 if(!ofs)
456 {
457 log.error() << "Failed to open json output '" << json_file << "'"
458 << messaget::eom;
460 }
461
463 }
464
466 }
467
468 if(options.get_bool_option("unreachable-functions") &&
469 options.get_bool_option("specific-analysis"))
470 {
471 const std::string json_file=cmdline.get_value("json");
472
473 if(json_file.empty())
474 unreachable_functions(goto_model, false, std::cout);
475 else if(json_file=="-")
476 unreachable_functions(goto_model, true, std::cout);
477 else
478 {
479 std::ofstream ofs(json_file);
480 if(!ofs)
481 {
482 log.error() << "Failed to open json output '" << json_file << "'"
483 << messaget::eom;
485 }
486
488 }
489
491 }
492
493 if(options.get_bool_option("reachable-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 reachable_functions(goto_model, false, std::cout);
500 else if(json_file=="-")
501 reachable_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
513 }
514
516 }
517
518 if(options.get_bool_option("show-local-may-alias"))
519 {
521
523 {
524 std::cout << ">>>>\n";
525 std::cout << ">>>> " << gf_entry.first << '\n';
526 std::cout << ">>>>\n";
527 local_may_aliast local_may_alias(gf_entry.second);
528 local_may_alias.output(std::cout, gf_entry.second, ns);
529 std::cout << '\n';
530 }
531
533 }
534
536
537 if(cmdline.isset("show-properties"))
538 {
541 }
542
543 if(cmdline.isset("property"))
545
546 if(options.get_bool_option("general-analysis"))
547 {
548 // Output file factory
549 const std::string outfile=options.get_option("outfile");
550
551 std::ofstream output_stream;
552 if(outfile != "-" && !outfile.empty())
553 output_stream.open(outfile);
554
555 std::ostream &out(
556 (outfile == "-" || outfile.empty()) ? std::cout : output_stream);
557
558 if(!out)
559 {
560 log.error() << "Failed to open output file '" << outfile << "'"
561 << messaget::eom;
563 }
564
565 // Build analyzer
566 log.status() << "Selecting abstract domain" << messaget::eom;
567 namespacet ns(goto_model.symbol_table); // Must live as long as the domain.
568 std::unique_ptr<ai_baset> analyzer;
569
570 try
571 {
573 }
575 {
576 log.error() << e.what() << messaget::eom;
578 }
579
580 if(analyzer == nullptr)
581 {
582 log.status() << "Task / Interpreter combination not supported"
583 << messaget::eom;
585 }
586
587 // Run
588 log.status() << "Computing abstract states" << messaget::eom;
589 (*analyzer)(goto_model);
590
591 // Perform the task
592 log.status() << "Performing task" << messaget::eom;
593
594 bool result = true;
595
596 if(options.get_bool_option("show"))
597 {
598 static_show_domain(goto_model, *analyzer, options, out);
600 }
601 else if(options.get_bool_option("show-on-source"))
602 {
605 }
606 else if(options.get_bool_option("verify"))
607 {
608 result = static_verifier(
609 goto_model, *analyzer, options, ui_message_handler, out);
610 }
611 else if(options.get_bool_option("simplify"))
612 {
613 PRECONDITION(!outfile.empty() && outfile != "-");
614 output_stream.close();
615 output_stream.open(outfile, std::ios::binary);
616 result = static_simplifier(
617 goto_model, *analyzer, options, ui_message_handler, out);
618 }
619 else if(options.get_bool_option("unreachable-instructions"))
620 {
622 *analyzer,
623 options,
624 out);
625 }
626 else if(options.get_bool_option("unreachable-functions"))
627 {
629 *analyzer,
630 options,
631 out);
632 }
633 else if(options.get_bool_option("reachable-functions"))
634 {
636 *analyzer,
637 options,
638 out);
639 }
640 else
641 {
642 log.error() << "Unhandled task" << messaget::eom;
644 }
645
646 return result ?
648 }
649
650 // Final defensive error case
651 log.error() << "no analysis option given -- consider reading --help"
652 << messaget::eom;
654}
655
657 const optionst &options)
658{
659 // Remove inline assembler; this needs to happen before
660 // adding the library.
662
663 // add the library
664 log.status() << "Adding CPROVER library (" << config.ansi_c.arch << ")"
665 << messaget::eom;
668
669 // Common removal of types and complex constructs
671 return true;
672
673 return false;
674}
675
678{
679 // clang-format off
680 std::cout << '\n' << banner_string("GOTO-ANALYZER", CBMC_VERSION) << '\n'
681 << align_center_with_border("Copyright (C) 2017-2018") << '\n'
682 << align_center_with_border("Daniel Kroening, Diffblue") << '\n'
683 << align_center_with_border("kroening@kroening.com") << '\n'
684 <<
685 "\n"
686 "Usage: Purpose:\n"
687 "\n"
688 " goto-analyzer [-h] [--help] show help\n"
689 " goto-analyzer file.c ... source file names\n"
690 "\n"
691 "Task options:\n"
692 " --show display the abstract states on the goto program\n" // NOLINT(*)
693 " --show-on-source display the abstract states on the source\n"
694 // NOLINTNEXTLINE(whitespace/line_length)
695 " --verify use the abstract domains to check assertions\n"
696 // NOLINTNEXTLINE(whitespace/line_length)
697 " --simplify file_name use the abstract domains to simplify the program\n"
698 " --unreachable-instructions list dead code\n"
699 // NOLINTNEXTLINE(whitespace/line_length)
700 " --unreachable-functions list functions unreachable from the entry point\n"
701 // NOLINTNEXTLINE(whitespace/line_length)
702 " --reachable-functions list functions reachable from the entry point\n"
703 "\n"
704 "Abstract interpreter options:\n"
705 // NOLINTNEXTLINE(whitespace/line_length)
706 " --recursive-interprocedural use recursion to handle interprocedural reasoning\n"
707 // NOLINTNEXTLINE(whitespace/line_length)
708 " --three-way-merge use VSD's three-way merge on return from function call\n"
709 // NOLINTNEXTLINE(whitespace/line_length)
710 " --legacy-ait recursion for function and one domain per location\n"
711 // NOLINTNEXTLINE(whitespace/line_length)
712 " --legacy-concurrent legacy-ait with an extended fixed-point for concurrency\n"
713 "\n"
714 "History options:\n"
715 // NOLINTNEXTLINE(whitespace/line_length)
716 " --ahistorical the most basic history, tracks locations only\n"
717 // NOLINTNEXTLINE(whitespace/line_length)
718 " --call-stack n track the calling location stack for each function\n"
719 // NOLINTNEXTLINE(whitespace/line_length)
720 " limiting to at most n recursive loops, 0 to disable\n"
721 // NOLINTNEXTLINE(whitespace/line_length)
722 " --loop-unwind n track the number of loop iterations within a function\n"
723 // NOLINTNEXTLINE(whitespace/line_length)
724 " limited to n histories per location, 0 is unlimited\n"
725 // NOLINTNEXTLINE(whitespace/line_length)
726 " --branching n track the forwards jumps (if, switch, etc.) within a function\n"
727 // NOLINTNEXTLINE(whitespace/line_length)
728 " limited to n histories per location, 0 is unlimited\n"
729 // NOLINTNEXTLINE(whitespace/line_length)
730 " --loop-unwind-and-branching n track all local control flow\n"
731 // NOLINTNEXTLINE(whitespace/line_length)
732 " limited to n histories per location, 0 is unlimited\n"
733 "\n"
734 "Domain options:\n"
735 " --constants a constant for each variable if possible\n"
736 " --intervals an interval for each variable\n"
737 " --non-null tracks which pointers are non-null\n"
738 " --dependence-graph data and control dependencies between instructions\n" // NOLINT(*)
739 " --vsd a configurable non-relational domain\n" // NOLINT(*)
740 " --dependence-graph-vs dependencies between instructions using VSD\n" // NOLINT(*)
741 "\n"
742 "Variable sensitivity domain (VSD) options:\n"
744 "\n"
745 "Storage options:\n"
746 // NOLINTNEXTLINE(whitespace/line_length)
747 " --one-domain-per-history stores a domain for each history object created\n"
748 " --one-domain-per-location stores a domain for each location reached\n"
749 "\n"
750 "Output options:\n"
751 " --text file_name output results in plain text to given file\n"
752 // NOLINTNEXTLINE(whitespace/line_length)
753 " --json file_name output results in JSON format to given file\n"
754 " --xml file_name output results in XML format to given file\n"
755 " --dot file_name output results in DOT format to given file\n"
756 "\n"
757 "Specific analyses:\n"
758 // NOLINTNEXTLINE(whitespace/line_length)
759 " --taint file_name perform taint analysis using rules in given file\n"
760 "\n"
761 "C/C++ frontend options:\n"
764 "\n"
765 "Platform options:\n"
767 "\n"
768 "Program representations:\n"
769 " --show-parse-tree show parse tree\n"
770 " --show-symbol-table show loaded symbol table\n"
773 "\n"
774 "Program instrumentation options:\n"
777 "\n"
778 "Other options:\n"
780 " --version show version and exit\n"
783 "\n";
784 // clang-format on
785}
Abstract Interpretation.
void cprover_c_library_factory(const std::set< irep_idt > &functions, symbol_tablet &symbol_table, message_handlert &message_handler)
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: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
bool set(const cmdlinet &cmdline)
Definition config.cpp:798
struct configt::ansi_ct ansi_c
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:98
symbol_tablet symbol_table
Symbol table.
Definition goto_model.h:30
goto_functionst goto_functions
GOTO functions.
Definition goto_model.h:33
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
configt config
Definition config.cpp:25
#define HELP_CONFIG_LIBRARY
Definition config.h:62
#define HELP_CONFIG_PLATFORM
Definition config.h:81
#define HELP_CONFIG_C_CPP
Definition config.h:33
void cprover_cpp_library_factory(const std::set< irep_idt > &functions, symbol_tablet &symbol_table, message_handlert &message_handler)
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
Goto-Analyser Command Line Option Processing.
#define GOTO_ANALYSER_OPTIONS
#define PARSE_OPTIONS_GOTO_CHECK(cmdline, options)
#define HELP_GOTO_CHECK
goto_modelt initialize_goto_model(const std::vector< std::string > &files, message_handlert &message_handler, const optionst &options)
Initialize a Goto Program.
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)
#define HELP_FUNCTIONS
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.
Replace function returns by assignments to global variables.
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_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_tablet &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