soteria
READ-ONLY MIRROR of the previous soteria repo
Star
Fork
Watch

Commits on experiment/array-repeat

N1ark
Experiment: add array repetition to rust_val
committed
N1ark
Rust edition 2024 pretty please
committed
N1ark
Keep using the old mono for now...
committed
N1ark
Llogging change: subst Charon w Obol if `--obol`
committed
N1ark
Better unsizing algorithm (ignore empty fields)
committed
N1ark
Stylistic change
committed
N1ark
Extract `Rust_val.ml` from `Charon_util.ml`
committed
N1ark
Better handle very large array types
committed
N1ark
Fix exception in diagnostics
committed
N1ark
Marginally nicer handling of ZST enums
committed
N1ark
Handle ZST enums (`enum { A(()) }` etc)
committed
N1ark
Update Charon for globals as places
committed
N1ark
Stuff to help Obol
committed
N1ark
Fix `ShallowInitBox`
committed
N1ark
Add `--log-compilation` flag
committed
N1ark
Auto-generated intrinsics (#96)
committed
N1ark
Add `soteria-rust obol` command (#95)
committed
N1ark
Log all our known failures (#94)
committed
N1ark
Add Cargo support! And better language support (#93)
committed
Sacha Ayoun
Us Hc instead of Hashcons (#92)
committed
N1ark
Interval analysis (#87)
committed
Sacha Ayoun
bit not and other fmt (#91)
committed
N1ark
Rename `Heap` -> `State` (#88)
committed
Sacha Ayoun
Track allocation origin to improve signalling of memory leaks (#89)
committed
Sacha Ayoun
Minor C stuff (#86)
committed
N1ark
Rust: fix `Box`, disable UB checks, bump Charon (#85)
committed
Sacha Ayoun
Various C improvements (#84)
committed
Sacha Ayoun
implement switch (finally finally) (#83)
committed
Sacha Ayoun
Soteria-C: Support for continue/break/goto (#82)
committed
N1ark
Interpreter Monad for Rust (#81)
committed
Sacha Ayoun
prog as effect (#80)
committed
Sacha Ayoun
Interpreter monad (#79)
committed
N1ark
Add `--ignore-aliasing` (#77)
committed
Sacha Ayoun
Optimise store (#78)
committed
Sacha Ayoun
Experiment scripts (#74)
committed
N1ark
Rust: SLL, annotations, diag printing (#75)
committed
Sacha Ayoun
Logo in Readme (#76)
committed
N1ark
Add `Soteria_terminal` (#72)
committed
N1ark
Add `grace` for Rust (#71)
committed
Sacha Ayoun
Solver cleanup (#70)
committed
Sacha Ayoun
Beautiful error messages ✨✨✨✨ (#69)
committed
Sacha Ayoun
Styling for progress bar (#68)
committed
Sacha Ayoun
Progress bar, improve reporting after execution in Coteria (#67)
committed
N1ark
Add dynamic function call (#65)
committed
Sacha Ayoun
add trivial model checkers (#66)
committed
N1ark
Support unwinds (#64)
committed
N1ark
Support `std::intrinsics::float_to_int_unchecked` (#63)
committed
N1ark
Add `eval` and `eval-diff` commands to script (#62)
committed
Sacha Ayoun
Propose a non-incremental Z3solver (#60)
committed
Sacha Ayoun
Add support for a few character sequences in soteria-c (#61)
committed
N1ark
More and more and more Kani, but cleaned up : ) (#59)
committed
N1ark
More SValues ! (#58)
committed
N1ark
Rework scripts in Python (#57)
committed
N1ark
Merge plugins, add `Crate` (#56)
committed
Sacha Ayoun
Real parser monad (#55)
committed
Sacha Ayoun
Cerberus new error nodes + short-circuiting boolean operators (#53)
committed
N1ark
Use Soteria.C_vals (#52)
committed
N1ark
Support `Cell`, better tree borrows, fix unions (#51)
committed
Sacha Ayoun
Extract c_values into a re-usable module (#50)
committed
Sacha Ayoun
Fix bug, add interface to execute only one function (#49)
committed