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 <cstdlib> // exit()
15 #include <iostream>
16 #include <memory>
17 
18 #include <util/config.h>
19 #include <util/exit_codes.h>
20 #include <util/invariant.h>
21 #include <util/make_unique.h>
22 #include <util/version.h>
23 #include <util/xml.h>
24 
25 #include <langapi/language.h>
26 
27 #include <ansi-c/ansi_c_language.h>
28 
34 
38 #include <goto-programs/loop_ids.h>
47 
51 
53 
55 
57 
58 #include <langapi/mode.h>
59 
72 
73 jbmc_parse_optionst::jbmc_parse_optionst(int argc, const char **argv)
76  argc,
77  argv,
78  std::string("JBMC ") + CBMC_VERSION)
79 {
82 }
83 
85  int argc,
86  const char **argv,
87  const std::string &extra_options)
89  JBMC_OPTIONS + extra_options,
90  argc,
91  argv,
92  std::string("JBMC ") + CBMC_VERSION)
93 {
96 }
97 
99 {
100  // Default true
101  options.set_option("assertions", true);
102  options.set_option("assumptions", true);
103  options.set_option("built-in-assertions", true);
104  options.set_option("lazy-methods", true);
105  options.set_option("pretty-names", true);
106  options.set_option("propagation", true);
107  options.set_option("refine-strings", true);
108  options.set_option("sat-preprocessor", true);
109  options.set_option("simple-slice", true);
110  options.set_option("simplify", true);
111  options.set_option("simplify-if", true);
112  options.set_option("show-goto-symex-steps", false);
113 
114  // Other default
115  options.set_option("arrays-uf", "auto");
116  options.set_option("depth", UINT32_MAX);
117 }
118 
120 {
121  if(config.set(cmdline))
122  {
123  usage_error();
124  exit(1); // should contemplate EX_USAGE from sysexits.h
125  }
126 
128 
129  if(cmdline.isset("function"))
130  options.set_option("function", cmdline.get_value("function"));
131 
134 
135  if(cmdline.isset("max-field-sensitivity-array-size"))
136  {
137  options.set_option(
138  "max-field-sensitivity-array-size",
139  cmdline.get_value("max-field-sensitivity-array-size"));
140  }
141 
142  if(cmdline.isset("no-array-field-sensitivity"))
143  {
144  if(cmdline.isset("max-field-sensitivity-array-size"))
145  {
146  log.error()
147  << "--no-array-field-sensitivity and --max-field-sensitivity-array-size"
148  << " must not be given together" << messaget::eom;
150  }
151  options.set_option("no-array-field-sensitivity", true);
152  }
153 
154  if(cmdline.isset("show-symex-strategies"))
155  {
157  exit(CPROVER_EXIT_SUCCESS);
158  }
159 
161 
162  if(cmdline.isset("program-only"))
163  options.set_option("program-only", true);
164 
165  if(cmdline.isset("show-vcc"))
166  options.set_option("show-vcc", true);
167 
168  if(cmdline.isset("nondet-static"))
169  options.set_option("nondet-static", true);
170 
171  if(cmdline.isset("no-simplify"))
172  options.set_option("simplify", false);
173 
174  if(cmdline.isset("stop-on-fail") ||
175  cmdline.isset("dimacs") ||
176  cmdline.isset("outfile"))
177  options.set_option("stop-on-fail", true);
178 
179  if(
180  cmdline.isset("trace") || cmdline.isset("compact-trace") ||
181  cmdline.isset("stack-trace") || cmdline.isset("stop-on-fail") ||
183  !cmdline.isset("cover")))
184  {
185  options.set_option("trace", true);
186  }
187 
188  if(cmdline.isset("validate-trace"))
189  {
190  options.set_option("validate-trace", true);
191  options.set_option("trace", true);
192  }
193 
194  if(cmdline.isset("localize-faults"))
195  options.set_option("localize-faults", true);
196 
197  if(cmdline.isset("symex-complexity-limit"))
198  {
199  options.set_option(
200  "symex-complexity-limit", cmdline.get_value("symex-complexity-limit"));
201  }
202 
203  if(cmdline.isset("symex-complexity-failed-child-loops-limit"))
204  {
205  options.set_option(
206  "symex-complexity-failed-child-loops-limit",
207  cmdline.get_value("symex-complexity-failed-child-loops-limit"));
208  }
209 
210  if(cmdline.isset("unwind"))
211  options.set_option("unwind", cmdline.get_value("unwind"));
212 
213  if(cmdline.isset("depth"))
214  options.set_option("depth", cmdline.get_value("depth"));
215 
216  if(cmdline.isset("debug-level"))
217  options.set_option("debug-level", cmdline.get_value("debug-level"));
218 
219  if(cmdline.isset("unwindset"))
220  options.set_option("unwindset", cmdline.get_value("unwindset"));
221 
222  // constant propagation
223  if(cmdline.isset("no-propagation"))
224  options.set_option("propagation", false);
225 
226  // transform self loops to assumptions
227  options.set_option(
228  "self-loops-to-assumptions",
229  !cmdline.isset("no-self-loops-to-assumptions"));
230 
231  // all checks supported by goto_check
233 
234  // unwind loops in java enum static initialization
235  if(cmdline.isset("java-unwind-enum-static"))
236  options.set_option("java-unwind-enum-static", true);
237 
238  // check assertions
239  if(cmdline.isset("no-assertions"))
240  options.set_option("assertions", false);
241 
242  // use assumptions
243  if(cmdline.isset("no-assumptions"))
244  options.set_option("assumptions", false);
245 
246  // generate unwinding assertions
247  if(cmdline.isset("unwinding-assertions"))
248  options.set_option("unwinding-assertions", true);
249 
250  // generate unwinding assumptions otherwise
251  options.set_option(
252  "partial-loops",
253  cmdline.isset("partial-loops"));
254 
255  if(options.get_bool_option("partial-loops") &&
256  options.get_bool_option("unwinding-assertions"))
257  {
258  log.error() << "--partial-loops and --unwinding-assertions "
259  << "must not be given together" << messaget::eom;
260  exit(1); // should contemplate EX_USAGE from sysexits.h
261  }
262 
263  // remove unused equations
264  options.set_option(
265  "slice-formula",
266  cmdline.isset("slice-formula"));
267 
268  // simplify if conditions and branches
269  if(cmdline.isset("no-simplify-if"))
270  options.set_option("simplify-if", false);
271 
272  if(cmdline.isset("arrays-uf-always"))
273  options.set_option("arrays-uf", "always");
274  else if(cmdline.isset("arrays-uf-never"))
275  options.set_option("arrays-uf", "never");
276 
277  if(cmdline.isset("dimacs"))
278  options.set_option("dimacs", true);
279 
280  if(cmdline.isset("refine-arrays"))
281  {
282  options.set_option("refine", true);
283  options.set_option("refine-arrays", true);
284  }
285 
286  if(cmdline.isset("refine-arithmetic"))
287  {
288  options.set_option("refine", true);
289  options.set_option("refine-arithmetic", true);
290  }
291 
292  if(cmdline.isset("refine"))
293  {
294  options.set_option("refine", true);
295  options.set_option("refine-arrays", true);
296  options.set_option("refine-arithmetic", true);
297  }
298 
299  if(cmdline.isset("no-refine-strings"))
300  options.set_option("refine-strings", false);
301 
302  if(cmdline.isset("string-printable") && cmdline.isset("no-refine-strings"))
303  {
305  "cannot use --string-printable with --no-refine-strings",
306  "--string-printable");
307  }
308 
309  if(cmdline.isset("string-input-value") && cmdline.isset("no-refine-strings"))
310  {
312  "cannot use --string-input-value with --no-refine-strings",
313  "--string-input-value");
314  }
315 
316  if(
317  cmdline.isset("no-refine-strings") &&
318  cmdline.isset("max-nondet-string-length"))
319  {
321  "cannot use --max-nondet-string-length with --no-refine-strings",
322  "--max-nondet-string-length");
323  }
324 
325  if(cmdline.isset("max-node-refinement"))
326  options.set_option(
327  "max-node-refinement",
328  cmdline.get_value("max-node-refinement"));
329 
330  // SMT Options
331 
332  if(cmdline.isset("smt1"))
333  {
334  log.error() << "--smt1 is no longer supported" << messaget::eom;
336  }
337 
338  if(cmdline.isset("smt2"))
339  options.set_option("smt2", true);
340 
341  if(cmdline.isset("fpa"))
342  options.set_option("fpa", true);
343 
344  bool solver_set=false;
345 
346  if(cmdline.isset("boolector"))
347  {
348  options.set_option("boolector", true), solver_set=true;
349  options.set_option("smt2", true);
350  }
351 
352  if(cmdline.isset("mathsat"))
353  {
354  options.set_option("mathsat", true), solver_set=true;
355  options.set_option("smt2", true);
356  }
357 
358  if(cmdline.isset("cvc4"))
359  {
360  options.set_option("cvc4", true), solver_set=true;
361  options.set_option("smt2", true);
362  }
363 
364  if(cmdline.isset("yices"))
365  {
366  options.set_option("yices", true), solver_set=true;
367  options.set_option("smt2", true);
368  }
369 
370  if(cmdline.isset("z3"))
371  {
372  options.set_option("z3", true), solver_set=true;
373  options.set_option("smt2", true);
374  }
375 
376  if(cmdline.isset("smt2") && !solver_set)
377  {
378  if(cmdline.isset("outfile"))
379  {
380  // outfile and no solver should give standard compliant SMT-LIB
381  options.set_option("generic", true);
382  }
383  else
384  {
385  // the default smt2 solver
386  options.set_option("z3", true);
387  }
388  }
389 
390  if(cmdline.isset("beautify"))
391  options.set_option("beautify", true);
392 
393  if(cmdline.isset("no-sat-preprocessor"))
394  options.set_option("sat-preprocessor", false);
395 
396  options.set_option(
397  "pretty-names",
398  !cmdline.isset("no-pretty-names"));
399 
400  if(cmdline.isset("outfile"))
401  options.set_option("outfile", cmdline.get_value("outfile"));
402 
403  if(cmdline.isset("graphml-witness"))
404  {
405  options.set_option("graphml-witness", cmdline.get_value("graphml-witness"));
406  options.set_option("stop-on-fail", true);
407  options.set_option("trace", true);
408  }
409 
410  if(cmdline.isset("symex-coverage-report"))
411  options.set_option(
412  "symex-coverage-report",
413  cmdline.get_value("symex-coverage-report"));
414 
415  if(cmdline.isset("validate-ssa-equation"))
416  {
417  options.set_option("validate-ssa-equation", true);
418  }
419 
420  if(cmdline.isset("validate-goto-model"))
421  {
422  options.set_option("validate-goto-model", true);
423  }
424 
425  options.set_option(
426  "symex-cache-dereferences", cmdline.isset("symex-cache-dereferences"));
427 
429 
430  if(cmdline.isset("no-lazy-methods"))
431  options.set_option("lazy-methods", false);
432 
433  if(cmdline.isset("symex-driven-lazy-loading"))
434  {
435  options.set_option("symex-driven-lazy-loading", true);
436  for(const char *opt :
437  { "nondet-static",
438  "full-slice",
439  "reachability-slice",
440  "reachability-slice-fb" })
441  {
442  if(cmdline.isset(opt))
443  {
444  throw std::string("Option ") + opt +
445  " can't be used with --symex-driven-lazy-loading";
446  }
447  }
448  }
449 
450  // The 'allow-pointer-unsoundness' option prevents symex from throwing an
451  // exception when it encounters pointers that are shared across threads.
452  // This is unsound but given that pointers are ubiquitous in java this check
453  // must be disabled in order to support the analysis of multithreaded java
454  // code.
455  if(cmdline.isset("java-threading"))
456  options.set_option("allow-pointer-unsoundness", true);
457 
458  if(cmdline.isset("show-goto-symex-steps"))
459  options.set_option("show-goto-symex-steps", true);
460 }
461 
464 {
465  if(cmdline.isset("version"))
466  {
467  std::cout << CBMC_VERSION << '\n';
468  return CPROVER_EXIT_SUCCESS;
469  }
470 
473 
474  //
475  // command line options
476  //
477 
478  optionst options;
479  get_command_line_options(options);
480 
482 
483  // output the options
484  switch(ui_message_handler.get_ui())
485  {
488  log.debug(), [&options](messaget::mstreamt &debug_stream) {
489  debug_stream << "\nOptions: \n";
490  options.output(debug_stream);
491  debug_stream << messaget::eom;
492  });
493  break;
495  {
496  json_objectt json_options{{"options", options.to_json()}};
497  log.debug() << json_options;
498  break;
499  }
501  log.debug() << options.to_xml();
502  break;
503  }
504 
507 
508  if(!((cmdline.isset("jar") && cmdline.args.empty()) ||
509  (cmdline.isset("gb") && cmdline.args.empty()) ||
510  (!cmdline.isset("jar") && !cmdline.isset("gb") &&
511  (cmdline.args.size() == 1))))
512  {
513  log.error() << "Please give exactly one class name, "
514  << "and/or use -jar jarfile or --gb goto-binary"
515  << messaget::eom;
517  }
518 
519  if((cmdline.args.size() == 1) && !cmdline.isset("show-parse-tree"))
520  {
521  std::string main_class = cmdline.args[0];
522  // `java` accepts slashes and dots as package separators
523  std::replace(main_class.begin(), main_class.end(), '/', '.');
524  config.java.main_class = main_class;
525  cmdline.args.pop_back();
526  }
527 
528  if(cmdline.isset("jar"))
529  {
530  cmdline.args.push_back(cmdline.get_value("jar"));
531  }
532 
533  if(cmdline.isset("gb"))
534  {
535  cmdline.args.push_back(cmdline.get_value("gb"));
536  }
537 
538  // Shows the parse tree of the main class
539  if(cmdline.isset("show-parse-tree"))
540  {
541  std::unique_ptr<languaget> language = get_language_from_mode(ID_java);
542  CHECK_RETURN(language != nullptr);
543  language->set_language_options(options);
545 
546  log.status() << "Parsing ..." << messaget::eom;
547 
548  if(static_cast<java_bytecode_languaget *>(language.get())->parse())
549  {
550  log.error() << "PARSING ERROR" << messaget::eom;
552  }
553 
554  language->show_parse(std::cout);
555  return CPROVER_EXIT_SUCCESS;
556  }
557 
558  object_factory_params.set(options);
559 
561  options.get_bool_option("java-assume-inputs-non-null");
562 
563  std::unique_ptr<abstract_goto_modelt> goto_model_ptr;
564  int get_goto_program_ret = get_goto_program(goto_model_ptr, options);
565  if(get_goto_program_ret != -1)
566  return get_goto_program_ret;
567 
568  if(
569  options.get_bool_option("program-only") ||
570  options.get_bool_option("show-vcc") ||
571  (options.get_bool_option("symex-driven-lazy-loading") &&
572  (cmdline.isset("show-symbol-table") || cmdline.isset("list-symbols") ||
573  cmdline.isset("show-goto-functions") ||
574  cmdline.isset("list-goto-functions") ||
575  cmdline.isset("show-properties") || cmdline.isset("show-loops"))))
576  {
577  if(options.get_bool_option("paths"))
578  {
580  options, ui_message_handler, *goto_model_ptr);
581  (void)verifier();
582  }
583  else
584  {
586  options, ui_message_handler, *goto_model_ptr);
587  (void)verifier();
588  }
589 
590  if(options.get_bool_option("symex-driven-lazy-loading"))
591  {
592  // We can only output these after goto-symex has run.
593  (void)show_loaded_symbols(*goto_model_ptr);
594  (void)show_loaded_functions(*goto_model_ptr);
595  }
596 
597  return CPROVER_EXIT_SUCCESS;
598  }
599 
600  if(
601  options.get_bool_option("dimacs") || !options.get_option("outfile").empty())
602  {
603  if(options.get_bool_option("paths"))
604  {
606  options, ui_message_handler, *goto_model_ptr);
607  (void)verifier();
608  }
609  else
610  {
612  options, ui_message_handler, *goto_model_ptr);
613  (void)verifier();
614  }
615 
616  return CPROVER_EXIT_SUCCESS;
617  }
618 
619  std::unique_ptr<goto_verifiert> verifier = nullptr;
620 
621  if(
622  options.get_bool_option("stop-on-fail") && options.get_bool_option("paths"))
623  {
624  verifier =
625  util_make_unique<stop_on_fail_verifiert<java_single_path_symex_checkert>>(
626  options, ui_message_handler, *goto_model_ptr);
627  }
628  else if(
629  options.get_bool_option("stop-on-fail") &&
630  !options.get_bool_option("paths"))
631  {
632  if(options.get_bool_option("localize-faults"))
633  {
634  verifier =
637  options, ui_message_handler, *goto_model_ptr);
638  }
639  else
640  {
641  verifier = util_make_unique<
643  options, ui_message_handler, *goto_model_ptr);
644  }
645  }
646  else if(
647  !options.get_bool_option("stop-on-fail") &&
648  options.get_bool_option("paths"))
649  {
652  options, ui_message_handler, *goto_model_ptr);
653  }
654  else if(
655  !options.get_bool_option("stop-on-fail") &&
656  !options.get_bool_option("paths"))
657  {
658  if(options.get_bool_option("localize-faults"))
659  {
660  verifier =
663  options, ui_message_handler, *goto_model_ptr);
664  }
665  else
666  {
669  options, ui_message_handler, *goto_model_ptr);
670  }
671  }
672  else
673  {
674  UNREACHABLE;
675  }
676 
677  const resultt result = (*verifier)();
678  verifier->report();
679  return result_to_exit_code(result);
680 }
681 
683  std::unique_ptr<abstract_goto_modelt> &goto_model_ptr,
684  const optionst &options)
685 {
686  if(options.is_set("context-include") || options.is_set("context-exclude"))
687  method_context = get_context(options);
688  lazy_goto_modelt lazy_goto_model =
690  lazy_goto_model.initialize(cmdline.args, options);
691 
693  util_make_unique<class_hierarchyt>(lazy_goto_model.symbol_table);
694 
695  // Show the class hierarchy
696  if(cmdline.isset("show-class-hierarchy"))
697  {
699  return CPROVER_EXIT_SUCCESS;
700  }
701 
702  // Add failed symbols for any symbol created prior to loading any
703  // particular function:
704  add_failed_symbols(lazy_goto_model.symbol_table);
705 
706  if(!options.get_bool_option("symex-driven-lazy-loading"))
707  {
708  log.status() << "Generating GOTO Program" << messaget::eom;
709  lazy_goto_model.load_all_functions();
710 
711  // show symbol table or list symbols
712  if(show_loaded_symbols(lazy_goto_model))
713  return CPROVER_EXIT_SUCCESS;
714 
715  // Move the model out of the local lazy_goto_model
716  // and into the caller's goto_model
718  std::move(lazy_goto_model));
719  if(goto_model_ptr == nullptr)
721 
722  goto_modelt &goto_model = dynamic_cast<goto_modelt &>(*goto_model_ptr);
723 
724  // if we added the ansi-c library models here this should also call
725  // add_malloc_may_fail_variable_initializations(goto_model);
726  // here
727 
728  if(cmdline.isset("validate-goto-model"))
729  {
730  goto_model.validate();
731  }
732 
733  if(show_loaded_functions(goto_model))
734  return CPROVER_EXIT_SUCCESS;
735 
736  if(cmdline.isset("property"))
737  ::set_properties(goto_model, cmdline.get_values("property"));
738  }
739  else
740  {
741  // The precise wording of this error matches goto-symex's complaint when no
742  // __CPROVER_start exists (if we just go ahead and run it anyway it will
743  // trip an invariant when it tries to load it)
745  {
746  log.error() << "the program has no entry point" << messaget::eom;
748  }
749 
750  if(cmdline.isset("validate-goto-model"))
751  {
752  lazy_goto_model.validate();
753  }
754 
755  goto_model_ptr =
756  util_make_unique<lazy_goto_modelt>(std::move(lazy_goto_model));
757  }
758 
760 
761  return -1; // no error, continue
762 }
763 
765  goto_model_functiont &function,
766  const abstract_goto_modelt &model,
767  const optionst &options)
768 {
769  journalling_symbol_tablet &symbol_table = function.get_symbol_table();
770  namespacet ns(symbol_table);
771  goto_functionst::goto_functiont &goto_function = function.get_goto_function();
772 
773  bool using_symex_driven_loading =
774  options.get_bool_option("symex-driven-lazy-loading");
775 
776  // Removal of RTTI inspection:
778  function.get_function_id(),
779  goto_function,
780  symbol_table,
783  // Java virtual functions -> explicit dispatch tables:
785 
786  auto function_is_stub = [&symbol_table, &model](const irep_idt &id) {
787  return symbol_table.lookup_ref(id).value.is_nil() &&
788  !model.can_produce_function(id);
789  };
790 
791  remove_returns(function, function_is_stub);
792 
793  replace_java_nondet(function);
794 
795  // Similar removal of java nondet statements:
797 
798  if(using_symex_driven_loading)
799  {
800  // remove exceptions
801  // If using symex-driven function loading we need to do this now so that
802  // symex doesn't have to cope with exception-handling constructs; however
803  // the results are slightly worse than running it in whole-program mode
804  // (e.g. dead catch sites will be retained)
806  function.get_function_id(),
807  goto_function.body,
808  symbol_table,
809  *class_hierarchy.get(),
811  }
812 
813  // add generic checks
814  goto_check(
815  function.get_function_id(), function.get_goto_function(), ns, options);
816 
817  // Replace Java new side effects
819  function.get_function_id(),
820  goto_function,
821  symbol_table,
823 
824  // checks don't know about adjusted float expressions
825  adjust_float_expressions(goto_function, ns);
826 
827  // add failed symbols for anything created relating to this particular
828  // function (note this means subsequent passes mustn't create more!):
830  symbol_table.get_inserted();
831  for(const irep_idt &new_symbol_name : new_symbols)
832  {
834  symbol_table.lookup_ref(new_symbol_name), symbol_table);
835  }
836 
837  // If using symex-driven function loading we must label the assertions
838  // now so symex sees its targets; otherwise we leave this until
839  // process_goto_functions, as we haven't run remove_exceptions yet, and that
840  // pass alters the CFG.
841  if(using_symex_driven_loading)
842  {
843  // label the assertions
844  label_properties(goto_function.body);
845 
846  goto_function.body.update();
847  function.compute_location_numbers();
848  goto_function.body.compute_loop_numbers();
849  }
850 }
851 
853  const abstract_goto_modelt &goto_model)
854 {
855  if(cmdline.isset("show-symbol-table"))
856  {
858  return true;
859  }
860  else if(cmdline.isset("list-symbols"))
861  {
863  return true;
864  }
865 
866  return false;
867 }
868 
870  const abstract_goto_modelt &goto_model)
871 {
872  if(cmdline.isset("show-loops"))
873  {
875  return true;
876  }
877 
878  if(
879  cmdline.isset("show-goto-functions") ||
880  cmdline.isset("list-goto-functions"))
881  {
882  namespacet ns(goto_model.get_symbol_table());
884  ns,
886  goto_model.get_goto_functions(),
887  cmdline.isset("list-goto-functions"));
888  return true;
889  }
890 
891  if(cmdline.isset("show-properties"))
892  {
893  namespacet ns(goto_model.get_symbol_table());
895  return true;
896  }
897 
898  return false;
899 }
900 
902  goto_modelt &goto_model,
903  const optionst &options)
904 {
905  log.status() << "Running GOTO functions transformation passes"
906  << messaget::eom;
907 
908  bool using_symex_driven_loading =
909  options.get_bool_option("symex-driven-lazy-loading");
910 
911  // When using symex-driven lazy loading, *all* relevant processing is done
912  // during process_goto_function, so we have nothing to do here.
913  if(using_symex_driven_loading)
914  return false;
915 
916  // remove catch and throw
918 
919  // instrument library preconditions
920  instrument_preconditions(goto_model);
921 
922  // ignore default/user-specified initialization
923  // of variables with static lifetime
924  if(cmdline.isset("nondet-static"))
925  {
926  log.status() << "Adding nondeterministic initialization "
927  "of static/global variables"
928  << messaget::eom;
929  nondet_static(goto_model);
930  }
931 
932  // recalculate numbers, etc.
933  goto_model.goto_functions.update();
934 
935  if(cmdline.isset("drop-unused-functions"))
936  {
937  // Entry point will have been set before and function pointers removed
938  log.status() << "Removing unused functions" << messaget::eom;
940  }
941 
942  // remove skips such that trivial GOTOs are deleted
943  remove_skip(goto_model);
944 
945  // label the assertions
946  // This must be done after adding assertions and
947  // before using the argument of the "property" option.
948  // Do not re-label after using the property slicer because
949  // this would cause the property identifiers to change.
950  label_properties(goto_model);
951 
952  // reachability slice?
953  if(cmdline.isset("reachability-slice-fb"))
954  {
955  if(cmdline.isset("reachability-slice"))
956  {
957  log.error() << "--reachability-slice and --reachability-slice-fb "
958  << "must not be given together" << messaget::eom;
959  return true;
960  }
961 
962  log.status() << "Performing a forwards-backwards reachability slice"
963  << messaget::eom;
964  if(cmdline.isset("property"))
965  reachability_slicer(goto_model, cmdline.get_values("property"), true);
966  else
967  reachability_slicer(goto_model, true);
968  }
969 
970  if(cmdline.isset("reachability-slice"))
971  {
972  log.status() << "Performing a reachability slice" << messaget::eom;
973  if(cmdline.isset("property"))
974  reachability_slicer(goto_model, cmdline.get_values("property"));
975  else
976  reachability_slicer(goto_model);
977  }
978 
979  // full slice?
980  if(cmdline.isset("full-slice"))
981  {
982  log.status() << "Performing a full slice" << messaget::eom;
983  if(cmdline.isset("property"))
984  property_slicer(goto_model, cmdline.get_values("property"));
985  else
986  full_slicer(goto_model);
987  }
988 
989  // remove any skips introduced
990  remove_skip(goto_model);
991 
992  return false;
993 }
994 
996 {
997  static const irep_idt initialize_id = INITIALIZE_FUNCTION;
998 
999  return name != goto_functionst::entry_point() && name != initialize_id;
1000 }
1001 
1003  const irep_idt &function_name,
1004  symbol_table_baset &symbol_table,
1005  goto_functiont &function,
1006  bool body_available)
1007 {
1008  // Provide a simple stub implementation for any function we don't have a
1009  // bytecode implementation for:
1010 
1011  if(
1012  body_available &&
1013  (!method_context || (*method_context)(id2string(function_name))))
1014  return false;
1015 
1016  if(!can_generate_function_body(function_name))
1017  return false;
1018 
1019  if(symbol_table.lookup_ref(function_name).mode == ID_java)
1020  {
1022  function_name,
1023  symbol_table,
1027 
1028  goto_convert_functionst converter(symbol_table, ui_message_handler);
1029  converter.convert_function(function_name, function);
1030 
1031  return true;
1032  }
1033  else
1034  {
1035  return false;
1036  }
1037 }
1038 
1041 {
1042  // clang-format off
1043  std::cout << '\n' << banner_string("JBMC", CBMC_VERSION) << '\n'
1044  << align_center_with_border("Copyright (C) 2001-2018") << '\n'
1045  << align_center_with_border("Daniel Kroening, Edmund Clarke") << '\n' // NOLINT(*)
1046  << align_center_with_border("Carnegie Mellon University, Computer Science Department") << '\n' // NOLINT(*)
1047  << align_center_with_border("kroening@kroening.com") << '\n'
1048  << "\n"
1049  "Usage: Purpose:\n"
1050  "\n"
1051  " jbmc [-?] [-h] [--help] show help\n"
1052  " jbmc\n"
1054  " jbmc\n"
1056  " jbmc\n"
1058  " jbmc\n"
1060  "\n"
1063  "\n"
1064  "Analysis options:\n"
1066  " --symex-coverage-report f generate a Cobertura XML coverage report in f\n" // NOLINT(*)
1067  " --property id only check one specific property\n"
1068  " --trace give a counterexample trace for failed properties\n" //NOLINT(*)
1069  " --stop-on-fail stop analysis once a failed property is detected\n" // NOLINT(*)
1070  " (implies --trace)\n"
1072  "\n"
1073  "Program representations:\n"
1074  " --show-parse-tree show parse tree\n"
1075  " --show-symbol-table show loaded symbol table\n"
1076  " --list-symbols list symbols with type information\n"
1078  " --drop-unused-functions drop functions trivially unreachable\n"
1079  " from main function\n"
1081  "\n"
1082  "Program instrumentation options:\n"
1083  " --no-assertions ignore user assertions\n"
1084  " --no-assumptions ignore user assumptions\n"
1085  " --error-label label check that label is unreachable\n"
1086  " --mm MM memory consistency model for concurrent programs\n" // NOLINT(*)
1088  " --full-slice run full slicer (experimental)\n" // NOLINT(*)
1089  "\n"
1090  "Java Bytecode frontend options:\n"
1092  // This one is handled by jbmc_parse_options not by the Java frontend,
1093  // hence its presence here:
1094  " --java-threading enable java multi-threading support (experimental)\n" // NOLINT(*)
1095  " --java-unwind-enum-static unwind loops in static initialization of enums\n" // NOLINT(*)
1096  // Currently only supported in the JBMC frontend:
1097  " --symex-driven-lazy-loading only load functions when first entered by symbolic\n" // NOLINT(*)
1098  " execution. Note that --show-symbol-table,\n"
1099  " --show-goto-functions/properties output\n"
1100  " will be restricted to loaded methods in this case,\n" // NOLINT(*)
1101  " and only output after the symex phase.\n"
1102  "\n"
1103  "Semantic transformations:\n"
1104  // NOLINTNEXTLINE(whitespace/line_length)
1105  " --nondet-static add nondeterministic initialization of variables with static lifetime\n"
1106  "\n"
1107  "BMC options:\n"
1108  HELP_BMC
1109  "\n"
1110  "Backend options:\n"
1111  " --object-bits n number of bits used for object addresses\n"
1112  " --dimacs generate CNF in DIMACS format\n"
1113  " --beautify beautify the counterexample (greedy heuristic)\n" // NOLINT(*)
1114  " --localize-faults localize faults (experimental)\n"
1115  " --smt1 use default SMT1 solver (obsolete)\n"
1116  " --smt2 use default SMT2 solver (Z3)\n"
1117  " --boolector use Boolector\n"
1118  " --mathsat use MathSAT\n"
1119  " --cvc4 use CVC4\n"
1120  " --yices use Yices\n"
1121  " --z3 use Z3\n"
1122  " --refine use refinement procedure (experimental)\n"
1124  " --outfile filename output formula to given file\n"
1125  " --arrays-uf-never never turn arrays into uninterpreted functions\n" // NOLINT(*)
1126  " --arrays-uf-always always turn arrays into uninterpreted functions\n" // NOLINT(*)
1127  "\n"
1128  "Other options:\n"
1129  " --version show version and exit\n"
1134  HELP_FLUSH
1135  " --verbosity # verbosity level\n"
1137  "\n";
1138  // clang-format on
1139 }
cmdlinet::args
argst args
Definition: cmdline.h:143
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
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:201
HELP_SHOW_GOTO_FUNCTIONS
#define HELP_SHOW_GOTO_FUNCTIONS
Definition: show_goto_functions.h:25
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:1316
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:247
PARSE_OPTIONS_GOTO_CHECK
#define PARSE_OPTIONS_GOTO_CHECK(cmdline, options)
Definition: goto_check.h:70
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:119
HELP_GOTO_TRACE
#define HELP_GOTO_TRACE
Definition: goto_trace.h:277
parse_options_baset::ui_message_handler
ui_message_handlert ui_message_handler
Definition: parse_options.h:45
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:53
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:55
resultt
resultt
The result of goto verifying.
Definition: properties.h:45
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:901
optionst
Definition: options.h:23
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
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:262
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:44
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
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:764
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:144
replace
void replace(const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)
Definition: string_constraint.cpp:69
new_java_bytecode_language
std::unique_ptr< languaget > new_java_bytecode_language()
Definition: java_bytecode_language.cpp:1523
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:51
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:28
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:367
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:724
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:21
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:2371
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:171
parse_options_baset::log_version_and_architecture
void log_version_and_architecture(const std::string &front_end)
Write version and system architecture to log.status().
Definition: parse_options.cpp:152
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:1002
jbmc_parse_optionst::object_factory_params
java_object_factory_parameterst object_factory_params
Definition: jbmc_parse_options.h:127
JBMC_OPTIONS
#define JBMC_OPTIONS
Definition: jbmc_parse_options.h:43
show_symbol_table
void show_symbol_table(const symbol_tablet &symbol_table, ui_message_handlert &ui)
Definition: show_symbol_table.cpp:242
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:45
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:128
languaget::set_language_options
virtual void set_language_options(const optionst &)
Set language-specific options.
Definition: language.h:41
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:15
HELP_JAVA_JAR
#define HELP_JAVA_JAR
Definition: java_bytecode_language.h:159
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:297
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:137
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:33
parse_options_baset::usage_error
virtual void usage_error()
Definition: parse_options.cpp:49
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
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:164
full_slicer
void full_slicer(goto_functionst &goto_functions, const namespacet &ns, const slicing_criteriont &criterion)
Definition: full_slicer.cpp:348
jbmc_parse_optionst::doit
virtual int doit() override
invoke main modules
Definition: jbmc_parse_options.cpp:463
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:42
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:269
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:995
HELP_STRING_REFINEMENT
#define HELP_STRING_REFINEMENT
Definition: string_refinement.h:39
banner_string
std::string banner_string(const std::string &front_end, const std::string &version)
Definition: parse_options.cpp:174
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:693
instrument_preconditions
void instrument_preconditions(const goto_modelt &goto_model, goto_programt &goto_program)
Definition: instrument_preconditions.cpp:93
jbmc_parse_optionst::show_loaded_symbols
bool show_loaded_symbols(const abstract_goto_modelt &goto_model)
Definition: jbmc_parse_options.cpp:852
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:371
goto_convert_functionst
Definition: goto_convert_functions.h:41
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:114
jbmc_parse_optionst::class_hierarchy
std::unique_ptr< class_hierarchyt > class_hierarchy
Definition: jbmc_parse_options.h:130
INITIALIZE_FUNCTION
#define INITIALIZE_FUNCTION
Definition: static_lifetime_init.h:22
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:30
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:149
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:367
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:20
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:24
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:114
java_single_path_symex_checkert
Definition: java_single_path_symex_checker.h:20
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:435
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:144
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:25
remove_instanceof.h
Remove Instance-of Operators.
goto_functionst::goto_functiont
::goto_functiont goto_functiont
Definition: goto_functions.h:27
parse_options_baset::log
messaget log
Definition: parse_options.h:46
jbmc_parse_optionst::help
virtual void help() override
display command line help
Definition: jbmc_parse_options.cpp:1040
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:274
result_to_exit_code
int result_to_exit_code(resultt result)
Definition: properties.cpp:142
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:39
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:798
java_multi_path_symex_checkert
Definition: java_multi_path_symex_checker.h:20
HELP_JAVA_CLASSPATH
#define HELP_JAVA_CLASSPATH
Definition: java_bytecode_language.h:134
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:682
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:62
remove_returns
void remove_returns(symbol_table_baset &symbol_table, goto_functionst &goto_functions)
removes returns
Definition: remove_returns.cpp:252
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:139
new_ansi_c_language
std::unique_ptr< languaget > new_ansi_c_language()
Definition: ansi_c_language.cpp:141
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:83
configt::java
struct configt::javat java
show_path_strategies
std::string show_path_strategies()
suitable for displaying as a front-end help message
Definition: path_storage.cpp:111
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:310
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:98
PARSE_OPTIONS_GOTO_TRACE
#define PARSE_OPTIONS_GOTO_TRACE(cmdline, options)
Definition: goto_trace.h:285
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:84
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:272
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:92
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:73
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:77
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:105
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:273
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:869
set_properties
void set_properties(goto_programt &goto_program, std::unordered_set< irep_idt > &property_set)
Definition: set_properties.cpp:21
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:161
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:108
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:142
CPROVER_EXIT_PARSE_ERROR
#define CPROVER_EXIT_PARSE_ERROR
An error during parsing of the input program.
Definition: exit_codes.h:37