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--
.gitignore
7
log
plain
-rw-r--r--
.ocamlformat
19
log
plain
-rw-r--r--
AssociatedTypes.ml
23755
log
plain
-rw-r--r--
Assumed.ml
9367
log
plain
-rw-r--r--
Collections.ml
27
log
plain
-rw-r--r--
Config.ml
12868
log
plain
-rw-r--r--
ConstStrings.ml
342
log
plain
-rw-r--r--
Contexts.ml
20673
log
plain
-rw-r--r--
Cps.ml
7549
log
plain
-rw-r--r--
Expressions.ml
27
log
plain
-rw-r--r--
ExpressionsUtils.ml
32
log
plain
-rw-r--r--
Extract.ml
103186
log
plain
-rw-r--r--
ExtractBase.ml
73796
log
plain
-rw-r--r--
ExtractBuiltin.ml
19939
log
plain
-rw-r--r--
ExtractName.ml
4110
log
plain
-rw-r--r--
ExtractTypes.ml
66834
log
plain
-rw-r--r--
FunsAnalysis.ml
8479
log
plain
-rw-r--r--
Identifiers.ml
27
log
plain
-rw-r--r--
Interpreter.ml
25242
log
plain
-rw-r--r--
InterpreterBorrows.ml
104528
log
plain
-rw-r--r--
InterpreterBorrows.mli
7672
log
plain
-rw-r--r--
InterpreterBorrowsCore.ml
42648
log
plain
-rw-r--r--
InterpreterExpansion.ml
28681
log
plain
-rw-r--r--
InterpreterExpansion.mli
3049
log
plain
-rw-r--r--
InterpreterExpressions.ml
32747
log
plain
-rw-r--r--
InterpreterExpressions.mli
2286
log
plain
-rw-r--r--
InterpreterLoops.ml
8438
log
plain
-rw-r--r--
InterpreterLoops.mli
1736
log
plain
-rw-r--r--
InterpreterLoopsCore.ml
11033
log
plain
-rw-r--r--
InterpreterLoopsFixedPoint.ml
34208
log
plain
-rw-r--r--
InterpreterLoopsFixedPoint.mli
5479
log
plain
-rw-r--r--
InterpreterLoopsJoinCtxs.ml
25356
log
plain
-rw-r--r--
InterpreterLoopsJoinCtxs.mli
3320
log
plain
-rw-r--r--
InterpreterLoopsMatchCtxs.ml
61026
log
plain
-rw-r--r--
InterpreterLoopsMatchCtxs.mli
10746
log
plain
-rw-r--r--
InterpreterPaths.ml
25262
log
plain
-rw-r--r--
InterpreterPaths.mli
3760
log
plain
-rw-r--r--
InterpreterProjectors.ml
20958
log
plain
-rw-r--r--
InterpreterProjectors.mli
4286
log
plain
-rw-r--r--
InterpreterStatements.ml
59584
log
plain
-rw-r--r--
InterpreterStatements.mli
1811
log
plain
-rw-r--r--
InterpreterUtils.ml
17860
log
plain
-rw-r--r--
Invariants.ml
31928
log
plain
-rw-r--r--
LlbcAst.ml
427
log
plain
-rw-r--r--
LlbcAstUtils.ml
2391
log
plain
-rw-r--r--
LlbcOfJson.ml
26
log
plain
-rw-r--r--
Logging.ml
2578
log
plain
-rw-r--r--
Main.ml
9875
log
plain
-rw-r--r--
Makefile
30
log
plain
-rw-r--r--
Meta.ml
20
log
plain
-rw-r--r--
PrePasses.ml
13038
log
plain
-rw-r--r--
Print.ml
23496
log
plain
-rw-r--r--
PrintPure.ml
30494
log
plain
-rw-r--r--
Pure.ml
37683
log
plain
-rw-r--r--
PureMicroPasses.ml
86915
log
plain
-rw-r--r--
PureTypeCheck.ml
9584
log
plain
-rw-r--r--
PureUtils.ml
23102
log
plain
-rw-r--r--
RegionsHierarchy.ml
11064
log
plain
-rw-r--r--
ReorderDecls.ml
3665
log
plain
-rw-r--r--
SCC.ml
11421
log
plain
-rw-r--r--
Scalars.ml
23
log
plain
-rw-r--r--
StringUtils.ml
27
log
plain
-rw-r--r--
Substitute.ml
20363
log
plain
-rw-r--r--
SymbolicAst.ml
10697
log
plain
-rw-r--r--
SymbolicToPure.ml
124645
log
plain
-rw-r--r--
SynthesizeSymbolic.ml
7356
log
plain
-rw-r--r--
Translate.ml
57720
log
plain
-rw-r--r--
TranslateCore.ml
3074
log
plain
-rw-r--r--
Types.ml
21
log
plain
-rw-r--r--
TypesAnalysis.ml
12411
log
plain
-rw-r--r--
TypesUtils.ml
3810
log
plain
-rw-r--r--
Utils.ml
21
log
plain
-rw-r--r--
Values.ml
32460
log
plain
-rw-r--r--
ValuesUtils.ml
7053
log
plain
-rw-r--r--
aeneas.opam
711
log
plain
-rw-r--r--
dune
1567
log
plain
-rw-r--r--
dune-project
357
log
plain