cprover
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 <cstdlib> // exit()
15#include <fstream>
16#include <iostream>
17#include <memory>
18
19#include <util/config.h>
20#include <util/exit_codes.h>
21#include <util/invariant.h>
22#include <util/make_unique.h>
23#include <util/version.h>
24
25#ifdef _MSC_VER
26# include <util/unicode.h>
27#endif
28
29#include <langapi/language.h>
30
31#include <ansi-c/c_preprocess.h>
33#include <ansi-c/gcc_version.h>
34
36
37#include <cpp/cprover_library.h>
38
52
64
69
71
73
74#include <langapi/mode.h>
75
77
78cbmc_parse_optionst::cbmc_parse_optionst(int argc, const char **argv)
81 argc,
82 argv,
83 std::string("CBMC ") + CBMC_VERSION)
84{
88
90 int argc,
91 const char **argv,
92 const std::string &extra_options)
94 CBMC_OPTIONS + extra_options,
95 argc,
96 argv,
97 std::string("CBMC ") + CBMC_VERSION)
98{
101}
102
104{
105 // Default true
106 options.set_option("built-in-assertions", true);
107 options.set_option("pretty-names", true);
108 options.set_option("propagation", true);
109 options.set_option("sat-preprocessor", true);
110 options.set_option("simple-slice", true);
111 options.set_option("simplify", true);
112 options.set_option("simplify-if", true);
113 options.set_option("show-goto-symex-steps", false);
114 options.set_option("show-points-to-sets", false);
115 options.set_option("show-array-constraints", false);
116
117 // Other default
118 options.set_option("arrays-uf", "auto");
119 options.set_option("depth", UINT32_MAX);
120}
121
123{
124 if(config.set(cmdline))
125 {
126 usage_error();
128 }
129
132
133 if(cmdline.isset("function"))
134 options.set_option("function", cmdline.get_value("function"));
135
136 if(cmdline.isset("cover") && cmdline.isset("unwinding-assertions"))
137 {
138 log.error()
139 << "--cover and --unwinding-assertions must not be given together"
140 << messaget::eom;
142 }
143
144 if(cmdline.isset("max-field-sensitivity-array-size"))
145 {
146 options.set_option(
147 "max-field-sensitivity-array-size",
148 cmdline.get_value("max-field-sensitivity-array-size"));
149 }
150
151 if(cmdline.isset("no-array-field-sensitivity"))
152 {
153 if(cmdline.isset("max-field-sensitivity-array-size"))
154 {
155 log.error()
156 << "--no-array-field-sensitivity and --max-field-sensitivity-array-size"
157 << " must not be given together" << messaget::eom;
159 }
160 options.set_option("no-array-field-sensitivity", true);
161 }
162
163 if(cmdline.isset("partial-loops") && cmdline.isset("unwinding-assertions"))
164 {
165 log.error()
166 << "--partial-loops and --unwinding-assertions must not be given "
167 << "together" << messaget::eom;
169 }
170
171 if(cmdline.isset("reachability-slice") &&
172 cmdline.isset("reachability-slice-fb"))
173 {
174 log.error()
175 << "--reachability-slice and --reachability-slice-fb must not be "
176 << "given together" << messaget::eom;
178 }
179
180 if(cmdline.isset("full-slice"))
181 options.set_option("full-slice", true);
182
183 if(cmdline.isset("show-symex-strategies"))
184 {
187 }
188
190
191 if(cmdline.isset("program-only"))
192 options.set_option("program-only", true);
193
194 if(cmdline.isset("show-byte-ops"))
195 options.set_option("show-byte-ops", true);
196
197 if(cmdline.isset("show-vcc"))
198 options.set_option("show-vcc", true);
199
200 if(cmdline.isset("cover"))
202
203 if(cmdline.isset("mm"))
204 options.set_option("mm", cmdline.get_value("mm"));
205
206 if(cmdline.isset("symex-complexity-limit"))
207 options.set_option(
208 "symex-complexity-limit", cmdline.get_value("symex-complexity-limit"));
209
210 if(cmdline.isset("symex-complexity-failed-child-loops-limit"))
211 options.set_option(
212 "symex-complexity-failed-child-loops-limit",
213 cmdline.get_value("symex-complexity-failed-child-loops-limit"));
214
215 if(cmdline.isset("property"))
216 options.set_option("property", cmdline.get_values("property"));
217
218 if(cmdline.isset("drop-unused-functions"))
219 options.set_option("drop-unused-functions", true);
220
221 if(cmdline.isset("havoc-undefined-functions"))
222 options.set_option("havoc-undefined-functions", true);
223
224 if(cmdline.isset("string-abstraction"))
225 options.set_option("string-abstraction", true);
226
227 if(cmdline.isset("reachability-slice-fb"))
228 options.set_option("reachability-slice-fb", true);
229
230 if(cmdline.isset("reachability-slice"))
231 options.set_option("reachability-slice", true);
232
233 if(cmdline.isset("nondet-static"))
234 options.set_option("nondet-static", true);
235
236 if(cmdline.isset("no-simplify"))
237 options.set_option("simplify", false);
238
239 if(cmdline.isset("stop-on-fail") ||
240 cmdline.isset("dimacs") ||
241 cmdline.isset("outfile"))
242 options.set_option("stop-on-fail", true);
243
244 if(
245 cmdline.isset("trace") || cmdline.isset("compact-trace") ||
246 cmdline.isset("stack-trace") || cmdline.isset("stop-on-fail") ||
248 !cmdline.isset("cover")))
249 {
250 options.set_option("trace", true);
251 }
252
253 if(cmdline.isset("localize-faults"))
254 options.set_option("localize-faults", true);
255
256 if(cmdline.isset("unwind"))
257 options.set_option("unwind", cmdline.get_value("unwind"));
258
259 if(cmdline.isset("depth"))
260 options.set_option("depth", cmdline.get_value("depth"));
261
262 if(cmdline.isset("debug-level"))
263 options.set_option("debug-level", cmdline.get_value("debug-level"));
264
265 if(cmdline.isset("slice-by-trace"))
266 {
267 log.error() << "--slice-by-trace has been removed" << messaget::eom;
269 }
270
271 if(cmdline.isset("unwindset"))
272 options.set_option("unwindset", cmdline.get_values("unwindset"));
273
274 // constant propagation
275 if(cmdline.isset("no-propagation"))
276 options.set_option("propagation", false);
277
278 // transform self loops to assumptions
279 options.set_option(
280 "self-loops-to-assumptions",
281 !cmdline.isset("no-self-loops-to-assumptions"));
282
283 // all checks supported by goto_check
285
286 // generate unwinding assertions
287 if(cmdline.isset("unwinding-assertions"))
288 {
289 options.set_option("unwinding-assertions", true);
290 options.set_option("paths-symex-explore-all", true);
291 }
292
293 if(cmdline.isset("partial-loops"))
294 options.set_option("partial-loops", true);
295
296 // remove unused equations
297 if(cmdline.isset("slice-formula"))
298 options.set_option("slice-formula", true);
299
300 // simplify if conditions and branches
301 if(cmdline.isset("no-simplify-if"))
302 options.set_option("simplify-if", false);
303
304 if(cmdline.isset("arrays-uf-always"))
305 options.set_option("arrays-uf", "always");
306 else if(cmdline.isset("arrays-uf-never"))
307 options.set_option("arrays-uf", "never");
308
309 if(cmdline.isset("dimacs"))
310 options.set_option("dimacs", true);
311
312 if(cmdline.isset("show-array-constraints"))
313 options.set_option("show-array-constraints", true);
314
315 if(cmdline.isset("refine-arrays"))
316 {
317 options.set_option("refine", true);
318 options.set_option("refine-arrays", true);
319 }
320
321 if(cmdline.isset("refine-arithmetic"))
322 {
323 options.set_option("refine", true);
324 options.set_option("refine-arithmetic", true);
325 }
326
327 if(cmdline.isset("refine"))
328 {
329 options.set_option("refine", true);
330 options.set_option("refine-arrays", true);
331 options.set_option("refine-arithmetic", true);
332 }
333
334 if(cmdline.isset("refine-strings"))
335 {
336 options.set_option("refine-strings", true);
337 options.set_option("string-printable", cmdline.isset("string-printable"));
338 }
339
340 if(cmdline.isset("max-node-refinement"))
341 options.set_option(
342 "max-node-refinement",
343 cmdline.get_value("max-node-refinement"));
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 // SMT Options
373
374 if(cmdline.isset("smt1"))
375 {
376 log.error() << "--smt1 is no longer supported" << messaget::eom;
378 }
379
380 if(cmdline.isset("smt2"))
381 options.set_option("smt2", true);
382
383 if(cmdline.isset("fpa"))
384 options.set_option("fpa", true);
385
386 bool solver_set=false;
387
388 if(cmdline.isset("boolector"))
389 {
390 options.set_option("boolector", true), solver_set=true;
391 options.set_option("smt2", true);
392 }
393
394 if(cmdline.isset("cprover-smt2"))
395 {
396 options.set_option("cprover-smt2", true), solver_set = true;
397 options.set_option("smt2", true);
398 }
399
400 if(cmdline.isset("mathsat"))
401 {
402 options.set_option("mathsat", true), solver_set=true;
403 options.set_option("smt2", true);
404 }
405
406 if(cmdline.isset("cvc4"))
407 {
408 options.set_option("cvc4", true), solver_set=true;
409 options.set_option("smt2", true);
410 }
411
412 if(cmdline.isset("incremental-smt2-solver"))
413 {
414 options.set_option(
415 "incremental-smt2-solver", cmdline.get_value("incremental-smt2-solver")),
416 solver_set = true;
417 }
418
419 if(cmdline.isset("external-sat-solver"))
420 {
421 options.set_option(
422 "external-sat-solver", cmdline.get_value("external-sat-solver")),
423 solver_set = true;
424 }
425
426 if(cmdline.isset("yices"))
427 {
428 options.set_option("yices", true), solver_set=true;
429 options.set_option("smt2", true);
430 }
431
432 if(cmdline.isset("z3"))
433 {
434 options.set_option("z3", true), solver_set=true;
435 options.set_option("smt2", true);
436 }
437
438 if(cmdline.isset("smt2") && !solver_set)
439 {
440 if(cmdline.isset("outfile"))
441 {
442 // outfile and no solver should give standard compliant SMT-LIB
443 options.set_option("generic", true);
444 }
445 else
446 {
447 // the default smt2 solver
448 options.set_option("z3", true);
449 }
450 }
451
452 if(cmdline.isset("write-solver-stats-to"))
453 {
454 options.set_option(
455 "write-solver-stats-to", cmdline.get_value("write-solver-stats-to"));
456 }
457
458 if(cmdline.isset("beautify"))
459 options.set_option("beautify", true);
460
461 if(cmdline.isset("no-sat-preprocessor"))
462 options.set_option("sat-preprocessor", false);
463
464 if(cmdline.isset("no-pretty-names"))
465 options.set_option("pretty-names", false);
466
467 if(cmdline.isset("outfile"))
468 options.set_option("outfile", cmdline.get_value("outfile"));
469
470 if(cmdline.isset("graphml-witness"))
471 {
472 options.set_option("graphml-witness", cmdline.get_value("graphml-witness"));
473 options.set_option("stop-on-fail", true);
474 options.set_option("trace", true);
475 }
476
477 if(cmdline.isset("symex-coverage-report"))
478 {
479 options.set_option(
480 "symex-coverage-report",
481 cmdline.get_value("symex-coverage-report"));
482 options.set_option("paths-symex-explore-all", true);
483 }
484
485 if(cmdline.isset("validate-ssa-equation"))
486 {
487 options.set_option("validate-ssa-equation", true);
488 }
489
490 if(cmdline.isset("validate-goto-model"))
491 {
492 options.set_option("validate-goto-model", true);
493 }
494
495 if(cmdline.isset("show-goto-symex-steps"))
496 options.set_option("show-goto-symex-steps", true);
497
498 if(cmdline.isset("show-points-to-sets"))
499 options.set_option("show-points-to-sets", true);
500
502
503 // Options for process_goto_program
504 options.set_option("rewrite-union", true);
505}
506
509{
510 if(cmdline.isset("version"))
511 {
512 std::cout << CBMC_VERSION << '\n';
514 }
515
516 //
517 // command line options
518 //
519
520 optionst options;
522
525
527
528 //
529 // Unwinding of transition systems is done by hw-cbmc.
530 //
531
532 if(cmdline.isset("module") ||
533 cmdline.isset("gen-interface"))
534 {
535 log.error() << "This version of CBMC has no support for "
536 " hardware modules. Please use hw-cbmc."
537 << messaget::eom;
539 }
540
541 if(cmdline.isset("show-points-to-sets"))
542 {
543 if(!cmdline.isset("json-ui") || cmdline.isset("xml-ui"))
544 {
545 log.error() << "--show-points-to-sets supports only"
546 " json output. Use --json-ui."
547 << messaget::eom;
549 }
550 }
551
552 if(cmdline.isset("show-array-constraints"))
553 {
554 if(!cmdline.isset("json-ui") || cmdline.isset("xml-ui"))
555 {
556 log.error() << "--show-array-constraints supports only"
557 " json output. Use --json-ui."
558 << messaget::eom;
560 }
561 }
562
564
565 // configure gcc, if required
567 {
568 gcc_versiont gcc_version;
569 gcc_version.get("gcc");
570 configure_gcc(gcc_version);
571 }
572
573 if(cmdline.isset("test-preprocessor"))
577
578 if(cmdline.isset("preprocess"))
579 {
580 preprocessing(options);
582 }
583
584 if(cmdline.isset("show-parse-tree"))
585 {
586 if(
587 cmdline.args.size() != 1 ||
589 {
590 log.error() << "Please give exactly one source file" << messaget::eom;
592 }
593
594 std::string filename=cmdline.args[0];
595
596 #ifdef _MSC_VER
597 std::ifstream infile(widen(filename));
598 #else
599 std::ifstream infile(filename);
600 #endif
601
602 if(!infile)
603 {
604 log.error() << "failed to open input file '" << filename << "'"
605 << messaget::eom;
607 }
608
609 std::unique_ptr<languaget> language=
611
612 if(language==nullptr)
613 {
614 log.error() << "failed to figure out type of file '" << filename << "'"
615 << messaget::eom;
617 }
618
619 language->set_language_options(options);
620 language->set_message_handler(ui_message_handler);
621
622 log.status() << "Parsing " << filename << messaget::eom;
623
624 if(language->parse(infile, filename))
625 {
626 log.error() << "PARSING ERROR" << messaget::eom;
628 }
629
630 language->show_parse(std::cout);
632 }
633
634 int get_goto_program_ret =
636
637 if(get_goto_program_ret!=-1)
638 return get_goto_program_ret;
639
640 if(cmdline.isset("show-claims") || // will go away
641 cmdline.isset("show-properties")) // use this one
642 {
645 }
646
647 if(set_properties())
649
650 if(
651 options.get_bool_option("program-only") ||
652 options.get_bool_option("show-vcc") ||
653 options.get_bool_option("show-byte-ops"))
654 {
655 if(options.get_bool_option("paths"))
656 {
659 (void)verifier();
660 }
661 else
662 {
665 (void)verifier();
666 }
667
669 }
670
671 if(
672 options.get_bool_option("dimacs") || !options.get_option("outfile").empty())
673 {
674 if(options.get_bool_option("paths"))
675 {
678 (void)verifier();
679 }
680 else
681 {
684 (void)verifier();
685 }
686
688 }
689
690 if(options.is_set("cover"))
691 {
693 verifier(options, ui_message_handler, goto_model);
694 (void)verifier();
695 verifier.report();
696
697 if(options.get_bool_option("show-test-suite"))
698 {
699 c_test_input_generatort test_generator(ui_message_handler, options);
700 test_generator(verifier.get_traces());
701 }
702
704 }
705
706 std::unique_ptr<goto_verifiert> verifier = nullptr;
707
708 if(options.is_set("incremental-loop"))
709 {
710 if(options.get_bool_option("stop-on-fail"))
711 {
712 verifier = util_make_unique<
715 }
716 else
717 {
721 }
722 }
723 else if(
724 options.get_bool_option("stop-on-fail") && options.get_bool_option("paths"))
725 {
726 verifier =
727 util_make_unique<stop_on_fail_verifiert<single_path_symex_checkert>>(
729 }
730 else if(
731 options.get_bool_option("stop-on-fail") &&
732 !options.get_bool_option("paths"))
733 {
734 if(options.get_bool_option("localize-faults"))
735 {
736 verifier =
739 }
740 else
741 {
742 verifier =
743 util_make_unique<stop_on_fail_verifiert<multi_path_symex_checkert>>(
745 }
746 }
747 else if(
748 !options.get_bool_option("stop-on-fail") &&
749 options.get_bool_option("paths"))
750 {
751 verifier = util_make_unique<
754 }
755 else if(
756 !options.get_bool_option("stop-on-fail") &&
757 !options.get_bool_option("paths"))
758 {
759 if(options.get_bool_option("localize-faults"))
760 {
761 verifier =
764 }
765 else
766 {
767 verifier = util_make_unique<
770 }
771 }
772 else
773 {
775 }
776
777 const resultt result = (*verifier)();
778 verifier->report();
779
780 return result_to_exit_code(result);
781}
782
784{
785 if(cmdline.isset("claim")) // will go away
787
788 if(cmdline.isset("property")) // use this one
790
791 return false;
792}
793
795 goto_modelt &goto_model,
796 const optionst &options,
797 const cmdlinet &cmdline,
798 ui_message_handlert &ui_message_handler)
799{
801 if(cmdline.args.empty())
802 {
803 log.error() << "Please provide a program to verify" << messaget::eom;
805 }
806
808
809 if(cmdline.isset("show-symbol-table"))
810 {
813 }
814
817
818 if(cmdline.isset("validate-goto-model"))
819 {
821 }
822
823 // show it?
824 if(cmdline.isset("show-loops"))
825 {
828 }
829
830 // show it?
831 if(
832 cmdline.isset("show-goto-functions") ||
833 cmdline.isset("list-goto-functions"))
834 {
836 goto_model, ui_message_handler, cmdline.isset("list-goto-functions"));
838 }
839
841
842 return -1; // no error, continue
843}
844
846{
847 if(cmdline.args.size() != 1)
848 {
849 log.error() << "Please provide one program to preprocess" << messaget::eom;
850 return;
851 }
852
853 std::string filename = cmdline.args[0];
854
855 std::ifstream infile(filename);
856
857 if(!infile)
858 {
859 log.error() << "failed to open input file" << messaget::eom;
860 return;
861 }
862
863 std::unique_ptr<languaget> language = get_language_from_filename(filename);
864 language->set_language_options(options);
865
866 if(language == nullptr)
867 {
868 log.error() << "failed to figure out type of file" << messaget::eom;
869 return;
870 }
871
872 language->set_message_handler(ui_message_handler);
873
874 if(language->preprocess(infile, filename, std::cout))
875 log.error() << "PREPROCESSING ERROR" << messaget::eom;
876}
877
879 goto_modelt &goto_model,
880 const optionst &options,
881 messaget &log)
882{
883 // Remove inline assembler; this needs to happen before
884 // adding the library.
886
887 // add the library
888 log.status() << "Adding CPROVER library (" << config.ansi_c.arch << ")"
889 << messaget::eom;
894
895 // Common removal of types and complex constructs
897 return true;
898
899 // ignore default/user-specified initialization
900 // of variables with static lifetime
901 if(options.get_bool_option("nondet-static"))
902 {
903 log.status() << "Adding nondeterministic initialization "
904 "of static/global variables"
905 << messaget::eom;
907 }
908
909 // add failed symbols
910 // needs to be done before pointer analysis
912
913 if(options.get_bool_option("drop-unused-functions"))
914 {
915 // Entry point will have been set before and function pointers removed
916 log.status() << "Removing unused functions" << messaget::eom;
918 }
919
920 // remove skips such that trivial GOTOs are deleted and not considered
921 // for coverage annotation:
923
924 // instrument cover goals
925 if(options.is_set("cover"))
926 {
927 const auto cover_config = get_cover_config(
930 cover_config, goto_model, log.get_message_handler()))
931 return true;
932 }
933
934 // label the assertions
935 // This must be done after adding assertions and
936 // before using the argument of the "property" option.
937 // Do not re-label after using the property slicer because
938 // this would cause the property identifiers to change.
940
941 // reachability slice?
942 if(options.get_bool_option("reachability-slice-fb"))
943 {
944 log.status() << "Performing a forwards-backwards reachability slice"
945 << messaget::eom;
946 if(options.is_set("property"))
948 goto_model, options.get_list_option("property"), true);
949 else
951 }
952
953 if(options.get_bool_option("reachability-slice"))
954 {
955 log.status() << "Performing a reachability slice" << messaget::eom;
956 if(options.is_set("property"))
957 reachability_slicer(goto_model, options.get_list_option("property"));
958 else
960 }
961
962 // full slice?
963 if(options.get_bool_option("full-slice"))
964 {
965 log.status() << "Performing a full slice" << messaget::eom;
966 if(options.is_set("property"))
967 property_slicer(goto_model, options.get_list_option("property"));
968 else
970 }
971
972 // remove any skips introduced since coverage instrumentation
974
975 return false;
976}
977
980{
981 // clang-format off
982 std::cout << '\n' << banner_string("CBMC", CBMC_VERSION) << '\n'
983 << align_center_with_border("Copyright (C) 2001-2018") << '\n'
984 << align_center_with_border("Daniel Kroening, Edmund Clarke") << '\n' // NOLINT(*)
985 << align_center_with_border("Carnegie Mellon University, Computer Science Department") << '\n' // NOLINT(*)
986 << align_center_with_border("kroening@kroening.com") << '\n' // NOLINT(*)
987 << align_center_with_border("Protected in part by U.S. patent 7,225,417") << '\n' // NOLINT(*)
988 <<
989 "\n"
990 "Usage: Purpose:\n"
991 "\n"
992 " cbmc [-?] [-h] [--help] show help\n"
993 " cbmc file.c ... source file names\n"
994 "\n"
995 "Analysis options:\n"
997 " --symex-coverage-report f generate a Cobertura XML coverage report in f\n" // NOLINT(*)
998 " --property id only check one specific property\n"
999 " --trace give a counterexample trace for failed properties\n" //NOLINT(*)
1000 " --stop-on-fail stop analysis once a failed property is detected\n" // NOLINT(*)
1001 " (implies --trace)\n"
1002 "\n"
1003 "C/C++ frontend options:\n"
1004 " --preprocess stop after preprocessing\n"
1008 "\n"
1009 "Platform options:\n"
1011 "\n"
1012 "Program representations:\n"
1013 " --show-parse-tree show parse tree\n"
1014 " --show-symbol-table show loaded symbol table\n"
1016 "\n"
1017 "Program instrumentation options:\n"
1020 " --mm MM memory consistency model for concurrent programs (default: sc)\n" // NOLINT(*)
1024 " --full-slice run full slicer (experimental)\n" // NOLINT(*)
1025 " --drop-unused-functions drop functions trivially unreachable from main function\n" // NOLINT(*)
1026 " --havoc-undefined-functions\n"
1027 " for any function that has no body, assign non-deterministic values to\n" // NOLINT(*)
1028 " any parameters passed as non-const pointers and the return value\n" // NOLINT(*)
1029 "\n"
1030 "Semantic transformations:\n"
1031 // NOLINTNEXTLINE(whitespace/line_length)
1032 " --nondet-static add nondeterministic initialization of variables with static lifetime\n"
1033 "\n"
1034 "BMC options:\n"
1035 HELP_BMC
1036 "\n"
1037 "Backend options:\n"
1039 " --dimacs generate CNF in DIMACS format\n"
1040 " --beautify beautify the counterexample (greedy heuristic)\n" // NOLINT(*)
1041 " --localize-faults localize faults (experimental)\n"
1042 " --smt2 use default SMT2 solver (Z3)\n"
1043 " --boolector use Boolector\n"
1044 " --cprover-smt2 use CPROVER SMT2 solver\n"
1045 " --cvc4 use CVC4\n"
1046 " --mathsat use MathSAT\n"
1047 " --yices use Yices\n"
1048 " --z3 use Z3\n"
1049 " --refine use refinement procedure (experimental)\n"
1050 " --incremental-smt2-solver cmd\n"
1051 " command to invoke external SMT solver for\n"
1052 " incremental solving (experimental)\n"
1053 " --external-sat-solver cmd command to invoke SAT solver process\n"
1055 " --outfile filename output formula to given file\n"
1056 " --arrays-uf-never never turn arrays into uninterpreted functions\n" // NOLINT(*)
1057 " --arrays-uf-always always turn arrays into uninterpreted functions\n" // NOLINT(*)
1058 "\n"
1059 "Other options:\n"
1060 " --version show version and exit\n"
1066 " --verbosity # verbosity level\n"
1068 " --write-solver-stats-to json-file\n"
1069 " collect the solver query complexity\n"
1070 " --show-array-constraints show array theory constraints added\n"
1071 " during post processing.\n"
1072 " Requires --json-ui.\n"
1073 "\n";
1074 // clang-format on
1075}
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, symbol_tablet &symbol_table, message_handlert &message_handler)
#define HELP_ANSI_C_LANGUAGE
Bounded Model Checking Utilities.
#define HELP_BMC
Definition: bmc_util.h:201
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
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
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:1339
struct configt::ansi_ct ansi_c
void get(const std::string &executable)
Definition: gcc_version.cpp:18
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
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
@ 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
Definition: parse_options.h:45
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...
Stops when the first failing property is found.
virtual uit get_ui() const
Definition: ui_message.h:33
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
#define HELP_CONFIG_BACKEND
Definition: config.h:96
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:32
Goto verifier for covering goals that stores traces.
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_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)
Definition: goto_check_c.h:74
#define HELP_GOTO_CHECK
Definition: goto_check_c.h:53
#define PARSE_OPTIONS_GOTO_TRACE(cmdline, options)
Definition: goto_trace.h:285
#define HELP_GOTO_TRACE
Definition: goto_trace.h:277
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.
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)
Definition: properties.cpp:143
Properties.
resultt
The result of goto verifying.
Definition: properties.h:45
void reachability_slicer(goto_modelt &goto_model, const bool include_forward_reachability)
Perform reachability slicing on goto_model, with respect to the criterion given by all properties.
#define HELP_REACHABILITY_SLICER_FB
#define HELP_REACHABILITY_SLICER
bool is_goto_binary(const std::string &filename, message_handlert &message_handler)
Read Goto Programs.
#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...
Definition: remove_asm.cpp:512
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
Definition: remove_skip.cpp:88
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.
void show_goto_functions(const namespacet &ns, ui_message_handlert &ui_message_handler, const goto_functionst &goto_functions, bool list_only)
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_tablet &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.
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
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
irep_idt arch
Definition: config.h:191
preprocessort preprocessor
Definition: config.h:233
#define HELP_TIMESTAMP
Definition: timestamper.h:14
#define HELP_FLUSH
Definition: ui_message.h:108
std::wstring widen(const char *s)
Definition: unicode.cpp:48
#define HELP_VALIDATE
const char * CBMC_VERSION
void xml_interface(cmdlinet &cmdline, message_handlert &message_handler)
Parse XML-formatted commandline options from stdin.
#define HELP_XML_INTERFACE
Definition: xml_interface.h:39