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
25408
log
plain
-rw-r--r--
Assumed.ml
10021
log
plain
-rw-r--r--
Collections.ml
27
log
plain
-rw-r--r--
Config.ml
12191
log
plain
-rw-r--r--
ConstStrings.ml
342
log
plain
-rw-r--r--
Contexts.ml
23701
log
plain
-rw-r--r--
Cps.ml
7629
log
plain
-rw-r--r--
Driver.ml
8675
log
plain
-rw-r--r--
Expressions.ml
27
log
plain
-rw-r--r--
ExpressionsUtils.ml
32
log
plain
-rw-r--r--
Extract.ml
96694
log
plain
-rw-r--r--
ExtractBase.ml
52368
log
plain
-rw-r--r--
ExtractBuiltin.ml
20284
log
plain
-rw-r--r--
ExtractTypes.ml
89039
log
plain
-rw-r--r--
FunsAnalysis.ml
7520
log
plain
-rw-r--r--
Identifiers.ml
27
log
plain
-rw-r--r--
Interpreter.ml
24720
log
plain
-rw-r--r--
InterpreterBorrows.ml
106012
log
plain
-rw-r--r--
InterpreterBorrows.mli
7975
log
plain
-rw-r--r--
InterpreterBorrowsCore.ml
42911
log
plain
-rw-r--r--
InterpreterExpansion.ml
29039
log
plain
-rw-r--r--
InterpreterExpansion.mli
3295
log
plain
-rw-r--r--
InterpreterExpressions.ml
32779
log
plain
-rw-r--r--
InterpreterExpressions.mli
2510
log
plain
-rw-r--r--
InterpreterLoops.ml
8567
log
plain
-rw-r--r--
InterpreterLoops.mli
1725
log
plain
-rw-r--r--
InterpreterLoopsCore.ml
11640
log
plain
-rw-r--r--
InterpreterLoopsFixedPoint.ml
34705
log
plain
-rw-r--r--
InterpreterLoopsFixedPoint.mli
5701
log
plain
-rw-r--r--
InterpreterLoopsJoinCtxs.ml
25993
log
plain
-rw-r--r--
InterpreterLoopsJoinCtxs.mli
3554
log
plain
-rw-r--r--
InterpreterLoopsMatchCtxs.ml
61929
log
plain
-rw-r--r--
InterpreterLoopsMatchCtxs.mli
10854
log
plain
-rw-r--r--
InterpreterPaths.ml
25712
log
plain
-rw-r--r--
InterpreterPaths.mli
3912
log
plain
-rw-r--r--
InterpreterProjectors.ml
21195
log
plain
-rw-r--r--
InterpreterProjectors.mli
4384
log
plain
-rw-r--r--
InterpreterStatements.ml
57755
log
plain
-rw-r--r--
InterpreterStatements.mli
2040
log
plain
-rw-r--r--
InterpreterUtils.ml
18356
log
plain
-rw-r--r--
Invariants.ml
32045
log
plain
-rw-r--r--
LlbcAst.ml
454
log
plain
-rw-r--r--
LlbcAstUtils.ml
2125
log
plain
-rw-r--r--
LlbcOfJson.ml
26
log
plain
-rw-r--r--
Logging.ml
2393
log
plain
-rw-r--r--
Makefile
30
log
plain
-rw-r--r--
Meta.ml
20
log
plain
-rw-r--r--
Names.ml
21
log
plain
-rw-r--r--
PrePasses.ml
13179
log
plain
-rw-r--r--
PrimitiveValues.ml
31
log
plain
-rw-r--r--
PrimitiveValuesUtils.ml
36
log
plain
-rw-r--r--
Print.ml
32033
log
plain
-rw-r--r--
PrintPure.ml
34327
log
plain
-rw-r--r--
Pure.ml
35274
log
plain
-rw-r--r--
PureMicroPasses.ml
87750
log
plain
-rw-r--r--
PureTypeCheck.ml
9567
log
plain
-rw-r--r--
PureUtils.ml
22148
log
plain
-rw-r--r--
ReorderDecls.ml
6356
log
plain
-rw-r--r--
SCC.ml
8331
log
plain
-rw-r--r--
Scalars.ml
23
log
plain
-rw-r--r--
StringUtils.ml
3562
log
plain
-rw-r--r--
Substitute.ml
23753
log
plain
-rw-r--r--
SymbolicAst.ml
11363
log
plain
-rw-r--r--
SymbolicToPure.ml
122677
log
plain
-rw-r--r--
SynthesizeSymbolic.ml
7577
log
plain
-rw-r--r--
Translate.ml
54147
log
plain
-rw-r--r--
TranslateCore.ml
2895
log
plain
-rw-r--r--
Types.ml
21
log
plain
-rw-r--r--
TypesAnalysis.ml
12453
log
plain
-rw-r--r--
TypesUtils.ml
1177
log
plain
-rw-r--r--
Utils.ml
21
log
plain
-rw-r--r--
Values.ml
36912
log
plain
-rw-r--r--
ValuesUtils.ml
6879
log
plain
-rw-r--r--
aeneas.opam
711
log
plain
-rw-r--r--
dune
1594
log
plain
-rw-r--r--
dune-project
357
log
plain