Skip to content

VerCors 1.3.0
Compare
Choose a tag to compare
@pieter-bos pieter-bos released this 03 Feb 14:16
· 3134 commits to master since this release
v1.3.0
c42ff88

Features

  • The webpage code was moved to a different repository
  • Added detection for contracts of which the requirements are unsatisfiable
  • Added type checking to jspec rewriting rules
  • Refactored the test framework
  • Warn users when using integer division in permission values
  • Updated viper to release 20.07
  • Improve the support for sequences, sets and options in PVL, and add support for Maps, Set comprehension (@OmerSakar)
  • Fixed all warnings in the build, greatly improving build time
  • Pointers may now be assigned by subscript
  • Updated z3 to 4.8.6
  • Added various simplifying rewrite rules
  • Added support for exceptions and exceptional statements (break, continue) (@bobismijnnaam)
  • Improved C and GPGPU support: pure methods and functions, ghost statements, CUDA kernel invocations, kernel invariants and atomics
  • Improved syntax highlighting for PVL
  • --version now outputs better diagnostic information, including the commit
  • Range syntax was changed from [a..b) to {a..b}
  • Parsing frontend was redone: specifications are parsed in the first pass and attached in the tree; the parse tree is transformed by destructuring pattern match in Scala
  • All expression classes are now case classes, and consequently have structural equality
  • Add support for the ambiguous boolean/bitwise operators in Java: ^, | and &
  • Contracts are attached correctly to labeled loops
  • NameScanner was refactored (@bobismijnnaam)
  • Pure function application is now allowed in invariants
  • The user can be notified of completion of verification with --notify
  • Switched to GitHub Actions
  • Added various new examples

Bugfixes

  • Fixed a case where the origin of contracts was not preserved
  • Fixed that vercors warned about simplification failures in simple quantified statements about arrays
  • Fixed an infinite loop in the array encoding
  • Map the Head operator to Viper again
  • ==> and -* are now right-associative
  • Fixed a case where an expression was extracted to a variable in flatten without effect
  • Some examples that used old backends were refactored to use silicon (@Sophietje)
  • Disallow writing to locals in parallel blocks (which caused unsoundness)
  • Disallow using \result in signals specifications
  • Warn that inner classes are not supported, instead of crashing
Assets 5
Loading