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
26
27#include <analyses/ai.h>
30#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 optionst &options,
61 const bool enabled)
62{
63 // Checks enabled by default in v6.0+.
64 options.set_option("bounds-check", enabled);
65 options.set_option("pointer-check", enabled);
66 options.set_option("pointer-primitive-check", enabled);
67 options.set_option("div-by-zero-check", enabled);
68 options.set_option("signed-overflow-check", enabled);
69 options.set_option("undefined-shift-check", enabled);
70
71 if(enabled)
72 {
73 config.ansi_c.malloc_may_fail = true;
74 config.ansi_c.malloc_failure_mode =
76 }
77 else
78 {
79 config.ansi_c.malloc_may_fail = false;
80 config.ansi_c.malloc_failure_mode =
82 }
83
84 // This is in-line with the options we set for CBMC in cbmc_parse_optionst
85 // with the exception of unwinding-assertions, which don't make sense in
86 // the context of abstract interpretation.
87}
88
90{
92 options, !cmdline.isset("no-standard-checks"));
93
94 if(config.set(cmdline))
95 {
98 }
99
100 if(cmdline.isset("function"))
101 options.set_option("function", cmdline.get_value("function"));
102
103 // all (other) checks supported by goto_check
105
106 // The user should either select:
107 // 1. a specific analysis, or
108 // 2. a tuple of task / analyser options / outputs
109
110 // Select a specific analysis
111 if(cmdline.isset("taint"))
112 {
113 options.set_option("taint", true);
114 options.set_option("specific-analysis", true);
115 }
116 // For backwards compatibility,
117 // these are first recognised as specific analyses
118 bool reachability_task = false;
119 if(cmdline.isset("unreachable-instructions"))
120 {
121 options.set_option("unreachable-instructions", true);
122 options.set_option("specific-analysis", true);
123 reachability_task = true;
124 }
125 if(cmdline.isset("unreachable-functions"))
126 {
127 options.set_option("unreachable-functions", true);
128 options.set_option("specific-analysis", true);
129 reachability_task = true;
130 }
131 if(cmdline.isset("reachable-functions"))
132 {
133 options.set_option("reachable-functions", true);
134 options.set_option("specific-analysis", true);
135 reachability_task = true;
136 }
137 if(cmdline.isset("show-local-may-alias"))
138 {
139 options.set_option("show-local-may-alias", true);
140 options.set_option("specific-analysis", true);
141 }
142
143 // Output format choice
144 if(cmdline.isset("text"))
145 {
146 options.set_option("text", true);
147 options.set_option("outfile", cmdline.get_value("text"));
148 }
149 else if(cmdline.isset("json"))
150 {
151 options.set_option("json", true);
152 options.set_option("outfile", cmdline.get_value("json"));
153 }
154 else if(cmdline.isset("xml"))
155 {
156 options.set_option("xml", true);
157 options.set_option("outfile", cmdline.get_value("xml"));
158 }
159 else if(cmdline.isset("dot"))
160 {
161 options.set_option("dot", true);
162 options.set_option("outfile", cmdline.get_value("dot"));
163 }
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("show-on-source"))
172 {
173 options.set_option("show-on-source", true);
174 options.set_option("general-analysis", true);
175 }
176 else if(cmdline.isset("verify"))
177 {
178 options.set_option("verify", true);
179 options.set_option("general-analysis", true);
180 }
181 else if(cmdline.isset("simplify"))
182 {
183 if(cmdline.get_value("simplify") == "-")
185 "cannot output goto binary to stdout", "--simplify");
186
187 options.set_option("simplify", true);
188 options.set_option("outfile", cmdline.get_value("simplify"));
189 options.set_option("general-analysis", true);
190
191 // For development allow slicing to be disabled in the simplify task
192 options.set_option(
193 "simplify-slicing",
194 !(cmdline.isset("no-simplify-slicing")));
195 }
196 else if(cmdline.isset("show-intervals"))
197 {
198 // For backwards compatibility
199 options.set_option("show", true);
200 options.set_option("general-analysis", true);
201 options.set_option("intervals", true);
202 options.set_option("domain set", true);
203 }
204 else if(cmdline.isset("show-non-null"))
205 {
206 // For backwards compatibility
207 options.set_option("show", true);
208 options.set_option("general-analysis", true);
209 options.set_option("non-null", true);
210 options.set_option("domain set", true);
211 }
212 else if(cmdline.isset("intervals") || cmdline.isset("non-null"))
213 {
214 // Partial backwards compatability, just giving these domains without
215 // a task will work. However it will use the general default of verify
216 // rather than their historical default of show.
217 options.set_option("verify", true);
218 options.set_option("general-analysis", true);
219 }
220
221 if(options.get_bool_option("general-analysis") || reachability_task)
222 {
223 // Abstract interpreter choice
224 if(cmdline.isset("recursive-interprocedural"))
225 options.set_option("recursive-interprocedural", true);
226 else if(cmdline.isset("three-way-merge"))
227 options.set_option("three-way-merge", true);
228 else if(cmdline.isset("legacy-ait") || cmdline.isset("location-sensitive"))
229 {
230 options.set_option("legacy-ait", true);
231 // Fixes a number of other options as well
232 options.set_option("ahistorical", true);
233 options.set_option("history set", true);
234 options.set_option("one-domain-per-location", true);
235 options.set_option("storage set", true);
236 }
237 else if(cmdline.isset("legacy-concurrent") || cmdline.isset("concurrent"))
238 {
239 options.set_option("legacy-concurrent", true);
240 options.set_option("ahistorical", true);
241 options.set_option("history set", true);
242 options.set_option("one-domain-per-location", true);
243 options.set_option("storage set", true);
244 }
245 else
246 {
247 // Silently default to legacy-ait for backwards compatability
248 options.set_option("legacy-ait", true);
249 // Fixes a number of other options as well
250 options.set_option("ahistorical", true);
251 options.set_option("history set", true);
252 options.set_option("one-domain-per-location", true);
253 options.set_option("storage set", true);
254 }
255
256 // History choice
257 if(cmdline.isset("ahistorical"))
258 {
259 options.set_option("ahistorical", true);
260 options.set_option("history set", true);
261 }
262 else if(cmdline.isset("call-stack"))
263 {
264 options.set_option("call-stack", true);
265 options.set_option(
266 "call-stack-recursion-limit", cmdline.get_value("call-stack"));
267 options.set_option("history set", true);
268 }
269 else if(cmdline.isset("loop-unwind"))
270 {
271 options.set_option("local-control-flow-history", true);
272 options.set_option("local-control-flow-history-forward", false);
273 options.set_option("local-control-flow-history-backward", true);
274 options.set_option(
275 "local-control-flow-history-limit", cmdline.get_value("loop-unwind"));
276 options.set_option("history set", true);
277 }
278 else if(cmdline.isset("branching"))
279 {
280 options.set_option("local-control-flow-history", true);
281 options.set_option("local-control-flow-history-forward", true);
282 options.set_option("local-control-flow-history-backward", false);
283 options.set_option(
284 "local-control-flow-history-limit", cmdline.get_value("branching"));
285 options.set_option("history set", true);
286 }
287 else if(cmdline.isset("loop-unwind-and-branching"))
288 {
289 options.set_option("local-control-flow-history", true);
290 options.set_option("local-control-flow-history-forward", true);
291 options.set_option("local-control-flow-history-backward", true);
292 options.set_option(
293 "local-control-flow-history-limit",
294 cmdline.get_value("loop-unwind-and-branching"));
295 options.set_option("history set", true);
296 }
297
298 if(!options.get_bool_option("history set"))
299 {
300 // Default to ahistorical as it is the expected for of analysis
301 log.status() << "History not specified, defaulting to --ahistorical"
302 << messaget::eom;
303 options.set_option("ahistorical", true);
304 options.set_option("history set", true);
305 }
306
307 // Domain choice
308 if(cmdline.isset("constants"))
309 {
310 options.set_option("constants", true);
311 options.set_option("domain set", true);
312 }
313 else if(cmdline.isset("dependence-graph"))
314 {
315 options.set_option("dependence-graph", true);
316 options.set_option("domain set", true);
317 }
318 else if(cmdline.isset("intervals"))
319 {
320 options.set_option("intervals", true);
321 options.set_option("domain set", true);
322 }
323 else if(cmdline.isset("non-null"))
324 {
325 options.set_option("non-null", true);
326 options.set_option("domain set", true);
327 }
328 else if(cmdline.isset("vsd") || cmdline.isset("variable-sensitivity"))
329 {
330 options.set_option("vsd", true);
331 options.set_option("domain set", true);
332
333 PARSE_OPTIONS_VSD(cmdline, options);
334 }
335 else if(cmdline.isset("dependence-graph-vs"))
336 {
337 options.set_option("dependence-graph-vs", true);
338 options.set_option("domain set", true);
339
340 PARSE_OPTIONS_VSD(cmdline, options);
341 options.set_option("data-dependencies", true); // Always set
342 }
343
344 // Reachability questions, when given with a domain swap from specific
345 // to general tasks so that they can use the domain & parameterisations.
346 if(reachability_task)
347 {
348 if(options.get_bool_option("domain set"))
349 {
350 options.set_option("specific-analysis", false);
351 options.set_option("general-analysis", true);
352 }
353 }
354 else
355 {
356 if(!options.get_bool_option("domain set"))
357 {
358 // Default to constants as it is light-weight but useful
359 log.status() << "Domain not specified, defaulting to --constants"
360 << messaget::eom;
361 options.set_option("constants", true);
362 }
363 }
364 }
365
366 // Storage choice
367 if(cmdline.isset("one-domain-per-history"))
368 {
369 options.set_option("one-domain-per-history", true);
370 options.set_option("storage set", true);
371 }
372 else if(cmdline.isset("one-domain-per-location"))
373 {
374 options.set_option("one-domain-per-location", true);
375 options.set_option("storage set", true);
376 }
377
378 if(!options.get_bool_option("storage set"))
379 {
380 // one-domain-per-location and one-domain-per-history are effectively
381 // the same when using ahistorical so we default to per-history so that
382 // more sophisticated history objects work as expected
383 log.status() << "Storage not specified,"
384 << " defaulting to --one-domain-per-history" << messaget::eom;
385 options.set_option("one-domain-per-history", true);
386 options.set_option("storage set", true);
387 }
388
389 if(cmdline.isset("validate-goto-model"))
390 {
391 options.set_option("validate-goto-model", true);
392 }
393}
394
397{
398 if(cmdline.isset("version"))
399 {
400 std::cout << CBMC_VERSION << '\n';
402 }
403
404 //
405 // command line options
406 //
407
408 optionst options;
411 cmdline.get_value("verbosity"), messaget::M_STATUS, ui_message_handler);
412
413 log_version_and_architecture("GOTO-ANALYZER");
414
416
417 // configure gcc, if required
418 if(config.ansi_c.preprocessor == configt::ansi_ct::preprocessort::GCC)
419 {
420 gcc_versiont gcc_version;
421 gcc_version.get("gcc");
422 configure_gcc(gcc_version);
423 }
424
426
427 // Preserve backwards compatibility in processing
428 options.set_option("partial-inline", true);
429 options.set_option("rewrite-rw-ok", false);
430 options.set_option("rewrite-union", false);
431 options.set_option("remove-returns", true);
432
433 if(process_goto_program(options))
435
436 if(cmdline.isset("validate-goto-model"))
437 {
438 goto_model.validate();
439 }
440
441 // show it?
442 if(cmdline.isset("show-symbol-table"))
443 {
446 }
447
448 // show it?
449 if(
450 cmdline.isset("show-goto-functions") ||
451 cmdline.isset("list-goto-functions"))
452 {
454 goto_model, ui_message_handler, cmdline.isset("list-goto-functions"));
456 }
457
458 return perform_analysis(options);
459}
460
463{
464 if(options.get_bool_option("taint"))
465 {
466 std::string taint_file=cmdline.get_value("taint");
467
468 if(cmdline.isset("show-taint"))
469 {
470 taint_analysis(goto_model, taint_file, ui_message_handler, true);
472 }
473 else
474 {
475 std::string json_file=cmdline.get_value("json");
476 bool result = taint_analysis(
477 goto_model, taint_file, ui_message_handler, false, json_file);
479 }
480 }
481
482 // If no domain is given, this lightweight version of the analysis is used.
483 if(options.get_bool_option("unreachable-instructions") &&
484 options.get_bool_option("specific-analysis"))
485 {
486 const std::string json_file=cmdline.get_value("json");
487
488 if(json_file.empty())
489 unreachable_instructions(goto_model, false, std::cout);
490 else if(json_file=="-")
491 unreachable_instructions(goto_model, true, std::cout);
492 else
493 {
494 std::ofstream ofs(json_file);
495 if(!ofs)
496 {
497 log.error() << "Failed to open json output '" << json_file << "'"
498 << messaget::eom;
500 }
501
503 }
504
506 }
507
508 if(options.get_bool_option("unreachable-functions") &&
509 options.get_bool_option("specific-analysis"))
510 {
511 const std::string json_file=cmdline.get_value("json");
512
513 if(json_file.empty())
514 unreachable_functions(goto_model, false, std::cout);
515 else if(json_file=="-")
516 unreachable_functions(goto_model, true, std::cout);
517 else
518 {
519 std::ofstream ofs(json_file);
520 if(!ofs)
521 {
522 log.error() << "Failed to open json output '" << json_file << "'"
523 << messaget::eom;
525 }
526
528 }
529
531 }
532
533 if(options.get_bool_option("reachable-functions") &&
534 options.get_bool_option("specific-analysis"))
535 {
536 const std::string json_file=cmdline.get_value("json");
537
538 if(json_file.empty())
539 reachable_functions(goto_model, false, std::cout);
540 else if(json_file=="-")
541 reachable_functions(goto_model, true, std::cout);
542 else
543 {
544 std::ofstream ofs(json_file);
545 if(!ofs)
546 {
547 log.error() << "Failed to open json output '" << json_file << "'"
548 << messaget::eom;
550 }
551
553 }
554
556 }
557
558 if(options.get_bool_option("show-local-may-alias"))
559 {
560 namespacet ns(goto_model.symbol_table);
561
562 for(const auto &gf_entry : goto_model.goto_functions.function_map)
563 {
564 std::cout << ">>>>\n";
565 std::cout << ">>>> " << gf_entry.first << '\n';
566 std::cout << ">>>>\n";
567 local_may_aliast local_may_alias(gf_entry.second);
568 local_may_alias.output(std::cout, gf_entry.second, ns);
569 std::cout << '\n';
570 }
571
573 }
574
576
577 if(cmdline.isset("show-properties"))
578 {
581 }
582
583 if(cmdline.isset("property"))
584 ::set_properties(goto_model, cmdline.get_values("property"));
585
586 if(options.get_bool_option("general-analysis"))
587 {
588 // Output file factory
589 const std::string outfile=options.get_option("outfile");
590
591 std::ofstream output_stream;
592 if(outfile != "-" && !outfile.empty())
593 output_stream.open(outfile);
594
595 std::ostream &out(
596 (outfile == "-" || outfile.empty()) ? std::cout : output_stream);
597
598 if(!out)
599 {
600 log.error() << "Failed to open output file '" << outfile << "'"
601 << messaget::eom;
603 }
604
605 // Build analyzer
606 log.status() << "Selecting abstract domain" << messaget::eom;
607 namespacet ns(goto_model.symbol_table); // Must live as long as the domain.
608 std::unique_ptr<ai_baset> analyzer;
609
610 try
611 {
612 analyzer = build_analyzer(options, goto_model, ns, ui_message_handler);
613 }
615 {
616 log.error() << e.what() << messaget::eom;
618 }
619
620 if(analyzer == nullptr)
621 {
622 log.status() << "Task / Interpreter combination not supported"
623 << messaget::eom;
625 }
626
627 // Run
628 log.status() << "Computing abstract states" << messaget::eom;
629 (*analyzer)(goto_model);
630
631 // Perform the task
632 log.status() << "Performing task" << messaget::eom;
633
634 bool result = true;
635
636 if(options.get_bool_option("show"))
637 {
638 static_show_domain(goto_model, *analyzer, options, out);
640 }
641 else if(options.get_bool_option("show-on-source"))
642 {
645 }
646 else if(options.get_bool_option("verify"))
647 {
648 result = static_verifier(
649 goto_model, *analyzer, options, ui_message_handler, out);
650 }
651 else if(options.get_bool_option("simplify"))
652 {
653 PRECONDITION(!outfile.empty() && outfile != "-");
654 output_stream.close();
655 output_stream.open(outfile, std::ios::binary);
656 result = static_simplifier(
657 goto_model, *analyzer, options, ui_message_handler, out);
658 }
659 else if(options.get_bool_option("unreachable-instructions"))
660 {
662 *analyzer,
663 options,
664 out);
665 }
666 else if(options.get_bool_option("unreachable-functions"))
667 {
669 *analyzer,
670 options,
671 out);
672 }
673 else if(options.get_bool_option("reachable-functions"))
674 {
676 *analyzer,
677 options,
678 out);
679 }
680 else
681 {
682 log.error() << "Unhandled task" << messaget::eom;
684 }
685
686 return result ?
688 }
689
690 // Final defensive error case
691 log.error() << "no analysis option given -- consider reading --help"
692 << messaget::eom;
694}
695
697 const optionst &options)
698{
699 // Remove inline assembler; this needs to happen before
700 // adding the library.
702
703 // add the library
704 log.status() << "Adding CPROVER library (" << config.ansi_c.arch << ")"
705 << messaget::eom;
708 // library functions may introduce inline assembler
709 while(has_asm(goto_model))
710 {
715 }
716
717 // Common removal of types and complex constructs
719 return true;
720
721 return false;
722}
723
726{
727 std::cout << '\n'
728 << banner_string("GOTO-ANALYZER", CBMC_VERSION) << '\n'
729 << align_center_with_border("Copyright (C) 2017-2018") << '\n'
730 << align_center_with_border("Daniel Kroening, Diffblue") << '\n'
731 << align_center_with_border("kroening@kroening.com") << '\n';
732
733 // clang-format off
734 std::cout << help_formatter(
735 "\n"
736 "Usage: \tPurpose:\n"
737 "\n"
738 " {bgoto-analyzer} [{y-?}|{y-h}|{y--help}] \t show this help\n"
739 " {bgoto-analyzer} {ufile.c...} \t source file names\n"
740 "\n"
741 "Task options:\n"
742 " {y--show} \t display the abstract states on the goto program\n"
743 " {y--show-on-source} \t display the abstract states on the source\n"
744 " {y--verify} \t use the abstract domains to check assertions\n"
745 " {y--simplify} {ufile_name} \t use the abstract domains to simplify the"
746 " program\n"
747 " {y--no-simplify-slicing} \t do not remove instructions from which no"
748 " property can be reached (use with {y--simplify})\n"
749 " {y--unreachable-instructions} \t list dead code\n"
750 " {y--unreachable-functions} \t list functions unreachable from the entry"
751 " point\n"
752 " {y--reachable-functions} \t list functions reachable from the entry"
753 " point\n"
754 "\n"
755 "Abstract interpreter options:\n"
756 " {y--legacy-ait} \t recursion for function and one domain per location\n"
757 " {y--recursive-interprocedural} \t use recursion to handle interprocedural"
758 " reasoning\n"
759 " {y--three-way-merge} \t use VSD's three-way merge on return from function"
760 " call\n"
761 " {y--legacy-concurrent} \t legacy-ait with an extended fixed-point for"
762 " concurrency\n"
763 " {y--location-sensitive} \t use location-sensitive abstract interpreter\n"
764 "\n"
765 "History options:\n"
766 " {y--ahistorical} \t the most basic history, tracks locations only\n"
767 " {y--call-stack} {un} \t track the calling location stack for each"
768 " function limiting to at most {un} recursive loops, 0 to disable\n"
769 " {y--loop-unwind} {un} \t track the number of loop iterations within a"
770 " function limited to {un} histories per location, 0 is unlimited\n"
771 " {y--branching} {un} \t track the forwards jumps (if, switch, etc.) within"
772 " a function limited to {un} histories per location, 0 is unlimited\n"
773 " {y--loop-unwind-and-branching} {un} \t track all local control flow"
774 " limited to {un} histories per location, 0 is unlimited\n"
775 "\n"
776 "Domain options:\n"
777 " {y--constants} \t a constant for each variable if possible\n"
778 " {y--intervals} \t an interval for each variable\n"
779 " {y--non-null} \t tracks which pointers are non-null\n"
780 " {y--dependence-graph} \t data and control dependencies between"
781 " instructions\n"
782 " {y--vsd}, {y--variable-sensitivity} \t a configurable non-relational"
783 " domain\n"
784 " {y--dependence-graph-vs} \t dependencies between instructions using VSD\n"
785 "\n"
786 "Variable sensitivity domain (VSD) options:\n"
788 "\n"
789 "Storage options:\n"
790 " {y--one-domain-per-location} \t stores a domain for each location"
791 " reached\n"
792 " {y--one-domain-per-history} \t stores a domain for each history object"
793 " created\n"
794 "\n"
795 "Output options:\n"
796 " {y--text} {ufile_name} \t output results in plain text to given file\n"
797 " {y--json} {ufile_name} \t output results in JSON format to given file\n"
798 " {y--xml} {ufile_name} \t output results in XML format to given file\n"
799 " {y--dot} {ufile_name} \t output results in DOT format to given file\n"
800 "\n"
801 "Specific analyses:\n"
802 " {y--taint} {ufile_name} \t perform taint analysis using rules in given"
803 " file\n"
804 " {y--show-taint} \t print taint analysis results on stdout\n"
805 " {y--show-local-may-alias} \t perform procedure-local may alias analysis\n"
806 "\n"
807 "C/C++ frontend options:\n"
810 "\n"
811 "Platform options:\n"
813 "\n"
814 "Program representations:\n"
815 " {y--show-parse-tree} \t show parse tree\n"
816 " {y--show-symbol-table} \t show loaded symbol table\n"
819 "\n"
820 "Program instrumentation options:\n"
821 " {y--property} {uid} \t enable selected properties only\n"
824 "\n"
825 "Other options:\n"
827 " {y--version} \t show version and exit\n"
829 " {y--verbosity} {u#} \t verbosity level\n"
831 "\n");
832 // clang-format on
833}
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.
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
static void set_default_analysis_flags(optionst &options, const bool enabled)
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
@ M_STATUS
Definition message.h:169
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()
parse_options_baset(const std::string &optstring, int argc, const char **argv, const std::string &program)
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:83
#define HELP_CONFIG_PLATFORM
Definition config.h:102
#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:34
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, message_handlert &message_handler)
Replaces inline assembly instructions in the goto program (i.e., instructions of kind OTHER with a co...
bool has_asm(const goto_functionst &goto_functions)
returns true iff the given goto functions use asm instructions
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.
@ malloc_failure_mode_return_null
Definition config.h:306
@ malloc_failure_mode_none
Definition config.h:305
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
#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