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);
621  language->set_message_handler(ui_message_handler);
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 
873  language->set_message_handler(ui_message_handler);
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 }
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.
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 ...
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:47
virtual bool isset(char option) const
Definition: cmdline.cpp:29
argst args
Definition: cmdline.h:143
const std::list< std::string > & get_values(const std::string &option) const
Definition: cmdline.cpp:108
bool set(const cmdlinet &cmdline)
Definition: config.cpp:798
std::string object_bits_info()
Definition: config.cpp:1316
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
mstreamt & status() const
Definition: message.h:414
message_handlert & get_message_handler()
Definition: message.h:184
@ M_STATISTICS
Definition: message.h:171
static eomt eom
Definition: message.h:297
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:63
#define HELP_CONFIG_PLATFORM
Definition: config.h:82
#define HELP_CONFIG_C_CPP
Definition: config.h:34
#define HELP_CONFIG_BACKEND
Definition: config.h:97
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:180
void parse_cover_options(const cmdlinet &cmdline, optionst &options)
Parses coverage-related command line options.
Definition: cover.cpp:142
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.h:70
#define HELP_GOTO_CHECK
Definition: goto_check.h:49
#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)
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:142
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:511
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:86
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:164
preprocessort preprocessor
Definition: config.h:199
#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