index
:
aeneas
isabelle
aeneas rust verifier with a hacky Isabelle backend
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
tests
(
follow
)
Commit message (
Expand
)
Author
Age
Files
Lines
*
Update charon
Nadrieril
2024-06-24
1
-6
/
+6
*
Update charon
Nadrieril
2024-06-24
9
-9
/
+9
*
Do some cleanup in the Lean backend (#257)
Son HO
2024-06-22
1
-56
/
+20
*
Improve `scalar_tac` and `scalar_decr_tac` (#256)
Son HO
2024-06-22
1
-76
/
+24
*
Add some proofs for the Lean backend (#255)
Son HO
2024-06-21
9
-125
/
+1038
*
Update charon
Nadrieril
2024-06-21
1
-3
/
+3
*
Support for renaming using the rename attribute in charon (#239)
Escherichia
2024-06-18
15
-6
/
+2309
*
Bump charon
Nadrieril
2024-06-18
16
-60
/
+60
*
Tiny dedup
Nadrieril
2024-06-18
1
-1
/
+1
*
Merge branch 'main' into son/cleanup
Son HO
2024-06-17
15
-18
/
+18
|
\
|
*
Regenerate the tests
Son Ho
2024-06-17
15
-18
/
+18
*
|
Regenerate the tests
Son Ho
2024-06-17
26
-2
/
+77
*
|
Update the tests
Son Ho
2024-06-17
6
-4
/
+31
*
|
Update Hashmap/Properties.lean
Son Ho
2024-06-17
1
-36
/
+34
*
|
Update the code of the hashmap
Son Ho
2024-06-17
12
-459
/
+465
|
/
*
Update the Lean dependencies
Son Ho
2024-06-17
1
-4
/
+4
*
Update the tests
Son Ho
2024-06-14
2
-4
/
+4
*
Update the tests
Son Ho
2024-06-13
3
-29
/
+29
*
Update the code extraction and regenerate the tests
Son Ho
2024-06-12
1
-2
/
+2
*
Revert "Regenerate the tests"
Son Ho
2024-06-12
12
-333
/
+338
*
Revert "Fix some mistakes"
Son Ho
2024-06-12
3
-15
/
+15
*
Fix some mistakes
Son Ho
2024-06-12
3
-15
/
+15
*
Regenerate the tests
Son Ho
2024-06-12
12
-338
/
+333
*
Deactivate the use of tuple projectors in the Lean backend
Son Ho
2024-06-11
1
-2
/
+4
*
Update the tests for tuples
Son Ho
2024-06-11
4
-22
/
+85
*
Regenerate the Coq and Lean betrees
Son Ho
2024-06-05
2
-178
/
+423
*
Update the F* betree
Son Ho
2024-06-05
3
-144
/
+280
*
Update the betree
Son Ho
2024-06-05
1
-99
/
+98
*
Regenerate some tests
Son Ho
2024-06-05
1
-14
/
+2
*
Add some negative tests for the borrow checker
Son Ho
2024-06-05
2
-0
/
+105
*
Add more tests
Son Ho
2024-06-05
5
-0
/
+79
*
Update the test runner
Son Ho
2024-06-05
1
-1
/
+4
*
Update the test runner to allow the syntax [!lean] and [borrow-check]
Son Ho
2024-06-05
14
-34
/
+65
*
Merge branch 'main' into son/clean-synthesis
Son Ho
2024-06-05
33
-407
/
+418
|
\
|
*
Update charon
Nadrieril
2024-06-05
27
-287
/
+278
|
*
Merge branch 'main' into son/loops2
Son Ho
2024-06-04
169
-5583
/
+2423
|
|
\
|
*
|
Add a test
Son Ho
2024-06-03
4
-103
/
+123
|
*
|
Regenerate tests
Aymeric Fromherz
2024-05-31
13
-35
/
+35
|
*
|
Regenerate test output
Aymeric Fromherz
2024-05-31
19
-108
/
+2588
|
*
|
Implement two phases of loops join + collapse
Aymeric Fromherz
2024-05-30
19
-2588
/
+108
|
*
|
Add type and set/map for marker and borrow id
Aymeric Fromherz
2024-05-28
1
-1
/
+1
|
*
|
Downgrade the version of dune
Son Ho
2024-05-24
1
-1
/
+1
*
|
|
Remove the options from the functions synthesizing the symbolic AST
Son Ho
2024-05-30
1
-6
/
+6
|
|
/
|
/
|
*
|
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
*
|
Fix an issue with some names being ignored when generating unique variable names
Son Ho
2024-05-28
2
-4
/
+4
*
|
Reactivate the infinite-loop.rs test
Son Ho
2024-05-28
4
-1
/
+76
[next]