eurecom-s3/s2e — pull request #1 by cojocar (2013-05-09 09:40:21+00:00)
Title: qemu-arm: bugfix: env is RO when the tlb is filled

An update of env will cause klee to throw an error:
"""
KLEE: ERROR: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
"""

To trigger the error the following test case can be used:

/* assuming D is not in the TLB */
#define D (*((unsigned int *)0x85000000))

static void my_test(void)
{
char b;
s2e_make_symbolic(&b, 1, "my_buf");

if (b == 'A') {
D = 0;
s2e_kill_state(0, "A");
} else {
s2e_kill_state(0, "not A");
}
}

The fix is just an old hack that has been introduced in the commit:
394a0e3b999c9c4d76691ff81163731d908cdebb

I suspect that this issue was caused by a merge (e1cf109dd37a3f0d0deb0f5ff8137908db9b1ea3), because the current s2e/arm-experimental branch (on which eurecom/arm branch is based) contains a similar fix.