symbiotic
symbiotic copied to clipboard
staticafi
Symbiotic is a tool for finding bugs in computer programs based on instrumentation, program slicing and KLEE
Symbiotic reports `false(def-behavior)` for this program ```C int main() { int array1[1]; int count; for(count=0;count
The following piece of code contains an error but Symbiotic does not see it: ```c #include #include int main(void) { void* a = malloc(sizeof(int)); void* b = malloc(sizeof(int)); if (a...
I've following suggestions for rewording of current error traces emitted by `klee`. * All error traces that contain info about the origin of the allocated memory are only pointing to...
Symbiotic does not detect UB when the memory regions of arguments of `memcpy`, `strcpy` or `strncpy` overlap. This should be quite an easy fix as we just need to add...
This should be fixed in upstream KLEE as well. I guess that there will be a similar problem with writing as well. However, writing to the padding is UB as...
Might be related to #103. Input: ```c #include int main(int argc, char * argv[]) { assert(argc == 1); const char *ptr = argv[10]; /* error */ } ``` Output: ```...
Hi, Symbiotic fails to find a property violation in the following piece of code: ```c #include int main(void) { *NULL; } ``` Output: ``` $ symbiotic --prp=memsafety null.c 7.0.0-dev-llvm-9.0.1-symbiotic:03f217bf-dg:e89761ff-sbt-slicer:fff6245c-sbt-instrumentation:34bbe496-klee:e773a1f8 INFO:...
When verifying programs that use output like `printf,puts,fprintf`, Symbiotic is unable to tell the difference between output from klee and output from the verified program. To reproduce the problem, verify...
Some sv-benchmarks are preprocessed using glibc. Symbiotic doesn't seem to understand glibc's expansion of `assert` macro. It looks like this: `__assert("", "sources/sys/sv_comp.h", 5, "0"));` where `__assert` is an ordinary function...
This code has a memory leak as the `a[1] = 20` overwrites the pointer to the malloced memory. ```C int main() { void *p = malloc(3U); char *a = (char*)...