Memcpy model doesn't work if a struct contains a pointer to a struct #2925

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

Closed

peterschrammel opened this issue Sep 9, 2018 · 0 comments · Fixed by #6042

Labels

Member

peterschrammel commented Sep 9, 2018

(generalised example reported by a user)

tautschnig added a commit to tautschnig/cbmc that referenced this issue


          Memcpy for pointers involving structs was fixed via field sensitivity

5b30b06

This test passes as of ca9fcb7, except for the missing "line NN" part
that wasn't included in the pattern to be matched.

Fixes: diffblue#2925

tautschnig mentioned this issue

Memcpy for pointers involving structs was fixed via field sensitivity #6042

Merged

3 tasks

tautschnig added the pending merge label

kroening closed this as completed in #6042

jezhiggins pushed a commit to jezhiggins/cbmc that referenced this issue


          Memcpy for pointers involving structs was fixed via field sensitivity

544a4aa

This test passes as of ca9fcb7, except for the missing "line NN" part
that wasn't included in the pattern to be matched.

Fixes: diffblue#2925

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment