search

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
313 stars 55 forks source link

Support glibc-preprocessed asserts #177

Open tomsik68 opened 4 years ago

tomsik68 commented 4 years ago

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 (not a macro). This works like __assert_fail, so we could technically just replace it.

tomsik68 commented 4 years ago

I just came across more assert functions:

extern void __assert_fail (const char *__assertion, const char *__file,
      unsigned int __line, const char *__function)
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
extern void __assert_perror_fail (int __errnum, const char *__file,
      unsigned int __line, const char *__function)
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
extern void __assert (const char *__assertion, const char *__file, int __line)
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
mchalupa commented 4 years ago

In general, we would like to handle these other assertions (probably as you proposed: just replace these with __assert_fail) but in the context of SV-COMP, these are wrong benchmarks and they should be fixed. EDIT: Of course, if these assertions in the benchmark are those whose validity is being verified (they can be used just for aborting undesirable paths).