matita.cs.unibo.it Git - pkg-cerco/acc-trusted.git/tree

drwxr-xr-x		..
-rw-r--r--	48	MODIFIED_BY_HAND	blob \| history \| raw
-rwxr-xr-x	478	Makefile	blob \| history \| raw
-rw-r--r--	499	PROBLEMS	blob \| history \| raw
-rw-r--r--	234960	aSM.ml	blob \| history \| raw
-rw-r--r--	66041	aSM.mli	blob \| history \| raw
-rw-r--r--	31627	aSMCosts.ml	blob \| history \| raw
-rw-r--r--	2065	aSMCosts.mli	blob \| history \| raw
-rw-r--r--	3362	aSMCostsSplit.ml	blob \| history \| raw
-rw-r--r--	1281	aSMCostsSplit.mli	blob \| history \| raw
-rw-r--r--	56631	aST.ml	blob \| history \| raw
-rw-r--r--	19833	aST.mli	blob \| history \| raw
-rw-r--r--	4072	abstractStatus.ml	blob \| history \| raw
-rw-r--r--	1347	abstractStatus.mli	blob \| history \| raw
-rw-r--r--	27772	arithmetic.ml	blob \| history \| raw
-rw-r--r--	8384	arithmetic.mli	blob \| history \| raw
-rw-r--r--	186596	assembly.ml	blob \| history \| raw
-rw-r--r--	4186	assembly.mli	blob \| history \| raw
-rw-r--r--	979	assocList.ml	blob \| history \| raw
-rw-r--r--	534	assocList.mli	blob \| history \| raw
-rw-r--r--	1047	bEMem.ml	blob \| history \| raw
-rw-r--r--	801	bEMem.mli	blob \| history \| raw
-rw-r--r--	46837	backEndOps.ml	blob \| history \| raw
-rw-r--r--	8844	backEndOps.mli	blob \| history \| raw
-rw-r--r--	12186	bigops.ml	blob \| history \| raw
-rw-r--r--	5907	bigops.mli	blob \| history \| raw
-rw-r--r--	1751	bindLists.ml	blob \| history \| raw
-rw-r--r--	1089	bindLists.mli	blob \| history \| raw
-rw-r--r--	4954	bind_new.ml	blob \| history \| raw
-rw-r--r--	2260	bind_new.mli	blob \| history \| raw
-rw-r--r--	2188	bitVector.ml	blob \| history \| raw
-rw-r--r--	1126	bitVector.mli	blob \| history \| raw
-rw-r--r--	11376	bitVectorTrie.ml	blob \| history \| raw
-rw-r--r--	3819	bitVectorTrie.mli	blob \| history \| raw
-rw-r--r--	3124	bitVectorTrieSet.ml	blob \| history \| raw
-rw-r--r--	924	bitVectorTrieSet.mli	blob \| history \| raw
-rw-r--r--	2720	bitVectorZ.ml	blob \| history \| raw
-rw-r--r--	743	bitVectorZ.mli	blob \| history \| raw
-rw-r--r--	2535	blocks.ml	blob \| history \| raw
-rw-r--r--	1721	blocks.mli	blob \| history \| raw
-rw-r--r--	2535	bool.ml	blob \| history \| raw
-rw-r--r--	924	bool.mli	blob \| history \| raw
-rw-r--r--	41774	byteValues.ml	blob \| history \| raw
-rw-r--r--	14157	byteValues.mli	blob \| history \| raw
-rw-r--r--	892	casts.ml	blob \| history \| raw
-rw-r--r--	746	casts.mli	blob \| history \| raw
-rw-r--r--	49161	cexec.ml	blob \| history \| raw
-rw-r--r--	3182	cexec.mli	blob \| history \| raw
-rw-r--r--	548	cexecInd.ml	blob \| history \| raw
-rw-r--r--	548	cexecInd.mli	blob \| history \| raw
-rw-r--r--	875	cexecSound.ml	blob \| history \| raw
-rw-r--r--	875	cexecSound.mli	blob \| history \| raw
-rw-r--r--	41069	classifyOp.ml	blob \| history \| raw
-rw-r--r--	18406	classifyOp.mli	blob \| history \| raw
-rw-r--r--	2849	clight_abstract.ml	blob \| history \| raw
-rw-r--r--	1463	clight_abstract.mli	blob \| history \| raw
-rw-r--r--	1808	clight_classified_system.ml	blob \| history \| raw
-rw-r--r--	1125	clight_classified_system.mli	blob \| history \| raw
-rw-r--r--	3361	cminor_abstract.ml	blob \| history \| raw
-rw-r--r--	1854	cminor_abstract.mli	blob \| history \| raw
-rw-r--r--	1852	cminor_classified_system.ml	blob \| history \| raw
-rw-r--r--	1093	cminor_classified_system.mli	blob \| history \| raw
-rw-r--r--	37109	cminor_semantics.ml	blob \| history \| raw
-rw-r--r--	11395	cminor_semantics.mli	blob \| history \| raw
-rw-r--r--	42447	cminor_syntax.ml	blob \| history \| raw
-rw-r--r--	19715	cminor_syntax.mli	blob \| history \| raw
-rw-r--r--	24794	compiler.ml	blob \| history \| raw
-rw-r--r--	8675	compiler.mli	blob \| history \| raw
-rw-r--r--	363	coqlib.ml	blob \| history \| raw
-rw-r--r--	238	coqlib.mli	blob \| history \| raw
-rw-r--r--	15	core_notation.ml	blob \| history \| raw
-rw-r--r--	15	core_notation.mli	blob \| history \| raw
-rw-r--r--	5555	costCheck.ml	blob \| history \| raw
-rw-r--r--	1507	costCheck.mli	blob \| history \| raw
-rw-r--r--	2287	costInj.ml	blob \| history \| raw
-rw-r--r--	1166	costInj.mli	blob \| history \| raw
-rw-r--r--	711	costLabel.ml	blob \| history \| raw
-rw-r--r--	547	costLabel.mli	blob \| history \| raw
-rw-r--r--	816	costMisc.ml	blob \| history \| raw
-rw-r--r--	816	costMisc.mli	blob \| history \| raw
-rw-r--r--	4122	costSpec.ml	blob \| history \| raw
-rw-r--r--	1104	costSpec.mli	blob \| history \| raw
-rw-r--r--	51532	csem.ml	blob \| history \| raw
-rw-r--r--	14036	csem.mli	blob \| history \| raw
-rw-r--r--	57954	csyntax.ml	blob \| history \| raw
-rw-r--r--	22883	csyntax.mli	blob \| history \| raw
-rw-r--r--	4067	deqsets.ml	blob \| history \| raw
-rw-r--r--	1851	deqsets.mli	blob \| history \| raw
-rw-r--r--	454	deqsets_extra.ml	blob \| history \| raw
-rw-r--r--	314	deqsets_extra.mli	blob \| history \| raw
-rw-r--r--	3443	div_and_mod.ml	blob \| history \| raw
-rw-r--r--	1558	div_and_mod.mli	blob \| history \| raw
-rw-r--r--	7334	division.ml	blob \| history \| raw
-rw-r--r--	1611	division.mli	blob \| history \| raw
-rw-r--r--	25755	eRTL.ml	blob \| history \| raw
-rw-r--r--	10742	eRTL.mli	blob \| history \| raw
-rw-r--r--	38021	eRTLToLTL.ml	blob \| history \| raw
-rw-r--r--	8659	eRTLToLTL.mli	blob \| history \| raw
-rw-r--r--	1306	eRTL_printer.ml	blob \| history \| raw
-rw-r--r--	1040	eRTL_printer.mli	blob \| history \| raw
-rw-r--r--	11607	eRTL_semantics.ml	blob \| history \| raw
-rw-r--r--	3265	eRTL_semantics.mli	blob \| history \| raw
-rw-r--r--	1340	errorMessages.ml	blob \| history \| raw
-rw-r--r--	1340	errorMessages.mli	blob \| history \| raw
-rw-r--r--	9863	errors.ml	blob \| history \| raw
-rw-r--r--	4593	errors.mli	blob \| history \| raw
-rw-r--r--	11346	events.ml	blob \| history \| raw
-rw-r--r--	5063	events.mli	blob \| history \| raw
-rw-r--r--	658	executions.ml	blob \| history \| raw
-rw-r--r--	658	executions.mli	blob \| history \| raw
-rw-r--r--	268	exp.ml	blob \| history \| raw
-rw-r--r--	177	exp.mli	blob \| history \| raw
-rw-r--r--	697	extraGlobalenvs.ml	blob \| history \| raw
-rw-r--r--	697	extraGlobalenvs.mli	blob \| history \| raw
-rw-r--r--	10468	extraMonads.ml	blob \| history \| raw
-rw-r--r--	5292	extraMonads.mli	blob \| history \| raw
-rw-r--r--	463	extra_bool.ml	blob \| history \| raw
-rw-r--r--	271	extra_bool.mli	blob \| history \| raw
-rw-r--r--	1594	extralib.ml	blob \| history \| raw
-rw-r--r--	635	extralib.mli	blob \| history \| raw
-rw-r--r--	6198	extranat.ml	blob \| history \| raw
-rw-r--r--	2699	extranat.mli	blob \| history \| raw
-rw-r--r--	83429	fetch.ml	blob \| history \| raw
-rw-r--r--	1486	fetch.mli	blob \| history \| raw
-rw-r--r--	10321	fixpoints.ml	blob \| history \| raw
-rw-r--r--	5340	fixpoints.mli	blob \| history \| raw
-rw-r--r--	1584	foldStuff.ml	blob \| history \| raw
-rw-r--r--	741	foldStuff.mli	blob \| history \| raw
-rw-r--r--	2193	fresh.ml	blob \| history \| raw
-rw-r--r--	1234	fresh.mli	blob \| history \| raw
-rw-r--r--	3064	frontEndMem.ml	blob \| history \| raw
-rw-r--r--	1278	frontEndMem.mli	blob \| history \| raw
-rw-r--r--	58235	frontEndOps.ml	blob \| history \| raw
-rw-r--r--	23988	frontEndOps.mli	blob \| history \| raw
-rw-r--r--	4471	frontEndVal.ml	blob \| history \| raw
-rw-r--r--	1190	frontEndVal.mli	blob \| history \| raw
-rw-r--r--	6238	frontend_misc.ml	blob \| history \| raw
-rw-r--r--	2275	frontend_misc.mli	blob \| history \| raw
-rw-r--r--	9980	genMem.ml	blob \| history \| raw
-rw-r--r--	4191	genMem.mli	blob \| history \| raw
-rw-r--r--	26823	globalenvs.ml	blob \| history \| raw
-rw-r--r--	11910	globalenvs.mli	blob \| history \| raw
-rw-r--r--	1133	graphs.ml	blob \| history \| raw
-rw-r--r--	833	graphs.mli	blob \| history \| raw
-rw-r--r--	81	hide.ml	blob \| history \| raw
-rw-r--r--	81	hide.mli	blob \| history \| raw
-rw-r--r--	162	hints_declaration.ml	blob \| history \| raw
-rw-r--r--	162	hints_declaration.mli	blob \| history \| raw
-rw-r--r--	33740	i8051.ml	blob \| history \| raw
-rw-r--r--	6708	i8051.mli	blob \| history \| raw
-rw-r--r--	551	i8051bis.ml	blob \| history \| raw
-rw-r--r--	211	i8051bis.mli	blob \| history \| raw
-rw-r--r--	7092	iO.ml	blob \| history \| raw
-rw-r--r--	2751	iO.mli	blob \| history \| raw
-rw-r--r--	19024	iOMonad.ml	blob \| history \| raw
-rw-r--r--	9555	iOMonad.mli	blob \| history \| raw
-rw-r--r--	18151	identifiers.ml	blob \| history \| raw
-rw-r--r--	9049	identifiers.mli	blob \| history \| raw
-rw-r--r--	5682	initialisation.ml	blob \| history \| raw
-rw-r--r--	1878	initialisation.mli	blob \| history \| raw
-rw-r--r--	9948	integers.ml	blob \| history \| raw
-rw-r--r--	3025	integers.mli	blob \| history \| raw
-rw-r--r--	8855	interference.ml	blob \| history \| raw
-rw-r--r--	4455	interference.mli	blob \| history \| raw
-rw-r--r--	250289	interpret.ml	blob \| history \| raw
-rw-r--r--	2709	interpret.mli	blob \| history \| raw
-rw-r--r--	16918	interpret2.ml	blob \| history \| raw
-rw-r--r--	3098	interpret2.mli	blob \| history \| raw
-rw-r--r--	3969	jmeq.ml	blob \| history \| raw
-rw-r--r--	1719	jmeq.mli	blob \| history \| raw
-rw-r--r--	115884	joint.ml	blob \| history \| raw
-rw-r--r--	56166	joint.mli	blob \| history \| raw
-rw-r--r--	13104	joint_LTL_LIN.ml	blob \| history \| raw
-rw-r--r--	5777	joint_LTL_LIN.mli	blob \| history \| raw
-rw-r--r--	8661	joint_LTL_LIN_semantics.ml	blob \| history \| raw
-rw-r--r--	2349	joint_LTL_LIN_semantics.mli	blob \| history \| raw
-rw-r--r--	3282	joint_fullexec.ml	blob \| history \| raw
-rw-r--r--	1520	joint_fullexec.mli	blob \| history \| raw
-rw-r--r--	64038	joint_printer.ml	blob \| history \| raw
-rw-r--r--	27394	joint_printer.mli	blob \| history \| raw
-rw-r--r--	113965	joint_semantics.ml	blob \| history \| raw
-rw-r--r--	52656	joint_semantics.mli	blob \| history \| raw
-rw-r--r--	1997	lIN.ml	blob \| history \| raw
-rw-r--r--	1032	lIN.mli	blob \| history \| raw
-rw-r--r--	67822	lINToASM.ml	blob \| history \| raw
-rw-r--r--	10339	lINToASM.mli	blob \| history \| raw
-rw-r--r--	1309	lIN_printer.ml	blob \| history \| raw
-rw-r--r--	1056	lIN_printer.mli	blob \| history \| raw
-rw-r--r--	1531	lIN_semantics.ml	blob \| history \| raw
-rw-r--r--	1224	lIN_semantics.mli	blob \| history \| raw
-rw-r--r--	4234	lTL.ml	blob \| history \| raw
-rw-r--r--	2027	lTL.mli	blob \| history \| raw
-rw-r--r--	1051	lTLToLIN.ml	blob \| history \| raw
-rw-r--r--	982	lTLToLIN.mli	blob \| history \| raw
-rw-r--r--	1315	lTL_printer.ml	blob \| history \| raw
-rw-r--r--	1056	lTL_printer.mli	blob \| history \| raw
-rw-r--r--	1494	lTL_semantics.ml	blob \| history \| raw
-rw-r--r--	1229	lTL_semantics.mli	blob \| history \| raw
-rw-r--r--	26668	label.ml	blob \| history \| raw
-rw-r--r--	2734	label.mli	blob \| history \| raw
-rw-r--r--	2152	labelledObjects.ml	blob \| history \| raw
-rw-r--r--	1140	labelledObjects.mli	blob \| history \| raw
-rw-r--r--	11155	linearise.ml	blob \| history \| raw
-rw-r--r--	2253	linearise.mli	blob \| history \| raw
-rw-r--r--	9276	list.ml	blob \| history \| raw
-rw-r--r--	3900	list.mli	blob \| history \| raw
-rw-r--r--	1171	listb.ml	blob \| history \| raw
-rw-r--r--	477	listb.mli	blob \| history \| raw
-rw-r--r--	283	listb_extra.ml	blob \| history \| raw
-rw-r--r--	283	listb_extra.mli	blob \| history \| raw
-rw-r--r--	2392	lists.ml	blob \| history \| raw
-rw-r--r--	945	lists.mli	blob \| history \| raw
-rw-r--r--	14773	liveness.ml	blob \| history \| raw
-rw-r--r--	2596	liveness.mli	blob \| history \| raw
-rw-r--r--	6489	logic.ml	blob \| history \| raw
-rw-r--r--	2704	logic.mli	blob \| history \| raw
-rw-r--r--	21063	measurable.ml	blob \| history \| raw
-rw-r--r--	9008	measurable.mli	blob \| history \| raw
-rw-r--r--	1327	memProperties.ml	blob \| history \| raw
-rw-r--r--	1016	memProperties.mli	blob \| history \| raw
-rw-r--r--	5205	memoryInjections.ml	blob \| history \| raw
-rw-r--r--	2927	memoryInjections.mli	blob \| history \| raw
-rw-r--r--	20562	monad.ml	blob \| history \| raw
-rw-r--r--	9687	monad.mli	blob \| history \| raw
-rw-r--r--	3227	nat.ml	blob \| history \| raw
-rw-r--r--	1182	nat.mli	blob \| history \| raw
-rw-r--r--	1026	option.ml	blob \| history \| raw
-rw-r--r--	366	option.mli	blob \| history \| raw
-rw-r--r--	2633	order.ml	blob \| history \| raw
-rw-r--r--	968	order.mli	blob \| history \| raw
-rw-r--r--	11312	pointers.ml	blob \| history \| raw
-rw-r--r--	4667	pointers.mli	blob \| history \| raw
-rw-r--r--	4905	policy.ml	blob \| history \| raw
-rw-r--r--	1209	policy.mli	blob \| history \| raw
-rw-r--r--	28420	policyFront.ml	blob \| history \| raw
-rw-r--r--	2692	policyFront.mli	blob \| history \| raw
-rw-r--r--	7260	policyStep.ml	blob \| history \| raw
-rw-r--r--	864	policyStep.mli	blob \| history \| raw
-rw-r--r--	12408	positive.ml	blob \| history \| raw
-rw-r--r--	3890	positive.mli	blob \| history \| raw
-rw-r--r--	13025	positiveMap.ml	blob \| history \| raw
-rw-r--r--	4103	positiveMap.mli	blob \| history \| raw
-rw-r--r--	6891	preIdentifiers.ml	blob \| history \| raw
-rw-r--r--	2854	preIdentifiers.mli	blob \| history \| raw
-rw-r--r--	64	preamble.ml	blob \| history \| raw
-rw-r--r--	97	proper.ml	blob \| history \| raw
-rw-r--r--	97	proper.mli	blob \| history \| raw
-rw-r--r--	35	pts.ml	blob \| history \| raw
-rw-r--r--	35	pts.mli	blob \| history \| raw
-rw-r--r--	9337	rTL.ml	blob \| history \| raw
-rw-r--r--	3433	rTL.mli	blob \| history \| raw
-rw-r--r--	18235	rTLToERTL.ml	blob \| history \| raw
-rw-r--r--	3982	rTLToERTL.mli	blob \| history \| raw
-rw-r--r--	1295	rTL_printer.ml	blob \| history \| raw
-rw-r--r--	1036	rTL_printer.mli	blob \| history \| raw
-rw-r--r--	28712	rTL_semantics.ml	blob \| history \| raw
-rw-r--r--	7912	rTL_semantics.mli	blob \| history \| raw
-rw-r--r--	50428	rTLabsToRTL.ml	blob \| history \| raw
-rw-r--r--	11097	rTLabsToRTL.mli	blob \| history \| raw
-rw-r--r--	22101	rTLabs_abstract.ml	blob \| history \| raw
-rw-r--r--	7875	rTLabs_abstract.mli	blob \| history \| raw
-rw-r--r--	2440	rTLabs_classified_system.ml	blob \| history \| raw
-rw-r--r--	1243	rTLabs_classified_system.mli	blob \| history \| raw
-rw-r--r--	87052	rTLabs_semantics.ml	blob \| history \| raw
-rw-r--r--	10121	rTLabs_semantics.mli	blob \| history \| raw
-rw-r--r--	31161	rTLabs_syntax.ml	blob \| history \| raw
-rw-r--r--	18601	rTLabs_syntax.mli	blob \| history \| raw
-rw-r--r--	92846	rTLabs_traces.ml	blob \| history \| raw
-rw-r--r--	35240	rTLabs_traces.mli	blob \| history \| raw
-rw-r--r--	11898	registerSet.ml	blob \| history \| raw
-rw-r--r--	6414	registerSet.mli	blob \| history \| raw
-rw-r--r--	645	registers.ml	blob \| history \| raw
-rw-r--r--	564	registers.mli	blob \| history \| raw
-rw-r--r--	324	relations.ml	blob \| history \| raw
-rw-r--r--	286	relations.mli	blob \| history \| raw
-rw-r--r--	104	russell.ml	blob \| history \| raw
-rw-r--r--	104	russell.mli	blob \| history \| raw
-rw-r--r--	9539	semantics.ml	blob \| history \| raw
-rw-r--r--	5049	semantics.mli	blob \| history \| raw
-rw-r--r--	29035	semanticsUtils.ml	blob \| history \| raw
-rw-r--r--	14063	semanticsUtils.mli	blob \| history \| raw
-rw-r--r--	2402	setoids.ml	blob \| history \| raw
-rw-r--r--	1178	setoids.mli	blob \| history \| raw
-rw-r--r--	81	sets.ml	blob \| history \| raw
-rw-r--r--	81	sets.mli	blob \| history \| raw
-rw-r--r--	25759	simplifyCasts.ml	blob \| history \| raw
-rw-r--r--	2346	simplifyCasts.mli	blob \| history \| raw
-rw-r--r--	17081	smallstep.ml	blob \| history \| raw
-rw-r--r--	7980	smallstep.mli	blob \| history \| raw
-rw-r--r--	21986	smallstepExec.ml	blob \| history \| raw
-rw-r--r--	10474	smallstepExec.mli	blob \| history \| raw
-rw-r--r--	8734	stacksize.ml	blob \| history \| raw
-rw-r--r--	3763	stacksize.mli	blob \| history \| raw
-rw-r--r--	97	star.ml	blob \| history \| raw
-rw-r--r--	97	star.mli	blob \| history \| raw
-rw-r--r--	1133	state.ml	blob \| history \| raw
-rw-r--r--	539	state.mli	blob \| history \| raw
-rw-r--r--	251980	status.ml	blob \| history \| raw
-rw-r--r--	17778	status.mli	blob \| history \| raw
-rw-r--r--	599	statusProofs.ml	blob \| history \| raw
-rw-r--r--	599	statusProofs.mli	blob \| history \| raw
-rw-r--r--	890	string.ml	blob \| history \| raw
-rw-r--r--	350	string.mli	blob \| history \| raw
-rw-r--r--	82632	structuredTraces.ml	blob \| history \| raw
-rw-r--r--	37398	structuredTraces.mli	blob \| history \| raw
-rw-r--r--	19833	switchRemoval.ml	blob \| history \| raw
-rw-r--r--	5655	switchRemoval.mli	blob \| history \| raw
-rw-r--r--	97253	toCminor.ml	blob \| history \| raw
-rw-r--r--	15564	toCminor.mli	blob \| history \| raw
-rw-r--r--	55950	toRTLabs.ml	blob \| history \| raw
-rw-r--r--	22553	toRTLabs.mli	blob \| history \| raw
-rw-r--r--	24165	traces.ml	blob \| history \| raw
-rw-r--r--	9836	traces.mli	blob \| history \| raw
-rw-r--r--	29631	translateUtils.ml	blob \| history \| raw
-rw-r--r--	14583	translateUtils.mli	blob \| history \| raw
-rw-r--r--	8007	typeComparison.ml	blob \| history \| raw
-rw-r--r--	1128	typeComparison.mli	blob \| history \| raw
-rw-r--r--	14473	types.ml	blob \| history \| raw
-rw-r--r--	6087	types.mli	blob \| history \| raw
drwxr-xr-x	-	untrusted	tree \| history
-rw-r--r--	3567	uses.ml	blob \| history \| raw
-rw-r--r--	1008	uses.mli	blob \| history \| raw
-rw-r--r--	21466	util.ml	blob \| history \| raw
-rw-r--r--	6525	util.mli	blob \| history \| raw
-rw-r--r--	445	utilBranch.ml	blob \| history \| raw
-rw-r--r--	361	utilBranch.mli	blob \| history \| raw
-rw-r--r--	14178	values.ml	blob \| history \| raw
-rw-r--r--	3382	values.mli	blob \| history \| raw
-rw-r--r--	15189	vector.ml	blob \| history \| raw
-rw-r--r--	5134	vector.mli	blob \| history \| raw
-rw-r--r--	7734	z.ml	blob \| history \| raw
-rw-r--r--	2034	z.mli	blob \| history \| raw