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
/
ExtractBase.ml
(
follow
)
Commit message (
Expand
)
Author
Age
Files
Lines
*
resolved requested changes
Escherichia
2024-04-03
1
-1
/
+0
*
resolved requested changes
Escherichia
2024-04-03
1
-1
/
+1
*
added Error and EError to expressions and propagated related changes
Escherichia
2024-04-03
1
-1
/
+3
*
formatting and changed save_error condition for failing from b to not b
Escherichia
2024-03-29
1
-4
/
+3
*
added file and line arg to craise, cassert and all related functions
Escherichia
2024-03-29
1
-3
/
+3
*
added file and line arg to craise and cassert
Escherichia
2024-03-29
1
-16
/
+17
*
Revert some changes which shouldn't be here
Son Ho
2024-03-28
1
-6
/
+5
*
formatting
Escherichia
2024-03-28
1
-104
/
+133
*
changes after git rebase main
Escherichia
2024-03-28
1
-8
/
+16
*
Should answer all comments, there are still some TODO: error message left
Escherichia
2024-03-28
1
-46
/
+42
*
Added sanity_check and sanity_check_opt_meta helpers and changed sanity check...
Escherichia
2024-03-28
1
-1
/
+1
*
changes to extract_ty and related functions to use the right meta
Escherichia
2024-03-28
1
-18
/
+11
*
added a meta option field to norm_ctx and changed the meta used by some asser...
Escherichia
2024-03-28
1
-1
/
+0
*
Replaced some unclear TODOs error message placeholder by clearer TODOs, they ...
Escherichia
2024-03-28
1
-2
/
+2
*
Still need to fill the TODO: error message and check some meta but it builds
Escherichia
2024-03-28
1
-39
/
+39
*
WIP: translate.ml and extract.ml do not compile. Some assert left to do and w...
Escherichia
2024-03-28
1
-136
/
+139
*
Update following changes in Charon
Son Ho
2024-03-17
1
-1
/
+1
*
Update the generation of names
Son Ho
2024-03-11
1
-6
/
+15
*
Update the name generation and add CLI to print external pat names
Son Ho
2024-03-10
1
-6
/
+12
*
Make progress on propagating the changes
Son Ho
2024-03-08
1
-139
/
+22
*
Remove the option to split fwd/back functions and update SymbolicToPure
Son Ho
2024-03-08
1
-59
/
+23
*
Update the code generation
Son Ho
2024-03-08
1
-2
/
+6
*
Fix minor issues
Son Ho
2023-12-22
1
-27
/
+54
*
Use indices starting at 1 to make variable names unique at code gen
Son Ho
2023-12-21
1
-1
/
+1
*
Update the extraction to handle casts between integers/bools
Son Ho
2023-12-13
1
-1
/
+9
*
Use a better syntax when extracting tuple types (structures with unnamed fields)
Son Ho
2023-12-07
1
-8
/
+9
*
Update following changes in Charon
Son Ho
2023-12-05
1
-1
/
+1
*
Add support for more bitwise operations and update the extraction
Son Ho
2023-11-29
1
-7
/
+5
*
Fix the issues with the cross-references for OCaml doc
Son Ho
2023-11-27
1
-3
/
+3
*
Add the alloc::string::String type in the builtins
Son Ho
2023-11-24
1
-2
/
+3
*
Update a comment
Son Ho
2023-11-24
1
-2
/
+3
*
Update some assumed type names/variants
Son Ho
2023-11-24
1
-28
/
+40
*
Improve the error messages for some name collisions
Son Ho
2023-11-24
1
-2
/
+4
*
Improve further the generation of parent clause/trait clause names
Son Ho
2023-11-22
1
-27
/
+75
*
Improve the generation of parent clause names
Son Ho
2023-11-21
1
-4
/
+19
*
Update the generation of names for the parent trait clauses
Son Ho
2023-11-21
1
-4
/
+29
*
Reorganize the "Extract" files
Son Ho
2023-11-21
1
-510
/
+1125
*
Use the name matcher implemented in Charon
Son Ho
2023-11-20
1
-2
/
+1
*
Start updating the name type, cleanup the names and the module abbrevs
Son Ho
2023-11-15
1
-138
/
+54
*
Add RegionsHierarchy.ml
Son Ho
2023-11-13
1
-2
/
+6
*
Prefix variants related to types with "T"
Son Ho
2023-11-12
1
-13
/
+14
*
Remove the 'r type variable from the ty type definition
Son Ho
2023-11-12
1
-27
/
+27
*
Make the traits work for Coq
Son Ho
2023-11-09
1
-0
/
+8
*
Fix a small issue in AssociatedTypes
Son Ho
2023-11-09
1
-6
/
+6
*
Fix minor issues in the name collision detection
Son Ho
2023-10-27
1
-9
/
+23
*
Make minor modifications and update the array test for F*
Son Ho
2023-10-26
1
-12
/
+10
*
Make progress on fixing the extraction for Lean
Son Ho
2023-10-26
1
-63
/
+102
*
Make the hashmap files typecheck again in Lean
Son Ho
2023-10-25
1
-0
/
+2
*
Update following the addition of raw pointers
Son Ho
2023-10-25
1
-2
/
+3
*
Handle properly the builtin, non fallible functions
Son Ho
2023-10-24
1
-2
/
+2
[next]