Skip to content

Add refutation support#583

Merged
JonasAlaif merged 7 commits into
masterfrom
refute
Jun 30, 2022
Merged

Add refutation support#583
JonasAlaif merged 7 commits into
masterfrom
refute

Conversation

@JonasAlaif

@JonasAlaif JonasAlaif commented Jun 2, 2022

Copy link
Copy Markdown
Contributor

Adds a refute expr statement, which is an assert expr with errors inverted and without assuming anything in the following statements (an assert expr assumes expr afterwards). That is, a refute expr does not report an error iff an assert expr would. Note that this is not the same as assert !expr since both asserts fail in the following snippet:

var b: Bool
if (*) { assert b }
else { assert !b }

One useful application is to check reachability (e.g. for identifying dead code) since all assertions pass in unreachable code (i.e. refute false will only error in dead code).

To workaround Silicon's numberOfErrorsToReport limit, this PR also adds an ExpectFail info tag to be used on assertions which should not be counted towards the limit (see linked Silicon PR).

  • Decide if ExpectFail should be an abstract class instead
  • Decide if ⭐ is a good name for a non-deterministic local variable, avoiding clashes
  • Add more tests

@mschwerhoff mschwerhoff left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks good, mostly a few minor comments.

Comment thread src/main/scala/viper/silver/ast/Ast.scala
Comment thread src/main/scala/viper/silver/ast/Ast.scala Outdated
Comment thread src/main/scala/viper/silver/plugin/standard/refute/RefuteErrors.scala Outdated
Comment thread src/main/scala/viper/silver/plugin/standard/refute/RefuteErrors.scala Outdated

@mschwerhoff mschwerhoff left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks good, modulo a few minor comments

Comment thread src/main/scala/viper/silver/ast/Ast.scala Outdated
Comment thread src/main/scala/viper/silver/plugin/standard/refute/RefutePlugin.scala Outdated
Comment thread src/main/scala/viper/silver/verifier/VerificationError.scala Outdated
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants