Skip to content

Commit 8a7e1b9

Browse files
authored
Merge pull request diffblue#4392 from tautschnig/fix-byte-op-lowering-docs
Fix lower_byte_{extract,update}'s documentation
2 parents 4df008a + f3cbb8f commit 8a7e1b9

File tree

1 file changed

+8
-4
lines changed

1 file changed

+8
-4
lines changed

src/solvers/lowering/expr_lowering.h

Lines changed: 8 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -19,15 +19,19 @@ class popcount_exprt;
1919
/// Rewrite a byte extract expression to more fundamental operations.
2020
/// \param src: Byte extract expression
2121
/// \param ns: Namespace
22-
/// \return Semantically equivalent expression that does not contain any \ref
23-
/// byte_extract_exprt or \ref byte_update_exprt.
22+
/// \return Semantically equivalent expression such that the top-level
23+
/// expression no longer is a \ref byte_extract_exprt or
24+
/// \ref byte_update_exprt. Use \ref lower_byte_operators to also remove all
25+
/// byte operators from any operands of \p src.
2426
exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns);
2527

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

3337
/// Rewrite an expression possibly containing byte-extract or -update

0 commit comments

Comments
 (0)