-
Notifications
You must be signed in to change notification settings - Fork 72
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
Add definitions for library functions used in cp
program
#865
Conversation
This is against |
Already thought of, here's a couple of examples: analyzer/src/analyses/libraryFunctions.ml Line 48 in 24ad290
analyzer/unittest/analyses/libraryDslTest.ml Lines 21 to 27 in 24ad290
|
I'm not sure if SV-COMP rules cover the POSIX stuff though, they're not exactly part of GCC itself, but glibc. |
CHANGES: Functionally equivalent to Goblint in SV-COMP 2023. * Add automatic configuration tuning (goblint/analyzer#772). * Add many library function specifications (goblint/analyzer#865, goblint/analyzer#868, goblint/analyzer#878, goblint/analyzer#884, goblint/analyzer#886). * Reorganize library stubs (goblint/analyzer#814, goblint/analyzer#845). * Add Trace Event Format output to timing (goblint/analyzer#844). * Optimize domains for address and path sets (goblint/analyzer#803, goblint/analyzer#809).
Adds definitions for the library functions encountered during #855. The following definitions are still missing:
atexit
part of (Support foratexit
,on_exit
andpthread_cleanup_handlers
#799)error
fscanf
@sim642 Is there currently support for varargs in your library DSL? We would need it here.