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--
AssociatedTypes.ml
24337
log
plain
-rw-r--r--
Assumed.ml
9367
log
plain
-rw-r--r--
Collections.ml
27
log
plain
-rw-r--r--
Config.ml
12197
log
plain
-rw-r--r--
ConstStrings.ml
342
log
plain
-rw-r--r--
Contexts.ml
22110
log
plain
-rw-r--r--
Cps.ml
5352
log
plain
-rw-r--r--
Errors.ml
2592
log
plain
-rw-r--r--
Expressions.ml
27
log
plain
-rw-r--r--
ExpressionsUtils.ml
32
log
plain
-rw-r--r--
Extract.ml
111314
log
plain
-rw-r--r--
ExtractBase.ml
73563
log
plain
-rw-r--r--
ExtractBuiltin.ml
27632
log
plain
-rw-r--r--
ExtractName.ml
4516
log
plain
-rw-r--r--
ExtractTypes.ml
75549
log
plain
-rw-r--r--
FunsAnalysis.ml
8896
log
plain
-rw-r--r--
Identifiers.ml
27
log
plain
-rw-r--r--
Interpreter.ml
26859
log
plain
-rw-r--r--
InterpreterBorrows.ml
109235
log
plain
-rw-r--r--
InterpreterBorrows.mli
7864
log
plain
-rw-r--r--
InterpreterBorrowsCore.ml
44580
log
plain
-rw-r--r--
InterpreterExpansion.ml
27768
log
plain
-rw-r--r--
InterpreterExpansion.mli
2599
log
plain
-rw-r--r--
InterpreterExpressions.ml
34620
log
plain
-rw-r--r--
InterpreterExpressions.mli
2128
log
plain
-rw-r--r--
InterpreterLoops.ml
12982
log
plain
-rw-r--r--
InterpreterLoops.mli
1882
log
plain
-rw-r--r--
InterpreterLoopsCore.ml
11894
log
plain
-rw-r--r--
InterpreterLoopsFixedPoint.ml
41640
log
plain
-rw-r--r--
InterpreterLoopsFixedPoint.mli
6298
log
plain
-rw-r--r--
InterpreterLoopsJoinCtxs.ml
26289
log
plain
-rw-r--r--
InterpreterLoopsJoinCtxs.mli
3365
log
plain
-rw-r--r--
InterpreterLoopsMatchCtxs.ml
75985
log
plain
-rw-r--r--
InterpreterLoopsMatchCtxs.mli
11264
log
plain
-rw-r--r--
InterpreterPaths.ml
26498
log
plain
-rw-r--r--
InterpreterPaths.mli
3929
log
plain
-rw-r--r--
InterpreterProjectors.ml
21755
log
plain
-rw-r--r--
InterpreterProjectors.mli
4384
log
plain
-rw-r--r--
InterpreterStatements.ml
66715
log
plain
-rw-r--r--
InterpreterStatements.mli
1870
log
plain
-rw-r--r--
InterpreterUtils.ml
18054
log
plain
-rw-r--r--
Invariants.ml
35196
log
plain
-rw-r--r--
LlbcAst.ml
427
log
plain
-rw-r--r--
LlbcAstUtils.ml
2389
log
plain
-rw-r--r--
LlbcOfJson.ml
26
log
plain
-rw-r--r--
Logging.ml
2654
log
plain
-rw-r--r--
Main.ml
10266
log
plain
-rw-r--r--
Makefile
30
log
plain
-rw-r--r--
Meta.ml
20
log
plain
-rw-r--r--
PrePasses.ml
14489
log
plain
-rw-r--r--
Print.ml
25060
log
plain
-rw-r--r--
PrintPure.ml
31885
log
plain
-rw-r--r--
Pure.ml
41096
log
plain
-rw-r--r--
PureMicroPasses.ml
87561
log
plain
-rw-r--r--
PureTypeCheck.ml
10653
log
plain
-rw-r--r--
PureUtils.ml
27075
log
plain
-rw-r--r--
RegionsHierarchy.ml
11462
log
plain
-rw-r--r--
ReorderDecls.ml
3587
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
8526
log
plain
-rw-r--r--
SymbolicAst.ml
11402
log
plain
-rw-r--r--
SymbolicToPure.ml
158393
log
plain
-rw-r--r--
SynthesizeSymbolic.ml
8297
log
plain
-rw-r--r--
Translate.ml
56938
log
plain
-rw-r--r--
TranslateCore.ml
3973
log
plain
-rw-r--r--
Types.ml
21
log
plain
-rw-r--r--
TypesAnalysis.ml
13353
log
plain
-rw-r--r--
TypesUtils.ml
4984
log
plain
-rw-r--r--
Utils.ml
21
log
plain
-rw-r--r--
Values.ml
30516
log
plain
-rw-r--r--
ValuesUtils.ml
7436
log
plain
-rw-r--r--
aeneas.opam
711
log
plain
l---------
charon
20
log
plain
-rw-r--r--
dune
1576
log
plain
-rw-r--r--
dune-project
357
log
plain