Skip to content

Better error spec#604

Merged
jcp19 merged 2 commits intomasterfrom
joao-better-error-spec
Jan 25, 2023
Merged

Better error spec#604
jcp19 merged 2 commits intomasterfrom
joao-better-error-spec

Conversation

@jcp19
Copy link
Contributor

@jcp19 jcp19 commented Jan 24, 2023

The version of error introduced in the previous spec caused a big performance degradation in verifiedSCION (likely, due to the use of wildcards in the spec of Error. This PR addresses that and recovers the original expressivity of the error type (in particular, implementations of Error that mutate the underlying data structure are still allowed)

@jcp19 jcp19 changed the title Joao better error spec Better error spec Jan 24, 2023
@jcp19 jcp19 requested review from ArquintL and Dspil January 24, 2023 12:52
@jcp19 jcp19 merged commit 67a4af8 into master Jan 25, 2023
@jcp19 jcp19 deleted the joao-better-error-spec branch January 25, 2023 09:29
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