staticafi / symbiotic

Symbiotic is a tool for finding bugs in computer programs based on instrumentation, program slicing and KLEE
http://staticafi.github.io/symbiotic/
MIT License
308 stars 56 forks source link

Copying of overlapping memory regions is undetected #197

Open lzaoral opened 3 years ago

lzaoral commented 3 years ago

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 some additional asserts to corresponding implementations in lib/libc (Divine does practically the same thing).

Tests: https://github.com/aufover/aufover-benchmark/tree/main/tests/single-c/mem-overlap

mchalupa commented 3 years ago

Yep, you are right.