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
(
follow
)
Commit message (
Expand
)
Author
Age
Files
Lines
*
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
*
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
*
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
4
-383
/
+552
*
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
3
-9
/
+21
*
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
*
Expand debug output in loops fixed points
Aymeric Fromherz
2024-05-24
1
-1
/
+16
*
Rename meta into span
Aymeric Fromherz
2024-05-24
51
-2939
/
+2943
*
Rename span into raw_span
Aymeric Fromherz
2024-05-24
4
-20
/
+20
*
Update charon pin
Nadrieril
2024-05-24
2
-2
/
+3
*
Fix a crash which happens when type definitions are ignored
Son Ho
2024-05-24
1
-2
/
+5
*
Print the name patterns of the definitions which fail to extract
Son Ho
2024-05-24
2
-15
/
+24
*
Update the interpreter so that it is not written in CPS style (#120)
Escherichia
2024-05-23
19
-2294
/
+2116
*
Catch new literal variants
Nadrieril
2024-05-14
2
-0
/
+6
*
Ensure `./charon` points to a valid charon clone
Nadrieril
2024-05-14
2
-1
/
+1
*
Update charon
Nadrieril
2024-05-06
2
-3
/
+12
*
Add error when handling mutually recursive traits
Aymeric Fromherz
2024-05-01
1
-1
/
+4
*
Update compiler/ExtractBuiltin.ml
Son HO
2024-04-26
1
-1
/
+1
*
Update the backend and ExtractBuiltin.ml
Son Ho
2024-04-25
1
-1
/
+4
*
Merge branch 'main' into core-option-unwrap
Son Ho
2024-04-25
1
-0
/
+25
|
\
|
*
Merge branch 'main' into option-take
Son Ho
2024-04-25
10
-100
/
+212
|
|
\
|
*
|
compiler: introduce Lean-only translations
Ryan Lahfa
2024-04-24
1
-10
/
+25
|
*
|
compiler: map `core::option::Option::is_none` to `Option.isNone`
Ryan Lahfa
2024-04-24
1
-0
/
+4
|
*
|
compiler: map `core::mem::swap` to the pure swap
Ryan Lahfa
2024-04-24
1
-0
/
+2
|
*
|
compiler: map `core::option::Option::take` to identity function
Ryan Lahfa
2024-04-17
1
-0
/
+4
*
|
|
Add core::option::unwrap builtin
Zyad Hassan
2024-04-24
1
-0
/
+2
|
|
/
|
/
|
*
|
Fix an issue when joining a symbolic value with bottom
Son Ho
2024-04-22
2
-11
/
+33
*
|
Reformat some files
Son Ho
2024-04-22
5
-24
/
+47
*
|
Merge pull request #146 from RaitoBezarius/main
Son HO
2024-04-19
1
-3
/
+69
|
\
\
|
*
|
fix(backends/lean): extract more keywords from `lstlean.tex`
Ryan Lahfa
2024-04-18
1
-0
/
+2
|
*
|
fix(backends/lean): extract more keywords from `lstlean.latex`
Ryan Lahfa
2024-04-18
1
-0
/
+62
[next]