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 
55 #include <goto-programs/loop_ids.h>
64 
65 #include <goto-instrument/cover.h>
69 
71 
73 
74 #include <langapi/mode.h>
75 
76 #include "c_test_input_generator.h"
77 
78 cbmc_parse_optionst::cbmc_parse_optionst(int argc, const char **argv)
81  argc,
82  argv,
83  std::string("CBMC ") + CBMC_VERSION)
84 {
87 }
88 
90  int argc,
91  const char **argv,
92  const std::string &extra_options)
94  CBMC_OPTIONS + extra_options,
95  argc,
96  argv,
97  std::string("CBMC ") + CBMC_VERSION)
98 {
101 }
102 
104 {
105  // Default true
106  options.set_option("built-in-assertions", true);
107  options.set_option("pretty-names", true);
108  options.set_option("propagation", true);
109  options.set_option("sat-preprocessor", true);
110  options.set_option("simple-slice", true);
111  options.set_option("simplify", true);
112  options.set_option("simplify-if", true);
113  options.set_option("show-goto-symex-steps", false);
114  options.set_option("show-points-to-sets", false);
115  options.set_option("show-array-constraints", false);
116 
117  // Other default
118  options.set_option("arrays-uf", "auto");
119  options.set_option("depth", UINT32_MAX);
120 }
121 
123 {
124  if(config.set(cmdline))
125  {
126  usage_error();
128  }
129 
132 
133  if(cmdline.isset("function"))
134  options.set_option("function", cmdline.get_value("function"));
135 
136  if(cmdline.isset("cover") && cmdline.isset("unwinding-assertions"))
137  {
138  log.error()
139  << "--cover and --unwinding-assertions must not be given together"
140  << messaget::eom;
142  }
143 
144  if(cmdline.isset("max-field-sensitivity-array-size"))
145  {
146  options.set_option(
147  "max-field-sensitivity-array-size",
148  cmdline.get_value("max-field-sensitivity-array-size"));
149  }
150 
151  if(cmdline.isset("no-array-field-sensitivity"))
152  {
153  if(cmdline.isset("max-field-sensitivity-array-size"))
154  {
155  log.error()
156  << "--no-array-field-sensitivity and --max-field-sensitivity-array-size"
157  << " must not be given together" << messaget::eom;
159  }
160  options.set_option("no-array-field-sensitivity", true);
161  }
162 
163  if(cmdline.isset("partial-loops") && cmdline.isset("unwinding-assertions"))
164  {
165  log.error()
166  << "--partial-loops and --unwinding-assertions must not be given "
167  << "together" << messaget::eom;
169  }
170 
171  if(cmdline.isset("reachability-slice") &&
172  cmdline.isset("reachability-slice-fb"))
173  {
174  log.error()
175  << "--reachability-slice and --reachability-slice-fb must not be "
176  << "given together" << messaget::eom;
178  }
179 
180  if(cmdline.isset("full-slice"))
181  options.set_option("full-slice", true);
182 
183  if(cmdline.isset("show-symex-strategies"))
184  {
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  options.set_option(
346  "symex-cache-dereferences", cmdline.isset("symex-cache-dereferences"));
347 
348  if(cmdline.isset("incremental-loop"))
349  {
350  options.set_option(
351  "incremental-loop", cmdline.get_value("incremental-loop"));
352  options.set_option("refine", true);
353  options.set_option("refine-arrays", true);
354 
355  if(cmdline.isset("unwind-min"))
356  options.set_option("unwind-min", cmdline.get_value("unwind-min"));
357 
358  if(cmdline.isset("unwind-max"))
359  options.set_option("unwind-max", cmdline.get_value("unwind-max"));
360 
361  if(cmdline.isset("ignore-properties-before-unwind-min"))
362  options.set_option("ignore-properties-before-unwind-min", true);
363 
364  if(cmdline.isset("paths"))
365  {
366  log.error() << "--paths not supported with --incremental-loop"
367  << messaget::eom;
369  }
370  }
371 
372  // SMT Options
373 
374  if(cmdline.isset("smt1"))
375  {
376  log.error() << "--smt1 is no longer supported" << messaget::eom;
378  }
379 
380  if(cmdline.isset("smt2"))
381  options.set_option("smt2", true);
382 
383  if(cmdline.isset("fpa"))
384  options.set_option("fpa", true);
385 
386  bool solver_set=false;
387 
388  if(cmdline.isset("boolector"))
389  {
390  options.set_option("boolector", true), solver_set=true;
391  options.set_option("smt2", true);
392  }
393 
394  if(cmdline.isset("cprover-smt2"))
395  {
396  options.set_option("cprover-smt2", true), solver_set = true;
397  options.set_option("smt2", true);
398  }
399 
400  if(cmdline.isset("mathsat"))
401  {
402  options.set_option("mathsat", true), solver_set=true;
403  options.set_option("smt2", true);
404  }
405 
406  if(cmdline.isset("cvc4"))
407  {
408  options.set_option("cvc4", true), solver_set=true;
409  options.set_option("smt2", true);
410  }
411 
412  if(cmdline.isset("incremental-smt2-solver"))
413  {
414  options.set_option(
415  "incremental-smt2-solver", cmdline.get_value("incremental-smt2-solver")),
416  solver_set = true;
417  }
418 
419  if(cmdline.isset("external-sat-solver"))
420  {
421  options.set_option(
422  "external-sat-solver", cmdline.get_value("external-sat-solver")),
423  solver_set = true;
424  }
425 
426  if(cmdline.isset("yices"))
427  {
428  options.set_option("yices", true), solver_set=true;
429  options.set_option("smt2", true);
430  }
431 
432  if(cmdline.isset("z3"))
433  {
434  options.set_option("z3", true), solver_set=true;
435  options.set_option("smt2", true);
436  }
437 
438  if(cmdline.isset("smt2") && !solver_set)
439  {
440  if(cmdline.isset("outfile"))
441  {
442  // outfile and no solver should give standard compliant SMT-LIB
443  options.set_option("generic", true);
444  }
445  else
446  {
447  // the default smt2 solver
448  options.set_option("z3", true);
449  }
450  }
451 
452  if(cmdline.isset("write-solver-stats-to"))
453  {
454  options.set_option(
455  "write-solver-stats-to", cmdline.get_value("write-solver-stats-to"));
456  }
457 
458  if(cmdline.isset("beautify"))
459  options.set_option("beautify", true);
460 
461  if(cmdline.isset("no-sat-preprocessor"))
462  options.set_option("sat-preprocessor", false);
463 
464  if(cmdline.isset("no-pretty-names"))
465  options.set_option("pretty-names", false);
466 
467  if(cmdline.isset("outfile"))
468  options.set_option("outfile", cmdline.get_value("outfile"));
469 
470  if(cmdline.isset("graphml-witness"))
471  {
472  options.set_option("graphml-witness", cmdline.get_value("graphml-witness"));
473  options.set_option("stop-on-fail", true);
474  options.set_option("trace", true);
475  }
476 
477  if(cmdline.isset("symex-coverage-report"))
478  {
479  options.set_option(
480  "symex-coverage-report",
481  cmdline.get_value("symex-coverage-report"));
482  options.set_option("paths-symex-explore-all", true);
483  }
484 
485  if(cmdline.isset("validate-ssa-equation"))
486  {
487  options.set_option("validate-ssa-equation", true);
488  }
489 
490  if(cmdline.isset("validate-goto-model"))
491  {
492  options.set_option("validate-goto-model", true);
493  }
494 
495  if(cmdline.isset("show-goto-symex-steps"))
496  options.set_option("show-goto-symex-steps", true);
497 
498  if(cmdline.isset("show-points-to-sets"))
499  options.set_option("show-points-to-sets", true);
500 
502 
503  // Options for process_goto_program
504  options.set_option("rewrite-union", true);
505 }
506 
509 {
510  if(cmdline.isset("version"))
511  {
512  std::cout << CBMC_VERSION << '\n';
513  return CPROVER_EXIT_SUCCESS;
514  }
515 
516  //
517  // command line options
518  //
519 
520  optionst options;
521  get_command_line_options(options);
522 
525 
527 
528  //
529  // Unwinding of transition systems is done by hw-cbmc.
530  //
531 
532  if(cmdline.isset("module") ||
533  cmdline.isset("gen-interface"))
534  {
535  log.error() << "This version of CBMC has no support for "
536  " hardware modules. Please use hw-cbmc."
537  << messaget::eom;
539  }
540 
541  if(cmdline.isset("show-points-to-sets"))
542  {
543  if(!cmdline.isset("json-ui") || cmdline.isset("xml-ui"))
544  {
545  log.error() << "--show-points-to-sets supports only"
546  " json output. Use --json-ui."
547  << messaget::eom;
549  }
550  }
551 
552  if(cmdline.isset("show-array-constraints"))
553  {
554  if(!cmdline.isset("json-ui") || cmdline.isset("xml-ui"))
555  {
556  log.error() << "--show-array-constraints supports only"
557  " json output. Use --json-ui."
558  << messaget::eom;
560  }
561  }
562 
564 
565  // configure gcc, if required
567  {
568  gcc_versiont gcc_version;
569  gcc_version.get("gcc");
570  configure_gcc(gcc_version);
571  }
572 
573  if(cmdline.isset("test-preprocessor"))
577 
578  if(cmdline.isset("preprocess"))
579  {
580  preprocessing(options);
581  return CPROVER_EXIT_SUCCESS;
582  }
583 
584  if(cmdline.isset("show-parse-tree"))
585  {
586  if(
587  cmdline.args.size() != 1 ||
589  {
590  log.error() << "Please give exactly one source file" << messaget::eom;
592  }
593 
594  std::string filename=cmdline.args[0];
595 
596  #ifdef _MSC_VER
597  std::ifstream infile(widen(filename));
598  #else
599  std::ifstream infile(filename);
600  #endif
601 
602  if(!infile)
603  {
604  log.error() << "failed to open input file '" << filename << "'"
605  << messaget::eom;
607  }
608 
609  std::unique_ptr<languaget> language=
610  get_language_from_filename(filename);
611 
612  if(language==nullptr)
613  {
614  log.error() << "failed to figure out type of file '" << filename << "'"
615  << messaget::eom;
617  }
618 
619  language->set_language_options(options);
620  language->set_message_handler(ui_message_handler);
621 
622  log.status() << "Parsing " << filename << messaget::eom;
623 
624  if(language->parse(infile, filename))
625  {
626  log.error() << "PARSING ERROR" << messaget::eom;
628  }
629 
630  language->show_parse(std::cout);
631  return CPROVER_EXIT_SUCCESS;
632  }
633 
634  int get_goto_program_ret =
636 
637  if(get_goto_program_ret!=-1)
638  return get_goto_program_ret;
639 
640  if(cmdline.isset("show-claims") || // will go away
641  cmdline.isset("show-properties")) // use this one
642  {
644  return CPROVER_EXIT_SUCCESS;
645  }
646 
647  if(set_properties())
649 
650  if(
651  options.get_bool_option("program-only") ||
652  options.get_bool_option("show-vcc") ||
653  options.get_bool_option("show-byte-ops"))
654  {
655  if(options.get_bool_option("paths"))
656  {
658  options, ui_message_handler, goto_model);
659  (void)verifier();
660  }
661  else
662  {
664  options, ui_message_handler, goto_model);
665  (void)verifier();
666  }
667 
668  return CPROVER_EXIT_SUCCESS;
669  }
670 
671  if(
672  options.get_bool_option("dimacs") || !options.get_option("outfile").empty())
673  {
674  if(options.get_bool_option("paths"))
675  {
677  options, ui_message_handler, goto_model);
678  (void)verifier();
679  }
680  else
681  {
683  options, ui_message_handler, goto_model);
684  (void)verifier();
685  }
686 
687  return CPROVER_EXIT_SUCCESS;
688  }
689 
690  if(options.is_set("cover"))
691  {
693  verifier(options, ui_message_handler, goto_model);
694  (void)verifier();
695  verifier.report();
696 
697  if(options.get_bool_option("show-test-suite"))
698  {
699  c_test_input_generatort test_generator(ui_message_handler, options);
700  test_generator(verifier.get_traces());
701  }
702 
703  return CPROVER_EXIT_SUCCESS;
704  }
705 
706  std::unique_ptr<goto_verifiert> verifier = nullptr;
707 
708  if(options.is_set("incremental-loop"))
709  {
710  if(options.get_bool_option("stop-on-fail"))
711  {
712  verifier = util_make_unique<
714  options, ui_message_handler, goto_model);
715  }
716  else
717  {
720  options, ui_message_handler, goto_model);
721  }
722  }
723  else if(
724  options.get_bool_option("stop-on-fail") && options.get_bool_option("paths"))
725  {
726  verifier =
727  util_make_unique<stop_on_fail_verifiert<single_path_symex_checkert>>(
728  options, ui_message_handler, goto_model);
729  }
730  else if(
731  options.get_bool_option("stop-on-fail") &&
732  !options.get_bool_option("paths"))
733  {
734  if(options.get_bool_option("localize-faults"))
735  {
736  verifier =
739  }
740  else
741  {
742  verifier =
743  util_make_unique<stop_on_fail_verifiert<multi_path_symex_checkert>>(
744  options, ui_message_handler, goto_model);
745  }
746  }
747  else if(
748  !options.get_bool_option("stop-on-fail") &&
749  options.get_bool_option("paths"))
750  {
751  verifier = util_make_unique<
753  options, ui_message_handler, goto_model);
754  }
755  else if(
756  !options.get_bool_option("stop-on-fail") &&
757  !options.get_bool_option("paths"))
758  {
759  if(options.get_bool_option("localize-faults"))
760  {
761  verifier =
764  }
765  else
766  {
767  verifier = util_make_unique<
769  options, ui_message_handler, goto_model);
770  }
771  }
772  else
773  {
774  UNREACHABLE;
775  }
776 
777  const resultt result = (*verifier)();
778  verifier->report();
779 
780  return result_to_exit_code(result);
781 }
782 
784 {
785  if(cmdline.isset("claim")) // will go away
787 
788  if(cmdline.isset("property")) // use this one
790 
791  return false;
792 }
793 
795  goto_modelt &goto_model,
796  const optionst &options,
797  const cmdlinet &cmdline,
798  ui_message_handlert &ui_message_handler)
799 {
801  if(cmdline.args.empty())
802  {
803  log.error() << "Please provide a program to verify" << messaget::eom;
805  }
806 
808 
809  if(cmdline.isset("show-symbol-table"))
810  {
812  return CPROVER_EXIT_SUCCESS;
813  }
814 
817 
818  if(cmdline.isset("validate-goto-model"))
819  {
821  }
822 
823  // show it?
824  if(cmdline.isset("show-loops"))
825  {
827  return CPROVER_EXIT_SUCCESS;
828  }
829 
830  // show it?
831  if(
832  cmdline.isset("show-goto-functions") ||
833  cmdline.isset("list-goto-functions"))
834  {
836  goto_model, ui_message_handler, cmdline.isset("list-goto-functions"));
837  return CPROVER_EXIT_SUCCESS;
838  }
839 
841 
842  return -1; // no error, continue
843 }
844 
846 {
847  if(cmdline.args.size() != 1)
848  {
849  log.error() << "Please provide one program to preprocess" << messaget::eom;
850  return;
851  }
852 
853  std::string filename = cmdline.args[0];
854 
855  std::ifstream infile(filename);
856 
857  if(!infile)
858  {
859  log.error() << "failed to open input file" << messaget::eom;
860  return;
861  }
862 
863  std::unique_ptr<languaget> language = get_language_from_filename(filename);
864  language->set_language_options(options);
865 
866  if(language == nullptr)
867  {
868  log.error() << "failed to figure out type of file" << messaget::eom;
869  return;
870  }
871 
872  language->set_message_handler(ui_message_handler);
873 
874  if(language->preprocess(infile, filename, std::cout))
875  log.error() << "PREPROCESSING ERROR" << messaget::eom;
876 }
877 
879  goto_modelt &goto_model,
880  const optionst &options,
881  messaget &log)
882 {
883  // Remove inline assembler; this needs to happen before
884  // adding the library.
886 
887  // add the library
888  log.status() << "Adding CPROVER library (" << config.ansi_c.arch << ")"
889  << messaget::eom;
894 
895  // Common removal of types and complex constructs
896  if(::process_goto_program(goto_model, options, log))
897  return true;
898 
899  // ignore default/user-specified initialization
900  // of variables with static lifetime
901  if(options.get_bool_option("nondet-static"))
902  {
903  log.status() << "Adding nondeterministic initialization "
904  "of static/global variables"
905  << messaget::eom;
907  }
908 
909  // add failed symbols
910  // needs to be done before pointer analysis
912 
913  if(options.get_bool_option("drop-unused-functions"))
914  {
915  // Entry point will have been set before and function pointers removed
916  log.status() << "Removing unused functions" << messaget::eom;
918  }
919 
920  // remove skips such that trivial GOTOs are deleted and not considered
921  // for coverage annotation:
923 
924  // instrument cover goals
925  if(options.is_set("cover"))
926  {
927  const auto cover_config = get_cover_config(
930  cover_config, goto_model, log.get_message_handler()))
931  return true;
932  }
933 
934  // label the assertions
935  // This must be done after adding assertions and
936  // before using the argument of the "property" option.
937  // Do not re-label after using the property slicer because
938  // this would cause the property identifiers to change.
940 
941  // reachability slice?
942  if(options.get_bool_option("reachability-slice-fb"))
943  {
944  log.status() << "Performing a forwards-backwards reachability slice"
945  << messaget::eom;
946  if(options.is_set("property"))
948  goto_model, options.get_list_option("property"), true);
949  else
951  }
952 
953  if(options.get_bool_option("reachability-slice"))
954  {
955  log.status() << "Performing a reachability slice" << messaget::eom;
956  if(options.is_set("property"))
957  reachability_slicer(goto_model, options.get_list_option("property"));
958  else
960  }
961 
962  // full slice?
963  if(options.get_bool_option("full-slice"))
964  {
965  log.status() << "Performing a full slice" << messaget::eom;
966  if(options.is_set("property"))
967  property_slicer(goto_model, options.get_list_option("property"));
968  else
970  }
971 
972  // remove any skips introduced since coverage instrumentation
974 
975  return false;
976 }
977 
980 {
981  // clang-format off
982  std::cout << '\n' << banner_string("CBMC", CBMC_VERSION) << '\n'
983  << align_center_with_border("Copyright (C) 2001-2018") << '\n'
984  << align_center_with_border("Daniel Kroening, Edmund Clarke") << '\n' // NOLINT(*)
985  << align_center_with_border("Carnegie Mellon University, Computer Science Department") << '\n' // NOLINT(*)
986  << align_center_with_border("kroening@kroening.com") << '\n' // NOLINT(*)
987  << align_center_with_border("Protected in part by U.S. patent 7,225,417") << '\n' // NOLINT(*)
988  <<
989  "\n"
990  "Usage: Purpose:\n"
991  "\n"
992  " cbmc [-?] [-h] [--help] show help\n"
993  " cbmc file.c ... source file names\n"
994  "\n"
995  "Analysis options:\n"
997  " --symex-coverage-report f generate a Cobertura XML coverage report in f\n" // NOLINT(*)
998  " --property id only check one specific property\n"
999  " --trace give a counterexample trace for failed properties\n" //NOLINT(*)
1000  " --stop-on-fail stop analysis once a failed property is detected\n" // NOLINT(*)
1001  " (implies --trace)\n"
1002  "\n"
1003  "C/C++ frontend options:\n"
1004  " --preprocess stop after preprocessing\n"
1008  "\n"
1009  "Platform options:\n"
1011  "\n"
1012  "Program representations:\n"
1013  " --show-parse-tree show parse tree\n"
1014  " --show-symbol-table show loaded symbol table\n"
1016  "\n"
1017  "Program instrumentation options:\n"
1019  HELP_COVER
1020  " --mm MM memory consistency model for concurrent programs (default: sc)\n" // NOLINT(*)
1024  " --full-slice run full slicer (experimental)\n" // NOLINT(*)
1025  " --drop-unused-functions drop functions trivially unreachable from main function\n" // NOLINT(*)
1026  " --havoc-undefined-functions\n"
1027  " for any function that has no body, assign non-deterministic values to\n" // NOLINT(*)
1028  " any parameters passed as non-const pointers and the return value\n" // NOLINT(*)
1029  "\n"
1030  "Semantic transformations:\n"
1031  // NOLINTNEXTLINE(whitespace/line_length)
1032  " --nondet-static add nondeterministic initialization of variables with static lifetime\n"
1033  "\n"
1034  "BMC options:\n"
1035  HELP_BMC
1036  "\n"
1037  "Backend options:\n"
1039  " --dimacs generate CNF in DIMACS format\n"
1040  " --beautify beautify the counterexample (greedy heuristic)\n" // NOLINT(*)
1041  " --localize-faults localize faults (experimental)\n"
1042  " --smt2 use default SMT2 solver (Z3)\n"
1043  " --boolector use Boolector\n"
1044  " --cprover-smt2 use CPROVER SMT2 solver\n"
1045  " --cvc4 use CVC4\n"
1046  " --mathsat use MathSAT\n"
1047  " --yices use Yices\n"
1048  " --z3 use Z3\n"
1049  " --refine use refinement procedure (experimental)\n"
1050  " --incremental-smt2-solver cmd\n"
1051  " command to invoke external SMT solver for\n"
1052  " incremental solving (experimental)\n"
1053  " --external-sat-solver cmd command to invoke SAT solver process\n"
1055  " --outfile filename output formula to given file\n"
1056  " --arrays-uf-never never turn arrays into uninterpreted functions\n" // NOLINT(*)
1057  " --arrays-uf-always always turn arrays into uninterpreted functions\n" // NOLINT(*)
1058  "\n"
1059  "Other options:\n"
1060  " --version show version and exit\n"
1065  HELP_FLUSH
1066  " --verbosity # verbosity level\n"
1068  " --write-solver-stats-to json-file\n"
1069  " collect the solver query complexity\n"
1070  " --show-array-constraints show array theory constraints added\n"
1071  " during post processing.\n"
1072  " Requires --json-ui.\n"
1073  "\n";
1074  // clang-format on
1075 }
void add_failed_symbols(symbol_table_baset &symbol_table)
Create a failed-dereference symbol for all symbols in the given table that need one (i....
Pointer Dereferencing.
Goto Verifier for Verifying all Properties.
Goto verifier for verifying all properties that stores traces and localizes faults.
Goto verifier for verifying all properties that stores traces.
void cprover_c_library_factory(const std::set< irep_idt > &functions, symbol_tablet &symbol_table, message_handlert &message_handler)
#define HELP_ANSI_C_LANGUAGE
Bounded Model Checking Utilities.
#define HELP_BMC
Definition: bmc_util.h:201
void parse_c_object_factory_options(const cmdlinet &cmdline, optionst &options)
Parse the c object factory parameters from a given command line.
bool test_c_preprocessor(message_handlert &message_handler)
Test Input Generator for C.
CBMC Command Line Option Processing.
#define CBMC_OPTIONS
Requires an incremental goto checker that is a goto_trace_providert and fault_localization_providert.
virtual int doit() override
invoke main modules
static bool process_goto_program(goto_modelt &, const optionst &, messaget &)
static void set_default_options(optionst &)
Set the options that have default values.
static int get_goto_program(goto_modelt &, const optionst &, const cmdlinet &, ui_message_handlert &)
void get_command_line_options(optionst &)
void register_languages() override
void preprocessing(const optionst &)
virtual void help() override
display command line help
cbmc_parse_optionst(int argc, const char **argv)
std::string get_value(char option) const
Definition: cmdline.cpp:48
virtual bool isset(char option) const
Definition: cmdline.cpp:30
argst args
Definition: cmdline.h:145
const std::list< std::string > & get_values(const std::string &option) const
Definition: cmdline.cpp:109
bool set(const cmdlinet &cmdline)
Definition: config.cpp:798
std::string object_bits_info()
Definition: config.cpp:1339
struct configt::ansi_ct ansi_c
void get(const std::string &executable)
Definition: gcc_version.cpp:18
void validate(const validation_modet vm=validation_modet::INVARIANT, const goto_model_validation_optionst &goto_model_validation_options=goto_model_validation_optionst{}) const override
Check that the goto model is well-formed.
Definition: goto_model.h:98
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
static unsigned eval_verbosity(const std::string &user_input, const message_levelt default_verbosity, message_handlert &dest)
Parse a (user-)provided string as a verbosity level and set it as the verbosity of dest.
Definition: message.cpp:105
mstreamt & error() const
Definition: message.h:399
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:62
#define HELP_CONFIG_PLATFORM
Definition: config.h:81
#define HELP_CONFIG_C_CPP
Definition: config.h:33
#define HELP_CONFIG_BACKEND
Definition: config.h:96
static void instrument_cover_goals(const irep_idt &function_id, goto_programt &goto_program, const cover_instrumenterst &instrumenters, const irep_idt &mode, message_handlert &message_handler, const cover_instrumenter_baset::assertion_factoryt &make_assertion)
Applies instrumenters to given goto program.
Definition: cover.cpp:37
cover_configt get_cover_config(const optionst &options, const symbol_tablet &symbol_table, message_handlert &message_handler)
Build data structures controlling coverage from command-line options.
Definition: cover.cpp:186
void parse_cover_options(const cmdlinet &cmdline, optionst &options)
Parses coverage-related command line options.
Definition: cover.cpp:148
Coverage Instrumentation.
#define HELP_COVER
Definition: cover.h:32
Goto verifier for covering goals that stores traces.
void cprover_cpp_library_factory(const std::set< irep_idt > &functions, symbol_tablet &symbol_table, message_handlert &message_handler)
Document and give macros for the exit codes of CPROVER binaries.
#define CPROVER_EXIT_INTERNAL_ERROR
An error has been encountered during processing the requested analysis.
Definition: exit_codes.h:45
#define CPROVER_EXIT_INCORRECT_TASK
The command line is correctly structured but cannot be carried out due to missing files,...
Definition: exit_codes.h:49
#define CPROVER_EXIT_USAGE_ERROR
A usage error is returned when the command line is invalid or conflicting.
Definition: exit_codes.h:33
#define CPROVER_EXIT_SUCCESS
Success indicates the required analysis has been performed without error.
Definition: exit_codes.h:16
#define CPROVER_EXIT_SET_PROPERTIES_FAILED
Failure to identify the properties to verify.
Definition: exit_codes.h:55
#define CPROVER_EXIT_PREPROCESSOR_TEST_FAILED
Failure of the test-preprocessor method.
Definition: exit_codes.h:59
void full_slicer(goto_functionst &goto_functions, const namespacet &ns, const slicing_criteriont &criterion)
void property_slicer(goto_functionst &goto_functions, const namespacet &ns, const std::list< std::string > &properties)
void configure_gcc(const gcc_versiont &gcc_version)
#define PARSE_OPTIONS_GOTO_CHECK(cmdline, options)
Definition: goto_check_c.h:74
#define HELP_GOTO_CHECK
Definition: goto_check_c.h:53
#define PARSE_OPTIONS_GOTO_TRACE(cmdline, options)
Definition: goto_trace.h:285
#define HELP_GOTO_TRACE
Definition: goto_trace.h:277
goto_modelt initialize_goto_model(const std::vector< std::string > &files, message_handlert &message_handler, const optionst &options)
Initialize a Goto Program.
void json_interface(cmdlinet &cmdline, message_handlert &message_handler)
Parses the JSON-formatted command line from stdin.
#define HELP_JSON_INTERFACE
Abstract interface to support a programming language.
void show_loop_ids(ui_message_handlert::uit ui, const goto_modelt &goto_model)
Definition: loop_ids.cpp:21
Loop IDs.
std::unique_ptr< T > util_make_unique(Ts &&... ts)
Definition: make_unique.h:19
std::unique_ptr< languaget > get_language_from_filename(const std::string &filename)
Get the language corresponding to the registered file name extensions.
Definition: mode.cpp:102
Goto Checker using Multi-Path Symbolic Execution.
Goto Checker using Multi-Path Symbolic Execution only (no SAT solving)
static void nondet_static(const namespacet &ns, goto_functionst &goto_functions, const irep_idt &fct_name)
Nondeterministically initializes global scope variables in a goto-function.
Nondeterministically initializes global scope variables, except for constants (such as string literal...
std::string align_center_with_border(const std::string &text)
Utility for displaying help centered messages borderered by "* *".
std::string banner_string(const std::string &front_end, const std::string &version)
void parse_path_strategy_options(const cmdlinet &cmdline, optionst &options, message_handlert &message_handler)
add paths and exploration-strategy option, suitable to be invoked from front-ends.
std::string show_path_strategies()
suitable for displaying as a front-end help message
Storage of symbolic execution paths to resume.
int result_to_exit_code(resultt result)
Definition: properties.cpp:143
Properties.
resultt
The result of goto verifying.
Definition: properties.h:45
void reachability_slicer(goto_modelt &goto_model, const bool include_forward_reachability)
Perform reachability slicing on goto_model, with respect to the criterion given by all properties.
#define HELP_REACHABILITY_SLICER_FB
#define HELP_REACHABILITY_SLICER
bool is_goto_binary(const std::string &filename, message_handlert &message_handler)
Read Goto Programs.
#define HELP_FUNCTIONS
void remove_asm(goto_functionst &goto_functions, symbol_tablet &symbol_table)
Replaces inline assembly instructions in the goto program (i.e., instructions of kind OTHER with a co...
Definition: remove_asm.cpp:512
Remove 'asm' statements by compiling them into suitable standard goto program instructions.
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:88
Program Transformation.
void remove_unused_functions(goto_modelt &goto_model, message_handlert &message_handler)
Unused function removal.
void label_properties(goto_modelt &goto_model)
Set the properties to check.
void show_goto_functions(const namespacet &ns, ui_message_handlert &ui_message_handler, const goto_functionst &goto_functions, bool list_only)
Show the goto functions.
#define HELP_SHOW_GOTO_FUNCTIONS
void show_properties(const namespacet &ns, const irep_idt &identifier, message_handlert &message_handler, ui_message_handlert::uit ui, const goto_programt &goto_program)
Show the properties.
#define HELP_SHOW_PROPERTIES
void show_symbol_table(const symbol_tablet &symbol_table, ui_message_handlert &ui)
Show the symbol table.
Goto Checker using multi-path symbolic execution with incremental unwinding of a specified loop.
Goto Checker using Single Path Symbolic Execution.
Goto Checker using Single Path Symbolic Execution only.
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
Goto Verifier for stopping at the first failing property.
Goto Verifier for stopping at the first failing property and localizing the fault.
#define HELP_STRING_REFINEMENT_CBMC
irep_idt arch
Definition: config.h:191
preprocessort preprocessor
Definition: config.h:233
#define HELP_TIMESTAMP
Definition: timestamper.h:14
#define HELP_FLUSH
Definition: ui_message.h:108
std::wstring widen(const char *s)
Definition: unicode.cpp:48
#define HELP_VALIDATE
const char * CBMC_VERSION
void xml_interface(cmdlinet &cmdline, message_handlert &message_handler)
Parse XML-formatted commandline options from stdin.
#define HELP_XML_INTERFACE
Definition: xml_interface.h:39