-
Notifications
You must be signed in to change notification settings - Fork 278
Description
This section constructs a with expression containing multiple where/new value pairs -
cbmc/src/solvers/lowering/byte_operators.cpp
Lines 1514 to 1517 in 8bd2617
if(result.id() != ID_with) | |
result = with_exprt{result, std::move(where), std::move(update_value)}; | |
else | |
result.add_to_operands(std::move(where), std::move(update_value)); |
However the API here only provides access to a single where/new value pair -
Lines 2444 to 2462 in 8bd2617
exprt &where() | |
{ | |
return op1(); | |
} | |
const exprt &where() const | |
{ | |
return op1(); | |
} | |
exprt &new_value() | |
{ | |
return op2(); | |
} | |
const exprt &new_value() const | |
{ | |
return op2(); | |
} |
What should be the preferred way to deal with this mismatch?
A. Update the lowering to nest with expressions rather than constructing a single expression with multiple pairs.
B. Update with_exprt
to expose the possibility of multiple pairs.
C. Work around the mismatch for the moment using exprt::operands
to access the additional pairs.
I am not a huge fan of option C as it leaves the possibility of multiple pairs relatively surprising when referring to with_exprt
. Option A seems relatively preferable as it keeps the API simpler, however I have also presented option B in case there are performance reasons for preferring more operands over more deeply nested expressions.
Metadata
Metadata
Assignees
Labels
Type
Projects
Status