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
/
Synthesis.ml
(
unfollow
)
Commit message (
Expand
)
Author
Files
Lines
2022-01-21
Start working on the generation of the symbolic AST
Son Ho
1
-2
/
+2
2022-01-20
Update Interpreter
Son Ho
1
-3
/
+3
2022-01-20
Finish updating InterpreterStatements
Son Ho
1
-4
/
+0
2022-01-20
Make good progress on updating InterpreterStatements to use CPS
Son Ho
1
-5
/
+19
2022-01-06
Cleanup
Son Ho
1
-1
/
+1
2022-01-06
Fix some issues when evaluating assertions
Son Ho
1
-0
/
+6
2022-01-06
Move more definitions and do more cleanup
Son Ho
1
-0
/
+2
2022-01-06
Cleanup the dependencies a bit
Son Ho
1
-5
/
+0
2022-01-06
Address some warnings
Son Ho
1
-19
/
+20
2022-01-05
Split eval_local_function_call_symbolic to isolate a function which can
Son Ho
1
-6
/
+1
2022-01-05
Finish implementing eval_local_function_call_symbolic
Son Ho
1
-1
/
+2
2022-01-05
Make good progress on eval_local_function_call_symbolic
Son Ho
1
-1
/
+1
2022-01-05
Remove synthesize_set_discriminant
Son Ho
1
-4
/
+0
2022-01-05
Finish implementing the symbolic case of switch evaluation
Son Ho
1
-3
/
+9
2022-01-05
Implement the symbolic case of eval_rvalue_discriminant
Son Ho
1
-2
/
+11
2022-01-05
Implement eval_binary_op_symbolic
Son Ho
1
-2
/
+2
2022-01-05
Implement eval_unary_op_symbolic
Son Ho
1
-1
/
+3
2022-01-05
Update a comment
Son Ho
1
-0
/
+2
2022-01-05
Add more calls to synthesis functions
Son Ho
1
-0
/
+59