Skip to content

Conversation

@michael-schwarz
Copy link
Member

Bump goblint-cil so changes from goblint/cil#48 become available. Currently still fails for the following tests:

12 test(s) failed: ["00/14 startstate", "04/33 kernel_rc", "04/34 kernel_nr", "04/39 rw_lock_nr", "04/40 rw_lock_rc", "04/48 assign_spawn", "04/53 kernel-spinlock", "09/07 kernel_list_rc", "09/08 kernel_list_nr", "09/14 kernel_foreach_rc", "09/15 kernel_foreach_nr", "41/02 bsearch"]

@michael-schwarz
Copy link
Member Author

The issue is in CIL, not Goblint.

@sim642
Copy link
Member

sim642 commented Dec 14, 2021

I fixed the bsearch test: our stub signature was missing const from an argument. The corrected combineTypes for C11 generics noticed the difference, while the old one did not.

The kernel ones might be related to the CInt change somehow, because that error comes from some integer manipulation.

@sim642
Copy link
Member

sim642 commented Dec 14, 2021

The kernel ones might be related to the CInt change somehow, because that error comes from some integer manipulation.

Actually no, it was also related to const (or more specifically pconst) in constFold of casts. I've fixed that in CIL and repinned.

@sim642 sim642 marked this pull request as ready for review December 14, 2021 08:27
@sim642 sim642 self-assigned this Dec 14, 2021
@michael-schwarz
Copy link
Member Author

👍
I'll start another sv-comp run to see if we now fail on some program where it worked before and then we can merge.

@michael-schwarz
Copy link
Member Author

michael-schwarz commented Dec 14, 2021

Looks like this was not enough, the newly added testcase over on the CIL repo still fails.

Nvm, I just had a brainfart.

@michael-schwarz michael-schwarz merged commit ed16687 into master Dec 14, 2021
@michael-schwarz michael-schwarz deleted the cil-c11-generic branch December 14, 2021 16:41
@sim642 sim642 added this to the v2.0.0 milestone Aug 12, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants