Skip to content

Error handling cleanup in solvers/flattening 7 #2944

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

Conversation

danpoe
Copy link
Contributor

@danpoe danpoe commented Sep 13, 2018

No description provided.

@@ -24,10 +24,9 @@ literalt equalityt::equality(const exprt &e1, const exprt &e2)

literalt equalityt::equality2(const exprt &e1, const exprt &e2)
{
const typet &type=e1.type();
PRECONDITION(e2.type() != e1.type());
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Those better be equal ;-)

throw "equalityt got boolean equality";
// return lequal(convert(e1), convert(e2));
INVARIANT(
type.id() != ID_bool, "method shall not be used to compare boolean types");
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

s/boolean/Boolean/

INVARIANT_WITH_DIAGNOSTICS(
false,
"flatten_byte_update should only be used on arrays of scalars",
subtype.id_string());
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

No, it can soundly be used on other types, it's just not yet implemented...

Files equality.cpp to pointer_logic.h
@danpoe danpoe force-pushed the refactor/error-handling-solvers-flattening-from-boolbv-equality branch from 0ccb8e8 to d07bba7 Compare September 21, 2018 12:58
Copy link
Contributor

@allredj allredj left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Passed Diffblue compatibility checks (cbmc commit: d07bba7).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/85574428

@danpoe
Copy link
Contributor Author

danpoe commented Sep 28, 2018

@tautschnig I think this is ready to be merged.

@tautschnig tautschnig merged commit ae9ea6d into diffblue:develop Sep 28, 2018
@danpoe danpoe deleted the refactor/error-handling-solvers-flattening-from-boolbv-equality branch June 2, 2020 17:18
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants