index
:
aeneas
isabelle
aeneas rust verifier with a hacky Isabelle backend
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
Files
Lines
...
|
*
|
More lisible sign for proj_right pretty-printing
Aymeric Fromherz
2024-05-30
1
-1
/
+1
|
*
|
Implement two phases of loops join + collapse
Aymeric Fromherz
2024-05-30
23
-2971
/
+660
|
*
|
Compute marker information for borrow/loan maps
Aymeric Fromherz
2024-05-28
3
-50
/
+73
|
*
|
Add type and set/map for marker and borrow id
Aymeric Fromherz
2024-05-28
4
-10
/
+22
|
*
|
Simplify collapse_ctx
Aymeric Fromherz
2024-05-27
1
-6
/
+5
|
*
|
Simplify reduce_ctx
Aymeric Fromherz
2024-05-27
1
-21
/
+6
|
*
|
Split collapse into collapse and reduce, rename accordingly
Aymeric Fromherz
2024-05-27
4
-13
/
+185
|
*
|
Add projection markers when joining environments
Aymeric Fromherz
2024-05-27
1
-0
/
+59
|
*
|
Add markers everywhere, do not use them yet
Aymeric Fromherz
2024-05-27
10
-139
/
+302
|
*
|
Start adding markers
Son Ho
2024-05-24
6
-50
/
+94
|
*
|
Downgrade the version of dune
Son Ho
2024-05-24
1
-1
/
+1
|
|
*
Remove the cps.eval_result type
Son Ho
2024-05-30
10
-38
/
+73
|
|
*
Remove the options from the functions synthesizing the symbolic AST
Son Ho
2024-05-30
11
-391
/
+282
|
|
/
|
/
|
*
|
Merge pull request #226 from AeneasVerif/remove-rust-scripts
Guillaume Boisseau
2024-05-30
2
-157
/
+0
|
\
\
|
*
|
Remove unused `rust-scripts`
Nadrieril
2024-05-30
2
-157
/
+0
|
/
/
*
|
Merge pull request #225 from AeneasVerif/update-charon-pin
Guillaume Boisseau
2024-05-30
2
-8
/
+14
|
\
\
|
*
|
Update charon pin to local commit when developing
Nadrieril
2024-05-30
2
-8
/
+14
|
/
/
*
|
Merge pull request #217 from AeneasVerif/document-tests
Guillaume Boisseau
2024-05-30
7
-197
/
+284
|
\
\
|
*
|
Improve the tests README
Nadrieril
2024-05-30
2
-14
/
+22
|
*
|
runner: Factor out backend-specific options
Nadrieril
2024-05-30
2
-49
/
+56
|
*
|
runner: Split up into multiple files
Nadrieril
2024-05-30
6
-198
/
+191
|
*
|
runner: make the backend map a submodule of `Backend`
Nadrieril
2024-05-30
1
-36
/
+48
|
*
|
tests: Add a README
Nadrieril
2024-05-30
1
-0
/
+67
|
/
/
*
|
Merge pull request #149 from RaitoBezarius/reexport-our-charon
Guillaume Boisseau
2024-05-29
2
-0
/
+20
|
\
\
|
*
|
chore: explain a Nix-powered workflow
Ryan Lahfa
2024-05-29
2
-0
/
+20
|
/
/
*
|
Merge pull request #218 from AeneasVerif/ci-check-pin
Guillaume Boisseau
2024-05-29
5
-2
/
+31
|
\
\
|
*
|
ci: Check correctness of the charon pinned commit
Nadrieril
2024-05-29
5
-2
/
+31
|
/
/
*
|
Merge pull request #222 from AeneasVerif/son/readme
Son HO
2024-05-29
1
-6
/
+7
|
\
\
|
*
|
Update the README
Son Ho
2024-05-29
1
-6
/
+7
|
/
/
*
|
Merge pull request #221 from AeneasVerif/son/builtins
Son HO
2024-05-29
2
-163
/
+124
|
\
\
|
*
\
Merge branch 'main' into son/builtins
Son HO
2024-05-29
0
-0
/
+0
|
|
\
\
|
|
/
/
|
/
|
|
*
|
|
Merge pull request #220 from AeneasVerif/son/collisions
Son HO
2024-05-29
3
-25
/
+23
|
\
\
\
|
*
\
\
Merge branch 'main' into son/collisions
Son HO
2024-05-29
0
-0
/
+0
|
|
\
\
\
|
|
/
/
/
|
/
|
|
|
*
|
|
|
Merge pull request #219 from AeneasVerif/son/infinite
Son HO
2024-05-28
5
-5
/
+77
|
\
\
\
\
|
|
|
*
|
Factor out code in ExtractBuiltin.ml
Son Ho
2024-05-29
2
-163
/
+124
|
|
|
/
/
|
|
*
/
Fix an issue with some names being ignored when generating unique variable names
Son Ho
2024-05-28
3
-25
/
+23
|
|
/
/
|
*
|
Reactivate the infinite-loop.rs test
Son Ho
2024-05-28
4
-1
/
+76
|
*
|
Fix a bug in SymbolicToPure.translate_loop
Son Ho
2024-05-28
1
-4
/
+1
|
/
/
*
|
Merge pull request #213 from AeneasVerif/cleanup-tests
Guillaume Boisseau
2024-05-28
84
-4396
/
+839
|
\
\
|
*
|
tests: Rename hashmap_utils -> utils
Nadrieril
2024-05-28
13
-42
/
+40
|
*
|
Add some tests
Nadrieril
2024-05-28
8
-0
/
+178
|
*
|
runner: Store options for crate tests in a separate file
Nadrieril
2024-05-28
2
-30
/
+14
|
*
|
tests: Rename betree_main -> betree
Nadrieril
2024-05-28
31
-365
/
+361
|
*
|
tests: Merge the hashmap test files
Nadrieril
2024-05-27
42
-3992
/
+279
|
/
/
*
|
Merge pull request #209 from AeneasVerif/negative-tests
Guillaume Boisseau
2024-05-27
8
-47
/
+159
|
\
\
|
*
|
runner: Add `no-check-output` option for unstable outputs
Nadrieril
2024-05-27
3
-27
/
+31
|
*
|
runner: Support negative tests
Nadrieril
2024-05-27
9
-26
/
+123
|
*
|
runner: Correctly catch command exit status
Nadrieril
2024-05-27
2
-29
/
+40
|
/
/
*
|
Merge pull request #184 from RaitoBezarius/unsigned-max
Son HO
2024-05-27
1
-0
/
+39
|
\
\
|
*
\
Merge branch 'main' into unsigned-max
Son HO
2024-05-27
118
-1449
/
+1626
|
|
\
\
|
|
/
/
|
/
|
|
[prev]
[next]