cprover
cbmc_parse_options.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: CBMC Command Line Option Processing
4 
5 Author: 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>
32 #include <ansi-c/cprover_library.h>
33 #include <ansi-c/gcc_version.h>
34 
35 #include <assembler/remove_asm.h>
36 
37 #include <cpp/cprover_library.h>
38 
42 #include <goto-checker/bmc_util.h>
52 
56 #include <goto-programs/loop_ids.h>
65 
66 #include <goto-instrument/cover.h>
70 
72 
74 
75 #include <langapi/mode.h>
76 
77 #include "c_test_input_generator.h"
78 
79 cbmc_parse_optionst::cbmc_parse_optionst(int argc, const char **argv)
82  argc,
83  argv,
84  std::string("CBMC ") + CBMC_VERSION)
85 {
88 }
89 
91  int argc,
92  const char **argv,
93  const std::string &extra_options)
95  CBMC_OPTIONS + extra_options,
96  argc,
97  argv,
98  std::string("CBMC ") + CBMC_VERSION)
99 {
102 }
103 
105 {
106  // Default true
107  options.set_option("built-in-assertions", true);
108  options.set_option("pretty-names", true);
109  options.set_option("propagation", true);
110  options.set_option("sat-preprocessor", true);
111  options.set_option("simple-slice", true);
112  options.set_option("simplify", true);
113  options.set_option("simplify-if", true);
114  options.set_option("show-goto-symex-steps", false);
115  options.set_option("show-points-to-sets", false);
116  options.set_option("show-array-constraints", false);
117 
118  // Other default
119  options.set_option("arrays-uf", "auto");
120  options.set_option("depth", UINT32_MAX);
121 }
122 
124 {
125  if(config.set(cmdline))
126  {
127  usage_error();
129  }
130 
133 
134  if(cmdline.isset("function"))
135  options.set_option("function", cmdline.get_value("function"));
136 
137  if(cmdline.isset("cover") && cmdline.isset("unwinding-assertions"))
138  {
139  log.error()
140  << "--cover and --unwinding-assertions must not be given together"
141  << messaget::eom;
143  }
144 
145  if(cmdline.isset("max-field-sensitivity-array-size"))
146  {
147  options.set_option(
148  "max-field-sensitivity-array-size",
149  cmdline.get_value("max-field-sensitivity-array-size"));
150  }
151 
152  if(cmdline.isset("no-array-field-sensitivity"))
153  {
154  if(cmdline.isset("max-field-sensitivity-array-size"))
155  {
156  log.error()
157  << "--no-array-field-sensitivity and --max-field-sensitivity-array-size"
158  << " must not be given together" << messaget::eom;
160  }
161  options.set_option("no-array-field-sensitivity", true);
162  }
163 
164  if(cmdline.isset("partial-loops") && cmdline.isset("unwinding-assertions"))
165  {
166  log.error()
167  << "--partial-loops and --unwinding-assertions must not be given "
168  << "together" << messaget::eom;
170  }
171 
172  if(cmdline.isset("reachability-slice") &&
173  cmdline.isset("reachability-slice-fb"))
174  {
175  log.error()
176  << "--reachability-slice and --reachability-slice-fb must not be "
177  << "given together" << messaget::eom;
179  }
180 
181  if(cmdline.isset("full-slice"))
182  options.set_option("full-slice", true);
183 
184  if(cmdline.isset("show-symex-strategies"))
185  {
187  exit(CPROVER_EXIT_SUCCESS);
188  }
189 
191 
192  if(cmdline.isset("program-only"))
193  options.set_option("program-only", true);
194 
195  if(cmdline.isset("show-byte-ops"))
196  options.set_option("show-byte-ops", true);
197 
198  if(cmdline.isset("show-vcc"))
199  options.set_option("show-vcc", true);
200 
201  if(cmdline.isset("cover"))
202  parse_cover_options(cmdline, options);
203 
204  if(cmdline.isset("mm"))
205  options.set_option("mm", cmdline.get_value("mm"));
206 
207  if(cmdline.isset("symex-complexity-limit"))
208  options.set_option(
209  "symex-complexity-limit", cmdline.get_value("symex-complexity-limit"));
210 
211  if(cmdline.isset("symex-complexity-failed-child-loops-limit"))
212  options.set_option(
213  "symex-complexity-failed-child-loops-limit",
214  cmdline.get_value("symex-complexity-failed-child-loops-limit"));
215 
216  if(cmdline.isset("property"))
217  options.set_option("property", cmdline.get_values("property"));
218 
219  if(cmdline.isset("drop-unused-functions"))
220  options.set_option("drop-unused-functions", true);
221 
222  if(cmdline.isset("havoc-undefined-functions"))
223  options.set_option("havoc-undefined-functions", true);
224 
225  if(cmdline.isset("string-abstraction"))
226  options.set_option("string-abstraction", true);
227 
228  if(cmdline.isset("reachability-slice-fb"))
229  options.set_option("reachability-slice-fb", true);
230 
231  if(cmdline.isset("reachability-slice"))
232  options.set_option("reachability-slice", true);
233 
234  if(cmdline.isset("nondet-static"))
235  options.set_option("nondet-static", true);
236 
237  if(cmdline.isset("no-simplify"))
238  options.set_option("simplify", false);
239 
240  if(cmdline.isset("stop-on-fail") ||
241  cmdline.isset("dimacs") ||
242  cmdline.isset("outfile"))
243  options.set_option("stop-on-fail", true);
244 
245  if(
246  cmdline.isset("trace") || cmdline.isset("compact-trace") ||
247  cmdline.isset("stack-trace") || cmdline.isset("stop-on-fail") ||
249  !cmdline.isset("cover")))
250  {
251  options.set_option("trace", true);
252  }
253 
254  if(cmdline.isset("localize-faults"))
255  options.set_option("localize-faults", true);
256 
257  if(cmdline.isset("unwind"))
258  options.set_option("unwind", cmdline.get_value("unwind"));
259 
260  if(cmdline.isset("depth"))
261  options.set_option("depth", cmdline.get_value("depth"));
262 
263  if(cmdline.isset("debug-level"))
264  options.set_option("debug-level", cmdline.get_value("debug-level"));
265 
266  if(cmdline.isset("slice-by-trace"))
267  {
268  log.error() << "--slice-by-trace has been removed" << messaget::eom;
270  }
271 
272  if(cmdline.isset("unwindset"))
273  options.set_option("unwindset", cmdline.get_values("unwindset"));
274 
275  // constant propagation
276  if(cmdline.isset("no-propagation"))
277  options.set_option("propagation", false);
278 
279  // transform self loops to assumptions
280  options.set_option(
281  "self-loops-to-assumptions",
282  !cmdline.isset("no-self-loops-to-assumptions"));
283 
284  // all checks supported by goto_check
286 
287  // generate unwinding assertions
288  if(cmdline.isset("unwinding-assertions"))
289  {
290  options.set_option("unwinding-assertions", true);
291  options.set_option("paths-symex-explore-all", true);
292  }
293 
294  if(cmdline.isset("partial-loops"))
295  options.set_option("partial-loops", true);
296 
297  // remove unused equations
298  if(cmdline.isset("slice-formula"))
299  options.set_option("slice-formula", true);
300 
301  // simplify if conditions and branches
302  if(cmdline.isset("no-simplify-if"))
303  options.set_option("simplify-if", false);
304 
305  if(cmdline.isset("arrays-uf-always"))
306  options.set_option("arrays-uf", "always");
307  else if(cmdline.isset("arrays-uf-never"))
308  options.set_option("arrays-uf", "never");
309 
310  if(cmdline.isset("dimacs"))
311  options.set_option("dimacs", true);
312 
313  if(cmdline.isset("show-array-constraints"))
314  options.set_option("show-array-constraints", true);
315 
316  if(cmdline.isset("refine-arrays"))
317  {
318  options.set_option("refine", true);
319  options.set_option("refine-arrays", true);
320  }
321 
322  if(cmdline.isset("refine-arithmetic"))
323  {
324  options.set_option("refine", true);
325  options.set_option("refine-arithmetic", true);
326  }
327 
328  if(cmdline.isset("refine"))
329  {
330  options.set_option("refine", true);
331  options.set_option("refine-arrays", true);
332  options.set_option("refine-arithmetic", true);
333  }
334 
335  if(cmdline.isset("refine-strings"))
336  {
337  options.set_option("refine-strings", true);
338  options.set_option("string-printable", cmdline.isset("string-printable"));
339  }
340 
341  if(cmdline.isset("max-node-refinement"))
342  options.set_option(
343  "max-node-refinement",
344  cmdline.get_value("max-node-refinement"));
345 
346  options.set_option(
347  "symex-cache-dereferences", cmdline.isset("symex-cache-dereferences"));
348 
349  if(cmdline.isset("incremental-loop"))
350  {
351  options.set_option(
352  "incremental-loop", cmdline.get_value("incremental-loop"));
353  options.set_option("refine", true);
354  options.set_option("refine-arrays", true);
355 
356  if(cmdline.isset("unwind-min"))
357  options.set_option("unwind-min", cmdline.get_value("unwind-min"));
358 
359  if(cmdline.isset("unwind-max"))
360  options.set_option("unwind-max", cmdline.get_value("unwind-max"));
361 
362  if(cmdline.isset("ignore-properties-before-unwind-min"))
363  options.set_option("ignore-properties-before-unwind-min", true);
364 
365  if(cmdline.isset("paths"))
366  {
367  log.error() << "--paths not supported with --incremental-loop"
368  << messaget::eom;
370  }
371  }
372 
373  // SMT Options
374 
375  if(cmdline.isset("smt1"))
376  {
377  log.error() << "--smt1 is no longer supported" << messaget::eom;
379  }
380 
381  if(cmdline.isset("smt2"))
382  options.set_option("smt2", true);
383 
384  if(cmdline.isset("fpa"))
385  options.set_option("fpa", true);
386 
387  bool solver_set=false;
388 
389  if(cmdline.isset("boolector"))
390  {
391  options.set_option("boolector", true), solver_set=true;
392  options.set_option("smt2", true);
393  }
394 
395  if(cmdline.isset("cprover-smt2"))
396  {
397  options.set_option("cprover-smt2", true), solver_set = true;
398  options.set_option("smt2", true);
399  }
400 
401  if(cmdline.isset("mathsat"))
402  {
403  options.set_option("mathsat", true), solver_set=true;
404  options.set_option("smt2", true);
405  }
406 
407  if(cmdline.isset("cvc4"))
408  {
409  options.set_option("cvc4", true), solver_set=true;
410  options.set_option("smt2", true);
411  }
412 
413  if(cmdline.isset("incremental-smt2-solver"))
414  {
415  options.set_option(
416  "incremental-smt2-solver", cmdline.get_value("incremental-smt2-solver")),
417  solver_set = true;
418  }
419 
420  if(cmdline.isset("external-sat-solver"))
421  {
422  options.set_option(
423  "external-sat-solver", cmdline.get_value("external-sat-solver")),
424  solver_set = true;
425  }
426 
427  if(cmdline.isset("yices"))
428  {
429  options.set_option("yices", true), solver_set=true;
430  options.set_option("smt2", true);
431  }
432 
433  if(cmdline.isset("z3"))
434  {
435  options.set_option("z3", true), solver_set=true;
436  options.set_option("smt2", true);
437  }
438 
439  if(cmdline.isset("smt2") && !solver_set)
440  {
441  if(cmdline.isset("outfile"))
442  {
443  // outfile and no solver should give standard compliant SMT-LIB
444  options.set_option("generic", true);
445  }
446  else
447  {
448  // the default smt2 solver
449  options.set_option("z3", true);
450  }
451  }
452 
453  if(cmdline.isset("write-solver-stats-to"))
454  {
455  options.set_option(
456  "write-solver-stats-to", cmdline.get_value("write-solver-stats-to"));
457  }
458 
459  if(cmdline.isset("beautify"))
460  options.set_option("beautify", true);
461 
462  if(cmdline.isset("no-sat-preprocessor"))
463  options.set_option("sat-preprocessor", false);
464 
465  if(cmdline.isset("no-pretty-names"))
466  options.set_option("pretty-names", false);
467 
468  if(cmdline.isset("outfile"))
469  options.set_option("outfile", cmdline.get_value("outfile"));
470 
471  if(cmdline.isset("graphml-witness"))
472  {
473  options.set_option("graphml-witness", cmdline.get_value("graphml-witness"));
474  options.set_option("stop-on-fail", true);
475  options.set_option("trace", true);
476  }
477 
478  if(cmdline.isset("symex-coverage-report"))
479  {
480  options.set_option(
481  "symex-coverage-report",
482  cmdline.get_value("symex-coverage-report"));
483  options.set_option("paths-symex-explore-all", true);
484  }
485 
486  if(cmdline.isset("validate-ssa-equation"))
487  {
488  options.set_option("validate-ssa-equation", true);
489  }
490 
491  if(cmdline.isset("validate-goto-model"))
492  {
493  options.set_option("validate-goto-model", true);
494  }
495 
496  if(cmdline.isset("show-goto-symex-steps"))
497  options.set_option("show-goto-symex-steps", true);
498 
499  if(cmdline.isset("show-points-to-sets"))
500  options.set_option("show-points-to-sets", true);
501 
503 
504  // Options for process_goto_program
505  options.set_option("rewrite-union", true);
506 }
507 
510 {
511  if(cmdline.isset("version"))
512  {
513  std::cout << CBMC_VERSION << '\n';
514  return CPROVER_EXIT_SUCCESS;
515  }
516 
517  //
518  // command line options
519  //
520 
521  optionst options;
522  get_command_line_options(options);
523 
526 
528 
529  //
530  // Unwinding of transition systems is done by hw-cbmc.
531  //
532 
533  if(cmdline.isset("module") ||
534  cmdline.isset("gen-interface"))
535  {
536  log.error() << "This version of CBMC has no support for "
537  " hardware modules. Please use hw-cbmc."
538  << messaget::eom;
540  }
541 
542  if(cmdline.isset("show-points-to-sets"))
543  {
544  if(!cmdline.isset("json-ui") || cmdline.isset("xml-ui"))
545  {
546  log.error() << "--show-points-to-sets supports only"
547  " json output. Use --json-ui."
548  << messaget::eom;
550  }
551  }
552 
553  if(cmdline.isset("show-array-constraints"))
554  {
555  if(!cmdline.isset("json-ui") || cmdline.isset("xml-ui"))
556  {
557  log.error() << "--show-array-constraints supports only"
558  " json output. Use --json-ui."
559  << messaget::eom;
561  }
562  }
563 
565 
566  // configure gcc, if required
568  {
569  gcc_versiont gcc_version;
570  gcc_version.get("gcc");
571  configure_gcc(gcc_version);
572  }
573 
574  if(cmdline.isset("test-preprocessor"))
578 
579  if(cmdline.isset("preprocess"))
580  {
581  preprocessing(options);
582  return CPROVER_EXIT_SUCCESS;
583  }
584 
585  if(cmdline.isset("show-parse-tree"))
586  {
587  if(
588  cmdline.args.size() != 1 ||
590  {
591  log.error() << "Please give exactly one source file" << messaget::eom;
593  }
594 
595  std::string filename=cmdline.args[0];
596 
597  #ifdef _MSC_VER
598  std::ifstream infile(widen(filename));
599  #else
600  std::ifstream infile(filename);
601  #endif
602 
603  if(!infile)
604  {
605  log.error() << "failed to open input file '" << filename << "'"
606  << messaget::eom;
608  }
609 
610  std::unique_ptr<languaget> language=
611  get_language_from_filename(filename);
612 
613  if(language==nullptr)
614  {
615  log.error() << "failed to figure out type of file '" << filename << "'"
616  << messaget::eom;
618  }
619 
620  language->set_language_options(options);
622 
623  log.status() << "Parsing " << filename << messaget::eom;
624 
625  if(language->parse(infile, filename))
626  {
627  log.error() << "PARSING ERROR" << messaget::eom;
629  }
630 
631  language->show_parse(std::cout);
632  return CPROVER_EXIT_SUCCESS;
633  }
634 
635  int get_goto_program_ret =
637 
638  if(get_goto_program_ret!=-1)
639  return get_goto_program_ret;
640 
641  if(cmdline.isset("show-claims") || // will go away
642  cmdline.isset("show-properties")) // use this one
643  {
645  return CPROVER_EXIT_SUCCESS;
646  }
647 
648  if(set_properties())
650 
651  if(
652  options.get_bool_option("program-only") ||
653  options.get_bool_option("show-vcc") ||
654  options.get_bool_option("show-byte-ops"))
655  {
656  if(options.get_bool_option("paths"))
657  {
659  options, ui_message_handler, goto_model);
660  (void)verifier();
661  }
662  else
663  {
665  options, ui_message_handler, goto_model);
666  (void)verifier();
667  }
668 
669  return CPROVER_EXIT_SUCCESS;
670  }
671 
672  if(
673  options.get_bool_option("dimacs") || !options.get_option("outfile").empty())
674  {
675  if(options.get_bool_option("paths"))
676  {
678  options, ui_message_handler, goto_model);
679  (void)verifier();
680  }
681  else
682  {
684  options, ui_message_handler, goto_model);
685  (void)verifier();
686  }
687 
688  return CPROVER_EXIT_SUCCESS;
689  }
690 
691  if(options.is_set("cover"))
692  {
694  verifier(options, ui_message_handler, goto_model);
695  (void)verifier();
696  verifier.report();
697 
698  if(options.get_bool_option("show-test-suite"))
699  {
700  c_test_input_generatort test_generator(ui_message_handler, options);
701  test_generator(verifier.get_traces());
702  }
703 
704  return CPROVER_EXIT_SUCCESS;
705  }
706 
707  std::unique_ptr<goto_verifiert> verifier = nullptr;
708 
709  if(options.is_set("incremental-loop"))
710  {
711  if(options.get_bool_option("stop-on-fail"))
712  {
713  verifier = util_make_unique<
715  options, ui_message_handler, goto_model);
716  }
717  else
718  {
721  options, ui_message_handler, goto_model);
722  }
723  }
724  else if(
725  options.get_bool_option("stop-on-fail") && options.get_bool_option("paths"))
726  {
727  verifier =
728  util_make_unique<stop_on_fail_verifiert<single_path_symex_checkert>>(
729  options, ui_message_handler, goto_model);
730  }
731  else if(
732  options.get_bool_option("stop-on-fail") &&
733  !options.get_bool_option("paths"))
734  {
735  if(options.get_bool_option("localize-faults"))
736  {
737  verifier =
740  }
741  else
742  {
743  verifier =
744  util_make_unique<stop_on_fail_verifiert<multi_path_symex_checkert>>(
745  options, ui_message_handler, goto_model);
746  }
747  }
748  else if(
749  !options.get_bool_option("stop-on-fail") &&
750  options.get_bool_option("paths"))
751  {
752  verifier = util_make_unique<
754  options, ui_message_handler, goto_model);
755  }
756  else if(
757  !options.get_bool_option("stop-on-fail") &&
758  !options.get_bool_option("paths"))
759  {
760  if(options.get_bool_option("localize-faults"))
761  {
762  verifier =
765  }
766  else
767  {
768  verifier = util_make_unique<
770  options, ui_message_handler, goto_model);
771  }
772  }
773  else
774  {
775  UNREACHABLE;
776  }
777 
778  const resultt result = (*verifier)();
779  verifier->report();
780 
781  return result_to_exit_code(result);
782 }
783 
785 {
786  if(cmdline.isset("claim")) // will go away
788 
789  if(cmdline.isset("property")) // use this one
791 
792  return false;
793 }
794 
796  goto_modelt &goto_model,
797  const optionst &options,
798  const cmdlinet &cmdline,
799  ui_message_handlert &ui_message_handler)
800 {
802  if(cmdline.args.empty())
803  {
804  log.error() << "Please provide a program to verify" << messaget::eom;
806  }
807 
809 
810  if(cmdline.isset("show-symbol-table"))
811  {
813  return CPROVER_EXIT_SUCCESS;
814  }
815 
818 
819  if(cmdline.isset("validate-goto-model"))
820  {
822  }
823 
824  // show it?
825  if(cmdline.isset("show-loops"))
826  {
828  return CPROVER_EXIT_SUCCESS;
829  }
830 
831  // show it?
832  if(
833  cmdline.isset("show-goto-functions") ||
834  cmdline.isset("list-goto-functions"))
835  {
837  goto_model, ui_message_handler, cmdline.isset("list-goto-functions"));
838  return CPROVER_EXIT_SUCCESS;
839  }
840 
842 
843  return -1; // no error, continue
844 }
845 
847 {
848  if(cmdline.args.size() != 1)
849  {
850  log.error() << "Please provide one program to preprocess" << messaget::eom;
851  return;
852  }
853 
854  std::string filename = cmdline.args[0];
855 
856  std::ifstream infile(filename);
857 
858  if(!infile)
859  {
860  log.error() << "failed to open input file" << messaget::eom;
861  return;
862  }
863 
864  std::unique_ptr<languaget> language = get_language_from_filename(filename);
865  language->set_language_options(options);
866 
867  if(language == nullptr)
868  {
869  log.error() << "failed to figure out type of file" << messaget::eom;
870  return;
871  }
872 
874 
875  if(language->preprocess(infile, filename, std::cout))
876  log.error() << "PREPROCESSING ERROR" << messaget::eom;
877 }
878 
880  goto_modelt &goto_model,
881  const optionst &options,
882  messaget &log)
883 {
884  // Remove inline assembler; this needs to happen before
885  // adding the library.
887 
888  // add the library
889  log.status() << "Adding CPROVER library (" << config.ansi_c.arch << ")"
890  << messaget::eom;
895 
897 
898  // Common removal of types and complex constructs
899  if(::process_goto_program(goto_model, options, log))
900  return true;
901 
902  // ignore default/user-specified initialization
903  // of variables with static lifetime
904  if(options.get_bool_option("nondet-static"))
905  {
906  log.status() << "Adding nondeterministic initialization "
907  "of static/global variables"
908  << messaget::eom;
910  }
911 
912  // add failed symbols
913  // needs to be done before pointer analysis
915 
916  if(options.get_bool_option("drop-unused-functions"))
917  {
918  // Entry point will have been set before and function pointers removed
919  log.status() << "Removing unused functions" << messaget::eom;
921  }
922 
923  // remove skips such that trivial GOTOs are deleted and not considered
924  // for coverage annotation:
926 
927  // instrument cover goals
928  if(options.is_set("cover"))
929  {
930  const auto cover_config = get_cover_config(
933  cover_config, goto_model, log.get_message_handler()))
934  return true;
935  }
936 
937  // label the assertions
938  // This must be done after adding assertions and
939  // before using the argument of the "property" option.
940  // Do not re-label after using the property slicer because
941  // this would cause the property identifiers to change.
943 
944  // reachability slice?
945  if(options.get_bool_option("reachability-slice-fb"))
946  {
947  log.status() << "Performing a forwards-backwards reachability slice"
948  << messaget::eom;
949  if(options.is_set("property"))
951  goto_model, options.get_list_option("property"), true);
952  else
954  }
955 
956  if(options.get_bool_option("reachability-slice"))
957  {
958  log.status() << "Performing a reachability slice" << messaget::eom;
959  if(options.is_set("property"))
960  reachability_slicer(goto_model, options.get_list_option("property"));
961  else
963  }
964 
965  // full slice?
966  if(options.get_bool_option("full-slice"))
967  {
968  log.status() << "Performing a full slice" << messaget::eom;
969  if(options.is_set("property"))
970  property_slicer(goto_model, options.get_list_option("property"));
971  else
973  }
974 
975  // remove any skips introduced since coverage instrumentation
977 
978  return false;
979 }
980 
983 {
984  // clang-format off
985  std::cout << '\n' << banner_string("CBMC", CBMC_VERSION) << '\n'
986  << align_center_with_border("Copyright (C) 2001-2018") << '\n'
987  << align_center_with_border("Daniel Kroening, Edmund Clarke") << '\n' // NOLINT(*)
988  << align_center_with_border("Carnegie Mellon University, Computer Science Department") << '\n' // NOLINT(*)
989  << align_center_with_border("kroening@kroening.com") << '\n' // NOLINT(*)
990  << align_center_with_border("Protected in part by U.S. patent 7,225,417") << '\n' // NOLINT(*)
991  <<
992  "\n"
993  "Usage: Purpose:\n"
994  "\n"
995  " cbmc [-?] [-h] [--help] show help\n"
996  " cbmc file.c ... source file names\n"
997  "\n"
998  "Analysis options:\n"
1000  " --symex-coverage-report f generate a Cobertura XML coverage report in f\n" // NOLINT(*)
1001  " --property id only check one specific property\n"
1002  " --trace give a counterexample trace for failed properties\n" //NOLINT(*)
1003  " --stop-on-fail stop analysis once a failed property is detected\n" // NOLINT(*)
1004  " (implies --trace)\n"
1005  "\n"
1006  "C/C++ frontend options:\n"
1007  " --preprocess stop after preprocessing\n"
1011  "\n"
1012  "Platform options:\n"
1014  "\n"
1015  "Program representations:\n"
1016  " --show-parse-tree show parse tree\n"
1017  " --show-symbol-table show loaded symbol table\n"
1019  "\n"
1020  "Program instrumentation options:\n"
1022  HELP_COVER
1023  " --mm MM memory consistency model for concurrent programs (default: sc)\n" // NOLINT(*)
1027  " --full-slice run full slicer (experimental)\n" // NOLINT(*)
1028  " --drop-unused-functions drop functions trivially unreachable from main function\n" // NOLINT(*)
1029  " --havoc-undefined-functions\n"
1030  " for any function that has no body, assign non-deterministic values to\n" // NOLINT(*)
1031  " any parameters passed as non-const pointers and the return value\n" // NOLINT(*)
1032  "\n"
1033  "Semantic transformations:\n"
1034  // NOLINTNEXTLINE(whitespace/line_length)
1035  " --nondet-static add nondeterministic initialization of variables with static lifetime\n"
1036  "\n"
1037  "BMC options:\n"
1038  HELP_BMC
1039  "\n"
1040  "Backend options:\n"
1042  " --dimacs generate CNF in DIMACS format\n"
1043  " --beautify beautify the counterexample (greedy heuristic)\n" // NOLINT(*)
1044  " --localize-faults localize faults (experimental)\n"
1045  " --smt2 use default SMT2 solver (Z3)\n"
1046  " --boolector use Boolector\n"
1047  " --cprover-smt2 use CPROVER SMT2 solver\n"
1048  " --cvc4 use CVC4\n"
1049  " --mathsat use MathSAT\n"
1050  " --yices use Yices\n"
1051  " --z3 use Z3\n"
1052  " --refine use refinement procedure (experimental)\n"
1053  " --incremental-smt2-solver cmd\n"
1054  " command to invoke external SMT solver for\n"
1055  " incremental solving (experimental)\n"
1056  " --external-sat-solver cmd command to invoke SAT solver process\n"
1058  " --outfile filename output formula to given file\n"
1059  " --arrays-uf-never never turn arrays into uninterpreted functions\n" // NOLINT(*)
1060  " --arrays-uf-always always turn arrays into uninterpreted functions\n" // NOLINT(*)
1061  "\n"
1062  "Other options:\n"
1063  " --version show version and exit\n"
1068  HELP_FLUSH
1069  " --verbosity # verbosity level\n"
1071  " --write-solver-stats-to json-file\n"
1072  " collect the solver query complexity\n"
1073  " --show-array-constraints show array theory constraints added\n"
1074  " during post processing.\n"
1075  " Requires --json-ui.\n"
1076  "\n";
1077  // clang-format on
1078 }
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
cprover_library.h
cmdlinet::args
argst args
Definition: cmdline.h:143
cbmc_parse_optionst::doit
virtual int doit() override
invoke main modules
Definition: cbmc_parse_options.cpp:509
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
cover.h
Coverage Instrumentation.
HELP_REACHABILITY_SLICER
#define HELP_REACHABILITY_SLICER
Definition: reachability_slicer.h:43
HELP_BMC
#define HELP_BMC
Definition: bmc_util.h:201
HELP_SHOW_GOTO_FUNCTIONS
#define HELP_SHOW_GOTO_FUNCTIONS
Definition: show_goto_functions.h:25
languaget::show_parse
virtual void show_parse(std::ostream &out)=0
configt::object_bits_info
std::string object_bits_info()
Definition: config.cpp:1316
gcc_versiont::get
void get(const std::string &executable)
Definition: gcc_version.cpp:18
PARSE_OPTIONS_GOTO_CHECK
#define PARSE_OPTIONS_GOTO_CHECK(cmdline, options)
Definition: goto_check.h:70
add_malloc_may_fail_variable_initializations.h
HELP_GOTO_TRACE
#define HELP_GOTO_TRACE
Definition: goto_trace.h:277
parse_options_baset::ui_message_handler
ui_message_handlert ui_message_handler
Definition: parse_options.h:45
cbmc_parse_optionst::goto_model
goto_modelt goto_model
Definition: cbmc_parse_options.h:115
cbmc_parse_optionst::get_goto_program
static int get_goto_program(goto_modelt &, const optionst &, const cmdlinet &, ui_message_handlert &)
Definition: cbmc_parse_options.cpp:795
parse_options_baset
Definition: parse_options.h:20
single_loop_incremental_symex_checkert
Performs a multi-path symbolic execution using goto-symex that incrementally unwinds a given loop and...
Definition: single_loop_incremental_symex_checker.h:32
ui_message_handlert
Definition: ui_message.h:22
parse_c_object_factory_options
void parse_c_object_factory_options(const cmdlinet &cmdline, optionst &options)
Parse the c object factory parameters from a given command line.
Definition: c_object_factory_parameters.cpp:11
resultt
resultt
The result of goto verifying.
Definition: properties.h:45
cmdlinet::isset
virtual bool isset(char option) const
Definition: cmdline.cpp:29
stop_on_fail_verifiert
Stops when the first failing property is found.
Definition: stop_on_fail_verifier.h:23
optionst
Definition: options.h:23
gcc_version.h
all_properties_verifiert
Definition: all_properties_verifier.h:23
optionst::get_option
const std::string get_option(const std::string &option) const
Definition: options.cpp:67
messaget::M_STATISTICS
@ M_STATISTICS
Definition: message.h:171
messaget::status
mstreamt & status() const
Definition: message.h:414
multi_path_symex_only_checker.h
Goto Checker using Multi-Path Symbolic Execution only (no SAT solving)
show_properties
void show_properties(const namespacet &ns, const irep_idt &identifier, message_handlert &message_handler, ui_message_handlert::uit ui, const goto_programt &goto_program)
Definition: show_properties.cpp:44
HELP_FUNCTIONS
#define HELP_FUNCTIONS
Definition: rebuild_goto_start_function.h:27
remove_skip
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:86
cover_goals_verifier_with_trace_storaget::get_traces
const goto_trace_storaget & get_traces() const
Definition: cover_goals_verifier_with_trace_storage.h:64
HELP_CONFIG_PLATFORM
#define HELP_CONFIG_PLATFORM
Definition: config.h:82
invariant.h
remove_asm.h
Remove 'asm' statements by compiling them into suitable standard goto program instructions.
reachability_slicer
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.
Definition: reachability_slicer.cpp:367
configure_gcc
void configure_gcc(const gcc_versiont &gcc_version)
Definition: gcc_version.cpp:145
c_preprocess.h
goto_modelt
Definition: goto_model.h:26
show_goto_functions.h
Show the goto functions.
mode.h
show_loop_ids
void show_loop_ids(ui_message_handlert::uit ui, const goto_modelt &goto_model)
Definition: loop_ids.cpp:21
all_properties_verifier.h
Goto Verifier for Verifying all Properties.
HELP_COVER
#define HELP_COVER
Definition: cover.h:32
optionst::set_option
void set_option(const std::string &option, const bool value)
Definition: options.cpp:28
parse_options_baset::log_version_and_architecture
void log_version_and_architecture(const std::string &front_end)
Write version and system architecture to log.status().
Definition: parse_options.cpp:152
messaget::eom
static eomt eom
Definition: message.h:297
instrument_cover_goals
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
show_symbol_table
void show_symbol_table(const symbol_tablet &symbol_table, ui_message_handlert &ui)
Definition: show_symbol_table.cpp:242
configt::ansi_c
struct configt::ansi_ct ansi_c
version.h
remove_unused_functions
void remove_unused_functions(goto_modelt &goto_model, message_handlert &message_handler)
Definition: remove_unused_functions.cpp:18
cbmc_parse_optionst::cbmc_parse_optionst
cbmc_parse_optionst(int argc, const char **argv)
Definition: cbmc_parse_options.cpp:79
nondet_static.h
Nondeterministically initializes global scope variables, except for constants (such as string literal...
HELP_REACHABILITY_SLICER_FB
#define HELP_REACHABILITY_SLICER_FB
Definition: reachability_slicer.h:50
stop_on_fail_verifier_with_fault_localization.h
Goto Verifier for stopping at the first failing property and localizing the fault.
label_properties
void label_properties(goto_modelt &goto_model)
Definition: set_properties.cpp:45
path_storage.h
Storage of symbolic execution paths to resume.
languaget::set_language_options
virtual void set_language_options(const optionst &)
Set language-specific options.
Definition: language.h:41
nondet_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.
Definition: nondet_static.cpp:79
parse_path_strategy_options
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.
Definition: path_storage.cpp:137
HELP_JSON_INTERFACE
#define HELP_JSON_INTERFACE
Definition: json_interface.h:45
ui_message_handlert::get_ui
virtual uit get_ui() const
Definition: ui_message.h:33
parse_options_baset::usage_error
virtual void usage_error()
Definition: parse_options.cpp:49
util_make_unique
std::unique_ptr< T > util_make_unique(Ts &&... ts)
Definition: make_unique.h:19
bmc_util.h
Bounded Model Checking Utilities.
set_properties.h
Set the properties to check.
get_cover_config
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:180
full_slicer
void full_slicer(goto_functionst &goto_functions, const namespacet &ns, const slicing_criteriont &criterion)
Definition: full_slicer.cpp:348
c_test_input_generator.h
Test Input Generator for C.
get_language_from_filename
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
cmdlinet
Definition: cmdline.h:21
CBMC_VERSION
const char * CBMC_VERSION
cover_goals_verifier_with_trace_storage.h
Goto verifier for covering goals that stores traces.
HELP_CONFIG_C_CPP
#define HELP_CONFIG_C_CPP
Definition: config.h:34
make_unique.h
messaget::error
mstreamt & error() const
Definition: message.h:399
cover_goals_verifier_with_trace_storaget
Definition: cover_goals_verifier_with_trace_storage.h:25
multi_path_symex_checkert
Performs a multi-path symbolic execution using goto-symex and calls a SAT/SMT solver to check the sta...
Definition: multi_path_symex_checker.h:29
all_properties_verifier_with_trace_storage.h
Goto verifier for verifying all properties that stores traces.
initialize_goto_model.h
Initialize a Goto Program.
banner_string
std::string banner_string(const std::string &front_end, const std::string &version)
Definition: parse_options.cpp:174
c_test_input_generatort
Definition: c_test_input_generator.h:51
cbmc_parse_options.h
CBMC Command Line Option Processing.
cbmc_parse_optionst::get_command_line_options
void get_command_line_options(optionst &)
Definition: cbmc_parse_options.cpp:123
configt::ansi_ct::preprocessor
preprocessort preprocessor
Definition: config.h:199
optionst::is_set
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
property_slicer
void property_slicer(goto_functionst &goto_functions, const namespacet &ns, const std::list< std::string > &properties)
Definition: full_slicer.cpp:371
show_properties.h
Show the properties.
multi_path_symex_checker.h
Goto Checker using Multi-Path Symbolic Execution.
cmdlinet::get_value
std::string get_value(char option) const
Definition: cmdline.cpp:47
show_symbol_table.h
Show the symbol table.
languaget::parse
virtual bool parse(std::istream &instream, const std::string &path)=0
CPROVER_EXIT_PREPROCESSOR_TEST_FAILED
#define CPROVER_EXIT_PREPROCESSOR_TEST_FAILED
Failure of the test-preprocessor method.
Definition: exit_codes.h:59
language.h
Abstract interface to support a programming language.
messaget::set_message_handler
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:179
HELP_SHOW_PROPERTIES
#define HELP_SHOW_PROPERTIES
Definition: show_properties.h:30
all_properties_verifier_with_trace_storaget
Definition: all_properties_verifier_with_trace_storage.h:25
cbmc_parse_optionst::process_goto_program
static bool process_goto_program(goto_modelt &, const optionst &, messaget &)
Definition: cbmc_parse_options.cpp:879
single_path_symex_checker.h
Goto Checker using Single Path Symbolic Execution.
CPROVER_EXIT_SET_PROPERTIES_FAILED
#define CPROVER_EXIT_SET_PROPERTIES_FAILED
Failure to identify the properties to verify.
Definition: exit_codes.h:55
xml_interface
void xml_interface(cmdlinet &cmdline, message_handlert &message_handler)
Parse XML-formatted commandline options from stdin.
Definition: xml_interface.cpp:47
configt::ansi_ct::arch
irep_idt arch
Definition: config.h:164
show_goto_functions
void show_goto_functions(const namespacet &ns, ui_message_handlert &ui_message_handler, const goto_functionst &goto_functions, bool list_only)
Definition: show_goto_functions.cpp:20
HELP_CONFIG_LIBRARY
#define HELP_CONFIG_LIBRARY
Definition: config.h:63
json_interface
void json_interface(cmdlinet &cmdline, message_handlert &message_handler)
Parses the JSON-formatted command line from stdin.
Definition: json_interface.cpp:88
parse_cover_options
void parse_cover_options(const cmdlinet &cmdline, optionst &options)
Parses coverage-related command line options.
Definition: cover.cpp:142
cbmc_parse_optionst::set_properties
bool set_properties()
Definition: cbmc_parse_options.cpp:784
HELP_STRING_REFINEMENT_CBMC
#define HELP_STRING_REFINEMENT_CBMC
Definition: string_refinement.h:57
widen
std::wstring widen(const char *s)
Definition: unicode.cpp:48
read_goto_binary.h
Read Goto Programs.
all_properties_verifier_with_fault_localization.h
Goto verifier for verifying all properties that stores traces and localizes faults.
CPROVER_EXIT_INCORRECT_TASK
#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
full_slicer.h
Slicing.
configt::ansi_ct::preprocessort::GCC
@ GCC
HELP_ANSI_C_LANGUAGE
#define HELP_ANSI_C_LANGUAGE
Definition: ansi_c_language.h:27
add_malloc_may_fail_variable_initializations
void add_malloc_may_fail_variable_initializations(goto_modelt &goto_model)
Some variables have different initial values based on what flags are being passed to cbmc; since the ...
Definition: add_malloc_may_fail_variable_initializations.cpp:24
goto_verifiert::report
virtual void report()=0
Report results.
remove_unused_functions.h
Unused function removal.
config
configt config
Definition: config.cpp:25
gcc_versiont
Definition: gcc_version.h:20
parse_options_baset::log
messaget log
Definition: parse_options.h:46
messaget::get_message_handler
message_handlert & get_message_handler()
Definition: message.h:184
result_to_exit_code
int result_to_exit_code(resultt result)
Definition: properties.cpp:142
ui_message_handlert::uit::PLAIN
@ PLAIN
stop_on_fail_verifier.h
Goto Verifier for stopping at the first failing property.
HELP_GOTO_CHECK
#define HELP_GOTO_CHECK
Definition: goto_check.h:49
cprover_c_library_factory
void cprover_c_library_factory(const std::set< irep_idt > &functions, symbol_tablet &symbol_table, message_handlert &message_handler)
Definition: cprover_library.cpp:80
configt::set
bool set(const cmdlinet &cmdline)
Definition: config.cpp:798
exit_codes.h
Document and give macros for the exit codes of CPROVER binaries.
optionst::get_bool_option
bool get_bool_option(const std::string &option) const
Definition: options.cpp:44
CPROVER_EXIT_USAGE_ERROR
#define CPROVER_EXIT_USAGE_ERROR
A usage error is returned when the command line is invalid or conflicting.
Definition: exit_codes.h:33
cbmc_parse_optionst::help
virtual void help() override
display command line help
Definition: cbmc_parse_options.cpp:982
remove_asm
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:511
unicode.h
is_goto_binary
bool is_goto_binary(const std::string &filename, message_handlert &message_handler)
Definition: read_goto_binary.cpp:191
show_path_strategies
std::string show_path_strategies()
suitable for displaying as a front-end help message
Definition: path_storage.cpp:111
config.h
goto_modelt::validate
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
languaget::preprocess
virtual bool preprocess(std::istream &instream, const std::string &path, std::ostream &outstream)
Definition: language.h:47
loop_ids.h
Loop IDs.
reachability_slicer.h
Slicing.
PARSE_OPTIONS_GOTO_TRACE
#define PARSE_OPTIONS_GOTO_TRACE(cmdline, options)
Definition: goto_trace.h:285
HELP_CONFIG_BACKEND
#define HELP_CONFIG_BACKEND
Definition: config.h:97
single_loop_incremental_symex_checker.h
Goto Checker using multi-path symbolic execution with incremental unwinding of a specified loop.
stop_on_fail_verifier_with_fault_localizationt
Stops when the first failing property is found and localizes the fault Requires an incremental goto c...
Definition: stop_on_fail_verifier_with_fault_localization.h:26
add_failed_symbols.h
Pointer Dereferencing.
CPROVER_EXIT_INTERNAL_ERROR
#define CPROVER_EXIT_INTERNAL_ERROR
An error has been encountered during processing the requested analysis.
Definition: exit_codes.h:45
properties.h
Properties.
initialize_goto_model
goto_modelt initialize_goto_model(const std::vector< std::string > &files, message_handlert &message_handler, const optionst &options)
Definition: initialize_goto_model.cpp:60
add_failed_symbols
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....
Definition: add_failed_symbols.cpp:77
CPROVER_EXIT_SUCCESS
#define CPROVER_EXIT_SUCCESS
Success indicates the required analysis has been performed without error.
Definition: exit_codes.h:16
cbmc_parse_optionst::register_languages
void register_languages() override
Definition: cbmc_languages.cpp:25
messaget::eval_verbosity
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
remove_skip.h
Program Transformation.
cbmc_parse_optionst::set_default_options
static void set_default_options(optionst &)
Set the options that have default values.
Definition: cbmc_parse_options.cpp:104
all_properties_verifier_with_fault_localizationt
Requires an incremental goto checker that is a goto_trace_providert and fault_localization_providert.
Definition: all_properties_verifier_with_fault_localization.h:28
cmdlinet::get_values
const std::list< std::string > & get_values(const std::string &option) const
Definition: cmdline.cpp:108
cover_goals_verifier_with_trace_storaget::report
void report() override
Report results.
Definition: cover_goals_verifier_with_trace_storage.h:59
parse_options_baset::cmdline
cmdlinet cmdline
Definition: parse_options.h:28
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
single_path_symex_only_checker.h
Goto Checker using Single Path Symbolic Execution only.
align_center_with_border
std::string align_center_with_border(const std::string &text)
Utility for displaying help centered messages borderered by "* *".
Definition: parse_options.cpp:161
optionst::get_list_option
const value_listt & get_list_option(const std::string &option) const
Definition: options.cpp:80
cprover_library.h
HELP_XML_INTERFACE
#define HELP_XML_INTERFACE
Definition: xml_interface.h:39
process_goto_program.h
HELP_TIMESTAMP
#define HELP_TIMESTAMP
Definition: timestamper.h:14
HELP_FLUSH
#define HELP_FLUSH
Definition: ui_message.h:108
CBMC_OPTIONS
#define CBMC_OPTIONS
Definition: cbmc_parse_options.h:41
cbmc_parse_optionst::preprocessing
void preprocessing(const optionst &)
Definition: cbmc_parse_options.cpp:846
cprover_cpp_library_factory
void cprover_cpp_library_factory(const std::set< irep_idt > &functions, symbol_tablet &symbol_table, message_handlert &message_handler)
Definition: cprover_library.cpp:38
test_c_preprocessor
bool test_c_preprocessor(message_handlert &message_handler)
Definition: c_preprocess.cpp:749
HELP_VALIDATE
#define HELP_VALIDATE
Definition: validation_interface.h:16