Skip to content

Fixes filtering of termination-related failures#584

Merged
ArquintL merged 3 commits into
masterfrom
failure-filtering-fix
Dec 16, 2021
Merged

Fixes filtering of termination-related failures#584
ArquintL merged 3 commits into
masterfrom
failure-filtering-fix

Conversation

@ArquintL

Copy link
Copy Markdown
Member

Assert stmts generated by the termination plugin have no position and no information.
Thus, the current filtering of failures introduces by PR #575 will filter these failures (see example added by Silver PR #546).
This fix adapts the filtering mechanism to take error transformers into account.
@mschwerhoff: What is the convention with error transformers? Should they be applied as early as possible? I was not sure whether the failures should contain the untransformed errors (as it is now) or whether it would be fine to only return the transformed errors.

@ArquintL ArquintL requested a review from mschwerhoff December 13, 2021 11:49

@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 to me, modulo the two minor comments.

Comment thread src/main/scala/Silicon.scala Outdated
Comment thread src/main/scala/Silicon.scala Outdated
@ArquintL ArquintL merged commit 22551b4 into master Dec 16, 2021
@ArquintL ArquintL deleted the failure-filtering-fix branch December 16, 2021 14:34
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.

2 participants