Skip to content

Fix lower_byte_{extract,update}'s documentation #4392

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

Merged
merged 1 commit into from
Mar 15, 2019
Merged

Fix lower_byte_{extract,update}'s documentation #4392

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 8 additions & 4 deletions src/solvers/lowering/expr_lowering.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,15 +19,19 @@ class popcount_exprt;
/// Rewrite a byte extract expression to more fundamental operations.
/// \param src: Byte extract expression
/// \param ns: Namespace
/// \return Semantically equivalent expression that does not contain any \ref
/// byte_extract_exprt or \ref byte_update_exprt.
/// \return Semantically equivalent expression such that the top-level
/// expression no longer is a \ref byte_extract_exprt or
/// \ref byte_update_exprt. Use \ref lower_byte_operators to also remove all
/// byte operators from any operands of \p src.
exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns);

/// Rewrite a byte update expression to more fundamental operations.
/// \param src: Byte update expression
/// \param ns: Namespace
/// \return Semantically equivalent expression that does not contain any \ref
/// byte_extract_exprt or \ref byte_update_exprt.
/// \return Semantically equivalent expression such that the top-level
/// expression no longer is a \ref byte_extract_exprt or
/// \ref byte_update_exprt. Use \ref lower_byte_operators to also remove all
/// byte operators from any operands of \p src.
exprt lower_byte_update(const byte_update_exprt &src, const namespacet &ns);

/// Rewrite an expression possibly containing byte-extract or -update
Expand Down