Incremental unwinding of one specified loop

src/goto-symex/goto_symex.h

@@ -201,6 +201,13 @@ class goto_symext
   /// by the symbolic executions.
   bool ignore_assertions = false;
 
+  virtual bool check_break(
+    const irep_idt &id,
+    bool is_function,
+    statet &state,
+    const exprt &cond,
+    unsigned unwind);
+
 protected:
   /// The configuration to use for this symbolic execution
   const symex_configt symex_config;

src/goto-symex/symex_goto.cpp

@@ -288,6 +288,7 @@ void goto_symext::symex_goto(statet &state)
 
     if(should_stop_unwind(state.source, state.call_stack(), unwind))
     {
+      // we break the loop
       loop_bound_exceeded(state, new_guard);
 
       // next instruction
@@ -297,6 +298,11 @@ void goto_symext::symex_goto(statet &state)
 
     if(new_guard.is_true())
     {
+      // we continue executing the loop
+      if(check_break(loop_id, false, state, new_guard, unwind))
+      {
+        should_pause_symex = true;
+      }
       symex_transition(state, goto_target, true);
       return; // nothing else to do
     }
@@ -516,6 +522,17 @@ void goto_symext::symex_goto(statet &state)
   }
 }
 
+bool goto_symext::check_break(
+  const irep_idt &id,
+  bool is_function,
+  statet &state,
+  const exprt &cond,
+  unsigned unwind)
+{
+  // dummy implementation
+  return false;
+}
+
 void goto_symext::merge_gotos(statet &state)
 {
   framet &frame = state.call_stack().top();