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
/
coq
/
misc
(
unfollow
)
Commit message (
Expand
)
Author
Files
Lines
2024-05-24
Update output files
Nadrieril
7
-161
/
+161
2024-05-24
Update test outputs
Nadrieril
7
-161
/
+161
2024-05-24
Tweak a path
Nadrieril
7
-161
/
+161
2024-05-23
Bump charon version
Nadrieril
4
-6
/
+6
2024-04-25
Regenerate and fix the tests
Son Ho
1
-0
/
+7
2024-04-25
Update the tests for External
Son Ho
7
-92
/
+134
2024-04-24
Update tests
Zyad Hassan
1
-7
/
+0
2024-04-18
Ensure we regenerate files properly in CI
Nadrieril
2
-2
/
+0
2024-04-17
Bump charon
Nadrieril
1
-159
/
+56
2024-04-11
Fix a Coq file
Son Ho
1
-1
/
+1
2024-04-04
Regenerate the test files
Son Ho
8
-185
/
+165
2024-04-04
Regenerate the test files
Son Ho
7
-59
/
+63
2024-03-20
Regenerate the code
Son Ho
4
-22
/
+17
2024-03-19
Regenerate the tests
Son Ho
2
-31
/
+12
2024-03-18
Regenerate the test files
Son Ho
1
-18
/
+18
2024-03-18
Regenerate the constants tests and update Primitives/Base.lean
Son Ho
1
-18
/
+35
2024-03-11
Update the generated files
Son Ho
2
-31
/
+32
2024-03-09
Regenerate the test files
Son Ho
1
-0
/
+64
2024-02-02
Rename and regenerate some files
Son Ho
1
-1
/
+1
2024-01-25
Regenerate the files
Son Ho
1
-35
/
+58
2023-12-23
Fix an issue in External_FunsExternal.v
Son Ho
1
-15
/
+3
2023-12-23
Fix an issue when deconstructing tuples in Coq
Son Ho
1
-2
/
+2
2023-12-23
Regenerate the files
Son Ho
4
-38
/
+22
2023-12-23
Improve the micro passes to eliminate pattern `let f := fun x => g x`
Son Ho
1
-18
/
+8
2023-12-22
Regenerate the test files and add the fstar-split tests
Son Ho
9
-653
/
+378
2023-12-22
Annotate the bound vars in the lambdas for Coq
Son Ho
2
-273
/
+231
2023-12-13
Regenerate the test files
Son Ho
2
-61
/
+75
2023-12-07
Regenerate the tests
Son Ho
1
-1
/
+33
2023-12-05
Update following changes in Charon
Son Ho
2
-74
/
+132
2023-11-29
Regenerate the other files
Son Ho
2
-0
/
+77
2023-11-29
Generate the Bitwise test files
Son Ho
1
-0
/
+38
2023-11-27
Generate a dedicated file for the external types
Son Ho
12
-24
/
+59
2023-11-27
Update the generation of files for external definitions and regenerate the tests
Son Ho
4
-5
/
+50
2023-11-21
Regenerate the files
Son Ho
8
-188
/
+376
2023-11-21
Regenerate most of the test files
Son Ho
5
-54
/
+60
2023-11-09
Regenerate the Coq test files
Son Ho
5
-27
/
+27
2023-11-08
Update the Makefile and regenerate some tests
Son Ho
1
-0
/
+12
2023-10-27
Regenerate the Coq test files
Son Ho
9
-514
/
+802
2023-09-07
Regenerate the test files and fix a proof
Son Ho
2
-5
/
+15
2023-08-09
Update the nix flake and regenerate the code
Son Ho
1
-1
/
+1
2023-08-08
Regenerate the test files
Son Ho
1
-9
/
+9
2023-08-04
Update the Makefile and regenerate the test files
Son Ho
9
-6
/
+65
2023-07-06
Improve the generated comments
Son Ho
8
-153
/
+158
2023-07-05
Start using namespaces in the Lean backend
Son Ho
1
-1
/
+1
2023-06-04
Make good progress on generating code for HOL4
Son Ho
5
-64
/
+60
2023-06-04
Start updating simplify_aggregates
Son Ho
2
-7
/
+7
2023-06-04
Make sure let-bindings in Lean end with line breaks and improve formatting
Son Ho
4
-21
/
+39
2023-02-03
Improve the pretty names generation for loops
Son Ho
1
-19
/
+19
2023-02-03
Implement a pass to filter the unused input arguments in the loop functions
Son Ho
1
-11
/
+7
2023-02-03
Improve the order of the loop input parameters
Son Ho
1
-4
/
+4
[next]