From 74310393232d081d983d9199874234eb4950e250 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 18 Dec 2016 13:56:20 +0000 Subject: [PATCH] Skip unreachable instructions Unconditional forward gotos previously would still cause the subsequent instruction to be considered. This causes unnecessary goto_statet copying. --- src/goto-symex/symex_goto.cpp | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp index 74c7b3c775d..b8e6f1a0a36 100644 --- a/src/goto-symex/symex_goto.cpp +++ b/src/goto-symex/symex_goto.cpp @@ -102,6 +102,17 @@ void goto_symext::symex_goto(statet &state) new_state_pc=goto_target; state_pc=state.source.pc; state_pc++; + + // skip dead instructions + if(new_guard.is_true()) + while(state_pc!=goto_target && !state_pc->is_target()) + ++state_pc; + + if(state_pc==goto_target) + { + state.source.pc=goto_target; + return; // nothing else to do + } } else {