Skip to content

Commit 5bc51ef

Browse files
Make shadow memory instrumentation available to goto_symex
This will allow us to call the shadow memory instrumentation API.
1 parent 6242787 commit 5bc51ef

File tree

1 file changed

+14
-1
lines changed

1 file changed

+14
-1
lines changed

src/goto-symex/goto_symex.h

Lines changed: 14 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,7 @@ Author: Daniel Kroening, [email protected]
1515
#include <util/message.h>
1616

1717
#include "complexity_limiter.h"
18+
#include "shadow_memory.h"
1819
#include "symex_config.h"
1920
#include "symex_target_equation.h"
2021

@@ -66,7 +67,16 @@ class goto_symext
6667
path_segment_vccs(0),
6768
_total_vccs(std::numeric_limits<unsigned>::max()),
6869
_remaining_vccs(std::numeric_limits<unsigned>::max()),
69-
complexity_module(mh, options)
70+
complexity_module(mh, options),
71+
shadow_memory(
72+
std::bind(
73+
&goto_symext::symex_assign,
74+
this,
75+
std::placeholders::_1,
76+
std::placeholders::_2,
77+
std::placeholders::_3),
78+
ns,
79+
mh)
7080
{
7181
}
7282

@@ -822,6 +832,9 @@ class goto_symext
822832

823833
complexity_limitert complexity_module;
824834

835+
/// Shadow memory instrumentation API
836+
shadow_memoryt shadow_memory;
837+
825838
public:
826839
unsigned get_total_vccs() const
827840
{

0 commit comments

Comments
 (0)