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/unicode.h>
24 #include <util/version.h>
25 
26 #include <langapi/language.h>
27 
28 #include <ansi-c/c_preprocess.h>
29 #include <ansi-c/cprover_library.h>
30 
31 #include <cpp/cprover_library.h>
32 
37 #include <goto-programs/loop_ids.h>
38 #include <goto-programs/mm_io.h>
54 
58 #include <goto-instrument/cover.h>
59 
61 
62 #include <langapi/mode.h>
63 
64 #include "xml_interface.h"
65 
66 cbmc_parse_optionst::cbmc_parse_optionst(int argc, const char **argv)
67  : parse_options_baset(CBMC_OPTIONS, argc, argv),
68  xml_interfacet(cmdline),
69  messaget(ui_message_handler),
70  ui_message_handler(cmdline, std::string("CBMC ") + CBMC_VERSION),
71  path_strategy_chooser()
72 {
73 }
74 
76  int argc,
77  const char **argv,
78  const std::string &extra_options)
79  : parse_options_baset(CBMC_OPTIONS + extra_options, argc, argv),
80  xml_interfacet(cmdline),
81  messaget(ui_message_handler),
82  ui_message_handler(cmdline, std::string("CBMC ") + CBMC_VERSION),
83  path_strategy_chooser()
84 {
85 }
86 
88 {
89  // Default true
90  options.set_option("assertions", true);
91  options.set_option("assumptions", true);
92  options.set_option("built-in-assertions", true);
93  options.set_option("pretty-names", true);
94  options.set_option("propagation", true);
95  options.set_option("sat-preprocessor", true);
96  options.set_option("simplify", true);
97  options.set_option("simplify-if", true);
98 
99  // Other default
100  options.set_option("arrays-uf", "auto");
101 }
102 
104 {
105  if(config.set(cmdline))
106  {
107  usage_error();
109  }
110 
113 
114  if(cmdline.isset("function"))
115  options.set_option("function", cmdline.get_value("function"));
116 
117  if(cmdline.isset("cover") && cmdline.isset("unwinding-assertions"))
118  {
119  error() << "--cover and --unwinding-assertions must not be given together"
120  << eom;
122  }
123 
124  if(cmdline.isset("partial-loops") && cmdline.isset("unwinding-assertions"))
125  {
126  error() << "--partial-loops and --unwinding-assertions must not be given "
127  << "together" << eom;
129  }
130 
131  if(cmdline.isset("reachability-slice") &&
132  cmdline.isset("reachability-slice-fb"))
133  {
134  error() << "--reachability-slice and --reachability-slice-fb must not be "
135  << "given together" << eom;
137  }
138 
139  if(cmdline.isset("full-slice"))
140  options.set_option("full-slice", true);
141 
142  if(cmdline.isset("show-symex-strategies"))
143  {
144  std::cout << path_strategy_chooser.show_strategies();
145  exit(CPROVER_EXIT_SUCCESS);
146  }
147 
149 
150  if(cmdline.isset("program-only"))
151  options.set_option("program-only", true);
152 
153  if(cmdline.isset("show-vcc"))
154  options.set_option("show-vcc", true);
155 
156  if(cmdline.isset("cover"))
157  parse_cover_options(cmdline, options);
158 
159  if(cmdline.isset("mm"))
160  options.set_option("mm", cmdline.get_value("mm"));
161 
162  if(cmdline.isset("c89"))
164 
165  if(cmdline.isset("c99"))
167 
168  if(cmdline.isset("c11"))
170 
171  if(cmdline.isset("cpp98"))
172  config.cpp.set_cpp98();
173 
174  if(cmdline.isset("cpp03"))
175  config.cpp.set_cpp03();
176 
177  if(cmdline.isset("cpp11"))
178  config.cpp.set_cpp11();
179 
180  if(cmdline.isset("property"))
181  options.set_option("property", cmdline.get_values("property"));
182 
183  if(cmdline.isset("drop-unused-functions"))
184  options.set_option("drop-unused-functions", true);
185 
186  if(cmdline.isset("string-abstraction"))
187  options.set_option("string-abstraction", true);
188 
189  if(cmdline.isset("reachability-slice-fb"))
190  options.set_option("reachability-slice-fb", true);
191 
192  if(cmdline.isset("reachability-slice"))
193  options.set_option("reachability-slice", true);
194 
195  if(cmdline.isset("nondet-static"))
196  options.set_option("nondet-static", true);
197 
198  if(cmdline.isset("no-simplify"))
199  options.set_option("simplify", false);
200 
201  if(cmdline.isset("stop-on-fail") ||
202  cmdline.isset("dimacs") ||
203  cmdline.isset("outfile"))
204  options.set_option("stop-on-fail", true);
205 
206  if(
207  cmdline.isset("trace") || cmdline.isset("compact-trace") ||
208  cmdline.isset("stack-trace") || cmdline.isset("stop-on-fail"))
209  {
210  options.set_option("trace", true);
211  }
212 
213  if(cmdline.isset("localize-faults"))
214  options.set_option("localize-faults", true);
215  if(cmdline.isset("localize-faults-method"))
216  {
217  options.set_option(
218  "localize-faults-method",
219  cmdline.get_value("localize-faults-method"));
220  }
221 
222  if(cmdline.isset("unwind"))
223  options.set_option("unwind", cmdline.get_value("unwind"));
224 
225  if(cmdline.isset("depth"))
226  options.set_option("depth", cmdline.get_value("depth"));
227 
228  if(cmdline.isset("debug-level"))
229  options.set_option("debug-level", cmdline.get_value("debug-level"));
230 
231  if(cmdline.isset("slice-by-trace"))
232  options.set_option("slice-by-trace", cmdline.get_value("slice-by-trace"));
233 
234  if(cmdline.isset("unwindset"))
235  options.set_option("unwindset", cmdline.get_value("unwindset"));
236 
237  // constant propagation
238  if(cmdline.isset("no-propagation"))
239  options.set_option("propagation", false);
240 
241  // transform self loops to assumptions
242  options.set_option(
243  "self-loops-to-assumptions",
244  !cmdline.isset("no-self-loops-to-assumptions"));
245 
246  // all checks supported by goto_check
248 
249  // check assertions
250  if(cmdline.isset("no-assertions"))
251  options.set_option("assertions", false);
252 
253  // use assumptions
254  if(cmdline.isset("no-assumptions"))
255  options.set_option("assumptions", false);
256 
257  // magic error label
258  if(cmdline.isset("error-label"))
259  options.set_option("error-label", cmdline.get_values("error-label"));
260 
261  // generate unwinding assertions
262  if(cmdline.isset("unwinding-assertions"))
263  options.set_option("unwinding-assertions", true);
264 
265  if(cmdline.isset("partial-loops"))
266  options.set_option("partial-loops", true);
267 
268  // remove unused equations
269  if(cmdline.isset("slice-formula"))
270  options.set_option("slice-formula", true);
271 
272  // simplify if conditions and branches
273  if(cmdline.isset("no-simplify-if"))
274  options.set_option("simplify-if", false);
275 
276  if(cmdline.isset("arrays-uf-always"))
277  options.set_option("arrays-uf", "always");
278  else if(cmdline.isset("arrays-uf-never"))
279  options.set_option("arrays-uf", "never");
280 
281  if(cmdline.isset("dimacs"))
282  options.set_option("dimacs", true);
283 
284  if(cmdline.isset("refine-arrays"))
285  {
286  options.set_option("refine", true);
287  options.set_option("refine-arrays", true);
288  }
289 
290  if(cmdline.isset("refine-arithmetic"))
291  {
292  options.set_option("refine", true);
293  options.set_option("refine-arithmetic", true);
294  }
295 
296  if(cmdline.isset("refine"))
297  {
298  options.set_option("refine", true);
299  options.set_option("refine-arrays", true);
300  options.set_option("refine-arithmetic", true);
301  }
302 
303  if(cmdline.isset("refine-strings"))
304  {
305  options.set_option("refine-strings", true);
306  options.set_option("string-printable", cmdline.isset("string-printable"));
307  }
308 
309  if(cmdline.isset("max-node-refinement"))
310  options.set_option(
311  "max-node-refinement",
312  cmdline.get_value("max-node-refinement"));
313 
314  // SMT Options
315 
316  if(cmdline.isset("smt1"))
317  {
318  error() << "--smt1 is no longer supported" << eom;
320  }
321 
322  if(cmdline.isset("smt2"))
323  options.set_option("smt2", true);
324 
325  if(cmdline.isset("fpa"))
326  options.set_option("fpa", true);
327 
328  bool solver_set=false;
329 
330  if(cmdline.isset("boolector"))
331  {
332  options.set_option("boolector", true), solver_set=true;
333  options.set_option("smt2", true);
334  }
335 
336  if(cmdline.isset("cprover-smt2"))
337  {
338  options.set_option("cprover-smt2", true), solver_set = true;
339  options.set_option("smt2", true);
340  }
341 
342  if(cmdline.isset("mathsat"))
343  {
344  options.set_option("mathsat", true), solver_set=true;
345  options.set_option("smt2", true);
346  }
347 
348  if(cmdline.isset("cvc4"))
349  {
350  options.set_option("cvc4", true), solver_set=true;
351  options.set_option("smt2", true);
352  }
353 
354  if(cmdline.isset("yices"))
355  {
356  options.set_option("yices", true), solver_set=true;
357  options.set_option("smt2", true);
358  }
359 
360  if(cmdline.isset("z3"))
361  {
362  options.set_option("z3", true), solver_set=true;
363  options.set_option("smt2", true);
364  }
365 
366  if(cmdline.isset("smt2") && !solver_set)
367  {
368  if(cmdline.isset("outfile"))
369  {
370  // outfile and no solver should give standard compliant SMT-LIB
371  options.set_option("generic", true);
372  }
373  else
374  {
375  // the default smt2 solver
376  options.set_option("z3", true);
377  }
378  }
379 
380  if(cmdline.isset("beautify"))
381  options.set_option("beautify", true);
382 
383  if(cmdline.isset("no-sat-preprocessor"))
384  options.set_option("sat-preprocessor", false);
385 
386  if(cmdline.isset("no-pretty-names"))
387  options.set_option("pretty-names", false);
388 
389  if(cmdline.isset("outfile"))
390  options.set_option("outfile", cmdline.get_value("outfile"));
391 
392  if(cmdline.isset("graphml-witness"))
393  {
394  options.set_option("graphml-witness", cmdline.get_value("graphml-witness"));
395  options.set_option("stop-on-fail", true);
396  options.set_option("trace", true);
397  }
398 
399  if(cmdline.isset("symex-coverage-report"))
400  options.set_option(
401  "symex-coverage-report",
402  cmdline.get_value("symex-coverage-report"));
403 
404  if(cmdline.isset("validate-ssa-equation"))
405  {
406  options.set_option("validate-ssa-equation", true);
407  }
408 
409  if(cmdline.isset("validate-goto-model"))
410  {
411  options.set_option("validate-goto-model", true);
412  }
413 
415 }
416 
419 {
420  if(cmdline.isset("version"))
421  {
422  std::cout << CBMC_VERSION << '\n';
423  return CPROVER_EXIT_SUCCESS;
424  }
425 
426  //
427  // command line options
428  //
429 
430  optionst options;
431  try
432  {
433  get_command_line_options(options);
434  }
435 
436  catch(const char *error_msg)
437  {
438  error() << error_msg << eom;
439  return CPROVER_EXIT_EXCEPTION;
440  }
441 
442  catch(const std::string &error_msg)
443  {
444  error() << error_msg << eom;
445  return CPROVER_EXIT_EXCEPTION;
446  }
447 
450 
451  //
452  // Print a banner
453  //
454  status() << "CBMC version " << CBMC_VERSION << " " << sizeof(void *) * 8
455  << "-bit " << config.this_architecture() << " "
457 
458  //
459  // Unwinding of transition systems is done by hw-cbmc.
460  //
461 
462  if(cmdline.isset("module") ||
463  cmdline.isset("gen-interface"))
464  {
465  error() << "This version of CBMC has no support for "
466  " hardware modules. Please use hw-cbmc." << eom;
468  }
469 
471 
472  if(cmdline.isset("test-preprocessor"))
476 
477  if(cmdline.isset("preprocess"))
478  {
479  preprocessing(options);
480  return CPROVER_EXIT_SUCCESS;
481  }
482 
483  if(cmdline.isset("show-parse-tree"))
484  {
485  if(cmdline.args.size()!=1 ||
487  {
488  error() << "Please give exactly one source file" << eom;
490  }
491 
492  std::string filename=cmdline.args[0];
493 
494  #ifdef _MSC_VER
495  std::ifstream infile(widen(filename));
496  #else
497  std::ifstream infile(filename);
498  #endif
499 
500  if(!infile)
501  {
502  error() << "failed to open input file `"
503  << filename << "'" << eom;
505  }
506 
507  std::unique_ptr<languaget> language=
508  get_language_from_filename(filename);
509 
510  if(language==nullptr)
511  {
512  error() << "failed to figure out type of file `"
513  << filename << "'" << eom;
515  }
516 
517  language->set_language_options(options);
519 
520  status() << "Parsing " << filename << eom;
521 
522  if(language->parse(infile, filename))
523  {
524  error() << "PARSING ERROR" << eom;
526  }
527 
528  language->show_parse(std::cout);
529  return CPROVER_EXIT_SUCCESS;
530  }
531 
532  int get_goto_program_ret =
534 
535  if(get_goto_program_ret!=-1)
536  return get_goto_program_ret;
537 
538  if(cmdline.isset("show-claims") || // will go away
539  cmdline.isset("show-properties")) // use this one
540  {
543  return CPROVER_EXIT_SUCCESS;
544  }
545 
546  if(set_properties())
548 
549  if(cmdline.isset("validate-goto-model"))
550  {
552  }
553 
556 }
557 
559 {
560  try
561  {
562  if(cmdline.isset("claim")) // will go away
564 
565  if(cmdline.isset("property")) // use this one
567  }
568 
569  catch(const char *e)
570  {
571  error() << e << eom;
572  return true;
573  }
574 
575  catch(const std::string &e)
576  {
577  error() << e << eom;
578  return true;
579  }
580 
581  catch(int e)
582  {
583  error() << "Numeric exception : " << e << eom;
584  return true;
585  }
586 
587  return false;
588 }
589 
591  goto_modelt &goto_model,
592  const optionst &options,
593  const cmdlinet &cmdline,
594  messaget &log,
595  ui_message_handlert &ui_message_handler)
596 {
597  if(cmdline.args.empty())
598  {
599  log.error() << "Please provide a program to verify" << log.eom;
601  }
602 
603  try
604  {
605  goto_model =
607 
608  if(cmdline.isset("show-symbol-table"))
609  {
611  return CPROVER_EXIT_SUCCESS;
612  }
613 
616 
617  // show it?
618  if(cmdline.isset("show-loops"))
619  {
621  return CPROVER_EXIT_SUCCESS;
622  }
623 
624  // show it?
625  if(
626  cmdline.isset("show-goto-functions") ||
627  cmdline.isset("list-goto-functions"))
628  {
630  goto_model,
633  cmdline.isset("list-goto-functions"));
634  return CPROVER_EXIT_SUCCESS;
635  }
636 
637  log.status() << config.object_bits_info() << log.eom;
638  }
639 
641  {
642  log.error() << e.what() << log.eom;
643  return CPROVER_EXIT_EXCEPTION;
644  }
645 
646  catch(const char *e)
647  {
648  log.error() << e << log.eom;
649  return CPROVER_EXIT_EXCEPTION;
650  }
651 
652  catch(const std::string &e)
653  {
654  log.error() << e << log.eom;
655  return CPROVER_EXIT_EXCEPTION;
656  }
657 
658  catch(int e)
659  {
660  log.error() << "Numeric exception : " << e << log.eom;
661  return CPROVER_EXIT_EXCEPTION;
662  }
663 
664  catch(const std::bad_alloc &)
665  {
666  log.error() << "Out of memory" << log.eom;
668  }
669 
670  return -1; // no error, continue
671 }
672 
674 {
675  try
676  {
677  if(cmdline.args.size()!=1)
678  {
679  error() << "Please provide one program to preprocess" << eom;
680  return;
681  }
682 
683  std::string filename=cmdline.args[0];
684 
685  std::ifstream infile(filename);
686 
687  if(!infile)
688  {
689  error() << "failed to open input file" << eom;
690  return;
691  }
692 
693  std::unique_ptr<languaget> language=get_language_from_filename(filename);
694  language->set_language_options(options);
695 
696  if(language==nullptr)
697  {
698  error() << "failed to figure out type of file" << eom;
699  return;
700  }
701 
703 
704  if(language->preprocess(infile, filename, std::cout))
705  error() << "PREPROCESSING ERROR" << eom;
706  }
707 
708  catch(const char *e)
709  {
710  error() << e << eom;
711  }
712 
713  catch(const std::string &e)
714  {
715  error() << e << eom;
716  }
717 
718  catch(int e)
719  {
720  error() << "Numeric exception : " << e << eom;
721  }
722 
723  catch(const std::bad_alloc &)
724  {
725  error() << "Out of memory" << eom;
727  }
728 }
729 
731  goto_modelt &goto_model,
732  const optionst &options,
733  messaget &log)
734 {
735  try
736  {
737  // Remove inline assembler; this needs to happen before
738  // adding the library.
740 
741  // add the library
742  log.status() << "Adding CPROVER library (" << config.ansi_c.arch << ")"
743  << eom;
748 
749  if(options.get_bool_option("string-abstraction"))
751 
752  // remove function pointers
753  log.status() << "Removal of function pointers and virtual functions" << eom;
755  log.get_message_handler(),
756  goto_model,
757  options.get_bool_option("pointer-check"));
758 
759  mm_io(goto_model);
760 
761  // instrument library preconditions
763 
764  // remove returns, gcc vectors, complex
769 
770  // add generic checks
771  log.status() << "Generic Property Instrumentation" << eom;
772  goto_check(options, goto_model);
773 
774  // checks don't know about adjusted float expressions
776 
777  // ignore default/user-specified initialization
778  // of variables with static lifetime
779  if(options.get_bool_option("nondet-static"))
780  {
781  log.status() << "Adding nondeterministic initialization "
782  "of static/global variables"
783  << eom;
785  }
786 
787  if(options.get_bool_option("string-abstraction"))
788  {
789  log.status() << "String Abstraction" << eom;
791  }
792 
793  // add failed symbols
794  // needs to be done before pointer analysis
796 
797  // recalculate numbers, etc.
799 
800  // add loop ids
802 
803  if(options.get_bool_option("drop-unused-functions"))
804  {
805  // Entry point will have been set before and function pointers removed
806  log.status() << "Removing unused functions" << eom;
808  }
809 
810  // remove skips such that trivial GOTOs are deleted and not considered
811  // for coverage annotation:
813 
814  // instrument cover goals
815  if(options.is_set("cover"))
816  {
818  return true;
819  }
820 
821  // label the assertions
822  // This must be done after adding assertions and
823  // before using the argument of the "property" option.
824  // Do not re-label after using the property slicer because
825  // this would cause the property identifiers to change.
827 
828  // reachability slice?
829  if(options.get_bool_option("reachability-slice-fb"))
830  {
831  log.status() << "Performing a forwards-backwards reachability slice"
832  << eom;
833  if(options.is_set("property"))
835  goto_model, options.get_list_option("property"), true);
836  else
838  }
839 
840  if(options.get_bool_option("reachability-slice"))
841  {
842  log.status() << "Performing a reachability slice" << eom;
843  if(options.is_set("property"))
844  reachability_slicer(goto_model, options.get_list_option("property"));
845  else
847  }
848 
849  // full slice?
850  if(options.get_bool_option("full-slice"))
851  {
852  log.status() << "Performing a full slice" << eom;
853  if(options.is_set("property"))
854  property_slicer(goto_model, options.get_list_option("property"));
855  else
857  }
858 
859  // remove any skips introduced since coverage instrumentation
861  }
862 
863  catch(const char *e)
864  {
865  log.error() << e << eom;
866  return true;
867  }
868 
869  catch(const std::string &e)
870  {
871  log.error() << e << eom;
872  return true;
873  }
874 
875  catch(int e)
876  {
877  log.error() << "Numeric exception : " << e << eom;
878  return true;
879  }
880 
881  catch(const std::bad_alloc &)
882  {
883  log.error() << "Out of memory" << eom;
885  return true;
886  }
887 
888  return false;
889 }
890 
893 {
894  // clang-format off
895  std::cout << '\n' << banner_string("CBMC", CBMC_VERSION) << '\n'
896  <<
897  "* * Copyright (C) 2001-2018 * *\n"
898  "* * Daniel Kroening, Edmund Clarke * *\n"
899  "* * Carnegie Mellon University, Computer Science Department * *\n"
900  "* * kroening@kroening.com * *\n"
901  "* * Protected in part by U.S. patent 7,225,417 * *\n"
902  "\n"
903  "Usage: Purpose:\n"
904  "\n"
905  " cbmc [-?] [-h] [--help] show help\n"
906  " cbmc file.c ... source file names\n"
907  "\n"
908  "Analysis options:\n"
910  " --symex-coverage-report f generate a Cobertura XML coverage report in f\n" // NOLINT(*)
911  " --property id only check one specific property\n"
912  " --stop-on-fail stop analysis once a failed property is detected\n" // NOLINT(*)
913  " --trace give a counterexample trace for failed properties\n" //NOLINT(*)
914  "\n"
915  "C/C++ frontend options:\n"
916  " -I path set include path (C/C++)\n"
917  " -D macro define preprocessor macro (C/C++)\n"
918  " --preprocess stop after preprocessing\n"
919  " --16, --32, --64 set width of int\n"
920  " --LP64, --ILP64, --LLP64,\n"
921  " --ILP32, --LP32 set width of int, long and pointers\n"
922  " --little-endian allow little-endian word-byte conversions\n"
923  " --big-endian allow big-endian word-byte conversions\n"
924  " --unsigned-char make \"char\" unsigned by default\n"
925  " --mm model set memory model (default: sc)\n"
926  " --arch set architecture (default: "
927  << configt::this_architecture() << ")\n"
928  " --os set operating system (default: "
929  << configt::this_operating_system() << ")\n"
930  " --c89/99/11 set C language standard (default: "
936  configt::ansi_ct::c_standardt::C11?"c11":"") << ")\n" // NOLINT(*)
937  " --cpp98/03/11 set C++ language standard (default: "
939  configt::cppt::cpp_standardt::CPP98?"cpp98": // NOLINT(*)
941  configt::cppt::cpp_standardt::CPP03?"cpp03": // NOLINT(*)
943  configt::cppt::cpp_standardt::CPP11?"cpp11":"") << ")\n" // NOLINT(*)
944  #ifdef _WIN32
945  " --gcc use GCC as preprocessor\n"
946  #endif
947  " --no-arch don't set up an architecture\n"
948  " --no-library disable built-in abstract C library\n"
949  " --round-to-nearest rounding towards nearest even (default)\n"
950  " --round-to-plus-inf rounding towards plus infinity\n"
951  " --round-to-minus-inf rounding towards minus infinity\n"
952  " --round-to-zero rounding towards zero\n"
955  "\n"
956  "Program representations:\n"
957  " --show-parse-tree show parse tree\n"
958  " --show-symbol-table show loaded symbol table\n"
960  "\n"
961  "Program instrumentation options:\n"
963  " --no-assertions ignore user assertions\n"
964  " --no-assumptions ignore user assumptions\n"
965  " --error-label label check that label is unreachable\n"
966  " --cover CC create test-suite with coverage criterion CC\n" // NOLINT(*)
967  " --mm MM memory consistency model for concurrent programs\n" // NOLINT(*)
970  " --full-slice run full slicer (experimental)\n" // NOLINT(*)
971  " --drop-unused-functions drop functions trivially unreachable from main function\n" // NOLINT(*)
972  "\n"
973  "Semantic transformations:\n"
974  // NOLINTNEXTLINE(whitespace/line_length)
975  " --nondet-static add nondeterministic initialization of variables with static lifetime\n"
976  "\n"
977  "BMC options:\n"
978  HELP_BMC
979  "\n"
980  "Backend options:\n"
981  " --object-bits n number of bits used for object addresses\n"
982  " --dimacs generate CNF in DIMACS format\n"
983  " --beautify beautify the counterexample (greedy heuristic)\n" // NOLINT(*)
984  " --localize-faults localize faults (experimental)\n"
985  " --smt2 use default SMT2 solver (Z3)\n"
986  " --boolector use Boolector\n"
987  " --cprover-smt2 use CPROVER SMT2 solver\n"
988  " --cvc4 use CVC4\n"
989  " --mathsat use MathSAT\n"
990  " --yices use Yices\n"
991  " --z3 use Z3\n"
992  " --refine use refinement procedure (experimental)\n"
994  " --outfile filename output formula to given file\n"
995  " --arrays-uf-never never turn arrays into uninterpreted functions\n" // NOLINT(*)
996  " --arrays-uf-always always turn arrays into uninterpreted functions\n" // NOLINT(*)
997  "\n"
998  "Other options:\n"
999  " --version show version and exit\n"
1000  " --xml-ui use XML-formatted output\n"
1001  " --xml-interface bi-directional XML interface\n"
1002  " --json-ui use JSON-formatted output\n"
1003  // NOLINTNEXTLINE(whitespace/line_length)
1006  HELP_FLUSH
1007  " --verbosity # verbosity level\n"
1009  "\n";
1010  // clang-format on
1011 }
const std::list< std::string > & get_values(const std::string &option) const
Definition: cmdline.cpp:110
Symbolic Execution.
void show_loop_ids(ui_message_handlert::uit ui, const goto_modelt &goto_model)
Definition: loop_ids.cpp:21
struct configt::ansi_ct ansi_c
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.
void string_abstraction(symbol_tablet &symbol_table, message_handlert &message_handler, goto_programt &dest)
#define HELP_REACHABILITY_SLICER
void instrument_preconditions(const goto_modelt &goto_model, goto_programt &goto_program)
void get_command_line_options(optionst &)
static int get_goto_program(goto_modelt &, const optionst &, const cmdlinet &, messaget &, ui_message_handlert &)
Remove Indirect Function Calls.
std::wstring widen(const char *s)
Definition: unicode.cpp:52
uit get_ui() const
Definition: ui_message.h:30
std::string object_bits_info()
Definition: config.cpp:1257
void compute_loop_numbers()
#define HELP_VALIDATE
Show the symbol table.
#define HELP_ANSI_C_LANGUAGE
Show the goto functions.
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:98
bool is_goto_binary(const std::string &filename)
Read Goto Programs.
Remove the 'complex' data type by compilation into structs.
#define HELP_REACHABILITY_SLICER_FB
std::string get_value(char option) const
Definition: cmdline.cpp:45
void set_cpp98()
Definition: config.h:140
void remove_unused_functions(goto_modelt &goto_model, message_handlert &message_handler)
#define HELP_STRING_REFINEMENT_CBMC
const value_listt & get_list_option(const std::string &option) const
Definition: options.cpp:78
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
virtual bool preprocess(std::istream &instream, const std::string &path, std::ostream &outstream)
Definition: language.h:49
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
Pointer Dereferencing.
#define CPROVER_EXIT_INTERNAL_ERROR
An error has been encountered during processing the requested analysis.
Definition: exit_codes.h:46
void show_goto_functions(const namespacet &ns, message_handlert &message_handler, ui_message_handlert::uit ui, const goto_functionst &goto_functions, bool list_only)
String Abstraction.
configt config
Definition: config.cpp:24
Remove 'asm' statements by compiling them into suitable standard goto program instructions.
#define HELP_FUNCTIONS
const path_strategy_choosert path_strategy_chooser
void cprover_c_library_factory(const std::set< irep_idt > &functions, symbol_tablet &symbol_table, message_handlert &message_handler)
void adjust_float_expressions(exprt &expr, const exprt &rounding_mode)
This adds the rounding mode to floating-point operations, including those in vectors and complex numb...
#define CPROVER_EXIT_SUCCESS
Success indicates the required analysis has been performed without error.
Definition: exit_codes.h:16
void parse_cover_options(const cmdlinet &cmdline, optionst &options)
Parses coverage-related command line options.
Definition: cover.cpp:160
Set the properties to check.
#define HELP_GOTO_CHECK
Definition: goto_check.h:43
static bool process_goto_program(goto_modelt &, const optionst &, messaget &)
Unused function removal.
#define PARSE_OPTIONS_GOTO_TRACE(cmdline, options)
Definition: goto_trace.h:267
bool set(const cmdlinet &cmdline)
Definition: config.cpp:767
void set_c89()
Definition: config.h:51
void preprocessing(const optionst &)
Perform Memory-mapped I/O instrumentation.
#define HELP_TIMESTAMP
Definition: timestamper.h:14
argst args
Definition: cmdline.h:44
std::string show_strategies() const
suitable for displaying as a front-end help message
void string_instrumentation(symbol_tablet &symbol_table, message_handlert &message_handler, goto_programt &dest)
virtual bool isset(char option) const
Definition: cmdline.cpp:27
#define CBMC_OPTIONS
void set_path_strategy_options(const cmdlinet &, optionst &, messaget &) const
add paths and exploration-strategy option, suitable to be invoked from front-ends.
Initialize a Goto Program.
String Abstraction.
#define HELP_SHOW_PROPERTIES
void show_symbol_table(const symbol_tablet &symbol_table, ui_message_handlert &ui)
Nondeterministically initializes global scope variables, except for constants (such as string literal...
#define HELP_FLUSH
Definition: ui_message.h:104
bool get_bool_option(const std::string &option) const
Definition: options.cpp:42
mstreamt & error() const
Definition: message.h:386
irep_idt arch
Definition: config.h:84
#define HELP_BMC
Definition: bmc.h:303
Abstract interface to support a programming language.
Loop IDs.
bool remove_function_pointers(message_handlert &_message_handler, symbol_tablet &symbol_table, const goto_functionst &goto_functions, goto_programt &goto_program, bool add_safety_assertion, bool only_remove_const_fps)
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:169
void cprover_cpp_library_factory(const std::set< irep_idt > &functions, symbol_tablet &symbol_table, message_handlert &message_handler)
void validate(const validation_modet vm) const
Check that the goto model is well-formed.
Definition: goto_model.h:97
Remove function returns.
void rewrite_union(exprt &expr)
We rewrite u.c for unions u into byte_extract(u, 0), and { .c = v } into byte_update(NIL,...
void property_slicer(goto_functionst &goto_functions, const namespacet &ns, const std::list< std::string > &properties)
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:144
CBMC Command Line Option Processing.
std::string banner_string(const std::string &front_end, const std::string &version)
void instrument_cover_goals(goto_programt &goto_program, const cover_instrumenterst &instrumenters, const irep_idt &mode, message_handlert &message_handler)
Applies instrumenters to given goto program.
Definition: cover.cpp:33
#define PARSE_OPTIONS_GOTO_CHECK(cmdline, options)
Definition: goto_check.h:58
Symbolic Execution.
void remove_returns(symbol_table_baset &symbol_table, goto_functionst &goto_functions)
removes returns
void goto_check(const namespacet &ns, const optionst &options, const irep_idt &mode, goto_functionst::goto_functiont &goto_function)
void set_c11()
Definition: config.h:53
#define CPROVER_EXIT_EXCEPTION
An (unanticipated) exception was thrown during computation.
Definition: exit_codes.h:41
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:516
virtual int doit() override
invoke main modules
static c_standardt default_c_standard()
Definition: config.cpp:675
static eomt eom
Definition: message.h:284
bool test_c_preprocessor(message_handlert &message_handler)
virtual void show_parse(std::ostream &out)=0
static irep_idt this_operating_system()
Definition: config.cpp:1368
#define CPROVER_EXIT_INTERNAL_OUT_OF_MEMORY
Memory allocation has failed and this has been detected within the program.
Definition: exit_codes.h:53
struct configt::cppt cpp
void set_c99()
Definition: config.h:52
static int do_language_agnostic_bmc(const path_strategy_choosert &path_strategy_chooser, const optionst &opts, abstract_goto_modelt &goto_model, ui_message_handlert &ui, std::function< void(bmct &, const symbol_tablet &)> driver_configure_bmc=nullptr, std::function< bool(void)> callback_after_symex=nullptr)
Perform core BMC, using an abstract model to supply GOTO function bodies (perhaps created on demand).
Definition: bmc.cpp:502
static void set_default_options(optionst &)
Set the options that have default values.
message_handlert & get_message_handler()
Definition: message.h:174
void set_cpp11()
Definition: config.h:142
#define HELP_GOTO_TRACE
Definition: goto_trace.h:259
Document and give macros for the exit codes of CPROVER binaries.
Thrown when a goto program that's being processed is in an invalid format, for example passing the wr...
mstreamt & status() const
Definition: message.h:401
void full_slicer(goto_functionst &goto_functions, const namespacet &ns, const slicing_criteriont &criterion)
#define HELP_SHOW_GOTO_FUNCTIONS
const char * CBMC_VERSION
Definition: version.cpp:1
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....
cbmc_parse_optionst(int argc, const char **argv)
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:86
goto_modelt initialize_goto_model(const std::vector< std::string > &files, message_handlert &message_handler, const optionst &options)
void parse_c_object_factory_options(const cmdlinet &cmdline, optionst &options)
Parse the c object factory parameters from a given command line.
virtual void set_language_options(const optionst &)
Set language-specific options.
Definition: language.h:43
Remove the 'vector' data type by compilation into arrays.
std::string what() const override
A human readable description of what went wrong.
virtual void usage_error()
Show the properties.
Coverage Instrumentation.
#define CPROVER_EXIT_INCORRECT_TASK
The command line is correctly structured but cannot be carried out due to missing files,...
Definition: exit_codes.h:50
void set_option(const std::string &option, const bool value)
Definition: options.cpp:26
static void remove_complex(typet &)
removes complex data type
ui_message_handlert ui_message_handler
virtual bool parse(std::istream &instream, const std::string &path)=0
Program Transformation.
#define CPROVER_EXIT_USAGE_ERROR
A usage error is returned when the command line is invalid or conflicting.
Definition: exit_codes.h:33
static cpp_standardt default_cpp_standard()
Definition: config.cpp:689
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:33
void set_cpp03()
Definition: config.h:141
#define CPROVER_EXIT_PREPROCESSOR_TEST_FAILED
Failure of the test-preprocessor method.
Definition: exit_codes.h:60
void label_properties(goto_modelt &goto_model)
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
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:60
XML Interface.
static void remove_vector(typet &)
removes vector data type
static irep_idt this_architecture()
Definition: config.cpp:1268
void nondet_static(const namespacet &ns, goto_functionst &goto_functions, const irep_idt &fct_name)
Nondeterministically initializes global scope variables in a goto-function.
#define CPROVER_EXIT_SET_PROPERTIES_FAILED
Failure to identify the properties to verify.
Definition: exit_codes.h:56
virtual void help() override
display command line help
void show_properties(const namespacet &ns, const irep_idt &identifier, message_handlert &message_handler, ui_message_handlert::uit ui, const goto_programt &goto_program)