Skip to content

Commit

Permalink
Added invalid memory access example
Browse files Browse the repository at this point in the history
  • Loading branch information
ChrisEdel committed Jun 15, 2019
1 parent 2ff6c68 commit b3de1ed
Showing 1 changed file with 29 additions and 0 deletions.
29 changes: 29 additions & 0 deletions manuscript/code/symbolic/invalid-memory-access.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,29 @@
/*
The purpose of this code is to demonstrate the capabilities
of the monster model generator of selfie. Monster translates
the code to an SMT-LIB or BTOR2 formula that is satisfiable
if and only if the code exits with a non-zero exit code, or
performs division by zero or invalid/unsafe memory accesses.
Input == #b00110001 (== 49 == '1')
*/

uint64_t main() {
uint64_t a;
uint64_t* x;

x = malloc(8);

read(1, x, 1);

if (*x == 48)
// address outside of virtual address space -> invalid memory access
*(x + 4294967296) = 0;

a = *x - 7;

if (a == 42)
return 1;
else
return 0;
}

0 comments on commit b3de1ed

Please sign in to comment.