Lithium: a Rust-native back end - #1321

Open

JakuJ wants to merge 55 commits into

viperproject:masterfrom

Commits on Oct 22, 2023

Add Lithium back end
JakuJ
committed
0928308
Add Lithium to VerificationBackend enum
JakuJ
committed
6821cff
Fix simple branching (if-statements in low vir)
JakuJ
committed
eb4c416
Wonky way of reporting offending positions
JakuJ
committed
daceb78
Fix branching assumptions for switchInt
JakuJ
committed
35843ff
Fix "otherwise" branch of switchInt statements
JakuJ
committed
74b090f
Fix after rebase
JakuJ
committed
f6e7e11
Add tests for loops, remove empty Conditional statements
JakuJ
committed
33fe480
Fix mod operator
JakuJ
committed
e3cb301
Add initial F32 and F64 support
JakuJ
committed
c68d489
Use FP operators, choose correct type declaration
JakuJ
committed
9caacd3
Tests for floating-point support
JakuJ
committed
412772f
Add preamble for CVC5, split fp.neq into 32 and 64-bit variants
JakuJ
committed
9f3b962
Fixes after merge
JakuJ
committed
f69cb0b
Quantifiers to snapshots, fix unsized type bound checking bug
JakuJ
committed
62f4a9b
Hack quantifier generation for complex types
JakuJ
committed
08c1e9e
Fix after rebase
JakuJ
committed
d195597
Fix lowering for quantifiers that use closures over function arguments
JakuJ
committed
ada6736
Add sum-of-primes test file
JakuJ
committed
6370a93
Add super sale test case
JakuJ
committed
64d8cd2
Update test cases
JakuJ
committed
fda0031
Add Euclid test case, fix quantifiers type mismatch
JakuJ
committed
15579d1
Optimization module
JakuJ
committed
fcfeda2
Correct reporting of failure reason positions
JakuJ
committed
9a6c479
Remove redundant reasons for failure if the same as failing place
JakuJ
committed
4585665
FP != for Viper
JakuJ
committed
4b5e026
Passing FP test case
JakuJ
committed
ddddb3a
Remove main.rs from Lithium
JakuJ
committed
c36a25d
Commit the config
JakuJ
committed
9b08400
Use files, not stdio, fix negative int encoding
JakuJ
committed
c8a4d51
Make clippy happy
JakuJ
committed
4e368ac
cargo fmt
JakuJ
committed
9ad4f34
More cargo fmt
JakuJ
committed
614ebc1
Increase SMT timeout, comment out problematic code in error_manager
JakuJ
committed
fc2e056
Fix abs(i32::MIN) overflowing
JakuJ
committed
41bbaaa
Refactor encoding of Statement::Conditional
JakuJ
committed
6f3ffcc
Fix invalid file paths when emitting SMT files
JakuJ
committed
25ee57b
Fix quantifier optimization rules
JakuJ
committed
6fedb19
Various bugfixes
JakuJ
committed
56c0678
Make sure positions are preserved by the optimizer
JakuJ
committed
f7bec36
Add bisect test case
JakuJ
committed
bc085e4
Remove overcomplicated tests
JakuJ
committed
1ad0fbe
Fix test error placement
JakuJ
committed
d97b664
Clean up SMT preambles, fix modulo operator encoding
JakuJ
committed
8e18928
Add Lithium test coverage script
JakuJ
committed
6a216fe
Fixes after merging master
JakuJ
committed
18db007
Make clippy happy
JakuJ
committed
dce49bb
Fix test compilation error
JakuJ
committed
9ba703d
Restore config
JakuJ
committed
18bc02f
Fixes after rebase
JakuJ
committed
9aed8af
Clippy
JakuJ
committed
8372022

Commits on Oct 27, 2023

Fix stopwatch getting released immediately
JakuJ
committed
000c701
Merge branch 'master' into lithium
JakuJ
committed
cb38222
Add PRUSTI_NATIVE_VERIFIER env variable
JakuJ
committed
09066e1
Restore test case unrelated to Lithium
JakuJ
committed
7664629