Hi Mark, I’m not sure if I understood the question correctly. My understanding was that you would like to define a safe region for the application and then treat all the memory accesses falling outside of that region as invalid - is that correct? One idea might be to do that with an additional intrinsic. That would, however, mean introducing instrumentation into the source code of the tested application. In the intrinsic you would say, e.g., that addresses 0xABCD - 0xEFFF are valid and then you would check inside the executeMemoryOperation method, whether the address being accessed falls into this valid range. Things probably will be more complicated for these addresses that are symbolic. I guess for these, one would need to request a concrete value from the SMT solver. I can imagine a situation in which the valid range for the pointer expression only partially overlaps with the defined valid memory region, so I think that probably the solver query should also include range constraints for our defined valid memory region (in order to avoid false positives resulting from the fact that the solver just happened to return a value falling into the valid range). Please note that KLEE runs in the same address space as the interpreted program.
Hope that helps, Tomek On 22 Nov 2014, at 10:31, Mark R. Tuttle <[email protected]> wrote: > How would you define a region of memory and assert that a pointer should > never point outside of that region? > > To assert that all reads and writes should access only memory within that > region? > > Thanks, > Mark > > _______________________________________________ > klee-dev mailing list > [email protected] > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
<<attachment: winmail.dat>>
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
