cprover
jbmc_parse_options.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: JBMC Command Line Option Processing
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "jbmc_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/make_unique.h>
23 #include <util/unicode.h>
24 #include <util/version.h>
25 #include <util/xml.h>
26 
27 #include <langapi/language.h>
28 
29 #include <ansi-c/ansi_c_language.h>
30 
36 
41 #include <goto-programs/loop_ids.h>
50 
54 
56 
58 
60 
61 #include <langapi/mode.h>
62 
76 
77 jbmc_parse_optionst::jbmc_parse_optionst(int argc, const char **argv)
80  argc,
81  argv,
82  std::string("JBMC ") + CBMC_VERSION)
83 {
86 }
87 
89  int argc,
90  const char **argv,
91  const std::string &extra_options)
93  JBMC_OPTIONS + extra_options,
94  argc,
95  argv,
96  std::string("JBMC ") + CBMC_VERSION)
97 {
100 }
101 
103 {
104  // Default true
105  options.set_option("assertions", true);
106  options.set_option("assumptions", true);
107  options.set_option("built-in-assertions", true);
108  options.set_option("lazy-methods", true);
109  options.set_option("pretty-names", true);
110  options.set_option("propagation", true);
111  options.set_option("refine-strings", true);
112  options.set_option("sat-preprocessor", true);
113  options.set_option("simple-slice", true);
114  options.set_option("simplify", true);
115  options.set_option("simplify-if", true);
116  options.set_option("show-goto-symex-steps", false);
117 
118  // Other default
119  options.set_option("arrays-uf", "auto");
120 }
121 
123 {
124  if(config.set(cmdline))
125  {
126  usage_error();
127  exit(1); // should contemplate EX_USAGE from sysexits.h
128  }
129 
131 
132  if(cmdline.isset("function"))
133  options.set_option("function", cmdline.get_value("function"));
134 
137 
138  if(cmdline.isset("max-field-sensitivity-array-size"))
139  {
140  options.set_option(
141  "max-field-sensitivity-array-size",
142  cmdline.get_value("max-field-sensitivity-array-size"));
143  }
144 
145  if(cmdline.isset("no-array-field-sensitivity"))
146  {
147  if(cmdline.isset("max-field-sensitivity-array-size"))
148  {
149  log.error()
150  << "--no-array-field-sensitivity and --max-field-sensitivity-array-size"
151  << " must not be given together" << messaget::eom;
153  }
154  options.set_option("no-array-field-sensitivity", true);
155  }
156 
157  if(cmdline.isset("show-symex-strategies"))
158  {
160  exit(CPROVER_EXIT_SUCCESS);
161  }
162 
164 
165  if(cmdline.isset("program-only"))
166  options.set_option("program-only", true);
167 
168  if(cmdline.isset("show-vcc"))
169  options.set_option("show-vcc", true);
170 
171  if(cmdline.isset("nondet-static"))
172  options.set_option("nondet-static", true);
173 
174  if(cmdline.isset("no-simplify"))
175  options.set_option("simplify", false);
176 
177  if(cmdline.isset("stop-on-fail") ||
178  cmdline.isset("dimacs") ||
179  cmdline.isset("outfile"))
180  options.set_option("stop-on-fail", true);
181 
182  if(
183  cmdline.isset("trace") || cmdline.isset("compact-trace") ||
184  cmdline.isset("stack-trace") || cmdline.isset("stop-on-fail") ||
186  !cmdline.isset("cover")))
187  {
188  options.set_option("trace", true);
189  }
190 
191  if(cmdline.isset("validate-trace"))
192  {
193  options.set_option("validate-trace", true);
194  options.set_option("trace", true);
195  }
196 
197  if(cmdline.isset("localize-faults"))
198  options.set_option("localize-faults", true);
199 
200  if(cmdline.isset("symex-complexity-limit"))
201  {
202  options.set_option(
203  "symex-complexity-limit", cmdline.get_value("symex-complexity-limit"));
204  }
205 
206  if(cmdline.isset("symex-complexity-failed-child-loops-limit"))
207  {
208  options.set_option(
209  "symex-complexity-failed-child-loops-limit",
210  cmdline.get_value("symex-complexity-failed-child-loops-limit"));
211  }
212 
213  if(cmdline.isset("unwind"))
214  options.set_option("unwind", cmdline.get_value("unwind"));
215 
216  if(cmdline.isset("depth"))
217  options.set_option("depth", cmdline.get_value("depth"));
218 
219  if(cmdline.isset("debug-level"))
220  options.set_option("debug-level", cmdline.get_value("debug-level"));
221 
222  if(cmdline.isset("unwindset"))
223  options.set_option("unwindset", cmdline.get_value("unwindset"));
224 
225  // constant propagation
226  if(cmdline.isset("no-propagation"))
227  options.set_option("propagation", false);
228 
229  // transform self loops to assumptions
230  options.set_option(
231  "self-loops-to-assumptions",
232  !cmdline.isset("no-self-loops-to-assumptions"));
233 
234  // all checks supported by goto_check
236 
237  // unwind loops in java enum static initialization
238  if(cmdline.isset("java-unwind-enum-static"))
239  options.set_option("java-unwind-enum-static", true);
240 
241  // check assertions
242  if(cmdline.isset("no-assertions"))
243  options.set_option("assertions", false);
244 
245  // use assumptions
246  if(cmdline.isset("no-assumptions"))
247  options.set_option("assumptions", false);
248 
249  // generate unwinding assertions
250  if(cmdline.isset("unwinding-assertions"))
251  options.set_option("unwinding-assertions", true);
252 
253  // generate unwinding assumptions otherwise
254  options.set_option(
255  "partial-loops",
256  cmdline.isset("partial-loops"));
257 
258  if(options.get_bool_option("partial-loops") &&
259  options.get_bool_option("unwinding-assertions"))
260  {
261  log.error() << "--partial-loops and --unwinding-assertions "
262  << "must not be given together" << messaget::eom;
263  exit(1); // should contemplate EX_USAGE from sysexits.h
264  }
265 
266  // remove unused equations
267  options.set_option(
268  "slice-formula",
269  cmdline.isset("slice-formula"));
270 
271  // simplify if conditions and branches
272  if(cmdline.isset("no-simplify-if"))
273  options.set_option("simplify-if", false);
274 
275  if(cmdline.isset("arrays-uf-always"))
276  options.set_option("arrays-uf", "always");
277  else if(cmdline.isset("arrays-uf-never"))
278  options.set_option("arrays-uf", "never");
279 
280  if(cmdline.isset("dimacs"))
281  options.set_option("dimacs", true);
282 
283  if(cmdline.isset("refine-arrays"))
284  {
285  options.set_option("refine", true);
286  options.set_option("refine-arrays", true);
287  }
288 
289  if(cmdline.isset("refine-arithmetic"))
290  {
291  options.set_option("refine", true);
292  options.set_option("refine-arithmetic", true);
293  }
294 
295  if(cmdline.isset("refine"))
296  {
297  options.set_option("refine", true);
298  options.set_option("refine-arrays", true);
299  options.set_option("refine-arithmetic", true);
300  }
301 
302  if(cmdline.isset("no-refine-strings"))
303  options.set_option("refine-strings", false);
304 
305  if(cmdline.isset("string-printable") && cmdline.isset("no-refine-strings"))
306  {
308  "cannot use --string-printable with --no-refine-strings",
309  "--string-printable");
310  }
311 
312  if(cmdline.isset("string-input-value") && cmdline.isset("no-refine-strings"))
313  {
315  "cannot use --string-input-value with --no-refine-strings",
316  "--string-input-value");
317  }
318 
319  if(
320  cmdline.isset("no-refine-strings") &&
321  cmdline.isset("max-nondet-string-length"))
322  {
324  "cannot use --max-nondet-string-length with --no-refine-strings",
325  "--max-nondet-string-length");
326  }
327 
328  if(cmdline.isset("max-node-refinement"))
329  options.set_option(
330  "max-node-refinement",
331  cmdline.get_value("max-node-refinement"));
332 
333  // SMT Options
334 
335  if(cmdline.isset("smt1"))
336  {
337  log.error() << "--smt1 is no longer supported" << messaget::eom;
339  }
340 
341  if(cmdline.isset("smt2"))
342  options.set_option("smt2", true);
343 
344  if(cmdline.isset("fpa"))
345  options.set_option("fpa", true);
346 
347  bool solver_set=false;
348 
349  if(cmdline.isset("boolector"))
350  {
351  options.set_option("boolector", true), solver_set=true;
352  options.set_option("smt2", true);
353  }
354 
355  if(cmdline.isset("mathsat"))
356  {
357  options.set_option("mathsat", true), solver_set=true;
358  options.set_option("smt2", true);
359  }
360 
361  if(cmdline.isset("cvc4"))
362  {
363  options.set_option("cvc4", true), solver_set=true;
364  options.set_option("smt2", true);
365  }
366 
367  if(cmdline.isset("yices"))
368  {
369  options.set_option("yices", true), solver_set=true;
370  options.set_option("smt2", true);
371  }
372 
373  if(cmdline.isset("z3"))
374  {
375  options.set_option("z3", true), solver_set=true;
376  options.set_option("smt2", true);
377  }
378 
379  if(cmdline.isset("smt2") && !solver_set)
380  {
381  if(cmdline.isset("outfile"))
382  {
383  // outfile and no solver should give standard compliant SMT-LIB
384  options.set_option("generic", true);
385  }
386  else
387  {
388  // the default smt2 solver
389  options.set_option("z3", true);
390  }
391  }
392 
393  if(cmdline.isset("beautify"))
394  options.set_option("beautify", true);
395 
396  if(cmdline.isset("no-sat-preprocessor"))
397  options.set_option("sat-preprocessor", false);
398 
399  options.set_option(
400  "pretty-names",
401  !cmdline.isset("no-pretty-names"));
402 
403  if(cmdline.isset("outfile"))
404  options.set_option("outfile", cmdline.get_value("outfile"));
405 
406  if(cmdline.isset("graphml-witness"))
407  {
408  options.set_option("graphml-witness", cmdline.get_value("graphml-witness"));
409  options.set_option("stop-on-fail", true);
410  options.set_option("trace", true);
411  }
412 
413  if(cmdline.isset("symex-coverage-report"))
414  options.set_option(
415  "symex-coverage-report",
416  cmdline.get_value("symex-coverage-report"));
417 
418  if(cmdline.isset("validate-ssa-equation"))
419  {
420  options.set_option("validate-ssa-equation", true);
421  }
422 
423  if(cmdline.isset("validate-goto-model"))
424  {
425  options.set_option("validate-goto-model", true);
426  }
427 
428  options.set_option(
429  "symex-cache-dereferences", cmdline.isset("symex-cache-dereferences"));
430 
432 
433  if(cmdline.isset("no-lazy-methods"))
434  options.set_option("lazy-methods", false);
435 
436  if(cmdline.isset("symex-driven-lazy-loading"))
437  {
438  options.set_option("symex-driven-lazy-loading", true);
439  for(const char *opt :
440  { "nondet-static",
441  "full-slice",
442  "reachability-slice",
443  "reachability-slice-fb" })
444  {
445  if(cmdline.isset(opt))
446  {
447  throw std::string("Option ") + opt +
448  " can't be used with --symex-driven-lazy-loading";
449  }
450  }
451  }
452 
453  // The 'allow-pointer-unsoundness' option prevents symex from throwing an
454  // exception when it encounters pointers that are shared across threads.
455  // This is unsound but given that pointers are ubiquitous in java this check
456  // must be disabled in order to support the analysis of multithreaded java
457  // code.
458  if(cmdline.isset("java-threading"))
459  options.set_option("allow-pointer-unsoundness", true);
460 
461  if(cmdline.isset("show-goto-symex-steps"))
462  options.set_option("show-goto-symex-steps", true);
463 }
464 
467 {
468  if(cmdline.isset("version"))
469  {
470  std::cout << CBMC_VERSION << '\n';
471  return CPROVER_EXIT_SUCCESS;
472  }
473 
476 
477  //
478  // command line options
479  //
480 
481  optionst options;
482  get_command_line_options(options);
483 
484  //
485  // Print a banner
486  //
487  log.status() << "JBMC version " << CBMC_VERSION << " " << sizeof(void *) * 8
488  << "-bit " << config.this_architecture() << " "
490 
491  // output the options
492  switch(ui_message_handler.get_ui())
493  {
496  log.debug(), [&options](messaget::mstreamt &debug_stream) {
497  debug_stream << "\nOptions: \n";
498  options.output(debug_stream);
499  debug_stream << messaget::eom;
500  });
501  break;
503  {
504  json_objectt json_options{{"options", options.to_json()}};
505  log.debug() << json_options;
506  break;
507  }
509  log.debug() << options.to_xml();
510  break;
511  }
512 
515 
516  if(!((cmdline.isset("jar") && cmdline.args.empty()) ||
517  (cmdline.isset("gb") && cmdline.args.empty()) ||
518  (!cmdline.isset("jar") && !cmdline.isset("gb") &&
519  (cmdline.args.size() == 1))))
520  {
521  log.error() << "Please give exactly one class name, "
522  << "and/or use -jar jarfile or --gb goto-binary"
523  << messaget::eom;
525  }
526 
527  if((cmdline.args.size() == 1) && !cmdline.isset("show-parse-tree"))
528  {
529  std::string main_class = cmdline.args[0];
530  // `java` accepts slashes and dots as package separators
531  std::replace(main_class.begin(), main_class.end(), '/', '.');
532  config.java.main_class = main_class;
533  cmdline.args.pop_back();
534  }
535 
536  if(cmdline.isset("jar"))
537  {
538  cmdline.args.push_back(cmdline.get_value("jar"));
539  }
540 
541  if(cmdline.isset("gb"))
542  {
543  cmdline.args.push_back(cmdline.get_value("gb"));
544  }
545 
546  // Shows the parse tree of the main class
547  if(cmdline.isset("show-parse-tree"))
548  {
549  std::unique_ptr<languaget> language = get_language_from_mode(ID_java);
550  CHECK_RETURN(language != nullptr);
551  language->set_language_options(options);
553 
554  log.status() << "Parsing ..." << messaget::eom;
555 
556  if(static_cast<java_bytecode_languaget *>(language.get())->parse())
557  {
558  log.error() << "PARSING ERROR" << messaget::eom;
560  }
561 
562  language->show_parse(std::cout);
563  return CPROVER_EXIT_SUCCESS;
564  }
565 
566  object_factory_params.set(options);
567 
569  options.get_bool_option("java-assume-inputs-non-null");
570 
571  std::unique_ptr<abstract_goto_modelt> goto_model_ptr;
572  int get_goto_program_ret = get_goto_program(goto_model_ptr, options);
573  if(get_goto_program_ret != -1)
574  return get_goto_program_ret;
575 
576  if(
577  options.get_bool_option("program-only") ||
578  options.get_bool_option("show-vcc") ||
579  (options.get_bool_option("symex-driven-lazy-loading") &&
580  (cmdline.isset("show-symbol-table") || cmdline.isset("list-symbols") ||
581  cmdline.isset("show-goto-functions") ||
582  cmdline.isset("list-goto-functions") ||
583  cmdline.isset("show-properties") || cmdline.isset("show-loops"))))
584  {
585  if(options.get_bool_option("paths"))
586  {
588  options, ui_message_handler, *goto_model_ptr);
589  (void)verifier();
590  }
591  else
592  {
594  options, ui_message_handler, *goto_model_ptr);
595  (void)verifier();
596  }
597 
598  if(options.get_bool_option("symex-driven-lazy-loading"))
599  {
600  // We can only output these after goto-symex has run.
601  (void)show_loaded_symbols(*goto_model_ptr);
602  (void)show_loaded_functions(*goto_model_ptr);
603  }
604 
605  return CPROVER_EXIT_SUCCESS;
606  }
607 
608  if(
609  options.get_bool_option("dimacs") || !options.get_option("outfile").empty())
610  {
611  if(options.get_bool_option("paths"))
612  {
614  options, ui_message_handler, *goto_model_ptr);
615  (void)verifier();
616  }
617  else
618  {
620  options, ui_message_handler, *goto_model_ptr);
621  (void)verifier();
622  }
623 
624  return CPROVER_EXIT_SUCCESS;
625  }
626 
627  std::unique_ptr<goto_verifiert> verifier = nullptr;
628 
629  if(
630  options.get_bool_option("stop-on-fail") && options.get_bool_option("paths"))
631  {
632  verifier =
633  util_make_unique<stop_on_fail_verifiert<java_single_path_symex_checkert>>(
634  options, ui_message_handler, *goto_model_ptr);
635  }
636  else if(
637  options.get_bool_option("stop-on-fail") &&
638  !options.get_bool_option("paths"))
639  {
640  if(options.get_bool_option("localize-faults"))
641  {
642  verifier =
645  options, ui_message_handler, *goto_model_ptr);
646  }
647  else
648  {
649  verifier = util_make_unique<
651  options, ui_message_handler, *goto_model_ptr);
652  }
653  }
654  else if(
655  !options.get_bool_option("stop-on-fail") &&
656  options.get_bool_option("paths"))
657  {
660  options, ui_message_handler, *goto_model_ptr);
661  }
662  else if(
663  !options.get_bool_option("stop-on-fail") &&
664  !options.get_bool_option("paths"))
665  {
666  if(options.get_bool_option("localize-faults"))
667  {
668  verifier =
671  options, ui_message_handler, *goto_model_ptr);
672  }
673  else
674  {
677  options, ui_message_handler, *goto_model_ptr);
678  }
679  }
680  else
681  {
682  UNREACHABLE;
683  }
684 
685  const resultt result = (*verifier)();
686  verifier->report();
687  return result_to_exit_code(result);
688 }
689 
691  std::unique_ptr<abstract_goto_modelt> &goto_model_ptr,
692  const optionst &options)
693 {
694  if(options.is_set("context-include") || options.is_set("context-exclude"))
695  method_context = get_context(options);
696  lazy_goto_modelt lazy_goto_model =
698  lazy_goto_model.initialize(cmdline.args, options);
699 
701  util_make_unique<class_hierarchyt>(lazy_goto_model.symbol_table);
702 
703  // Show the class hierarchy
704  if(cmdline.isset("show-class-hierarchy"))
705  {
707  return CPROVER_EXIT_SUCCESS;
708  }
709 
710  // Add failed symbols for any symbol created prior to loading any
711  // particular function:
712  add_failed_symbols(lazy_goto_model.symbol_table);
713 
714  if(!options.get_bool_option("symex-driven-lazy-loading"))
715  {
716  log.status() << "Generating GOTO Program" << messaget::eom;
717  lazy_goto_model.load_all_functions();
718 
719  // show symbol table or list symbols
720  if(show_loaded_symbols(lazy_goto_model))
721  return CPROVER_EXIT_SUCCESS;
722 
723  // Move the model out of the local lazy_goto_model
724  // and into the caller's goto_model
726  std::move(lazy_goto_model));
727  if(goto_model_ptr == nullptr)
729 
730  goto_modelt &goto_model = dynamic_cast<goto_modelt &>(*goto_model_ptr);
731 
732  // if we added the ansi-c library models here this should also call
733  // add_malloc_may_fail_variable_initializations(goto_model);
734  // here
735 
736  if(cmdline.isset("validate-goto-model"))
737  {
738  goto_model.validate();
739  }
740 
741  if(show_loaded_functions(goto_model))
742  return CPROVER_EXIT_SUCCESS;
743 
744  if(cmdline.isset("property"))
745  ::set_properties(goto_model, cmdline.get_values("property"));
746  }
747  else
748  {
749  // The precise wording of this error matches goto-symex's complaint when no
750  // __CPROVER_start exists (if we just go ahead and run it anyway it will
751  // trip an invariant when it tries to load it)
753  {
754  log.error() << "the program has no entry point" << messaget::eom;
756  }
757 
758  if(cmdline.isset("validate-goto-model"))
759  {
760  lazy_goto_model.validate();
761  }
762 
763  goto_model_ptr =
764  util_make_unique<lazy_goto_modelt>(std::move(lazy_goto_model));
765  }
766 
768 
769  return -1; // no error, continue
770 }
771 
773  goto_model_functiont &function,
774  const abstract_goto_modelt &model,
775  const optionst &options)
776 {
777  journalling_symbol_tablet &symbol_table = function.get_symbol_table();
778  namespacet ns(symbol_table);
779  goto_functionst::goto_functiont &goto_function = function.get_goto_function();
780 
781  bool using_symex_driven_loading =
782  options.get_bool_option("symex-driven-lazy-loading");
783 
784  // Removal of RTTI inspection:
786  function.get_function_id(),
787  goto_function,
788  symbol_table,
791  // Java virtual functions -> explicit dispatch tables:
793 
794  auto function_is_stub = [&symbol_table, &model](const irep_idt &id) {
795  return symbol_table.lookup_ref(id).value.is_nil() &&
796  !model.can_produce_function(id);
797  };
798 
799  remove_returns(function, function_is_stub);
800 
801  replace_java_nondet(function);
802 
803  // Similar removal of java nondet statements:
805 
806  if(using_symex_driven_loading)
807  {
808  // remove exceptions
809  // If using symex-driven function loading we need to do this now so that
810  // symex doesn't have to cope with exception-handling constructs; however
811  // the results are slightly worse than running it in whole-program mode
812  // (e.g. dead catch sites will be retained)
814  function.get_function_id(),
815  goto_function.body,
816  symbol_table,
817  *class_hierarchy.get(),
819  }
820 
821  // add generic checks
822  goto_check(
823  function.get_function_id(), function.get_goto_function(), ns, options);
824 
825  // Replace Java new side effects
827  function.get_function_id(),
828  goto_function,
829  symbol_table,
831 
832  // checks don't know about adjusted float expressions
833  adjust_float_expressions(goto_function, ns);
834 
835  // add failed symbols for anything created relating to this particular
836  // function (note this means subsequent passes mustn't create more!):
838  symbol_table.get_inserted();
839  for(const irep_idt &new_symbol_name : new_symbols)
840  {
842  symbol_table.lookup_ref(new_symbol_name), symbol_table);
843  }
844 
845  // If using symex-driven function loading we must label the assertions
846  // now so symex sees its targets; otherwise we leave this until
847  // process_goto_functions, as we haven't run remove_exceptions yet, and that
848  // pass alters the CFG.
849  if(using_symex_driven_loading)
850  {
851  // label the assertions
852  label_properties(goto_function.body);
853 
854  goto_function.body.update();
855  function.compute_location_numbers();
856  goto_function.body.compute_loop_numbers();
857  }
858 }
859 
861  const abstract_goto_modelt &goto_model)
862 {
863  if(cmdline.isset("show-symbol-table"))
864  {
866  return true;
867  }
868  else if(cmdline.isset("list-symbols"))
869  {
871  return true;
872  }
873 
874  return false;
875 }
876 
878  const abstract_goto_modelt &goto_model)
879 {
880  if(cmdline.isset("show-loops"))
881  {
883  return true;
884  }
885 
886  if(
887  cmdline.isset("show-goto-functions") ||
888  cmdline.isset("list-goto-functions"))
889  {
890  namespacet ns(goto_model.get_symbol_table());
892  ns,
894  goto_model.get_goto_functions(),
895  cmdline.isset("list-goto-functions"));
896  return true;
897  }
898 
899  if(cmdline.isset("show-properties"))
900  {
901  namespacet ns(goto_model.get_symbol_table());
903  return true;
904  }
905 
906  return false;
907 }
908 
910  goto_modelt &goto_model,
911  const optionst &options)
912 {
913  log.status() << "Running GOTO functions transformation passes"
914  << messaget::eom;
915 
916  bool using_symex_driven_loading =
917  options.get_bool_option("symex-driven-lazy-loading");
918 
919  // When using symex-driven lazy loading, *all* relevant processing is done
920  // during process_goto_function, so we have nothing to do here.
921  if(using_symex_driven_loading)
922  return false;
923 
924  // remove catch and throw
926 
927  // instrument library preconditions
928  instrument_preconditions(goto_model);
929 
930  // ignore default/user-specified initialization
931  // of variables with static lifetime
932  if(cmdline.isset("nondet-static"))
933  {
934  log.status() << "Adding nondeterministic initialization "
935  "of static/global variables"
936  << messaget::eom;
937  nondet_static(goto_model);
938  }
939 
940  // recalculate numbers, etc.
941  goto_model.goto_functions.update();
942 
943  if(cmdline.isset("drop-unused-functions"))
944  {
945  // Entry point will have been set before and function pointers removed
946  log.status() << "Removing unused functions" << messaget::eom;
948  }
949 
950  // remove skips such that trivial GOTOs are deleted
951  remove_skip(goto_model);
952 
953  // label the assertions
954  // This must be done after adding assertions and
955  // before using the argument of the "property" option.
956  // Do not re-label after using the property slicer because
957  // this would cause the property identifiers to change.
958  label_properties(goto_model);
959 
960  // reachability slice?
961  if(cmdline.isset("reachability-slice-fb"))
962  {
963  if(cmdline.isset("reachability-slice"))
964  {
965  log.error() << "--reachability-slice and --reachability-slice-fb "
966  << "must not be given together" << messaget::eom;
967  return true;
968  }
969 
970  log.status() << "Performing a forwards-backwards reachability slice"
971  << messaget::eom;
972  if(cmdline.isset("property"))
973  reachability_slicer(goto_model, cmdline.get_values("property"), true);
974  else
975  reachability_slicer(goto_model, true);
976  }
977 
978  if(cmdline.isset("reachability-slice"))
979  {
980  log.status() << "Performing a reachability slice" << messaget::eom;
981  if(cmdline.isset("property"))
982  reachability_slicer(goto_model, cmdline.get_values("property"));
983  else
984  reachability_slicer(goto_model);
985  }
986 
987  // full slice?
988  if(cmdline.isset("full-slice"))
989  {
990  log.status() << "Performing a full slice" << messaget::eom;
991  if(cmdline.isset("property"))
992  property_slicer(goto_model, cmdline.get_values("property"));
993  else
994  full_slicer(goto_model);
995  }
996 
997  // remove any skips introduced
998  remove_skip(goto_model);
999 
1000  return false;
1001 }
1002 
1004 {
1005  static const irep_idt initialize_id = INITIALIZE_FUNCTION;
1006 
1007  return name != goto_functionst::entry_point() && name != initialize_id;
1008 }
1009 
1011  const irep_idt &function_name,
1012  symbol_table_baset &symbol_table,
1013  goto_functiont &function,
1014  bool body_available)
1015 {
1016  // Provide a simple stub implementation for any function we don't have a
1017  // bytecode implementation for:
1018 
1019  if(
1020  body_available &&
1021  (!method_context || (*method_context)(id2string(function_name))))
1022  return false;
1023 
1024  if(!can_generate_function_body(function_name))
1025  return false;
1026 
1027  if(symbol_table.lookup_ref(function_name).mode == ID_java)
1028  {
1030  function_name,
1031  symbol_table,
1035 
1036  goto_convert_functionst converter(symbol_table, ui_message_handler);
1037  converter.convert_function(function_name, function);
1038 
1039  return true;
1040  }
1041  else
1042  {
1043  return false;
1044  }
1045 }
1046 
1049 {
1050  // clang-format off
1051  std::cout << '\n' << banner_string("JBMC", CBMC_VERSION) << '\n'
1052  << align_center_with_border("Copyright (C) 2001-2018") << '\n'
1053  << align_center_with_border("Daniel Kroening, Edmund Clarke") << '\n' // NOLINT(*)
1054  << align_center_with_border("Carnegie Mellon University, Computer Science Department") << '\n' // NOLINT(*)
1055  << align_center_with_border("kroening@kroening.com") << '\n'
1056  << "\n"
1057  "Usage: Purpose:\n"
1058  "\n"
1059  " jbmc [-?] [-h] [--help] show help\n"
1060  " jbmc\n"
1062  " jbmc\n"
1064  " jbmc\n"
1066  " jbmc\n"
1068  "\n"
1071  "\n"
1072  "Analysis options:\n"
1074  " --symex-coverage-report f generate a Cobertura XML coverage report in f\n" // NOLINT(*)
1075  " --property id only check one specific property\n"
1076  " --trace give a counterexample trace for failed properties\n" //NOLINT(*)
1077  " --stop-on-fail stop analysis once a failed property is detected\n" // NOLINT(*)
1078  " (implies --trace)\n"
1080  "\n"
1081  "Program representations:\n"
1082  " --show-parse-tree show parse tree\n"
1083  " --show-symbol-table show loaded symbol table\n"
1084  " --list-symbols list symbols with type information\n"
1086  " --drop-unused-functions drop functions trivially unreachable\n"
1087  " from main function\n"
1089  "\n"
1090  "Program instrumentation options:\n"
1091  " --no-assertions ignore user assertions\n"
1092  " --no-assumptions ignore user assumptions\n"
1093  " --error-label label check that label is unreachable\n"
1094  " --mm MM memory consistency model for concurrent programs\n" // NOLINT(*)
1096  " --full-slice run full slicer (experimental)\n" // NOLINT(*)
1097  "\n"
1098  "Java Bytecode frontend options:\n"
1100  // This one is handled by jbmc_parse_options not by the Java frontend,
1101  // hence its presence here:
1102  " --java-threading enable java multi-threading support (experimental)\n" // NOLINT(*)
1103  " --java-unwind-enum-static unwind loops in static initialization of enums\n" // NOLINT(*)
1104  // Currently only supported in the JBMC frontend:
1105  " --symex-driven-lazy-loading only load functions when first entered by symbolic\n" // NOLINT(*)
1106  " execution. Note that --show-symbol-table,\n"
1107  " --show-goto-functions/properties output\n"
1108  " will be restricted to loaded methods in this case,\n" // NOLINT(*)
1109  " and only output after the symex phase.\n"
1110  "\n"
1111  "Semantic transformations:\n"
1112  // NOLINTNEXTLINE(whitespace/line_length)
1113  " --nondet-static add nondeterministic initialization of variables with static lifetime\n"
1114  "\n"
1115  "BMC options:\n"
1116  HELP_BMC
1117  "\n"
1118  "Backend options:\n"
1119  " --object-bits n number of bits used for object addresses\n"
1120  " --dimacs generate CNF in DIMACS format\n"
1121  " --beautify beautify the counterexample (greedy heuristic)\n" // NOLINT(*)
1122  " --localize-faults localize faults (experimental)\n"
1123  " --smt1 use default SMT1 solver (obsolete)\n"
1124  " --smt2 use default SMT2 solver (Z3)\n"
1125  " --boolector use Boolector\n"
1126  " --mathsat use MathSAT\n"
1127  " --cvc4 use CVC4\n"
1128  " --yices use Yices\n"
1129  " --z3 use Z3\n"
1130  " --refine use refinement procedure (experimental)\n"
1132  " --outfile filename output formula to given file\n"
1133  " --arrays-uf-never never turn arrays into uninterpreted functions\n" // NOLINT(*)
1134  " --arrays-uf-always always turn arrays into uninterpreted functions\n" // NOLINT(*)
1135  "\n"
1136  "Other options:\n"
1137  " --version show version and exit\n"
1142  HELP_FLUSH
1143  " --verbosity # verbosity level\n"
1145  "\n";
1146  // clang-format on
1147 }
cmdlinet::args
argst args
Definition: cmdline.h:143
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
convert_java_nondet.h
Convert side_effect_expr_nondett expressions using java_object_factory.
abstract_goto_modelt::can_produce_function
virtual bool can_produce_function(const irep_idt &id) const =0
Determines if this model can produce a body for the given function.
symbol_table_baset::has_symbol
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
Definition: symbol_table_base.h:87
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
HELP_REACHABILITY_SLICER
#define HELP_REACHABILITY_SLICER
Definition: reachability_slicer.h:43
HELP_BMC
#define HELP_BMC
Definition: bmc_util.h:203
HELP_SHOW_GOTO_FUNCTIONS
#define HELP_SHOW_GOTO_FUNCTIONS
Definition: show_goto_functions.h:26
lazy_goto_modelt::symbol_table
symbol_tablet & symbol_table
Reference to symbol_table in the internal goto_model.
Definition: lazy_goto_model.h:265
languaget::show_parse
virtual void show_parse(std::ostream &out)=0
configt::object_bits_info
std::string object_bits_info()
Definition: config.cpp:1314
symbol_table_baset::lookup_ref
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Definition: symbol_table_base.h:104
configt::javat::main_class
irep_idt main_class
Definition: config.h:248
PARSE_OPTIONS_GOTO_CHECK
#define PARSE_OPTIONS_GOTO_CHECK(cmdline, options)
Definition: goto_check.h:70
optionst::output
void output(std::ostream &out) const
Outputs the options to out
Definition: options.cpp:121
lazy_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: lazy_goto_model.h:252
abstract_goto_modelt::get_symbol_table
virtual const symbol_tablet & get_symbol_table() const =0
Accessor to get the symbol table.
jbmc_parse_optionst::get_command_line_options
void get_command_line_options(optionst &)
Definition: jbmc_parse_options.cpp:122
HELP_GOTO_TRACE
#define HELP_GOTO_TRACE
Definition: goto_trace.h:279
parse_options_baset::ui_message_handler
ui_message_handlert ui_message_handler
Definition: parse_options.h:42
parse_options_baset
Definition: parse_options.h:20
java_bytecode_language.h
JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP
#define JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP
Definition: java_bytecode_language.h:55
parse_java_language_options
void parse_java_language_options(const cmdlinet &cmd, optionst &options)
Parse options that are java bytecode specific.
Definition: java_bytecode_language.cpp:56
resultt
resultt
The result of goto verifying.
Definition: properties.h:44
cmdlinet::isset
virtual bool isset(char option) const
Definition: cmdline.cpp:29
stop_on_fail_verifiert
Stops when the first failing property is found.
Definition: stop_on_fail_verifier.h:23
ui_message_handlert::uit::XML_UI
@ XML_UI
jbmc_parse_optionst::process_goto_functions
bool process_goto_functions(goto_modelt &goto_model, const optionst &options)
Definition: jbmc_parse_options.cpp:909
goto_inline.h
Function Inlining.
optionst
Definition: options.h:23
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
show_class_hierarchy
void show_class_hierarchy(const class_hierarchyt &hierarchy, ui_message_handlert &message_handler, bool children_only)
Output the class hierarchy.
Definition: class_hierarchy.cpp:261
all_properties_verifiert
Definition: all_properties_verifier.h:23
optionst::get_option
const std::string get_option(const std::string &option) const
Definition: options.cpp:67
messaget::M_STATISTICS
@ M_STATISTICS
Definition: message.h:171
messaget::status
mstreamt & status() const
Definition: message.h:414
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
lazy_goto_modelt::process_whole_model_and_freeze
static std::unique_ptr< goto_modelt > process_whole_model_and_freeze(lazy_goto_modelt &&model)
The model returned here has access to the functions we've already loaded but is frozen in the sense t...
Definition: lazy_goto_model.h:203
java_enum_static_init_unwind_handler.h
Unwind loops in static initializers.
jbmc_parse_optionst::process_goto_function
void process_goto_function(goto_model_functiont &function, const abstract_goto_modelt &, const optionst &)
Definition: jbmc_parse_options.cpp:772
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:86
goto_convert_functionst::convert_function
void convert_function(const irep_idt &identifier, goto_functionst::goto_functiont &result)
Definition: goto_convert_functions.cpp:145
replace
void replace(const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)
Definition: string_constraint.cpp:67
new_java_bytecode_language
std::unique_ptr< languaget > new_java_bytecode_language()
Definition: java_bytecode_language.cpp:1524
get_language_from_mode
std::unique_ptr< languaget > get_language_from_mode(const irep_idt &mode)
Get the language corresponding to the given mode.
Definition: mode.cpp:50
invariant.h
remove_virtual_functions.h
Functions for replacing virtual function call with a static function calls in functions,...
HELP_SHOW_CLASS_HIERARCHY
#define HELP_SHOW_CLASS_HIERARCHY
Definition: class_hierarchy.h:29
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:370
remove_virtual_functions
void remove_virtual_functions(symbol_table_baset &symbol_table, goto_functionst &goto_functions)
Remove virtual function calls from all functions in the specified list and replace them with their mo...
Definition: remove_virtual_functions.cpp:725
goto_modelt
Definition: goto_model.h:26
show_goto_functions.h
Show the goto functions.
mode.h
show_loop_ids
void show_loop_ids(ui_message_handlert::uit ui, const goto_modelt &goto_model)
Definition: loop_ids.cpp:19
all_properties_verifier.h
Goto Verifier for Verifying all Properties.
goto_check
void goto_check(const irep_idt &function_identifier, goto_functionst::goto_functiont &goto_function, const namespacet &ns, const optionst &options)
Definition: goto_check.cpp:2338
optionst::set_option
void set_option(const std::string &option, const bool value)
Definition: options.cpp:28
HELP_JAVA_GOTO_BINARY
#define HELP_JAVA_GOTO_BINARY
Definition: java_bytecode_language.h:173
messaget::eom
static eomt eom
Definition: message.h:297
jbmc_parse_optionst::generate_function_body
bool generate_function_body(const irep_idt &function_name, symbol_table_baset &symbol_table, goto_functiont &function, bool body_available)
Definition: jbmc_parse_options.cpp:1010
jbmc_parse_optionst::object_factory_params
java_object_factory_parameterst object_factory_params
Definition: jbmc_parse_options.h:128
JBMC_OPTIONS
#define JBMC_OPTIONS
Definition: jbmc_parse_options.h:44
show_symbol_table
void show_symbol_table(const symbol_tablet &symbol_table, ui_message_handlert &ui)
Definition: show_symbol_table.cpp:268
version.h
remove_unused_functions
void remove_unused_functions(goto_modelt &goto_model, message_handlert &message_handler)
Definition: remove_unused_functions.cpp:18
nondet_static.h
Nondeterministically initializes global scope variables, except for constants (such as string literal...
lazy_goto_model.h
Author: Diffblue Ltd.
xml.h
simple_method_stubbing.h
Java simple opaque stub generation.
stop_on_fail_verifier_with_fault_localization.h
Goto Verifier for stopping at the first failing property and localizing the fault.
label_properties
void label_properties(goto_modelt &goto_model)
Definition: set_properties.cpp:43
path_storage.h
Storage of symbolic execution paths to resume.
jbmc_parse_optionst::stub_objects_are_not_null
bool stub_objects_are_not_null
Definition: jbmc_parse_options.h:129
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
java_object_factory_parameterst::set
void set(const optionst &)
Assigns the parameters from given options.
Definition: java_object_factory_parameters.cpp:17
HELP_JAVA_JAR
#define HELP_JAVA_JAR
Definition: java_bytecode_language.h:161
remove_instanceof
void remove_instanceof(const irep_idt &function_identifier, goto_programt::targett target, goto_programt &goto_program, symbol_table_baset &symbol_table, const class_hierarchyt &class_hierarchy, message_handlert &message_handler)
Replace an instanceof in the expression or guard of the passed instruction of the given function body...
Definition: remove_instanceof.cpp:300
HELP_JAVA_TRACE_VALIDATION
#define HELP_JAVA_TRACE_VALIDATION
Definition: java_trace_validation.h:29
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
json_objectt
Definition: json.h:300
HELP_JSON_INTERFACE
#define HELP_JSON_INTERFACE
Definition: json_interface.h:45
ui_message_handlert::get_ui
virtual uit get_ui() const
Definition: ui_message.h:31
parse_options_baset::usage_error
virtual void usage_error()
Definition: parse_options.cpp:47
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
util_make_unique
std::unique_ptr< T > util_make_unique(Ts &&... ts)
Definition: make_unique.h:19
set_properties.h
Set the properties to check.
lazy_goto_modelt::from_handler_object
static lazy_goto_modelt from_handler_object(THandler &handler, const optionst &options, message_handlert &message_handler)
Create a lazy_goto_modelt from a object that defines function/module pass handlers.
Definition: lazy_goto_model.h:153
optionst::to_json
json_objectt to_json() const
Returns the options as JSON key value pairs.
Definition: options.cpp:93
convert_nondet
void convert_nondet(const irep_idt &function_identifier, goto_programt &goto_program, symbol_table_baset &symbol_table, message_handlert &message_handler, const java_object_factory_parameterst &user_object_factory_parameters, const irep_idt &mode)
For each instruction in the goto program, checks if it is an assignment from nondet and replaces it w...
Definition: convert_java_nondet.cpp:167
full_slicer
void full_slicer(goto_functionst &goto_functions, const namespacet &ns, const slicing_criteriont &criterion)
Definition: full_slicer.cpp:347
jbmc_parse_optionst::doit
virtual int doit() override
invoke main modules
Definition: jbmc_parse_options.cpp:466
CBMC_VERSION
const char * CBMC_VERSION
parse_java_object_factory_options
void parse_java_object_factory_options(const cmdlinet &cmdline, optionst &options)
Parse the java object factory parameters from a given command line.
Definition: java_object_factory_parameters.cpp:44
symbolt::mode
irep_idt mode
Language mode.
Definition: symbol.h:49
show_symbol_table_brief
void show_symbol_table_brief(const symbol_tablet &symbol_table, ui_message_handlert &ui)
Definition: show_symbol_table.cpp:295
make_unique.h
messaget::error
mstreamt & error() const
Definition: message.h:399
all_properties_verifier_with_trace_storage.h
Goto verifier for verifying all properties that stores traces.
jbmc_parse_optionst::can_generate_function_body
bool can_generate_function_body(const irep_idt &name)
Definition: jbmc_parse_options.cpp:1003
HELP_STRING_REFINEMENT
#define HELP_STRING_REFINEMENT
Definition: string_refinement.h:43
banner_string
std::string banner_string(const std::string &front_end, const std::string &version)
Definition: parse_options.cpp:163
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
ui_message_handlert::uit::JSON_UI
@ JSON_UI
lazy_goto_modelt
A GOTO model that produces function bodies on demand.
Definition: lazy_goto_model.h:43
remove_exceptions
void remove_exceptions(symbol_table_baset &symbol_table, goto_functionst &goto_functions, const class_hierarchyt &class_hierarchy, message_handlert &message_handler)
removes throws/CATCH-POP/CATCH-PUSH
Definition: remove_exceptions.cpp:696
instrument_preconditions
void instrument_preconditions(const goto_modelt &goto_model, goto_programt &goto_program)
Definition: instrument_preconditions.cpp:90
jbmc_parse_optionst::show_loaded_symbols
bool show_loaded_symbols(const abstract_goto_modelt &goto_model)
Definition: jbmc_parse_options.cpp:860
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
symbol_table_baset
The symbol table base class interface.
Definition: symbol_table_base.h:22
property_slicer
void property_slicer(goto_functionst &goto_functions, const namespacet &ns, const std::list< std::string > &properties)
Definition: full_slicer.cpp:370
goto_convert_functionst
Definition: goto_convert_functions.h:40
show_properties.h
Show the properties.
java_single_path_symex_checker.h
Goto Checker using Single Path Symbolic Execution for Java.
get_context
prefix_filtert get_context(const optionst &options)
Definition: java_bytecode_language.cpp:115
jbmc_parse_optionst::class_hierarchy
std::unique_ptr< class_hierarchyt > class_hierarchy
Definition: jbmc_parse_options.h:131
INITIALIZE_FUNCTION
#define INITIALIZE_FUNCTION
Definition: static_lifetime_init.h:23
cmdlinet::get_value
std::string get_value(char option) const
Definition: cmdline.cpp:47
show_symbol_table.h
Show the symbol table.
language.h
Abstract interface to support a programming language.
messaget::set_message_handler
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:179
journalling_symbol_tablet::changesett
std::unordered_set< irep_idt > changesett
Definition: journalling_symbol_table.h:38
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
HELP_JAVA_CLASS_NAME
#define HELP_JAVA_CLASS_NAME
Definition: java_bytecode_language.h:151
configt::this_operating_system
static irep_idt this_operating_system()
Definition: config.cpp:1425
java_bytecode_languaget::parse
virtual bool parse()
We set the main class (i.e. class to start the class loading analysis, see java_class_loadert) when w...
Definition: java_bytecode_language.cpp:368
xml_interface
void xml_interface(cmdlinet &cmdline, message_handlert &message_handler)
Parse XML-formatted commandline options from stdin.
Definition: xml_interface.cpp:47
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
irept::is_nil
bool is_nil() const
Definition: irep.h:387
json_interface
void json_interface(cmdlinet &cmdline, message_handlert &message_handler)
Parses the JSON-formatted command line from stdin.
Definition: json_interface.cpp:88
goto_functiont
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
Definition: goto_function.h:27
lazy_goto_modelt::initialize
void initialize(const std::vector< std::string > &files, const optionst &options)
Performs initial symbol table and language_filest initialization from a given commandline and parsed ...
Definition: lazy_goto_model.cpp:111
java_single_path_symex_checkert
Definition: java_single_path_symex_checker.h:24
remove_java_new
void remove_java_new(const irep_idt &function_identifier, goto_programt::targett target, goto_programt &goto_program, symbol_table_baset &symbol_table, message_handlert &message_handler)
Replace every java_new or java_new_array by a malloc side-effect and zero initialization.
Definition: remove_java_new.cpp:436
all_properties_verifier_with_fault_localization.h
Goto verifier for verifying all properties that stores traces and localizes faults.
CPROVER_EXIT_INCORRECT_TASK
#define CPROVER_EXIT_INCORRECT_TASK
The command line is correctly structured but cannot be carried out due to missing files,...
Definition: exit_codes.h:49
full_slicer.h
Slicing.
HELP_JAVA_METHOD_NAME
#define HELP_JAVA_METHOD_NAME
Definition: java_bytecode_language.h:146
goto_verifiert::report
virtual void report()=0
Report results.
remove_returns.h
Replace function returns by assignments to global variables.
remove_exceptions.h
Remove function exceptional returns.
remove_unused_functions.h
Unused function removal.
config
configt config
Definition: config.cpp:24
remove_instanceof.h
Remove Instance-of Operators.
goto_functionst::goto_functiont
::goto_functiont goto_functiont
Definition: goto_functions.h:25
parse_options_baset::log
messaget log
Definition: parse_options.h:43
configt::this_architecture
static irep_idt this_architecture()
Definition: config.cpp:1325
jbmc_parse_optionst::help
virtual void help() override
display command line help
Definition: jbmc_parse_options.cpp:1048
abstract_goto_modelt::get_goto_functions
virtual const goto_functionst & get_goto_functions() const =0
Accessor to get a raw goto_functionst.
symbolt::value
exprt value
Initial value of symbol.
Definition: symbol.h:34
java_generate_simple_method_stub
void java_generate_simple_method_stub(const irep_idt &function_name, symbol_table_baset &symbol_table, bool assume_non_null, const java_object_factory_parameterst &object_factory_parameters, message_handlert &message_handler)
Definition: simple_method_stubbing.cpp:272
result_to_exit_code
int result_to_exit_code(resultt result)
Definition: properties.cpp:140
register_language
void register_language(language_factoryt factory)
Register a language Note: registering a language is required for using the functions in language_util...
Definition: mode.cpp:38
jbmc_parse_options.h
JBMC Command Line Option Processing.
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
ansi_c_language.h
ui_message_handlert::uit::PLAIN
@ PLAIN
stop_on_fail_verifier.h
Goto Verifier for stopping at the first failing property.
configt::set
bool set(const cmdlinet &cmdline)
Definition: config.cpp:797
java_multi_path_symex_checkert
Definition: java_multi_path_symex_checker.h:23
HELP_JAVA_CLASSPATH
#define HELP_JAVA_CLASSPATH
Definition: java_bytecode_language.h:136
exit_codes.h
Document and give macros for the exit codes of CPROVER binaries.
jbmc_parse_optionst::get_goto_program
int get_goto_program(std::unique_ptr< abstract_goto_modelt > &goto_model, const optionst &)
Definition: jbmc_parse_options.cpp:690
optionst::get_bool_option
bool get_bool_option(const std::string &option) const
Definition: options.cpp:44
add_failed_symbol_if_needed
void add_failed_symbol_if_needed(const symbolt &symbol, symbol_table_baset &symbol_table)
Create a failed-dereference symbol for the given base symbol if it is pointer-typed,...
Definition: add_failed_symbols.cpp:61
remove_returns
void remove_returns(symbol_table_baset &symbol_table, goto_functionst &goto_functions)
removes returns
Definition: remove_returns.cpp:257
messaget::conditional_output
void conditional_output(mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) const
Generate output to message_stream using output_generator if the configured verbosity is at least as h...
Definition: message.cpp:138
new_ansi_c_language
std::unique_ptr< languaget > new_ansi_c_language()
Definition: ansi_c_language.cpp:143
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
goto_functionst::update
void update()
Definition: goto_functions.h:81
configt::java
struct configt::javat java
unicode.h
show_path_strategies
std::string show_path_strategies()
suitable for displaying as a front-end help message
Definition: path_storage.cpp:110
config.h
replace_java_nondet
static void replace_java_nondet(goto_programt &goto_program)
Checks each instruction in the goto program to see whether it is a method returning nondet.
Definition: replace_java_nondet.cpp:313
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
loop_ids.h
Loop IDs.
reachability_slicer.h
Slicing.
messaget::mstreamt
Definition: message.h:224
jbmc_parse_optionst::set_default_options
static void set_default_options(optionst &)
Set the options that have default values.
Definition: jbmc_parse_options.cpp:102
PARSE_OPTIONS_GOTO_TRACE
#define PARSE_OPTIONS_GOTO_TRACE(cmdline, options)
Definition: goto_trace.h:287
abstract_goto_modelt
Abstract interface to eager or lazy GOTO models.
Definition: abstract_goto_model.h:21
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:79
remove_java_new.h
Remove Java New Operators.
java_multi_path_symex_checker.h
Goto Checker using Bounded Model Checking for Java.
lazy_goto_modelt::load_all_functions
void load_all_functions() const
Eagerly loads all functions from the symbol table.
Definition: lazy_goto_model.cpp:269
messaget::debug
mstreamt & debug() const
Definition: message.h:429
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
optionst::to_xml
xmlt to_xml() const
Returns the options in XML format.
Definition: options.cpp:104
add_failed_symbols.h
Pointer Dereferencing.
goto_functionst::entry_point
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
Definition: goto_functions.h:90
journalling_symbol_tablet::get_inserted
const changesett & get_inserted() const
Definition: journalling_symbol_table.h:146
CPROVER_EXIT_INTERNAL_ERROR
#define CPROVER_EXIT_INTERNAL_ERROR
An error has been encountered during processing the requested analysis.
Definition: exit_codes.h:45
jbmc_parse_optionst::jbmc_parse_optionst
jbmc_parse_optionst(int argc, const char **argv)
Definition: jbmc_parse_options.cpp:77
goto_convert_functions.h
Goto Programs with Functions.
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
static_lifetime_init.h
CPROVER_EXIT_SUCCESS
#define CPROVER_EXIT_SUCCESS
Success indicates the required analysis has been performed without error.
Definition: exit_codes.h:16
messaget::eval_verbosity
static unsigned eval_verbosity(const std::string &user_input, const message_levelt default_verbosity, message_handlert &dest)
Parse a (user-)provided string as a verbosity level and set it as the verbosity of dest.
Definition: message.cpp:104
java_single_path_symex_only_checker.h
Goto Checker using Single Path Symbolic Execution for Java.
remove_skip.h
Program Transformation.
java_bytecode_languaget
Definition: java_bytecode_language.h:275
adjust_float_expressions.h
Symbolic Execution.
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
invalid_command_line_argument_exceptiont
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
Definition: exception_utils.h:38
cmdlinet::get_values
const std::list< std::string > & get_values(const std::string &option) const
Definition: cmdline.cpp:108
java_multi_path_symex_only_checker.h
Goto Checker using Bounded Model Checking for Java.
parse_options_baset::cmdline
cmdlinet cmdline
Definition: parse_options.h:28
jbmc_parse_optionst::show_loaded_functions
bool show_loaded_functions(const abstract_goto_modelt &goto_model)
Definition: jbmc_parse_options.cpp:877
set_properties
void set_properties(goto_programt &goto_program, std::unordered_set< irep_idt > &property_set)
Definition: set_properties.cpp:19
journalling_symbol_tablet
A symbol table wrapper that records which entries have been updated/removedA caller can pass a journa...
Definition: journalling_symbol_table.h:36
align_center_with_border
std::string align_center_with_border(const std::string &text)
Utility for displaying help centered messages borderered by "* *".
Definition: parse_options.cpp:150
journalling_symbol_tablet::get_symbol_table
virtual const symbol_tablet & get_symbol_table() const override
Definition: journalling_symbol_table.h:75
goto_model_functiont
Interface providing access to a single function in a GOTO model, plus its associated symbol table.
Definition: goto_model.h:183
HELP_XML_INTERFACE
#define HELP_XML_INTERFACE
Definition: xml_interface.h:39
HELP_TIMESTAMP
#define HELP_TIMESTAMP
Definition: timestamper.h:14
HELP_FLUSH
#define HELP_FLUSH
Definition: ui_message.h:106
replace_java_nondet.h
Replace Java Nondet expressions.
HELP_VALIDATE
#define HELP_VALIDATE
Definition: validation_interface.h:16
jbmc_parse_optionst::method_context
optionalt< prefix_filtert > method_context
See java_bytecode_languaget::method_context.
Definition: jbmc_parse_options.h:143
CPROVER_EXIT_PARSE_ERROR
#define CPROVER_EXIT_PARSE_ERROR
An error during parsing of the input program.
Definition: exit_codes.h:37