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.

Sign up for GitHub

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

Jump to bottom

Support for valid-memsafety-ub #1227

Closed
michael-schwarz opened this issue Oct 31, 2023 · 1 comment
Closed

Support for valid-memsafety-ub #1227

michael-schwarz opened this issue Oct 31, 2023 · 1 comment
Labels
sv-comp SV-COMP (analyses, results), witnesses
Milestone
SV-COMP 2024

Comments

@michael-schwarz
Copy link
Member

In SV-COMP there likely will be a new property checking only

CHECK( init(main()), LTL(G valid-free) )
CHECK( init(main()), LTL(G valid-deref) )

we should add support for this. This is nice for us as valid-memtrack is hard for us.
@michael-schwarz michael-schwarz added the sv-comp SV-COMP (analyses, results), witnesses label Oct 31, 2023
@michael-schwarz michael-schwarz added this to the SV-COMP 2024 milestone Oct 31, 2023
@sim642
Copy link
Member

sim642 commented Oct 31, 2023

This duplicates #1220 which is fixed by #1228.

@sim642 sim642 closed this as not planned Won't fix, can't repro, duplicate, stale Oct 31, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
sv-comp SV-COMP (analyses, results), witnesses
Projects
None yet
Milestone
SV-COMP 2024
Development

No branches or pull requests
2 participants
@sim642 @michael-schwarz