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
27
log
plain
-rw-r--r--
Config.ml
10143
log
plain
-rw-r--r--
ConstStrings.ml
342
log
plain
-rw-r--r--
Contexts.ml
17993
log
plain
-rw-r--r--
Cps.ml
7091
log
plain
-rw-r--r--
Driver.ml
6744
log
plain
-rw-r--r--
Expressions.ml
27
log
plain
-rw-r--r--
ExpressionsUtils.ml
32
log
plain
-rw-r--r--
Extract.ml
80240
log
plain
-rw-r--r--
ExtractBase.ml
30006
log
plain
-rw-r--r--
FunsAnalysis.ml
5958
log
plain
-rw-r--r--
Identifiers.ml
27
log
plain
-rw-r--r--
Interpreter.ml
15695
log
plain
-rw-r--r--
InterpreterBorrows.ml
100329
log
plain
-rw-r--r--
InterpreterBorrows.mli
7451
log
plain
-rw-r--r--
InterpreterBorrowsCore.ml
41781
log
plain
-rw-r--r--
InterpreterExpansion.ml
29497
log
plain
-rw-r--r--
InterpreterExpansion.mli
3290
log
plain
-rw-r--r--
InterpreterExpressions.ml
28147
log
plain
-rw-r--r--
InterpreterExpressions.mli
2486
log
plain
-rw-r--r--
InterpreterLoops.ml
70201
log
plain
-rw-r--r--
InterpreterPaths.ml
26509
log
plain
-rw-r--r--
InterpreterPaths.mli
4055
log
plain
-rw-r--r--
InterpreterProjectors.ml
21511
log
plain
-rw-r--r--
InterpreterProjectors.mli
3896
log
plain
-rw-r--r--
InterpreterStatements.ml
52802
log
plain
-rw-r--r--
InterpreterStatements.mli
2242
log
plain
-rw-r--r--
InterpreterUtils.ml
11188
log
plain
-rw-r--r--
Invariants.ml
30945
log
plain
-rw-r--r--
LlbcAst.ml
398
log
plain
-rw-r--r--
LlbcAstUtils.ml
489
log
plain
-rw-r--r--
LlbcOfJson.ml
26
log
plain
-rw-r--r--
Logging.ml
1663
log
plain
-rw-r--r--
Meta.ml
20
log
plain
-rw-r--r--
Names.ml
21
log
plain
-rw-r--r--
PrePasses.ml
4850
log
plain
-rw-r--r--
PrimitiveValues.ml
31
log
plain
-rw-r--r--
Print.ml
23220
log
plain
-rw-r--r--
PrintPure.ml
25065
log
plain
-rw-r--r--
Pure.ml
22330
log
plain
-rw-r--r--
PureMicroPasses.ml
55697
log
plain
-rw-r--r--
PureTypeCheck.ml
7545
log
plain
-rw-r--r--
PureUtils.ml
16923
log
plain
-rw-r--r--
Scalars.ml
23
log
plain
-rw-r--r--
StringUtils.ml
3388
log
plain
-rw-r--r--
Substitute.ml
18077
log
plain
-rw-r--r--
SymbolicAst.ml
4818
log
plain
-rw-r--r--
SymbolicToPure.ml
82479
log
plain
-rw-r--r--
SynthesizeSymbolic.ml
6577
log
plain
-rw-r--r--
Translate.ml
32201
log
plain
-rw-r--r--
TranslateCore.ml
2161
log
plain
-rw-r--r--
Types.ml
21
log
plain
-rw-r--r--
TypesAnalysis.ml
12155
log
plain
-rw-r--r--
TypesUtils.ml
1177
log
plain
-rw-r--r--
Utils.ml
21
log
plain
-rw-r--r--
Values.ml
36970
log
plain
-rw-r--r--
ValuesUtils.ml
5907
log
plain
-rw-r--r--
aeneas.opam
711
log
plain
-rw-r--r--
dune
1382
log
plain
-rw-r--r--
dune-project
357
log
plain