From 243b3ed420ddd4da9809020d1b7cedd8bf446725 Mon Sep 17 00:00:00 2001
From: Benedikt Radtke <benediktradtke@gmail.com>
Date: Tue, 12 Jan 2021 18:00:30 +0100
Subject: [PATCH] Expose the checkpoint and some task/frame members public

---
 isla-lib/Cargo.toml      |  2 +-
 isla-lib/src/executor.rs | 18 +++++++++---------
 isla-lib/src/smt.rs      |  6 +++---
 3 files changed, 13 insertions(+), 13 deletions(-)

diff --git a/isla-lib/Cargo.toml b/isla-lib/Cargo.toml
index 64af7c7e..499d4c05 100644
--- a/isla-lib/Cargo.toml
+++ b/isla-lib/Cargo.toml
@@ -23,7 +23,7 @@ lalrpop-util = "0.19.0"
 crossbeam = "0.7.3"
 lazy_static = "1.4.0"
 toml = "0.5.5"
-z3-sys = "0.5.0"
+z3-sys = "0.6.3"
 libc = "0.2.5"
 serde = { version = "1.0.104", features = ["derive"] }
 bincode = "1.2.1"
diff --git a/isla-lib/src/executor.rs b/isla-lib/src/executor.rs
index b76fd9d9..4f0e365a 100644
--- a/isla-lib/src/executor.rs
+++ b/isla-lib/src/executor.rs
@@ -426,13 +426,13 @@ pub struct Frame<'ir, B> {
 /// executing thread. It is turned into an immutable `Frame` when the
 /// control flow forks on a choice, which can be shared by threads.
 pub struct LocalFrame<'ir, B> {
-    function_name: Name,
-    pc: usize,
+    pub function_name: Name,
+    pub pc: usize,
     forks: u32,
     backjumps: u32,
     local_state: LocalState<'ir, B>,
     memory: Memory<B>,
-    instrs: &'ir [Instr<Name, B>],
+    pub instrs: &'ir [Instr<Name, B>],
     stack_vars: Vec<Bindings<'ir, B>>,
     stack_call: Stack<'ir, B>,
     backtrace: Backtrace,
@@ -1050,12 +1050,12 @@ impl<B> Default for TaskState<B> {
 /// SMT solver state, and finally an option SMTLIB definiton which is
 /// added to the solver state when the task is resumed.
 pub struct Task<'ir, 'task, B> {
-    id: usize,
-    frame: Frame<'ir, B>,
-    checkpoint: Checkpoint<B>,
-    fork_cond: Option<smtlib::Def>,
-    state: &'task TaskState<B>,
-    stop_functions: Option<&'task HashSet<Name>>,
+    pub id: usize,
+    pub frame: Frame<'ir, B>,
+    pub checkpoint: Checkpoint<B>,
+    pub fork_cond: Option<smtlib::Def>,
+    pub state: &'task TaskState<B>,
+    pub stop_functions: Option<&'task HashSet<Name>>,
 }
 
 impl<'ir, 'task, B> Task<'ir, 'task, B> {
diff --git a/isla-lib/src/smt.rs b/isla-lib/src/smt.rs
index 42fdd126..813dd933 100644
--- a/isla-lib/src/smt.rs
+++ b/isla-lib/src/smt.rs
@@ -311,7 +311,7 @@ use smtlib::*;
 pub struct Checkpoint<B> {
     num: usize,
     next_var: u32,
-    trace: Arc<Option<Trace<B>>>,
+    pub trace: Arc<Option<Trace<B>>>,
 }
 
 impl<B> Checkpoint<B> {
@@ -451,8 +451,8 @@ pub type EvPath<B> = Vec<Event<B>>;
 #[derive(Debug)]
 pub struct Trace<B> {
     checkpoints: usize,
-    head: Vec<Event<B>>,
-    tail: Arc<Option<Trace<B>>>,
+    pub head: Vec<Event<B>>,
+    pub tail: Arc<Option<Trace<B>>>,
 }
 
 impl<B: BV> Trace<B> {