cprover
cbmc_parse_options.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: CBMC Command Line Option Processing
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "cbmc_parse_options.h"
13 
14 #include <fstream>
15 #include <cstdlib> // exit()
16 #include <iostream>
17 #include <memory>
18 
19 #include <util/config.h>
20 #include <util/exception_utils.h>
21 #include <util/exit_codes.h>
22 #include <util/invariant.h>
23 #include <util/make_unique.h>
24 #include <util/unicode.h>
25 #include <util/version.h>
26 
27 #include <langapi/language.h>
28 
29 #include <ansi-c/c_preprocess.h>
30 #include <ansi-c/cprover_library.h>
31 #include <ansi-c/gcc_version.h>
32 
33 #include <assembler/remove_asm.h>
34 
35 #include <cpp/cprover_library.h>
36 
40 #include <goto-checker/bmc_util.h>
50 
55 #include <goto-programs/loop_ids.h>
56 #include <goto-programs/mm_io.h>
72 
73 #include <goto-instrument/cover.h>
77 
79 
81 
82 #include <langapi/mode.h>
83 
84 #include "c_test_input_generator.h"
85 
86 cbmc_parse_optionst::cbmc_parse_optionst(int argc, const char **argv)
89  argc,
90  argv,
91  std::string("CBMC ") + CBMC_VERSION)
92 {
95 }
96 
98  int argc,
99  const char **argv,
100  const std::string &extra_options)
102  CBMC_OPTIONS + extra_options,
103  argc,
104  argv,
105  std::string("CBMC ") + CBMC_VERSION)
106 {
109 }
110 
112 {
113  // Default true
114  options.set_option("assertions", true);
115  options.set_option("assumptions", true);
116  options.set_option("built-in-assertions", true);
117  options.set_option("pretty-names", true);
118  options.set_option("propagation", true);
119  options.set_option("sat-preprocessor", true);
120  options.set_option("simple-slice", true);
121  options.set_option("simplify", true);
122  options.set_option("simplify-if", true);
123  options.set_option("show-goto-symex-steps", false);
124 
125  // Other default
126  options.set_option("arrays-uf", "auto");
127 }
128 
130 {
131  if(config.set(cmdline))
132  {
133  usage_error();
135  }
136 
139 
140  if(cmdline.isset("function"))
141  options.set_option("function", cmdline.get_value("function"));
142 
143  if(cmdline.isset("cover") && cmdline.isset("unwinding-assertions"))
144  {
145  log.error()
146  << "--cover and --unwinding-assertions must not be given together"
147  << messaget::eom;
149  }
150 
151  if(cmdline.isset("max-field-sensitivity-array-size"))
152  {
153  options.set_option(
154  "max-field-sensitivity-array-size",
155  cmdline.get_value("max-field-sensitivity-array-size"));
156  }
157 
158  if(cmdline.isset("no-array-field-sensitivity"))
159  {
160  if(cmdline.isset("max-field-sensitivity-array-size"))
161  {
162  log.error()
163  << "--no-array-field-sensitivity and --max-field-sensitivity-array-size"
164  << " must not be given together" << messaget::eom;
166  }
167  options.set_option("no-array-field-sensitivity", true);
168  }
169 
170  if(cmdline.isset("partial-loops") && cmdline.isset("unwinding-assertions"))
171  {
172  log.error()
173  << "--partial-loops and --unwinding-assertions must not be given "
174  << "together" << messaget::eom;
176  }
177 
178  if(cmdline.isset("reachability-slice") &&
179  cmdline.isset("reachability-slice-fb"))
180  {
181  log.error()
182  << "--reachability-slice and --reachability-slice-fb must not be "
183  << "given together" << messaget::eom;
185  }
186 
187  if(cmdline.isset("full-slice"))
188  options.set_option("full-slice", true);
189 
190  if(cmdline.isset("show-symex-strategies"))
191  {
193  exit(CPROVER_EXIT_SUCCESS);
194  }
195 
197 
198  if(cmdline.isset("program-only"))
199  options.set_option("program-only", true);
200 
201  if(cmdline.isset("show-vcc"))
202  options.set_option("show-vcc", true);
203 
204  if(cmdline.isset("cover"))
205  parse_cover_options(cmdline, options);
206 
207  if(cmdline.isset("mm"))
208  options.set_option("mm", cmdline.get_value("mm"));
209 
210  if(cmdline.isset("c89"))
212 
213  if(cmdline.isset("symex-complexity-limit"))
214  options.set_option(
215  "symex-complexity-limit", cmdline.get_value("symex-complexity-limit"));
216 
217  if(cmdline.isset("symex-complexity-failed-child-loops-limit"))
218  options.set_option(
219  "symex-complexity-failed-child-loops-limit",
220  cmdline.get_value("symex-complexity-failed-child-loops-limit"));
221 
222  if(cmdline.isset("c99"))
224 
225  if(cmdline.isset("c11"))
227 
228  if(cmdline.isset("cpp98"))
229  config.cpp.set_cpp98();
230 
231  if(cmdline.isset("cpp03"))
232  config.cpp.set_cpp03();
233 
234  if(cmdline.isset("cpp11"))
235  config.cpp.set_cpp11();
236 
237  if(cmdline.isset("property"))
238  options.set_option("property", cmdline.get_values("property"));
239 
240  if(cmdline.isset("drop-unused-functions"))
241  options.set_option("drop-unused-functions", true);
242 
243  if(cmdline.isset("string-abstraction"))
244  options.set_option("string-abstraction", true);
245 
246  if(cmdline.isset("reachability-slice-fb"))
247  options.set_option("reachability-slice-fb", true);
248 
249  if(cmdline.isset("reachability-slice"))
250  options.set_option("reachability-slice", true);
251 
252  if(cmdline.isset("nondet-static"))
253  options.set_option("nondet-static", true);
254 
255  if(cmdline.isset("no-simplify"))
256  options.set_option("simplify", false);
257 
258  if(cmdline.isset("stop-on-fail") ||
259  cmdline.isset("dimacs") ||
260  cmdline.isset("outfile"))
261  options.set_option("stop-on-fail", true);
262 
263  if(
264  cmdline.isset("trace") || cmdline.isset("compact-trace") ||
265  cmdline.isset("stack-trace") || cmdline.isset("stop-on-fail") ||
267  !cmdline.isset("cover")))
268  {
269  options.set_option("trace", true);
270  }
271 
272  if(cmdline.isset("localize-faults"))
273  options.set_option("localize-faults", true);
274 
275  if(cmdline.isset("unwind"))
276  options.set_option("unwind", cmdline.get_value("unwind"));
277 
278  if(cmdline.isset("depth"))
279  options.set_option("depth", cmdline.get_value("depth"));
280 
281  if(cmdline.isset("debug-level"))
282  options.set_option("debug-level", cmdline.get_value("debug-level"));
283 
284  if(cmdline.isset("slice-by-trace"))
285  {
286  log.error() << "--slice-by-trace has been removed" << messaget::eom;
288  }
289 
290  if(cmdline.isset("unwindset"))
291  options.set_option("unwindset", cmdline.get_values("unwindset"));
292 
293  // constant propagation
294  if(cmdline.isset("no-propagation"))
295  options.set_option("propagation", false);
296 
297  // transform self loops to assumptions
298  options.set_option(
299  "self-loops-to-assumptions",
300  !cmdline.isset("no-self-loops-to-assumptions"));
301 
302  // all checks supported by goto_check
304 
305  // check assertions
306  if(cmdline.isset("no-assertions"))
307  options.set_option("assertions", false);
308 
309  // use assumptions
310  if(cmdline.isset("no-assumptions"))
311  options.set_option("assumptions", false);
312 
313  // magic error label
314  if(cmdline.isset("error-label"))
315  options.set_option("error-label", cmdline.get_values("error-label"));
316 
317  // generate unwinding assertions
318  if(cmdline.isset("unwinding-assertions"))
319  {
320  options.set_option("unwinding-assertions", true);
321  options.set_option("paths-symex-explore-all", true);
322  }
323 
324  if(cmdline.isset("partial-loops"))
325  options.set_option("partial-loops", true);
326 
327  // remove unused equations
328  if(cmdline.isset("slice-formula"))
329  options.set_option("slice-formula", true);
330 
331  // simplify if conditions and branches
332  if(cmdline.isset("no-simplify-if"))
333  options.set_option("simplify-if", false);
334 
335  if(cmdline.isset("arrays-uf-always"))
336  options.set_option("arrays-uf", "always");
337  else if(cmdline.isset("arrays-uf-never"))
338  options.set_option("arrays-uf", "never");
339 
340  if(cmdline.isset("dimacs"))
341  options.set_option("dimacs", true);
342 
343  if(cmdline.isset("refine-arrays"))
344  {
345  options.set_option("refine", true);
346  options.set_option("refine-arrays", true);
347  }
348 
349  if(cmdline.isset("refine-arithmetic"))
350  {
351  options.set_option("refine", true);
352  options.set_option("refine-arithmetic", true);
353  }
354 
355  if(cmdline.isset("refine"))
356  {
357  options.set_option("refine", true);
358  options.set_option("refine-arrays", true);
359  options.set_option("refine-arithmetic", true);
360  }
361 
362  if(cmdline.isset("refine-strings"))
363  {
364  options.set_option("refine-strings", true);
365  options.set_option("string-printable", cmdline.isset("string-printable"));
366  }
367 
368  if(cmdline.isset("max-node-refinement"))
369  options.set_option(
370  "max-node-refinement",
371  cmdline.get_value("max-node-refinement"));
372 
373  if(cmdline.isset("incremental-loop"))
374  {
375  options.set_option(
376  "incremental-loop", cmdline.get_value("incremental-loop"));
377  options.set_option("refine", true);
378  options.set_option("refine-arrays", true);
379 
380  if(cmdline.isset("unwind-min"))
381  options.set_option("unwind-min", cmdline.get_value("unwind-min"));
382 
383  if(cmdline.isset("unwind-max"))
384  options.set_option("unwind-max", cmdline.get_value("unwind-max"));
385 
386  if(cmdline.isset("ignore-properties-before-unwind-min"))
387  options.set_option("ignore-properties-before-unwind-min", true);
388 
389  if(cmdline.isset("paths"))
390  {
391  log.error() << "--paths not supported with --incremental-loop"
392  << messaget::eom;
394  }
395  }
396 
397  // SMT Options
398 
399  if(cmdline.isset("smt1"))
400  {
401  log.error() << "--smt1 is no longer supported" << messaget::eom;
403  }
404 
405  if(cmdline.isset("smt2"))
406  options.set_option("smt2", true);
407 
408  if(cmdline.isset("fpa"))
409  options.set_option("fpa", true);
410 
411  bool solver_set=false;
412 
413  if(cmdline.isset("boolector"))
414  {
415  options.set_option("boolector", true), solver_set=true;
416  options.set_option("smt2", true);
417  }
418 
419  if(cmdline.isset("cprover-smt2"))
420  {
421  options.set_option("cprover-smt2", true), solver_set = true;
422  options.set_option("smt2", true);
423  }
424 
425  if(cmdline.isset("mathsat"))
426  {
427  options.set_option("mathsat", true), solver_set=true;
428  options.set_option("smt2", true);
429  }
430 
431  if(cmdline.isset("cvc4"))
432  {
433  options.set_option("cvc4", true), solver_set=true;
434  options.set_option("smt2", true);
435  }
436 
437  if(cmdline.isset("yices"))
438  {
439  options.set_option("yices", true), solver_set=true;
440  options.set_option("smt2", true);
441  }
442 
443  if(cmdline.isset("z3"))
444  {
445  options.set_option("z3", true), solver_set=true;
446  options.set_option("smt2", true);
447  }
448 
449  if(cmdline.isset("smt2") && !solver_set)
450  {
451  if(cmdline.isset("outfile"))
452  {
453  // outfile and no solver should give standard compliant SMT-LIB
454  options.set_option("generic", true);
455  }
456  else
457  {
458  // the default smt2 solver
459  options.set_option("z3", true);
460  }
461  }
462 
463  if(cmdline.isset("beautify"))
464  options.set_option("beautify", true);
465 
466  if(cmdline.isset("no-sat-preprocessor"))
467  options.set_option("sat-preprocessor", false);
468 
469  if(cmdline.isset("no-pretty-names"))
470  options.set_option("pretty-names", false);
471 
472  if(cmdline.isset("outfile"))
473  options.set_option("outfile", cmdline.get_value("outfile"));
474 
475  if(cmdline.isset("graphml-witness"))
476  {
477  options.set_option("graphml-witness", cmdline.get_value("graphml-witness"));
478  options.set_option("stop-on-fail", true);
479  options.set_option("trace", true);
480  }
481 
482  if(cmdline.isset("symex-coverage-report"))
483  {
484  options.set_option(
485  "symex-coverage-report",
486  cmdline.get_value("symex-coverage-report"));
487  options.set_option("paths-symex-explore-all", true);
488  }
489 
490  if(cmdline.isset("validate-ssa-equation"))
491  {
492  options.set_option("validate-ssa-equation", true);
493  }
494 
495  if(cmdline.isset("validate-goto-model"))
496  {
497  options.set_option("validate-goto-model", true);
498  }
499 
500  if(cmdline.isset("show-goto-symex-steps"))
501  options.set_option("show-goto-symex-steps", true);
502 
504 }
505 
508 {
509  if(cmdline.isset("version"))
510  {
511  std::cout << CBMC_VERSION << '\n';
512  return CPROVER_EXIT_SUCCESS;
513  }
514 
515  //
516  // command line options
517  //
518 
519  optionst options;
520  get_command_line_options(options);
521 
524 
525  //
526  // Print a banner
527  //
528  log.status() << "CBMC version " << CBMC_VERSION << " " << sizeof(void *) * 8
529  << "-bit " << config.this_architecture() << " "
531 
532  //
533  // Unwinding of transition systems is done by hw-cbmc.
534  //
535 
536  if(cmdline.isset("module") ||
537  cmdline.isset("gen-interface"))
538  {
539  log.error() << "This version of CBMC has no support for "
540  " hardware modules. Please use hw-cbmc."
541  << messaget::eom;
543  }
544 
546 
547  // configure gcc, if required
549  {
550  gcc_versiont gcc_version;
551  gcc_version.get("gcc");
552  configure_gcc(gcc_version);
553  }
554 
555  if(cmdline.isset("test-preprocessor"))
559 
560  if(cmdline.isset("preprocess"))
561  {
562  preprocessing(options);
563  return CPROVER_EXIT_SUCCESS;
564  }
565 
566  if(cmdline.isset("show-parse-tree"))
567  {
568  if(
569  cmdline.args.size() != 1 ||
571  {
572  log.error() << "Please give exactly one source file" << messaget::eom;
574  }
575 
576  std::string filename=cmdline.args[0];
577 
578  #ifdef _MSC_VER
579  std::ifstream infile(widen(filename));
580  #else
581  std::ifstream infile(filename);
582  #endif
583 
584  if(!infile)
585  {
586  log.error() << "failed to open input file '" << filename << "'"
587  << messaget::eom;
589  }
590 
591  std::unique_ptr<languaget> language=
592  get_language_from_filename(filename);
593 
594  if(language==nullptr)
595  {
596  log.error() << "failed to figure out type of file '" << filename << "'"
597  << messaget::eom;
599  }
600 
601  language->set_language_options(options);
603 
604  log.status() << "Parsing " << filename << messaget::eom;
605 
606  if(language->parse(infile, filename))
607  {
608  log.error() << "PARSING ERROR" << messaget::eom;
610  }
611 
612  language->show_parse(std::cout);
613  return CPROVER_EXIT_SUCCESS;
614  }
615 
616  int get_goto_program_ret =
618 
619  if(get_goto_program_ret!=-1)
620  return get_goto_program_ret;
621 
622  if(cmdline.isset("show-claims") || // will go away
623  cmdline.isset("show-properties")) // use this one
624  {
626  return CPROVER_EXIT_SUCCESS;
627  }
628 
629  if(set_properties())
631 
632  if(
633  options.get_bool_option("program-only") ||
634  options.get_bool_option("show-vcc"))
635  {
636  if(options.get_bool_option("paths"))
637  {
639  options, ui_message_handler, goto_model);
640  (void)verifier();
641  }
642  else
643  {
645  options, ui_message_handler, goto_model);
646  (void)verifier();
647  }
648 
649  return CPROVER_EXIT_SUCCESS;
650  }
651 
652  if(
653  options.get_bool_option("dimacs") || !options.get_option("outfile").empty())
654  {
655  if(options.get_bool_option("paths"))
656  {
658  options, ui_message_handler, goto_model);
659  (void)verifier();
660  }
661  else
662  {
664  options, ui_message_handler, goto_model);
665  (void)verifier();
666  }
667 
668  return CPROVER_EXIT_SUCCESS;
669  }
670 
671  if(options.is_set("cover"))
672  {
674  verifier(options, ui_message_handler, goto_model);
675  (void)verifier();
676  verifier.report();
677 
678  c_test_input_generatort test_generator(ui_message_handler, options);
679  test_generator(verifier.get_traces());
680 
681  return CPROVER_EXIT_SUCCESS;
682  }
683 
684  std::unique_ptr<goto_verifiert> verifier = nullptr;
685 
686  if(options.is_set("incremental-loop"))
687  {
688  if(options.get_bool_option("stop-on-fail"))
689  {
690  verifier = util_make_unique<
692  options, ui_message_handler, goto_model);
693  }
694  else
695  {
698  options, ui_message_handler, goto_model);
699  }
700  }
701  else if(
702  options.get_bool_option("stop-on-fail") && options.get_bool_option("paths"))
703  {
704  verifier =
705  util_make_unique<stop_on_fail_verifiert<single_path_symex_checkert>>(
706  options, ui_message_handler, goto_model);
707  }
708  else if(
709  options.get_bool_option("stop-on-fail") &&
710  !options.get_bool_option("paths"))
711  {
712  if(options.get_bool_option("localize-faults"))
713  {
714  verifier =
717  }
718  else
719  {
720  verifier =
721  util_make_unique<stop_on_fail_verifiert<multi_path_symex_checkert>>(
722  options, ui_message_handler, goto_model);
723  }
724  }
725  else if(
726  !options.get_bool_option("stop-on-fail") &&
727  options.get_bool_option("paths"))
728  {
729  verifier = util_make_unique<
731  options, ui_message_handler, goto_model);
732  }
733  else if(
734  !options.get_bool_option("stop-on-fail") &&
735  !options.get_bool_option("paths"))
736  {
737  if(options.get_bool_option("localize-faults"))
738  {
739  verifier =
742  }
743  else
744  {
745  verifier = util_make_unique<
747  options, ui_message_handler, goto_model);
748  }
749  }
750  else
751  {
752  UNREACHABLE;
753  }
754 
755  const resultt result = (*verifier)();
756  verifier->report();
757 
758  return result_to_exit_code(result);
759 }
760 
762 {
763  if(cmdline.isset("claim")) // will go away
765 
766  if(cmdline.isset("property")) // use this one
768 
769  return false;
770 }
771 
773  goto_modelt &goto_model,
774  const optionst &options,
775  const cmdlinet &cmdline,
776  ui_message_handlert &ui_message_handler)
777 {
779  if(cmdline.args.empty())
780  {
781  log.error() << "Please provide a program to verify" << messaget::eom;
783  }
784 
786 
787  if(cmdline.isset("show-symbol-table"))
788  {
790  return CPROVER_EXIT_SUCCESS;
791  }
792 
795 
796  if(cmdline.isset("validate-goto-model"))
797  {
799  }
800 
801  // show it?
802  if(cmdline.isset("show-loops"))
803  {
805  return CPROVER_EXIT_SUCCESS;
806  }
807 
808  // show it?
809  if(
810  cmdline.isset("show-goto-functions") ||
811  cmdline.isset("list-goto-functions"))
812  {
814  goto_model, ui_message_handler, cmdline.isset("list-goto-functions"));
815  return CPROVER_EXIT_SUCCESS;
816  }
817 
819 
820  return -1; // no error, continue
821 }
822 
824 {
825  if(cmdline.args.size() != 1)
826  {
827  log.error() << "Please provide one program to preprocess" << messaget::eom;
828  return;
829  }
830 
831  std::string filename = cmdline.args[0];
832 
833  std::ifstream infile(filename);
834 
835  if(!infile)
836  {
837  log.error() << "failed to open input file" << messaget::eom;
838  return;
839  }
840 
841  std::unique_ptr<languaget> language = get_language_from_filename(filename);
842  language->set_language_options(options);
843 
844  if(language == nullptr)
845  {
846  log.error() << "failed to figure out type of file" << messaget::eom;
847  return;
848  }
849 
851 
852  if(language->preprocess(infile, filename, std::cout))
853  log.error() << "PREPROCESSING ERROR" << messaget::eom;
854 }
855 
857  goto_modelt &goto_model,
858  const optionst &options,
859  messaget &log)
860 {
861  // Remove inline assembler; this needs to happen before
862  // adding the library.
864 
865  // add the library
866  log.status() << "Adding CPROVER library (" << config.ansi_c.arch << ")"
867  << messaget::eom;
872 
873  if(options.get_bool_option("string-abstraction"))
875 
876  // remove function pointers
877  log.status() << "Removal of function pointers and virtual functions"
878  << messaget::eom;
881  goto_model,
882  options.get_bool_option("pointer-check"));
883 
884  mm_io(goto_model);
885 
886  // instrument library preconditions
888 
889  // remove returns, gcc vectors, complex
894 
895  // add generic checks
896  log.status() << "Generic Property Instrumentation" << messaget::eom;
897  goto_check(options, goto_model);
898 
899  // checks don't know about adjusted float expressions
901 
902  // ignore default/user-specified initialization
903  // of variables with static lifetime
904  if(options.get_bool_option("nondet-static"))
905  {
906  log.status() << "Adding nondeterministic initialization "
907  "of static/global variables"
908  << messaget::eom;
910  }
911 
912  if(options.get_bool_option("string-abstraction"))
913  {
914  log.status() << "String Abstraction" << messaget::eom;
916  }
917 
918  // add failed symbols
919  // needs to be done before pointer analysis
921 
922  // recalculate numbers, etc.
924 
925  // add loop ids
927 
928  if(options.get_bool_option("drop-unused-functions"))
929  {
930  // Entry point will have been set before and function pointers removed
931  log.status() << "Removing unused functions" << messaget::eom;
933  }
934 
935  // remove skips such that trivial GOTOs are deleted and not considered
936  // for coverage annotation:
938 
939  // instrument cover goals
940  if(options.is_set("cover"))
941  {
942  const auto cover_config = get_cover_config(
945  cover_config, goto_model, log.get_message_handler()))
946  return true;
947  }
948 
949  // label the assertions
950  // This must be done after adding assertions and
951  // before using the argument of the "property" option.
952  // Do not re-label after using the property slicer because
953  // this would cause the property identifiers to change.
955 
956  // reachability slice?
957  if(options.get_bool_option("reachability-slice-fb"))
958  {
959  log.status() << "Performing a forwards-backwards reachability slice"
960  << messaget::eom;
961  if(options.is_set("property"))
963  goto_model, options.get_list_option("property"), true);
964  else
966  }
967 
968  if(options.get_bool_option("reachability-slice"))
969  {
970  log.status() << "Performing a reachability slice" << messaget::eom;
971  if(options.is_set("property"))
972  reachability_slicer(goto_model, options.get_list_option("property"));
973  else
975  }
976 
977  // full slice?
978  if(options.get_bool_option("full-slice"))
979  {
980  log.status() << "Performing a full slice" << messaget::eom;
981  if(options.is_set("property"))
982  property_slicer(goto_model, options.get_list_option("property"));
983  else
985  }
986 
987  // remove any skips introduced since coverage instrumentation
989 
990  return false;
991 }
992 
995 {
996  // clang-format off
997  std::cout << '\n' << banner_string("CBMC", CBMC_VERSION) << '\n'
998  << align_center_with_border("Copyright (C) 2001-2018") << '\n'
999  << align_center_with_border("Daniel Kroening, Edmund Clarke") << '\n' // NOLINT(*)
1000  << align_center_with_border("Carnegie Mellon University, Computer Science Department") << '\n' // NOLINT(*)
1001  << align_center_with_border("kroening@kroening.com") << '\n' // NOLINT(*)
1002  << align_center_with_border("Protected in part by U.S. patent 7,225,417") << '\n' // NOLINT(*)
1003  <<
1004  "\n"
1005  "Usage: Purpose:\n"
1006  "\n"
1007  " cbmc [-?] [-h] [--help] show help\n"
1008  " cbmc file.c ... source file names\n"
1009  "\n"
1010  "Analysis options:\n"
1012  " --symex-coverage-report f generate a Cobertura XML coverage report in f\n" // NOLINT(*)
1013  " --property id only check one specific property\n"
1014  " --stop-on-fail stop analysis once a failed property is detected\n" // NOLINT(*)
1015  " --trace give a counterexample trace for failed properties\n" //NOLINT(*)
1016  "\n"
1017  "C/C++ frontend options:\n"
1018  " -I path set include path (C/C++)\n"
1019  " -D macro define preprocessor macro (C/C++)\n"
1020  " --preprocess stop after preprocessing\n"
1021  " --16, --32, --64 set width of int\n"
1022  " --LP64, --ILP64, --LLP64,\n"
1023  " --ILP32, --LP32 set width of int, long and pointers\n"
1024  " --little-endian allow little-endian word-byte conversions\n"
1025  " --big-endian allow big-endian word-byte conversions\n"
1026  " --unsigned-char make \"char\" unsigned by default\n"
1027  " --mm model set memory model (default: sc)\n"
1028  " --arch set architecture (default: "
1029  << configt::this_architecture() << ")\n"
1030  " --os set operating system (default: "
1031  << configt::this_operating_system() << ")\n"
1032  " --c89/99/11 set C language standard (default: "
1038  configt::ansi_ct::c_standardt::C11?"c11":"") << ")\n" // NOLINT(*)
1039  " --cpp98/03/11 set C++ language standard (default: "
1041  configt::cppt::cpp_standardt::CPP98?"cpp98": // NOLINT(*)
1043  configt::cppt::cpp_standardt::CPP03?"cpp03": // NOLINT(*)
1045  configt::cppt::cpp_standardt::CPP11?"cpp11":"") << ")\n" // NOLINT(*)
1046  #ifdef _WIN32
1047  " --gcc use GCC as preprocessor\n"
1048  #endif
1049  " --no-arch don't set up an architecture\n"
1050  " --no-library disable built-in abstract C library\n"
1051  " --round-to-nearest rounding towards nearest even (default)\n"
1052  " --round-to-plus-inf rounding towards plus infinity\n"
1053  " --round-to-minus-inf rounding towards minus infinity\n"
1054  " --round-to-zero rounding towards zero\n"
1057  "\n"
1058  "Program representations:\n"
1059  " --show-parse-tree show parse tree\n"
1060  " --show-symbol-table show loaded symbol table\n"
1062  "\n"
1063  "Program instrumentation options:\n"
1065  " --no-assertions ignore user assertions\n"
1066  " --no-assumptions ignore user assumptions\n"
1067  " --error-label label check that label is unreachable\n"
1068  " --cover CC create test-suite with coverage criterion CC\n" // NOLINT(*)
1069  " --mm MM memory consistency model for concurrent programs\n" // NOLINT(*)
1072  " --full-slice run full slicer (experimental)\n" // NOLINT(*)
1073  " --drop-unused-functions drop functions trivially unreachable from main function\n" // NOLINT(*)
1074  "\n"
1075  "Semantic transformations:\n"
1076  // NOLINTNEXTLINE(whitespace/line_length)
1077  " --nondet-static add nondeterministic initialization of variables with static lifetime\n"
1078  "\n"
1079  "BMC options:\n"
1080  HELP_BMC
1081  "\n"
1082  "Backend options:\n"
1083  " --object-bits n number of bits used for object addresses\n"
1084  " --dimacs generate CNF in DIMACS format\n"
1085  " --beautify beautify the counterexample (greedy heuristic)\n" // NOLINT(*)
1086  " --localize-faults localize faults (experimental)\n"
1087  " --smt2 use default SMT2 solver (Z3)\n"
1088  " --boolector use Boolector\n"
1089  " --cprover-smt2 use CPROVER SMT2 solver\n"
1090  " --cvc4 use CVC4\n"
1091  " --mathsat use MathSAT\n"
1092  " --yices use Yices\n"
1093  " --z3 use Z3\n"
1094  " --refine use refinement procedure (experimental)\n"
1096  " --outfile filename output formula to given file\n"
1097  " --arrays-uf-never never turn arrays into uninterpreted functions\n" // NOLINT(*)
1098  " --arrays-uf-always always turn arrays into uninterpreted functions\n" // NOLINT(*)
1099  "\n"
1100  "Other options:\n"
1101  " --version show version and exit\n"
1106  HELP_FLUSH
1107  " --verbosity # verbosity level\n"
1109  "\n";
1110  // clang-format on
1111 }
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:152
cprover_library.h
cmdlinet::args
argst args
Definition: cmdline.h:85
CBMC_VERSION
const char * CBMC_VERSION
Definition: version.cpp:1
cbmc_parse_optionst::doit
virtual int doit() override
invoke main modules
Definition: cbmc_parse_options.cpp:507
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
exception_utils.h
cover.h
HELP_REACHABILITY_SLICER
#define HELP_REACHABILITY_SLICER
Definition: reachability_slicer.h:43
HELP_BMC
#define HELP_BMC
Definition: bmc_util.h:200
configt::cppt::cpp_standardt::CPP98
@ CPP98
HELP_SHOW_GOTO_FUNCTIONS
#define HELP_SHOW_GOTO_FUNCTIONS
Definition: show_goto_functions.h:26
string_abstraction.h
languaget::show_parse
virtual void show_parse(std::ostream &out)=0
configt::object_bits_info
std::string object_bits_info()
Definition: config.cpp:1264
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:60
rewrite_union.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:114
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:772
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:28
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:168
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:400
multi_path_symex_only_checker.h
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
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
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_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:2143
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:283
string_abstraction
void string_abstraction(symbol_tablet &symbol_table, message_handlert &message_handler, goto_programt &dest)
Definition: string_abstraction.cpp:65
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:86
nondet_static.h
string_instrumentation.h
HELP_REACHABILITY_SLICER_FB
#define HELP_REACHABILITY_SLICER_FB
Definition: reachability_slicer.h:50
stop_on_fail_verifier_with_fault_localization.h
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
instrument_cover_goals
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)
Applies instrumenters to given goto program.
Definition: cover.cpp:33
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:45
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:141
util_make_unique
std::unique_ptr< T > util_make_unique(Ts &&... ts)
Definition: make_unique.h:19
bmc_util.h
remove_complex.h
set_properties.h
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:171
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
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
cover_goals_verifier_with_trace_storage.h
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:385
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
initialize_goto_model.h
banner_string
std::string banner_string(const std::string &front_end, const std::string &version)
Definition: parse_options.cpp:146
mm_io.h
c_test_input_generatort
Definition: c_test_input_generator.h:50
cbmc_parse_options.h
cbmc_parse_optionst::get_command_line_options
void get_command_line_options(optionst &)
Definition: cbmc_parse_options.cpp:129
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
configt::cppt::set_cpp11
void set_cpp11()
Definition: config.h:143
multi_path_symex_checker.h
cmdlinet::get_value
std::string get_value(char option) const
Definition: cmdline.cpp:46
show_symbol_table.h
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
messaget::set_message_handler
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:176
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:856
single_path_symex_checker.h
configt::this_operating_system
static irep_idt this_operating_system()
Definition: config.cpp:1375
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:137
cbmc_parse_optionst::set_properties
bool set_properties()
Definition: cbmc_parse_options.cpp:761
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:57
read_goto_binary.h
all_properties_verifier_with_fault_localization.h
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
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
remove_vector.h
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
remove_unused_functions.h
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:1275
configt::ansi_ct::c_standardt::C11
@ C11
messaget::get_message_handler
message_handlert & get_message_handler()
Definition: message.h:181
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
HELP_GOTO_CHECK
#define HELP_GOTO_CHECK
Definition: goto_check.h:44
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:77
configt::set
bool set(const cmdlinet &cmdline)
Definition: config.cpp:768
configt::cppt::default_cpp_standard
static cpp_standardt default_cpp_standard()
Definition: config.cpp:690
exit_codes.h
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:994
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
reachability_slicer.h
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
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
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
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:99
remove_skip.h
cbmc_parse_optionst::set_default_options
static void set_default_options(optionst &)
Set the options that have default values.
Definition: cbmc_parse_options.cpp:111
adjust_float_expressions.h
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:107
remove_function_pointers.h
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
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:133
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:105
CBMC_OPTIONS
#define CBMC_OPTIONS
Definition: cbmc_parse_options.h:41
configt::cppt::set_cpp03
void set_cpp03()
Definition: config.h:142
cbmc_parse_optionst::preprocessing
void preprocessing(const optionst &)
Definition: cbmc_parse_options.cpp:823
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