symbiotic
symbiotic copied to clipboard
Support glibc-preprocessed asserts
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.
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__));
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).