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/string2int.h>
20 #include <util/config.h>
21 #include <util/language.h>
22 #include <util/unicode.h>
23 #include <util/memory_info.h>
24 #include <util/invariant.h>
25 
26 #include <ansi-c/c_preprocess.h>
27 
39 #include <goto-programs/mm_io.h>
46 #include <goto-programs/loop_ids.h>
50 
53 
56 #include <goto-instrument/cover.h>
57 
59 
60 #include <langapi/mode.h>
61 
62 #include "cbmc_solvers.h"
63 #include "bmc.h"
64 #include "version.h"
65 #include "xml_interface.h"
66 
67 cbmc_parse_optionst::cbmc_parse_optionst(int argc, const char **argv):
68  parse_options_baset(CBMC_OPTIONS, argc, argv),
69  xml_interfacet(cmdline),
70  language_uit(cmdline, ui_message_handler),
71  ui_message_handler(cmdline, "CBMC " CBMC_VERSION)
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  language_uit(cmdline, ui_message_handler),
82  ui_message_handler(cmdline, "CBMC " CBMC_VERSION)
83 {
84 }
85 
87 {
88  // this is our default verbosity
89  unsigned int v=messaget::M_STATISTICS;
90 
91  if(cmdline.isset("verbosity"))
92  {
94  if(v>10)
95  v=10;
96  }
97 
99 }
100 
102 {
103  if(config.set(cmdline))
104  {
105  usage_error();
106  exit(1); // should contemplate EX_USAGE from sysexits.h
107  }
108 
109  if(cmdline.isset("program-only"))
110  options.set_option("program-only", true);
111 
112  if(cmdline.isset("show-vcc"))
113  options.set_option("show-vcc", true);
114 
115  if(cmdline.isset("cover"))
116  options.set_option("cover", cmdline.get_values("cover"));
117 
118  if(cmdline.isset("mm"))
119  options.set_option("mm", cmdline.get_value("mm"));
120 
121  if(cmdline.isset("c89"))
123 
124  if(cmdline.isset("c99"))
126 
127  if(cmdline.isset("c11"))
129 
130  if(cmdline.isset("cpp98"))
131  config.cpp.set_cpp98();
132 
133  if(cmdline.isset("cpp03"))
134  config.cpp.set_cpp03();
135 
136  if(cmdline.isset("cpp11"))
137  config.cpp.set_cpp11();
138 
139  if(cmdline.isset("no-simplify"))
140  options.set_option("simplify", false);
141  else
142  options.set_option("simplify", true);
143 
144  if(cmdline.isset("stop-on-fail") ||
145  cmdline.isset("dimacs") ||
146  cmdline.isset("outfile"))
147  options.set_option("stop-on-fail", true);
148  else
149  options.set_option("stop-on-fail", false);
150 
151  if(cmdline.isset("trace") ||
152  cmdline.isset("stop-on-fail"))
153  options.set_option("trace", true);
154 
155  if(cmdline.isset("localize-faults"))
156  options.set_option("localize-faults", true);
157  if(cmdline.isset("localize-faults-method"))
158  {
159  options.set_option(
160  "localize-faults-method",
161  cmdline.get_value("localize-faults-method"));
162  }
163 
164  if(cmdline.isset("unwind"))
165  options.set_option("unwind", cmdline.get_value("unwind"));
166 
167  if(cmdline.isset("depth"))
168  options.set_option("depth", cmdline.get_value("depth"));
169 
170  if(cmdline.isset("debug-level"))
171  options.set_option("debug-level", cmdline.get_value("debug-level"));
172 
173  if(cmdline.isset("slice-by-trace"))
174  options.set_option("slice-by-trace", cmdline.get_value("slice-by-trace"));
175 
176  if(cmdline.isset("unwindset"))
177  options.set_option("unwindset", cmdline.get_value("unwindset"));
178 
179  // constant propagation
180  if(cmdline.isset("no-propagation"))
181  options.set_option("propagation", false);
182  else
183  options.set_option("propagation", true);
184 
185  // all checks supported by goto_check
187 
188  // unwind loops in java enum static initialization
189  if(cmdline.isset("java-unwind-enum-static"))
190  options.set_option("java-unwind-enum-static", true);
191 
192  // check assertions
193  if(cmdline.isset("no-assertions"))
194  options.set_option("assertions", false);
195  else
196  options.set_option("assertions", true);
197 
198  // use assumptions
199  if(cmdline.isset("no-assumptions"))
200  options.set_option("assumptions", false);
201  else
202  options.set_option("assumptions", true);
203 
204  // magic error label
205  if(cmdline.isset("error-label"))
206  options.set_option("error-label", cmdline.get_values("error-label"));
207 
208  // generate unwinding assertions
209  if(cmdline.isset("cover"))
210  options.set_option("unwinding-assertions", false);
211  else
212  {
213  options.set_option(
214  "unwinding-assertions",
215  cmdline.isset("unwinding-assertions"));
216  }
217 
218  // generate unwinding assumptions otherwise
219  options.set_option(
220  "partial-loops",
221  cmdline.isset("partial-loops"));
222 
223  if(options.get_bool_option("partial-loops") &&
224  options.get_bool_option("unwinding-assertions"))
225  {
226  error() << "--partial-loops and --unwinding-assertions "
227  << "must not be given together" << eom;
228  exit(1); // should contemplate EX_USAGE from sysexits.h
229  }
230 
231  // remove unused equations
232  options.set_option(
233  "slice-formula",
234  cmdline.isset("slice-formula"));
235 
236  // simplify if conditions and branches
237  if(cmdline.isset("no-simplify-if"))
238  options.set_option("simplify-if", false);
239  else
240  options.set_option("simplify-if", true);
241 
242  if(cmdline.isset("arrays-uf-always"))
243  options.set_option("arrays-uf", "always");
244  else if(cmdline.isset("arrays-uf-never"))
245  options.set_option("arrays-uf", "never");
246  else
247  options.set_option("arrays-uf", "auto");
248 
249  if(cmdline.isset("dimacs"))
250  options.set_option("dimacs", true);
251 
252  if(cmdline.isset("refine-arrays"))
253  {
254  options.set_option("refine", true);
255  options.set_option("refine-arrays", true);
256  }
257 
258  if(cmdline.isset("refine-arithmetic"))
259  {
260  options.set_option("refine", true);
261  options.set_option("refine-arithmetic", true);
262  }
263 
264  if(cmdline.isset("refine"))
265  {
266  options.set_option("refine", true);
267  options.set_option("refine-arrays", true);
268  options.set_option("refine-arithmetic", true);
269  }
270 
271  if(cmdline.isset("max-node-refinement"))
272  options.set_option(
273  "max-node-refinement",
274  cmdline.get_value("max-node-refinement"));
275 
276  if(cmdline.isset("aig"))
277  options.set_option("aig", true);
278 
279  // SMT Options
280  bool version_set=false;
281 
282  if(cmdline.isset("smt1"))
283  {
284  options.set_option("smt1", true);
285  options.set_option("smt2", false);
286  version_set=true;
287  }
288 
289  if(cmdline.isset("smt2"))
290  {
291  // If both are given, smt2 takes precedence
292  options.set_option("smt1", false);
293  options.set_option("smt2", true);
294  version_set=true;
295  }
296 
297  if(cmdline.isset("fpa"))
298  options.set_option("fpa", true);
299 
300 
301  bool solver_set=false;
302 
303  if(cmdline.isset("boolector"))
304  {
305  options.set_option("boolector", true), solver_set=true;
306  if(!version_set)
307  options.set_option("smt2", true), version_set=true;
308  }
309 
310  if(cmdline.isset("mathsat"))
311  {
312  options.set_option("mathsat", true), solver_set=true;
313  if(!version_set)
314  options.set_option("smt2", true), version_set=true;
315  }
316 
317  if(cmdline.isset("cvc3"))
318  {
319  options.set_option("cvc3", true), solver_set=true;
320  if(!version_set)
321  options.set_option("smt1", true), version_set=true;
322  }
323 
324  if(cmdline.isset("cvc4"))
325  {
326  options.set_option("cvc4", true), solver_set=true;
327  if(!version_set)
328  options.set_option("smt2", true), version_set=true;
329  }
330 
331  if(cmdline.isset("yices"))
332  {
333  options.set_option("yices", true), solver_set=true;
334  if(!version_set)
335  options.set_option("smt2", true), version_set=true;
336  }
337 
338  if(cmdline.isset("z3"))
339  {
340  options.set_option("z3", true), solver_set=true;
341  if(!version_set)
342  options.set_option("smt2", true), version_set=true;
343  }
344 
345  if(cmdline.isset("opensmt"))
346  {
347  options.set_option("opensmt", true), solver_set=true;
348  if(!version_set)
349  options.set_option("smt1", true), version_set=true;
350  }
351 
352  if(version_set && !solver_set)
353  {
354  if(cmdline.isset("outfile"))
355  {
356  // outfile and no solver should give standard compliant SMT-LIB
357  options.set_option("generic", true), solver_set=true;
358  }
359  else
360  {
361  if(options.get_bool_option("smt1"))
362  {
363  options.set_option("boolector", true), solver_set=true;
364  }
365  else
366  {
367  assert(options.get_bool_option("smt2"));
368  options.set_option("z3", true), solver_set=true;
369  }
370  }
371  }
372  // Either have solver and standard version set, or neither.
373  assert(version_set==solver_set);
374 
375  if(cmdline.isset("beautify"))
376  options.set_option("beautify", true);
377 
378  if(cmdline.isset("no-sat-preprocessor"))
379  options.set_option("sat-preprocessor", false);
380  else
381  options.set_option("sat-preprocessor", true);
382 
383  options.set_option(
384  "pretty-names",
385  !cmdline.isset("no-pretty-names"));
386 
387  if(cmdline.isset("outfile"))
388  options.set_option("outfile", cmdline.get_value("outfile"));
389 
390  if(cmdline.isset("graphml-witness"))
391  {
392  options.set_option("graphml-witness", cmdline.get_value("graphml-witness"));
393  options.set_option("stop-on-fail", true);
394  options.set_option("trace", true);
395  }
396 
397  if(cmdline.isset("symex-coverage-report"))
398  options.set_option(
399  "symex-coverage-report",
400  cmdline.get_value("symex-coverage-report"));
401 }
402 
405 {
406  if(cmdline.isset("version"))
407  {
408  std::cout << CBMC_VERSION << '\n';
409  return 0; // should contemplate EX_OK from sysexits.h
410  }
411 
412  //
413  // command line options
414  //
415 
416  optionst options;
417  get_command_line_options(options);
418  eval_verbosity();
419 
420  //
421  // Print a banner
422  //
423  status() << "CBMC version " CBMC_VERSION " "
424  << sizeof(void *)*8 << "-bit "
425  << config.this_architecture() << " "
427 
428  //
429  // Unwinding of transition systems is done by hw-cbmc.
430  //
431 
432  if(cmdline.isset("module") ||
433  cmdline.isset("gen-interface"))
434  {
435  error() << "This version of CBMC has no support for "
436  " hardware modules. Please use hw-cbmc." << eom;
437  return 1; // should contemplate EX_USAGE from sysexits.h
438  }
439 
441 
442  if(cmdline.isset("test-preprocessor"))
444 
445  if(cmdline.isset("preprocess"))
446  {
447  preprocessing();
448  return 0; // should contemplate EX_OK from sysexits.h
449  }
450 
451  goto_functionst goto_functions;
452 
453  expr_listt bmc_constraints;
454 
455  int get_goto_program_ret=
456  get_goto_program(options, bmc_constraints, goto_functions);
457 
458  if(get_goto_program_ret!=-1)
459  return get_goto_program_ret;
460 
461  if(cmdline.isset("show-claims") || // will go away
462  cmdline.isset("show-properties")) // use this one
463  {
464  const namespacet ns(symbol_table);
465  show_properties(ns, get_ui(), goto_functions);
466  return 0; // should contemplate EX_OK from sysexits.h
467  }
468 
469  if(set_properties(goto_functions))
470  return 7; // should contemplate EX_USAGE from sysexits.h
471 
472  // unwinds <clinit> loops to number of enum elements
473  // side effect: add this as explicit unwind to unwind set
474  if(options.get_bool_option("java-unwind-enum-static"))
475  remove_static_init_loops(symbol_table, goto_functions, options);
476 
477  // get solver
478  cbmc_solverst cbmc_solvers(options, symbol_table, ui_message_handler);
479  cbmc_solvers.set_ui(get_ui());
480 
481  std::unique_ptr<cbmc_solverst::solvert> cbmc_solver;
482 
483  try
484  {
485  cbmc_solver=cbmc_solvers.get_solver();
486  }
487 
488  catch(const char *error_msg)
489  {
490  error() << error_msg << eom;
491  return 1; // should contemplate EX_SOFTWARE from sysexits.h
492  }
493 
494  prop_convt &prop_conv=cbmc_solver->prop_conv();
495 
496  bmct bmc(options, symbol_table, ui_message_handler, prop_conv);
497 
498  // do actual BMC
499  return do_bmc(bmc, goto_functions);
500 }
501 
503 {
504  try
505  {
506  if(cmdline.isset("claim")) // will go away
507  ::set_properties(goto_functions, cmdline.get_values("claim"));
508 
509  if(cmdline.isset("property")) // use this one
510  ::set_properties(goto_functions, cmdline.get_values("property"));
511  }
512 
513  catch(const char *e)
514  {
515  error() << e << eom;
516  return true;
517  }
518 
519  catch(const std::string e)
520  {
521  error() << e << eom;
522  return true;
523  }
524 
525  catch(int)
526  {
527  return true;
528  }
529 
530  return false;
531 }
532 
534  const optionst &options,
535  expr_listt &bmc_constraints, // for get_modules
536  goto_functionst &goto_functions)
537 {
538  if(cmdline.args.empty())
539  {
540  error() << "Please provide a program to verify" << eom;
541  return 6;
542  }
543 
544  try
545  {
546  if(cmdline.isset("show-parse-tree"))
547  {
548  if(cmdline.args.size()!=1 ||
550  {
551  error() << "Please give exactly one source file" << eom;
552  return 6;
553  }
554 
555  std::string filename=cmdline.args[0];
556 
557  #ifdef _MSC_VER
558  std::ifstream infile(widen(filename));
559  #else
560  std::ifstream infile(filename);
561  #endif
562 
563  if(!infile)
564  {
565  error() << "failed to open input file `"
566  << filename << "'" << eom;
567  return 6;
568  }
569 
570  languaget *language=get_language_from_filename(filename);
571 
572  if(language==nullptr)
573  {
574  error() << "failed to figure out type of file `"
575  << filename << "'" << eom;
576  return 6;
577  }
578 
580 
581  status() << "Parsing " << filename << eom;
582 
583  if(language->parse(infile, filename))
584  {
585  error() << "PARSING ERROR" << eom;
586  return 6;
587  }
588 
589  language->show_parse(std::cout);
590  return 0;
591  }
592 
593  cmdlinet::argst binaries;
594  binaries.reserve(cmdline.args.size());
595 
596  for(cmdlinet::argst::iterator
597  it=cmdline.args.begin();
598  it!=cmdline.args.end();
599  ) // no ++it
600  {
601  if(is_goto_binary(*it))
602  {
603  binaries.push_back(*it);
604  it=cmdline.args.erase(it);
605  continue;
606  }
607 
608  ++it;
609  }
610 
611  if(!cmdline.args.empty())
612  {
613  if(parse())
614  return 6;
615  if(typecheck())
616  return 6;
617  int get_modules_ret=get_modules(bmc_constraints);
618  if(get_modules_ret!=-1)
619  return get_modules_ret;
620  if(binaries.empty() && final())
621  return 6;
622 
623  // we no longer need any parse trees or language files
624  clear_parse();
625  }
626 
627  for(const auto &bin : binaries)
628  {
629  status() << "Reading GOTO program from file " << eom;
630 
632  bin,
633  symbol_table,
634  goto_functions,
636  {
637  return 6;
638  }
639  }
640 
641  if(!binaries.empty())
643 
644  if(cmdline.isset("show-symbol-table"))
645  {
647  return 0;
648  }
649 
650  status() << "Generating GOTO Program" << eom;
651 
652  goto_convert(symbol_table, goto_functions, ui_message_handler);
653 
654  if(process_goto_program(options, goto_functions))
655  return 6;
656 
657  // show it?
658  if(cmdline.isset("show-loops"))
659  {
660  show_loop_ids(get_ui(), goto_functions);
661  return 0;
662  }
663 
664  // show it?
665  if(cmdline.isset("show-goto-functions"))
666  {
668  show_goto_functions(ns, get_ui(), goto_functions);
669  return 0;
670  }
671  }
672 
673  catch(const char *e)
674  {
675  error() << e << eom;
676  return 6;
677  }
678 
679  catch(const std::string e)
680  {
681  error() << e << eom;
682  return 6;
683  }
684 
685  catch(int)
686  {
687  return 6;
688  }
689 
690  catch(std::bad_alloc)
691  {
692  error() << "Out of memory" << eom;
693  return 6;
694  }
695 
696  return -1; // no error, continue
697 }
698 
700 {
701  try
702  {
703  if(cmdline.args.size()!=1)
704  {
705  error() << "Please provide one program to preprocess" << eom;
706  return;
707  }
708 
709  std::string filename=cmdline.args[0];
710 
711  std::ifstream infile(filename);
712 
713  if(!infile)
714  {
715  error() << "failed to open input file" << eom;
716  return;
717  }
718 
719  languaget *ptr=get_language_from_filename(filename);
720 
721  if(ptr==nullptr)
722  {
723  error() << "failed to figure out type of file" << eom;
724  return;
725  }
726 
728 
729  std::unique_ptr<languaget> language(ptr);
730 
731  if(language->preprocess(infile, filename, std::cout))
732  error() << "PREPROCESSING ERROR" << eom;
733  }
734 
735  catch(const char *e)
736  {
737  error() << e << eom;
738  }
739 
740  catch(const std::string e)
741  {
742  error() << e << eom;
743  }
744 
745  catch(int)
746  {
747  }
748 
749  catch(std::bad_alloc)
750  {
751  error() << "Out of memory" << eom;
752  }
753 }
754 
756  const optionst &options,
757  goto_functionst &goto_functions)
758 {
759  try
760  {
762 
763  // Remove inline assembler; this needs to happen before
764  // adding the library.
765  remove_asm(symbol_table, goto_functions);
766 
767  // add the library
769 
770  if(cmdline.isset("string-abstraction"))
772  symbol_table, get_message_handler(), goto_functions);
773 
774  // remove function pointers
775  status() << "Removal of function pointers and virtual functions" << eom;
778  symbol_table,
779  goto_functions,
780  cmdline.isset("pointer-check"));
781  // Java virtual functions -> explicit dispatch tables:
782  remove_virtual_functions(symbol_table, goto_functions);
783  // remove catch and throw
784  remove_exceptions(symbol_table, goto_functions);
785  // Similar removal of RTTI inspection:
786  remove_instanceof(symbol_table, goto_functions);
787 
788  mm_io(symbol_table, goto_functions);
789 
790  // do partial inlining
791  status() << "Partial Inlining" << eom;
792  goto_partial_inline(goto_functions, ns, ui_message_handler);
793 
794  // remove returns, gcc vectors, complex
795  remove_returns(symbol_table, goto_functions);
796  remove_vector(symbol_table, goto_functions);
797  remove_complex(symbol_table, goto_functions);
798  rewrite_union(goto_functions, ns);
799 
800  // add generic checks
801  status() << "Generic Property Instrumentation" << eom;
802  goto_check(ns, options, goto_functions);
803 
804  // checks don't know about adjusted float expressions
805  adjust_float_expressions(goto_functions, ns);
806 
807  // ignore default/user-specified initialization
808  // of variables with static lifetime
809  if(cmdline.isset("nondet-static"))
810  {
811  status() << "Adding nondeterministic initialization "
812  "of static/global variables" << eom;
813  nondet_static(ns, goto_functions);
814  }
815 
816  if(cmdline.isset("string-abstraction"))
817  {
818  status() << "String Abstraction" << eom;
820  symbol_table,
822  goto_functions);
823  }
824 
825  // add failed symbols
826  // needs to be done before pointer analysis
828 
829  // recalculate numbers, etc.
830  goto_functions.update();
831 
832  // add loop ids
833  goto_functions.compute_loop_numbers();
834 
835  if(cmdline.isset("drop-unused-functions"))
836  {
837  // Entry point will have been set before and function pointers removed
838  status() << "Removing unused functions" << eom;
840  }
841 
842  // instrument cover goals
843  if(cmdline.isset("cover"))
844  {
846  cmdline,
847  symbol_table,
848  goto_functions,
850  return true;
851  }
852 
853  // label the assertions
854  // This must be done after adding assertions and
855  // before using the argument of the "property" option.
856  // Do not re-label after using the property slicer because
857  // this would cause the property identifiers to change.
858  label_properties(goto_functions);
859 
860  // full slice?
861  if(cmdline.isset("full-slice"))
862  {
863  status() << "Performing a full slice" << eom;
864  if(cmdline.isset("property"))
865  property_slicer(goto_functions, ns, cmdline.get_values("property"));
866  else
867  full_slicer(goto_functions, ns);
868  }
869 
870  // remove skips
871  remove_skip(goto_functions);
872  goto_functions.update();
873  }
874 
875  catch(const char *e)
876  {
877  error() << e << eom;
878  return true;
879  }
880 
881  catch(const std::string e)
882  {
883  error() << e << eom;
884  return true;
885  }
886 
887  catch(int)
888  {
889  return true;
890  }
891 
892  catch(std::bad_alloc)
893  {
894  error() << "Out of memory" << eom;
895  return true;
896  }
897 
898  return false;
899 }
900 
903  bmct &bmc,
904  const goto_functionst &goto_functions)
905 {
906  bmc.set_ui(get_ui());
907 
908  int result=6;
909 
910  // do actual BMC
911  switch(bmc.run(goto_functions))
912  {
914  result=0;
915  break;
917  result=10;
918  break;
920  result=6;
921  break;
922  }
923 
924  // let's log some more statistics
925  debug() << "Memory consumption:" << messaget::endl;
926  memory_info(debug());
927  debug() << eom;
928 
929  return result;
930 }
931 
934 {
935  std::cout <<
936  "\n"
937  "* * CBMC " CBMC_VERSION " - Copyright (C) 2001-2017 ";
938 
939  std::cout << "(" << (sizeof(void *)*8) << "-bit version)";
940 
941  std::cout << " * *\n";
942 
943  std::cout <<
944  "* * Daniel Kroening, Edmund Clarke * *\n"
945  "* * Carnegie Mellon University, Computer Science Department * *\n"
946  "* * kroening@kroening.com * *\n"
947  "* * Protected in part by U.S. patent 7,225,417 * *\n"
948  "\n"
949  "Usage: Purpose:\n"
950  "\n"
951  " cbmc [-?] [-h] [--help] show help\n"
952  " cbmc file.c ... source file names\n"
953  "\n"
954  "Analysis options:\n"
955  " --show-properties show the properties, but don't run analysis\n" // NOLINT(*)
956  " --symex-coverage-report f generate a Cobertura XML coverage report in f\n" // NOLINT(*)
957  " --property id only check one specific property\n"
958  " --stop-on-fail stop analysis once a failed property is detected\n" // NOLINT(*)
959  " --trace give a counterexample trace for failed properties\n" //NOLINT(*)
960  "\n"
961  "C/C++ frontend options:\n"
962  " -I path set include path (C/C++)\n"
963  " -D macro define preprocessor macro (C/C++)\n"
964  " --preprocess stop after preprocessing\n"
965  " --16, --32, --64 set width of int\n"
966  " --LP64, --ILP64, --LLP64,\n"
967  " --ILP32, --LP32 set width of int, long and pointers\n"
968  " --little-endian allow little-endian word-byte conversions\n"
969  " --big-endian allow big-endian word-byte conversions\n"
970  " --unsigned-char make \"char\" unsigned by default\n"
971  " --mm model set memory model (default: sc)\n"
972  " --arch set architecture (default: "
973  << configt::this_architecture() << ")\n"
974  " --os set operating system (default: "
975  << configt::this_operating_system() << ")\n"
976  " --c89/99/11 set C language standard (default: "
982  configt::ansi_ct::c_standardt::C11?"c11":"") << ")\n" // NOLINT(*)
983  " --cpp98/03/11 set C++ language standard (default: "
985  configt::cppt::cpp_standardt::CPP98?"cpp98": // NOLINT(*)
987  configt::cppt::cpp_standardt::CPP03?"cpp03": // NOLINT(*)
989  configt::cppt::cpp_standardt::CPP11?"cpp11":"") << ")\n" // NOLINT(*)
990  #ifdef _WIN32
991  " --gcc use GCC as preprocessor\n"
992  #endif
993  " --no-arch don't set up an architecture\n"
994  " --no-library disable built-in abstract C library\n"
995  " --round-to-nearest rounding towards nearest even (default)\n"
996  " --round-to-plus-inf rounding towards plus infinity\n"
997  " --round-to-minus-inf rounding towards minus infinity\n"
998  " --round-to-zero rounding towards zero\n"
999  " --function name set main function name\n"
1000  "\n"
1001  "Program representations:\n"
1002  " --show-parse-tree show parse tree\n"
1003  " --show-symbol-table show symbol table\n"
1005  " --drop-unused-functions drop functions trivially unreachable from main function\n" // NOLINT(*)
1006  "\n"
1007  "Program instrumentation options:\n"
1009  " --no-assertions ignore user assertions\n"
1010  " --no-assumptions ignore user assumptions\n"
1011  " --error-label label check that label is unreachable\n"
1012  " --cover CC create test-suite with coverage criterion CC\n" // NOLINT(*)
1013  " --mm MM memory consistency model for concurrent programs\n" // NOLINT(*)
1014  "\n"
1015  "Java Bytecode frontend options:\n"
1016  " --classpath dir/jar set the classpath\n"
1017  " --main-class class-name set the name of the main class\n"
1018  // NOLINTNEXTLINE(whitespace/line_length)
1019  " --java-max-vla-length limit the length of user-code-created arrays\n"
1020  // NOLINTNEXTLINE(whitespace/line_length)
1021  " --java-cp-include-files regexp or JSON list of files to load (with '@' prefix)\n"
1022  " --java-unwind-enum-static try to unwind loops in static initialization of enums\n"
1023  "\n"
1024  "Semantic transformations:\n"
1025  " --nondet-static add nondeterministic initialization of variables with static lifetime\n" // NOLINT(*)
1026  "\n"
1027  "BMC options:\n"
1028  " --program-only only show program expression\n"
1029  " --show-loops show the loops in the program\n"
1030  " --depth nr limit search depth\n"
1031  " --unwind nr unwind nr times\n"
1032  " --unwindset L:B,... unwind loop L with a bound of B\n"
1033  " (use --show-loops to get the loop IDs)\n"
1034  " --show-vcc show the verification conditions\n"
1035  " --slice-formula remove assignments unrelated to property\n"
1036  " --unwinding-assertions generate unwinding assertions\n"
1037  " --partial-loops permit paths with partial loops\n"
1038  " --no-pretty-names do not simplify identifiers\n"
1039  " --graphml-witness filename write the witness in GraphML format to filename\n" // NOLINT(*)
1040  "\n"
1041  "Backend options:\n"
1042  " --dimacs generate CNF in DIMACS format\n"
1043  " --beautify beautify the counterexample (greedy heuristic)\n" // NOLINT(*)
1044  " --localize-faults localize faults (experimental)\n"
1045  " --smt1 use default SMT1 solver (obsolete)\n"
1046  " --smt2 use default SMT2 solver (Z3)\n"
1047  " --boolector use Boolector\n"
1048  " --mathsat use MathSAT\n"
1049  " --cvc4 use CVC4\n"
1050  " --yices use Yices\n"
1051  " --z3 use Z3\n"
1052  " --refine use refinement procedure (experimental)\n"
1053  " --outfile filename output formula to given file\n"
1054  " --arrays-uf-never never turn arrays into uninterpreted functions\n" // NOLINT(*)
1055  " --arrays-uf-always always turn arrays into uninterpreted functions\n" // NOLINT(*)
1056  "\n"
1057  "Other options:\n"
1058  " --version show version and exit\n"
1059  " --xml-ui use XML-formatted output\n"
1060  " --xml-interface bi-directional XML interface\n"
1061  " --json-ui use JSON-formatted output\n"
1062  " --verbosity # verbosity level\n"
1063  "\n";
1064 }
symbol_tablet symbol_table
Definition: language_ui.h:24
const std::list< std::string > & get_values(const std::string &option) const
Definition: cmdline.cpp:90
Symbolic Execution.
mstreamt & result()
Definition: message.h:233
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 string_abstraction(symbol_tablet &symbol_table, message_handlert &message_handler, goto_programt &dest)
void goto_convert(const codet &code, symbol_tablet &symbol_table, goto_programt &dest, message_handlert &message_handler)
virtual bool parse()
Definition: language_ui.cpp:37
Remove function exceptional returns.
Remove Instance-of Operators.
void remove_asm(symbol_tablet &symbol_table, goto_functionst &goto_functions)
removes assembler
Definition: remove_asm.cpp:317
Remove Indirect Function Calls.
std::wstring widen(const char *s)
Definition: unicode.cpp:56
Remove Virtual Function (Method) Calls.
mstreamt & status()
Definition: message.h:238
void remove_unused_functions(goto_functionst &functions, message_handlert &message_handler)
void goto_check(const namespacet &ns, const optionst &options, goto_functionst::goto_functiont &goto_function)
uit get_ui()
Definition: language_ui.h:47
bool set_properties(goto_functionst &goto_functions)
unsigned unsafe_string2unsigned(const std::string &str, int base)
Definition: string2int.cpp:66
void remove_static_init_loops(const symbol_tablet &symbol_table, const goto_functionst &goto_functions, optionst &options)
this is the entry point for the removal of loops in static initialization code of Java enums ...
Show the goto functions.
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:46
prop_convt & prop_conv() const
Definition: cbmc_solvers.h:72
void show_properties(const namespacet &ns, const irep_idt &identifier, ui_message_handlert::uit ui, const goto_programt &goto_program)
void set_cpp98()
Definition: config.h:128
virtual bool typecheck()
Definition: language_ui.cpp:99
virtual void show_symbol_table(bool brief=false)
virtual bool preprocess(std::istream &instream, const std::string &path, std::ostream &outstream)
Definition: language.h:35
Pointer Dereferencing.
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
String Abstraction.
configt config
Definition: config.cpp:21
Remove &#39;asm&#39; statements by compiling into suitable standard code.
void remove_exceptions(symbol_tablet &symbol_table, goto_functionst &goto_functions)
removes throws/CATCH-POP/CATCH-PUSH
void remove_virtual_functions(const symbol_tablet &symbol_table, goto_functionst &goto_functions)
void goto_partial_inline(goto_modelt &goto_model, message_handlert &message_handler, unsigned smallfunc_limit, bool adjust_function)
Inline all function calls to functions either marked as "inlined" or smaller than smallfunc_limit (by...
Set the properties to check.
#define HELP_GOTO_CHECK
Definition: goto_check.h:41
Unused function removal.
bool set(const cmdlinet &cmdline)
Definition: config.cpp:727
void set_c89()
Definition: config.h:50
virtual void get_command_line_options(optionst &options)
virtual int do_bmc(bmct &bmc, const goto_functionst &goto_functions)
invoke main modules
Perform Memory-mapped I/O instrumentation.
argst args
Definition: cmdline.h:35
void string_instrumentation(symbol_tablet &symbol_table, message_handlert &message_handler, goto_programt &dest)
virtual bool isset(char option) const
Definition: cmdline.cpp:30
#define CBMC_OPTIONS
virtual std::unique_ptr< solvert > get_solver()
Definition: cbmc_solvers.h:106
void remove_instanceof(symbol_tablet &symbol_table, goto_functionst &goto_functions)
See function above.
virtual bool process_goto_program(const optionst &options, goto_functionst &goto_functions)
String Abstraction.
void set_ui(language_uit::uit _ui)
Definition: bmc.h:59
virtual int get_modules(expr_listt &bmc_constraints)
Nondeterministic initialization of certain global scope variables.
void instrument_cover_goals(const symbol_tablet &symbol_table, goto_programt &goto_program, coverage_criteriont criterion)
Definition: cover.cpp:832
bool get_bool_option(const std::string &option) const
Definition: options.cpp:42
TO_BE_DOCUMENTED.
Definition: namespace.h:62
Function Inlining.
static mstreamt & endl(mstreamt &m)
Definition: message.h:211
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 resultt run(const goto_functionst &goto_functions)
Definition: bmc.cpp:310
void set_ui(language_uit::uit _ui)
Definition: cbmc_solvers.h:128
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:122
void full_slicer(goto_functionst &goto_functions, const namespacet &ns, slicing_criteriont &criterion)
std::vector< std::string > argst
Definition: cmdline.h:34
Remove function returns.
void property_slicer(goto_functionst &goto_functions, const namespacet &ns, const std::list< std::string > &properties)
void adjust_float_expressions(exprt &expr, const namespacet &ns)
This adds the rounding mode to floating-point operations, including those in vectors and complex numb...
CBMC Command Line Option Processing.
bool read_object_and_link(const std::string &file_name, symbol_tablet &symbol_table, goto_functionst &functions, message_handlert &message_handler)
reads an object file
std::list< exprt > expr_listt
Definition: expr.h:166
#define PARSE_OPTIONS_GOTO_CHECK(cmdline, options)
Definition: goto_check.h:55
Symbolic Execution.
void set_c11()
Definition: config.h:52
void set_from_symbol_table(const symbol_tablet &)
Definition: config.cpp:1091
virtual int doit() override
invoke main modules
static c_standardt default_c_standard()
Definition: config.cpp:645
bool test_c_preprocessor(message_handlert &message_handler)
virtual void show_parse(std::ostream &out)=0
virtual int get_goto_program(const optionst &options, expr_listt &bmc_constraints, goto_functionst &goto_functions)
virtual void clear_parse()
Definition: language_ui.h:36
static irep_idt this_operating_system()
Definition: config.cpp:1258
mstreamt & debug()
Definition: message.h:253
struct configt::cppt cpp
void remove_skip(goto_programt &goto_program)
remove unnecessary skip statements
Definition: remove_skip.cpp:71
void set_c99()
Definition: config.h:51
message_handlert & get_message_handler()
Definition: message.h:127
Bounded Model Checking for ANSI-C + HDL.
void set_cpp11()
Definition: config.h:130
Goto Programs with Functions.
#define HELP_SHOW_GOTO_FUNCTIONS
languaget * get_language_from_filename(const std::string &filename)
Definition: mode.cpp:51
cbmc_parse_optionst(int argc, const char **argv)
Slicing.
void memory_info(std::ostream &out)
Definition: memory_info.cpp:28
Definition: bmc.h:32
void remove_returns(symbol_tablet &symbol_table, goto_functionst &goto_functions)
removes returns
Bounded Model Checking for ANSI-C + HDL.
mstreamt & error()
Definition: message.h:223
Remove the &#39;vector&#39; data type by compilation into arrays.
void set_verbosity(unsigned _verbosity)
Definition: message.h:44
#define CBMC_VERSION
Definition: version.h:4
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.
void set_option(const std::string &option, const bool value)
Definition: options.cpp:24
void add_failed_symbols(symbol_tablet &symbol_table)
static void remove_complex(typet &)
removes complex data type
ui_message_handlert ui_message_handler
void show_goto_functions(const namespacet &ns, ui_message_handlert::uit ui, const goto_functionst &goto_functions)
virtual bool parse(std::istream &instream, const std::string &path)=0
Program Transformation.
static cpp_standardt default_cpp_standard()
Definition: config.cpp:658
Unwind loops in static initializers.
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:129
void label_properties(goto_modelt &goto_model)
XML Interface.
static void remove_vector(typet &)
removes vector data type
static irep_idt this_architecture()
Definition: config.cpp:1148
void nondet_static(const namespacet &ns, goto_functionst &goto_functions, const irep_idt &fct_name)
virtual void help() override
display command line help
virtual void register_languages()