Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Support glibc-preprocessed asserts #177

Open
tomsik68 opened this issue Oct 23, 2020 · 2 comments
Open

Support glibc-preprocessed asserts #177

tomsik68 opened this issue Oct 23, 2020 · 2 comments
Labels
sv-comp Related to sv-comp

Comments

@tomsik68
Copy link
Member

tomsik68 commented Oct 23, 2020

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 tomsik68 added the sv-comp Related to sv-comp label Oct 23, 2020
@tomsik68
Copy link
Member Author

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
Copy link
Member

mchalupa commented Oct 23, 2020

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
sv-comp Related to sv-comp
Projects
None yet
Development

No branches or pull requests

2 participants