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
/
Interpreter.ml
(
follow
)
Commit message (
Expand
)
Author
Age
Files
Lines
*
Cleanup a bit Interpreter.ml
Son Ho
2021-11-30
1
-20
/
+17
*
Remove the vector type for the Id module
Son Ho
2021-11-30
1
-140
/
+68
*
Debug box_free
Son Ho
2021-11-30
1
-61
/
+87
*
Fix an issue
Son Ho
2021-11-30
1
-15
/
+55
*
Replace the env parameters/return types with eval_ctx in many functions
Son Ho
2021-11-30
1
-163
/
+166
*
Make minor modifications
Son Ho
2021-11-30
1
-27
/
+71
*
Fix another bug
Son Ho
2021-11-30
1
-4
/
+10
*
Fix more bugs
Son Ho
2021-11-30
1
-7
/
+42
*
Fix another bug
Son Ho
2021-11-30
1
-1
/
+5
*
Fix another bug
Son Ho
2021-11-30
1
-1
/
+4
*
Add more debugging facilities
Son Ho
2021-11-30
1
-1
/
+10
*
Fix another bug
Son Ho
2021-11-30
1
-4
/
+8
*
Debug some issues in the interpreter
Son Ho
2021-11-30
1
-2
/
+24
*
Debug some issues
Son Ho
2021-11-29
1
-6
/
+13
*
Start deriving formatters for debugging
Son Ho
2021-11-29
1
-9
/
+21
*
Fix a small mistake
Son Ho
2021-11-29
1
-3
/
+1
*
Improve formatting
Son Ho
2021-11-29
1
-2
/
+2
*
Start fixing bugs in the unit test evaluation
Son Ho
2021-11-29
1
-1
/
+7
*
Fix some issues, introduce debugging log in the interpreter
Son Ho
2021-11-29
1
-1
/
+20
*
Test the unit functions
Son Ho
2021-11-29
1
-6
/
+6
*
Start working logging and make progress on printing ASTs
Son Ho
2021-11-29
1
-0
/
+1
*
Cleanup a bit to remove the warnings
Son Ho
2021-11-29
1
-11
/
+23
*
Implement test_all_unit_functions
Son Ho
2021-11-26
1
-5
/
+26
*
Implement test_unit_function
Son Ho
2021-11-26
1
-0
/
+32
*
Implement box dereferencement (concrete interpreter)
Son Ho
2021-11-26
1
-8
/
+42
*
Make progress on evaluate_non_local_function_call
Son Ho
2021-11-26
1
-21
/
+165
*
Add some comments
Son Ho
2021-11-26
1
-0
/
+10
*
Implement eval_expression
Son Ho
2021-11-26
1
-4
/
+72
*
Make good progress on eval_local_function_call
Son Ho
2021-11-26
1
-28
/
+114
*
Update the way operands and assignments are evaluated
Son Ho
2021-11-26
1
-114
/
+74
*
Update the env definition to make the frames easier to manipulate
Son Ho
2021-11-26
1
-14
/
+26
*
Start working on eval_local_function_call
Son Ho
2021-11-25
1
-11
/
+47
*
Start working on function calls
Son Ho
2021-11-25
1
-0
/
+23
*
Finish the implementation of set_discriminant
Son Ho
2021-11-25
1
-3
/
+10
*
Implement the Adt case of set_discriminant
Son Ho
2021-11-25
1
-5
/
+26
*
Start working on set_discriminant and factorize a bit
Son Ho
2021-11-25
1
-36
/
+88
*
Implement the assertion case of eval_statement
Son Ho
2021-11-25
1
-1
/
+7
*
Implement the Drop case of eval_statement
Son Ho
2021-11-25
1
-1
/
+6
*
Make progress on eval_statement
Son Ho
2021-11-25
1
-12
/
+12
*
Implement the Assign case of eval_statement
Son Ho
2021-11-25
1
-6
/
+75
*
Replace `open Types` by `module T = Types` in Interpreter.ml
Son Ho
2021-11-25
1
-89
/
+88
*
Replace `open Values` with `module V = Values` in Interpreter
Son Ho
2021-11-25
1
-384
/
+412
*
Replace `open Expressions` by `module E = Expressions` in Interpreter.ml
Son Ho
2021-11-25
1
-65
/
+67
*
Replace `open Contexts` by `module C = Contexts` in Interpreter.ml
Son Ho
2021-11-25
1
-138
/
+108
*
Start working on eval_statement
Son Ho
2021-11-25
1
-0
/
+20
*
Implement the Aggregate branch of eval_rvalue
Son Ho
2021-11-25
1
-12
/
+29
*
Take care of warnings and fix some mistakes
Son Ho
2021-11-25
1
-18
/
+23
*
Start working on type substitution
Son Ho
2021-11-25
1
-0
/
+2
*
Make progress on eval_rvalue and update aggregate_kind
Son Ho
2021-11-24
1
-14
/
+83
*
Implement the discriminant case of eval_rvalue
Son Ho
2021-11-24
1
-5
/
+21
[next]