search

rems-project / isla

Symbolic execution tool for Sail ISA specifications
Other
62 stars 10 forks source link

Support concrete writes to non-volatile memory sections #20

Closed Trolldemorted closed 3 years ago

Trolldemorted commented 3 years ago

As discussed in #16, a write of a concrete Val::Bits(_) will not cause that value to be read at the moment. This makes it impossible to emulate code that pushes return adresses to the stack, since an unconstrained symbol will be popped into PC.

Trolldemorted commented 3 years ago

Solved by the custom memory regions