From be9135c8071c4234c90d641e0ca5cff7fe0b8f18 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sun, 3 Feb 2019 14:43:19 +0000 Subject: [PATCH] Add function for reverting formula slicing This functionality is necessary to use slicing of symex_target_equationt in combination with incremental unwinding. Assertions in future unwindings may depend on steps that have been sliced away in previous unwindings. Thus, we have to undo and recompute the slice. --- src/goto-symex/slice.cpp | 9 +++++++++ src/goto-symex/slice.h | 3 +++ 2 files changed, 12 insertions(+) diff --git a/src/goto-symex/slice.cpp b/src/goto-symex/slice.cpp index 5da99ac49b0..565f9e1b24b 100644 --- a/src/goto-symex/slice.cpp +++ b/src/goto-symex/slice.cpp @@ -262,3 +262,12 @@ void simple_slice(symex_target_equationt &equation) s_it->ignore=true; } } + +void revert_slice(symex_target_equationt &equation) +{ + // set ignore to false + for(auto step : equation.SSA_steps) + { + step.ignore = false; + } +} diff --git a/src/goto-symex/slice.h b/src/goto-symex/slice.h index 5d62bd5d92a..ae906e5518e 100644 --- a/src/goto-symex/slice.h +++ b/src/goto-symex/slice.h @@ -19,6 +19,9 @@ Author: Daniel Kroening, kroening@kroening.com // slice an equation with respect to the assertions contained therein void slice(symex_target_equationt &equation); +/// Undo whatever has been done by `slice` +void revert_slice(symex_target_equationt &); + // this simply slices away anything after the last assertion void simple_slice(symex_target_equationt &equation);