Timotej Kapus

Pending constraints and ZESTI searcher

5

This is the bare bone implementation of pending constraints. It is enough for an md5 example to work, but I haven't tested it any other benchmarks yet. I think this...

KLEE flushes uninitialised memory, which I encountered during sqlite runs. Given this program: ```C #include "assert.h" int main() { char* a = malloc(2048); unsigned i; klee_make_symbolic(&i, sizeof(i), "i"); klee_assume(i <...

klee doesn't handle passing structures properly

7

``` C struct S1 { char f0; unsigned long f1; unsigned f2 :19; long f3; short f4; }; static int func_13(char p_14, struct S1 p_16) { p_16.f0 = p_14; return...

return struct crestc error

1

Compiling ```C struct a { char const b; } g_1782; struct a c() { for (;;) return g_1782; } int main() { } ``` With ```crestc``` gives me ``` test7.c:...

I've encountered another prediction failed issue, it looks very different from the other one to me. Running: ```C unsigned short a = 0; unsigned char b = 1; void main()...

I think I found another issue with crest when dealing with bit fields. Given a program like: ```C struct { unsigned a : 16; } b = {1}; int d;...