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
/
SymbolicAst.ml
(
follow
)
Commit message (
Collapse
)
Author
Age
Files
Lines
*
Introduce the App expression, and make progress updating the code
Son Ho
2022-04-26
1
-1
/
+1
|
*
Improve the generation of names for given back values
Son Ho
2022-04-21
1
-2
/
+2
|
*
Rename CFIM to LLBC
Son Ho
2022-03-03
1
-1
/
+1
|
*
Cleanup a bit
Son Ho
2022-02-03
1
-1
/
+0
|
*
Remove the Aggregated variant from SymbolicAst.meta as it is included in
Son Ho
2022-01-28
1
-2
/
+0
|
|
|
|
the Assignment variant
*
Generate meta-information for the assignments
Son Ho
2022-01-28
1
-10
/
+10
|
*
Generate meta-information for assignments in the symbolic AST
Son Ho
2022-01-27
1
-0
/
+2
|
*
Rename the meta-places to [mplace] and update some comments
Son Ho
2022-01-27
1
-6
/
+6
|
*
Add meta information for the variable names in SymbolicAst
Son Ho
2022-01-27
1
-2
/
+33
|
*
Make more progress on generating the symbolic AST for the backward
Son Ho
2022-01-26
1
-3
/
+5
|
|
|
|
functions
*
Make progress on SymbolicToPure.translate_end_abstraction
Son Ho
2022-01-25
1
-0
/
+1
|
*
Make good progress on SymbolicToPure.translate_expansion
Son Ho
2022-01-25
1
-5
/
+8
|
*
Implement SymbolicToPure.translate_fun_sig
Son Ho
2022-01-25
1
-3
/
+9
|
*
Make minor modifications
Son Ho
2022-01-24
1
-0
/
+1
|
*
Finish updating the calls to the synthesis functions to generate the
Son Ho
2022-01-21
1
-4
/
+10
|
|
|
|
symbolic AST
*
Start working on the generation of the symbolic AST
Son Ho
2022-01-21
1
-0
/
+47