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
/
SynthesizeSymbolic.ml
(
follow
)
Commit message (
Collapse
)
Author
Age
Files
Lines
*
Corrected translation without using functions, remaining bug in hashmap ↵
Sidney Congard
2022-08-10
1
-0
/
+6
|
|
|
|
translation
*
Improve the generation of names for given back values
Son Ho
2022-04-21
1
-3
/
+3
|
*
Rename CFIM to LLBC
Son Ho
2022-03-03
1
-1
/
+1
|
*
Remove the Aggregated variant from SymbolicAst.meta as it is included in
Son Ho
2022-01-28
1
-6
/
+0
|
|
|
|
the Assignment variant
*
Generate meta-information for assignments in the symbolic AST
Son Ho
2022-01-27
1
-0
/
+6
|
*
Rename the meta-places to [mplace] and update some comments
Son Ho
2022-01-27
1
-19
/
+23
|
*
Add meta information for the variable names in SymbolicAst
Son Ho
2022-01-27
1
-16
/
+45
|
*
Cleanup a bit by removing useless `open`
Son Ho
2022-01-27
1
-2
/
+0
|
*
Make progress on SymbolicToPure.translate_end_abstraction
Son Ho
2022-01-25
1
-8
/
+11
|
*
Make good progress on SymbolicToPure.translate_expansion
Son Ho
2022-01-25
1
-23
/
+16
|
*
Finish updating the calls to the synthesis functions to generate the
Son Ho
2022-01-21
1
-2
/
+38
|
|
|
|
symbolic AST
*
Start working on the generation of the symbolic AST
Son Ho
2022-01-21
1
-0
/
+89