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
9512
log
plain
-rw-r--r--
Collections.ml
11104
log
plain
-rw-r--r--
ConstStrings.ml
217
log
plain
-rw-r--r--
Contexts.ml
16641
log
plain
-rw-r--r--
Cps.ml
6713
log
plain
-rw-r--r--
Crates.ml
2918
log
plain
-rw-r--r--
Errors.ml
58
log
plain
-rw-r--r--
Expressions.ml
2730
log
plain
-rw-r--r--
ExpressionsUtils.ml
338
log
plain
-rw-r--r--
ExtractToFStar.ml
57836
log
plain
-rw-r--r--
FunsAnalysis.ml
5576
log
plain
-rw-r--r--
Identifiers.ml
3759
log
plain
-rw-r--r--
Interpreter.ml
15526
log
plain
-rw-r--r--
InterpreterBorrows.ml
67236
log
plain
-rw-r--r--
InterpreterBorrowsCore.ml
41283
log
plain
-rw-r--r--
InterpreterExpansion.ml
30071
log
plain
-rw-r--r--
InterpreterExpressions.ml
27882
log
plain
-rw-r--r--
InterpreterPaths.ml
33258
log
plain
-rw-r--r--
InterpreterProjectors.ml
22313
log
plain
-rw-r--r--
InterpreterStatements.ml
53269
log
plain
-rw-r--r--
InterpreterUtils.ml
7888
log
plain
-rw-r--r--
Invariants.ml
30815
log
plain
-rw-r--r--
LlbcAst.ml
5822
log
plain
-rw-r--r--
LlbcAstUtils.ml
2378
log
plain
-rw-r--r--
LlbcOfJson.ml
29233
log
plain
-rw-r--r--
Logging.ml
4929
log
plain
-rw-r--r--
Names.ml
3126
log
plain
-rw-r--r--
OfJsonBasic.ml
2334
log
plain
-rw-r--r--
PrePasses.ml
1606
log
plain
-rw-r--r--
Print.ml
48524
log
plain
-rw-r--r--
PrintPure.ml
23163
log
plain
-rw-r--r--
PrintSymbolicAst.ml
1568
log
plain
-rw-r--r--
Pure.ml
19889
log
plain
-rw-r--r--
PureMicroPasses.ml
53621
log
plain
-rw-r--r--
PureToExtract.ml
26542
log
plain
-rw-r--r--
PureTypeCheck.ml
7065
log
plain
-rw-r--r--
PureUtils.ml
14980
log
plain
-rw-r--r--
Scalars.ml
2338
log
plain
-rw-r--r--
StringUtils.ml
3370
log
plain
-rw-r--r--
Substitute.ml
13550
log
plain
-rw-r--r--
SymbolicAst.ml
3818
log
plain
-rw-r--r--
SymbolicToPure.ml
72951
log
plain
-rw-r--r--
SynthesizeSymbolic.ml
6225
log
plain
-rw-r--r--
Translate.ml
30779
log
plain
-rw-r--r--
TranslateCore.ml
2161
log
plain
-rw-r--r--
Types.ml
5836
log
plain
-rw-r--r--
TypesAnalysis.ml
12142
log
plain
-rw-r--r--
TypesUtils.ml
6598
log
plain
-rw-r--r--
Utils.ml
191
log
plain
-rw-r--r--
Values.ml
31484
log
plain
-rw-r--r--
ValuesUtils.ml
3270
log
plain
-rw-r--r--
dune
430
log
plain
-rw-r--r--
main.ml
6945
log
plain