cprover
Loading...
Searching...
No Matches
jbmc_parse_options.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: JBMC Command Line Option Processing
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#include "jbmc_parse_options.h"
13
14#include <util/config.h>
15#include <util/exit_codes.h>
16#include <util/help_formatter.h>
17#include <util/invariant.h>
18#include <util/version.h>
19#include <util/xml.h>
20
33
57#include <langapi/language.h>
58#include <langapi/mode.h>
61
62#include <cstdlib> // exit()
63#include <iostream>
64#include <memory>
65
76
78 int argc,
79 const char **argv,
80 const std::string &extra_options)
82 JBMC_OPTIONS + extra_options,
83 argc,
84 argv,
85 std::string("JBMC ") + CBMC_VERSION)
86{
89}
90
92{
93 // Default true
94 options.set_option("assertions", true);
95 options.set_option("assumptions", true);
96 options.set_option("built-in-assertions", true);
97 options.set_option("propagation", true);
98 options.set_option("refine-strings", true);
99 options.set_option("simple-slice", true);
100 options.set_option("simplify", true);
101 options.set_option("show-goto-symex-steps", false);
102
103 // Other default
104 options.set_option("arrays-uf", "auto");
105 options.set_option("depth", UINT32_MAX);
106}
107
109{
110 if(config.set(cmdline))
111 {
112 usage_error();
113 exit(1); // should contemplate EX_USAGE from sysexits.h
114 }
115
117
118 if(cmdline.isset("function"))
119 options.set_option("function", cmdline.get_value("function"));
120
123
124 if(cmdline.isset("max-field-sensitivity-array-size"))
125 {
126 options.set_option(
127 "max-field-sensitivity-array-size",
128 cmdline.get_value("max-field-sensitivity-array-size"));
129 }
130
131 if(cmdline.isset("no-array-field-sensitivity"))
132 {
133 if(cmdline.isset("max-field-sensitivity-array-size"))
134 {
135 log.error()
136 << "--no-array-field-sensitivity and --max-field-sensitivity-array-size"
137 << " must not be given together" << messaget::eom;
139 }
140 options.set_option("no-array-field-sensitivity", true);
141 }
142
143 if(cmdline.isset("show-symex-strategies"))
144 {
147 }
148
150
151 if(cmdline.isset("program-only"))
152 options.set_option("program-only", true);
153
154 if(cmdline.isset("show-vcc"))
155 options.set_option("show-vcc", true);
156
157 if(cmdline.isset("nondet-static"))
158 options.set_option("nondet-static", true);
159
160 if(cmdline.isset("no-simplify"))
161 options.set_option("simplify", false);
162
163 if(cmdline.isset("stop-on-fail") ||
164 cmdline.isset("dimacs") ||
165 cmdline.isset("outfile"))
166 options.set_option("stop-on-fail", true);
167
168 if(
169 cmdline.isset("trace") || cmdline.isset("compact-trace") ||
170 cmdline.isset("stack-trace") || cmdline.isset("stop-on-fail") ||
172 !cmdline.isset("cover")))
173 {
174 options.set_option("trace", true);
175 }
176
177 if(cmdline.isset("validate-trace"))
178 {
179 options.set_option("validate-trace", true);
180 options.set_option("trace", true);
181 }
182
183 if(cmdline.isset("localize-faults"))
184 options.set_option("localize-faults", true);
185
186 if(cmdline.isset("symex-complexity-limit"))
187 {
188 options.set_option(
189 "symex-complexity-limit", cmdline.get_value("symex-complexity-limit"));
190 log.warning() << "**** WARNING: Complexity-limited analysis may yield "
191 "unsound verification results"
192 << messaget::eom;
193 }
194
195 if(cmdline.isset("symex-complexity-failed-child-loops-limit"))
196 {
197 options.set_option(
198 "symex-complexity-failed-child-loops-limit",
199 cmdline.get_value("symex-complexity-failed-child-loops-limit"));
200 if(!cmdline.isset("symex-complexity-limit"))
201 {
202 log.warning() << "**** WARNING: Complexity-limited analysis may yield "
203 "unsound verification results"
204 << messaget::eom;
205 }
206 }
207
208 // generate unwinding assertions
209 options.set_option(
210 "unwinding-assertions",
211 cmdline.isset("unwinding-assertions") ||
212 !cmdline.isset("no-unwinding-assertions"));
213
214 if(cmdline.isset("unwind"))
215 {
216 options.set_option("unwind", cmdline.get_value("unwind"));
217 if(!options.get_bool_option("unwinding-assertions"))
218 {
219 log.warning() << "**** WARNING: Use --unwinding-assertions to obtain "
220 "sound verification results"
221 << messaget::eom;
222 }
223 }
224
225 if(cmdline.isset("depth"))
226 {
227 options.set_option("depth", cmdline.get_value("depth"));
228 log.warning()
229 << "**** WARNING: Depth-bounded analysis may yield unsound verification "
230 "results"
231 << messaget::eom;
232 }
233
234 if(cmdline.isset("unwindset"))
235 {
236 options.set_option(
237 "unwindset", cmdline.get_comma_separated_values("unwindset"));
238 if(!options.get_bool_option("unwinding-assertions"))
239 {
240 log.warning() << "**** WARNING: Use --unwinding-assertions to obtain "
241 "sound verification results"
242 << messaget::eom;
243 }
244 }
245
246 // constant propagation
247 if(cmdline.isset("no-propagation"))
248 options.set_option("propagation", false);
249
250 // transform self loops to assumptions
251 options.set_option(
252 "self-loops-to-assumptions",
253 !cmdline.isset("no-self-loops-to-assumptions"));
254
255 // unwind loops in java enum static initialization
256 if(cmdline.isset("java-unwind-enum-static"))
257 options.set_option("java-unwind-enum-static", true);
258
259 // check assertions
260 if(cmdline.isset("no-assertions"))
261 options.set_option("assertions", false);
262
263 // use assumptions
264 if(cmdline.isset("no-assumptions"))
265 options.set_option("assumptions", false);
266
267 // generate unwinding assumptions otherwise
268 if(cmdline.isset("partial-loops"))
269 {
270 options.set_option("partial-loops", true);
271 log.warning()
272 << "**** WARNING: --partial-loops may yield unsound verification results"
273 << messaget::eom;
274 }
275
276 // remove unused equations
277 options.set_option(
278 "slice-formula",
279 cmdline.isset("slice-formula"));
280
281 if(cmdline.isset("arrays-uf-always"))
282 options.set_option("arrays-uf", "always");
283 else if(cmdline.isset("arrays-uf-never"))
284 options.set_option("arrays-uf", "never");
285
286 if(cmdline.isset("no-refine-strings"))
287 options.set_option("refine-strings", false);
288
289 if(cmdline.isset("string-printable") && cmdline.isset("no-refine-strings"))
290 {
292 "cannot use --string-printable with --no-refine-strings",
293 "--string-printable");
294 }
295
296 if(cmdline.isset("string-input-value") && cmdline.isset("no-refine-strings"))
297 {
299 "cannot use --string-input-value with --no-refine-strings",
300 "--string-input-value");
301 }
302
303 if(
304 cmdline.isset("no-refine-strings") &&
305 cmdline.isset("max-nondet-string-length"))
306 {
308 "cannot use --max-nondet-string-length with --no-refine-strings",
309 "--max-nondet-string-length");
310 }
311
312 if(cmdline.isset("graphml-witness"))
313 {
314 options.set_option("graphml-witness", cmdline.get_value("graphml-witness"));
315 options.set_option("stop-on-fail", true);
316 options.set_option("trace", true);
317 }
318
319 if(cmdline.isset("symex-coverage-report"))
320 options.set_option(
321 "symex-coverage-report",
322 cmdline.get_value("symex-coverage-report"));
323
324 if(cmdline.isset("validate-ssa-equation"))
325 {
326 options.set_option("validate-ssa-equation", true);
327 }
328
329 if(cmdline.isset("validate-goto-model"))
330 {
331 options.set_option("validate-goto-model", true);
332 }
333
334 options.set_option(
335 "symex-cache-dereferences", cmdline.isset("symex-cache-dereferences"));
336
338
339 if(cmdline.isset("symex-driven-lazy-loading"))
340 {
341 options.set_option("symex-driven-lazy-loading", true);
342 for(const char *opt :
343 { "nondet-static",
344 "full-slice",
345 "reachability-slice",
346 "reachability-slice-fb" })
347 {
348 if(cmdline.isset(opt))
349 {
350 throw std::string("Option ") + opt +
351 " can't be used with --symex-driven-lazy-loading";
352 }
353 }
354 }
355
356 // The 'allow-pointer-unsoundness' option prevents symex from throwing an
357 // exception when it encounters pointers that are shared across threads.
358 // This is unsound but given that pointers are ubiquitous in java this check
359 // must be disabled in order to support the analysis of multithreaded java
360 // code.
361 if(cmdline.isset("java-threading"))
362 options.set_option("allow-pointer-unsoundness", true);
363
364 if(cmdline.isset("show-goto-symex-steps"))
365 options.set_option("show-goto-symex-steps", true);
366
367 if(cmdline.isset("smt1"))
368 {
369 log.error() << "--smt1 is no longer supported" << messaget::eom;
371 }
372
374}
375
378{
379 if(cmdline.isset("version"))
380 {
381 std::cout << CBMC_VERSION << '\n';
383 }
384
387
388 //
389 // command line options
390 //
391
392 optionst options;
394
396
397 // output the options
398 switch(ui_message_handler.get_ui())
399 {
402 log.debug(), [&options](messaget::mstreamt &debug_stream) {
403 debug_stream << "\nOptions: \n";
404 options.output(debug_stream);
405 debug_stream << messaget::eom;
406 });
407 break;
409 {
410 json_objectt json_options{{"options", options.to_json()}};
411 log.debug() << json_options;
412 break;
413 }
415 log.debug() << options.to_xml();
416 break;
417 }
418
421
422 if(!((cmdline.isset("jar") && cmdline.args.empty()) ||
423 (cmdline.isset("gb") && cmdline.args.empty()) ||
424 (!cmdline.isset("jar") && !cmdline.isset("gb") &&
425 (cmdline.args.size() == 1))))
426 {
427 log.error() << "Please give exactly one class name, "
428 << "and/or use -jar jarfile or --gb goto-binary"
429 << messaget::eom;
431 }
432
433 if((cmdline.args.size() == 1) && !cmdline.isset("show-parse-tree"))
434 {
435 std::string main_class = cmdline.args[0];
436 // `java` accepts slashes and dots as package separators
437 std::replace(main_class.begin(), main_class.end(), '/', '.');
438 config.java.main_class = main_class;
439 cmdline.args.pop_back();
440 }
441
442 if(cmdline.isset("jar"))
443 {
444 cmdline.args.push_back(cmdline.get_value("jar"));
445 }
446
447 if(cmdline.isset("gb"))
448 {
449 cmdline.args.push_back(cmdline.get_value("gb"));
450 }
451
452 // Shows the parse tree of the main class
453 if(cmdline.isset("show-parse-tree"))
454 {
455 std::unique_ptr<languaget> language = get_language_from_mode(ID_java);
456 CHECK_RETURN(language != nullptr);
457 language->set_language_options(options, ui_message_handler);
458
459 log.status() << "Parsing ..." << messaget::eom;
460
461 std::istringstream unused;
462 if(language.get()->parse(unused, "", ui_message_handler))
463 {
464 log.error() << "PARSING ERROR" << messaget::eom;
466 }
467
468 language->show_parse(std::cout, ui_message_handler);
470 }
471
472 object_factory_params.set(options);
473
475 options.get_bool_option("java-assume-inputs-non-null");
476
477 std::unique_ptr<abstract_goto_modelt> goto_model_ptr;
478 int get_goto_program_ret = get_goto_program(goto_model_ptr, options);
479 if(get_goto_program_ret != -1)
480 return get_goto_program_ret;
481
482 if(
483 options.get_bool_option("program-only") ||
484 options.get_bool_option("show-vcc") ||
485 (options.get_bool_option("symex-driven-lazy-loading") &&
486 (cmdline.isset("show-symbol-table") || cmdline.isset("list-symbols") ||
487 cmdline.isset("show-goto-functions") ||
488 cmdline.isset("list-goto-functions") ||
489 cmdline.isset("show-properties") || cmdline.isset("show-loops"))))
490 {
491 if(options.get_bool_option("paths"))
492 {
494 options, ui_message_handler, *goto_model_ptr);
495 (void)verifier();
496 }
497 else
498 {
500 options, ui_message_handler, *goto_model_ptr);
501 (void)verifier();
502 }
503
504 if(options.get_bool_option("symex-driven-lazy-loading"))
505 {
506 // We can only output these after goto-symex has run.
507 (void)show_loaded_symbols(*goto_model_ptr);
508 (void)show_loaded_functions(*goto_model_ptr);
509 }
510
512 }
513
514 if(
515 options.get_bool_option("dimacs") || !options.get_option("outfile").empty())
516 {
517 if(options.get_bool_option("paths"))
518 {
520 options, ui_message_handler, *goto_model_ptr);
521 (void)verifier();
522 }
523 else
524 {
526 options, ui_message_handler, *goto_model_ptr);
527 (void)verifier();
528 }
529
531 }
532
533 std::unique_ptr<goto_verifiert> verifier = nullptr;
534
535 if(
536 options.get_bool_option("stop-on-fail") && options.get_bool_option("paths"))
537 {
538 verifier =
539 std::make_unique<stop_on_fail_verifiert<java_single_path_symex_checkert>>(
540 options, ui_message_handler, *goto_model_ptr);
541 }
542 else if(
543 options.get_bool_option("stop-on-fail") &&
544 !options.get_bool_option("paths"))
545 {
546 if(options.get_bool_option("localize-faults"))
547 {
548 verifier =
551 options, ui_message_handler, *goto_model_ptr);
552 }
553 else
554 {
555 verifier = std::make_unique<
557 options, ui_message_handler, *goto_model_ptr);
558 }
559 }
560 else if(
561 !options.get_bool_option("stop-on-fail") &&
562 options.get_bool_option("paths"))
563 {
564 verifier = std::make_unique<all_properties_verifier_with_trace_storaget<
566 options, ui_message_handler, *goto_model_ptr);
567 }
568 else if(
569 !options.get_bool_option("stop-on-fail") &&
570 !options.get_bool_option("paths"))
571 {
572 if(options.get_bool_option("localize-faults"))
573 {
574 verifier =
577 options, ui_message_handler, *goto_model_ptr);
578 }
579 else
580 {
581 verifier = std::make_unique<all_properties_verifier_with_trace_storaget<
583 options, ui_message_handler, *goto_model_ptr);
584 }
585 }
586 else
587 {
589 }
590
591 const resultt result = (*verifier)();
592 verifier->report();
593 return result_to_exit_code(result);
594}
595
597 std::unique_ptr<abstract_goto_modelt> &goto_model_ptr,
598 const optionst &options)
599{
600 if(options.is_set("context-include") || options.is_set("context-exclude"))
601 method_context = get_context(options);
602 lazy_goto_modelt lazy_goto_model =
604 lazy_goto_model.initialize(cmdline.args, options);
605
607 std::make_unique<class_hierarchyt>(lazy_goto_model.symbol_table);
608
609 // Show the class hierarchy
610 if(cmdline.isset("show-class-hierarchy"))
611 {
614 }
615
616 // Add failed symbols for any symbol created prior to loading any
617 // particular function:
618 add_failed_symbols(lazy_goto_model.symbol_table);
619
620 if(!options.get_bool_option("symex-driven-lazy-loading"))
621 {
622 log.status() << "Generating GOTO Program" << messaget::eom;
623 lazy_goto_model.load_all_functions();
624
625 // show symbol table or list symbols
626 if(show_loaded_symbols(lazy_goto_model))
628
629 // Move the model out of the local lazy_goto_model
630 // and into the caller's goto_model
632 std::move(lazy_goto_model));
633 if(goto_model_ptr == nullptr)
635
636 goto_modelt &goto_model = dynamic_cast<goto_modelt &>(*goto_model_ptr);
637
638 if(cmdline.isset("validate-goto-model"))
639 {
640 goto_model.validate();
641 }
642
643 if(show_loaded_functions(goto_model))
645
646 if(cmdline.isset("property"))
647 ::set_properties(goto_model, cmdline.get_values("property"));
648 }
649 else
650 {
651 // The precise wording of this error matches goto-symex's complaint when no
652 // __CPROVER_start exists (if we just go ahead and run it anyway it will
653 // trip an invariant when it tries to load it)
655 {
656 log.error() << "the program has no entry point" << messaget::eom;
658 }
659
660 if(cmdline.isset("validate-goto-model"))
661 {
662 lazy_goto_model.validate();
663 }
664
665 goto_model_ptr =
666 std::make_unique<lazy_goto_modelt>(std::move(lazy_goto_model));
667 }
668
670
671 return -1; // no error, continue
672}
673
675 goto_model_functiont &function,
676 const abstract_goto_modelt &model,
677 const optionst &options)
678{
679 journalling_symbol_tablet &symbol_table = function.get_symbol_table();
680 namespacet ns(symbol_table);
681 goto_functionst::goto_functiont &goto_function = function.get_goto_function();
682
683 bool using_symex_driven_loading =
684 options.get_bool_option("symex-driven-lazy-loading");
685
686 // Removal of RTTI inspection:
688 function.get_function_id(),
689 goto_function,
690 symbol_table,
693 // Java virtual functions -> explicit dispatch tables:
695
696 auto function_is_stub = [&symbol_table, &model](const irep_idt &id) {
697 return symbol_table.lookup_ref(id).value.is_nil() &&
698 !model.can_produce_function(id);
699 };
700
701 remove_returns(function, function_is_stub);
702
703 replace_java_nondet(function);
704
705 // Similar removal of java nondet statements:
707
708 if(using_symex_driven_loading)
709 {
710 // remove exceptions
711 // If using symex-driven function loading we need to do this now so that
712 // symex doesn't have to cope with exception-handling constructs; however
713 // the results are slightly worse than running it in whole-program mode
714 // (e.g. dead catch sites will be retained)
716 function.get_function_id(),
717 goto_function.body,
718 symbol_table,
719 *class_hierarchy.get(),
721 }
722
723 transform_assertions_assumptions(options, function.get_goto_function().body);
724
725 // Replace Java new side effects
727 function.get_function_id(),
728 goto_function,
729 symbol_table,
731
732 // checks don't know about adjusted float expressions
733 adjust_float_expressions(goto_function, ns);
734
735 // add failed symbols for anything created relating to this particular
736 // function (note this means subsequent passes mustn't create more!):
738 symbol_table.get_inserted();
739 for(const irep_idt &new_symbol_name : new_symbols)
740 {
742 symbol_table.lookup_ref(new_symbol_name), symbol_table);
743 }
744
745 // If using symex-driven function loading we must label the assertions
746 // now so symex sees its targets; otherwise we leave this until
747 // process_goto_functions, as we haven't run remove_exceptions yet, and that
748 // pass alters the CFG.
749 if(using_symex_driven_loading)
750 {
751 // label the assertions
752 label_properties(function.get_function_id(), goto_function.body);
753
754 goto_function.body.update();
755 function.compute_location_numbers();
756 goto_function.body.compute_loop_numbers();
757 }
758}
759
761 const abstract_goto_modelt &goto_model)
762{
763 if(cmdline.isset("show-symbol-table"))
764 {
766 return true;
767 }
768 else if(cmdline.isset("list-symbols"))
769 {
771 return true;
772 }
773
774 return false;
775}
776
778 const abstract_goto_modelt &goto_model)
779{
780 if(cmdline.isset("show-loops"))
781 {
783 return true;
784 }
785
786 if(
787 cmdline.isset("show-goto-functions") ||
788 cmdline.isset("list-goto-functions"))
789 {
790 namespacet ns(goto_model.get_symbol_table());
792 ns,
794 goto_model.get_goto_functions(),
795 cmdline.isset("list-goto-functions"));
796 return true;
797 }
798
799 if(cmdline.isset("show-properties"))
800 {
801 namespacet ns(goto_model.get_symbol_table());
803 return true;
804 }
805
806 return false;
807}
808
810 goto_modelt &goto_model,
811 const optionst &options)
812{
813 log.status() << "Running GOTO functions transformation passes"
814 << messaget::eom;
815
816 bool using_symex_driven_loading =
817 options.get_bool_option("symex-driven-lazy-loading");
818
819 // When using symex-driven lazy loading, *all* relevant processing is done
820 // during process_goto_function, so we have nothing to do here.
821 if(using_symex_driven_loading)
822 return false;
823
824 // remove catch and throw
826
827 // instrument library preconditions
828 instrument_preconditions(goto_model);
829
830 // ignore default/user-specified initialization
831 // of variables with static lifetime
832 if(cmdline.isset("nondet-static"))
833 {
834 log.status() << "Adding nondeterministic initialization "
835 "of static/global variables"
836 << messaget::eom;
837 nondet_static(goto_model);
838 }
839
840 // recalculate numbers, etc.
841 goto_model.goto_functions.update();
842
843 if(cmdline.isset("drop-unused-functions"))
844 {
845 // Entry point will have been set before and function pointers removed
846 log.status() << "Removing unused functions" << messaget::eom;
848 }
849
850 // remove skips such that trivial GOTOs are deleted
851 remove_skip(goto_model);
852
853 // label the assertions
854 // This must be done after adding assertions and
855 // before using the argument of the "property" option.
856 // Do not re-label after using the property slicer because
857 // this would cause the property identifiers to change.
858 label_properties(goto_model);
859
860 // reachability slice?
861 if(cmdline.isset("reachability-slice-fb"))
862 {
863 if(cmdline.isset("reachability-slice"))
864 {
865 log.error() << "--reachability-slice and --reachability-slice-fb "
866 << "must not be given together" << messaget::eom;
867 return true;
868 }
869
870 log.status() << "Performing a forwards-backwards reachability slice"
871 << messaget::eom;
872 if(cmdline.isset("property"))
873 {
875 goto_model, cmdline.get_values("property"), true, ui_message_handler);
876 }
877 else
878 reachability_slicer(goto_model, true, ui_message_handler);
879 }
880
881 if(cmdline.isset("reachability-slice"))
882 {
883 log.status() << "Performing a reachability slice" << messaget::eom;
884 if(cmdline.isset("property"))
885 {
887 goto_model, cmdline.get_values("property"), ui_message_handler);
888 }
889 else
891 }
892
893 // full slice?
894 if(cmdline.isset("full-slice"))
895 {
896 log.warning() << "**** WARNING: Experimental option --full-slice, "
897 << "analysis results may be unsound. See "
898 << "https://github.com/diffblue/cbmc/issues/260"
899 << messaget::eom;
900 log.status() << "Performing a full slice" << messaget::eom;
901 if(cmdline.isset("property"))
903 goto_model, cmdline.get_values("property"), ui_message_handler);
904 else
905 full_slicer(goto_model, ui_message_handler);
906 }
907
908 // remove any skips introduced
909 remove_skip(goto_model);
910
911 return false;
912}
913
915{
916 static const irep_idt initialize_id = INITIALIZE_FUNCTION;
917
918 return name != goto_functionst::entry_point() && name != initialize_id;
919}
920
922 const irep_idt &function_name,
923 symbol_table_baset &symbol_table,
924 goto_functiont &function,
925 bool body_available)
926{
927 // Provide a simple stub implementation for any function we don't have a
928 // bytecode implementation for:
929
930 if(
931 body_available &&
932 (!method_context || (*method_context)(id2string(function_name))))
933 return false;
934
935 if(!can_generate_function_body(function_name))
936 return false;
937
938 if(symbol_table.lookup_ref(function_name).mode == ID_java)
939 {
941 function_name,
942 symbol_table,
946
947 goto_convert_functionst converter(symbol_table, ui_message_handler);
948 converter.convert_function(function_name, function);
949
950 return true;
951 }
952 else
953 {
954 return false;
955 }
956}
957
960{
961 // clang-format off
962 std::cout << '\n' << banner_string("JBMC", CBMC_VERSION) << '\n'
963 << align_center_with_border("Copyright (C) 2001-2018") << '\n'
964 << align_center_with_border("Daniel Kroening, Edmund Clarke") << '\n' // NOLINT(*)
965 << align_center_with_border("Carnegie Mellon University, Computer Science Department") << '\n' // NOLINT(*)
966 << align_center_with_border("kroening@kroening.com") << '\n';
967
968 std::cout << help_formatter(
969 "\n"
970 "Usage: \tPurpose:\n"
971 "\n"
972 " {bjbmc} [{y-?}] [{y-h}] [{y--help}] \t show this help\n"
973 " {bjbmc}\n"
975 " {bjbmc}\n"
977 " {bjbmc}\n"
979 " {bjbmc}\n"
981 "\n"
984 "\n"
985 "Analysis options:\n"
987 " {y--symex-coverage-report} {uf} \t generate a Cobertura XML coverage"
988 " report in {uf}\n"
989 " {y--property} {uid} \t only check one specific property\n"
990 " {y--trace} \t give a counterexample trace for failed properties\n"
991 " {y--stop-on-fail} \t stop analysis once a failed property is detected"
992 " (implies {y--trace})\n"
993 " {y--localize-faults} \t localize faults (experimental)\n"
995 "\n"
996 "Platform options:\n"
998 "\n"
999 "Program representations:\n"
1000 " {y--show-parse-tree} \t show parse tree\n"
1001 " {y--show-symbol-table} \t show loaded symbol table\n"
1002 " {y--list-symbols} \t list symbols with type information\n"
1004 " {y--drop-unused-functions} \t drop functions trivially unreachable"
1005 " from main function\n"
1007 "\n"
1008 "Program instrumentation options:\n"
1009 " {y--no-assertions} \t ignore user assertions\n"
1010 " {y--no-assumptions} \t ignore user assumptions\n"
1011 " {y--mm} {uMM} \t memory consistency model for concurrent programs\n"
1013 " {y--full-slice} \t run full slicer (experimental)\n"
1014 "\n"
1015 "Java Bytecode frontend options:\n"
1017 // This one is handled by jbmc_parse_options not by the Java frontend,
1018 // hence its presence here:
1019 " {y--java-threading} \t enable java multi-threading support"
1020 " (experimental)\n"
1021 " {y--java-unwind-enum-static} \t unwind loops in static initialization of"
1022 " enums\n"
1023 " {y--symex-driven-lazy-loading} \t only load functions when first entered"
1024 " by symbolic execution. Note that {y--show-symbol-table},"
1025 " {y--show-goto-functions}, {y--show-properties} output will be restricted"
1026 " to loaded methods in this case, and only output after the symex phase.\n"
1027 "\n"
1028 "Semantic transformations:\n"
1029 " {y--nondet-static} \t add nondeterministic initialization of variables"
1030 " with static lifetime\n"
1031 "\n"
1032 "BMC options:\n"
1033 HELP_BMC
1034 "\n"
1035 "Backend options:\n"
1039 " {y--arrays-uf-never} \t never turn arrays into uninterpreted functions\n"
1040 " {y--arrays-uf-always} \t always turn arrays into uninterpreted"
1041 " functions\n"
1042 "\n"
1043 "Other options:\n"
1044 " {y--version} \t show version and exit\n"
1050 " {y--verbosity} {u#} \t verbosity level\n"
1052 "\n");
1053 // clang-format on
1054}
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,...
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....
Pointer Dereferencing.
void adjust_float_expressions(exprt &expr, const exprt &rounding_mode)
Replaces arithmetic operations and typecasts involving floating point numbers with their equivalent f...
Symbolic Execution.
Goto Verifier for Verifying all Properties.
Goto verifier for verifying all properties that stores traces and localizes faults.
Goto verifier for verifying all properties that stores traces.
std::unique_ptr< languaget > new_ansi_c_language()
configt config
Definition config.cpp:25
#define HELP_BMC
Definition bmc_util.h:197
void show_class_hierarchy(const class_hierarchyt &hierarchy, ui_message_handlert &message_handler, bool children_only)
Output the class hierarchy.
#define HELP_SHOW_CLASS_HIERARCHY
Abstract interface to eager or lazy GOTO models.
virtual bool can_produce_function(const irep_idt &id) const =0
Determines if this model can produce a body for the given function.
virtual const symbol_tablet & get_symbol_table() const =0
Accessor to get the symbol table.
virtual const goto_functionst & get_goto_functions() const =0
Accessor to get a raw goto_functionst.
Requires an incremental goto checker that is a goto_trace_providert and fault_localization_providert.
std::string get_value(char option) const
Definition cmdline.cpp:48
virtual bool isset(char option) const
Definition cmdline.cpp:30
std::list< std::string > get_comma_separated_values(const char *option) const
Collect all occurrences of option option and split their values on each comma, merging them into a si...
Definition cmdline.cpp:121
argst args
Definition cmdline.h:151
const std::list< std::string > & get_values(const std::string &option) const
Definition cmdline.cpp:109
bool set(const cmdlinet &cmdline)
Definition config.cpp:860
std::string object_bits_info()
Definition config.cpp:1428
struct configt::javat java
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
void convert_function(const irep_idt &identifier, goto_functionst::goto_functiont &result)
::goto_functiont goto_functiont
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
Interface providing access to a single function in a GOTO model, plus its associated symbol table.
Definition goto_model.h:190
const irep_idt & get_function_id()
Get function id.
Definition goto_model.h:239
goto_functionst::goto_functiont & get_goto_function()
Get GOTO function.
Definition goto_model.h:232
void compute_location_numbers()
Re-number our goto_function.
Definition goto_model.h:216
journalling_symbol_tablet & get_symbol_table()
Get symbol table.
Definition goto_model.h:225
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:105
goto_functionst goto_functions
GOTO functions.
Definition goto_model.h:34
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
bool is_nil() const
Definition irep.h:368
bool show_loaded_functions(const abstract_goto_modelt &goto_model)
void get_command_line_options(optionst &)
bool can_generate_function_body(const irep_idt &name)
std::unique_ptr< class_hierarchyt > class_hierarchy
bool show_loaded_symbols(const abstract_goto_modelt &goto_model)
virtual int doit() override
invoke main modules
std::optional< prefix_filtert > method_context
See java_bytecode_languaget::method_context.
virtual void help() override
display command line help
void process_goto_function(goto_model_functiont &function, const abstract_goto_modelt &, const optionst &)
java_object_factory_parameterst object_factory_params
bool process_goto_functions(goto_modelt &goto_model, const optionst &options)
int get_goto_program(std::unique_ptr< abstract_goto_modelt > &goto_model, const optionst &)
jbmc_parse_optionst(int argc, const char **argv)
bool generate_function_body(const irep_idt &function_name, symbol_table_baset &symbol_table, goto_functiont &function, bool body_available)
static void set_default_options(optionst &)
Set the options that have default values.
A symbol table wrapper that records which entries have been updated/removedA caller can pass a journa...
const changesett & get_inserted() const
std::unordered_set< irep_idt > changesett
A GOTO model that produces function bodies on demand.
void load_all_functions() const
Eagerly loads all functions from the symbol table.
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...
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.
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.
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 ...
symbol_tablet & symbol_table
Reference to symbol_table in the internal goto_model.
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
mstreamt & error() const
Definition message.h:391
mstreamt & debug() const
Definition message.h:421
mstreamt & warning() const
Definition message.h:396
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
@ M_STATISTICS
Definition message.h:170
static eomt eom
Definition message.h:289
mstreamt & status() const
Definition message.h:406
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:94
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
json_objectt to_json() const
Returns the options as JSON key value pairs.
Definition options.cpp:93
bool get_bool_option(const std::string &option) const
Definition options.cpp:44
void set_option(const std::string &option, const bool value)
Definition options.cpp:28
const std::string get_option(const std::string &option) const
Definition options.cpp:67
xmlt to_xml() const
Returns the options in XML format.
Definition options.cpp:104
virtual void usage_error()
void log_version_and_architecture(const std::string &front_end)
Write version and system architecture to log.status().
ui_message_handlert ui_message_handler
Stops when the first failing property is found and localizes the fault Requires an incremental goto c...
Stops when the first failing property is found.
The symbol table base class interface.
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
exprt value
Initial value of symbol.
Definition symbol.h:34
irep_idt mode
Language mode.
Definition symbol.h:49
virtual uit get_ui() const
Definition ui_message.h:33
#define HELP_CONFIG_PLATFORM
Definition config.h:96
#define HELP_CONFIG_BACKEND
Definition config.h:126
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...
Convert side_effect_expr_nondett expressions using java_object_factory.
static void show_goto_functions(const goto_modelt &goto_model)
Document and give macros for the exit codes of CPROVER binaries.
#define CPROVER_EXIT_INTERNAL_ERROR
An error has been encountered during processing the requested analysis.
Definition exit_codes.h:45
#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
#define CPROVER_EXIT_PARSE_ERROR
An error during parsing of the input program.
Definition exit_codes.h:37
#define CPROVER_EXIT_USAGE_ERROR
A usage error is returned when the command line is invalid or conflicting.
Definition exit_codes.h:33
#define CPROVER_EXIT_SUCCESS
Success indicates the required analysis has been performed without error.
Definition exit_codes.h:16
void property_slicer(goto_functionst &goto_functions, const namespacet &ns, const std::list< std::string > &properties, message_handlert &message_handler)
void full_slicer(goto_functionst &goto_functions, const namespacet &ns, const slicing_criteriont &criterion, message_handlert &message_handler)
static void transform_assertions_assumptions(goto_programt &goto_program, bool enable_assertions, bool enable_built_in_assertions, bool enable_assumptions)
Checks for Errors in C and Java Programs.
Goto Programs with Functions.
#define PARSE_OPTIONS_GOTO_TRACE(cmdline, options)
Definition goto_trace.h:287
#define HELP_GOTO_TRACE
Definition goto_trace.h:279
Help Formatter.
static help_formattert help_formatter(const std::string &s)
void instrument_preconditions(const goto_modelt &goto_model, goto_programt &goto_program)
const std::string & id2string(const irep_idt &d)
Definition irep.h:44
void parse_java_language_options(const cmdlinet &cmd, optionst &options)
Parse options that are java bytecode specific.
std::unique_ptr< languaget > new_java_bytecode_language()
prefix_filtert get_context(const optionst &options)
#define HELP_JAVA_METHOD_NAME
#define JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP
#define HELP_JAVA_GOTO_BINARY
#define HELP_JAVA_CLASSPATH
#define HELP_JAVA_JAR
#define HELP_JAVA_CLASS_NAME
Goto Checker using Bounded Model Checking for Java.
Goto Checker using Bounded Model Checking for Java.
void parse_java_object_factory_options(const cmdlinet &cmdline, optionst &options)
Parse the java object factory parameters from a given command line.
Goto Checker using Single Path Symbolic Execution for Java.
Goto Checker using Single Path Symbolic Execution for Java.
#define HELP_JAVA_TRACE_VALIDATION
JBMC Command Line Option Processing.
#define JBMC_OPTIONS
void json_interface(cmdlinet &cmdline, message_handlert &message_handler)
Parses the JSON-formatted command line from stdin.
#define HELP_JSON_INTERFACE
Abstract interface to support a programming language.
#define HELP_FUNCTIONS
Definition language.h:34
Author: Diffblue Ltd.
void show_loop_ids(ui_message_handlert::uit ui, const goto_modelt &goto_model)
Definition loop_ids.cpp:21
Loop IDs.
std::unique_ptr< languaget > get_language_from_mode(const irep_idt &mode)
Get the language corresponding to the given mode.
Definition mode.cpp:51
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
STL namespace.
static void nondet_static(const namespacet &ns, goto_modelt &goto_model, const irep_idt &fct_name)
Nondeterministically initializes global scope variables in a goto-function.
Nondeterministically initializes global scope variables, except for constants (such as string literal...
std::string align_center_with_border(const std::string &text)
Utility for displaying help centered messages borderered by "* *".
std::string banner_string(const std::string &front_end, const std::string &version)
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.
std::string show_path_strategies()
suitable for displaying as a front-end help message
Storage of symbolic execution paths to resume.
int result_to_exit_code(resultt result)
resultt
The result of goto verifying.
Definition properties.h:45
void reachability_slicer(goto_modelt &goto_model, const bool include_forward_reachability, message_handlert &message_handler)
Perform reachability slicing on goto_model, with respect to the criterion given by all properties.
#define HELP_REACHABILITY_SLICER
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
Remove function exceptional returns.
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...
Remove Instance-of Operators.
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.
Remove Java New Operators.
void remove_returns(symbol_table_baset &symbol_table, goto_functionst &goto_functions)
removes returns
Replace function returns by assignments to global variables.
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Program Transformation.
void remove_unused_functions(goto_modelt &goto_model, message_handlert &message_handler)
Unused function removal.
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...
Functions for replacing virtual function call with a static function calls in functions,...
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.
Replace Java Nondet expressions.
void set_properties(goto_programt &goto_program, std::unordered_set< irep_idt > &property_set)
void label_properties(goto_modelt &goto_model)
Set the properties to check.
Show the goto functions.
#define HELP_SHOW_GOTO_FUNCTIONS
void show_properties(const namespacet &ns, const irep_idt &identifier, message_handlert &message_handler, ui_message_handlert::uit ui, const goto_programt &goto_program)
Show the properties.
#define HELP_SHOW_PROPERTIES
void show_symbol_table(const symbol_table_baset &symbol_table, ui_message_handlert &ui)
void show_symbol_table_brief(const symbol_table_baset &symbol_table, ui_message_handlert &ui)
Show the symbol table.
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)
Java simple opaque stub generation.
void parse_solver_options(const cmdlinet &cmdline, optionst &options)
Parse solver-related command-line parameters in cmdline and set corresponding values in options.
#define HELP_SOLVER
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:525
#define INITIALIZE_FUNCTION
Goto Verifier for stopping at the first failing property.
Goto Verifier for stopping at the first failing property and localizing the fault.
#define HELP_STRING_REFINEMENT
irep_idt main_class
Definition config.h:347
void set(const optionst &)
Assigns the parameters from given options.
#define HELP_TIMESTAMP
Definition timestamper.h:14
#define HELP_FLUSH
Definition ui_message.h:108
#define HELP_VALIDATE
const char * CBMC_VERSION
void xml_interface(cmdlinet &cmdline, message_handlert &message_handler)
Parse XML-formatted commandline options from stdin.
#define HELP_XML_INTERFACE