Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Failing crates in the top-500 test #87

Closed
6 of 8 tasks
fpoli opened this issue Jun 29, 2020 · 2 comments
Closed
6 of 8 tasks

Failing crates in the top-500 test #87

fpoli opened this issue Jun 29, 2020 · 2 comments
Assignees
Labels
bug Something isn't working

Comments

@fpoli
Copy link
Member

fpoli commented Jun 29, 2020

There are a few crates on which cargo-prusti fails, as reported in the top-500 test.

Panic

'not yet implemented: TyParam(T/#0)', prusti-viper/src/encoder/type_encoder.rs:128:22

  • 074_futures
  • 111_num-complex
  • 342_euclid
  • 348_cgmath

Consistency error

No matching identifier equals$__$TY$__m_log$$Level$opensqu$0$closesqu$$beg$end$m_log$$LevelFilter$opensqu$0$closesqu$$beg$end$$bool$ found of type Function

  • 002_log
  • 423_h2

Unregistered verification error

[function.not.wellformed:insufficient.permission] Function might not be well-formed. There might be insufficient permission to access _arg.f$0.

  • 341_winit

Timeout

@fpoli fpoli added the bug Something isn't working label Jun 29, 2020
@cmatheja cmatheja self-assigned this Jun 29, 2020
@cmatheja
Copy link
Contributor

cmatheja commented Jul 2, 2020

After the update, verification fails for three crates:

  • 033_unicode-normalization (timeout)
  • 199_tokio-threadpool (fold-unfold issue)
  • 423_h2 (consistency error in code generated by the snapshot encoder)

@fpoli
Copy link
Member Author

fpoli commented Dec 2, 2020

Superseded by #169

@fpoli fpoli closed this as completed Dec 2, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something isn't working
Projects
None yet
Development

No branches or pull requests

2 participants