cprover
Loading...
Searching...
No Matches
cbmc_parse_options.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: CBMC Command Line Option Processing
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#include "cbmc_parse_options.h"
13
14#include <util/config.h>
15#include <util/exit_codes.h>
16#include <util/help_formatter.h>
17#include <util/invariant.h>
18#include <util/make_unique.h>
19#include <util/unicode.h>
20#include <util/version.h>
21
34
35#include <ansi-c/c_preprocess.h>
37#include <ansi-c/gcc_version.h>
39#include <cpp/cprover_library.h>
58#include <langapi/language.h>
59#include <langapi/mode.h>
61
63
64#include <cstdlib> // exit()
65#include <fstream> // IWYU pragma: keep
66#include <iostream>
67#include <memory>
68
79
81 int argc,
82 const char **argv,
83 const std::string &extra_options)
86 argc,
87 argv,
88 std::string("CBMC ") + CBMC_VERSION)
89{
92}
93
95{
96 // Default true
97 options.set_option("built-in-assertions", true);
98 options.set_option("propagation", true);
99 options.set_option("simple-slice", true);
100 options.set_option("simplify", true);
101 options.set_option("show-goto-symex-steps", false);
102 options.set_option("show-points-to-sets", false);
103 options.set_option("show-array-constraints", false);
104
105 // Other default
106 options.set_option("arrays-uf", "auto");
107 options.set_option("depth", UINT32_MAX);
108}
109
111{
112 if(config.set(cmdline))
113 {
114 usage_error();
116 }
117
120
121 if(cmdline.isset("function"))
122 options.set_option("function", cmdline.get_value("function"));
123
124 if(cmdline.isset("cover") && cmdline.isset("unwinding-assertions"))
125 {
126 log.error()
127 << "--cover and --unwinding-assertions must not be given together"
128 << messaget::eom;
130 }
131
132 if(cmdline.isset("max-field-sensitivity-array-size"))
133 {
134 options.set_option(
135 "max-field-sensitivity-array-size",
136 cmdline.get_value("max-field-sensitivity-array-size"));
137 }
138
139 if(cmdline.isset("no-array-field-sensitivity"))
140 {
141 if(cmdline.isset("max-field-sensitivity-array-size"))
142 {
143 log.error()
144 << "--no-array-field-sensitivity and --max-field-sensitivity-array-size"
145 << " must not be given together" << messaget::eom;
147 }
148 options.set_option("no-array-field-sensitivity", true);
149 }
150
151 if(cmdline.isset("reachability-slice") &&
152 cmdline.isset("reachability-slice-fb"))
153 {
154 log.error()
155 << "--reachability-slice and --reachability-slice-fb must not be "
156 << "given together" << messaget::eom;
158 }
159
160 if(cmdline.isset("full-slice"))
161 options.set_option("full-slice", true);
162
163 if(cmdline.isset("show-symex-strategies"))
164 {
167 }
168
170
171 if(cmdline.isset("program-only"))
172 options.set_option("program-only", true);
173
174 if(cmdline.isset("show-byte-ops"))
175 options.set_option("show-byte-ops", true);
176
177 if(cmdline.isset("show-vcc"))
178 options.set_option("show-vcc", true);
179
180 if(cmdline.isset("cover"))
182
183 if(cmdline.isset("mm"))
184 options.set_option("mm", cmdline.get_value("mm"));
185
186 if(cmdline.isset("symex-complexity-limit"))
187 {
188 options.set_option(
189 "symex-complexity-limit", cmdline.get_value("symex-complexity-limit"));
190 log.warning() << "**** WARNING: Complexity-limited analysis may yield "
191 "unsound verification results"
192 << messaget::eom;
193 }
194
195 if(cmdline.isset("symex-complexity-failed-child-loops-limit"))
196 {
197 options.set_option(
198 "symex-complexity-failed-child-loops-limit",
199 cmdline.get_value("symex-complexity-failed-child-loops-limit"));
200 if(!cmdline.isset("symex-complexity-limit"))
201 {
202 log.warning() << "**** WARNING: Complexity-limited analysis may yield "
203 "unsound verification results"
204 << messaget::eom;
205 }
206 }
207
208 if(cmdline.isset("property"))
209 options.set_option("property", cmdline.get_values("property"));
210
211 if(cmdline.isset("drop-unused-functions"))
212 options.set_option("drop-unused-functions", true);
213
214 if(cmdline.isset("havoc-undefined-functions"))
215 options.set_option("havoc-undefined-functions", true);
216
217 if(cmdline.isset("string-abstraction"))
218 options.set_option("string-abstraction", true);
219
220 if(cmdline.isset("reachability-slice-fb"))
221 options.set_option("reachability-slice-fb", true);
222
223 if(cmdline.isset("reachability-slice"))
224 options.set_option("reachability-slice", true);
225
226 if(cmdline.isset("nondet-static"))
227 options.set_option("nondet-static", true);
228
229 if(cmdline.isset("no-simplify"))
230 options.set_option("simplify", false);
231
232 if(cmdline.isset("stop-on-fail") ||
233 cmdline.isset("dimacs") ||
234 cmdline.isset("outfile"))
235 options.set_option("stop-on-fail", true);
236
237 if(
238 cmdline.isset("trace") || cmdline.isset("compact-trace") ||
239 cmdline.isset("stack-trace") || cmdline.isset("stop-on-fail") ||
241 !cmdline.isset("cover")))
242 {
243 options.set_option("trace", true);
244 }
245
246 if(cmdline.isset("export-symex-ready-goto"))
247 {
248 options.set_option(
249 "export-symex-ready-goto", cmdline.get_value("export-symex-ready-goto"));
250 if(options.get_option("export-symex-ready-goto").empty())
251 {
252 log.error()
253 << "ERROR: Please provide a filename to write the goto-binary to."
254 << messaget::eom;
256 }
257 }
258
259 if(cmdline.isset("localize-faults"))
260 options.set_option("localize-faults", true);
261
262 if(cmdline.isset("unwind"))
263 {
264 options.set_option("unwind", cmdline.get_value("unwind"));
265 if(!cmdline.isset("unwinding-assertions"))
266 {
267 log.warning() << "**** WARNING: Use --unwinding-assertions to obtain "
268 "sound verification results"
269 << messaget::eom;
270 }
271 }
272
273 if(cmdline.isset("depth"))
274 {
275 options.set_option("depth", cmdline.get_value("depth"));
276 log.warning()
277 << "**** WARNING: Depth-bounded analysis may yield unsound verification "
278 "results"
279 << messaget::eom;
280 }
281
282 if(cmdline.isset("slice-by-trace"))
283 {
284 log.error() << "--slice-by-trace has been removed" << messaget::eom;
286 }
287
288 if(cmdline.isset("unwindset"))
289 {
290 options.set_option(
291 "unwindset", cmdline.get_comma_separated_values("unwindset"));
292 if(!cmdline.isset("unwinding-assertions"))
293 {
294 log.warning() << "**** WARNING: Use --unwinding-assertions to obtain "
295 "sound verification results"
296 << messaget::eom;
297 }
298 }
299
300 // constant propagation
301 if(cmdline.isset("no-propagation"))
302 options.set_option("propagation", false);
303
304 // transform self loops to assumptions
305 options.set_option(
306 "self-loops-to-assumptions",
307 !cmdline.isset("no-self-loops-to-assumptions"));
308
309 // all checks supported by goto_check
311
312 // generate unwinding assertions
313 if(cmdline.isset("unwinding-assertions"))
314 {
315 options.set_option("unwinding-assertions", true);
316 options.set_option("paths-symex-explore-all", true);
317 }
318
319 if(cmdline.isset("partial-loops"))
320 {
321 options.set_option("partial-loops", true);
322 log.warning()
323 << "**** WARNING: --partial-loops may yield unsound verification results"
324 << messaget::eom;
325 }
326
327 // remove unused equations
328 if(cmdline.isset("slice-formula"))
329 options.set_option("slice-formula", true);
330
331 if(cmdline.isset("arrays-uf-always"))
332 options.set_option("arrays-uf", "always");
333 else if(cmdline.isset("arrays-uf-never"))
334 options.set_option("arrays-uf", "never");
335
336 if(cmdline.isset("show-array-constraints"))
337 options.set_option("show-array-constraints", true);
338
339 if(cmdline.isset("refine-strings"))
340 {
341 options.set_option("refine-strings", true);
342 options.set_option("string-printable", cmdline.isset("string-printable"));
343 }
344
345 options.set_option(
346 "symex-cache-dereferences", cmdline.isset("symex-cache-dereferences"));
347
348 if(cmdline.isset("incremental-loop"))
349 {
350 options.set_option(
351 "incremental-loop", cmdline.get_value("incremental-loop"));
352 options.set_option("refine", true);
353 options.set_option("refine-arrays", true);
354
355 if(cmdline.isset("unwind-min"))
356 options.set_option("unwind-min", cmdline.get_value("unwind-min"));
357
358 if(cmdline.isset("unwind-max"))
359 options.set_option("unwind-max", cmdline.get_value("unwind-max"));
360
361 if(cmdline.isset("ignore-properties-before-unwind-min"))
362 options.set_option("ignore-properties-before-unwind-min", true);
363
364 if(cmdline.isset("paths"))
365 {
366 log.error() << "--paths not supported with --incremental-loop"
367 << messaget::eom;
369 }
370 }
371
372 if(cmdline.isset("graphml-witness"))
373 {
374 options.set_option("graphml-witness", cmdline.get_value("graphml-witness"));
375 options.set_option("stop-on-fail", true);
376 options.set_option("trace", true);
377 }
378
379 if(cmdline.isset("symex-coverage-report"))
380 {
381 options.set_option(
382 "symex-coverage-report",
383 cmdline.get_value("symex-coverage-report"));
384 options.set_option("paths-symex-explore-all", true);
385 }
386
387 if(cmdline.isset("validate-ssa-equation"))
388 {
389 options.set_option("validate-ssa-equation", true);
390 }
391
392 if(cmdline.isset("validate-goto-model"))
393 {
394 options.set_option("validate-goto-model", true);
395 }
396
397 if(cmdline.isset("show-goto-symex-steps"))
398 options.set_option("show-goto-symex-steps", true);
399
400 if(cmdline.isset("show-points-to-sets"))
401 options.set_option("show-points-to-sets", true);
402
404
405 // Options for process_goto_program
406 options.set_option("rewrite-rw-ok", true);
407 options.set_option("rewrite-union", true);
408
409 if(cmdline.isset("smt1"))
410 {
411 log.error() << "--smt1 is no longer supported" << messaget::eom;
413 }
414
416}
417
420{
421 if(cmdline.isset("version"))
422 {
423 std::cout << CBMC_VERSION << '\n';
425 }
426
427 //
428 // command line options
429 //
430
431 optionst options;
433
436
438
439 //
440 // Unwinding of transition systems is done by hw-cbmc.
441 //
442
443 if(cmdline.isset("module") ||
444 cmdline.isset("gen-interface"))
445 {
446 log.error() << "This version of CBMC has no support for "
447 " hardware modules. Please use hw-cbmc."
448 << messaget::eom;
450 }
451
452 if(cmdline.isset("show-points-to-sets"))
453 {
454 if(!cmdline.isset("json-ui") || cmdline.isset("xml-ui"))
455 {
456 log.error() << "--show-points-to-sets supports only"
457 " json output. Use --json-ui."
458 << messaget::eom;
460 }
461 }
462
463 if(cmdline.isset("show-array-constraints"))
464 {
465 if(!cmdline.isset("json-ui") || cmdline.isset("xml-ui"))
466 {
467 log.error() << "--show-array-constraints supports only"
468 " json output. Use --json-ui."
469 << messaget::eom;
471 }
472 }
473
475
476 // configure gcc, if required
478 {
479 gcc_versiont gcc_version;
480 gcc_version.get("gcc");
481 configure_gcc(gcc_version);
482 }
483
484 if(cmdline.isset("test-preprocessor"))
488
489 if(cmdline.isset("preprocess"))
490 {
491 preprocessing(options);
493 }
494
495 if(cmdline.isset("show-parse-tree"))
496 {
497 if(
498 cmdline.args.size() != 1 ||
500 {
501 log.error() << "Please give exactly one source file" << messaget::eom;
503 }
504
505 std::string filename=cmdline.args[0];
506
507 std::ifstream infile(widen_if_needed(filename));
508
509 if(!infile)
510 {
511 log.error() << "failed to open input file '" << filename << "'"
512 << messaget::eom;
514 }
515
516 std::unique_ptr<languaget> language=
518
519 if(language==nullptr)
520 {
521 log.error() << "failed to figure out type of file '" << filename << "'"
522 << messaget::eom;
524 }
525
526 language->set_language_options(options);
527 language->set_message_handler(ui_message_handler);
528
529 log.status() << "Parsing " << filename << messaget::eom;
530
531 if(language->parse(infile, filename))
532 {
533 log.error() << "PARSING ERROR" << messaget::eom;
535 }
536
537 language->show_parse(std::cout);
539 }
540
543
546
547 if(cmdline.isset("show-claims") || // will go away
548 cmdline.isset("show-properties")) // use this one
549 {
552 }
553
554 if(set_properties())
556
557 // At this point, our goto-model should be in symex-ready-goto form (all of
558 // the transformations have been run and the program is ready to be given
559 // to the solver).
560 if(options.is_set("export-symex-ready-goto"))
561 {
563 options.get_option("export-symex-ready-goto");
564
567
568 if(!success)
569 {
570 log.error() << "ERROR: Unable to export goto-program in file "
573 }
574 else
575 {
576 log.status() << "Exported goto-program in symex-ready-goto form at "
579 }
580 }
581
582 if(
583 options.get_bool_option("program-only") ||
584 options.get_bool_option("show-vcc") ||
585 options.get_bool_option("show-byte-ops"))
586 {
587 if(options.get_bool_option("paths"))
588 {
591 (void)verifier();
592 }
593 else
594 {
597 (void)verifier();
598 }
599
601 }
602
603 if(
604 options.get_bool_option("dimacs") || !options.get_option("outfile").empty())
605 {
606 if(options.get_bool_option("paths"))
607 {
610 (void)verifier();
611 }
612 else
613 {
616 (void)verifier();
617 }
618
620 }
621
622 if(options.is_set("cover"))
623 {
626 (void)verifier();
627 verifier.report();
628
629 if(options.get_bool_option("show-test-suite"))
630 {
632 test_generator(verifier.get_traces());
633 }
634
636 }
637
638 std::unique_ptr<goto_verifiert> verifier = nullptr;
639
640 if(options.is_set("incremental-loop"))
641 {
642 if(options.get_bool_option("stop-on-fail"))
643 {
647 }
648 else
649 {
653 }
654 }
655 else if(
656 options.get_bool_option("stop-on-fail") && options.get_bool_option("paths"))
657 {
658 verifier =
661 }
662 else if(
663 options.get_bool_option("stop-on-fail") &&
664 !options.get_bool_option("paths"))
665 {
666 if(options.get_bool_option("localize-faults"))
667 {
668 verifier =
671 }
672 else
673 {
674 verifier =
677 }
678 }
679 else if(
680 !options.get_bool_option("stop-on-fail") &&
681 options.get_bool_option("paths"))
682 {
686 }
687 else if(
688 !options.get_bool_option("stop-on-fail") &&
689 !options.get_bool_option("paths"))
690 {
691 if(options.get_bool_option("localize-faults"))
692 {
693 verifier =
696 }
697 else
698 {
702 }
703 }
704 else
705 {
707 }
708
709 const resultt result = (*verifier)();
710 verifier->report();
711
712 return result_to_exit_code(result);
713}
714
716{
717 if(cmdline.isset("claim")) // will go away
719
720 if(cmdline.isset("property")) // use this one
722
723 return false;
724}
725
727 goto_modelt &goto_model,
728 const optionst &options,
729 const cmdlinet &cmdline,
730 ui_message_handlert &ui_message_handler)
731{
733 if(cmdline.args.empty())
734 {
735 log.error() << "Please provide a program to verify" << messaget::eom;
737 }
738
740
741 if(cmdline.isset("show-symbol-table"))
742 {
745 }
746
749
750 if(cmdline.isset("validate-goto-model"))
751 {
753 }
754
755 // show it?
756 if(cmdline.isset("show-loops"))
757 {
760 }
761
762 // show it?
763 if(
764 cmdline.isset("show-goto-functions") ||
765 cmdline.isset("list-goto-functions"))
766 {
768 goto_model, ui_message_handler, cmdline.isset("list-goto-functions"));
770 }
771
773
774 return -1; // no error, continue
775}
776
778{
779 if(cmdline.args.size() != 1)
780 {
781 log.error() << "Please provide one program to preprocess" << messaget::eom;
782 return;
783 }
784
785 std::string filename = cmdline.args[0];
786
787 std::ifstream infile(filename);
788
789 if(!infile)
790 {
791 log.error() << "failed to open input file" << messaget::eom;
792 return;
793 }
794
795 std::unique_ptr<languaget> language = get_language_from_filename(filename);
796 language->set_language_options(options);
797
798 if(language == nullptr)
799 {
800 log.error() << "failed to figure out type of file" << messaget::eom;
801 return;
802 }
803
804 language->set_message_handler(ui_message_handler);
805
806 if(language->preprocess(infile, filename, std::cout))
807 log.error() << "PREPROCESSING ERROR" << messaget::eom;
808}
809
811 goto_modelt &goto_model,
812 const optionst &options,
813 messaget &log)
814{
815 // Remove inline assembler; this needs to happen before
816 // adding the library.
818
819 // add the library
820 log.status() << "Adding CPROVER library (" << config.ansi_c.arch << ")"
821 << messaget::eom;
826
827 // Common removal of types and complex constructs
829 return true;
830
831 // ignore default/user-specified initialization
832 // of variables with static lifetime
833 if(options.get_bool_option("nondet-static"))
834 {
835 log.status() << "Adding nondeterministic initialization "
836 "of static/global variables"
837 << messaget::eom;
839 }
840
841 // add failed symbols
842 // needs to be done before pointer analysis
844
845 if(options.get_bool_option("drop-unused-functions"))
846 {
847 // Entry point will have been set before and function pointers removed
848 log.status() << "Removing unused functions" << messaget::eom;
850 }
851
852 // remove skips such that trivial GOTOs are deleted and not considered
853 // for coverage annotation:
855
856 // instrument cover goals
857 if(options.is_set("cover"))
858 {
859 const auto cover_config = get_cover_config(
863 return true;
864 }
865
866 // label the assertions
867 // This must be done after adding assertions and
868 // before using the argument of the "property" option.
869 // Do not re-label after using the property slicer because
870 // this would cause the property identifiers to change.
872
873 // reachability slice?
874 if(options.get_bool_option("reachability-slice-fb"))
875 {
876 log.status() << "Performing a forwards-backwards reachability slice"
877 << messaget::eom;
878 if(options.is_set("property"))
879 {
882 options.get_list_option("property"),
883 true,
885 }
886 else
888 }
889
890 if(options.get_bool_option("reachability-slice"))
891 {
892 log.status() << "Performing a reachability slice" << messaget::eom;
893 if(options.is_set("property"))
894 {
897 options.get_list_option("property"),
899 }
900 else
902 }
903
904 // full slice?
905 if(options.get_bool_option("full-slice"))
906 {
907 log.warning() << "**** WARNING: Experimental option --full-slice, "
908 << "analysis results may be unsound. See "
909 << "https://github.com/diffblue/cbmc/issues/260"
910 << messaget::eom;
911 log.status() << "Performing a full slice" << messaget::eom;
912 if(options.is_set("property"))
913 property_slicer(goto_model, options.get_list_option("property"));
914 else
916 }
917
918 // remove any skips introduced since coverage instrumentation
920
921 return false;
922}
923
926{
927 // clang-format off
928 std::cout << '\n' << banner_string("CBMC", CBMC_VERSION) << '\n'
929 << align_center_with_border("Copyright (C) 2001-2018") << '\n'
930 << align_center_with_border("Daniel Kroening, Edmund Clarke") << '\n' // NOLINT(*)
931 << align_center_with_border("Carnegie Mellon University, Computer Science Department") << '\n' // NOLINT(*)
932 << align_center_with_border("kroening@kroening.com") << '\n' // NOLINT(*)
933 << align_center_with_border("Protected in part by U.S. patent 7,225,417") << '\n'; // NOLINT(*)
934
935 std::cout << help_formatter(
936 "\n"
937 "Usage: \tPurpose:\n"
938 "\n"
939 " {bcbmc} [{y-?}] [{y-h}] [{y--help}] \t show this help\n"
940 " {bcbmc} {y--version} \t show version and exit\n"
941 " {bcbmc} [options] {ufile.c} {u...} \t perform bounded model checking\n"
942 "\n"
943 "Analysis options:\n"
945 " {y--symex-coverage-report} {uf} \t generate a Cobertura XML coverage"
946 " report in {uf}\n"
947 " {y--property} {uid} \t only check one specific property\n"
948 " {y--trace} \t give a counterexample trace for failed properties\n"
949 " {y--stop-on-fail} \t stop analysis once a failed property is detected"
950 " (implies {y--trace})\n"
951 " {y--localize-faults} \t localize faults (experimental)\n"
952 "\n"
953 "C/C++ frontend options:\n"
954 " {y--preprocess} \t stop after preprocessing\n"
955 " {y--test-preprocessor} \t stop after preprocessing, discard output\n"
959 "\n"
960 "Platform options:\n"
962 "\n"
963 "Program representations:\n"
964 " {y--show-parse-tree} \t show parse tree\n"
965 " {y--show-symbol-table} \t show loaded symbol table\n"
968 " {y--export-symex-ready-goto} {uf} \t "
969 "serialise goto-program in symex-ready-goto form in {uf}\n"
970 "\n"
971 "Program instrumentation options:\n"
974 " {y--mm} {uMM} \t memory consistency model for concurrent programs"
975 " (default: {ysc})\n"
978 " {y--full-slice} \t run full slicer (experimental)\n"
979 " {y--drop-unused-functions} \t drop functions trivially unreachable from"
980 " main function\n"
981 " {y--havoc-undefined-functions} \t for any function that has no body,"
982 " assign non-deterministic values to any parameters passed as non-const"
983 " pointers and the return value\n"
984 "\n"
985 "Semantic transformations:\n"
986 " {y--nondet-static} \t add nondeterministic initialization of variables"
987 " with static lifetime\n"
988 "\n"
989 "BMC options:\n"
991 "\n"
992 "Backend options:\n"
996 " {y--arrays-uf-never} \t never turn arrays into uninterpreted functions\n"
997 " {y--arrays-uf-always} \t always turn arrays into uninterpreted"
998 " functions\n"
999 " {y--show-array-constraints} \t show array theory constraints added"
1000 " during post processing. Requires {y--json-ui}.\n"
1001 "\n"
1002 "User-interface options:\n"
1007 " {y--verbosity} {u#} \t verbosity level\n"
1009 "\n");
1010 // clang-format on
1011}
void add_failed_symbols(symbol_table_baset &symbol_table)
Create a failed-dereference symbol for all symbols in the given table that need one (i....
Pointer Dereferencing.
Goto Verifier for Verifying all Properties.
Goto verifier for verifying all properties that stores traces and localizes faults.
Goto verifier for verifying all properties that stores traces.
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)
#define HELP_ANSI_C_LANGUAGE
configt config
Definition config.cpp:25
Bounded Model Checking Utilities.
#define HELP_BMC
Definition bmc_util.h:197
void parse_c_object_factory_options(const cmdlinet &cmdline, optionst &options)
Parse the c object factory parameters from a given command line.
bool test_c_preprocessor(message_handlert &message_handler)
Test Input Generator for C.
CBMC Command Line Option Processing.
#define CBMC_OPTIONS
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
Requires an incremental goto checker that is a goto_trace_providert and fault_localization_providert.
virtual int doit() override
invoke main modules
static bool process_goto_program(goto_modelt &, const optionst &, messaget &)
static void set_default_options(optionst &)
Set the options that have default values.
static int get_goto_program(goto_modelt &, const optionst &, const cmdlinet &, ui_message_handlert &)
void get_command_line_options(optionst &)
void register_languages() override
void preprocessing(const optionst &)
virtual void help() override
display command line help
cbmc_parse_optionst(int argc, const char **argv)
std::string get_value(char option) const
Definition cmdline.cpp:48
virtual bool isset(char option) const
Definition cmdline.cpp:30
std::list< std::string > get_comma_separated_values(const char *option) const
Collect all occurrences of option option and split their values on each comma, merging them into a si...
Definition cmdline.cpp:121
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
std::string object_bits_info()
Definition config.cpp:1340
struct configt::ansi_ct ansi_c
void get(const std::string &executable)
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
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:155
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
message_handlert & get_message_handler()
Definition message.h:184
mstreamt & warning() const
Definition message.h:404
@ M_STATISTICS
Definition message.h:171
static eomt eom
Definition message.h:297
mstreamt & status() const
Definition message.h:414
Performs a multi-path symbolic execution using goto-symex and calls a SAT/SMT solver to check the sta...
bool is_set(const std::string &option) const
N.B. opts.is_set("foo") does not imply opts.get_bool_option("foo")
Definition options.cpp:62
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
const value_listt & get_list_option(const std::string &option) const
Definition options.cpp:80
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
Performs a multi-path symbolic execution using goto-symex that incrementally unwinds a given loop and...
Stops when the first failing property is found and localizes the fault Requires an incremental goto c...
virtual uit get_ui() const
Definition ui_message.h:33
#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
#define HELP_CONFIG_BACKEND
Definition config.h:123
static void instrument_cover_goals(const irep_idt &function_id, goto_programt &goto_program, const cover_instrumenterst &instrumenters, const irep_idt &mode, message_handlert &message_handler, const cover_instrumenter_baset::assertion_factoryt &make_assertion)
Applies instrumenters to given goto program.
Definition cover.cpp:37
cover_configt get_cover_config(const optionst &options, const symbol_tablet &symbol_table, message_handlert &message_handler)
Build data structures controlling coverage from command-line options.
Definition cover.cpp:186
void parse_cover_options(const cmdlinet &cmdline, optionst &options)
Parses coverage-related command line options.
Definition cover.cpp:148
Coverage Instrumentation.
#define HELP_COVER
Definition cover.h:33
Goto verifier for covering goals that stores traces.
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_INCORRECT_TASK
The command line is correctly structured but cannot be carried out due to missing files,...
Definition exit_codes.h:49
#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
#define CPROVER_EXIT_SET_PROPERTIES_FAILED
Failure to identify the properties to verify.
Definition exit_codes.h:55
#define CPROVER_EXIT_PREPROCESSOR_TEST_FAILED
Failure of the test-preprocessor method.
Definition exit_codes.h:59
void full_slicer(goto_functionst &goto_functions, const namespacet &ns, const slicing_criteriont &criterion)
void property_slicer(goto_functionst &goto_functions, const namespacet &ns, const std::list< std::string > &properties)
void configure_gcc(const gcc_versiont &gcc_version)
#define PARSE_OPTIONS_GOTO_CHECK(cmdline, options)
#define HELP_GOTO_CHECK
#define PARSE_OPTIONS_GOTO_TRACE(cmdline, options)
Definition goto_trace.h:287
#define HELP_GOTO_TRACE
Definition goto_trace.h:279
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.
void json_interface(cmdlinet &cmdline, message_handlert &message_handler)
Parses the JSON-formatted command line from stdin.
#define HELP_JSON_INTERFACE
Abstract interface to support a programming language.
#define HELP_FUNCTIONS
Definition language.h:33
void show_loop_ids(ui_message_handlert::uit ui, const goto_modelt &goto_model)
Definition loop_ids.cpp:21
Loop IDs.
std::unique_ptr< T > util_make_unique(Ts &&... ts)
Definition make_unique.h:19
std::unique_ptr< languaget > get_language_from_filename(const std::string &filename)
Get the language corresponding to the registered file name extensions.
Definition mode.cpp:102
Goto Checker using Multi-Path Symbolic Execution.
Goto Checker using Multi-Path Symbolic Execution only (no SAT solving)
STL namespace.
static void nondet_static(const namespacet &ns, goto_functionst &goto_functions, const irep_idt &fct_name)
Nondeterministically initializes global scope variables in a goto-function.
Nondeterministically initializes global scope variables, except for constants (such as string literal...
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 parse_path_strategy_options(const cmdlinet &cmdline, optionst &options, message_handlert &message_handler)
add paths and exploration-strategy option, suitable to be invoked from front-ends.
std::string show_path_strategies()
suitable for displaying as a front-end help message
Storage of symbolic execution paths to resume.
int result_to_exit_code(resultt result)
Properties.
resultt
The result of goto verifying.
Definition properties.h:45
void reachability_slicer(goto_modelt &goto_model, const bool include_forward_reachability, message_handlert &message_handler)
Perform reachability slicing on goto_model, with respect to the criterion given by all properties.
#define HELP_REACHABILITY_SLICER
bool is_goto_binary(const std::string &filename, message_handlert &message_handler)
Read Goto Programs.
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 remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Program Transformation.
void remove_unused_functions(goto_modelt &goto_model, message_handlert &message_handler)
Unused function removal.
void label_properties(goto_modelt &goto_model)
Set the properties to check.
Show the goto functions.
#define HELP_SHOW_GOTO_FUNCTIONS
void show_properties(const namespacet &ns, const irep_idt &identifier, message_handlert &message_handler, ui_message_handlert::uit ui, const goto_programt &goto_program)
Show the properties.
#define HELP_SHOW_PROPERTIES
void show_symbol_table(const symbol_table_baset &symbol_table, ui_message_handlert &ui)
Show the symbol table.
Goto Checker using multi-path symbolic execution with incremental unwinding of a specified loop.
Goto Checker using Single Path Symbolic Execution.
Goto Checker using Single Path Symbolic Execution only.
void parse_solver_options(const cmdlinet &cmdline, optionst &options)
Parse solver-related command-line parameters in cmdline and set corresponding values in options.
#define HELP_SOLVER
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:525
Goto Verifier for stopping at the first failing property.
Goto Verifier for stopping at the first failing property and localizing the fault.
#define HELP_STRING_REFINEMENT_CBMC
#define HELP_TIMESTAMP
Definition timestamper.h:14
#define HELP_FLUSH
Definition ui_message.h:108
#define widen_if_needed(s)
Definition unicode.h:28
#define HELP_VALIDATE
const char * CBMC_VERSION
static void write_goto_binary(std::ostream &out, const symbol_table_baset &symbol_table, const goto_functionst &goto_functions, irep_serializationt &irepconverter)
Writes a goto program to disc, using goto binary format.
Write GOTO binaries.
void xml_interface(cmdlinet &cmdline, message_handlert &message_handler)
Parse XML-formatted commandline options from stdin.
#define HELP_XML_INTERFACE