diff --git a/regression/book-examples/free_safety/memory_safety.desc b/regression/book-examples/free_safety/memory_safety.desc index 6ebbbf11b..850a30fcd 100644 --- a/regression/book-examples/free_safety/memory_safety.desc +++ b/regression/book-examples/free_safety/memory_safety.desc @@ -1,6 +1,6 @@ CORE free_safety.c ---pointer-check --heap --inline +--pointer-check --heap ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/book-examples/free_safety/memory_safety_free_error.desc b/regression/book-examples/free_safety/memory_safety_free_error.desc index 69b710ddb..3813421a2 100644 --- a/regression/book-examples/free_safety/memory_safety_free_error.desc +++ b/regression/book-examples/free_safety/memory_safety_free_error.desc @@ -1,6 +1,6 @@ CORE free_safety.c ---pointer-check --heap --inline -DINVALID_FREE +--pointer-check --heap -DINVALID_FREE ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/book-examples/sll_min/assertions.desc b/regression/book-examples/sll_min/assertions.desc index b9285bd6f..ce1d5a281 100644 --- a/regression/book-examples/sll_min/assertions.desc +++ b/regression/book-examples/sll_min/assertions.desc @@ -1,6 +1,6 @@ CORE sll_min.c ---heap-values-refine --sympath --inline +--heap-values-refine ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/heap-data/calendar/test.desc b/regression/heap-data/calendar/test.desc index b48b4027a..b83f79c6e 100644 --- a/regression/heap-data/calendar/test.desc +++ b/regression/heap-data/calendar/test.desc @@ -1,6 +1,6 @@ CORE main.c ---heap-values-refine --sympath --inline +--heap-values-refine ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/heap-data/cart/test.desc b/regression/heap-data/cart/test.desc index b48b4027a..b83f79c6e 100644 --- a/regression/heap-data/cart/test.desc +++ b/regression/heap-data/cart/test.desc @@ -1,6 +1,6 @@ CORE main.c ---heap-values-refine --sympath --inline +--heap-values-refine ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/heap-data/hash_fun/test.desc b/regression/heap-data/hash_fun/test.desc index b48b4027a..b83f79c6e 100644 --- a/regression/heap-data/hash_fun/test.desc +++ b/regression/heap-data/hash_fun/test.desc @@ -1,6 +1,6 @@ CORE main.c ---heap-values-refine --sympath --inline +--heap-values-refine ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/heap-data/min_max/test.desc b/regression/heap-data/min_max/test.desc index b48b4027a..b83f79c6e 100644 --- a/regression/heap-data/min_max/test.desc +++ b/regression/heap-data/min_max/test.desc @@ -1,6 +1,6 @@ CORE main.c ---heap-values-refine --sympath --inline +--heap-values-refine ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/heap-data/packet_filter/test.desc b/regression/heap-data/packet_filter/test.desc index 2ed70fde0..0b918f142 100644 --- a/regression/heap-data/packet_filter/test.desc +++ b/regression/heap-data/packet_filter/test.desc @@ -1,6 +1,6 @@ THOROUGH main.c ---heap-values-refine --sympath --inline +--heap-values-refine ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/heap-data/process_queue/test.desc b/regression/heap-data/process_queue/test.desc index 2ed70fde0..0b918f142 100644 --- a/regression/heap-data/process_queue/test.desc +++ b/regression/heap-data/process_queue/test.desc @@ -1,6 +1,6 @@ THOROUGH main.c ---heap-values-refine --sympath --inline +--heap-values-refine ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/heap-data/quick_sort_split/test.desc b/regression/heap-data/quick_sort_split/test.desc index b48b4027a..b83f79c6e 100644 --- a/regression/heap-data/quick_sort_split/test.desc +++ b/regression/heap-data/quick_sort_split/test.desc @@ -1,6 +1,6 @@ CORE main.c ---heap-values-refine --sympath --inline +--heap-values-refine ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/heap-data/running_example/test.desc b/regression/heap-data/running_example/test.desc index b48b4027a..b83f79c6e 100644 --- a/regression/heap-data/running_example/test.desc +++ b/regression/heap-data/running_example/test.desc @@ -1,6 +1,6 @@ CORE main.c ---heap-values-refine --sympath --inline +--heap-values-refine ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/heap-data/running_example_assume/test.desc b/regression/heap-data/running_example_assume/test.desc index 253d82f29..0c55e707a 100644 --- a/regression/heap-data/running_example_assume/test.desc +++ b/regression/heap-data/running_example_assume/test.desc @@ -1,6 +1,6 @@ KNOWNBUG main.c ---heap-values-refine --sympath --inline +--heap-values-refine ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/heap-data/shared_mem1/test.desc b/regression/heap-data/shared_mem1/test.desc index b48b4027a..b83f79c6e 100644 --- a/regression/heap-data/shared_mem1/test.desc +++ b/regression/heap-data/shared_mem1/test.desc @@ -1,6 +1,6 @@ CORE main.c ---heap-values-refine --sympath --inline +--heap-values-refine ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/heap-data/shared_mem2/test.desc b/regression/heap-data/shared_mem2/test.desc index b48b4027a..b83f79c6e 100644 --- a/regression/heap-data/shared_mem2/test.desc +++ b/regression/heap-data/shared_mem2/test.desc @@ -1,6 +1,6 @@ CORE main.c ---heap-values-refine --sympath --inline +--heap-values-refine ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/heap/built_from_end/test.desc b/regression/heap/built_from_end/test.desc index e086f8559..df624d753 100644 --- a/regression/heap/built_from_end/test.desc +++ b/regression/heap/built_from_end/test.desc @@ -1,6 +1,6 @@ CORE main.c ---heap-interval --inline --no-propagation --sympath +--heap-interval --no-propagation ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/heap/dll1_simple/test.desc b/regression/heap/dll1_simple/test.desc index 92784083a..8b51481de 100644 --- a/regression/heap/dll1_simple/test.desc +++ b/regression/heap/dll1_simple/test.desc @@ -1,6 +1,6 @@ KNOWNBUG main.c ---heap --inline --no-propagation +--heap --no-propagation ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/heap/list_false/test.desc b/regression/heap/list_false/test.desc index 450b08c19..9556b3310 100644 --- a/regression/heap/list_false/test.desc +++ b/regression/heap/list_false/test.desc @@ -1,6 +1,6 @@ CORE main.c ---heap-interval --sympath --inline --no-propagation +--heap-interval --no-propagation ^EXIT=5$ ^SIGNAL=0$ ^VERIFICATION INCONCLUSIVE$ diff --git a/regression/heap/list_false_kind/test.desc b/regression/heap/list_false_kind/test.desc index 93984c1aa..3d24fc98f 100644 --- a/regression/heap/list_false_kind/test.desc +++ b/regression/heap/list_false_kind/test.desc @@ -1,6 +1,6 @@ CORE main.c ---heap-interval --sympath --inline --no-propagation --k-induction +--heap-interval --no-propagation --k-induction ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/heap/list_true/test.desc b/regression/heap/list_true/test.desc index e2ef350dc..4a60b0de7 100644 --- a/regression/heap/list_true/test.desc +++ b/regression/heap/list_true/test.desc @@ -1,6 +1,6 @@ KNOWNBUG main.c ---heap-interval --sympath --inline --no-propagation +--heap-interval --no-propagation ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/heap/simple_false/test.desc b/regression/heap/simple_false/test.desc index 450b08c19..9556b3310 100644 --- a/regression/heap/simple_false/test.desc +++ b/regression/heap/simple_false/test.desc @@ -1,6 +1,6 @@ CORE main.c ---heap-interval --sympath --inline --no-propagation +--heap-interval --no-propagation ^EXIT=5$ ^SIGNAL=0$ ^VERIFICATION INCONCLUSIVE$ diff --git a/regression/heap/simple_false_kind/test.desc b/regression/heap/simple_false_kind/test.desc index 93984c1aa..3d24fc98f 100644 --- a/regression/heap/simple_false_kind/test.desc +++ b/regression/heap/simple_false_kind/test.desc @@ -1,6 +1,6 @@ CORE main.c ---heap-interval --sympath --inline --no-propagation --k-induction +--heap-interval --no-propagation --k-induction ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/heap/simple_true/test.desc b/regression/heap/simple_true/test.desc index 405084afc..4a60b0de7 100644 --- a/regression/heap/simple_true/test.desc +++ b/regression/heap/simple_true/test.desc @@ -1,6 +1,6 @@ KNOWNBUG main.c ---heap-interval --inline --no-propagation --sympath +--heap-interval --no-propagation ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/heap/sll_rhs_concretisation/test.desc b/regression/heap/sll_rhs_concretisation/test.desc index ed14b476a..75c6bdd58 100644 --- a/regression/heap/sll_rhs_concretisation/test.desc +++ b/regression/heap/sll_rhs_concretisation/test.desc @@ -1,6 +1,6 @@ CORE main.c ---heap --inline --no-propagation +--heap --no-propagation ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/heap/sll_simple/test.desc b/regression/heap/sll_simple/test.desc index b13e412ea..b0b056464 100644 --- a/regression/heap/sll_simple/test.desc +++ b/regression/heap/sll_simple/test.desc @@ -1,6 +1,6 @@ CORE main.c ---heap --inline --no-propagation --heap-interval +--heap --no-propagation --heap-interval ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/memsafety/built_from_end/test.desc b/regression/memsafety/built_from_end/test.desc index 02a269a04..6cb3dc340 100644 --- a/regression/memsafety/built_from_end/test.desc +++ b/regression/memsafety/built_from_end/test.desc @@ -1,6 +1,6 @@ CORE main.c ---heap-interval --inline --sympath --pointer-check --no-assertions +--heap-interval --pointer-check --no-assertions ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/memsafety/built_from_end_false/test.desc b/regression/memsafety/built_from_end_false/test.desc index f93d3925c..6875c0855 100644 --- a/regression/memsafety/built_from_end_false/test.desc +++ b/regression/memsafety/built_from_end_false/test.desc @@ -1,6 +1,6 @@ CORE main.c ---heap-interval --sympath --inline --pointer-check --no-assertions --k-induction +--heap-interval --pointer-check --no-assertions --k-induction ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/memsafety/simple_false/test.desc b/regression/memsafety/simple_false/test.desc index 0812ec27e..23247e589 100644 --- a/regression/memsafety/simple_false/test.desc +++ b/regression/memsafety/simple_false/test.desc @@ -1,6 +1,6 @@ CORE main.c ---heap-interval --sympath --inline --pointer-check --k-induction +--heap-interval --pointer-check --k-induction ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/memsafety/simple_true/test.desc b/regression/memsafety/simple_true/test.desc index 02a269a04..6cb3dc340 100644 --- a/regression/memsafety/simple_true/test.desc +++ b/regression/memsafety/simple_true/test.desc @@ -1,6 +1,6 @@ CORE main.c ---heap-interval --inline --sympath --pointer-check --no-assertions +--heap-interval --pointer-check --no-assertions ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/src/2ls/2ls_parse_options.cpp b/src/2ls/2ls_parse_options.cpp index 2e4b4a3d9..308b74605 100644 --- a/src/2ls/2ls_parse_options.cpp +++ b/src/2ls/2ls_parse_options.cpp @@ -207,6 +207,15 @@ void twols_parse_optionst::get_command_line_options(optionst &options) options.set_option("binsearch-solver", true); } + if(cmdline.isset("heap") || + cmdline.isset("heap-interval") || + cmdline.isset("heap-zones") || + cmdline.isset("heap-values-refine")) + { + options.set_option("inline", true); + options.set_option("sympath", true); + } + // use incremental assertion checks if(cmdline.isset("non-incremental")) options.set_option("incremental", false);