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 
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 
481  //
482  // Print a banner
483  //
484  log.status() << "JBMC version " << CBMC_VERSION << " " << sizeof(void *) * 8
485  << "-bit " << config.this_architecture() << " "
487 
488  // output the options
489  switch(ui_message_handler.get_ui())
490  {
493  log.debug(), [&options](messaget::mstreamt &debug_stream) {
494  debug_stream << "\nOptions: \n";
495  options.output(debug_stream);
496  debug_stream << messaget::eom;
497  });
498  break;
500  {
501  json_objectt json_options{{"options", options.to_json()}};
502  log.debug() << json_options;
503  break;
504  }
506  log.debug() << options.to_xml();
507  break;
508  }
509 
512 
513  if(!((cmdline.isset("jar") && cmdline.args.empty()) ||
514  (cmdline.isset("gb") && cmdline.args.empty()) ||
515  (!cmdline.isset("jar") && !cmdline.isset("gb") &&
516  (cmdline.args.size() == 1))))
517  {
518  log.error() << "Please give exactly one class name, "
519  << "and/or use -jar jarfile or --gb goto-binary"
520  << messaget::eom;
522  }
523 
524  if((cmdline.args.size() == 1) && !cmdline.isset("show-parse-tree"))
525  {
526  std::string main_class = cmdline.args[0];
527  // `java` accepts slashes and dots as package separators
528  std::replace(main_class.begin(), main_class.end(), '/', '.');
529  config.java.main_class = main_class;
530  cmdline.args.pop_back();
531  }
532 
533  if(cmdline.isset("jar"))
534  {
535  cmdline.args.push_back(cmdline.get_value("jar"));
536  }
537 
538  if(cmdline.isset("gb"))
539  {
540  cmdline.args.push_back(cmdline.get_value("gb"));
541  }
542 
543  // Shows the parse tree of the main class
544  if(cmdline.isset("show-parse-tree"))
545  {
546  std::unique_ptr<languaget> language = get_language_from_mode(ID_java);
547  CHECK_RETURN(language != nullptr);
548  language->set_language_options(options);
550 
551  log.status() << "Parsing ..." << messaget::eom;
552 
553  if(static_cast<java_bytecode_languaget *>(language.get())->parse())
554  {
555  log.error() << "PARSING ERROR" << messaget::eom;
557  }
558 
559  language->show_parse(std::cout);
560  return CPROVER_EXIT_SUCCESS;
561  }
562 
563  object_factory_params.set(options);
564 
566  options.get_bool_option("java-assume-inputs-non-null");
567 
568  std::unique_ptr<abstract_goto_modelt> goto_model_ptr;
569  int get_goto_program_ret = get_goto_program(goto_model_ptr, options);
570  if(get_goto_program_ret != -1)
571  return get_goto_program_ret;
572 
573  if(
574  options.get_bool_option("program-only") ||
575  options.get_bool_option("show-vcc") ||
576  (options.get_bool_option("symex-driven-lazy-loading") &&
577  (cmdline.isset("show-symbol-table") || cmdline.isset("list-symbols") ||
578  cmdline.isset("show-goto-functions") ||
579  cmdline.isset("list-goto-functions") ||
580  cmdline.isset("show-properties") || cmdline.isset("show-loops"))))
581  {
582  if(options.get_bool_option("paths"))
583  {
585  options, ui_message_handler, *goto_model_ptr);
586  (void)verifier();
587  }
588  else
589  {
591  options, ui_message_handler, *goto_model_ptr);
592  (void)verifier();
593  }
594 
595  if(options.get_bool_option("symex-driven-lazy-loading"))
596  {
597  // We can only output these after goto-symex has run.
598  (void)show_loaded_symbols(*goto_model_ptr);
599  (void)show_loaded_functions(*goto_model_ptr);
600  }
601 
602  return CPROVER_EXIT_SUCCESS;
603  }
604 
605  if(
606  options.get_bool_option("dimacs") || !options.get_option("outfile").empty())
607  {
608  if(options.get_bool_option("paths"))
609  {
611  options, ui_message_handler, *goto_model_ptr);
612  (void)verifier();
613  }
614  else
615  {
617  options, ui_message_handler, *goto_model_ptr);
618  (void)verifier();
619  }
620 
621  return CPROVER_EXIT_SUCCESS;
622  }
623 
624  std::unique_ptr<goto_verifiert> verifier = nullptr;
625 
626  if(
627  options.get_bool_option("stop-on-fail") && options.get_bool_option("paths"))
628  {
629  verifier =
630  util_make_unique<stop_on_fail_verifiert<java_single_path_symex_checkert>>(
631  options, ui_message_handler, *goto_model_ptr);
632  }
633  else if(
634  options.get_bool_option("stop-on-fail") &&
635  !options.get_bool_option("paths"))
636  {
637  if(options.get_bool_option("localize-faults"))
638  {
639  verifier =
642  options, ui_message_handler, *goto_model_ptr);
643  }
644  else
645  {
646  verifier = util_make_unique<
648  options, ui_message_handler, *goto_model_ptr);
649  }
650  }
651  else if(
652  !options.get_bool_option("stop-on-fail") &&
653  options.get_bool_option("paths"))
654  {
657  options, ui_message_handler, *goto_model_ptr);
658  }
659  else if(
660  !options.get_bool_option("stop-on-fail") &&
661  !options.get_bool_option("paths"))
662  {
663  if(options.get_bool_option("localize-faults"))
664  {
665  verifier =
668  options, ui_message_handler, *goto_model_ptr);
669  }
670  else
671  {
674  options, ui_message_handler, *goto_model_ptr);
675  }
676  }
677  else
678  {
679  UNREACHABLE;
680  }
681 
682  const resultt result = (*verifier)();
683  verifier->report();
684  return result_to_exit_code(result);
685 }
686 
688  std::unique_ptr<abstract_goto_modelt> &goto_model_ptr,
689  const optionst &options)
690 {
691  if(options.is_set("context-include") || options.is_set("context-exclude"))
692  method_context = get_context(options);
693  lazy_goto_modelt lazy_goto_model =
695  lazy_goto_model.initialize(cmdline.args, options);
696 
698  util_make_unique<class_hierarchyt>(lazy_goto_model.symbol_table);
699 
700  // Show the class hierarchy
701  if(cmdline.isset("show-class-hierarchy"))
702  {
704  return CPROVER_EXIT_SUCCESS;
705  }
706 
707  // Add failed symbols for any symbol created prior to loading any
708  // particular function:
709  add_failed_symbols(lazy_goto_model.symbol_table);
710 
711  if(!options.get_bool_option("symex-driven-lazy-loading"))
712  {
713  log.status() << "Generating GOTO Program" << messaget::eom;
714  lazy_goto_model.load_all_functions();
715 
716  // show symbol table or list symbols
717  if(show_loaded_symbols(lazy_goto_model))
718  return CPROVER_EXIT_SUCCESS;
719 
720  // Move the model out of the local lazy_goto_model
721  // and into the caller's goto_model
723  std::move(lazy_goto_model));
724  if(goto_model_ptr == nullptr)
726 
727  goto_modelt &goto_model = dynamic_cast<goto_modelt &>(*goto_model_ptr);
728 
729  // if we added the ansi-c library models here this should also call
730  // add_malloc_may_fail_variable_initializations(goto_model);
731  // here
732 
733  if(cmdline.isset("validate-goto-model"))
734  {
735  goto_model.validate();
736  }
737 
738  if(show_loaded_functions(goto_model))
739  return CPROVER_EXIT_SUCCESS;
740 
741  if(cmdline.isset("property"))
742  ::set_properties(goto_model, cmdline.get_values("property"));
743  }
744  else
745  {
746  // The precise wording of this error matches goto-symex's complaint when no
747  // __CPROVER_start exists (if we just go ahead and run it anyway it will
748  // trip an invariant when it tries to load it)
750  {
751  log.error() << "the program has no entry point" << messaget::eom;
753  }
754 
755  if(cmdline.isset("validate-goto-model"))
756  {
757  lazy_goto_model.validate();
758  }
759 
760  goto_model_ptr =
761  util_make_unique<lazy_goto_modelt>(std::move(lazy_goto_model));
762  }
763 
765 
766  return -1; // no error, continue
767 }
768 
770  goto_model_functiont &function,
771  const abstract_goto_modelt &model,
772  const optionst &options)
773 {
774  journalling_symbol_tablet &symbol_table = function.get_symbol_table();
775  namespacet ns(symbol_table);
776  goto_functionst::goto_functiont &goto_function = function.get_goto_function();
777 
778  bool using_symex_driven_loading =
779  options.get_bool_option("symex-driven-lazy-loading");
780 
781  // Removal of RTTI inspection:
783  function.get_function_id(),
784  goto_function,
785  symbol_table,
788  // Java virtual functions -> explicit dispatch tables:
790 
791  auto function_is_stub = [&symbol_table, &model](const irep_idt &id) {
792  return symbol_table.lookup_ref(id).value.is_nil() &&
793  !model.can_produce_function(id);
794  };
795 
796  remove_returns(function, function_is_stub);
797 
798  replace_java_nondet(function);
799 
800  // Similar removal of java nondet statements:
802 
803  if(using_symex_driven_loading)
804  {
805  // remove exceptions
806  // If using symex-driven function loading we need to do this now so that
807  // symex doesn't have to cope with exception-handling constructs; however
808  // the results are slightly worse than running it in whole-program mode
809  // (e.g. dead catch sites will be retained)
811  function.get_function_id(),
812  goto_function.body,
813  symbol_table,
814  *class_hierarchy.get(),
816  }
817 
818  // add generic checks
819  goto_check(
820  function.get_function_id(), function.get_goto_function(), ns, options);
821 
822  // Replace Java new side effects
824  function.get_function_id(),
825  goto_function,
826  symbol_table,
828 
829  // checks don't know about adjusted float expressions
830  adjust_float_expressions(goto_function, ns);
831 
832  // add failed symbols for anything created relating to this particular
833  // function (note this means subsequent passes mustn't create more!):
835  symbol_table.get_inserted();
836  for(const irep_idt &new_symbol_name : new_symbols)
837  {
839  symbol_table.lookup_ref(new_symbol_name), symbol_table);
840  }
841 
842  // If using symex-driven function loading we must label the assertions
843  // now so symex sees its targets; otherwise we leave this until
844  // process_goto_functions, as we haven't run remove_exceptions yet, and that
845  // pass alters the CFG.
846  if(using_symex_driven_loading)
847  {
848  // label the assertions
849  label_properties(goto_function.body);
850 
851  goto_function.body.update();
852  function.compute_location_numbers();
853  goto_function.body.compute_loop_numbers();
854  }
855 }
856 
858  const abstract_goto_modelt &goto_model)
859 {
860  if(cmdline.isset("show-symbol-table"))
861  {
863  return true;
864  }
865  else if(cmdline.isset("list-symbols"))
866  {
868  return true;
869  }
870 
871  return false;
872 }
873 
875  const abstract_goto_modelt &goto_model)
876 {
877  if(cmdline.isset("show-loops"))
878  {
880  return true;
881  }
882 
883  if(
884  cmdline.isset("show-goto-functions") ||
885  cmdline.isset("list-goto-functions"))
886  {
887  namespacet ns(goto_model.get_symbol_table());
889  ns,
891  goto_model.get_goto_functions(),
892  cmdline.isset("list-goto-functions"));
893  return true;
894  }
895 
896  if(cmdline.isset("show-properties"))
897  {
898  namespacet ns(goto_model.get_symbol_table());
900  return true;
901  }
902 
903  return false;
904 }
905 
907  goto_modelt &goto_model,
908  const optionst &options)
909 {
910  log.status() << "Running GOTO functions transformation passes"
911  << messaget::eom;
912 
913  bool using_symex_driven_loading =
914  options.get_bool_option("symex-driven-lazy-loading");
915 
916  // When using symex-driven lazy loading, *all* relevant processing is done
917  // during process_goto_function, so we have nothing to do here.
918  if(using_symex_driven_loading)
919  return false;
920 
921  // remove catch and throw
923 
924  // instrument library preconditions
925  instrument_preconditions(goto_model);
926 
927  // ignore default/user-specified initialization
928  // of variables with static lifetime
929  if(cmdline.isset("nondet-static"))
930  {
931  log.status() << "Adding nondeterministic initialization "
932  "of static/global variables"
933  << messaget::eom;
934  nondet_static(goto_model);
935  }
936 
937  // recalculate numbers, etc.
938  goto_model.goto_functions.update();
939 
940  if(cmdline.isset("drop-unused-functions"))
941  {
942  // Entry point will have been set before and function pointers removed
943  log.status() << "Removing unused functions" << messaget::eom;
945  }
946 
947  // remove skips such that trivial GOTOs are deleted
948  remove_skip(goto_model);
949 
950  // label the assertions
951  // This must be done after adding assertions and
952  // before using the argument of the "property" option.
953  // Do not re-label after using the property slicer because
954  // this would cause the property identifiers to change.
955  label_properties(goto_model);
956 
957  // reachability slice?
958  if(cmdline.isset("reachability-slice-fb"))
959  {
960  if(cmdline.isset("reachability-slice"))
961  {
962  log.error() << "--reachability-slice and --reachability-slice-fb "
963  << "must not be given together" << messaget::eom;
964  return true;
965  }
966 
967  log.status() << "Performing a forwards-backwards reachability slice"
968  << messaget::eom;
969  if(cmdline.isset("property"))
970  reachability_slicer(goto_model, cmdline.get_values("property"), true);
971  else
972  reachability_slicer(goto_model, true);
973  }
974 
975  if(cmdline.isset("reachability-slice"))
976  {
977  log.status() << "Performing a reachability slice" << messaget::eom;
978  if(cmdline.isset("property"))
979  reachability_slicer(goto_model, cmdline.get_values("property"));
980  else
981  reachability_slicer(goto_model);
982  }
983 
984  // full slice?
985  if(cmdline.isset("full-slice"))
986  {
987  log.status() << "Performing a full slice" << messaget::eom;
988  if(cmdline.isset("property"))
989  property_slicer(goto_model, cmdline.get_values("property"));
990  else
991  full_slicer(goto_model);
992  }
993 
994  // remove any skips introduced
995  remove_skip(goto_model);
996 
997  return false;
998 }
999 
1001 {
1002  static const irep_idt initialize_id = INITIALIZE_FUNCTION;
1003 
1004  return name != goto_functionst::entry_point() && name != initialize_id;
1005 }
1006 
1008  const irep_idt &function_name,
1009  symbol_table_baset &symbol_table,
1010  goto_functiont &function,
1011  bool body_available)
1012 {
1013  // Provide a simple stub implementation for any function we don't have a
1014  // bytecode implementation for:
1015 
1016  if(
1017  body_available &&
1018  (!method_context || (*method_context)(id2string(function_name))))
1019  return false;
1020 
1021  if(!can_generate_function_body(function_name))
1022  return false;
1023 
1024  if(symbol_table.lookup_ref(function_name).mode == ID_java)
1025  {
1027  function_name,
1028  symbol_table,
1032 
1033  goto_convert_functionst converter(symbol_table, ui_message_handler);
1034  converter.convert_function(function_name, function);
1035 
1036  return true;
1037  }
1038  else
1039  {
1040  return false;
1041  }
1042 }
1043 
1046 {
1047  // clang-format off
1048  std::cout << '\n' << banner_string("JBMC", CBMC_VERSION) << '\n'
1049  << align_center_with_border("Copyright (C) 2001-2018") << '\n'
1050  << align_center_with_border("Daniel Kroening, Edmund Clarke") << '\n' // NOLINT(*)
1051  << align_center_with_border("Carnegie Mellon University, Computer Science Department") << '\n' // NOLINT(*)
1052  << align_center_with_border("kroening@kroening.com") << '\n'
1053  << "\n"
1054  "Usage: Purpose:\n"
1055  "\n"
1056  " jbmc [-?] [-h] [--help] show help\n"
1057  " jbmc\n"
1059  " jbmc\n"
1061  " jbmc\n"
1063  " jbmc\n"
1065  "\n"
1068  "\n"
1069  "Analysis options:\n"
1071  " --symex-coverage-report f generate a Cobertura XML coverage report in f\n" // NOLINT(*)
1072  " --property id only check one specific property\n"
1073  " --stop-on-fail stop analysis once a failed property is detected\n" // NOLINT(*)
1074  " --trace give a counterexample trace for failed properties\n" //NOLINT(*)
1076  "\n"
1077  "Program representations:\n"
1078  " --show-parse-tree show parse tree\n"
1079  " --show-symbol-table show loaded symbol table\n"
1080  " --list-symbols list symbols with type information\n"
1082  " --drop-unused-functions drop functions trivially unreachable\n"
1083  " from main function\n"
1085  "\n"
1086  "Program instrumentation options:\n"
1087  " --no-assertions ignore user assertions\n"
1088  " --no-assumptions ignore user assumptions\n"
1089  " --error-label label check that label is unreachable\n"
1090  " --mm MM memory consistency model for concurrent programs\n" // NOLINT(*)
1092  " --full-slice run full slicer (experimental)\n" // NOLINT(*)
1093  "\n"
1094  "Java Bytecode frontend options:\n"
1096  // This one is handled by jbmc_parse_options not by the Java frontend,
1097  // hence its presence here:
1098  " --java-threading enable java multi-threading support (experimental)\n" // NOLINT(*)
1099  " --java-unwind-enum-static unwind loops in static initialization of enums\n" // NOLINT(*)
1100  // Currently only supported in the JBMC frontend:
1101  " --symex-driven-lazy-loading only load functions when first entered by symbolic\n" // NOLINT(*)
1102  " execution. Note that --show-symbol-table,\n"
1103  " --show-goto-functions/properties output\n"
1104  " will be restricted to loaded methods in this case,\n" // NOLINT(*)
1105  " and only output after the symex phase.\n"
1106  "\n"
1107  "Semantic transformations:\n"
1108  // NOLINTNEXTLINE(whitespace/line_length)
1109  " --nondet-static add nondeterministic initialization of variables with static lifetime\n"
1110  "\n"
1111  "BMC options:\n"
1112  HELP_BMC
1113  "\n"
1114  "Backend options:\n"
1115  " --object-bits n number of bits used for object addresses\n"
1116  " --dimacs generate CNF in DIMACS format\n"
1117  " --beautify beautify the counterexample (greedy heuristic)\n" // NOLINT(*)
1118  " --localize-faults localize faults (experimental)\n"
1119  " --smt1 use default SMT1 solver (obsolete)\n"
1120  " --smt2 use default SMT2 solver (Z3)\n"
1121  " --boolector use Boolector\n"
1122  " --mathsat use MathSAT\n"
1123  " --cvc4 use CVC4\n"
1124  " --yices use Yices\n"
1125  " --z3 use Z3\n"
1126  " --refine use refinement procedure (experimental)\n"
1128  " --outfile filename output formula to given file\n"
1129  " --arrays-uf-never never turn arrays into uninterpreted functions\n" // NOLINT(*)
1130  " --arrays-uf-always always turn arrays into uninterpreted functions\n" // NOLINT(*)
1131  "\n"
1132  "Other options:\n"
1133  " --version show version and exit\n"
1138  HELP_FLUSH
1139  " --verbosity # verbosity level\n"
1141  "\n";
1142  // clang-format on
1143 }
cmdlinet::args
argst args
Definition: cmdline.h:91
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:201
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:1291
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:168
PARSE_OPTIONS_GOTO_CHECK
#define PARSE_OPTIONS_GOTO_CHECK(cmdline, options)
Definition: goto_check.h:61
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:273
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:906
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:769
remove_skip
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:85
goto_convert_functionst::convert_function
void convert_function(const irep_idt &identifier, goto_functionst::goto_functiont &result)
Definition: goto_convert_functions.cpp:142
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:1522
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:368
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:723
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:2231
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:1007
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:299
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:345
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: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:1000
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:44
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:697
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:857
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:368
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:1402
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:26
irept::is_nil
bool is_nil() const
Definition: irep.h:398
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 type (see type), function body (see body),...
Definition: goto_function.h:28
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:422
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:1302
jbmc_parse_optionst::help
virtual void help() override
display command line help
Definition: jbmc_parse_options.cpp:1045
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:798
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:687
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:256
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:315
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:281
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:78
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:874
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