Skip to content

Better side-effect checks for loop contracts #8393

Open
@qinheping

Description

@qinheping

#8360 adds an option to disable side-effect checks for loop contracts so that a larger range of expression can be used in loop contracts. But this option is unsound as it handover the responsibility of checking side-effect to users. We need to implement a better side-effect check and remove this option in the future.

Metadata

Metadata

Assignees

Labels

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions