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
Mode
Name
Size
-rw-r--r--
Assumed.ml
9524
log
plain
-rw-r--r--
Collections.ml
10875
log
plain
-rw-r--r--
ConstStrings.ml
217
log
plain
-rw-r--r--
Contexts.ml
16342
log
plain
-rw-r--r--
Cps.ml
5510
log
plain
-rw-r--r--
Errors.ml
59
log
plain
-rw-r--r--
Expressions.ml
3655
log
plain
-rw-r--r--
ExtractAst.ml
1807
log
plain
-rw-r--r--
ExtractToFStar.ml
53562
log
plain
-rw-r--r--
FunIdentifier.ml
45
log
plain
-rw-r--r--
FunsAnalysis.ml
3952
log
plain
-rw-r--r--
Identifiers.ml
3791
log
plain
-rw-r--r--
Interpreter.ml
14334
log
plain
-rw-r--r--
InterpreterBorrows.ml
66528
log
plain
-rw-r--r--
InterpreterBorrowsCore.ml
41288
log
plain
-rw-r--r--
InterpreterExpansion.ml
29897
log
plain
-rw-r--r--
InterpreterExpressions.ml
26522
log
plain
-rw-r--r--
InterpreterPaths.ml
33053
log
plain
-rw-r--r--
InterpreterProjectors.ml
22313
log
plain
-rw-r--r--
InterpreterStatements.ml
51993
log
plain
-rw-r--r--
InterpreterUtils.ml
7954
log
plain
-rw-r--r--
Invariants.ml
30818
log
plain
-rw-r--r--
LlbcAst.ml
5302
log
plain
-rw-r--r--
LlbcAstUtils.ml
2345
log
plain
-rw-r--r--
LlbcOfJson.ml
29168
log
plain
-rw-r--r--
Logging.ml
4929
log
plain
-rw-r--r--
Modules.ml
2422
log
plain
-rw-r--r--
Names.ml
3082
log
plain
-rw-r--r--
OfJsonBasic.ml
2334
log
plain
-rw-r--r--
PrePasses.ml
1617
log
plain
-rw-r--r--
Print.ml
48712
log
plain
-rw-r--r--
PrintPure.ml
23047
log
plain
-rw-r--r--
PrintSymbolicAst.ml
1587
log
plain
-rw-r--r--
Pure.ml
19780
log
plain
-rw-r--r--
PureMicroPasses.ml
53515
log
plain
-rw-r--r--
PureToExtract.ml
25645
log
plain
-rw-r--r--
PureTypeCheck.ml
6941
log
plain
-rw-r--r--
PureUtils.ml
14976
log
plain
-rw-r--r--
Scalars.ml
2360
log
plain
-rw-r--r--
StringUtils.ml
3370
log
plain
-rw-r--r--
Substitute.ml
13755
log
plain
-rw-r--r--
SymbolicAst.ml
3693
log
plain
-rw-r--r--
SymbolicToPure.ml
71612
log
plain
-rw-r--r--
SynthesizeSymbolic.ml
6016
log
plain
-rw-r--r--
Translate.ml
29372
log
plain
-rw-r--r--
TranslateCore.ml
1943
log
plain
-rw-r--r--
Types.ml
5853
log
plain
-rw-r--r--
TypesAnalysis.ml
12143
log
plain
-rw-r--r--
TypesUtils.ml
6596
log
plain
-rw-r--r--
Utils.ml
191
log
plain
-rw-r--r--
Values.ml
30943
log
plain
-rw-r--r--
ValuesUtils.ml
3276
log
plain
-rw-r--r--
dune
435
log
plain
-rw-r--r--
main.ml
6946
log
plain