document the CLI flag assume_no_casting_overflow#459
Merged
yoav-rodeh merged 2 commits intorelease/version_8.8.0from Feb 9, 2026
Merged
document the CLI flag assume_no_casting_overflow#459yoav-rodeh merged 2 commits intorelease/version_8.8.0from
assume_no_casting_overflow#459yoav-rodeh merged 2 commits intorelease/version_8.8.0from
Conversation
srunquist-certora
changed the base branch from
master
to
release/version_8.8.0
docs/prover/cli/options.md
Outdated
| (--assume_no_casting_overflow)= | ||
| ## `assume_no_casting_overflow` | ||
|
|
||
| This option adds an implicit assumption to all solidity casting operation. For example, if `int16(x)` appears in the solidity code, then it is assumed that `x` is indeed a valid `int16` at this point in the program. That is, `x` is in `[0, 2^15-1]` or in `[2^256 - 2^15, 2^256 - 1]` (this domain results from the EVM using 2s complement representation in 256 bits). |
Collaborator
There was a problem hiding this comment.
Suggested change
| This option adds an implicit assumption to all solidity casting operation. For example, if `int16(x)` appears in the solidity code, then it is assumed that `x` is indeed a valid `int16` at this point in the program. That is, `x` is in `[0, 2^15-1]` or in `[2^256 - 2^15, 2^256 - 1]` (this domain results from the EVM using 2s complement representation in 256 bits). | |
| This option adds an implicit assumption to all Solidity casting operation. For example, if `int16(x)` appears in the Solidity code, then it is assumed that `x` is indeed a valid `int16` at this point in the program. That is, `x` is in `[0, 2^15-1]` or in `[2^256 - 2^15, 2^256 - 1]` (this domain results from the EVM using 2s complement representation in 256 bits). |
Contributor
Author
There was a problem hiding this comment.
Capitalizaion fixed, and also the technical part dropped, as suggested by @jar-ben .
docs/prover/cli/options.md
Outdated
|
|
||
| This option adds an implicit assumption to all solidity casting operation. For example, if `int16(x)` appears in the solidity code, then it is assumed that `x` is indeed a valid `int16` at this point in the program. That is, `x` is in `[0, 2^15-1]` or in `[2^256 - 2^15, 2^256 - 1]` (this domain results from the EVM using 2s complement representation in 256 bits). | ||
|
|
||
| Note that this flag may result in an underapproximation, i.e., it may result in the tool not checking some valid runs. That is because solidity does not revert on out of bounds casting operations. Therefore, it is important to use this option with caution. |
Collaborator
There was a problem hiding this comment.
Suggested change
| Note that this flag may result in an underapproximation, i.e., it may result in the tool not checking some valid runs. That is because solidity does not revert on out of bounds casting operations. Therefore, it is important to use this option with caution. | |
| Note that this flag may result in an underapproximation, i.e., it may result in the tool not checking some valid runs. That is because solidity does not revert on out-of-bounds casting operations. Therefore, it is important to use this option with caution. |
|
|
||
| Note that this flag may result in an underapproximation, i.e., it may result in the tool not checking some valid runs. That is because solidity does not revert on out of bounds casting operations. Therefore, it is important to use this option with caution. | ||
|
|
||
|
|
Collaborator
There was a problem hiding this comment.
Suggested change
| **Example** | |
| To assume Solidity casts do not overflow / underflow: | |
| _Command line_ | |
| ```sh | |
| certoraRun proj.conf --assume_no_casting_overflow | |
| ``` | |
| _Configuration file_ | |
| ```json | |
| "assume_no_casting_overflow": true | |
| ``` | |
Contributor
Author
There was a problem hiding this comment.
done, except I believe it needs a true on the command line as well. So added that.
jar-ben
approved these changes
Feb 9, 2026
Contributor
jar-ben
left a comment
jar-ben
left a comment
There was a problem hiding this comment.
looks ok, thank you for the changes
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
as the flag says.
New content: https://certora-certora-prover-documentation--459.com.readthedocs.build/en/459/docs/prover/cli/options.html#assume-no-casting-overflow