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/make_unique.h>
19#include <util/version.h>
20#include <util/xml.h>
21
35
58#include <langapi/language.h>
59#include <langapi/mode.h>
62
63#include <cstdlib> // exit()
64#include <iostream>
65#include <memory>
66
77
79 int argc,
80 const char **argv,
81 const std::string &extra_options)
84 argc,
85 argv,
86 std::string("JBMC ") + CBMC_VERSION)
87{
90}
91
93{
94 // Default true
95 options.set_option("assertions", true);
96 options.set_option("assumptions", true);
97 options.set_option("built-in-assertions", true);
98 options.set_option("propagation", true);
99 options.set_option("refine-strings", true);
100 options.set_option("simple-slice", true);
101 options.set_option("simplify", true);
102 options.set_option("show-goto-symex-steps", false);
103
104 // Other default
105 options.set_option("arrays-uf", "auto");
106 options.set_option("depth", UINT32_MAX);
107}
108
110{
111 if(config.set(cmdline))
112 {
113 usage_error();
114 exit(1); // should contemplate EX_USAGE from sysexits.h
115 }
116
118
119 if(cmdline.isset("function"))
120 options.set_option("function", cmdline.get_value("function"));
121
124
125 if(cmdline.isset("max-field-sensitivity-array-size"))
126 {
127 options.set_option(
128 "max-field-sensitivity-array-size",
129 cmdline.get_value("max-field-sensitivity-array-size"));
130 }
131
132 if(cmdline.isset("no-array-field-sensitivity"))
133 {
134 if(cmdline.isset("max-field-sensitivity-array-size"))
135 {
136 log.error()
137 << "--no-array-field-sensitivity and --max-field-sensitivity-array-size"
138 << " must not be given together" << messaget::eom;
140 }
141 options.set_option("no-array-field-sensitivity", true);
142 }
143
144 if(cmdline.isset("show-symex-strategies"))
145 {
148 }
149
151
152 if(cmdline.isset("program-only"))
153 options.set_option("program-only", true);
154
155 if(cmdline.isset("show-vcc"))
156 options.set_option("show-vcc", true);
157
158 if(cmdline.isset("nondet-static"))
159 options.set_option("nondet-static", true);
160
161 if(cmdline.isset("no-simplify"))
162 options.set_option("simplify", false);
163
164 if(cmdline.isset("stop-on-fail") ||
165 cmdline.isset("dimacs") ||
166 cmdline.isset("outfile"))
167 options.set_option("stop-on-fail", true);
168
169 if(
170 cmdline.isset("trace") || cmdline.isset("compact-trace") ||
171 cmdline.isset("stack-trace") || cmdline.isset("stop-on-fail") ||
173 !cmdline.isset("cover")))
174 {
175 options.set_option("trace", true);
176 }
177
178 if(cmdline.isset("validate-trace"))
179 {
180 options.set_option("validate-trace", true);
181 options.set_option("trace", true);
182 }
183
184 if(cmdline.isset("localize-faults"))
185 options.set_option("localize-faults", true);
186
187 if(cmdline.isset("symex-complexity-limit"))
188 {
189 options.set_option(
190 "symex-complexity-limit", cmdline.get_value("symex-complexity-limit"));
191 log.warning() << "**** WARNING: Complexity-limited analysis may yield "
192 "unsound verification results"
193 << messaget::eom;
194 }
195
196 if(cmdline.isset("symex-complexity-failed-child-loops-limit"))
197 {
198 options.set_option(
199 "symex-complexity-failed-child-loops-limit",
200 cmdline.get_value("symex-complexity-failed-child-loops-limit"));
201 if(!cmdline.isset("symex-complexity-limit"))
202 {
203 log.warning() << "**** WARNING: Complexity-limited analysis may yield "
204 "unsound verification results"
205 << messaget::eom;
206 }
207 }
208
209 if(cmdline.isset("unwind"))
210 {
211 options.set_option("unwind", cmdline.get_value("unwind"));
212 if(!cmdline.isset("unwinding-assertions"))
213 {
214 log.warning() << "**** WARNING: Use --unwinding-assertions to obtain "
215 "sound verification results"
216 << messaget::eom;
217 }
218 }
219
220 if(cmdline.isset("depth"))
221 {
222 options.set_option("depth", cmdline.get_value("depth"));
223 log.warning()
224 << "**** WARNING: Depth-bounded analysis may yield unsound verification "
225 "results"
226 << messaget::eom;
227 }
228
229 if(cmdline.isset("unwindset"))
230 {
231 options.set_option(
232 "unwindset", cmdline.get_comma_separated_values("unwindset"));
233 if(!cmdline.isset("unwinding-assertions"))
234 {
235 log.warning() << "**** WARNING: Use --unwinding-assertions to obtain "
236 "sound verification results"
237 << messaget::eom;
238 }
239 }
240
241 // constant propagation
242 if(cmdline.isset("no-propagation"))
243 options.set_option("propagation", false);
244
245 // transform self loops to assumptions
246 options.set_option(
247 "self-loops-to-assumptions",
248 !cmdline.isset("no-self-loops-to-assumptions"));
249
250 // unwind loops in java enum static initialization
251 if(cmdline.isset("java-unwind-enum-static"))
252 options.set_option("java-unwind-enum-static", true);
253
254 // check assertions
255 if(cmdline.isset("no-assertions"))
256 options.set_option("assertions", false);
257
258 // use assumptions
259 if(cmdline.isset("no-assumptions"))
260 options.set_option("assumptions", false);
261
262 // generate unwinding assertions
263 if(cmdline.isset("unwinding-assertions"))
264 options.set_option("unwinding-assertions", true);
265
266 // generate unwinding assumptions otherwise
267 if(cmdline.isset("partial-loops"))
268 {
269 options.set_option("partial-loops", true);
270 log.warning()
271 << "**** WARNING: --partial-loops may yield unsound verification results"
272 << messaget::eom;
273 }
274
275 // remove unused equations
276 options.set_option(
277 "slice-formula",
278 cmdline.isset("slice-formula"));
279
280 if(cmdline.isset("arrays-uf-always"))
281 options.set_option("arrays-uf", "always");
282 else if(cmdline.isset("arrays-uf-never"))
283 options.set_option("arrays-uf", "never");
284
285 if(cmdline.isset("no-refine-strings"))
286 options.set_option("refine-strings", false);
287
288 if(cmdline.isset("string-printable") && cmdline.isset("no-refine-strings"))
289 {
291 "cannot use --string-printable with --no-refine-strings",
292 "--string-printable");
293 }
294
295 if(cmdline.isset("string-input-value") && cmdline.isset("no-refine-strings"))
296 {
298 "cannot use --string-input-value with --no-refine-strings",
299 "--string-input-value");
300 }
301
302 if(
303 cmdline.isset("no-refine-strings") &&
304 cmdline.isset("max-nondet-string-length"))
305 {
307 "cannot use --max-nondet-string-length with --no-refine-strings",
308 "--max-nondet-string-length");
309 }
310
311 if(cmdline.isset("graphml-witness"))
312 {
313 options.set_option("graphml-witness", cmdline.get_value("graphml-witness"));
314 options.set_option("stop-on-fail", true);
315 options.set_option("trace", true);
316 }
317
318 if(cmdline.isset("symex-coverage-report"))
319 options.set_option(
320 "symex-coverage-report",
321 cmdline.get_value("symex-coverage-report"));
322
323 if(cmdline.isset("validate-ssa-equation"))
324 {
325 options.set_option("validate-ssa-equation", true);
326 }
327
328 if(cmdline.isset("validate-goto-model"))
329 {
330 options.set_option("validate-goto-model", true);
331 }
332
333 options.set_option(
334 "symex-cache-dereferences", cmdline.isset("symex-cache-dereferences"));
335
337
338 if(cmdline.isset("symex-driven-lazy-loading"))
339 {
340 options.set_option("symex-driven-lazy-loading", true);
341 for(const char *opt :
342 { "nondet-static",
343 "full-slice",
344 "reachability-slice",
345 "reachability-slice-fb" })
346 {
347 if(cmdline.isset(opt))
348 {
349 throw std::string("Option ") + opt +
350 " can't be used with --symex-driven-lazy-loading";
351 }
352 }
353 }
354
355 // The 'allow-pointer-unsoundness' option prevents symex from throwing an
356 // exception when it encounters pointers that are shared across threads.
357 // This is unsound but given that pointers are ubiquitous in java this check
358 // must be disabled in order to support the analysis of multithreaded java
359 // code.
360 if(cmdline.isset("java-threading"))
361 options.set_option("allow-pointer-unsoundness", true);
362
363 if(cmdline.isset("show-goto-symex-steps"))
364 options.set_option("show-goto-symex-steps", true);
365
366 if(cmdline.isset("smt1"))
367 {
368 log.error() << "--smt1 is no longer supported" << messaget::eom;
370 }
371
373}
374
377{
378 if(cmdline.isset("version"))
379 {
380 std::cout << CBMC_VERSION << '\n';
382 }
383
386
387 //
388 // command line options
389 //
390
391 optionst options;
393
395
396 // output the options
397 switch(ui_message_handler.get_ui())
398 {
401 log.debug(), [&options](messaget::mstreamt &debug_stream) {
402 debug_stream << "\nOptions: \n";
403 options.output(debug_stream);
404 debug_stream << messaget::eom;
405 });
406 break;
408 {
409 json_objectt json_options{{"options", options.to_json()}};
411 break;
412 }
414 log.debug() << options.to_xml();
415 break;
416 }
417
420
421 if(!((cmdline.isset("jar") && cmdline.args.empty()) ||
422 (cmdline.isset("gb") && cmdline.args.empty()) ||
423 (!cmdline.isset("jar") && !cmdline.isset("gb") &&
424 (cmdline.args.size() == 1))))
425 {
426 log.error() << "Please give exactly one class name, "
427 << "and/or use -jar jarfile or --gb goto-binary"
428 << messaget::eom;
430 }
431
432 if((cmdline.args.size() == 1) && !cmdline.isset("show-parse-tree"))
433 {
434 std::string main_class = cmdline.args[0];
435 // `java` accepts slashes and dots as package separators
436 std::replace(main_class.begin(), main_class.end(), '/', '.');
437 config.java.main_class = main_class;
438 cmdline.args.pop_back();
439 }
440
441 if(cmdline.isset("jar"))
442 {
443 cmdline.args.push_back(cmdline.get_value("jar"));
444 }
445
446 if(cmdline.isset("gb"))
447 {
448 cmdline.args.push_back(cmdline.get_value("gb"));
449 }
450
451 // Shows the parse tree of the main class
452 if(cmdline.isset("show-parse-tree"))
453 {
454 std::unique_ptr<languaget> language = get_language_from_mode(ID_java);
455 CHECK_RETURN(language != nullptr);
456 language->set_language_options(options);
457 language->set_message_handler(ui_message_handler);
458
459 log.status() << "Parsing ..." << messaget::eom;
460
461 if(static_cast<java_bytecode_languaget *>(language.get())->parse())
462 {
463 log.error() << "PARSING ERROR" << messaget::eom;
465 }
466
467 language->show_parse(std::cout);
469 }
470
471 object_factory_params.set(options);
472
474 options.get_bool_option("java-assume-inputs-non-null");
475
476 std::unique_ptr<abstract_goto_modelt> goto_model_ptr;
478 if(get_goto_program_ret != -1)
480
481 if(
482 options.get_bool_option("program-only") ||
483 options.get_bool_option("show-vcc") ||
484 (options.get_bool_option("symex-driven-lazy-loading") &&
485 (cmdline.isset("show-symbol-table") || cmdline.isset("list-symbols") ||
486 cmdline.isset("show-goto-functions") ||
487 cmdline.isset("list-goto-functions") ||
488 cmdline.isset("show-properties") || cmdline.isset("show-loops"))))
489 {
490 if(options.get_bool_option("paths"))
491 {
494 (void)verifier();
495 }
496 else
497 {
500 (void)verifier();
501 }
502
503 if(options.get_bool_option("symex-driven-lazy-loading"))
504 {
505 // We can only output these after goto-symex has run.
508 }
509
511 }
512
513 if(
514 options.get_bool_option("dimacs") || !options.get_option("outfile").empty())
515 {
516 if(options.get_bool_option("paths"))
517 {
520 (void)verifier();
521 }
522 else
523 {
526 (void)verifier();
527 }
528
530 }
531
532 std::unique_ptr<goto_verifiert> verifier = nullptr;
533
534 if(
535 options.get_bool_option("stop-on-fail") && options.get_bool_option("paths"))
536 {
537 verifier =
540 }
541 else if(
542 options.get_bool_option("stop-on-fail") &&
543 !options.get_bool_option("paths"))
544 {
545 if(options.get_bool_option("localize-faults"))
546 {
547 verifier =
551 }
552 else
553 {
557 }
558 }
559 else if(
560 !options.get_bool_option("stop-on-fail") &&
561 options.get_bool_option("paths"))
562 {
566 }
567 else if(
568 !options.get_bool_option("stop-on-fail") &&
569 !options.get_bool_option("paths"))
570 {
571 if(options.get_bool_option("localize-faults"))
572 {
573 verifier =
577 }
578 else
579 {
583 }
584 }
585 else
586 {
588 }
589
590 const resultt result = (*verifier)();
591 verifier->report();
592 return result_to_exit_code(result);
593}
594
596 std::unique_ptr<abstract_goto_modelt> &goto_model_ptr,
597 const optionst &options)
598{
599 if(options.is_set("context-include") || options.is_set("context-exclude"))
600 method_context = get_context(options);
604
607
608 // Show the class hierarchy
609 if(cmdline.isset("show-class-hierarchy"))
610 {
613 }
614
615 // Add failed symbols for any symbol created prior to loading any
616 // particular function:
618
619 if(!options.get_bool_option("symex-driven-lazy-loading"))
620 {
621 log.status() << "Generating GOTO Program" << messaget::eom;
622 lazy_goto_model.load_all_functions();
623
624 // show symbol table or list symbols
627
628 // Move the model out of the local lazy_goto_model
629 // and into the caller's goto_model
631 std::move(lazy_goto_model));
632 if(goto_model_ptr == nullptr)
634
635 goto_modelt &goto_model = dynamic_cast<goto_modelt &>(*goto_model_ptr);
636
637 if(cmdline.isset("validate-goto-model"))
638 {
639 goto_model.validate();
640 }
641
642 if(show_loaded_functions(goto_model))
644
645 if(cmdline.isset("property"))
646 ::set_properties(goto_model, cmdline.get_values("property"));
647 }
648 else
649 {
650 // The precise wording of this error matches goto-symex's complaint when no
651 // __CPROVER_start exists (if we just go ahead and run it anyway it will
652 // trip an invariant when it tries to load it)
653 if(!lazy_goto_model.symbol_table.has_symbol(goto_functionst::entry_point()))
654 {
655 log.error() << "the program has no entry point" << messaget::eom;
657 }
658
659 if(cmdline.isset("validate-goto-model"))
660 {
661 lazy_goto_model.validate();
662 }
663
666 }
667
669
670 return -1; // no error, continue
671}
672
674 goto_model_functiont &function,
675 const abstract_goto_modelt &model,
676 const optionst &options)
677{
678 journalling_symbol_tablet &symbol_table = function.get_symbol_table();
679 namespacet ns(symbol_table);
680 goto_functionst::goto_functiont &goto_function = function.get_goto_function();
681
683 options.get_bool_option("symex-driven-lazy-loading");
684
685 // Removal of RTTI inspection:
687 function.get_function_id(),
688 goto_function,
689 symbol_table,
692 // Java virtual functions -> explicit dispatch tables:
694
695 auto function_is_stub = [&symbol_table, &model](const irep_idt &id) {
696 return symbol_table.lookup_ref(id).value.is_nil() &&
697 !model.can_produce_function(id);
698 };
699
701
702 replace_java_nondet(function);
703
704 // Similar removal of java nondet statements:
706
708 {
709 // remove exceptions
710 // If using symex-driven function loading we need to do this now so that
711 // symex doesn't have to cope with exception-handling constructs; however
712 // the results are slightly worse than running it in whole-program mode
713 // (e.g. dead catch sites will be retained)
715 function.get_function_id(),
716 goto_function.body,
717 symbol_table,
718 *class_hierarchy.get(),
720 }
721
722 transform_assertions_assumptions(options, function.get_goto_function().body);
723
724 // Replace Java new side effects
726 function.get_function_id(),
727 goto_function,
728 symbol_table,
730
731 // checks don't know about adjusted float expressions
732 adjust_float_expressions(goto_function, ns);
733
734 // add failed symbols for anything created relating to this particular
735 // function (note this means subsequent passes mustn't create more!):
737 symbol_table.get_inserted();
739 {
741 symbol_table.lookup_ref(new_symbol_name), symbol_table);
742 }
743
744 // If using symex-driven function loading we must label the assertions
745 // now so symex sees its targets; otherwise we leave this until
746 // process_goto_functions, as we haven't run remove_exceptions yet, and that
747 // pass alters the CFG.
749 {
750 // label the assertions
751 label_properties(function.get_function_id(), goto_function.body);
752
753 goto_function.body.update();
754 function.compute_location_numbers();
755 goto_function.body.compute_loop_numbers();
756 }
757}
758
760 const abstract_goto_modelt &goto_model)
761{
762 if(cmdline.isset("show-symbol-table"))
763 {
765 return true;
766 }
767 else if(cmdline.isset("list-symbols"))
768 {
770 return true;
771 }
772
773 return false;
774}
775
777 const abstract_goto_modelt &goto_model)
778{
779 if(cmdline.isset("show-loops"))
780 {
782 return true;
783 }
784
785 if(
786 cmdline.isset("show-goto-functions") ||
787 cmdline.isset("list-goto-functions"))
788 {
789 namespacet ns(goto_model.get_symbol_table());
791 ns,
793 goto_model.get_goto_functions(),
794 cmdline.isset("list-goto-functions"));
795 return true;
796 }
797
798 if(cmdline.isset("show-properties"))
799 {
800 namespacet ns(goto_model.get_symbol_table());
802 return true;
803 }
804
805 return false;
806}
807
809 goto_modelt &goto_model,
810 const optionst &options)
811{
812 log.status() << "Running GOTO functions transformation passes"
813 << messaget::eom;
814
816 options.get_bool_option("symex-driven-lazy-loading");
817
818 // When using symex-driven lazy loading, *all* relevant processing is done
819 // during process_goto_function, so we have nothing to do here.
821 return false;
822
823 // remove catch and throw
825
826 // instrument library preconditions
827 instrument_preconditions(goto_model);
828
829 // ignore default/user-specified initialization
830 // of variables with static lifetime
831 if(cmdline.isset("nondet-static"))
832 {
833 log.status() << "Adding nondeterministic initialization "
834 "of static/global variables"
835 << messaget::eom;
836 nondet_static(goto_model);
837 }
838
839 // recalculate numbers, etc.
840 goto_model.goto_functions.update();
841
842 if(cmdline.isset("drop-unused-functions"))
843 {
844 // Entry point will have been set before and function pointers removed
845 log.status() << "Removing unused functions" << messaget::eom;
847 }
848
849 // remove skips such that trivial GOTOs are deleted
850 remove_skip(goto_model);
851
852 // label the assertions
853 // This must be done after adding assertions and
854 // before using the argument of the "property" option.
855 // Do not re-label after using the property slicer because
856 // this would cause the property identifiers to change.
857 label_properties(goto_model);
858
859 // reachability slice?
860 if(cmdline.isset("reachability-slice-fb"))
861 {
862 if(cmdline.isset("reachability-slice"))
863 {
864 log.error() << "--reachability-slice and --reachability-slice-fb "
865 << "must not be given together" << messaget::eom;
866 return true;
867 }
868
869 log.status() << "Performing a forwards-backwards reachability slice"
870 << messaget::eom;
871 if(cmdline.isset("property"))
872 {
874 goto_model, cmdline.get_values("property"), true, ui_message_handler);
875 }
876 else
877 reachability_slicer(goto_model, true, ui_message_handler);
878 }
879
880 if(cmdline.isset("reachability-slice"))
881 {
882 log.status() << "Performing a reachability slice" << messaget::eom;
883 if(cmdline.isset("property"))
884 {
886 goto_model, cmdline.get_values("property"), ui_message_handler);
887 }
888 else
890 }
891
892 // full slice?
893 if(cmdline.isset("full-slice"))
894 {
895 log.warning() << "**** WARNING: Experimental option --full-slice, "
896 << "analysis results may be unsound. See "
897 << "https://github.com/diffblue/cbmc/issues/260"
898 << messaget::eom;
899 log.status() << "Performing a full slice" << messaget::eom;
900 if(cmdline.isset("property"))
901 property_slicer(goto_model, cmdline.get_values("property"));
902 else
903 full_slicer(goto_model);
904 }
905
906 // remove any skips introduced
907 remove_skip(goto_model);
908
909 return false;
910}
911
918
920 const irep_idt &function_name,
921 symbol_table_baset &symbol_table,
922 goto_functiont &function,
923 bool body_available)
924{
925 // Provide a simple stub implementation for any function we don't have a
926 // bytecode implementation for:
927
928 if(
929 body_available &&
930 (!method_context || (*method_context)(id2string(function_name))))
931 return false;
932
933 if(!can_generate_function_body(function_name))
934 return false;
935
936 if(symbol_table.lookup_ref(function_name).mode == ID_java)
937 {
939 function_name,
940 symbol_table,
944
945 goto_convert_functionst converter(symbol_table, ui_message_handler);
946 converter.convert_function(function_name, function);
947
948 return true;
949 }
950 else
951 {
952 return false;
953 }
954}
955
958{
959 // clang-format off
960 std::cout << '\n' << banner_string("JBMC", CBMC_VERSION) << '\n'
961 << align_center_with_border("Copyright (C) 2001-2018") << '\n'
962 << align_center_with_border("Daniel Kroening, Edmund Clarke") << '\n' // NOLINT(*)
963 << align_center_with_border("Carnegie Mellon University, Computer Science Department") << '\n' // NOLINT(*)
964 << align_center_with_border("kroening@kroening.com") << '\n';
965
966 std::cout << help_formatter(
967 "\n"
968 "Usage: \tPurpose:\n"
969 "\n"
970 " {bjbmc} [{y-?}] [{y-h}] [{y--help}] \t show this help\n"
971 " {bjbmc}\n"
973 " {bjbmc}\n"
975 " {bjbmc}\n"
977 " {bjbmc}\n"
979 "\n"
982 "\n"
983 "Analysis options:\n"
985 " {y--symex-coverage-report} {uf} \t generate a Cobertura XML coverage"
986 " report in {uf}\n"
987 " {y--property} {uid} \t only check one specific property\n"
988 " {y--trace} \t give a counterexample trace for failed properties\n"
989 " {y--stop-on-fail} \t stop analysis once a failed property is detected"
990 " (implies {y--trace})\n"
991 " {y--localize-faults} \t localize faults (experimental)\n"
993 "\n"
994 "Platform options:\n"
996 "\n"
997 "Program representations:\n"
998 " {y--show-parse-tree} \t show parse tree\n"
999 " {y--show-symbol-table} \t show loaded symbol table\n"
1000 " {y--list-symbols} \t list symbols with type information\n"
1002 " {y--drop-unused-functions} \t drop functions trivially unreachable"
1003 " from main function\n"
1005 "\n"
1006 "Program instrumentation options:\n"
1007 " {y--no-assertions} \t ignore user assertions\n"
1008 " {y--no-assumptions} \t ignore user assumptions\n"
1009 " {y--mm} {uMM} \t memory consistency model for concurrent programs\n"
1011 " {y--full-slice} \t run full slicer (experimental)\n"
1012 "\n"
1013 "Java Bytecode frontend options:\n"
1015 // This one is handled by jbmc_parse_options not by the Java frontend,
1016 // hence its presence here:
1017 " {y--java-threading} \t enable java multi-threading support"
1018 " (experimental)\n"
1019 " {y--java-unwind-enum-static} \t unwind loops in static initialization of"
1020 " enums\n"
1021 " {y--symex-driven-lazy-loading} \t only load functions when first entered"
1022 " by symbolic execution. Note that {y--show-symbol-table},"
1023 " {y--show-goto-functions}, {y--show-properties} output will be restricted"
1024 " to loaded methods in this case, and only output after the symex phase.\n"
1025 "\n"
1026 "Semantic transformations:\n"
1027 " {y--nondet-static} \t add nondeterministic initialization of variables"
1028 " with static lifetime\n"
1029 "\n"
1030 "BMC options:\n"
1031 HELP_BMC
1032 "\n"
1033 "Backend options:\n"
1037 " {y--arrays-uf-never} \t never turn arrays into uninterpreted functions\n"
1038 " {y--arrays-uf-always} \t always turn arrays into uninterpreted"
1039 " functions\n"
1040 "\n"
1041 "Other options:\n"
1042 " {y--version} \t show version and exit\n"
1048 " {y--verbosity} {u#} \t verbosity level\n"
1050 "\n");
1051 // clang-format on
1052}
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.
virtual void initialize(const irep_idt &function_id, const goto_programt &goto_program)
Initialize all the abstract states for a single function.
Definition ai.cpp:194
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
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:145
const std::list< std::string > & get_values(const std::string &option) const
Definition cmdline.cpp:109
bool set(const cmdlinet &cmdline)
Definition config.cpp:798
std::string object_bits_info()
Definition config.cpp:1342
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:39
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 ...
virtual bool parse()
We set the main class (i.e. class to start the class loading analysis, see java_class_loadert) when w...
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
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)
optionalt< prefix_filtert > method_context
See java_bytecode_languaget::method_context.
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.
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...
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.
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:399
mstreamt & debug() const
Definition message.h:429
mstreamt & warning() const
Definition message.h:404
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:171
static eomt eom
Definition message.h:297
mstreamt & status() const
Definition message.h:414
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
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...
The symbol table base class interface.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
virtual uit get_ui() const
Definition ui_message.h:33
#define HELP_CONFIG_PLATFORM
Definition config.h:94
#define HELP_CONFIG_BACKEND
Definition config.h:123
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 full_slicer(goto_functionst &goto_functions, const namespacet &ns, const slicing_criteriont &criterion)
void property_slicer(goto_functionst &goto_functions, const namespacet &ns, const std::list< std::string > &properties)
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:47
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:33
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< T > util_make_unique(Ts &&... ts)
Definition make_unique.h:19
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_functionst &goto_functions, 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
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