index
:
aeneas
isabelle
aeneas rust verifier with a hacky Isabelle backend
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
src
/
Substitute.ml
(
follow
)
Commit message (
Collapse
)
Author
Age
Files
Lines
*
Make good progress on adding support for external and opaque
Son Ho
2022-03-03
1
-4
/
+4
|
|
|
|
declarations
*
Rename CFIM to LLBC
Son Ho
2022-03-03
1
-1
/
+1
|
*
Add an Opaque variant to type_decl_kind and start updating the code
Son Ho
2022-03-03
1
-0
/
+2
|
*
Rename TypeDef...,type_def...,FunDef,fun_def to ...Decl,...decl
Son Ho
2022-03-03
1
-13
/
+13
|
*
Start adding more assumed types and functions
Son Ho
2022-02-08
1
-2
/
+8
|
*
Implement sanity checks to check the types of the input/output arguments
Son Ho
2022-01-26
1
-1
/
+4
|
|
|
|
given to backward functions
*
Update the types and deserialization following charon's updates
Son Ho
2022-01-18
1
-6
/
+6
|
*
Make the symbolic, borrow, region and abstration counters global and
Son Ho
2022-01-06
1
-8
/
+4
|
|
|
|
stateful
*
Implement statement_has_loops and make minor modifications
Son Ho
2022-01-06
1
-1
/
+0
|
*
Cleanup a bit
Son Ho
2022-01-05
1
-0
/
+2
|
*
Make good progress on eval_local_function_call_symbolic
Son Ho
2022-01-05
1
-0
/
+50
|
*
Implement compute_expanded_symbolic_adt_value
Son Ho
2022-01-04
1
-0
/
+28
|
*
Implement apply_proj_borrows_on_shared_borrow
Son Ho
2021-12-17
1
-0
/
+21
|
*
Rename some functions
Son Ho
2021-12-17
1
-4
/
+4
|
*
Add more field type instantiation functions for the ADTs
Son Ho
2021-12-17
1
-1
/
+40
|
*
Rename some functions
Son Ho
2021-12-17
1
-3
/
+3
|
*
Use RegionVarId and RegionId in a more consistent manner
Son Ho
2021-12-17
1
-2
/
+2
|
*
Merge the ADTs, tuples and assumed types in the type and value
Son Ho
2021-12-01
1
-6
/
+3
|
|
|
|
definitions
*
Factorize type_var and region_var
Son Ho
2021-12-01
1
-1
/
+1
|
*
Reimplement [erase_regions] with the substitution functions
Son Ho
2021-12-01
1
-0
/
+4
|
*
Move some definitions to new files
Son Ho
2021-12-01
1
-1
/
+2
|
*
Move the var definition
Son Ho
2021-12-01
1
-2
/
+2
|
*
Merge statements and expressions into statements
Son Ho
2021-12-01
1
-17
/
+11
|
*
Remove the vector type for the Id module
Son Ho
2021-11-30
1
-11
/
+6
|
*
Test the unit functions
Son Ho
2021-11-29
1
-1
/
+1
|
*
Make various improvements in Print
Son Ho
2021-11-29
1
-18
/
+0
|
*
Start working logging and make progress on printing ASTs
Son Ho
2021-11-29
1
-1
/
+1
|
*
Update the env definition to make the frames easier to manipulate
Son Ho
2021-11-26
1
-0
/
+1
|
*
Implement type substitution for function definitions (and expressions,
Son Ho
2021-11-25
1
-1
/
+122
|
|
|
|
etc.)
*
Start working on function calls
Son Ho
2021-11-25
1
-4
/
+23
|
*
Implement the Aggregate branch of eval_rvalue
Son Ho
2021-11-25
1
-1
/
+9
|
*
Implement various substitution functions
Son Ho
2021-11-25
1
-42
/
+54
|
*
Commit Substitute.ml (forgotten in previous commit)
Son Ho
2021-11-25
1
-0
/
+72