symbiotic icon indicating copy to clipboard operation
symbiotic copied to clipboard

Support glibc-preprocessed asserts

Open tomsik68 opened this issue 3 years ago • 2 comments

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 avatar Oct 23 '20 07:10 tomsik68

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__));

tomsik68 avatar Oct 23 '20 07:10 tomsik68

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).

mchalupa avatar Oct 23 '20 13:10 mchalupa