Code

Lithium: a Rust-native back end#1321

Code

Open

JakuJ wants to merge 55 commits intoviperproject:masterviperproject/prusti-dev:masterfrom JakuJ:lithiumJakuJ/prusti-dev:lithiumCopy head branch name to clipboard

+3,359-206

Commits

Commits on Oct 22, 2023

• Add Lithium back end

  JakuJ

  committed
  0928308

  Copy full SHA for 0928308

• Add Lithium to VerificationBackend enum

  JakuJ

  committed
  6821cff

  Copy full SHA for 6821cff

• Fix simple branching (if-statements in low vir)

  JakuJ

  committed
  eb4c416

  Copy full SHA for eb4c416

• Wonky way of reporting offending positions

  JakuJ

  committed
  daceb78

  Copy full SHA for daceb78

• Fix branching assumptions for switchInt

  JakuJ

  committed
  35843ff

  Copy full SHA for 35843ff

• Fix "otherwise" branch of switchInt statements

  JakuJ

  committed
  74b090f

  Copy full SHA for 74b090f

• Fix after rebase

  JakuJ

  committed
  f6e7e11

  Copy full SHA for f6e7e11

• Add tests for loops, remove empty Conditional statements

  JakuJ

  committed
  33fe480

  Copy full SHA for 33fe480

• Fix mod operator

  JakuJ

  committed
  e3cb301

  Copy full SHA for e3cb301

• Add initial F32 and F64 support

  JakuJ

  committed
  c68d489

  Copy full SHA for c68d489

• Use FP operators, choose correct type declaration

  JakuJ

  committed
  9caacd3

  Copy full SHA for 9caacd3

• Tests for floating-point support

  JakuJ

  committed
  412772f

  Copy full SHA for 412772f

• Add preamble for CVC5, split fp.neq into 32 and 64-bit variants

  JakuJ

  committed
  9f3b962

  Copy full SHA for 9f3b962

• Fixes after merge

  JakuJ

  committed
  f69cb0b

  Copy full SHA for f69cb0b

• Quantifiers to snapshots, fix unsized type bound checking bug

  JakuJ

  committed
  62f4a9b

  Copy full SHA for 62f4a9b

• Hack quantifier generation for complex types

  JakuJ

  committed
  08c1e9e

  Copy full SHA for 08c1e9e

• Fix after rebase

  JakuJ

  committed
  d195597

  Copy full SHA for d195597

• Fix lowering for quantifiers that use closures over function arguments

  JakuJ

  committed
  ada6736

  Copy full SHA for ada6736

• Add sum-of-primes test file

  JakuJ

  committed
  6370a93

  Copy full SHA for 6370a93

• Add super sale test case

  JakuJ

  committed
  64d8cd2

  Copy full SHA for 64d8cd2

• Update test cases

  JakuJ

  committed
  fda0031

  Copy full SHA for fda0031

• Add Euclid test case, fix quantifiers type mismatch

  JakuJ

  committed
  15579d1

  Copy full SHA for 15579d1

• Optimization module

  JakuJ

  committed
  fcfeda2

  Copy full SHA for fcfeda2

• Correct reporting of failure reason positions

  JakuJ

  committed
  9a6c479

  Copy full SHA for 9a6c479

• Remove redundant reasons for failure if the same as failing place

  JakuJ

  committed
  4585665

  Copy full SHA for 4585665

• FP != for Viper

  JakuJ

  committed
  4b5e026

  Copy full SHA for 4b5e026

• Passing FP test case

  JakuJ

  committed
  ddddb3a

  Copy full SHA for ddddb3a

• Remove main.rs from Lithium

  JakuJ

  committed
  c36a25d

  Copy full SHA for c36a25d

• Commit the config

  JakuJ

  committed
  9b08400

  Copy full SHA for 9b08400

• Use files, not stdio, fix negative int encoding

  JakuJ

  committed
  c8a4d51

  Copy full SHA for c8a4d51

• Make clippy happy

  JakuJ

  committed
  4e368ac

  Copy full SHA for 4e368ac

• cargo fmt

  JakuJ

  committed
  9ad4f34

  Copy full SHA for 9ad4f34

• More cargo fmt

  JakuJ

  committed
  614ebc1

  Copy full SHA for 614ebc1

• Increase SMT timeout, comment out problematic code in error_manager

  JakuJ

  committed
  fc2e056

  Copy full SHA for fc2e056

• Fix abs(i32::MIN) overflowing

  JakuJ

  committed
  41bbaaa

  Copy full SHA for 41bbaaa

• Refactor encoding of Statement::Conditional

  JakuJ

  committed
  6f3ffcc

  Copy full SHA for 6f3ffcc

• Fix invalid file paths when emitting SMT files

  JakuJ

  committed
  25ee57b

  Copy full SHA for 25ee57b

• Fix quantifier optimization rules

  JakuJ

  committed
  6fedb19

  Copy full SHA for 6fedb19

• Various bugfixes

  JakuJ

  committed
  56c0678

  Copy full SHA for 56c0678

• Make sure positions are preserved by the optimizer

  JakuJ

  committed
  f7bec36

  Copy full SHA for f7bec36

• Add bisect test case

  JakuJ

  committed
  bc085e4

  Copy full SHA for bc085e4

• Remove overcomplicated tests

  JakuJ

  committed
  1ad0fbe

  Copy full SHA for 1ad0fbe

• Fix test error placement

  JakuJ

  committed
  d97b664

  Copy full SHA for d97b664

• Clean up SMT preambles, fix modulo operator encoding

  JakuJ

  committed
  8e18928

  Copy full SHA for 8e18928

• Add Lithium test coverage script

  Show description for 6a216fe
  JakuJ

  committed
  6a216fe

  Copy full SHA for 6a216fe

• Fixes after merging master

  JakuJ

  committed
  18db007

  Copy full SHA for 18db007

• Make clippy happy

  JakuJ

  committed
  dce49bb

  Copy full SHA for dce49bb

• Fix test compilation error

  JakuJ

  committed
  9ba703d

  Copy full SHA for 9ba703d

• Restore config

  JakuJ

  committed
  18bc02f

  Copy full SHA for 18bc02f

• Fixes after rebase

  JakuJ

  committed
  9aed8af

  Copy full SHA for 9aed8af

• Clippy

  JakuJ

  committed
  8372022

  Copy full SHA for 8372022

Commits on Oct 27, 2023

• Fix stopwatch getting released immediately

  JakuJ

  committed
  000c701

  Copy full SHA for 000c701

• Merge branch 'master' into lithium

  JakuJ

  committed
  cb38222

  Copy full SHA for cb38222

• Add PRUSTI_NATIVE_VERIFIER env variable

  JakuJ

  committed
  09066e1

  Copy full SHA for 09066e1

• Restore test case unrelated to Lithium

  JakuJ

  committed
  7664629

  Copy full SHA for 7664629