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
(
follow
)
Commit message (
Expand
)
Author
Age
Files
Lines
*
Fix the semantics of drop
Son Ho
2022-10-20
3
-4
/
+31
*
Rename Modules to Crates
Son Ho
2022-10-13
13
-77
/
+74
*
Reformat the project with dune
Son Ho
2022-09-22
18
-234
/
+58
*
Remove a useless file
Son Ho
2022-09-22
1
-57
/
+0
*
Make minor cleanup
Son Ho
2022-09-22
2
-22
/
+12
*
Add some comments
Son Ho
2022-09-22
1
-0
/
+3
*
Update the name registration for globals
Son Ho
2022-09-22
2
-6
/
+12
*
Update PureMicroPasses.inline_useless_var_reassignments
Son Ho
2022-09-22
2
-34
/
+39
*
Make minor cleanup
Son Ho
2022-09-22
11
-131
/
+135
*
Make minor modifications
Son Ho
2022-09-22
6
-107
/
+117
*
Update FunsAnalysis
Son Ho
2022-09-22
1
-24
/
+26
*
Update src/ExtractToFStar.ml
Son HO
2022-09-22
1
-1
/
+1
*
Update src/FunsAnalysis.ml
Son HO
2022-09-22
1
-0
/
+1
*
Update src/FunsAnalysis.ml
Son HO
2022-09-22
1
-1
/
+1
*
Update src/ExtractToFStar.ml
Son HO
2022-09-22
1
-1
/
+1
*
Update src/ExtractToFStar.ml
Son HO
2022-09-22
1
-1
/
+0
*
Update src/ExtractToFStar.ml
Son HO
2022-09-22
1
-1
/
+1
*
Update src/ExtractToFStar.ml
Son HO
2022-09-22
1
-1
/
+1
*
Update src/ExtractToFStar.ml
Son HO
2022-09-22
1
-1
/
+1
*
Update src/ExtractToFStar.ml
Son HO
2022-09-22
1
-1
/
+1
*
Update src/ExtractToFStar.ml
Son HO
2022-09-22
1
-1
/
+1
*
Update src/ExtractToFStar.ml
Son HO
2022-09-22
1
-1
/
+1
*
Update src/SymbolicAst.ml
Son HO
2022-09-22
1
-1
/
+1
*
Update src/TypesUtils.ml
Son HO
2022-09-22
1
-1
/
+1
*
Update src/Translate.ml
Son HO
2022-09-22
1
-1
/
+1
*
Correct last PR remarks
Sidney Congard
2022-08-11
2
-23
/
+17
*
Correct assertion for stateless globals
Sidney Congard
2022-08-11
1
-1
/
+1
*
Corrected translation without using functions, remaining bug in hashmap trans...
Sidney Congard
2022-08-10
8
-24
/
+31
*
Register global names, one error remaining
Sidney Congard
2022-08-08
4
-4
/
+23
*
Create global declaration group, address PR changes but introduce bugs
Sidney Congard
2022-07-29
10
-83
/
+134
*
Always put can_fail to true, specialize global traduction to concrete functio...
Sidney Congard
2022-07-28
2
-9
/
+18
*
Apply minor changes from PR comments
Sidney Congard
2022-07-25
5
-17
/
+23
*
Address much stuff of the PR, throw exceptions at remaining places
Sidney Congard
2022-07-18
16
-112
/
+172
*
Apply small changes from the PR
Sidney Congard
2022-07-13
4
-9
/
+12
*
Remove last prints, adapt JSON
Sidney Congard
2022-07-05
2
-6
/
+3
*
Merge branch 'main' of github.com:Kachoc/aeneas into constants-v2
Sidney Congard
2022-06-30
14
-178
/
+328
|
\
|
*
Take failing rvalues into account in FunsAnalysis.analyze_fun_decls
Son Ho
2022-06-30
4
-19
/
+22
|
*
Make minor modifications
Son Ho
2022-06-29
4
-6
/
+46
|
*
Add `can_end` in `abs` and use it for the return abs when generating the
Son Ho
2022-06-27
5
-33
/
+59
|
*
Update eval_operand_prepare to not give a value to the continuation
Son Ho
2022-06-27
4
-109
/
+181
*
|
Traduct globals body separately (WIP)
Sidney Congard
2022-06-30
11
-66
/
+208
*
|
adapt to new LLBC (without OperandConstantValue)
Sidney Congard
2022-06-23
2
-33
/
+27
*
|
concrete & symbolic evaluation work with new LLBC format
Sidney Congard
2022-06-21
22
-307
/
+260
*
|
crude generation working - missing unit tests & special constants handling
Sidney Congard
2022-06-13
5
-52
/
+70
*
|
read globals from LLBC JSON into functions
Sidney Congard
2022-06-08
20
-80
/
+161
|
/
*
Fix an issue when extracting assumed values
Son Ho
2022-05-16
1
-1
/
+1
*
Add a pass to cleanup the deconstructed ADTs and fix a small issue
Son Ho
2022-05-15
3
-12
/
+112
*
Treat integer casts in a general manner
Son Ho
2022-05-15
9
-50
/
+75
*
Add AggregatedOption
Son Ho
2022-05-15
5
-8
/
+37
*
Make minor modifications
Son Ho
2022-05-10
3
-8
/
+10
[next]