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 
56 #include <goto-programs/loop_ids.h>
57 #include <goto-programs/mm_io.h>
73 
74 #include <goto-instrument/cover.h>
78 
80 
82 
83 #include <langapi/mode.h>
84 
85 #include "c_test_input_generator.h"
86 
87 cbmc_parse_optionst::cbmc_parse_optionst(int argc, const char **argv)
90  argc,
91  argv,
92  std::string("CBMC ") + CBMC_VERSION)
93 {
96 }
97 
99  int argc,
100  const char **argv,
101  const std::string &extra_options)
103  CBMC_OPTIONS + extra_options,
104  argc,
105  argv,
106  std::string("CBMC ") + CBMC_VERSION)
107 {
110 }
111 
113 {
114  // Default true
115  options.set_option("assertions", true);
116  options.set_option("assumptions", true);
117  options.set_option("built-in-assertions", true);
118  options.set_option("pretty-names", true);
119  options.set_option("propagation", true);
120  options.set_option("sat-preprocessor", true);
121  options.set_option("simple-slice", true);
122  options.set_option("simplify", true);
123  options.set_option("simplify-if", true);
124  options.set_option("show-goto-symex-steps", false);
125 
126  // Other default
127  options.set_option("arrays-uf", "auto");
128 }
129 
131 {
132  if(config.set(cmdline))
133  {
134  usage_error();
136  }
137 
140 
141  if(cmdline.isset("function"))
142  options.set_option("function", cmdline.get_value("function"));
143 
144  if(cmdline.isset("cover") && cmdline.isset("unwinding-assertions"))
145  {
146  log.error()
147  << "--cover and --unwinding-assertions must not be given together"
148  << messaget::eom;
150  }
151 
152  if(cmdline.isset("max-field-sensitivity-array-size"))
153  {
154  options.set_option(
155  "max-field-sensitivity-array-size",
156  cmdline.get_value("max-field-sensitivity-array-size"));
157  }
158 
159  if(cmdline.isset("no-array-field-sensitivity"))
160  {
161  if(cmdline.isset("max-field-sensitivity-array-size"))
162  {
163  log.error()
164  << "--no-array-field-sensitivity and --max-field-sensitivity-array-size"
165  << " must not be given together" << messaget::eom;
167  }
168  options.set_option("no-array-field-sensitivity", true);
169  }
170 
171  if(cmdline.isset("partial-loops") && cmdline.isset("unwinding-assertions"))
172  {
173  log.error()
174  << "--partial-loops and --unwinding-assertions must not be given "
175  << "together" << messaget::eom;
177  }
178 
179  if(cmdline.isset("reachability-slice") &&
180  cmdline.isset("reachability-slice-fb"))
181  {
182  log.error()
183  << "--reachability-slice and --reachability-slice-fb must not be "
184  << "given together" << messaget::eom;
186  }
187 
188  if(cmdline.isset("full-slice"))
189  options.set_option("full-slice", true);
190 
191  if(cmdline.isset("show-symex-strategies"))
192  {
194  exit(CPROVER_EXIT_SUCCESS);
195  }
196 
198 
199  if(cmdline.isset("program-only"))
200  options.set_option("program-only", true);
201 
202  if(cmdline.isset("show-byte-ops"))
203  options.set_option("show-byte-ops", true);
204 
205  if(cmdline.isset("show-vcc"))
206  options.set_option("show-vcc", true);
207 
208  if(cmdline.isset("cover"))
209  parse_cover_options(cmdline, options);
210 
211  if(cmdline.isset("mm"))
212  options.set_option("mm", cmdline.get_value("mm"));
213 
214  if(cmdline.isset("c89"))
216 
217  if(cmdline.isset("symex-complexity-limit"))
218  options.set_option(
219  "symex-complexity-limit", cmdline.get_value("symex-complexity-limit"));
220 
221  if(cmdline.isset("symex-complexity-failed-child-loops-limit"))
222  options.set_option(
223  "symex-complexity-failed-child-loops-limit",
224  cmdline.get_value("symex-complexity-failed-child-loops-limit"));
225 
226  if(cmdline.isset("c99"))
228 
229  if(cmdline.isset("c11"))
231 
232  if(cmdline.isset("cpp98"))
233  config.cpp.set_cpp98();
234 
235  if(cmdline.isset("cpp03"))
236  config.cpp.set_cpp03();
237 
238  if(cmdline.isset("cpp11"))
239  config.cpp.set_cpp11();
240 
241  if(cmdline.isset("property"))
242  options.set_option("property", cmdline.get_values("property"));
243 
244  if(cmdline.isset("drop-unused-functions"))
245  options.set_option("drop-unused-functions", true);
246 
247  if(cmdline.isset("havoc-undefined-functions"))
248  options.set_option("havoc-undefined-functions", true);
249 
250  if(cmdline.isset("string-abstraction"))
251  options.set_option("string-abstraction", true);
252 
253  if(cmdline.isset("reachability-slice-fb"))
254  options.set_option("reachability-slice-fb", true);
255 
256  if(cmdline.isset("reachability-slice"))
257  options.set_option("reachability-slice", true);
258 
259  if(cmdline.isset("nondet-static"))
260  options.set_option("nondet-static", true);
261 
262  if(cmdline.isset("no-simplify"))
263  options.set_option("simplify", false);
264 
265  if(cmdline.isset("stop-on-fail") ||
266  cmdline.isset("dimacs") ||
267  cmdline.isset("outfile"))
268  options.set_option("stop-on-fail", true);
269 
270  if(
271  cmdline.isset("trace") || cmdline.isset("compact-trace") ||
272  cmdline.isset("stack-trace") || cmdline.isset("stop-on-fail") ||
274  !cmdline.isset("cover")))
275  {
276  options.set_option("trace", true);
277  }
278 
279  if(cmdline.isset("localize-faults"))
280  options.set_option("localize-faults", true);
281 
282  if(cmdline.isset("unwind"))
283  options.set_option("unwind", cmdline.get_value("unwind"));
284 
285  if(cmdline.isset("depth"))
286  options.set_option("depth", cmdline.get_value("depth"));
287 
288  if(cmdline.isset("debug-level"))
289  options.set_option("debug-level", cmdline.get_value("debug-level"));
290 
291  if(cmdline.isset("slice-by-trace"))
292  {
293  log.error() << "--slice-by-trace has been removed" << messaget::eom;
295  }
296 
297  if(cmdline.isset("unwindset"))
298  options.set_option("unwindset", cmdline.get_values("unwindset"));
299 
300  // constant propagation
301  if(cmdline.isset("no-propagation"))
302  options.set_option("propagation", false);
303 
304  // transform self loops to assumptions
305  options.set_option(
306  "self-loops-to-assumptions",
307  !cmdline.isset("no-self-loops-to-assumptions"));
308 
309  // all checks supported by goto_check
311 
312  // check assertions
313  if(cmdline.isset("no-assertions"))
314  options.set_option("assertions", false);
315 
316  // use assumptions
317  if(cmdline.isset("no-assumptions"))
318  options.set_option("assumptions", false);
319 
320  // magic error label
321  if(cmdline.isset("error-label"))
322  options.set_option("error-label", cmdline.get_values("error-label"));
323 
324  // generate unwinding assertions
325  if(cmdline.isset("unwinding-assertions"))
326  {
327  options.set_option("unwinding-assertions", true);
328  options.set_option("paths-symex-explore-all", true);
329  }
330 
331  if(cmdline.isset("partial-loops"))
332  options.set_option("partial-loops", true);
333 
334  // remove unused equations
335  if(cmdline.isset("slice-formula"))
336  options.set_option("slice-formula", true);
337 
338  // simplify if conditions and branches
339  if(cmdline.isset("no-simplify-if"))
340  options.set_option("simplify-if", false);
341 
342  if(cmdline.isset("arrays-uf-always"))
343  options.set_option("arrays-uf", "always");
344  else if(cmdline.isset("arrays-uf-never"))
345  options.set_option("arrays-uf", "never");
346 
347  if(cmdline.isset("dimacs"))
348  options.set_option("dimacs", true);
349 
350  if(cmdline.isset("refine-arrays"))
351  {
352  options.set_option("refine", true);
353  options.set_option("refine-arrays", true);
354  }
355 
356  if(cmdline.isset("refine-arithmetic"))
357  {
358  options.set_option("refine", true);
359  options.set_option("refine-arithmetic", true);
360  }
361 
362  if(cmdline.isset("refine"))
363  {
364  options.set_option("refine", true);
365  options.set_option("refine-arrays", true);
366  options.set_option("refine-arithmetic", true);
367  }
368 
369  if(cmdline.isset("refine-strings"))
370  {
371  options.set_option("refine-strings", true);
372  options.set_option("string-printable", cmdline.isset("string-printable"));
373  }
374 
375  if(cmdline.isset("max-node-refinement"))
376  options.set_option(
377  "max-node-refinement",
378  cmdline.get_value("max-node-refinement"));
379 
380  if(cmdline.isset("incremental-loop"))
381  {
382  options.set_option(
383  "incremental-loop", cmdline.get_value("incremental-loop"));
384  options.set_option("refine", true);
385  options.set_option("refine-arrays", true);
386 
387  if(cmdline.isset("unwind-min"))
388  options.set_option("unwind-min", cmdline.get_value("unwind-min"));
389 
390  if(cmdline.isset("unwind-max"))
391  options.set_option("unwind-max", cmdline.get_value("unwind-max"));
392 
393  if(cmdline.isset("ignore-properties-before-unwind-min"))
394  options.set_option("ignore-properties-before-unwind-min", true);
395 
396  if(cmdline.isset("paths"))
397  {
398  log.error() << "--paths not supported with --incremental-loop"
399  << messaget::eom;
401  }
402  }
403 
404  // SMT Options
405 
406  if(cmdline.isset("smt1"))
407  {
408  log.error() << "--smt1 is no longer supported" << messaget::eom;
410  }
411 
412  if(cmdline.isset("smt2"))
413  options.set_option("smt2", true);
414 
415  if(cmdline.isset("fpa"))
416  options.set_option("fpa", true);
417 
418  bool solver_set=false;
419 
420  if(cmdline.isset("boolector"))
421  {
422  options.set_option("boolector", true), solver_set=true;
423  options.set_option("smt2", true);
424  }
425 
426  if(cmdline.isset("cprover-smt2"))
427  {
428  options.set_option("cprover-smt2", true), solver_set = true;
429  options.set_option("smt2", true);
430  }
431 
432  if(cmdline.isset("mathsat"))
433  {
434  options.set_option("mathsat", true), solver_set=true;
435  options.set_option("smt2", true);
436  }
437 
438  if(cmdline.isset("cvc4"))
439  {
440  options.set_option("cvc4", true), solver_set=true;
441  options.set_option("smt2", true);
442  }
443 
444  if(cmdline.isset("external-sat-solver"))
445  {
446  options.set_option(
447  "external-sat-solver", cmdline.get_value("external-sat-solver")),
448  solver_set = true;
449  }
450 
451  if(cmdline.isset("yices"))
452  {
453  options.set_option("yices", true), solver_set=true;
454  options.set_option("smt2", true);
455  }
456 
457  if(cmdline.isset("z3"))
458  {
459  options.set_option("z3", true), solver_set=true;
460  options.set_option("smt2", true);
461  }
462 
463  if(cmdline.isset("smt2") && !solver_set)
464  {
465  if(cmdline.isset("outfile"))
466  {
467  // outfile and no solver should give standard compliant SMT-LIB
468  options.set_option("generic", true);
469  }
470  else
471  {
472  // the default smt2 solver
473  options.set_option("z3", true);
474  }
475  }
476 
477  if(cmdline.isset("write-solver-stats-to"))
478  {
479  options.set_option(
480  "write-solver-stats-to", cmdline.get_value("write-solver-stats-to"));
481  }
482 
483  if(cmdline.isset("beautify"))
484  options.set_option("beautify", true);
485 
486  if(cmdline.isset("no-sat-preprocessor"))
487  options.set_option("sat-preprocessor", false);
488 
489  if(cmdline.isset("no-pretty-names"))
490  options.set_option("pretty-names", false);
491 
492  if(cmdline.isset("outfile"))
493  options.set_option("outfile", cmdline.get_value("outfile"));
494 
495  if(cmdline.isset("graphml-witness"))
496  {
497  options.set_option("graphml-witness", cmdline.get_value("graphml-witness"));
498  options.set_option("stop-on-fail", true);
499  options.set_option("trace", true);
500  }
501 
502  if(cmdline.isset("symex-coverage-report"))
503  {
504  options.set_option(
505  "symex-coverage-report",
506  cmdline.get_value("symex-coverage-report"));
507  options.set_option("paths-symex-explore-all", true);
508  }
509 
510  if(cmdline.isset("validate-ssa-equation"))
511  {
512  options.set_option("validate-ssa-equation", true);
513  }
514 
515  if(cmdline.isset("validate-goto-model"))
516  {
517  options.set_option("validate-goto-model", true);
518  }
519 
520  if(cmdline.isset("show-goto-symex-steps"))
521  options.set_option("show-goto-symex-steps", true);
522 
524 }
525 
528 {
529  if(cmdline.isset("version"))
530  {
531  std::cout << CBMC_VERSION << '\n';
532  return CPROVER_EXIT_SUCCESS;
533  }
534 
535  //
536  // command line options
537  //
538 
539  optionst options;
540  get_command_line_options(options);
541 
544 
545  //
546  // Print a banner
547  //
548  log.status() << "CBMC version " << CBMC_VERSION << " " << sizeof(void *) * 8
549  << "-bit " << config.this_architecture() << " "
551 
552  //
553  // Unwinding of transition systems is done by hw-cbmc.
554  //
555 
556  if(cmdline.isset("module") ||
557  cmdline.isset("gen-interface"))
558  {
559  log.error() << "This version of CBMC has no support for "
560  " hardware modules. Please use hw-cbmc."
561  << messaget::eom;
563  }
564 
566 
567  // configure gcc, if required
569  {
570  gcc_versiont gcc_version;
571  gcc_version.get("gcc");
572  configure_gcc(gcc_version);
573  }
574 
575  if(cmdline.isset("test-preprocessor"))
579 
580  if(cmdline.isset("preprocess"))
581  {
582  preprocessing(options);
583  return CPROVER_EXIT_SUCCESS;
584  }
585 
586  if(cmdline.isset("show-parse-tree"))
587  {
588  if(
589  cmdline.args.size() != 1 ||
591  {
592  log.error() << "Please give exactly one source file" << messaget::eom;
594  }
595 
596  std::string filename=cmdline.args[0];
597 
598  #ifdef _MSC_VER
599  std::ifstream infile(widen(filename));
600  #else
601  std::ifstream infile(filename);
602  #endif
603 
604  if(!infile)
605  {
606  log.error() << "failed to open input file '" << filename << "'"
607  << messaget::eom;
609  }
610 
611  std::unique_ptr<languaget> language=
612  get_language_from_filename(filename);
613 
614  if(language==nullptr)
615  {
616  log.error() << "failed to figure out type of file '" << filename << "'"
617  << messaget::eom;
619  }
620 
621  language->set_language_options(options);
623 
624  log.status() << "Parsing " << filename << messaget::eom;
625 
626  if(language->parse(infile, filename))
627  {
628  log.error() << "PARSING ERROR" << messaget::eom;
630  }
631 
632  language->show_parse(std::cout);
633  return CPROVER_EXIT_SUCCESS;
634  }
635 
636  int get_goto_program_ret =
638 
639  if(get_goto_program_ret!=-1)
640  return get_goto_program_ret;
641 
642  if(cmdline.isset("show-claims") || // will go away
643  cmdline.isset("show-properties")) // use this one
644  {
646  return CPROVER_EXIT_SUCCESS;
647  }
648 
649  if(set_properties())
651 
652  if(
653  options.get_bool_option("program-only") ||
654  options.get_bool_option("show-vcc") ||
655  options.get_bool_option("show-byte-ops"))
656  {
657  if(options.get_bool_option("paths"))
658  {
660  options, ui_message_handler, goto_model);
661  (void)verifier();
662  }
663  else
664  {
666  options, ui_message_handler, goto_model);
667  (void)verifier();
668  }
669 
670  return CPROVER_EXIT_SUCCESS;
671  }
672 
673  if(
674  options.get_bool_option("dimacs") || !options.get_option("outfile").empty())
675  {
676  if(options.get_bool_option("paths"))
677  {
679  options, ui_message_handler, goto_model);
680  (void)verifier();
681  }
682  else
683  {
685  options, ui_message_handler, goto_model);
686  (void)verifier();
687  }
688 
689  return CPROVER_EXIT_SUCCESS;
690  }
691 
692  if(options.is_set("cover"))
693  {
695  verifier(options, ui_message_handler, goto_model);
696  (void)verifier();
697  verifier.report();
698 
699  c_test_input_generatort test_generator(ui_message_handler, options);
700  test_generator(verifier.get_traces());
701 
702  return CPROVER_EXIT_SUCCESS;
703  }
704 
705  std::unique_ptr<goto_verifiert> verifier = nullptr;
706 
707  if(options.is_set("incremental-loop"))
708  {
709  if(options.get_bool_option("stop-on-fail"))
710  {
711  verifier = util_make_unique<
713  options, ui_message_handler, goto_model);
714  }
715  else
716  {
719  options, ui_message_handler, goto_model);
720  }
721  }
722  else if(
723  options.get_bool_option("stop-on-fail") && options.get_bool_option("paths"))
724  {
725  verifier =
726  util_make_unique<stop_on_fail_verifiert<single_path_symex_checkert>>(
727  options, ui_message_handler, goto_model);
728  }
729  else if(
730  options.get_bool_option("stop-on-fail") &&
731  !options.get_bool_option("paths"))
732  {
733  if(options.get_bool_option("localize-faults"))
734  {
735  verifier =
738  }
739  else
740  {
741  verifier =
742  util_make_unique<stop_on_fail_verifiert<multi_path_symex_checkert>>(
743  options, ui_message_handler, goto_model);
744  }
745  }
746  else if(
747  !options.get_bool_option("stop-on-fail") &&
748  options.get_bool_option("paths"))
749  {
750  verifier = util_make_unique<
752  options, ui_message_handler, goto_model);
753  }
754  else if(
755  !options.get_bool_option("stop-on-fail") &&
756  !options.get_bool_option("paths"))
757  {
758  if(options.get_bool_option("localize-faults"))
759  {
760  verifier =
763  }
764  else
765  {
766  verifier = util_make_unique<
768  options, ui_message_handler, goto_model);
769  }
770  }
771  else
772  {
773  UNREACHABLE;
774  }
775 
776  const resultt result = (*verifier)();
777  verifier->report();
778 
779  return result_to_exit_code(result);
780 }
781 
783 {
784  if(cmdline.isset("claim")) // will go away
786 
787  if(cmdline.isset("property")) // use this one
789 
790  return false;
791 }
792 
794  goto_modelt &goto_model,
795  const optionst &options,
796  const cmdlinet &cmdline,
797  ui_message_handlert &ui_message_handler)
798 {
800  if(cmdline.args.empty())
801  {
802  log.error() << "Please provide a program to verify" << messaget::eom;
804  }
805 
807 
808  if(cmdline.isset("show-symbol-table"))
809  {
811  return CPROVER_EXIT_SUCCESS;
812  }
813 
816 
817  if(cmdline.isset("validate-goto-model"))
818  {
820  }
821 
822  // show it?
823  if(cmdline.isset("show-loops"))
824  {
826  return CPROVER_EXIT_SUCCESS;
827  }
828 
829  // show it?
830  if(
831  cmdline.isset("show-goto-functions") ||
832  cmdline.isset("list-goto-functions"))
833  {
835  goto_model, ui_message_handler, cmdline.isset("list-goto-functions"));
836  return CPROVER_EXIT_SUCCESS;
837  }
838 
840 
841  return -1; // no error, continue
842 }
843 
845 {
846  if(cmdline.args.size() != 1)
847  {
848  log.error() << "Please provide one program to preprocess" << messaget::eom;
849  return;
850  }
851 
852  std::string filename = cmdline.args[0];
853 
854  std::ifstream infile(filename);
855 
856  if(!infile)
857  {
858  log.error() << "failed to open input file" << messaget::eom;
859  return;
860  }
861 
862  std::unique_ptr<languaget> language = get_language_from_filename(filename);
863  language->set_language_options(options);
864 
865  if(language == nullptr)
866  {
867  log.error() << "failed to figure out type of file" << messaget::eom;
868  return;
869  }
870 
872 
873  if(language->preprocess(infile, filename, std::cout))
874  log.error() << "PREPROCESSING ERROR" << messaget::eom;
875 }
876 
878  goto_modelt &goto_model,
879  const optionst &options,
880  messaget &log)
881 {
882  // Remove inline assembler; this needs to happen before
883  // adding the library.
885 
886  // add the library
887  log.status() << "Adding CPROVER library (" << config.ansi_c.arch << ")"
888  << messaget::eom;
893 
895 
896  if(options.get_bool_option("string-abstraction"))
898 
899  // remove function pointers
900  log.status() << "Removal of function pointers and virtual functions"
901  << messaget::eom;
904  goto_model,
905  options.get_bool_option("pointer-check"));
906 
907  mm_io(goto_model);
908 
909  // instrument library preconditions
911 
912  // remove returns, gcc vectors, complex
917 
918  // add generic checks
919  log.status() << "Generic Property Instrumentation" << messaget::eom;
920  goto_check(options, goto_model);
921 
922  // checks don't know about adjusted float expressions
924 
925  // ignore default/user-specified initialization
926  // of variables with static lifetime
927  if(options.get_bool_option("nondet-static"))
928  {
929  log.status() << "Adding nondeterministic initialization "
930  "of static/global variables"
931  << messaget::eom;
933  }
934 
935  if(options.get_bool_option("string-abstraction"))
936  {
937  log.status() << "String Abstraction" << messaget::eom;
939  }
940 
941  // add failed symbols
942  // needs to be done before pointer analysis
944 
945  // recalculate numbers, etc.
947 
948  // add loop ids
950 
951  if(options.get_bool_option("drop-unused-functions"))
952  {
953  // Entry point will have been set before and function pointers removed
954  log.status() << "Removing unused functions" << messaget::eom;
956  }
957 
958  // remove skips such that trivial GOTOs are deleted and not considered
959  // for coverage annotation:
961 
962  // instrument cover goals
963  if(options.is_set("cover"))
964  {
965  const auto cover_config = get_cover_config(
968  cover_config, goto_model, log.get_message_handler()))
969  return true;
970  }
971 
972  // label the assertions
973  // This must be done after adding assertions and
974  // before using the argument of the "property" option.
975  // Do not re-label after using the property slicer because
976  // this would cause the property identifiers to change.
978 
979  // reachability slice?
980  if(options.get_bool_option("reachability-slice-fb"))
981  {
982  log.status() << "Performing a forwards-backwards reachability slice"
983  << messaget::eom;
984  if(options.is_set("property"))
986  goto_model, options.get_list_option("property"), true);
987  else
989  }
990 
991  if(options.get_bool_option("reachability-slice"))
992  {
993  log.status() << "Performing a reachability slice" << messaget::eom;
994  if(options.is_set("property"))
995  reachability_slicer(goto_model, options.get_list_option("property"));
996  else
998  }
999 
1000  // full slice?
1001  if(options.get_bool_option("full-slice"))
1002  {
1003  log.status() << "Performing a full slice" << messaget::eom;
1004  if(options.is_set("property"))
1005  property_slicer(goto_model, options.get_list_option("property"));
1006  else
1008  }
1009 
1010  // remove any skips introduced since coverage instrumentation
1012 
1013  return false;
1014 }
1015 
1018 {
1019  // clang-format off
1020  std::cout << '\n' << banner_string("CBMC", CBMC_VERSION) << '\n'
1021  << align_center_with_border("Copyright (C) 2001-2018") << '\n'
1022  << align_center_with_border("Daniel Kroening, Edmund Clarke") << '\n' // NOLINT(*)
1023  << align_center_with_border("Carnegie Mellon University, Computer Science Department") << '\n' // NOLINT(*)
1024  << align_center_with_border("kroening@kroening.com") << '\n' // NOLINT(*)
1025  << align_center_with_border("Protected in part by U.S. patent 7,225,417") << '\n' // NOLINT(*)
1026  <<
1027  "\n"
1028  "Usage: Purpose:\n"
1029  "\n"
1030  " cbmc [-?] [-h] [--help] show help\n"
1031  " cbmc file.c ... source file names\n"
1032  "\n"
1033  "Analysis options:\n"
1035  " --symex-coverage-report f generate a Cobertura XML coverage report in f\n" // NOLINT(*)
1036  " --property id only check one specific property\n"
1037  " --stop-on-fail stop analysis once a failed property is detected\n" // NOLINT(*)
1038  " --trace give a counterexample trace for failed properties\n" //NOLINT(*)
1039  "\n"
1040  "C/C++ frontend options:\n"
1041  " -I path set include path (C/C++)\n"
1042  " -D macro define preprocessor macro (C/C++)\n"
1043  " --preprocess stop after preprocessing\n"
1044  " --16, --32, --64 set width of int\n"
1045  " --LP64, --ILP64, --LLP64,\n"
1046  " --ILP32, --LP32 set width of int, long and pointers\n"
1047  " --little-endian allow little-endian word-byte conversions\n"
1048  " --big-endian allow big-endian word-byte conversions\n"
1049  " --unsigned-char make \"char\" unsigned by default\n"
1050  " --mm model set memory model (default: sc)\n"
1051  " --arch set architecture (default: "
1052  << configt::this_architecture() << ")\n"
1053  " --os set operating system (default: "
1054  << configt::this_operating_system() << ")\n"
1055  " --c89/99/11 set C language standard (default: "
1061  configt::ansi_ct::c_standardt::C11?"c11":"") << ")\n" // NOLINT(*)
1062  " --cpp98/03/11 set C++ language standard (default: "
1064  configt::cppt::cpp_standardt::CPP98?"cpp98": // NOLINT(*)
1066  configt::cppt::cpp_standardt::CPP03?"cpp03": // NOLINT(*)
1068  configt::cppt::cpp_standardt::CPP11?"cpp11":"") << ")\n" // NOLINT(*)
1069  #ifdef _WIN32
1070  " --gcc use GCC as preprocessor\n"
1071  #endif
1072  " --no-arch don't set up an architecture\n"
1073  " --no-library disable built-in abstract C library\n"
1074  " --round-to-nearest rounding towards nearest even (default)\n"
1075  " --round-to-plus-inf rounding towards plus infinity\n"
1076  " --round-to-minus-inf rounding towards minus infinity\n"
1077  " --round-to-zero rounding towards zero\n"
1080  "\n"
1081  "Program representations:\n"
1082  " --show-parse-tree show parse tree\n"
1083  " --show-symbol-table show loaded symbol table\n"
1085  "\n"
1086  "Program instrumentation options:\n"
1088  " --no-assertions ignore user assertions\n"
1089  " --no-assumptions ignore user assumptions\n"
1090  " --error-label label check that label is unreachable\n"
1091  " --cover CC create test-suite with coverage criterion CC\n" // NOLINT(*)
1092  " --mm MM memory consistency model for concurrent programs\n" // NOLINT(*)
1093  // NOLINTNEXTLINE(whitespace/line_length)
1094  " --malloc-fail-assert set malloc failure mode to assert-then-assume\n"
1095  " --malloc-fail-null set malloc failure mode to return null\n"
1096  // NOLINTNEXTLINE(whitespace/line_length)
1097  " --malloc-may-fail allow malloc calls to return a null pointer\n"
1100  " --full-slice run full slicer (experimental)\n" // NOLINT(*)
1101  " --drop-unused-functions drop functions trivially unreachable from main function\n" // NOLINT(*)
1102  " --havoc-undefined-functions\n"
1103  " for any function that has no body, assign non-deterministic values to\n" // NOLINT(*)
1104  " any parameters passed as non-const pointers and the return value\n" // NOLINT(*)
1105  "\n"
1106  "Semantic transformations:\n"
1107  // NOLINTNEXTLINE(whitespace/line_length)
1108  " --nondet-static add nondeterministic initialization of variables with static lifetime\n"
1109  "\n"
1110  "BMC options:\n"
1111  HELP_BMC
1112  "\n"
1113  "Backend options:\n"
1114  " --object-bits n number of bits used for object addresses\n"
1115  " --dimacs generate CNF in DIMACS format\n"
1116  " --beautify beautify the counterexample (greedy heuristic)\n" // NOLINT(*)
1117  " --localize-faults localize faults (experimental)\n"
1118  " --smt2 use default SMT2 solver (Z3)\n"
1119  " --boolector use Boolector\n"
1120  " --cprover-smt2 use CPROVER SMT2 solver\n"
1121  " --cvc4 use CVC4\n"
1122  " --mathsat use MathSAT\n"
1123  " --yices use Yices\n"
1124  " --z3 use Z3\n"
1125  " --refine use refinement procedure (experimental)\n"
1126  " --external-sat-solver cmd command to invoke SAT solver process\n"
1128  " --outfile filename output formula to given file\n"
1129  " --arrays-uf-never never turn arrays into uninterpreted functions\n" // NOLINT(*)
1130  " --arrays-uf-always always turn arrays into uninterpreted functions\n" // NOLINT(*)
1131  "\n"
1132  "Other options:\n"
1133  " --version show version and exit\n"
1138  HELP_FLUSH
1139  " --verbosity # verbosity level\n"
1141  " --write-solver-stats-to json-file\n"
1142  " collect the solver query complexity\n"
1143  "\n";
1144  // clang-format on
1145 }
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:91
cbmc_parse_optionst::doit
virtual int doit() override
invoke main modules
Definition: cbmc_parse_options.cpp:527
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:201
configt::cppt::cpp_standardt::CPP98
@ CPP98
HELP_SHOW_GOTO_FUNCTIONS
#define HELP_SHOW_GOTO_FUNCTIONS
Definition: show_goto_functions.h:26
string_abstraction.h
String Abstraction.
languaget::show_parse
virtual void show_parse(std::ostream &out)=0
configt::object_bits_info
std::string object_bits_info()
Definition: config.cpp:1291
configt::ansi_ct::set_c99
void set_c99()
Definition: config.h:53
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:61
rewrite_union.h
Symbolic Execution.
add_malloc_may_fail_variable_initializations.h
HELP_GOTO_TRACE
#define HELP_GOTO_TRACE
Definition: goto_trace.h:273
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:119
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:793
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
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
mm_io
void mm_io(const exprt &mm_io_r, const exprt &mm_io_w, goto_functionst::goto_functiont &goto_function, const namespacet &ns)
Definition: mm_io.cpp:32
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
instrument_preconditions.h
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
configt::cppt::cpp_standardt::CPP03
@ CPP03
cover_goals_verifier_with_trace_storaget::get_traces
const goto_trace_storaget & get_traces() const
Definition: cover_goals_verifier_with_trace_storage.h:59
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:368
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.
goto_check
void goto_check(const irep_idt &function_identifier, goto_functionst::goto_functiont &goto_function, const namespacet &ns, const optionst &options)
Definition: goto_check.cpp:2231
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
string_abstraction
void string_abstraction(symbol_tablet &symbol_table, message_handlert &message_handler, goto_programt &dest)
Definition: string_abstraction.cpp:65
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:87
nondet_static.h
Nondeterministically initializes global scope variables, except for constants (such as string literal...
string_instrumentation.h
String Abstraction.
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
remove_vector
static void remove_vector(typet &)
removes vector data type
Definition: remove_vector.cpp:166
configt::cppt::set_cpp98
void set_cpp98()
Definition: config.h:151
util_make_unique
std::unique_ptr< T > util_make_unique(Ts &&... ts)
Definition: make_unique.h:19
bmc_util.h
Bounded Model Checking Utilities.
remove_complex.h
Remove the 'complex' data type by compilation into structs.
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:176
configt::ansi_ct::c_standardt::C89
@ C89
full_slicer
void full_slicer(goto_functionst &goto_functions, const namespacet &ns, const slicing_criteriont &criterion)
Definition: full_slicer.cpp:345
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.
string_instrumentation
void string_instrumentation(symbol_tablet &symbol_table, message_handlert &message_handler, goto_programt &dest)
Definition: string_instrumentation.cpp:157
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
mm_io.h
Perform Memory-mapped I/O instrumentation.
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:130
configt::ansi_ct::preprocessor
preprocessort preprocessor
Definition: config.h:120
instrument_preconditions
void instrument_preconditions(const goto_modelt &goto_model, goto_programt &goto_program)
Definition: instrument_preconditions.cpp:90
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:368
show_properties.h
Show the properties.
configt::cppt::set_cpp11
void set_cpp11()
Definition: config.h:153
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
rewrite_union
void rewrite_union(exprt &expr)
We rewrite u.c for unions u into byte_extract(u, 0), and { .c = v } into byte_update(NIL,...
Definition: rewrite_union.cpp:66
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:877
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:1402
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:85
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
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:782
goto_functionst::compute_loop_numbers
void compute_loop_numbers()
Definition: goto_functions.cpp:52
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
configt::ansi_ct::default_c_standard
static c_standardt default_c_standard()
Definition: config.cpp:675
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:22
remove_vector.h
Remove the 'vector' data type by compilation into arrays.
remove_complex
static void remove_complex(typet &)
removes complex data type
Definition: remove_complex.cpp:231
goto_verifiert::report
virtual void report()=0
Report results.
remove_returns.h
Replace function returns by assignments to global variables.
remove_unused_functions.h
Unused function removal.
config
configt config
Definition: config.cpp:24
configt::ansi_ct::c_standardt::C99
@ C99
gcc_versiont
Definition: gcc_version.h:20
parse_options_baset::log
messaget log
Definition: parse_options.h:43
configt::ansi_ct::set_c11
void set_c11()
Definition: config.h:54
configt::this_architecture
static irep_idt this_architecture()
Definition: config.cpp:1302
configt::ansi_ct::c_standardt::C11
@ C11
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
configt::ansi_ct::set_c89
void set_c89()
Definition: config.h:52
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
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:45
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
configt::cppt::default_cpp_standard
static cpp_standardt default_cpp_standard()
Definition: config.cpp:690
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
remove_returns
void remove_returns(symbol_table_baset &symbol_table, goto_functionst &goto_functions)
removes returns
Definition: remove_returns.cpp:256
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:1017
goto_functionst::update
void update()
Definition: goto_functions.h:81
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:512
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:281
adjust_float_expressions
void adjust_float_expressions(exprt &expr, const exprt &rounding_mode)
Replaces arithmetic operations and typecasts involving floating point numbers with their equivalent f...
Definition: adjust_float_expressions.cpp:78
configt::cppt::cpp_standardt::CPP11
@ CPP11
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
configt::cpp
struct configt::cppt cpp
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:112
adjust_float_expressions.h
Symbolic Execution.
remove_function_pointers
bool remove_function_pointers(message_handlert &_message_handler, symbol_tablet &symbol_table, const goto_functionst &goto_functions, goto_programt &goto_program, const irep_idt &function_id, bool add_safety_assertion, bool only_remove_const_fps)
Definition: remove_function_pointers.cpp:519
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
remove_function_pointers.h
Remove Indirect Function Calls.
cover_goals_verifier_with_trace_storaget::report
void report() override
Report results.
Definition: cover_goals_verifier_with_trace_storage.h:54
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
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:41
configt::cppt::set_cpp03
void set_cpp03()
Definition: config.h:152
cbmc_parse_optionst::preprocessing
void preprocessing(const optionst &)
Definition: cbmc_parse_options.cpp:844
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:824
HELP_VALIDATE
#define HELP_VALIDATE
Definition: validation_interface.h:16