index
:
aeneas
isabelle
aeneas rust verifier with a hacky Isabelle backend
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
compiler
Mode
Name
Size
-rw-r--r--
.ocamlformat
19
log
plain
-rw-r--r--
Assumed.ml
9522
log
plain
-rw-r--r--
Collections.ml
11106
log
plain
-rw-r--r--
ConstStrings.ml
217
log
plain
-rw-r--r--
Contexts.ml
16629
log
plain
-rw-r--r--
Cps.ml
6742
log
plain
-rw-r--r--
Crates.ml
2918
log
plain
-rw-r--r--
Errors.ml
58
log
plain
-rw-r--r--
Expressions.ml
2734
log
plain
-rw-r--r--
ExpressionsUtils.ml
338
log
plain
-rw-r--r--
ExtractToFStar.ml
57851
log
plain
-rw-r--r--
FunsAnalysis.ml
5576
log
plain
-rw-r--r--
Identifiers.ml
3762
log
plain
-rw-r--r--
Interpreter.ml
15528
log
plain
-rw-r--r--
InterpreterBorrows.ml
67205
log
plain
-rw-r--r--
InterpreterBorrowsCore.ml
41323
log
plain
-rw-r--r--
InterpreterExpansion.ml
30078
log
plain
-rw-r--r--
InterpreterExpressions.ml
27886
log
plain
-rw-r--r--
InterpreterPaths.ml
33291
log
plain
-rw-r--r--
InterpreterProjectors.ml
22324
log
plain
-rw-r--r--
InterpreterStatements.ml
53313
log
plain
-rw-r--r--
InterpreterUtils.ml
7901
log
plain
-rw-r--r--
Invariants.ml
30817
log
plain
-rw-r--r--
LlbcAst.ml
6137
log
plain
-rw-r--r--
LlbcAstUtils.ml
2407
log
plain
-rw-r--r--
LlbcOfJson.ml
33959
log
plain
-rw-r--r--
Logging.ml
5072
log
plain
-rw-r--r--
Meta.ml
1423
log
plain
-rw-r--r--
Names.ml
3120
log
plain
-rw-r--r--
OfJsonBasic.ml
2334
log
plain
-rw-r--r--
PrePasses.ml
1670
log
plain
-rw-r--r--
Print.ml
48714
log
plain
-rw-r--r--
PrintPure.ml
23163
log
plain
-rw-r--r--
Pure.ml
19899
log
plain
-rw-r--r--
PureMicroPasses.ml
53666
log
plain
-rw-r--r--
PureToExtract.ml
26742
log
plain
-rw-r--r--
PureTypeCheck.ml
7065
log
plain
-rw-r--r--
PureUtils.ml
14990
log
plain
-rw-r--r--
Scalars.ml
2338
log
plain
-rw-r--r--
StringUtils.ml
3388
log
plain
-rw-r--r--
Substitute.ml
13737
log
plain
-rw-r--r--
SymbolicAst.ml
3819
log
plain
-rw-r--r--
SymbolicToPure.ml
72919
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
5891
log
plain
-rw-r--r--
TypesAnalysis.ml
12144
log
plain
-rw-r--r--
TypesUtils.ml
6658
log
plain
-rw-r--r--
Utils.ml
191
log
plain
-rw-r--r--
Values.ml
31571
log
plain
-rw-r--r--
ValuesUtils.ml
3270
log
plain
-rw-r--r--
aeneas.opam
643
log
plain
-rw-r--r--
driver.ml
7355
log
plain
-rw-r--r--
dune
1477
log
plain
-rw-r--r--
dune-project
371
log
plain
d---------
fstar
42
log
plain