index
:
aeneas
isabelle
aeneas rust verifier with a hacky Isabelle backend
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
compiler
(
unfollow
)
Commit message (
Expand
)
Author
Files
Lines
2024-06-04
Propagated changes to statement from Charon (#223)
Escherichia
2
-1
/
+2
2024-06-04
Improve collapse_ctx
Son Ho
1
-1
/
+42
2024-06-04
Do more cleanup
Son Ho
1
-40
/
+44
2024-06-04
Factor out the code in collapse_ctx
Son Ho
2
-153
/
+56
2024-06-04
Start factoring out the code of reduce_ctx and collapse_ctx
Son Ho
1
-91
/
+162
2024-06-04
Improve merge_abstractions by splitting the markers before merging
Son Ho
1
-0
/
+75
2024-06-04
Cleanup merge_abstractions
Son Ho
1
-96
/
+183
2024-06-03
Fix an issue with the type of the values given back by loops
Son Ho
3
-157
/
+237
2024-06-03
Fix a bug when composing the continuations in eval_statement
Son Ho
4
-122
/
+131
2024-06-03
feat: basic handling for `RValue::Len`, following AeneasVerif/charon#209
Lucas Franceschino
4
-2
/
+6
2024-06-03
Change the order in which we merge abstractions
Son Ho
5
-105
/
+99
2024-06-03
Cleanup a bit
Son Ho
3
-44
/
+53
2024-06-03
Factor out some code and update some comments
Son Ho
4
-166
/
+173
2024-06-03
Cleanup a bit
Son Ho
4
-91
/
+87
2024-06-03
Make minor modifications
Son Ho
4
-19
/
+25
2024-06-03
Update some comments
Son Ho
1
-2
/
+2
2024-05-31
format
Aymeric Fromherz
1
-18
/
+18
2024-05-31
Add documentation to collapse
Aymeric Fromherz
1
-1
/
+27
2024-05-31
Add missing reverse when collapsing environment
Aymeric Fromherz
1
-2
/
+1
2024-05-31
Fix unused variables warnings
Aymeric Fromherz
2
-13
/
+18
2024-05-31
Avoid adding shared loans twice when merging environments
Aymeric Fromherz
1
-5
/
+28
2024-05-31
Add markers when creating new abstractions because of a join with bottom
Aymeric Fromherz
3
-48
/
+63
2024-05-31
Also fix implementation of Join-SharedBorrow
Aymeric Fromherz
1
-3
/
+3
2024-05-30
destructure_abs can be called during collapse: markers should be allowed
Aymeric Fromherz
1
-4
/
+0
2024-05-30
Correct implementation of Join-MutBorrows: add markers when creating a new ab...
Aymeric Fromherz
1
-3
/
+4
2024-05-30
More lisible sign for proj_right pretty-printing
Aymeric Fromherz
1
-1
/
+1
2024-05-30
Implement two phases of loops join + collapse
Aymeric Fromherz
4
-383
/
+552
2024-05-29
Factor out code in ExtractBuiltin.ml
Son Ho
2
-163
/
+124
2024-05-28
Fix an issue with some names being ignored when generating unique variable names
Son Ho
1
-21
/
+19
2024-05-28
Fix a bug in SymbolicToPure.translate_loop
Son Ho
1
-4
/
+1
2024-05-28
Compute marker information for borrow/loan maps
Aymeric Fromherz
3
-50
/
+73
2024-05-28
Add type and set/map for marker and borrow id
Aymeric Fromherz
3
-9
/
+21
2024-05-27
Simplify collapse_ctx
Aymeric Fromherz
1
-6
/
+5
2024-05-27
Simplify reduce_ctx
Aymeric Fromherz
1
-21
/
+6
2024-05-27
Split collapse into collapse and reduce, rename accordingly
Aymeric Fromherz
4
-13
/
+185
2024-05-27
Add projection markers when joining environments
Aymeric Fromherz
1
-0
/
+59
2024-05-27
Add markers everywhere, do not use them yet
Aymeric Fromherz
10
-139
/
+302
2024-05-24
Factor out the code for Lean and Coq
Son Ho
1
-143
/
+41
2024-05-24
Start adding markers
Son Ho
6
-50
/
+94
2024-05-24
Expand debug output in loops fixed points
Aymeric Fromherz
1
-1
/
+16
2024-05-24
Rename meta into span
Aymeric Fromherz
51
-2939
/
+2943
2024-05-24
Rename span into raw_span
Aymeric Fromherz
4
-20
/
+20
2024-05-24
Update charon pin
Nadrieril
2
-2
/
+3
2024-05-24
Fix a crash which happens when type definitions are ignored
Son Ho
1
-2
/
+5
2024-05-24
Print the name patterns of the definitions which fail to extract
Son Ho
2
-15
/
+24
2024-05-23
Update the interpreter so that it is not written in CPS style (#120)
Escherichia
19
-2294
/
+2116
2024-05-23
Add simp, reducible attributes to generated Lean projectors
Aymeric Fromherz
1
-0
/
+10
2024-05-23
Do not expand field projector for recursive structs to a let binding in Lean
Aymeric Fromherz
1
-5
/
+0
2024-05-23
Improve formatting of Lean struct projectors
Aymeric Fromherz
1
-2
/
+6
2024-05-23
Add printing of projectors for recursive structs in Lean backend
Aymeric Fromherz
1
-3
/
+130
[next]