compiler - aeneas - aeneas rust verifier with a hacky Isabelle backend

Mode	Name	Size
-rw-r--r--	.gitignore	7	log plain
-rw-r--r--	.ocamlformat	19	log plain
-rw-r--r--	AssociatedTypes.ml	23447	log plain
-rw-r--r--	Assumed.ml	9301	log plain
-rw-r--r--	Collections.ml	27	log plain
-rw-r--r--	Config.ml	12689	log plain
-rw-r--r--	ConstStrings.ml	342	log plain
-rw-r--r--	Contexts.ml	20527	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	103465	log plain
-rw-r--r--	ExtractBase.ml	73033	log plain
-rw-r--r--	ExtractBuiltin.ml	19640	log plain
-rw-r--r--	ExtractName.ml	7163	log plain
-rw-r--r--	ExtractTypes.ml	66164	log plain
-rw-r--r--	FunsAnalysis.ml	7775	log plain
-rw-r--r--	Identifiers.ml	27	log plain
-rw-r--r--	Interpreter.ml	25234	log plain
-rw-r--r--	InterpreterBorrows.ml	104511	log plain
-rw-r--r--	InterpreterBorrows.mli	7672	log plain
-rw-r--r--	InterpreterBorrowsCore.ml	42573	log plain
-rw-r--r--	InterpreterExpansion.ml	28681	log plain
-rw-r--r--	InterpreterExpansion.mli	3040	log plain
-rw-r--r--	InterpreterExpressions.ml	31776	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	11008	log plain
-rw-r--r--	InterpreterLoopsFixedPoint.ml	34207	log plain
-rw-r--r--	InterpreterLoopsFixedPoint.mli	5479	log plain
-rw-r--r--	InterpreterLoopsJoinCtxs.ml	25359	log plain
-rw-r--r--	InterpreterLoopsJoinCtxs.mli	3320	log plain
-rw-r--r--	InterpreterLoopsMatchCtxs.ml	61023	log plain
-rw-r--r--	InterpreterLoopsMatchCtxs.mli	10647	log plain
-rw-r--r--	InterpreterPaths.ml	25265	log plain
-rw-r--r--	InterpreterPaths.mli	3760	log plain
-rw-r--r--	InterpreterProjectors.ml	20958	log plain
-rw-r--r--	InterpreterProjectors.mli	4258	log plain
-rw-r--r--	InterpreterStatements.ml	57778	log plain
-rw-r--r--	InterpreterStatements.mli	1801	log plain
-rw-r--r--	InterpreterUtils.ml	17735	log plain
-rw-r--r--	Invariants.ml	31931	log plain
-rw-r--r--	LlbcAst.ml	411	log plain
-rw-r--r--	LlbcAstUtils.ml	2325	log plain
-rw-r--r--	LlbcOfJson.ml	26	log plain
-rw-r--r--	Logging.ml	2578	log plain
-rw-r--r--	Main.ml	9027	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	23568	log plain
-rw-r--r--	PrintPure.ml	30459	log plain
-rw-r--r--	Pure.ml	37675	log plain
-rw-r--r--	PureMicroPasses.ml	86915	log plain
-rw-r--r--	PureTypeCheck.ml	9584	log plain
-rw-r--r--	PureUtils.ml	23132	log plain
-rw-r--r--	RegionsHierarchy.ml	9674	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	18608	log plain
-rw-r--r--	SymbolicAst.ml	10679	log plain
-rw-r--r--	SymbolicToPure.ml	123130	log plain
-rw-r--r--	SynthesizeSymbolic.ml	7356	log plain
-rw-r--r--	Translate.ml	53989	log plain
-rw-r--r--	TranslateCore.ml	2698	log plain
-rw-r--r--	Types.ml	21	log plain
-rw-r--r--	TypesAnalysis.ml	12401	log plain
-rw-r--r--	TypesUtils.ml	3672	log plain
-rw-r--r--	Utils.ml	21	log plain
-rw-r--r--	Values.ml	32402	log plain
-rw-r--r--	ValuesUtils.ml	7053	log plain
-rw-r--r--	aeneas.opam	711	log plain
-rw-r--r--	dune	1572	log plain
-rw-r--r--	dune-project	357	log plain