viperproject/prusti-dev

Issues

• Prusti server stopped working

  #1527 opened 3 months ago by cdstanford
  1

• linux-aarch64: "cargo-prusti: cannot execute binary file: Exec format error"

  #1526 opened 3 months ago by ValarMorghulisMaiDou
  0

• Feature Request: Add Configuration Flag to Lower Verify Errors to Warnings

  #1524 opened 3 months ago by seanrion
  1

• Prusti encounters unexpected internal error

  #1523 opened 4 months ago by lpnaunau
  3

• `len()` implementation without overflow errors

  #1516 opened 6 months ago by fpoli
  1

• Internal error: Location bb6[1] has not yet been encoded

  #1521 opened 5 months ago by nishanthkarthik
  0

• Assert(false) passing with Shared References

  #1518 opened 5 months ago by cliu369
  1

• unsupported feature: determining the region of a dereferentiation is not supported

  #1519 opened 5 months ago by nishanthkarthik
  0

• cannot generate fold-unfold Viper statements

  #1520 opened 5 months ago by nishanthkarthik
  0

• Error: cannot generate fold-unfold Viper statements

  #1517 opened 5 months ago by nishanthkarthik
  0

• External specification declared on a trait implementation did not resolve to a concrete type

  #1515 opened 6 months ago by nishanthkarthik
  0

• Enum: unsupported statement kind `Intrinsic(Assume(move _))`

  #1513 opened 7 months ago by nishanthkarthik
  0

• Enum discriminant completeness

  #1512 opened 7 months ago by nishanthkarthik
  0

• Wrong encoding of signed divisions

  #1505 opened 8 months ago by fpoli
  2

• ghost seq not implemented

  #1508 opened 8 months ago by nishanthkarthik
  1

• Error for missing model lifetime specifier recommends invalid syntax, has unclear fix

  #1509 opened 8 months ago by csgordon
  3

• Unsupported constant string in println

  #1504 opened 9 months ago by MathieuSoysal
  1

• Inconsistency in the encoding of Rust addresses as Viper Ref types

  #1506 opened 9 months ago by fpoli
  0

• Wrong encoding of signed discriminants in pure code

  #1501 opened 9 months ago by fpoli
  1

• Support for old(..) expressions in loop invariants

  #1500 opened 9 months ago by fpoli
  0

• Executable mode bits in release files not set

  #1497 opened 9 months ago by ifndefJOSH
  4

• Verifying 3rd party dependency crate results in compiler panic

  #1493 opened 9 months ago by nshyrei
  14

• Backward-incompatible `prusti_contracts`

  #1446 opened 10 months ago by fpoli
  1

• Unexpected order of verification errors

  #1489 opened 10 months ago by fpoli
  0

• Failing procedural macro of a contract

  #1480 opened a year ago by fpoli
  0

• Update rust nightly to support codegen-backend

  #1478 opened a year ago by sigmaSd
  1

• rustc removed plugins

  #1473 opened a year ago by safinaskar
  2

• Internal error when assigning a closure call to a reference

  #1472 opened a year ago by fpoli
  0

• Internal error when assigning to an argument

  #1471 opened a year ago by fpoli
  0

• Evaluate Profile-Guided Optimization (PGO) and LLVM BOLT

  #1454 opened a year ago by zamazan4ik
  1

• Prusti doesn’t run for the `thumbv7em-none-eabihf` target

  #1466 opened a year ago by pwnorbitals
  5

• Unsound verification when cloning vector elements

  #1423 opened a year ago by nokunish
  1

• (Documentation of) Closures

  #1431 opened a year ago by vfukala
  2

• Compiler shows `non_snake_case` warnings for internal `prusti_extern_spec_...` functions

  #1429 opened a year ago by vfukala
  1

• Issues with verifying the result is None

  #1427 opened a year ago by nokunish
  4

• Upgrade test suite to ui_test

  #1417 opened a year ago by fpoli
  2

• Help message for x.py

  #1469 opened a year ago by fpoli
  0

• Switch to the domain definition of `read$`

  #1468 opened a year ago by fpoli
  0

• Loop invariant might not hold, but there is none

  #1465 opened a year ago by fpoli
  0

• Details: Location bb15[12] has not yet been encoded

  #1462 opened a year ago by smokytheangel0
  3

• Prusti encounters unexpected internal error on return types containing references

  #1457 opened a year ago by benjaminflin
  1

• Stack overflow for mutually recursive specifications

  #1426 opened a year ago by vfukala
  0

• Insufficient access permission

  #1421 opened a year ago by nokunish
  1

• External specification for std::cmp::Ord crashing Prusti

  #1425 opened a year ago by nokunish
  1

• Cannot use PartialOrd in specifications despite marking them as #[pure] using external spec feature

  #1436 opened a year ago by Ramla-I
  3

• Prusti cannot detect that a generic type fulfills the Copy trait bound requirement

  #1453 opened a year ago by Ramla-I
  3

• Termination checks of mutually recursive functions

  #1443 opened a year ago by fpoli
  0

• Internal error: Viper doesn't support `folding .. in ..` expressions

  #1441 opened a year ago by fpoli
  0

• unsoundness when verifying reference-typed fields with quantifiers

  #1424 opened a year ago by nokunish
  0

• Prusti proves `false` in `tests/verify_overflow/pass/extern-spec/linked-list.rs`

  #1420 opened a year ago by vfukala
  2