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

CBMC does not ignore the is_padding comment on datatype fields #5818

Closed
danielsn opened this issue Feb 11, 2021 · 2 comments
Closed

CBMC does not ignore the is_padding comment on datatype fields #5818

danielsn opened this issue Feb 11, 2021 · 2 comments
Labels
pending merge

Comments

@danielsn
Copy link
Contributor

On a datatype_parameter, the field is marked with the following named sub if its padding

                    "#is_padding": {
                      "id": "1"
                    },

CBMC appears to consider two structs to have different types if they agree on all fields, but disagree on which ones have the #is_padding comments. Aren't comments supposed to be ignored when comparing equality?
@danielsn danielsn added the aws Bugs or features of importance to AWS CBMC users label Feb 11, 2021
@tautschnig
Copy link
Collaborator

On a second look, this doesn't seem to be #is_padding that's causing trouble. It's #5815, again, as a padding member looks like this:

    2:
      * type: unsignedbv
          * width: 24
      * #is_padding: 1
      * name: $pad2

Note the absence of pretty_name, which the C front-end otherwise does always seem to set.

tautschnig added a commit to tautschnig/cbmc that referenced this issue Feb 11, 2021
@tautschnig
Make componentt::{base,pretty}_name comments
30739e6 
The only semantically relevant name information is the ID_name entry.
Two components should not be considered different when they only differ
in their base_name or pretty_name. Thus, use ID_C_base_name and
ID_C_pretty_name, respectively, to store these.

The goto binary version is incremented as goto binaries compiled before
this patch are incompatible with the changes introduced here.

Fixes: diffblue#5818
tautschnig added a commit to tautschnig/cbmc that referenced this issue Mar 3, 2021
@tautschnig
Make componentt::{base,pretty}_name comments
a79a15d 
The only semantically relevant name information is the ID_name entry.
Two components should not be considered different when they only differ
in their base_name or pretty_name. Thus, use ID_C_base_name and
ID_C_pretty_name, respectively, to store these.

The goto binary version is incremented as goto binaries compiled before
this patch are incompatible with the changes introduced here.

Fixes: diffblue#5818
tautschnig added a commit to tautschnig/cbmc that referenced this issue Apr 30, 2021
@tautschnig
Make componentt::{base,pretty}_name comments
d657a5d 
The only semantically relevant name information is the ID_name entry.
Two components should not be considered different when they only differ
in their base_name or pretty_name. Thus, use ID_C_base_name and
ID_C_pretty_name, respectively, to store these.

The goto binary version is incremented as goto binaries compiled before
this patch are incompatible with the changes introduced here.

Fixes: diffblue#5818
tautschnig added a commit to tautschnig/cbmc that referenced this issue May 7, 2021
@tautschnig
Make componentt::{base,pretty}_name comments
1691c0d 
The only semantically relevant name information is the ID_name entry.
Two components should not be considered different when they only differ
in their base_name or pretty_name. Thus, use ID_C_base_name and
ID_C_pretty_name, respectively, to store these.

The goto binary version is incremented as goto binaries compiled before
this patch are incompatible with the changes introduced here.

Fixes: diffblue#5818
tautschnig added a commit to tautschnig/cbmc that referenced this issue Aug 13, 2021
@tautschnig
Make componentt::{base,pretty}_name comments
2ab9a7d 
The only semantically relevant name information is the ID_name entry.
Two components should not be considered different when they only differ
in their base_name or pretty_name. Thus, use ID_C_base_name and
ID_C_pretty_name, respectively, to store these.

The goto binary version is incremented as goto binaries compiled before
this patch are incompatible with the changes introduced here.

Fixes: diffblue#5818
@jimgrundy jimgrundy removed the aws Bugs or features of importance to AWS CBMC users label Aug 24, 2021
@jimgrundy
Copy link
Collaborator

Dropping AWS label after review with @danielsn as there is no particular AWS interest.

tautschnig added a commit to tautschnig/cbmc that referenced this issue Nov 22, 2022
@tautschnig
Make componentt::{base,pretty}_name comments
a43b83e 
The only semantically relevant name information is the ID_name entry.
Two components should not be considered different when they only differ
in their base_name or pretty_name. Thus, use ID_C_base_name and
ID_C_pretty_name, respectively, to store these.

The goto binary version is incremented as goto binaries compiled before
this patch are incompatible with the changes introduced here.

Fixes: diffblue#5818
tautschnig added a commit to tautschnig/cbmc that referenced this issue Nov 22, 2022
@tautschnig
Make componentt::{base,pretty}_name comments
e495599 
The only semantically relevant name information is the ID_name entry.
Two components should not be considered different when they only differ
in their base_name or pretty_name. Thus, use ID_C_base_name and
ID_C_pretty_name, respectively, to store these.

The goto binary version is incremented as goto binaries compiled before
this patch are incompatible with the changes introduced here.

Fixes: diffblue#5818
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
pending merge
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
3 participants
@tautschnig @danielsn @jimgrundy