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
/
LlbcAstUtils.ml
(
unfollow
)
Commit message (
Expand
)
Author
Files
Lines
2022-06-27
Add `can_end` in `abs` and use it for the return abs when generating the
Son Ho
1
-1
/
+2
2022-06-21
concrete & symbolic evaluation work with new LLBC format
Sidney Congard
1
-1
/
+0
2022-06-08
read globals from LLBC JSON into functions
Sidney Congard
1
-0
/
+1
2022-03-03
In fun_id rename the variant Local to Regular
Son Ho
1
-2
/
+2
2022-03-03
Make good progress on adding support for external and opaque
Son Ho
1
-4
/
+7
2022-03-03
Rename CFIM to LLBC
Son Ho
1
-1
/
+1
2022-03-03
Move the names from Identifiers to Names
Son Ho
1
-1
/
+1
2022-03-03
Rename TypeDef...,type_def...,FunDef,fun_def to ...Decl,...decl
Son Ho
1
-7
/
+7
2022-02-24
Update the way function names are handled
Son Ho
1
-1
/
+1
2022-02-09
Add definitions to Primitives.fst and start on improving/fixing the
Son Ho
1
-10
/
+2
2022-01-29
Make progress on PureToExtract
Son Ho
1
-0
/
+10
2022-01-28
Make minor modifications
Son Ho
1
-0
/
+10
2022-01-27
Fix some issues with the naming of input variables
Son Ho
1
-0
/
+4
2022-01-27
Fix a small issue in translate_back_ty
Son Ho
1
-0
/
+2
2022-01-26
Make progress on translation
Son Ho
1
-0
/
+32
2022-01-06
Make good progress on implementing utilities to test symbolic execution
Son Ho
1
-1
/
+4
2022-01-06
Implement statement_has_loops and make minor modifications
Son Ho
1
-0
/
+16