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
/
Extract.ml
(
unfollow
)
Commit message (
Expand
)
Author
Files
Lines
2024-03-08
Make progress on propagating the changes
Son Ho
1
-287
/
+157
2024-03-08
Update the code generated for tuple projectors
Son Ho
1
-18
/
+39
2024-03-08
Fix tuple indexing for Lean backend
Zyad Hassan
1
-4
/
+33
2024-03-08
Update the generation of constant bodies for Lean
Son Ho
1
-2
/
+1
2024-02-02
Start fixing the tests
Son Ho
1
-1
/
+1
2023-12-23
Fix an issue when deconstructing tuples in Coq
Son Ho
1
-2
/
+8
2023-12-22
Annotate the bound vars in the lambdas for Coq
Son Ho
1
-20
/
+36
2023-12-22
Fix a minor extraction issue
Son Ho
1
-1
/
+1
2023-12-22
Slightly update the formatting of the do blocks
Son Ho
1
-24
/
+26
2023-12-21
Update the formatting of comments
Son Ho
1
-8
/
+6
2023-12-21
Remove some asserts which are now useless
Son Ho
1
-4
/
+0
2023-12-21
Make good progress on merging the fwd/back functions
Son Ho
1
-1
/
+3
2023-12-18
Do not register the names of the back funs if they are merged with the fwd funs
Son Ho
1
-3
/
+8
2023-12-15
Make progress on propagating the changes
Son Ho
1
-4
/
+4
2023-12-15
Make progress on generalizing the signature information
Son Ho
1
-4
/
+4
2023-12-13
Update Pure.fun_sig_info
Son Ho
1
-2
/
+6
2023-12-07
Fix minor issues when extracting a structure with one field as a tuple
Son Ho
1
-21
/
+34
2023-12-07
Use a better syntax when extracting tuple types (structures with unnamed fields)
Son Ho
1
-26
/
+48
2023-11-24
Make a minor fix
Son Ho
1
-1
/
+1
2023-11-24
Update some assumed type names/variants
Son Ho
1
-6
/
+1
2023-11-22
Improve further the generation of parent clause/trait clause names
Son Ho
1
-7
/
+26
2023-11-21
Reorganize the "Extract" files
Son Ho
1
-24
/
+23
2023-11-21
Add span information to the generated code
Son Ho
1
-12
/
+19
2023-11-20
Use the name matcher implemented in Charon
Son Ho
1
-7
/
+11
2023-11-16
Finish propagating the changes to the names and cleaning
Son Ho
1
-19
/
+21
2023-11-12
Prefix variants related to types with "T"
Son Ho
1
-7
/
+7
2023-11-12
Remove the 'r type variable from the ty type definition
Son Ho
1
-13
/
+13
2023-11-09
Make the traits work for Coq
Son Ho
1
-140
/
+251
2023-11-09
Extract the trait parent clauses after the types and the constants
Son Ho
1
-24
/
+25
2023-11-09
Progress on making the traits work for F*
Son Ho
1
-9
/
+29
2023-11-09
Fix a small issue in AssociatedTypes
Son Ho
1
-2
/
+2
2023-11-07
Update the extraction
Son Ho
1
-2
/
+2
2023-11-06
Update following some changes in Charon
Son Ho
1
-22
/
+15
2023-10-26
Make progress on fixing the extraction for Lean
Son Ho
1
-1
/
+1
2023-10-26
Fix more issues at extraction and factor out defs in ExtractBuiltin
Son Ho
1
-6
/
+23
2023-10-25
Make the hashmap files typecheck again in Lean
Son Ho
1
-2391
/
+109
2023-10-25
Fix some issues at extraction and add builtins
Son Ho
1
-23
/
+22
2023-10-25
Update following the addition of raw pointers
Son Ho
1
-1
/
+4
2023-10-24
Fix an issue coming from the modification for the opaque signatures
Son Ho
1
-12
/
+7
2023-10-24
Fix a printing issue with scalar values
Son Ho
1
-3
/
+5
2023-10-24
Filter some type arguments for the builtin types/functions
Son Ho
1
-2
/
+65
2023-10-24
Remove the possibility of generating opaque module signatures
Son Ho
1
-116
/
+51
2023-10-24
Add support for builtin trait implementations
Son Ho
1
-2
/
+30
2023-10-24
Fix various issues with the builtins
Son Ho
1
-34
/
+81
2023-10-23
Make progress on handling the builtins
Son Ho
1
-42
/
+212
2023-10-23
Remove some assumed types and add more support for builtin definitions
Son Ho
1
-68
/
+77
2023-10-22
Add more support for numeric operations, xor, rotate
Jonathan Protzenko
1
-4
/
+7
2023-10-20
Start updating to handle function pointers
Son Ho
1
-2
/
+2
2023-10-16
Improve formatting of scalars in Lean
Son Ho
1
-23
/
+10
2023-10-13
Add sup
Son Ho
1
-1
/
+3
[next]