-
Notifications
You must be signed in to change notification settings - Fork 273
Introduce complex_imag_exprt and complex_real_exprt #2916
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
Introduce complex_imag_exprt and complex_real_exprt #2916
Conversation
src/util/std_expr.h
Outdated
@@ -1731,6 +1731,106 @@ inline void validate_expr(const complex_exprt &value) | |||
} | |||
|
|||
|
|||
/// \brief Real part |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
part ... of what? (I'd say "Real part of the expression describing a complex number.")
src/util/std_expr.h
Outdated
PRECONDITION(expr.id() == ID_complex_real); | ||
DATA_INVARIANT( | ||
expr.operands().size() == 1, | ||
"Real part retrieval operation must have one operand"); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Use lowercase for error messages (applies across this PR).
src/util/std_expr.h
Outdated
|
||
|
||
/// \brief Imaginary part | ||
class complex_imag_exprt:public unary_exprt |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think clang-format wants spaces around :
bb6ad6d
to
899fe03
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This PR failed Diffblue compatibility checks (cbmc commit: c76d96f).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/84129475
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.
Common spurious failures:
- the cbmc commit has disappeared in the mean time (e.g. in a force-push)
- the author is not in the list of contributors (e.g. first-time contributors).
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This PR failed Diffblue compatibility checks (cbmc commit: bb6ad6d).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/84132032
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.
Common spurious failures:
- the cbmc commit has disappeared in the mean time (e.g. in a force-push)
- the author is not in the list of contributors (e.g. first-time contributors).
There was a problem hiding this 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: 899fe03).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/84142660
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
LGTM - this seems a lot cleaner.
No description provided.