Merge pull request #140 from viktormalik/heap-auto-inline-sympath

peterschrammel · web-flow · commit 477e22526bb4 · 2020-03-17T19:59:52.000Z
Automatically set --inline and --sympath when --heap* is set
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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);
