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

Mode	Name	Size
-rw-r--r--	.ocamlformat	19	log plain
-rw-r--r--	AssociatedTypes.ml	24396	log plain
-rw-r--r--	Assumed.ml	9356	log plain
-rw-r--r--	BorrowCheck.ml	754	log plain
-rw-r--r--	Collections.ml	27	log plain
-rw-r--r--	Config.ml	13008	log plain
-rw-r--r--	ConstStrings.ml	342	log plain
-rw-r--r--	Contexts.ml	22110	log plain
-rw-r--r--	Cps.ml	4838	log plain
-rw-r--r--	Errors.ml	2644	log plain
-rw-r--r--	Expressions.ml	27	log plain
-rw-r--r--	ExpressionsUtils.ml	32	log plain
-rw-r--r--	Extract.ml	120761	log plain
-rw-r--r--	ExtractBase.ml	79665	log plain
-rw-r--r--	ExtractBuiltin.ml	26805	log plain
-rw-r--r--	ExtractName.ml	4516	log plain
-rw-r--r--	ExtractTypes.ml	78127	log plain
-rw-r--r--	FunsAnalysis.ml	9276	log plain
-rw-r--r--	Identifiers.ml	27	log plain
-rw-r--r--	Interpreter.ml	27762	log plain
-rw-r--r--	InterpreterBorrows.ml	126227	log plain
-rw-r--r--	InterpreterBorrows.mli	8513	log plain
-rw-r--r--	InterpreterBorrowsCore.ml	46229	log plain
-rw-r--r--	InterpreterExpansion.ml	27881	log plain
-rw-r--r--	InterpreterExpansion.mli	2529	log plain
-rw-r--r--	InterpreterExpressions.ml	34686	log plain
-rw-r--r--	InterpreterExpressions.mli	2224	log plain
-rw-r--r--	InterpreterLoops.ml	16044	log plain
-rw-r--r--	InterpreterLoops.mli	1882	log plain
-rw-r--r--	InterpreterLoopsCore.ml	14261	log plain
-rw-r--r--	InterpreterLoopsFixedPoint.ml	40897	log plain
-rw-r--r--	InterpreterLoopsFixedPoint.mli	6468	log plain
-rw-r--r--	InterpreterLoopsJoinCtxs.ml	35068	log plain
-rw-r--r--	InterpreterLoopsJoinCtxs.mli	3371	log plain
-rw-r--r--	InterpreterLoopsMatchCtxs.ml	78333	log plain
-rw-r--r--	InterpreterLoopsMatchCtxs.mli	11085	log plain
-rw-r--r--	InterpreterPaths.ml	26900	log plain
-rw-r--r--	InterpreterPaths.mli	3951	log plain
-rw-r--r--	InterpreterProjectors.ml	21801	log plain
-rw-r--r--	InterpreterProjectors.mli	4384	log plain
-rw-r--r--	InterpreterStatements.ml	66077	log plain
-rw-r--r--	InterpreterStatements.mli	1896	log plain
-rw-r--r--	InterpreterUtils.ml	18070	log plain
-rw-r--r--	Invariants.ml	36003	log plain
-rw-r--r--	LlbcAst.ml	427	log plain
-rw-r--r--	LlbcAstUtils.ml	2427	log plain
-rw-r--r--	LlbcOfJson.ml	26	log plain
-rw-r--r--	Logging.ml	2746	log plain
-rw-r--r--	Main.ml	12303	log plain
-rw-r--r--	Makefile	30	log plain
-rw-r--r--	Meta.ml	20	log plain
-rw-r--r--	PrePasses.ml	15810	log plain
-rw-r--r--	Print.ml	25383	log plain
-rw-r--r--	PrintPure.ml	31837	log plain
-rw-r--r--	Pure.ml	41088	log plain
-rw-r--r--	PureMicroPasses.ml	90116	log plain
-rw-r--r--	PureTypeCheck.ml	10653	log plain
-rw-r--r--	PureUtils.ml	27027	log plain
-rw-r--r--	RegionsHierarchy.ml	11435	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	8529	log plain
-rw-r--r--	SymbolicAst.ml	11478	log plain
-rw-r--r--	SymbolicToPure.ml	157878	log plain
-rw-r--r--	SynthesizeSymbolic.ml	7275	log plain
-rw-r--r--	Translate.ml	59059	log plain
-rw-r--r--	TranslateCore.ml	3973	log plain
-rw-r--r--	Types.ml	21	log plain
-rw-r--r--	TypesAnalysis.ml	13470	log plain
-rw-r--r--	TypesUtils.ml	4984	log plain
-rw-r--r--	Utils.ml	21	log plain
-rw-r--r--	Values.ml	31712	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	1590	log plain
-rw-r--r--	dune-project	357	log plain