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);
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 
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 }
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
cprover_library.h
cmdlinet::args
argst args
Definition: cmdline.h:143
cbmc_parse_optionst::doit
virtual int doit() override
invoke main modules
Definition: cbmc_parse_options.cpp:498
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
exception_utils.h
cover.h
Coverage Instrumentation.
HELP_REACHABILITY_SLICER
#define HELP_REACHABILITY_SLICER
Definition: reachability_slicer.h:43
HELP_BMC
#define HELP_BMC
Definition: bmc_util.h:202
HELP_SHOW_GOTO_FUNCTIONS
#define HELP_SHOW_GOTO_FUNCTIONS
Definition: show_goto_functions.h:26
languaget::show_parse
virtual void show_parse(std::ostream &out)=0
configt::object_bits_info
std::string object_bits_info()
Definition: config.cpp:1315
gcc_versiont::get
void get(const std::string &executable)
Definition: gcc_version.cpp:19
PARSE_OPTIONS_GOTO_CHECK
#define PARSE_OPTIONS_GOTO_CHECK(cmdline, options)
Definition: goto_check.h:71
add_malloc_may_fail_variable_initializations.h
HELP_GOTO_TRACE
#define HELP_GOTO_TRACE
Definition: goto_trace.h:279
parse_options_baset::ui_message_handler
ui_message_handlert ui_message_handler
Definition: parse_options.h:42
cbmc_parse_optionst::goto_model
goto_modelt goto_model
Definition: cbmc_parse_options.h:117
cbmc_parse_optionst::get_goto_program
static int get_goto_program(goto_modelt &, const optionst &, const cmdlinet &, ui_message_handlert &)
Definition: cbmc_parse_options.cpp:789
parse_options_baset
Definition: parse_options.h:20
single_loop_incremental_symex_checkert
Performs a multi-path symbolic execution using goto-symex that incrementally unwinds a given loop and...
Definition: single_loop_incremental_symex_checker.h:30
ui_message_handlert
Definition: ui_message.h:20
parse_c_object_factory_options
void parse_c_object_factory_options(const cmdlinet &cmdline, optionst &options)
Parse the c object factory parameters from a given command line.
Definition: c_object_factory_parameters.cpp:11
resultt
resultt
The result of goto verifying.
Definition: properties.h:44
cmdlinet::isset
virtual bool isset(char option) const
Definition: cmdline.cpp:29
stop_on_fail_verifiert
Stops when the first failing property is found.
Definition: stop_on_fail_verifier.h:23
goto_inline.h
Function Inlining.
optionst
Definition: options.h:23
gcc_version.h
all_properties_verifiert
Definition: all_properties_verifier.h:23
optionst::get_option
const std::string get_option(const std::string &option) const
Definition: options.cpp:67
messaget::M_STATISTICS
@ M_STATISTICS
Definition: message.h:171
messaget::status
mstreamt & status() const
Definition: message.h:414
multi_path_symex_only_checker.h
Goto Checker using Multi-Path Symbolic Execution only (no SAT solving)
show_properties
void show_properties(const namespacet &ns, const irep_idt &identifier, message_handlert &message_handler, ui_message_handlert::uit ui, const goto_programt &goto_program)
Definition: show_properties.cpp:47
HELP_FUNCTIONS
#define HELP_FUNCTIONS
Definition: rebuild_goto_start_function.h:27
remove_skip
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:85
cover_goals_verifier_with_trace_storaget::get_traces
const goto_trace_storaget & get_traces() const
Definition: cover_goals_verifier_with_trace_storage.h:64
HELP_CONFIG_PLATFORM
#define HELP_CONFIG_PLATFORM
Definition: config.h:83
invariant.h
remove_asm.h
Remove 'asm' statements by compiling them into suitable standard goto program instructions.
reachability_slicer
void reachability_slicer(goto_modelt &goto_model, const bool include_forward_reachability)
Perform reachability slicing on goto_model, with respect to the criterion given by all properties.
Definition: reachability_slicer.cpp:370
configure_gcc
void configure_gcc(const gcc_versiont &gcc_version)
Definition: gcc_version.cpp:146
c_preprocess.h
goto_modelt
Definition: goto_model.h:26
show_goto_functions.h
Show the goto functions.
mode.h
show_loop_ids
void show_loop_ids(ui_message_handlert::uit ui, const goto_modelt &goto_model)
Definition: loop_ids.cpp:19
all_properties_verifier.h
Goto Verifier for Verifying all Properties.
HELP_COVER
#define HELP_COVER
Definition: cover.h:30
optionst::set_option
void set_option(const std::string &option, const bool value)
Definition: options.cpp:28
messaget::eom
static eomt eom
Definition: message.h:297
instrument_cover_goals
static void instrument_cover_goals(const irep_idt &function_id, goto_programt &goto_program, const cover_instrumenterst &instrumenters, const irep_idt &mode, message_handlert &message_handler, const cover_instrumenter_baset::assertion_factoryt &make_assertion)
Applies instrumenters to given goto program.
Definition: cover.cpp:37
show_symbol_table
void show_symbol_table(const symbol_tablet &symbol_table, ui_message_handlert &ui)
Definition: show_symbol_table.cpp:268
configt::ansi_c
struct configt::ansi_ct ansi_c
version.h
remove_unused_functions
void remove_unused_functions(goto_modelt &goto_model, message_handlert &message_handler)
Definition: remove_unused_functions.cpp:18
cbmc_parse_optionst::cbmc_parse_optionst
cbmc_parse_optionst(int argc, const char **argv)
Definition: cbmc_parse_options.cpp:79
nondet_static.h
Nondeterministically initializes global scope variables, except for constants (such as string literal...
HELP_REACHABILITY_SLICER_FB
#define HELP_REACHABILITY_SLICER_FB
Definition: reachability_slicer.h:50
stop_on_fail_verifier_with_fault_localization.h
Goto Verifier for stopping at the first failing property and localizing the fault.
label_properties
void label_properties(goto_modelt &goto_model)
Definition: set_properties.cpp:43
path_storage.h
Storage of symbolic execution paths to resume.
languaget::set_language_options
virtual void set_language_options(const optionst &)
Set language-specific options.
Definition: language.h:43
nondet_static
void nondet_static(const namespacet &ns, goto_functionst &goto_functions, const irep_idt &fct_name)
Nondeterministically initializes global scope variables in a goto-function.
Definition: nondet_static.cpp:79
validate_goto_model.h
parse_path_strategy_options
void parse_path_strategy_options(const cmdlinet &cmdline, optionst &options, message_handlert &message_handler)
add paths and exploration-strategy option, suitable to be invoked from front-ends.
Definition: path_storage.cpp:136
cbmc_parse_optionst::register_languages
void register_languages()
Definition: cbmc_languages.cpp:25
HELP_JSON_INTERFACE
#define HELP_JSON_INTERFACE
Definition: json_interface.h:45
ui_message_handlert::get_ui
virtual uit get_ui() const
Definition: ui_message.h:31
parse_options_baset::usage_error
virtual void usage_error()
Definition: parse_options.cpp:47
util_make_unique
std::unique_ptr< T > util_make_unique(Ts &&... ts)
Definition: make_unique.h:19
bmc_util.h
Bounded Model Checking Utilities.
set_properties.h
Set the properties to check.
get_cover_config
cover_configt get_cover_config(const optionst &options, const symbol_tablet &symbol_table, message_handlert &message_handler)
Build data structures controlling coverage from command-line options.
Definition: cover.cpp:180
full_slicer
void full_slicer(goto_functionst &goto_functions, const namespacet &ns, const slicing_criteriont &criterion)
Definition: full_slicer.cpp:347
c_test_input_generator.h
Test Input Generator for C.
get_language_from_filename
std::unique_ptr< languaget > get_language_from_filename(const std::string &filename)
Get the language corresponding to the registered file name extensions.
Definition: mode.cpp:101
cmdlinet
Definition: cmdline.h:21
CBMC_VERSION
const char * CBMC_VERSION
cover_goals_verifier_with_trace_storage.h
Goto verifier for covering goals that stores traces.
HELP_CONFIG_C_CPP
#define HELP_CONFIG_C_CPP
Definition: config.h:35
make_unique.h
messaget::error
mstreamt & error() const
Definition: message.h:399
cover_goals_verifier_with_trace_storaget
Definition: cover_goals_verifier_with_trace_storage.h:25
multi_path_symex_checkert
Performs a multi-path symbolic execution using goto-symex and calls a SAT/SMT solver to check the sta...
Definition: multi_path_symex_checker.h:29
all_properties_verifier_with_trace_storage.h
Goto verifier for verifying all properties that stores traces.
initialize_goto_model.h
Initialize a Goto Program.
banner_string
std::string banner_string(const std::string &front_end, const std::string &version)
Definition: parse_options.cpp:163
c_test_input_generatort
Definition: c_test_input_generator.h:50
cbmc_parse_options.h
CBMC Command Line Option Processing.
cbmc_parse_optionst::get_command_line_options
void get_command_line_options(optionst &)
Definition: cbmc_parse_options.cpp:122
configt::ansi_ct::preprocessor
preprocessort preprocessor
Definition: config.h:200
optionst::is_set
bool is_set(const std::string &option) const
N.B. opts.is_set("foo") does not imply opts.get_bool_option("foo")
Definition: options.cpp:62
property_slicer
void property_slicer(goto_functionst &goto_functions, const namespacet &ns, const std::list< std::string > &properties)
Definition: full_slicer.cpp:370
show_properties.h
Show the properties.
multi_path_symex_checker.h
Goto Checker using Multi-Path Symbolic Execution.
cmdlinet::get_value
std::string get_value(char option) const
Definition: cmdline.cpp:47
show_symbol_table.h
Show the symbol table.
languaget::parse
virtual bool parse(std::istream &instream, const std::string &path)=0
CPROVER_EXIT_PREPROCESSOR_TEST_FAILED
#define CPROVER_EXIT_PREPROCESSOR_TEST_FAILED
Failure of the test-preprocessor method.
Definition: exit_codes.h:59
language.h
Abstract interface to support a programming language.
messaget::set_message_handler
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:179
HELP_SHOW_PROPERTIES
#define HELP_SHOW_PROPERTIES
Definition: show_properties.h:29
all_properties_verifier_with_trace_storaget
Definition: all_properties_verifier_with_trace_storage.h:25
cbmc_parse_optionst::process_goto_program
static bool process_goto_program(goto_modelt &, const optionst &, messaget &)
Definition: cbmc_parse_options.cpp:873
single_path_symex_checker.h
Goto Checker using Single Path Symbolic Execution.
configt::this_operating_system
static irep_idt this_operating_system()
Definition: config.cpp:1426
CPROVER_EXIT_SET_PROPERTIES_FAILED
#define CPROVER_EXIT_SET_PROPERTIES_FAILED
Failure to identify the properties to verify.
Definition: exit_codes.h:55
xml_interface
void xml_interface(cmdlinet &cmdline, message_handlert &message_handler)
Parse XML-formatted commandline options from stdin.
Definition: xml_interface.cpp:47
configt::ansi_ct::arch
irep_idt arch
Definition: config.h:165
show_goto_functions
void show_goto_functions(const namespacet &ns, ui_message_handlert &ui_message_handler, const goto_functionst &goto_functions, bool list_only)
Definition: show_goto_functions.cpp:26
HELP_CONFIG_LIBRARY
#define HELP_CONFIG_LIBRARY
Definition: config.h:64
json_interface
void json_interface(cmdlinet &cmdline, message_handlert &message_handler)
Parses the JSON-formatted command line from stdin.
Definition: json_interface.cpp:88
parse_cover_options
void parse_cover_options(const cmdlinet &cmdline, optionst &options)
Parses coverage-related command line options.
Definition: cover.cpp:142
cbmc_parse_optionst::set_properties
bool set_properties()
Definition: cbmc_parse_options.cpp:778
HELP_STRING_REFINEMENT_CBMC
#define HELP_STRING_REFINEMENT_CBMC
Definition: string_refinement.h:61
widen
std::wstring widen(const char *s)
Definition: unicode.cpp:50
read_goto_binary.h
Read Goto Programs.
all_properties_verifier_with_fault_localization.h
Goto verifier for verifying all properties that stores traces and localizes faults.
CPROVER_EXIT_INCORRECT_TASK
#define CPROVER_EXIT_INCORRECT_TASK
The command line is correctly structured but cannot be carried out due to missing files,...
Definition: exit_codes.h:49
full_slicer.h
Slicing.
configt::ansi_ct::preprocessort::GCC
@ GCC
HELP_ANSI_C_LANGUAGE
#define HELP_ANSI_C_LANGUAGE
Definition: ansi_c_language.h:27
add_malloc_may_fail_variable_initializations
void add_malloc_may_fail_variable_initializations(goto_modelt &goto_model)
Some variables have different initial values based on what flags are being passed to cbmc; since the ...
Definition: add_malloc_may_fail_variable_initializations.cpp:24
goto_verifiert::report
virtual void report()=0
Report results.
remove_unused_functions.h
Unused function removal.
config
configt config
Definition: config.cpp:24
gcc_versiont
Definition: gcc_version.h:20
parse_options_baset::log
messaget log
Definition: parse_options.h:43
configt::this_architecture
static irep_idt this_architecture()
Definition: config.cpp:1326
messaget::get_message_handler
message_handlert & get_message_handler()
Definition: message.h:184
result_to_exit_code
int result_to_exit_code(resultt result)
Definition: properties.cpp:140
ui_message_handlert::uit::PLAIN
@ PLAIN
stop_on_fail_verifier.h
Goto Verifier for stopping at the first failing property.
HELP_GOTO_CHECK
#define HELP_GOTO_CHECK
Definition: goto_check.h:49
cprover_c_library_factory
void cprover_c_library_factory(const std::set< irep_idt > &functions, symbol_tablet &symbol_table, message_handlert &message_handler)
Definition: cprover_library.cpp:79
configt::set
bool set(const cmdlinet &cmdline)
Definition: config.cpp:798
exit_codes.h
Document and give macros for the exit codes of CPROVER binaries.
optionst::get_bool_option
bool get_bool_option(const std::string &option) const
Definition: options.cpp:44
CPROVER_EXIT_USAGE_ERROR
#define CPROVER_EXIT_USAGE_ERROR
A usage error is returned when the command line is invalid or conflicting.
Definition: exit_codes.h:33
cbmc_parse_optionst::help
virtual void help() override
display command line help
Definition: cbmc_parse_options.cpp:976
remove_asm
void remove_asm(goto_functionst &goto_functions, symbol_tablet &symbol_table)
Replaces inline assembly instructions in the goto program (i.e., instructions of kind OTHER with a co...
Definition: remove_asm.cpp:511
unicode.h
is_goto_binary
bool is_goto_binary(const std::string &filename, message_handlert &message_handler)
Definition: read_goto_binary.cpp:190
show_path_strategies
std::string show_path_strategies()
suitable for displaying as a front-end help message
Definition: path_storage.cpp:110
config.h
goto_modelt::validate
void validate(const validation_modet vm=validation_modet::INVARIANT, const goto_model_validation_optionst &goto_model_validation_options=goto_model_validation_optionst{}) const override
Check that the goto model is well-formed.
Definition: goto_model.h:98
languaget::preprocess
virtual bool preprocess(std::istream &instream, const std::string &path, std::ostream &outstream)
Definition: language.h:49
loop_ids.h
Loop IDs.
reachability_slicer.h
Slicing.
PARSE_OPTIONS_GOTO_TRACE
#define PARSE_OPTIONS_GOTO_TRACE(cmdline, options)
Definition: goto_trace.h:287
HELP_CONFIG_BACKEND
#define HELP_CONFIG_BACKEND
Definition: config.h:98
single_loop_incremental_symex_checker.h
Goto Checker using multi-path symbolic execution with incremental unwinding of a specified loop.
stop_on_fail_verifier_with_fault_localizationt
Stops when the first failing property is found and localizes the fault Requires an incremental goto c...
Definition: stop_on_fail_verifier_with_fault_localization.h:26
add_failed_symbols.h
Pointer Dereferencing.
CPROVER_EXIT_INTERNAL_ERROR
#define CPROVER_EXIT_INTERNAL_ERROR
An error has been encountered during processing the requested analysis.
Definition: exit_codes.h:45
properties.h
Properties.
initialize_goto_model
goto_modelt initialize_goto_model(const std::vector< std::string > &files, message_handlert &message_handler, const optionst &options)
Definition: initialize_goto_model.cpp:59
add_failed_symbols
void add_failed_symbols(symbol_table_baset &symbol_table)
Create a failed-dereference symbol for all symbols in the given table that need one (i....
Definition: add_failed_symbols.cpp:76
CPROVER_EXIT_SUCCESS
#define CPROVER_EXIT_SUCCESS
Success indicates the required analysis has been performed without error.
Definition: exit_codes.h:16
messaget::eval_verbosity
static unsigned eval_verbosity(const std::string &user_input, const message_levelt default_verbosity, message_handlert &dest)
Parse a (user-)provided string as a verbosity level and set it as the verbosity of dest.
Definition: message.cpp:104
remove_skip.h
Program Transformation.
cbmc_parse_optionst::set_default_options
static void set_default_options(optionst &)
Set the options that have default values.
Definition: cbmc_parse_options.cpp:104
all_properties_verifier_with_fault_localizationt
Requires an incremental goto checker that is a goto_trace_providert and fault_localization_providert.
Definition: all_properties_verifier_with_fault_localization.h:28
cmdlinet::get_values
const std::list< std::string > & get_values(const std::string &option) const
Definition: cmdline.cpp:108
cover_goals_verifier_with_trace_storaget::report
void report() override
Report results.
Definition: cover_goals_verifier_with_trace_storage.h:59
parse_options_baset::cmdline
cmdlinet cmdline
Definition: parse_options.h:28
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
single_path_symex_only_checker.h
Goto Checker using Single Path Symbolic Execution only.
align_center_with_border
std::string align_center_with_border(const std::string &text)
Utility for displaying help centered messages borderered by "* *".
Definition: parse_options.cpp:150
optionst::get_list_option
const value_listt & get_list_option(const std::string &option) const
Definition: options.cpp:80
cprover_library.h
HELP_XML_INTERFACE
#define HELP_XML_INTERFACE
Definition: xml_interface.h:39
process_goto_program.h
HELP_TIMESTAMP
#define HELP_TIMESTAMP
Definition: timestamper.h:14
HELP_FLUSH
#define HELP_FLUSH
Definition: ui_message.h:106
CBMC_OPTIONS
#define CBMC_OPTIONS
Definition: cbmc_parse_options.h:44
cbmc_parse_optionst::preprocessing
void preprocessing(const optionst &)
Definition: cbmc_parse_options.cpp:840
cprover_cpp_library_factory
void cprover_cpp_library_factory(const std::set< irep_idt > &functions, symbol_tablet &symbol_table, message_handlert &message_handler)
Definition: cprover_library.cpp:38
test_c_preprocessor
bool test_c_preprocessor(message_handlert &message_handler)
Definition: c_preprocess.cpp:819
HELP_VALIDATE
#define HELP_VALIDATE
Definition: validation_interface.h:16