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/exit_codes.h>
21 #include <util/invariant.h>
22 #include <util/unicode.h>
23 #include <util/version.h>
24 
25 #include <langapi/language.h>
26 
27 #include <ansi-c/c_preprocess.h>
28 #include <ansi-c/cprover_library.h>
29 
30 #include <cpp/cprover_library.h>
31 
38 #include <goto-programs/loop_ids.h>
39 #include <goto-programs/mm_io.h>
54 
56 
60 #include <goto-instrument/cover.h>
61 
63 
64 #include <langapi/mode.h>
65 
66 #include "xml_interface.h"
67 
68 cbmc_parse_optionst::cbmc_parse_optionst(int argc, const char **argv)
69  : parse_options_baset(CBMC_OPTIONS, argc, argv),
70  xml_interfacet(cmdline),
71  messaget(ui_message_handler),
72  ui_message_handler(cmdline, std::string("CBMC ") + CBMC_VERSION),
73  path_strategy_chooser()
74 {
75 }
76 
78  int argc,
79  const char **argv,
80  const std::string &extra_options)
81  : parse_options_baset(CBMC_OPTIONS + extra_options, argc, argv),
82  xml_interfacet(cmdline),
83  messaget(ui_message_handler),
84  ui_message_handler(cmdline, std::string("CBMC ") + CBMC_VERSION),
85  path_strategy_chooser()
86 {
87 }
88 
90 {
91  // Default true
92  options.set_option("assertions", true);
93  options.set_option("assumptions", true);
94  options.set_option("built-in-assertions", true);
95  options.set_option("pretty-names", true);
96  options.set_option("propagation", true);
97  options.set_option("sat-preprocessor", true);
98  options.set_option("simplify", true);
99  options.set_option("simplify-if", true);
100 
101  // Other default
102  options.set_option("arrays-uf", "auto");
103 }
104 
106 {
107  if(config.set(cmdline))
108  {
109  usage_error();
111  }
112 
114 
115  if(cmdline.isset("cover") && cmdline.isset("unwinding-assertions"))
116  {
117  error() << "--cover and --unwinding-assertions must not be given together"
118  << eom;
120  }
121 
122  if(cmdline.isset("partial-loops") && cmdline.isset("unwinding-assertions"))
123  {
124  error() << "--partial-loops and --unwinding-assertions must not be given "
125  << "together" << eom;
127  }
128 
129  if(cmdline.isset("reachability-slice") &&
130  cmdline.isset("reachability-slice-fb"))
131  {
132  error() << "--reachability-slice and --reachability-slice-fb must not be "
133  << "given together" << eom;
135  }
136 
137  if(cmdline.isset("full-slice"))
138  options.set_option("full-slice", true);
139 
140  if(cmdline.isset("show-symex-strategies"))
141  {
142  std::cout << path_strategy_chooser.show_strategies();
143  exit(CPROVER_EXIT_SUCCESS);
144  }
145 
147 
148  if(cmdline.isset("program-only"))
149  options.set_option("program-only", true);
150 
151  if(cmdline.isset("show-vcc"))
152  options.set_option("show-vcc", true);
153 
154  if(cmdline.isset("cover"))
155  parse_cover_options(cmdline, options);
156 
157  if(cmdline.isset("mm"))
158  options.set_option("mm", cmdline.get_value("mm"));
159 
160  if(cmdline.isset("c89"))
162 
163  if(cmdline.isset("c99"))
165 
166  if(cmdline.isset("c11"))
168 
169  if(cmdline.isset("cpp98"))
170  config.cpp.set_cpp98();
171 
172  if(cmdline.isset("cpp03"))
173  config.cpp.set_cpp03();
174 
175  if(cmdline.isset("cpp11"))
176  config.cpp.set_cpp11();
177 
178  if(cmdline.isset("property"))
179  options.set_option("property", cmdline.get_values("property"));
180 
181  if(cmdline.isset("drop-unused-functions"))
182  options.set_option("drop-unused-functions", true);
183 
184  if(cmdline.isset("string-abstraction"))
185  options.set_option("string-abstraction", true);
186 
187  if(cmdline.isset("reachability-slice-fb"))
188  options.set_option("reachability-slice-fb", true);
189 
190  if(cmdline.isset("reachability-slice"))
191  options.set_option("reachability-slice", true);
192 
193  if(cmdline.isset("nondet-static"))
194  options.set_option("nondet-static", true);
195 
196  if(cmdline.isset("no-simplify"))
197  options.set_option("simplify", false);
198 
199  if(cmdline.isset("stop-on-fail") ||
200  cmdline.isset("dimacs") ||
201  cmdline.isset("outfile"))
202  options.set_option("stop-on-fail", true);
203 
204  if(cmdline.isset("trace") ||
205  cmdline.isset("stop-on-fail"))
206  options.set_option("trace", true);
207 
208  if(cmdline.isset("localize-faults"))
209  options.set_option("localize-faults", true);
210  if(cmdline.isset("localize-faults-method"))
211  {
212  options.set_option(
213  "localize-faults-method",
214  cmdline.get_value("localize-faults-method"));
215  }
216 
217  if(cmdline.isset("unwind"))
218  options.set_option("unwind", cmdline.get_value("unwind"));
219 
220  if(cmdline.isset("depth"))
221  options.set_option("depth", cmdline.get_value("depth"));
222 
223  if(cmdline.isset("debug-level"))
224  options.set_option("debug-level", cmdline.get_value("debug-level"));
225 
226  if(cmdline.isset("slice-by-trace"))
227  options.set_option("slice-by-trace", cmdline.get_value("slice-by-trace"));
228 
229  if(cmdline.isset("unwindset"))
230  options.set_option("unwindset", cmdline.get_value("unwindset"));
231 
232  // constant propagation
233  if(cmdline.isset("no-propagation"))
234  options.set_option("propagation", false);
235 
236  // transform self loops to assumptions
237  options.set_option(
238  "self-loops-to-assumptions",
239  !cmdline.isset("no-self-loops-to-assumptions"));
240 
241  // all checks supported by goto_check
243 
244  // check assertions
245  if(cmdline.isset("no-assertions"))
246  options.set_option("assertions", false);
247 
248  // use assumptions
249  if(cmdline.isset("no-assumptions"))
250  options.set_option("assumptions", false);
251 
252  // magic error label
253  if(cmdline.isset("error-label"))
254  options.set_option("error-label", cmdline.get_values("error-label"));
255 
256  // generate unwinding assertions
257  if(cmdline.isset("unwinding-assertions"))
258  options.set_option("unwinding-assertions", true);
259 
260  if(cmdline.isset("partial-loops"))
261  options.set_option("partial-loops", true);
262 
263  // remove unused equations
264  if(cmdline.isset("slice-formula"))
265  options.set_option("slice-formula", true);
266 
267  // simplify if conditions and branches
268  if(cmdline.isset("no-simplify-if"))
269  options.set_option("simplify-if", false);
270 
271  if(cmdline.isset("arrays-uf-always"))
272  options.set_option("arrays-uf", "always");
273  else if(cmdline.isset("arrays-uf-never"))
274  options.set_option("arrays-uf", "never");
275 
276  if(cmdline.isset("dimacs"))
277  options.set_option("dimacs", true);
278 
279  if(cmdline.isset("refine-arrays"))
280  {
281  options.set_option("refine", true);
282  options.set_option("refine-arrays", true);
283  }
284 
285  if(cmdline.isset("refine-arithmetic"))
286  {
287  options.set_option("refine", true);
288  options.set_option("refine-arithmetic", true);
289  }
290 
291  if(cmdline.isset("refine"))
292  {
293  options.set_option("refine", true);
294  options.set_option("refine-arrays", true);
295  options.set_option("refine-arithmetic", true);
296  }
297 
298  if(cmdline.isset("refine-strings"))
299  {
300  options.set_option("refine-strings", true);
301  options.set_option("string-printable", cmdline.isset("string-printable"));
302  if(cmdline.isset("string-max-length"))
303  options.set_option(
304  "string-max-length", cmdline.get_value("string-max-length"));
305  }
306 
307  if(cmdline.isset("max-node-refinement"))
308  options.set_option(
309  "max-node-refinement",
310  cmdline.get_value("max-node-refinement"));
311 
312  // SMT Options
313 
314  if(cmdline.isset("smt1"))
315  {
316  error() << "--smt1 is no longer supported" << eom;
318  }
319 
320  if(cmdline.isset("smt2"))
321  options.set_option("smt2", true);
322 
323  if(cmdline.isset("fpa"))
324  options.set_option("fpa", true);
325 
326  bool solver_set=false;
327 
328  if(cmdline.isset("boolector"))
329  {
330  options.set_option("boolector", true), solver_set=true;
331  options.set_option("smt2", true);
332  }
333 
334  if(cmdline.isset("mathsat"))
335  {
336  options.set_option("mathsat", true), solver_set=true;
337  options.set_option("smt2", true);
338  }
339 
340  if(cmdline.isset("cvc4"))
341  {
342  options.set_option("cvc4", true), solver_set=true;
343  options.set_option("smt2", true);
344  }
345 
346  if(cmdline.isset("yices"))
347  {
348  options.set_option("yices", true), solver_set=true;
349  options.set_option("smt2", true);
350  }
351 
352  if(cmdline.isset("z3"))
353  {
354  options.set_option("z3", true), solver_set=true;
355  options.set_option("smt2", true);
356  }
357 
358  if(cmdline.isset("smt2") && !solver_set)
359  {
360  if(cmdline.isset("outfile"))
361  {
362  // outfile and no solver should give standard compliant SMT-LIB
363  options.set_option("generic", true);
364  }
365  else
366  {
367  // the default smt2 solver
368  options.set_option("z3", true);
369  }
370  }
371 
372  if(cmdline.isset("beautify"))
373  options.set_option("beautify", true);
374 
375  if(cmdline.isset("no-sat-preprocessor"))
376  options.set_option("sat-preprocessor", false);
377 
378  if(cmdline.isset("no-pretty-names"))
379  options.set_option("pretty-names", false);
380 
381  if(cmdline.isset("outfile"))
382  options.set_option("outfile", cmdline.get_value("outfile"));
383 
384  if(cmdline.isset("graphml-witness"))
385  {
386  options.set_option("graphml-witness", cmdline.get_value("graphml-witness"));
387  options.set_option("stop-on-fail", true);
388  options.set_option("trace", true);
389  }
390 
391  if(cmdline.isset("symex-coverage-report"))
392  options.set_option(
393  "symex-coverage-report",
394  cmdline.get_value("symex-coverage-report"));
395 
397 }
398 
401 {
402  if(cmdline.isset("version"))
403  {
404  std::cout << CBMC_VERSION << '\n';
405  return CPROVER_EXIT_SUCCESS;
406  }
407 
408  //
409  // command line options
410  //
411 
412  optionst options;
413  try
414  {
415  get_command_line_options(options);
416  }
417 
418  catch(const char *error_msg)
419  {
420  error() << error_msg << eom;
421  return CPROVER_EXIT_EXCEPTION;
422  }
423 
424  catch(const std::string &error_msg)
425  {
426  error() << error_msg << eom;
427  return CPROVER_EXIT_EXCEPTION;
428  }
429 
432 
433  //
434  // Print a banner
435  //
436  status() << "CBMC version " << CBMC_VERSION << " " << sizeof(void *) * 8
437  << "-bit " << config.this_architecture() << " "
439 
440  //
441  // Unwinding of transition systems is done by hw-cbmc.
442  //
443 
444  if(cmdline.isset("module") ||
445  cmdline.isset("gen-interface"))
446  {
447  error() << "This version of CBMC has no support for "
448  " hardware modules. Please use hw-cbmc." << eom;
450  }
451 
453 
454  if(cmdline.isset("test-preprocessor"))
458 
459  if(cmdline.isset("preprocess"))
460  {
461  preprocessing();
462  return CPROVER_EXIT_SUCCESS;
463  }
464 
465  if(cmdline.isset("show-parse-tree"))
466  {
467  if(cmdline.args.size()!=1 ||
469  {
470  error() << "Please give exactly one source file" << eom;
472  }
473 
474  std::string filename=cmdline.args[0];
475 
476  #ifdef _MSC_VER
477  std::ifstream infile(widen(filename));
478  #else
479  std::ifstream infile(filename);
480  #endif
481 
482  if(!infile)
483  {
484  error() << "failed to open input file `"
485  << filename << "'" << eom;
487  }
488 
489  std::unique_ptr<languaget> language=
490  get_language_from_filename(filename);
491 
492  if(language==nullptr)
493  {
494  error() << "failed to figure out type of file `"
495  << filename << "'" << eom;
497  }
498 
499  language->get_language_options(cmdline);
501 
502  status() << "Parsing " << filename << eom;
503 
504  if(language->parse(infile, filename))
505  {
506  error() << "PARSING ERROR" << eom;
508  }
509 
510  language->show_parse(std::cout);
511  return CPROVER_EXIT_SUCCESS;
512  }
513 
514  int get_goto_program_ret =
516 
517  if(get_goto_program_ret!=-1)
518  return get_goto_program_ret;
519 
520  if(cmdline.isset("show-claims") || // will go away
521  cmdline.isset("show-properties")) // use this one
522  {
525  return CPROVER_EXIT_SUCCESS;
526  }
527 
528  if(set_properties())
530 
533  options,
534  goto_model,
536  *this);
537 }
538 
540 {
541  try
542  {
543  if(cmdline.isset("claim")) // will go away
545 
546  if(cmdline.isset("property")) // use this one
548  }
549 
550  catch(const char *e)
551  {
552  error() << e << eom;
553  return true;
554  }
555 
556  catch(const std::string &e)
557  {
558  error() << e << eom;
559  return true;
560  }
561 
562  catch(int e)
563  {
564  error() << "Numeric exception : " << e << eom;
565  return true;
566  }
567 
568  return false;
569 }
570 
572  goto_modelt &goto_model,
573  const optionst &options,
574  const cmdlinet &cmdline,
575  messaget &log,
576  ui_message_handlert &ui_message_handler)
577 {
578  if(cmdline.args.empty())
579  {
580  log.error() << "Please provide a program to verify" << log.eom;
582  }
583 
584  try
585  {
587 
588  if(cmdline.isset("show-symbol-table"))
589  {
591  return CPROVER_EXIT_SUCCESS;
592  }
593 
596 
597  // show it?
598  if(cmdline.isset("show-loops"))
599  {
601  return CPROVER_EXIT_SUCCESS;
602  }
603 
604  // show it?
605  if(
606  cmdline.isset("show-goto-functions") ||
607  cmdline.isset("list-goto-functions"))
608  {
610  goto_model,
613  cmdline.isset("list-goto-functions"));
614  return CPROVER_EXIT_SUCCESS;
615  }
616 
617  log.status() << config.object_bits_info() << log.eom;
618  }
619 
620  catch(const char *e)
621  {
622  log.error() << e << log.eom;
623  return CPROVER_EXIT_EXCEPTION;
624  }
625 
626  catch(const std::string &e)
627  {
628  log.error() << e << log.eom;
629  return CPROVER_EXIT_EXCEPTION;
630  }
631 
632  catch(int e)
633  {
634  log.error() << "Numeric exception : " << e << log.eom;
635  return CPROVER_EXIT_EXCEPTION;
636  }
637 
638  catch(const std::bad_alloc &)
639  {
640  log.error() << "Out of memory" << log.eom;
642  }
643 
644  return -1; // no error, continue
645 }
646 
648 {
649  try
650  {
651  if(cmdline.args.size()!=1)
652  {
653  error() << "Please provide one program to preprocess" << eom;
654  return;
655  }
656 
657  std::string filename=cmdline.args[0];
658 
659  std::ifstream infile(filename);
660 
661  if(!infile)
662  {
663  error() << "failed to open input file" << eom;
664  return;
665  }
666 
667  std::unique_ptr<languaget> language=get_language_from_filename(filename);
668  language->get_language_options(cmdline);
669 
670  if(language==nullptr)
671  {
672  error() << "failed to figure out type of file" << eom;
673  return;
674  }
675 
677 
678  if(language->preprocess(infile, filename, std::cout))
679  error() << "PREPROCESSING ERROR" << eom;
680  }
681 
682  catch(const char *e)
683  {
684  error() << e << eom;
685  }
686 
687  catch(const std::string &e)
688  {
689  error() << e << eom;
690  }
691 
692  catch(int e)
693  {
694  error() << "Numeric exception : " << e << eom;
695  }
696 
697  catch(const std::bad_alloc &)
698  {
699  error() << "Out of memory" << eom;
701  }
702 }
703 
705  goto_modelt &goto_model,
706  const optionst &options,
707  messaget &log)
708 {
709  try
710  {
711  // Remove inline assembler; this needs to happen before
712  // adding the library.
714 
715  // add the library
716  log.status() << "Adding CPROVER library (" << config.ansi_c.arch << ")"
717  << eom;
722 
723  if(options.get_bool_option("string-abstraction"))
725 
726  // remove function pointers
727  log.status() << "Removal of function pointers and virtual functions" << eom;
729  log.get_message_handler(),
730  goto_model,
731  options.get_bool_option("pointer-check"));
732 
733  mm_io(goto_model);
734 
735  // instrument library preconditions
737 
738  // remove returns, gcc vectors, complex
743 
744  // add generic checks
745  log.status() << "Generic Property Instrumentation" << eom;
746  goto_check(options, goto_model);
747 
748  // checks don't know about adjusted float expressions
750 
751  // ignore default/user-specified initialization
752  // of variables with static lifetime
753  if(options.get_bool_option("nondet-static"))
754  {
755  log.status() << "Adding nondeterministic initialization "
756  "of static/global variables"
757  << eom;
759  }
760 
761  if(options.get_bool_option("string-abstraction"))
762  {
763  log.status() << "String Abstraction" << eom;
765  }
766 
767  // add failed symbols
768  // needs to be done before pointer analysis
770 
771  // recalculate numbers, etc.
773 
774  // add loop ids
776 
777  if(options.get_bool_option("drop-unused-functions"))
778  {
779  // Entry point will have been set before and function pointers removed
780  log.status() << "Removing unused functions" << eom;
782  }
783 
784  // remove skips such that trivial GOTOs are deleted and not considered
785  // for coverage annotation:
787 
788  // instrument cover goals
789  if(options.is_set("cover"))
790  {
792  return true;
793  }
794 
795  // label the assertions
796  // This must be done after adding assertions and
797  // before using the argument of the "property" option.
798  // Do not re-label after using the property slicer because
799  // this would cause the property identifiers to change.
801 
802  // reachability slice?
803  if(options.get_bool_option("reachability-slice-fb"))
804  {
805  log.status() << "Performing a forwards-backwards reachability slice"
806  << eom;
807  if(options.is_set("property"))
809  goto_model, options.get_list_option("property"), true);
810  else
812  }
813 
814  if(options.get_bool_option("reachability-slice"))
815  {
816  log.status() << "Performing a reachability slice" << eom;
817  if(options.is_set("property"))
818  reachability_slicer(goto_model, options.get_list_option("property"));
819  else
821  }
822 
823  // full slice?
824  if(options.get_bool_option("full-slice"))
825  {
826  log.status() << "Performing a full slice" << eom;
827  if(options.is_set("property"))
828  property_slicer(goto_model, options.get_list_option("property"));
829  else
831  }
832 
833  // remove any skips introduced since coverage instrumentation
835  }
836 
837  catch(const char *e)
838  {
839  log.error() << e << eom;
840  return true;
841  }
842 
843  catch(const std::string &e)
844  {
845  log.error() << e << eom;
846  return true;
847  }
848 
849  catch(int e)
850  {
851  log.error() << "Numeric exception : " << e << eom;
852  return true;
853  }
854 
855  catch(const std::bad_alloc &)
856  {
857  log.error() << "Out of memory" << eom;
859  return true;
860  }
861 
862  return false;
863 }
864 
867 {
868  // clang-format off
869  std::cout << '\n' << banner_string("CBMC", CBMC_VERSION) << '\n'
870  <<
871  "* * Copyright (C) 2001-2018 * *\n"
872  "* * Daniel Kroening, Edmund Clarke * *\n"
873  "* * Carnegie Mellon University, Computer Science Department * *\n"
874  "* * kroening@kroening.com * *\n"
875  "* * Protected in part by U.S. patent 7,225,417 * *\n"
876  "\n"
877  "Usage: Purpose:\n"
878  "\n"
879  " cbmc [-?] [-h] [--help] show help\n"
880  " cbmc file.c ... source file names\n"
881  "\n"
882  "Analysis options:\n"
884  " --symex-coverage-report f generate a Cobertura XML coverage report in f\n" // NOLINT(*)
885  " --property id only check one specific property\n"
886  " --stop-on-fail stop analysis once a failed property is detected\n" // NOLINT(*)
887  " --trace give a counterexample trace for failed properties\n" //NOLINT(*)
888  "\n"
889  "C/C++ frontend options:\n"
890  " -I path set include path (C/C++)\n"
891  " -D macro define preprocessor macro (C/C++)\n"
892  " --preprocess stop after preprocessing\n"
893  " --16, --32, --64 set width of int\n"
894  " --LP64, --ILP64, --LLP64,\n"
895  " --ILP32, --LP32 set width of int, long and pointers\n"
896  " --little-endian allow little-endian word-byte conversions\n"
897  " --big-endian allow big-endian word-byte conversions\n"
898  " --unsigned-char make \"char\" unsigned by default\n"
899  " --mm model set memory model (default: sc)\n"
900  " --arch set architecture (default: "
901  << configt::this_architecture() << ")\n"
902  " --os set operating system (default: "
903  << configt::this_operating_system() << ")\n"
904  " --c89/99/11 set C language standard (default: "
910  configt::ansi_ct::c_standardt::C11?"c11":"") << ")\n" // NOLINT(*)
911  " --cpp98/03/11 set C++ language standard (default: "
913  configt::cppt::cpp_standardt::CPP98?"cpp98": // NOLINT(*)
915  configt::cppt::cpp_standardt::CPP03?"cpp03": // NOLINT(*)
917  configt::cppt::cpp_standardt::CPP11?"cpp11":"") << ")\n" // NOLINT(*)
918  #ifdef _WIN32
919  " --gcc use GCC as preprocessor\n"
920  #endif
921  " --no-arch don't set up an architecture\n"
922  " --no-library disable built-in abstract C library\n"
923  " --round-to-nearest rounding towards nearest even (default)\n"
924  " --round-to-plus-inf rounding towards plus infinity\n"
925  " --round-to-minus-inf rounding towards minus infinity\n"
926  " --round-to-zero rounding towards zero\n"
928  "\n"
929  "Program representations:\n"
930  " --show-parse-tree show parse tree\n"
931  " --show-symbol-table show loaded symbol table\n"
933  " --drop-unused-functions drop functions trivially unreachable from main function\n" // NOLINT(*)
934  "\n"
935  "Program instrumentation options:\n"
937  " --no-assertions ignore user assertions\n"
938  " --no-assumptions ignore user assumptions\n"
939  " --error-label label check that label is unreachable\n"
940  " --cover CC create test-suite with coverage criterion CC\n" // NOLINT(*)
941  " --mm MM memory consistency model for concurrent programs\n" // NOLINT(*)
943  " --full-slice run full slicer (experimental)\n" // NOLINT(*)
944  "\n"
945  "Semantic transformations:\n"
946  // NOLINTNEXTLINE(whitespace/line_length)
947  " --nondet-static add nondeterministic initialization of variables with static lifetime\n"
948  "\n"
949  "BMC options:\n"
950  HELP_BMC
951  "\n"
952  "Backend options:\n"
953  " --object-bits n number of bits used for object addresses\n"
954  " --dimacs generate CNF in DIMACS format\n"
955  " --beautify beautify the counterexample (greedy heuristic)\n" // NOLINT(*)
956  " --localize-faults localize faults (experimental)\n"
957  " --smt1 use default SMT1 solver (obsolete)\n"
958  " --smt2 use default SMT2 solver (Z3)\n"
959  " --boolector use Boolector\n"
960  " --mathsat use MathSAT\n"
961  " --cvc4 use CVC4\n"
962  " --yices use Yices\n"
963  " --z3 use Z3\n"
964  " --refine use refinement procedure (experimental)\n"
965  " --refine-strings use string refinement (experimental)\n"
966  " --string-printable add constraint that strings are printable (experimental)\n" // NOLINT(*)
967  " --string-max-input-length add constraint on the length of input strings\n" // NOLINT(*)
968  " --string-max-length add constraint on the length of strings"
969  " (deprecated: use string-max-input-length instead)\n" // NOLINT(*)
970  " --outfile filename output formula to given file\n"
971  " --arrays-uf-never never turn arrays into uninterpreted functions\n" // NOLINT(*)
972  " --arrays-uf-always always turn arrays into uninterpreted functions\n" // NOLINT(*)
973  "\n"
974  "Other options:\n"
975  " --version show version and exit\n"
976  " --xml-ui use XML-formatted output\n"
977  " --xml-interface bi-directional XML interface\n"
978  " --json-ui use JSON-formatted output\n"
980  HELP_FLUSH
981  " --verbosity # verbosity level\n"
983  "\n";
984  // clang-format on
985 }
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:46
uit get_ui() const
Definition: ui_message.h:37
virtual void get_language_options(const cmdlinet &)
Definition: language.h:43
std::string object_bits_info()
Definition: config.cpp:1203
void compute_loop_numbers()
Show the symbol table.
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:78
bool is_goto_binary(const std::string &filename)
Read Goto Programs.
Remove the &#39;complex&#39; data type by compilation into structs.
std::string get_value(char option) const
Definition: cmdline.cpp:45
void set_cpp98()
Definition: config.h:139
void remove_unused_functions(goto_modelt &goto_model, message_handlert &message_handler)
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
STL namespace.
virtual bool preprocess(std::istream &instream, const std::string &path, std::ostream &outstream)
Definition: language.h:47
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
Pointer Dereferencing.
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
#define CPROVER_EXIT_INTERNAL_ERROR
An error has been encountered during processing the requested analysis.
Definition: exit_codes.h:41
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:23
Remove &#39;asm&#39; statements by compiling into suitable standard code.
#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
static int do_language_agnostic_bmc(const path_strategy_choosert &path_strategy_chooser, const optionst &opts, abstract_goto_modelt &goto_model, const ui_message_handlert::uit &ui, messaget &message, 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:559
void parse_cover_options(const cmdlinet &cmdline, optionst &options)
Parses coverage-related command line options.
Definition: cover.cpp:163
Set the properties to check.
#define HELP_GOTO_CHECK
Definition: goto_check.h:42
static bool process_goto_program(goto_modelt &, const optionst &, messaget &)
Unused function removal.
#define PARSE_OPTIONS_GOTO_TRACE(cmdline, options)
Definition: goto_trace.h:258
bool set(const cmdlinet &cmdline)
Definition: config.cpp:738
void set_c89()
Definition: config.h:51
Perform Memory-mapped I/O instrumentation.
#define HELP_TIMESTAMP
Definition: timestamper.h:14
void show_symbol_table(const symbol_tablet &symbol_table, ui_message_handlert::uit ui)
argst args
Definition: cmdline.h:37
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
Nondeterministic initialization of certain global scope variables.
#define HELP_FLUSH
Definition: ui_message.h:108
bool get_bool_option(const std::string &option) const
Definition: options.cpp:42
mstreamt & error() const
Definition: message.h:302
irep_idt arch
Definition: config.h:84
Function Inlining.
#define HELP_BMC
Definition: bmc.h:315
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:148
void full_slicer(goto_functionst &goto_functions, const namespacet &ns, slicing_criteriont &criterion)
void cprover_cpp_library_factory(const std::set< irep_idt > &functions, symbol_tablet &symbol_table, message_handlert &message_handler)
Remove function returns.
void property_slicer(goto_functionst &goto_functions, const namespacet &ns, const std::list< std::string > &properties)
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:56
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:36
void remove_asm(goto_functionst &goto_functions, symbol_tablet &symbol_table)
removes assembler
Definition: remove_asm.cpp:482
virtual int doit() override
invoke main modules
static c_standardt default_c_standard()
Definition: config.cpp:648
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:1310
#define CPROVER_EXIT_INTERNAL_OUT_OF_MEMORY
Memory allocation has failed and this has been detected within the program.
Definition: exit_codes.h:48
struct configt::cppt cpp
void set_c99()
Definition: config.h:52
static void set_default_options(optionst &)
Set the options that have default values.
message_handlert & get_message_handler()
Definition: message.h:153
void set_cpp11()
Definition: config.h:141
Goto Programs with Functions.
#define HELP_GOTO_TRACE
Definition: goto_trace.h:252
Document and give macros for the exit codes of CPROVER binaries.
mstreamt & status() const
Definition: message.h:317
#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 cmdlinet &cmdline, message_handlert &message_handler)
Slicing.
Remove the &#39;vector&#39; data type by compilation into arrays.
virtual void usage_error()
Show the properties.
void rewrite_union(exprt &expr, const namespacet &ns)
We rewrite u.c for unions u into byte_extract(u, 0), and { .c = v } into byte_update(NIL, 0, v)
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:45
void set_option(const std::string &option, const bool value)
Definition: options.cpp:24
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:28
static cpp_standardt default_cpp_standard()
Definition: config.cpp:662
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:140
#define CPROVER_EXIT_PREPROCESSOR_TEST_FAILED
Failure of the test-preprocessor method.
Definition: exit_codes.h:55
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:1213
void nondet_static(const namespacet &ns, goto_functionst &goto_functions, const irep_idt &fct_name)
#define CPROVER_EXIT_SET_PROPERTIES_FAILED
Failure to identify the properties to verify.
Definition: exit_codes.h:51
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)