diff --git a/examples/linux/Makefile b/examples/linux/Makefile index d023235..3457510 100644 --- a/examples/linux/Makefile +++ b/examples/linux/Makefile @@ -3,10 +3,10 @@ CFLAGS=-O3 -static all: CFLAGS=-O3 -static all: NOSTDLIBFLAGS=-m32 -fno-builtin -static -nostdlib -fomit-frame-pointer -all: nostdlib basic sindex strncmp arguments ibranch sendmail crackme indexhell baby-re helloworld +all: nostdlib basic sindex strncmp arguments ibranch sendmail crackme indexhell baby-re helloworld simpleassert arm: CC=arm-linux-gnueabi-gcc -arm: basic sindex strncmp arguments ibranch sendmail crackme indexhell helloworld simple_copy +arm: basic sindex strncmp arguments ibranch sendmail crackme indexhell helloworld simple_copy simpleassert clean: rm -rf nostdlib basic sindex strncmp arguments sendmail server ibranch crackme indexhell crackme.c simple_copy helloworld nostdlib32 nostdlib64 @@ -23,6 +23,9 @@ simple_copy: simple_copy.c basic: basic.c $(CC) $(CFLAGS) basic.c -static -o basic +simpleassert: simpleassert.c + $(CC) $(CFLAGS) -O0 simpleassert.c -static -o simpleassert + sindex: sindex.c $(CC) $(CFLAGS) sindex.c -o sindex diff --git a/examples/linux/simpleassert.c b/examples/linux/simpleassert.c new file mode 100644 index 0000000..b022a22 --- /dev/null +++ b/examples/linux/simpleassert.c @@ -0,0 +1,56 @@ +/** + * Manticore should find 5 paths, one of which should be the `return -1` error + * path. + * + * This code is based on the symbolic execution example in these slides: + * https://www.cs.umd.edu/~mwh/se-tutorial/symbolic-exec.pdf + */ + +#include +#include +#include + +int main(int argc, char* argv[], char* envp[]){ + int a; + int b; + int c; + + int x = 0; + int y = 0; + int z = 0; + + if (read(0, &a, sizeof(a)) != sizeof(a)) + { + printf("Error reading stdin!"); + exit(-1); + } + if (read(0, &b, sizeof(b)) != sizeof(b)) + { + printf("Error reading stdin!"); + exit(-1); + } + if (read(0, &c, sizeof(c)) != sizeof(c)) + { + printf("Error reading stdin!"); + exit(-1); + } + + if (a) { + x = -2; + } + + if (b < 5) { + if (!a && c) { + y = 1; + } + z = 2; + } + + if (x + y + z == 3) { + return -1; + } + + return 0; +} + +