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 <fstream>
15 #include <cstdlib> // exit()
16 #include <iostream>
17 #include <memory>
18 
19 #include <util/config.h>
20 #include <util/exception_utils.h>
21 #include <util/exit_codes.h>
22 #include <util/invariant.h>
23 #include <util/make_unique.h>
24 #include <util/unicode.h>
25 #include <util/version.h>
26 
27 #include <langapi/language.h>
28 
29 #include <ansi-c/c_preprocess.h>
30 #include <ansi-c/cprover_library.h>
31 #include <ansi-c/gcc_version.h>
32 
33 #include <assembler/remove_asm.h>
34 
35 #include <cpp/cprover_library.h>
36 
40 #include <goto-checker/bmc_util.h>
50 
55 #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 }
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  {
186  exit(CPROVER_EXIT_SUCCESS);
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"))
201  parse_cover_options(cmdline, options);
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  if(cmdline.isset("incremental-loop"))
346  {
347  options.set_option(
348  "incremental-loop", cmdline.get_value("incremental-loop"));
349  options.set_option("refine", true);
350  options.set_option("refine-arrays", true);
351 
352  if(cmdline.isset("unwind-min"))
353  options.set_option("unwind-min", cmdline.get_value("unwind-min"));
354 
355  if(cmdline.isset("unwind-max"))
356  options.set_option("unwind-max", cmdline.get_value("unwind-max"));
357 
358  if(cmdline.isset("ignore-properties-before-unwind-min"))
359  options.set_option("ignore-properties-before-unwind-min", true);
360 
361  if(cmdline.isset("paths"))
362  {
363  log.error() << "--paths not supported with --incremental-loop"
364  << messaget::eom;
366  }
367  }
368 
369  // SMT Options
370 
371  if(cmdline.isset("smt1"))
372  {
373  log.error() << "--smt1 is no longer supported" << messaget::eom;
375  }
376 
377  if(cmdline.isset("smt2"))
378  options.set_option("smt2", true);
379 
380  if(cmdline.isset("fpa"))
381  options.set_option("fpa", true);
382 
383  bool solver_set=false;
384 
385  if(cmdline.isset("boolector"))
386  {
387  options.set_option("boolector", true), solver_set=true;
388  options.set_option("smt2", true);
389  }
390 
391  if(cmdline.isset("cprover-smt2"))
392  {
393  options.set_option("cprover-smt2", true), solver_set = true;
394  options.set_option("smt2", true);
395  }
396 
397  if(cmdline.isset("mathsat"))
398  {
399  options.set_option("mathsat", true), solver_set=true;
400  options.set_option("smt2", true);
401  }
402 
403  if(cmdline.isset("cvc4"))
404  {
405  options.set_option("cvc4", true), solver_set=true;
406  options.set_option("smt2", true);
407  }
408 
409  if(cmdline.isset("external-sat-solver"))
410  {
411  options.set_option(
412  "external-sat-solver", cmdline.get_value("external-sat-solver")),
413  solver_set = true;
414  }
415 
416  if(cmdline.isset("yices"))
417  {
418  options.set_option("yices", true), solver_set=true;
419  options.set_option("smt2", true);
420  }
421 
422  if(cmdline.isset("z3"))
423  {
424  options.set_option("z3", true), solver_set=true;
425  options.set_option("smt2", true);
426  }
427 
428  if(cmdline.isset("smt2") && !solver_set)
429  {
430  if(cmdline.isset("outfile"))
431  {
432  // outfile and no solver should give standard compliant SMT-LIB
433  options.set_option("generic", true);
434  }
435  else
436  {
437  // the default smt2 solver
438  options.set_option("z3", true);
439  }
440  }
441 
442  if(cmdline.isset("write-solver-stats-to"))
443  {
444  options.set_option(
445  "write-solver-stats-to", cmdline.get_value("write-solver-stats-to"));
446  }
447 
448  if(cmdline.isset("beautify"))
449  options.set_option("beautify", true);
450 
451  if(cmdline.isset("no-sat-preprocessor"))
452  options.set_option("sat-preprocessor", false);
453 
454  if(cmdline.isset("no-pretty-names"))
455  options.set_option("pretty-names", false);
456 
457  if(cmdline.isset("outfile"))
458  options.set_option("outfile", cmdline.get_value("outfile"));
459 
460  if(cmdline.isset("graphml-witness"))
461  {
462  options.set_option("graphml-witness", cmdline.get_value("graphml-witness"));
463  options.set_option("stop-on-fail", true);
464  options.set_option("trace", true);
465  }
466 
467  if(cmdline.isset("symex-coverage-report"))
468  {
469  options.set_option(
470  "symex-coverage-report",
471  cmdline.get_value("symex-coverage-report"));
472  options.set_option("paths-symex-explore-all", true);
473  }
474 
475  if(cmdline.isset("validate-ssa-equation"))
476  {
477  options.set_option("validate-ssa-equation", true);
478  }
479 
480  if(cmdline.isset("validate-goto-model"))
481  {
482  options.set_option("validate-goto-model", true);
483  }
484 
485  if(cmdline.isset("show-goto-symex-steps"))
486  options.set_option("show-goto-symex-steps", true);
487 
488  if(cmdline.isset("show-points-to-sets"))
489  options.set_option("show-points-to-sets", true);
490 
492 
493  // Options for process_goto_program
494  options.set_option("rewrite-union", true);
495 }
496 
499 {
500  if(cmdline.isset("version"))
501  {
502  std::cout << CBMC_VERSION << '\n';
503  return CPROVER_EXIT_SUCCESS;
504  }
505 
506  //
507  // command line options
508  //
509 
510  optionst options;
511  get_command_line_options(options);
512 
515 
516  //
517  // Print a banner
518  //
519  log.status() << "CBMC version " << CBMC_VERSION << " " << sizeof(void *) * 8
520  << "-bit " << config.this_architecture() << " "
522 
523  //
524  // Unwinding of transition systems is done by hw-cbmc.
525  //
526 
527  if(cmdline.isset("module") ||
528  cmdline.isset("gen-interface"))
529  {
530  log.error() << "This version of CBMC has no support for "
531  " hardware modules. Please use hw-cbmc."
532  << messaget::eom;
534  }
535 
536  if(cmdline.isset("show-points-to-sets"))
537  {
538  if(!cmdline.isset("json-ui") || cmdline.isset("xml-ui"))
539  {
540  log.error() << "--show-points-to-sets supports only"
541  " json output. Use --json-ui."
542  << messaget::eom;
544  }
545  }
546 
547  if(cmdline.isset("show-array-constraints"))
548  {
549  if(!cmdline.isset("json-ui") || cmdline.isset("xml-ui"))
550  {
551  log.error() << "--show-array-constraints supports only"
552  " json output. Use --json-ui."
553  << messaget::eom;
555  }
556  }
557 
559 
560  // configure gcc, if required
562  {
563  gcc_versiont gcc_version;
564  gcc_version.get("gcc");
565  configure_gcc(gcc_version);
566  }
567 
568  if(cmdline.isset("test-preprocessor"))
572 
573  if(cmdline.isset("preprocess"))
574  {
575  preprocessing(options);
576  return CPROVER_EXIT_SUCCESS;
577  }
578 
579  if(cmdline.isset("show-parse-tree"))
580  {
581  if(
582  cmdline.args.size() != 1 ||
584  {
585  log.error() << "Please give exactly one source file" << messaget::eom;
587  }
588 
589  std::string filename=cmdline.args[0];
590 
591  #ifdef _MSC_VER
592  std::ifstream infile(widen(filename));
593  #else
594  std::ifstream infile(filename);
595  #endif
596 
597  if(!infile)
598  {
599  log.error() << "failed to open input file '" << filename << "'"
600  << messaget::eom;
602  }
603 
604  std::unique_ptr<languaget> language=
605  get_language_from_filename(filename);
606 
607  if(language==nullptr)
608  {
609  log.error() << "failed to figure out type of file '" << filename << "'"
610  << messaget::eom;
612  }
613 
614  language->set_language_options(options);
615  language->set_message_handler(ui_message_handler);
616 
617  log.status() << "Parsing " << filename << messaget::eom;
618 
619  if(language->parse(infile, filename))
620  {
621  log.error() << "PARSING ERROR" << messaget::eom;
623  }
624 
625  language->show_parse(std::cout);
626  return CPROVER_EXIT_SUCCESS;
627  }
628 
629  int get_goto_program_ret =
631 
632  if(get_goto_program_ret!=-1)
633  return get_goto_program_ret;
634 
635  if(cmdline.isset("show-claims") || // will go away
636  cmdline.isset("show-properties")) // use this one
637  {
639  return CPROVER_EXIT_SUCCESS;
640  }
641 
642  if(set_properties())
644 
645  if(
646  options.get_bool_option("program-only") ||
647  options.get_bool_option("show-vcc") ||
648  options.get_bool_option("show-byte-ops"))
649  {
650  if(options.get_bool_option("paths"))
651  {
653  options, ui_message_handler, goto_model);
654  (void)verifier();
655  }
656  else
657  {
659  options, ui_message_handler, goto_model);
660  (void)verifier();
661  }
662 
663  return CPROVER_EXIT_SUCCESS;
664  }
665 
666  if(
667  options.get_bool_option("dimacs") || !options.get_option("outfile").empty())
668  {
669  if(options.get_bool_option("paths"))
670  {
672  options, ui_message_handler, goto_model);
673  (void)verifier();
674  }
675  else
676  {
678  options, ui_message_handler, goto_model);
679  (void)verifier();
680  }
681 
682  return CPROVER_EXIT_SUCCESS;
683  }
684 
685  if(options.is_set("cover"))
686  {
688  verifier(options, ui_message_handler, goto_model);
689  (void)verifier();
690  verifier.report();
691 
692  if(options.get_bool_option("show-test-suite"))
693  {
694  c_test_input_generatort test_generator(ui_message_handler, options);
695  test_generator(verifier.get_traces());
696  }
697 
698  return CPROVER_EXIT_SUCCESS;
699  }
700 
701  std::unique_ptr<goto_verifiert> verifier = nullptr;
702 
703  if(options.is_set("incremental-loop"))
704  {
705  if(options.get_bool_option("stop-on-fail"))
706  {
707  verifier = util_make_unique<
709  options, ui_message_handler, goto_model);
710  }
711  else
712  {
715  options, ui_message_handler, goto_model);
716  }
717  }
718  else if(
719  options.get_bool_option("stop-on-fail") && options.get_bool_option("paths"))
720  {
721  verifier =
722  util_make_unique<stop_on_fail_verifiert<single_path_symex_checkert>>(
723  options, ui_message_handler, goto_model);
724  }
725  else if(
726  options.get_bool_option("stop-on-fail") &&
727  !options.get_bool_option("paths"))
728  {
729  if(options.get_bool_option("localize-faults"))
730  {
731  verifier =
734  }
735  else
736  {
737  verifier =
738  util_make_unique<stop_on_fail_verifiert<multi_path_symex_checkert>>(
739  options, ui_message_handler, goto_model);
740  }
741  }
742  else if(
743  !options.get_bool_option("stop-on-fail") &&
744  options.get_bool_option("paths"))
745  {
746  verifier = util_make_unique<
748  options, ui_message_handler, goto_model);
749  }
750  else if(
751  !options.get_bool_option("stop-on-fail") &&
752  !options.get_bool_option("paths"))
753  {
754  if(options.get_bool_option("localize-faults"))
755  {
756  verifier =
759  }
760  else
761  {
762  verifier = util_make_unique<
764  options, ui_message_handler, goto_model);
765  }
766  }
767  else
768  {
769  UNREACHABLE;
770  }
771 
772  const resultt result = (*verifier)();
773  verifier->report();
774 
775  return result_to_exit_code(result);
776 }
777 
779 {
780  if(cmdline.isset("claim")) // will go away
782 
783  if(cmdline.isset("property")) // use this one
785 
786  return false;
787 }
788 
790  goto_modelt &goto_model,
791  const optionst &options,
792  const cmdlinet &cmdline,
793  ui_message_handlert &ui_message_handler)
794 {
796  if(cmdline.args.empty())
797  {
798  log.error() << "Please provide a program to verify" << messaget::eom;
800  }
801 
803 
804  if(cmdline.isset("show-symbol-table"))
805  {
807  return CPROVER_EXIT_SUCCESS;
808  }
809 
812 
813  if(cmdline.isset("validate-goto-model"))
814  {
816  }
817 
818  // show it?
819  if(cmdline.isset("show-loops"))
820  {
822  return CPROVER_EXIT_SUCCESS;
823  }
824 
825  // show it?
826  if(
827  cmdline.isset("show-goto-functions") ||
828  cmdline.isset("list-goto-functions"))
829  {
831  goto_model, ui_message_handler, cmdline.isset("list-goto-functions"));
832  return CPROVER_EXIT_SUCCESS;
833  }
834 
836 
837  return -1; // no error, continue
838 }
839 
841 {
842  if(cmdline.args.size() != 1)
843  {
844  log.error() << "Please provide one program to preprocess" << messaget::eom;
845  return;
846  }
847 
848  std::string filename = cmdline.args[0];
849 
850  std::ifstream infile(filename);
851 
852  if(!infile)
853  {
854  log.error() << "failed to open input file" << messaget::eom;
855  return;
856  }
857 
858  std::unique_ptr<languaget> language = get_language_from_filename(filename);
859  language->set_language_options(options);
860 
861  if(language == nullptr)
862  {
863  log.error() << "failed to figure out type of file" << messaget::eom;
864  return;
865  }
866 
867  language->set_message_handler(ui_message_handler);
868 
869  if(language->preprocess(infile, filename, std::cout))
870  log.error() << "PREPROCESSING ERROR" << messaget::eom;
871 }
872 
874  goto_modelt &goto_model,
875  const optionst &options,
876  messaget &log)
877 {
878  // Remove inline assembler; this needs to happen before
879  // adding the library.
881 
882  // add the library
883  log.status() << "Adding CPROVER library (" << config.ansi_c.arch << ")"
884  << messaget::eom;
889 
891 
892  // Common removal of types and complex constructs
893  if(::process_goto_program(goto_model, options, log))
894  return true;
895 
896  // ignore default/user-specified initialization
897  // of variables with static lifetime
898  if(options.get_bool_option("nondet-static"))
899  {
900  log.status() << "Adding nondeterministic initialization "
901  "of static/global variables"
902  << messaget::eom;
904  }
905 
906  // add failed symbols
907  // needs to be done before pointer analysis
909 
910  if(options.get_bool_option("drop-unused-functions"))
911  {
912  // Entry point will have been set before and function pointers removed
913  log.status() << "Removing unused functions" << messaget::eom;
915  }
916 
917  // remove skips such that trivial GOTOs are deleted and not considered
918  // for coverage annotation:
920 
921  // instrument cover goals
922  if(options.is_set("cover"))
923  {
924  const auto cover_config = get_cover_config(
927  cover_config, goto_model, log.get_message_handler()))
928  return true;
929  }
930 
931  // label the assertions
932  // This must be done after adding assertions and
933  // before using the argument of the "property" option.
934  // Do not re-label after using the property slicer because
935  // this would cause the property identifiers to change.
937 
938  // reachability slice?
939  if(options.get_bool_option("reachability-slice-fb"))
940  {
941  log.status() << "Performing a forwards-backwards reachability slice"
942  << messaget::eom;
943  if(options.is_set("property"))
945  goto_model, options.get_list_option("property"), true);
946  else
948  }
949 
950  if(options.get_bool_option("reachability-slice"))
951  {
952  log.status() << "Performing a reachability slice" << messaget::eom;
953  if(options.is_set("property"))
954  reachability_slicer(goto_model, options.get_list_option("property"));
955  else
957  }
958 
959  // full slice?
960  if(options.get_bool_option("full-slice"))
961  {
962  log.status() << "Performing a full slice" << messaget::eom;
963  if(options.is_set("property"))
964  property_slicer(goto_model, options.get_list_option("property"));
965  else
967  }
968 
969  // remove any skips introduced since coverage instrumentation
971 
972  return false;
973 }
974 
977 {
978  // clang-format off
979  std::cout << '\n' << banner_string("CBMC", CBMC_VERSION) << '\n'
980  << align_center_with_border("Copyright (C) 2001-2018") << '\n'
981  << align_center_with_border("Daniel Kroening, Edmund Clarke") << '\n' // NOLINT(*)
982  << align_center_with_border("Carnegie Mellon University, Computer Science Department") << '\n' // NOLINT(*)
983  << align_center_with_border("kroening@kroening.com") << '\n' // NOLINT(*)
984  << align_center_with_border("Protected in part by U.S. patent 7,225,417") << '\n' // NOLINT(*)
985  <<
986  "\n"
987  "Usage: Purpose:\n"
988  "\n"
989  " cbmc [-?] [-h] [--help] show help\n"
990  " cbmc file.c ... source file names\n"
991  "\n"
992  "Analysis options:\n"
994  " --symex-coverage-report f generate a Cobertura XML coverage report in f\n" // NOLINT(*)
995  " --property id only check one specific property\n"
996  " --trace give a counterexample trace for failed properties\n" //NOLINT(*)
997  " --stop-on-fail stop analysis once a failed property is detected\n" // NOLINT(*)
998  " (implies --trace)\n"
999  "\n"
1000  "C/C++ frontend options:\n"
1001  " --preprocess stop after preprocessing\n"
1005  "\n"
1006  "Platform options:\n"
1008  "\n"
1009  "Program representations:\n"
1010  " --show-parse-tree show parse tree\n"
1011  " --show-symbol-table show loaded symbol table\n"
1013  "\n"
1014  "Program instrumentation options:\n"
1016  HELP_COVER
1017  " --mm MM memory consistency model for concurrent programs (default: sc)\n" // NOLINT(*)
1021  " --full-slice run full slicer (experimental)\n" // NOLINT(*)
1022  " --drop-unused-functions drop functions trivially unreachable from main function\n" // NOLINT(*)
1023  " --havoc-undefined-functions\n"
1024  " for any function that has no body, assign non-deterministic values to\n" // NOLINT(*)
1025  " any parameters passed as non-const pointers and the return value\n" // NOLINT(*)
1026  "\n"
1027  "Semantic transformations:\n"
1028  // NOLINTNEXTLINE(whitespace/line_length)
1029  " --nondet-static add nondeterministic initialization of variables with static lifetime\n"
1030  "\n"
1031  "BMC options:\n"
1032  HELP_BMC
1033  "\n"
1034  "Backend options:\n"
1036  " --dimacs generate CNF in DIMACS format\n"
1037  " --beautify beautify the counterexample (greedy heuristic)\n" // NOLINT(*)
1038  " --localize-faults localize faults (experimental)\n"
1039  " --smt2 use default SMT2 solver (Z3)\n"
1040  " --boolector use Boolector\n"
1041  " --cprover-smt2 use CPROVER SMT2 solver\n"
1042  " --cvc4 use CVC4\n"
1043  " --mathsat use MathSAT\n"
1044  " --yices use Yices\n"
1045  " --z3 use Z3\n"
1046  " --refine use refinement procedure (experimental)\n"
1047  " --external-sat-solver cmd command to invoke SAT solver process\n"
1049  " --outfile filename output formula to given file\n"
1050  " --arrays-uf-never never turn arrays into uninterpreted functions\n" // NOLINT(*)
1051  " --arrays-uf-always always turn arrays into uninterpreted functions\n" // NOLINT(*)
1052  "\n"
1053  "Other options:\n"
1054  " --version show version and exit\n"
1059  HELP_FLUSH
1060  " --verbosity # verbosity level\n"
1062  " --write-solver-stats-to json-file\n"
1063  " collect the solver query complexity\n"
1064  " --show-array-constraints show array theory constraints added\n"
1065  " during post processing.\n"
1066  " Requires --json-ui.\n"
1067  "\n";
1068  // clang-format on
1069 }
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:202
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 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:1315
static irep_idt this_architecture()
Definition: config.cpp:1326
static irep_idt this_operating_system()
Definition: config.cpp:1426
struct configt::ansi_ct ansi_c
void get(const std::string &executable)
Definition: gcc_version.cpp:19
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:104
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()
ui_message_handlert ui_message_handler
Definition: parse_options.h:42
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:31
configt config
Definition: config.cpp:24
#define HELP_CONFIG_LIBRARY
Definition: config.h:64
#define HELP_CONFIG_PLATFORM
Definition: config.h:83
#define HELP_CONFIG_C_CPP
Definition: config.h:35
#define HELP_CONFIG_BACKEND
Definition: config.h:98
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:30
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:71
#define HELP_GOTO_CHECK
Definition: goto_check.h:49
Function Inlining.
#define PARSE_OPTIONS_GOTO_TRACE(cmdline, options)
Definition: goto_trace.h:287
#define HELP_GOTO_TRACE
Definition: goto_trace.h:279
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:19
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:101
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:140
Properties.
resultt
The result of goto verifying.
Definition: properties.h:44
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:85
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:504
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:165
preprocessort preprocessor
Definition: config.h:200
#define HELP_TIMESTAMP
Definition: timestamper.h:14
#define HELP_FLUSH
Definition: ui_message.h:106
std::wstring widen(const char *s)
Definition: unicode.cpp:50
#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