Skip to content

Introduce an overflow irep that takes lvalues as arguments #6841

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

Jump to bottom
Closed
tautschnig opened this issue May 4, 2022 · 0 comments · Fixed by #6903
Closed

Introduce an overflow irep that takes lvalues as arguments #6841

tautschnig opened this issue May 4, 2022 · 0 comments · Fixed by #6903
Labels
aws Bugs or features of importance to AWS CBMC users aws-high pending merge

Comments

@tautschnig
Copy link
Collaborator

In order to use __builtin_add_overflow and the likes, one has to introduce additional objects the address of which can be taken. To avoid such overhead when building goto programs directly, it would be desirable to have variants of the overflow intrinsics that take lvalues as (optional) parameters so that both is-there-an-overflow and the actual value can be assigned in a single instruction.
@tautschnig tautschnig self-assigned this May 4, 2022
@tautschnig tautschnig added aws Bugs or features of importance to AWS CBMC users aws-high labels May 4, 2022
tautschnig added a commit to tautschnig/cbmc that referenced this issue Jun 3, 2022
@tautschnig
Add overflow_result_exprt: compute result and overflow in one expression
50d5879 
Doing both the arithmetic operation and determining whether or not there
was an overflow previously required either multiple expressions or going
via `__builtin_X_overflow`, which should be specific to the C front-end.

The new expression returns a struct with two components, the first of
which has the type of the arithmetic operation, and the second is
Boolean.

Fixes: diffblue#6841
@tautschnig tautschnig removed their assignment Jun 3, 2022
@tautschnig tautschnig mentioned this issue Jun 3, 2022
Merged
5 tasks
tautschnig added a commit to tautschnig/cbmc that referenced this issue Jun 3, 2022
@tautschnig
Add overflow_result_exprt: compute result and overflow in one expression
d594a96 
Doing both the arithmetic operation and determining whether or not there
was an overflow previously required either multiple expressions or going
via `__builtin_X_overflow`, which should be specific to the C front-end.

The new expression returns a struct with two components, the first of
which has the type of the arithmetic operation, and the second is
Boolean.

Fixes: diffblue#6841
tautschnig added a commit to tautschnig/cbmc that referenced this issue Jun 3, 2022
@tautschnig
Add overflow_result_exprt: compute result and overflow in one expression
5ea97b3 
Doing both the arithmetic operation and determining whether or not there
was an overflow previously required either multiple expressions or going
via `__builtin_X_overflow`, which should be specific to the C front-end.

The new expression returns a struct with two components, the first of
which has the type of the arithmetic operation, and the second is
Boolean.

Fixes: diffblue#6841
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
aws Bugs or features of importance to AWS CBMC users aws-high pending merge
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Add overflow_result_exprt: compute result and overflow in one expression tautschnig/cbmc
1 participant
@tautschnig