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
...
|
*
|
Start factoring out the code of reduce_ctx and collapse_ctx
Son Ho
2024-06-04
1
-91
/
+162
|
*
|
Improve merge_abstractions by splitting the markers before merging
Son Ho
2024-06-04
1
-0
/
+75
|
*
|
Cleanup merge_abstractions
Son Ho
2024-06-04
1
-96
/
+183
|
*
|
Add a test
Son Ho
2024-06-03
4
-103
/
+123
|
*
|
Fix an issue with the type of the values given back by loops
Son Ho
2024-06-03
3
-157
/
+237
|
*
|
Fix a bug when composing the continuations in eval_statement
Son Ho
2024-06-03
4
-122
/
+131
|
*
|
Change the order in which we merge abstractions
Son Ho
2024-06-03
5
-105
/
+99
|
*
|
Cleanup a bit
Son Ho
2024-06-03
3
-44
/
+53
|
*
|
Factor out some code and update some comments
Son Ho
2024-06-03
4
-166
/
+173
|
*
|
Cleanup a bit
Son Ho
2024-06-03
4
-91
/
+87
|
*
|
Make minor modifications
Son Ho
2024-06-03
4
-19
/
+25
|
*
|
Update some comments
Son Ho
2024-06-03
1
-2
/
+2
|
*
|
format
Aymeric Fromherz
2024-05-31
1
-18
/
+18
|
*
|
Add documentation to collapse
Aymeric Fromherz
2024-05-31
1
-1
/
+27
|
*
|
Regenerate tests
Aymeric Fromherz
2024-05-31
13
-35
/
+35
|
*
|
Add missing reverse when collapsing environment
Aymeric Fromherz
2024-05-31
1
-2
/
+1
|
*
|
Fix unused variables warnings
Aymeric Fromherz
2024-05-31
2
-13
/
+18
|
*
|
Regenerate test output
Aymeric Fromherz
2024-05-31
19
-108
/
+2588
|
*
|
Avoid adding shared loans twice when merging environments
Aymeric Fromherz
2024-05-31
1
-5
/
+28
|
*
|
Add markers when creating new abstractions because of a join with bottom
Aymeric Fromherz
2024-05-31
3
-48
/
+63
|
*
|
Also fix implementation of Join-SharedBorrow
Aymeric Fromherz
2024-05-31
1
-3
/
+3
|
*
|
destructure_abs can be called during collapse: markers should be allowed
Aymeric Fromherz
2024-05-30
1
-4
/
+0
|
*
|
Correct implementation of Join-MutBorrows: add markers when creating a new ab...
Aymeric Fromherz
2024-05-30
1
-3
/
+4
|
*
|
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
|
/
/
[prev]
[next]