#
# ChangeLog for src/common
#
# Generated by Trac 1.2
# Dec 15, 2019, 6:55:29 PM

Wed, 06 Feb 2013 16:03:18 GMT campbell [2618]
	* src/common/FEMeasurable.ma (modified)
	* src/common/Measurable.ma (modified)
	* src/common/SmallstepExec.ma (modified)

	Tidy up measurable a little.


Wed, 06 Feb 2013 16:03:14 GMT campbell [2617]
	* src/common/Measurable.ma (modified)

	Trivial simplification on split_trace.


Wed, 06 Feb 2013 12:01:34 GMT garnier [2608]
	* src/Clight/Cexec.ma (modified)
	* src/Clight/CexecSound.ma (modified)
	* src/Clight/Csem.ma (modified)
	* src/Clight/MemProperties.ma (modified)
	* src/Clight/frontend_misc.ma (modified)
	* src/Clight/memoryInjections.ma (modified)
	* src/Clight/switchRemoval.ma (modified)
	* src/Clight/toCminorCorrectnessExpr.ma (modified)
	* src/Clight/toCminorOps.ma (modified)
	* src/Cminor/Cminor_semantics.ma (modified)
	* src/RTLabs/RTLabs_semantics.ma (modified)
	* src/RTLabs/RTLabs_traces.ma (modified)
	* src/common/ByteValues.ma (modified)
	* src/common/GenMem.ma (modified)
	* src/common/Globalenvs.ma (modified)
	* src/common/Pointers.ma (modified)
	* src/common/extraGlobalenvs.ma (modified)

	Regions are no more stored in blocks. block_region now tests the id, ...


Tue, 05 Feb 2013 21:49:42 GMT piccolo [2604]
	* src/ERTL/ERTL.ma (modified)
	* src/ERTL/ERTL_semantics.ma (modified)
	* src/ERTLptr/ERTLptr.ma (modified)
	* src/ERTLptr/ERTLptr_semantics.ma (modified)
	* src/ERTLptr/ERTLtoERTLptr.ma (modified)
	* src/ERTLptr/ERTLtoERTLptrOK.ma (modified)
	* src/common/BitVectorTrieMap.ma (added)

	ERTLtoERTLptr in place.


Tue, 05 Feb 2013 12:54:45 GMT piccolo [2603]
	* src/common/Registers.ma (modified)

	Dead code commented out.


Tue, 05 Feb 2013 12:36:31 GMT sacerdot [2601]
	* extracted (added)
	* extracted/PROBLEMS (added)
	* extracted/aSM.ml (added)
	* extracted/aSM.mli (added)
	* extracted/aSMCosts.ml (added)
	* extracted/aSMCosts.mli (added)
	* extracted/aSMCostsSplit.ml (added)
	* extracted/aSMCostsSplit.mli (added)
	* extracted/aST.ml (added)
	* extracted/aST.mli (added)
	* extracted/abstractStatus.ml (added)
	* extracted/abstractStatus.mli (added)
	* extracted/arithmetic.ml (added)
	* extracted/arithmetic.mli (added)
	* extracted/bitVector.ml (added)
	* extracted/bitVector.mli (added)
	* extracted/bitVectorTrie.ml (added)
	* extracted/bitVectorTrie.mli (added)
	* extracted/bitVectorZ.ml (added)
	* extracted/bitVectorZ.mli (added)
	* extracted/bool.ml (added)
	* extracted/bool.mli (added)
	* extracted/byteValues.ml (added)
	* extracted/byteValues.mli (added)
	* extracted/casts.ml (added)
	* extracted/casts.mli (added)
	* extracted/cexec.ml (added)
	* extracted/cexec.mli (added)
	* extracted/cexecInd.ml (added)
	* extracted/cexecInd.mli (added)
	* extracted/cexecSound.ml (added)
	* extracted/cexecSound.mli (added)
	* extracted/char.ml (added)
	* extracted/char.mli (added)
	* extracted/classifyOp.ml (added)
	* extracted/classifyOp.mli (added)
	* extracted/cminor_syntax.ml (added)
	* extracted/cminor_syntax.mli (added)
	* extracted/compiler.ml (added)
	* extracted/compiler.mli (added)
	* extracted/coqlib.ml (added)
	* extracted/coqlib.mli (added)
	* extracted/core_notation.ml (added)
	* extracted/core_notation.mli (added)
	* extracted/costLabel.ml (added)
	* extracted/costLabel.mli (added)
	* extracted/csem.ml (added)
	* extracted/csem.mli (added)
	* extracted/csyntax.ml (added)
	* extracted/csyntax.mli (added)
	* extracted/deqsets.ml (added)
	* extracted/deqsets.mli (added)
	* extracted/div_and_mod.ml (added)
	* extracted/div_and_mod.mli (added)
	* extracted/division.ml (added)
	* extracted/division.mli (added)
	* extracted/errors.ml (added)
	* extracted/errors.mli (added)
	* extracted/events.ml (added)
	* extracted/events.mli (added)
	* extracted/extra_bool.ml (added)
	* extracted/extra_bool.mli (added)
	* extracted/extralib.ml (added)
	* extracted/extralib.mli (added)
	* extracted/extranat.ml (added)
	* extracted/extranat.mli (added)
	* extracted/fetch.ml (added)
	* extracted/fetch.mli (added)
	* extracted/floats.ml (added)
	* extracted/floats.mli (added)
	* extracted/foldStuff.ml (added)
	* extracted/foldStuff.mli (added)
	* extracted/fresh.ml (added)
	* extracted/fresh.mli (added)
	* extracted/frontEndMem.ml (added)
	* extracted/frontEndMem.mli (added)
	* extracted/frontEndOps.ml (added)
	* extracted/frontEndOps.mli (added)
	* extracted/frontEndVal.ml (added)
	* extracted/frontEndVal.mli (added)
	* extracted/frontend_misc.ml (added)
	* extracted/frontend_misc.mli (added)
	* extracted/genMem.ml (added)
	* extracted/genMem.mli (added)
	* extracted/globalenvs.ml (added)
	* extracted/globalenvs.mli (added)
	* extracted/graphs.ml (added)
	* extracted/graphs.mli (added)
	* extracted/hide.ml (added)
	* extracted/hide.mli (added)
	* extracted/hints_declaration.ml (added)
	* extracted/hints_declaration.mli (added)
	* extracted/iO.ml (added)
	* extracted/iO.mli (added)
	* extracted/iOMonad.ml (added)
	* extracted/iOMonad.mli (added)
	* extracted/identifiers.ml (added)
	* extracted/identifiers.mli (added)
	* extracted/initialisation.ml (added)
	* extracted/initialisation.mli (added)
	* extracted/integers.ml (added)
	* extracted/integers.mli (added)
	* extracted/interpret.ml (added)
	* extracted/interpret.mli (added)
	* extracted/jmeq.ml (added)
	* extracted/jmeq.mli (added)
	* extracted/label.ml (added)
	* extracted/label.mli (added)
	* extracted/labelledObjects.ml (added)
	* extracted/labelledObjects.mli (added)
	* extracted/list.ml (added)
	* extracted/list.mli (added)
	* extracted/listb.ml (added)
	* extracted/listb.mli (added)
	* extracted/lists.ml (added)
	* extracted/lists.mli (added)
	* extracted/logic.ml (added)
	* extracted/logic.mli (added)
	* extracted/memProperties.ml (added)
	* extracted/memProperties.mli (added)
	* extracted/memoryInjections.ml (added)
	* extracted/memoryInjections.mli (added)
	* extracted/monad.ml (added)
	* extracted/monad.mli (added)
	* extracted/nat.ml (added)
	* extracted/nat.mli (added)
	* extracted/option.ml (added)
	* extracted/option.mli (added)
	* extracted/order.ml (added)
	* extracted/order.mli (added)
	* extracted/pointers.ml (added)
	* extracted/pointers.mli (added)
	* extracted/positive.ml (added)
	* extracted/positive.mli (added)
	* extracted/positiveMap.ml (added)
	* extracted/positiveMap.mli (added)
	* extracted/preIdentifiers.ml (added)
	* extracted/preIdentifiers.mli (added)
	* extracted/preamble.ml (added)
	* extracted/proper.ml (added)
	* extracted/proper.mli (added)
	* extracted/pts.ml (added)
	* extracted/pts.mli (added)
	* extracted/rTLabs_syntax.ml (added)
	* extracted/rTLabs_syntax.mli (added)
	* extracted/registers.ml (added)
	* extracted/registers.mli (added)
	* extracted/relations.ml (added)
	* extracted/relations.mli (added)
	* extracted/russell.ml (added)
	* extracted/russell.mli (added)
	* extracted/setoids.ml (added)
	* extracted/setoids.mli (added)
	* extracted/sets.ml (added)
	* extracted/sets.mli (added)
	* extracted/simplifyCasts.ml (added)
	* extracted/simplifyCasts.mli (added)
	* extracted/smallstep.ml (added)
	* extracted/smallstep.mli (added)
	* extracted/smallstepExec.ml (added)
	* extracted/smallstepExec.mli (added)
	* extracted/star.ml (added)
	* extracted/star.mli (added)
	* extracted/status.ml (added)
	* extracted/status.mli (added)
	* extracted/statusProofs.ml (added)
	* extracted/statusProofs.mli (added)
	* extracted/string.ml (added)
	* extracted/string.mli (added)
	* extracted/structuredTraces.ml (added)
	* extracted/structuredTraces.mli (added)
	* extracted/switchRemoval.ml (added)
	* extracted/switchRemoval.mli (added)
	* extracted/toCminor.ml (added)
	* extracted/toCminor.mli (added)
	* extracted/toRTLabs.ml (added)
	* extracted/toRTLabs.mli (added)
	* extracted/typeComparison.ml (added)
	* extracted/typeComparison.mli (added)
	* extracted/types.ml (added)
	* extracted/types.mli (added)
	* extracted/util.ml (added)
	* extracted/util.mli (added)
	* extracted/utilBranch.ml (added)
	* extracted/utilBranch.mli (added)
	* extracted/values.ml (added)
	* extracted/values.mli (added)
	* extracted/vector.ml (added)
	* extracted/vector.mli (added)
	* extracted/z.ml (added)
	* extracted/z.mli (added)
	* src/ASM/BitVector.ma (modified)
	* src/Clight/Clight_abstract.ma (moved)
	* src/Clight/toCminor.ma (modified)
	* src/Clight/toCminorCorrectness.ma (modified)
	* src/Clight/toCminorCorrectnessExpr.ma (modified)
	* src/Clight/toCminorOps.ma (modified)
	* src/Cminor/Cminor_abstract.ma (moved)
	* src/Cminor/Cminor_semantics.ma (moved)
	* src/Cminor/Cminor_syntax.ma (moved)
	* src/Cminor/initialisation.ma (modified)
	* src/Cminor/toRTLabs.ma (modified)
	* src/Cminor/toRTLabsCorrectness.ma (modified)
	* src/ERTL/ERTL_semantics.ma (moved)
	* src/ERTLptr/ERTLptr_semantics.ma (moved)
	* src/ERTLptr/ERTLtoERTLptrOK.ma (modified)
	* src/LIN/LIN_semantics.ma (moved)
	* src/LTL/LTL_semantics.ma (moved)
	* src/RTL/RTL_semantics.ma (moved)
	* src/RTLabs/CostCheck.ma (modified)
	* src/RTLabs/CostInj.ma (modified)
	* src/RTLabs/CostSpec.ma (modified)
	* src/RTLabs/MeasurableTraces.ma (modified)
	* src/RTLabs/RTLabsToRTL.ma (modified)
	* src/RTLabs/RTLabs_abstract.ma (moved)
	* src/RTLabs/RTLabs_semantics.ma (moved)
	* src/RTLabs/RTLabs_syntax.ma (moved)
	* src/RTLabs/RTLabs_traces.ma (moved)
	* src/RTLabs/debug.ma (modified)
	* src/RTLabs/import.ma (modified)
	* src/common/Globalenvs.ma (modified)
	* src/joint/Traces.ma (modified)
	* src/joint/joint_semantics.ma (moved)
	* src/joint/semanticsUtils.ma (modified)
	* src/joint/stacksize.ma (modified)
	* src/utilities/extra_bool.ma (moved)

	Extraction to ocaml is now working, with a couple of bugs left.
	One ...


Thu, 31 Jan 2013 16:15:49 GMT tranquil [2599]
	* src/common/Identifiers.ma (modified)
	* src/common/PositiveMap.ma (modified)
	* src/joint/blocks.ma (modified)
	* src/joint/semantics_blocks.ma (modified)

	* map_opt and map on positive maps are now clean (erase empty ...


Thu, 31 Jan 2013 11:07:02 GMT campbell [2597]
	* src/Clight/toCminorCorrectness.ma (modified)
	* src/Cminor/toRTLabsCorrectness.ma (modified)
	* src/common/FEMeasurable.ma (added)

	Some work in progress on measurable subtrace preservation.


Thu, 31 Jan 2013 11:06:58 GMT campbell [2596]
	* src/common/Measurable.ma (modified)
	* src/correctness.ma (modified)

	Use a simpler stack cost map, and then specialise to each semantics.


Thu, 24 Jan 2013 18:52:38 GMT piccolo [2590]
	* src/ERTL/semantics.ma (modified)
	* src/ERTLptr/ERTLtoERTLptrOK.ma (modified)
	* src/ERTLptr/semantics.ma (modified)
	* src/common/ExtraMonads.ma (modified)
	* src/common/PositiveMap.ma (modified)
	* src/common/extraGlobalenvs.ma (modified)
	* src/joint/Traces.ma (modified)
	* src/joint/semantics.ma (modified)

	added monad machineary for ERTL to ERTLptr translation ...


Tue, 15 Jan 2013 14:58:12 GMT garnier [2582]
	* src/Clight/frontend_misc.ma (modified)
	* src/Clight/toCminor.ma (modified)
	* src/Clight/toCminorCorrectness.ma (modified)
	* src/common/FrontEndOps.ma (modified)

	Some progress on CL to CM.


Sat, 05 Jan 2013 12:41:13 GMT piccolo [2570]
	* src/ERTLptr/ERTLtoERTLptr.ma (modified)
	* src/ERTLptr/ERTLtoERTLptrOK.ma (added)
	* src/common/ExtraMonads.ma (added)
	* src/common/extraGlobalenvs.ma (modified)
	* src/joint/linearise.ma (modified)
	* src/joint/lineariseProof.ma (modified)
	* src/joint/semantics.ma (modified)

	ERTLtoERTLptr in place


Fri, 04 Jan 2013 13:59:37 GMT campbell [2569]
	* src/Clight/Csem.ma (modified)
	* src/Clight/memoryInjections.ma (modified)
	* src/Clight/test/addptrcharboth.c (added)
	* src/Clight/test/addptrcharboth.c.ma (added)
	* src/Clight/test/addptrcharboth.test.ma (added)
	* src/Clight/toCminorCorrectness.ma (modified)
	* src/common/Pointers.ma (modified)

	Fix Clight semantics for ptr + char.  (Compiler works anyway.)


Wed, 12 Dec 2012 13:43:03 GMT tranquil [2553]
	* src/common/StatusSimulation.ma (modified)
	* src/common/StructuredTraces.ma (modified)
	* src/joint/Traces.ma (modified)
	* src/joint/lineariseProof.ma (modified)

	as_classify changed to a partial function
	added a status for tailcalls


Mon, 10 Dec 2012 13:33:40 GMT tranquil [2548]
	* src/common/BackEndOps.ma (modified)
	* src/joint/lineariseProof.ma (modified)

	in BackEndOps, cleaner def of be_op2
	new statement of ...


Thu, 06 Dec 2012 15:02:36 GMT tranquil [2541]
	* src/common/Identifiers.ma (modified)
	* src/common/PositiveMap.ma (modified)

	adapted size notation to last matita lib update (01/12/2012)
	that ...


Thu, 06 Dec 2012 14:17:12 GMT tranquil [2540]
	* src/common/StatusSimulation.ma (modified)

	cl_jump case now provides a proof of costedness of the following
	state


Thu, 06 Dec 2012 13:48:40 GMT tranquil [2539]
	* src/common/StatusSimulation.ma (modified)

	added cl_jump case to trace_any_any_free


Wed, 05 Dec 2012 18:20:27 GMT campbell [2534]
	* src/common/Measurable.ma (modified)

	Tweak measurable definition to stop at the return from a function.


Wed, 05 Dec 2012 18:20:23 GMT campbell [2533]
	* src/Clight/toCminor.ma (modified)
	* src/common/Animation.ma (modified)

	Some fall out from removing floats.


Wed, 05 Dec 2012 12:28:20 GMT mckinna [2531]
	* src/ASM/ASMCosts.ma (modified)
	* src/common/StructuredTraces.ma (modified)

	Trivial tweaks.


Tue, 04 Dec 2012 17:29:43 GMT tranquil [2530]
	* src/common/StatusSimulation.ma (modified)

	temporary switch to cl_jump treated as cl_other
	fixed script for new ...


Fri, 30 Nov 2012 17:31:29 GMT campbell [2511]
	* src/Cminor/toRTLabsCorrectness.ma (added)
	* src/RTLabs/MeasurableTraces.ma (modified)
	* src/RTLabs/abstract.ma (modified)
	* src/common/Measurable.ma (modified)

	Conjecture main Cminor/RTLabs simulation results.
	Add a few notes ...


Thu, 29 Nov 2012 19:12:34 GMT mckinna [2508]
	* src/ASM/ASMCostsSplit.ma (modified)
	* src/common/StructuredTraces.ma (modified)
	* src/compiler.ma (modified)

	more tweaks. compiler and correctness still build.


Thu, 29 Nov 2012 14:32:50 GMT mckinna [2503]
	* src/common/StructuredTraces.ma (modified)

	tidied up, with new auxiliary defns, some refactoring, some code ...


Thu, 29 Nov 2012 10:59:34 GMT campbell [2502]
	* src/RTLabs/MeasurableTraces.ma (added)
	* src/common/Measurable.ma (modified)

	Sketch a little about how measurable traces might work with RTLabs ...


Wed, 28 Nov 2012 16:57:38 GMT garnier [2500]
	* src/Clight/frontend_misc.ma (modified)
	* src/Clight/memoryInjections.ma (modified)
	* src/Clight/toCminorCorrectness.ma (modified)
	* src/common/Errors.ma (modified)

	Continuing work on simulation in Clight/Cminor


Tue, 27 Nov 2012 16:50:51 GMT garnier [2496]
	* src/Clight/abstract.ma (modified)
	* src/Clight/frontend_misc.ma (modified)
	* src/Clight/toCminor.ma (modified)
	* src/Clight/toCminorCorrectness.ma (modified)
	* src/Cminor/abstract.ma (modified)
	* src/common/Errors.ma (modified)

	Some tentative work on the simulation proof for expressions, in order ...


Fri, 23 Nov 2012 14:47:22 GMT campbell [2487]
	* src/Clight/labelSimulation.ma (modified)
	* src/Clight/switchRemoval.ma (modified)
	* src/common/Executions.ma (modified)
	* src/common/SmallstepExec.ma (modified)

	Set up "after_n_steps" to enforce an invariant on states.


Fri, 23 Nov 2012 11:18:57 GMT campbell [2486]
	* src/common/Measurable.ma (added)

	First go at a generalised version of measurable.


Tue, 20 Nov 2012 13:28:06 GMT tranquil [2478]
	* src/common/extraGlobalenvs.ma (modified)

	unified is_internal_function_of_program and is_internal_function


Tue, 20 Nov 2012 12:41:58 GMT tranquil [2477]
	* src/common/StatusSimulation.ma (modified)
	* src/joint/Traces.ma (modified)

	status_simulation reformulated
	definition of joint_classify split up ...


Mon, 19 Nov 2012 17:04:24 GMT piccolo [2476]
	* src/common/extraGlobalenvs.ma (modified)
	* src/joint/lineariseProof.ma (modified)

	fixed commutation lemmas in lineariseProof
	started proof of main ...


Mon, 19 Nov 2012 09:57:08 GMT tranquil [2474]
	* src/common/extraGlobalenvs.ma (modified)
	* src/joint/linearise.ma (modified)

	changed form of a statement


Fri, 16 Nov 2012 17:59:24 GMT tranquil [2473]
	* src/common/extraGlobalenvs.ma (added)
	* src/joint/Traces.ma (modified)
	* src/joint/linearise.ma (modified)
	* src/joint/semantics.ma (modified)

	put some generic stuff we need in the back end in extraGlobalenvs ...


Fri, 16 Nov 2012 17:41:49 GMT campbell [2471]
	* src/Clight/toCminorCorrectness.ma (modified)
	* src/common/Globalenvs.ma (modified)

	Tame global environments a little.


Thu, 15 Nov 2012 18:06:45 GMT tranquil [2470]
	* src/common/ByteValues.ma (modified)
	* src/joint/Traces.ma (modified)
	* src/joint/semantics.ma (modified)
	* src/joint/semanticsUtils.ma (modified)

	completely separated program counters from code pointers in joint ...


Thu, 15 Nov 2012 17:12:57 GMT garnier [2468]
	* src/Clight/Cexec.ma (modified)
	* src/Clight/CexecComplete.ma (modified)
	* src/Clight/CexecInd.ma (modified)
	* src/Clight/CexecSound.ma (modified)
	* src/Clight/ClassifyOp.ma (modified)
	* src/Clight/Csem.ma (modified)
	* src/Clight/Csyntax.ma (modified)
	* src/Clight/MemProperties.ma (modified)
	* src/Clight/SimplifyCasts.ma (modified)
	* src/Clight/TypeComparison.ma (modified)
	* src/Clight/frontend_misc.ma (modified)
	* src/Clight/labelSimulation.ma (modified)
	* src/Clight/memoryInjections.ma (modified)
	* src/Clight/switchRemoval.ma (modified)
	* src/Clight/toCminor.ma (modified)
	* src/Cminor/initialisation.ma (modified)
	* src/common/AST.ma (modified)
	* src/common/Events.ma (modified)
	* src/common/FrontEndOps.ma (modified)
	* src/common/FrontEndVal.ma (modified)
	* src/common/Globalenvs.ma (modified)
	* src/common/IO.ma (modified)
	* src/common/Values.ma (modified)

	Floats are gone from the front-end. Some trace amount might remain in ...


Wed, 14 Nov 2012 12:20:24 GMT tranquil [2463]
	* src/common/StatusSimulation.ma (modified)

	swapped back call_rel and ret_rel...


Wed, 14 Nov 2012 09:31:55 GMT tranquil [2462]
	* src/common/BackEndOps.ma (modified)
	* src/common/ByteValues.ma (modified)
	* src/joint/Joint.ma (modified)
	* src/joint/semantics.ma (modified)

	separated in back end values program counters from code pointers ...


Tue, 13 Nov 2012 17:30:55 GMT campbell [2459]
	* src/common/SmallstepExec.ma (modified)

	Syntax update


Tue, 13 Nov 2012 10:30:23 GMT tranquil [2457]
	* src/common/StatusSimulation.ma (modified)
	* src/joint/Joint.ma (modified)
	* src/joint/Traces.ma (modified)
	* src/joint/semantics.ma (modified)
	* src/joint/semanticsUtils.ma (moved)

	rewritten function handling in joint
	swapped call_rel with ret_rel ...


Mon, 12 Nov 2012 15:30:03 GMT tranquil [2453]
	* src/common/Errors.ma (modified)
	* src/common/IOMonad.ma (modified)
	* src/common/PositiveMap.ma (modified)
	* src/utilities/monad.ma (modified)

	come changes in monad notation to
	* avoid pretty printed monsters
	* ...


Thu, 08 Nov 2012 17:47:04 GMT campbell [2444]
	* src/common/IOMonad.ma (modified)
	* src/common/SmallstepExec.ma (modified)

	Some inversion lemmas for after_n_steps for dealing with >1 source ...


Thu, 08 Nov 2012 13:27:54 GMT tranquil [2443]
	* src/ERTL/ERTLToLTL.ma (modified)
	* src/LIN/LINToASM.ma (modified)
	* src/LIN/joint_LTL_LIN_semantics.ma (modified)
	* src/LIN/semantics.ma (modified)
	* src/LTL/semantics.ma (modified)
	* src/common/ByteValues.ma (modified)
	* src/joint/SemanticUtils.ma (modified)
	* src/joint/Traces.ma (modified)
	* src/joint/TranslateUtils.ma (modified)
	* src/joint/lineariseProof.ma (modified)
	* src/joint/semantics.ma (modified)
	* src/utilities/deqsets.ma (modified)
	* src/utilities/lists.ma (modified)

	changed joint's stack pointer and internal stack


Wed, 07 Nov 2012 15:42:02 GMT campbell [2439]
	* src/RTLabs/Traces.ma (modified)
	* src/common/AST.ma (modified)
	* src/common/Errors.ma (modified)
	* src/common/Globalenvs.ma (modified)
	* src/common/Identifiers.ma (modified)
	* src/common/PositiveMap.ma (modified)

	Get a proper reverse mapping of function blocks to identifiers by ...


Tue, 06 Nov 2012 15:13:00 GMT tranquil [2436]
	* src/common/StatusSimulation.ma (modified)

	small changes


Tue, 06 Nov 2012 15:12:21 GMT tranquil [2435]
	* src/common/BackEndOps.ma (modified)
	* src/common/ByteValues.ma (modified)
	* src/common/FrontEndVal.ma (modified)

	new back end operations


Tue, 06 Nov 2012 14:17:23 GMT campbell [2432]
	* src/common/FrontEndOps.ma (modified)

	Remove off-the-end pointers from front end ops.


Tue, 06 Nov 2012 11:53:46 GMT garnier [2429]
	* src/Clight/Csem.ma (modified)
	* src/common/FrontEndMem.ma (modified)

	Restrict semantics of pointer comparison to what CompCert does - i.e. ...


Tue, 06 Nov 2012 11:02:13 GMT campbell [2428]
	* src/Clight/Cexec.ma (modified)
	* src/Clight/CexecComplete.ma (modified)
	* src/Clight/CexecEquiv.ma (modified)
	* src/Clight/CexecSound.ma (modified)
	* src/Clight/Csem.ma (modified)
	* src/Clight/SimplifyCasts.ma (modified)
	* src/Clight/labelSimulation.ma (modified)
	* src/common/IOMonad.ma (modified)

	Tighten requirements on switch statements in Clight to only give ...


Wed, 31 Oct 2012 16:36:51 GMT boender [2426]
	* src/common/StructuredTraces_jaap.ma (deleted)
	* src/joint/Joint_jaap.ma (deleted)
	* src/joint/stacksize.ma (modified)

	- updated stacksize to reflect new developments, completed proof
	- ...


Tue, 30 Oct 2012 16:23:44 GMT tranquil [2423]
	* src/common/StructuredTraces.ma (modified)

	as_classifier predicate → as_classify function
	as_call predicate ...


Tue, 30 Oct 2012 15:18:20 GMT tranquil [2421]
	* src/common/StatusSimulation.ma (modified)

	added simulation of flat prefix, and comments to explain the code


Tue, 30 Oct 2012 11:32:31 GMT campbell [2420]
	* src/RTLabs/CostInj.ma (modified)
	* src/common/Identifiers.ma (modified)
	* src/common/PositiveMap.ma (modified)

	Tidy away generic results about folds on positive/identifier maps.


Mon, 29 Oct 2012 17:19:56 GMT campbell [2418]
	* src/RTLabs/CostInj.ma (added)
	* src/common/Identifiers.ma (modified)

	Add a checking function for the uniqueness of cost labels in RTLabs ...


Thu, 25 Oct 2012 14:36:07 GMT boender [2417]
	* src/common/StructuredTraces.ma (modified)
	* src/common/StructuredTraces_jaap.ma (added)
	* src/joint/Joint_jaap.ma (modified)
	* src/joint/stacksize.ma (modified)

	- reverted changes to StructuredTraces (shouldn't have been committed ...


Tue, 23 Oct 2012 13:57:02 GMT campbell [2415]
	* src/common/Globalenvs.ma (modified)
	* src/common/Identifiers.ma (modified)
	* src/common/PositiveMap.ma (modified)

	Add the ability to map blocks to symbols in preparation for stack
	space.


Tue, 23 Oct 2012 09:15:28 GMT tranquil [2413]
	* src/common/StatusSimulation.ma (added)
	* src/common/StructuredTraces.ma (modified)

	* tal_rel corrected to include cases where tal_base_call \approx ...


Wed, 17 Oct 2012 13:35:08 GMT boender [2398]
	* src/common/StructuredTraces.ma (modified)
	* src/joint/Joint_jaap.ma (added)
	* src/joint/stacksize.ma (added)

	- committed start of stacksize


Fri, 12 Oct 2012 13:33:53 GMT campbell [2395]
	* src/Clight/Csem.ma (modified)
	* src/Clight/test/endptr.test.ma (modified)
	* src/Clight/test/endptr2.c (added)
	* src/Clight/test/endptr2.c.ma (added)
	* src/Clight/test/endptr2.test.ma (copied)
	* src/Cminor/semantics.ma (modified)
	* src/RTLabs/semantics.ma (modified)
	* src/common/FrontEndMem.ma (modified)
	* src/common/FrontEndOps.ma (modified)

	Proper handling of comparison of pointers off-the-end of an object. ...


Wed, 26 Sep 2012 08:17:32 GMT campbell [2338]
	* src/Clight/labelSimulation.ma (modified)
	* src/common/Executions.ma (modified)
	* src/common/SmallstepExec.ma (modified)

	Use much nicer definition for making several steps in the labelling ...


Thu, 20 Sep 2012 16:57:34 GMT campbell [2335]
	* src/Cminor/toRTLabs.ma (modified)
	* src/common/Identifiers.ma (modified)
	* src/common/PositiveMap.ma (modified)

	Deal with goto labels in RTLabs to Cminor by fixing up goto ...


Wed, 12 Sep 2012 10:36:46 GMT garnier [2332]
	* src/Clight/frontend_misc.ma (modified)
	* src/Clight/memoryInjections.ma (modified)
	* src/Clight/switchRemoval.ma (modified)
	* src/common/GenMem.ma (modified)

	Some progress on switch removal. Small fix in the definition of free, ...


Mon, 03 Sep 2012 11:16:29 GMT campbell [2319]
	* src/Clight/label.ma (modified)
	* src/Clight/labelSimulation.ma (modified)
	* src/Clight/labelSpecification.ma (modified)
	* src/Cminor/initialisation.ma (modified)
	* src/Cminor/toRTLabs.ma (modified)
	* src/common/AST.ma (modified)
	* src/common/Globalenvs.ma (modified)
	* src/compiler.ma (modified)

	Generate per-program cost labels rather than per-function ones, and ...


Fri, 31 Aug 2012 14:12:35 GMT campbell [2314]
	* src/ASM/Util.ma (modified)
	* src/RTLabs/CostCheck.ma (modified)
	* src/RTLabs/Traces.ma (modified)
	* src/common/Identifiers.ma (modified)
	* src/utilities/bool.ma (added)
	* src/utilities/listb.ma (added)
	* src/utilities/lists.ma (modified)

	Move generic definitions from recent commit to appropriate places.


Thu, 30 Aug 2012 14:47:58 GMT campbell [2307]
	* src/ASM/Util.ma (modified)
	* src/RTLabs/CostCheck.ma (modified)
	* src/RTLabs/CostSpec.ma (modified)
	* src/RTLabs/Traces.ma (modified)
	* src/common/Identifiers.ma (modified)
	* src/common/PositiveMap.ma (modified)

	Half the proofs for sound cost labelling check.


Thu, 30 Aug 2012 14:47:54 GMT campbell [2305]
	* src/RTLabs/CostCheck.ma (modified)
	* src/common/Identifiers.ma (modified)
	* src/common/PositiveMap.ma (modified)

	RTLabs cost spec checking function implemented (lacks proof, or much ...


Fri, 24 Aug 2012 15:41:18 GMT campbell [2303]
	* src/RTLabs/CostCheck.ma (added)
	* src/RTLabs/CostSpec.ma (modified)
	* src/common/Identifiers.ma (modified)
	* src/common/PositiveMap.ma (modified)

	Some preliminary checking of cost labelling properties in RTLabs.


Tue, 21 Aug 2012 17:00:42 GMT campbell [2299]
	* src/RTLabs/Traces.ma (modified)
	* src/common/StructuredTraces.ma (modified)

	Soundly labelled RTLabs structured traces are "unrepeating".


Mon, 13 Aug 2012 12:18:31 GMT campbell [2296]
	* src/RTLabs/Traces.ma (modified)
	* src/RTLabs/semantics.ma (modified)
	* src/common/Pointers.ma (modified)
	* src/utilities/deqsets.ma (added)

	Tidy up some ill-placed definitions.


Thu, 02 Aug 2012 13:18:11 GMT tranquil [2286]
	* src/ASM/I8051.ma (modified)
	* src/ASM/Util.ma (modified)
	* src/ASM/Vector.ma (modified)
	* src/ERTL/ERTL.ma (modified)
	* src/ERTL/ERTLToLTL.ma (modified)
	* src/ERTL/ERTLToLTL_paolo.ma (deleted)
	* src/ERTL/ERTL_paolo.ma (deleted)
	* src/ERTL/Interference.ma (modified)
	* src/ERTL/Interference_paolo.ma (deleted)
	* src/ERTL/liveness.ma (modified)
	* src/ERTL/liveness_paolo.ma (deleted)
	* src/ERTL/semantics.ma (modified)
	* src/ERTL/semantics_paolo.ma (deleted)
	* src/LIN/LIN.ma (modified)
	* src/LIN/LINToASM.ma (modified)
	* src/LIN/LIN_paolo.ma (deleted)
	* src/LIN/joint_LTL_LIN.ma (modified)
	* src/LIN/joint_LTL_LIN_paolo.ma (deleted)
	* src/LIN/joint_LTL_LIN_semantics.ma (modified)
	* src/LIN/joint_LTL_LIN_semantics_paolo.ma (deleted)
	* src/LIN/semantics.ma (modified)
	* src/LIN/semantics_paolo.ma (deleted)
	* src/LTL/LTL.ma (modified)
	* src/LTL/LTLToLIN.ma (modified)
	* src/LTL/LTLToLIN_paolo.ma (deleted)
	* src/LTL/LTL_paolo.ma (deleted)
	* src/LTL/semantics.ma (modified)
	* src/LTL/semantics_paolo.ma (deleted)
	* src/RTL/RTL.ma (modified)
	* src/RTL/RTLTailcall.ma (modified)
	* src/RTL/RTLTailcall_paolo.ma (deleted)
	* src/RTL/RTLToERTL.ma (modified)
	* src/RTL/RTLToERTL_paolo.ma (deleted)
	* src/RTL/RTL_paolo.ma (deleted)
	* src/RTL/semantics.ma (modified)
	* src/RTL/semantics_paolo.ma (deleted)
	* src/RTLabs/RTLabsToRTL.ma (modified)
	* src/RTLabs/RTLabsToRTL_paolo.ma (deleted)
	* src/common/AST.ma (modified)
	* src/common/BackEndOps.ma (added)
	* src/common/ByteValues.ma (modified)
	* src/common/ByteValues_paolo.ma (deleted)
	* src/common/FrontEndVal.ma (modified)
	* src/common/Registers.ma (modified)
	* src/compiler.ma (modified)
	* src/joint/BEMem.ma (modified)
	* src/joint/Joint.ma (modified)
	* src/joint/Joint_paolo.ma (deleted)
	* src/joint/SemanticUtils.ma (modified)
	* src/joint/Traces.ma (modified)
	* src/joint/TranslateUtils.ma (modified)
	* src/joint/TranslateUtils_paolo.ma (deleted)
	* src/joint/blocks.ma (modified)
	* src/joint/linearise.ma (modified)
	* src/joint/semantics.ma (modified)
	* src/joint/semanticsUtils_paolo.ma (deleted)
	* src/joint/semantics_paolo.ma (deleted)
	* src/utilities/extranat.ma (modified)

	Big update!

	* merge of all _paolo variants
	* reorganised some ...


Mon, 30 Jul 2012 14:54:33 GMT tranquil [2277]
	* src/common/ByteValues_paolo.ma (modified)

	* replaced incorrect use of subvector_with


Mon, 30 Jul 2012 11:05:55 GMT tranquil [2275]
	* src/ASM/I8051.ma (modified)
	* src/common/ByteValues.ma (modified)
	* src/common/ByteValues_paolo.ma (copied)

	* moved around some code (I8051.ma does not depend on ByteValues.ma ...


Fri, 20 Jul 2012 16:36:34 GMT campbell [2226]
	* src/RTLabs/CostSpec.ma (modified)
	* src/RTLabs/Traces.ma (modified)
	* src/common/Globalenvs.ma (modified)

	Whole program proof.


Fri, 20 Jul 2012 08:58:15 GMT sacerdot [2222]
	* src/ASM/PolicyFront.ma (modified)
	* src/common/Identifiers.ma (modified)

	More robust to possible future changes to the "in match" semantics ...


Thu, 19 Jul 2012 16:45:49 GMT campbell [2218]
	* src/RTLabs/CostSpec.ma (added)
	* src/RTLabs/Traces.ma (modified)
	* src/common/Pointers.ma (modified)

	Separate out cost properties required of RTLabs programs from the ...


Wed, 18 Jul 2012 10:27:02 GMT campbell [2206]
	* src/common/Executions.ma (modified)

	Add note about cost maps to simulation definition.


Tue, 17 Jul 2012 16:57:40 GMT campbell [2203]
	* src/Clight/Cexec.ma (modified)
	* src/Clight/labelSimulation.ma (modified)
	* src/common/Executions.ma (modified)
	* src/common/SmallstepExec.ma (modified)

	A general result about simulations of executions.


Tue, 17 Jul 2012 16:57:39 GMT campbell [2202]
	* src/Clight/labelSimulation.ma (modified)
	* src/Clight/labelSpecification.ma (modified)
	* src/common/Executions.ma (added)
	* src/common/SmallstepExec.ma (modified)

	Start defining equivalent executions.


Mon, 16 Jul 2012 14:59:09 GMT tranquil [2186]
	* src/RTL/RTL_paolo.ma (modified)
	* src/common/StructuredTraces.ma (modified)
	* src/joint/Joint_paolo.ma (modified)
	* src/joint/Traces.ma (moved)
	* src/joint/blocks.ma (modified)
	* src/joint/semantics_blocks.ma (modified)
	* src/joint/semantics_paolo.ma (modified)

	updated joint semantics


Fri, 13 Jul 2012 17:59:43 GMT campbell [2185]
	* src/common/FrontEndMem.ma (modified)
	* src/common/GenMem.ma (modified)
	* src/common/Globalenvs.ma (modified)
	* src/common/Pointers.ma (modified)
	* src/joint/BEMem.ma (modified)
	* src/joint/semantics.ma (modified)

	Use bitvectors for offsets.


Fri, 13 Jul 2012 09:20:36 GMT tranquil [2182]
	* src/ERTL/liveness_paolo.ma (modified)
	* src/LIN/LIN_paolo.ma (added)
	* src/LTL/LTLToLIN_paolo.ma (added)
	* src/common/Identifiers.ma (modified)
	* src/joint/Joint_paolo.ma (modified)
	* src/joint/TranslateUtils_paolo.ma (modified)
	* src/joint/linearise.ma (added)

	updated linearisation pass


Thu, 12 Jul 2012 14:46:24 GMT campbell [2180]
	* src/Clight/test/oneoff.c (added)
	* src/Clight/test/oneoff.c.ma (added)
	* src/Clight/test/oneoff.test.ma (added)
	* src/common/GenMem.ma (modified)

	Fix off-by-one error in GenMem.ma.


Thu, 12 Jul 2012 12:56:50 GMT campbell [2177]
	* src/ASM/Arithmetic.ma (modified)
	* src/Clight/Csem.ma (modified)
	* src/common/FrontEndOps.ma (modified)

	Tidy up multiplication.


Thu, 12 Jul 2012 11:28:28 GMT campbell [2176]
	* src/Clight/Cexec.ma (modified)
	* src/Clight/CexecComplete.ma (modified)
	* src/Clight/CexecSound.ma (modified)
	* src/Clight/ClassifyOp.ma (modified)
	* src/Clight/Csem.ma (modified)
	* src/Clight/Csyntax.ma (modified)
	* src/Clight/SimplifyCasts.ma (modified)
	* src/Clight/TypeComparison.ma (modified)
	* src/Clight/clightPrintMatita.ml (modified)
	* src/Clight/labelSimulation.ma (modified)
	* src/Clight/test/duff.c.ma (modified)
	* src/Clight/test/insertsort.c.ma (modified)
	* src/Clight/test/memorymodel.ma (modified)
	* src/Clight/test/null-op.c.ma (modified)
	* src/Clight/test/search.c.ma (modified)
	* src/Clight/test/sum.c.ma (modified)
	* src/Clight/toCminor.ma (modified)
	* src/Cminor/initialisation.ma (modified)
	* src/Cminor/semantics.ma (modified)
	* src/Cminor/syntax.ma (modified)
	* src/Cminor/toRTLabs.ma (modified)
	* src/RTL/semantics.ma (modified)
	* src/RTLabs/RTLabsToRTL.ma (modified)
	* src/RTLabs/semantics.ma (modified)
	* src/common/AST.ma (modified)
	* src/common/Animation.ma (modified)
	* src/common/ByteValues.ma (modified)
	* src/common/FrontEndOps.ma (modified)
	* src/common/FrontEndVal.ma (modified)
	* src/common/GenMem.ma (modified)
	* src/common/Globalenvs.ma (modified)
	* src/common/IO.ma (modified)
	* src/common/Pointers.ma (modified)
	* src/common/Values.ma (modified)
	* src/joint/BEMem.ma (modified)
	* src/joint/SemanticUtils.ma (modified)
	* src/joint/semantics.ma (modified)

	Remove memory spaces other than XData and Code; simplify pointers as ...


Fri, 06 Jul 2012 09:25:43 GMT tranquil [2155]
	* src/RTL/RTL_paolo.ma (modified)
	* src/RTLabs/RTLabsToRTL_paolo.ma (modified)
	* src/common/Identifiers.ma (modified)
	* src/joint/Joint_paolo.ma (modified)
	* src/joint/TranslateUtils_paolo.ma (modified)
	* src/joint/blocks.ma (modified)
	* src/utilities/bindLists.ma (modified)

	updates to blocks and RTLabs to RTL translation (which sidesteps ...


Mon, 02 Jul 2012 14:12:12 GMT campbell [2145]
	* src/Clight/labelSimulation.ma (modified)
	* src/Clight/labelSpecification.ma (modified)
	* src/common/IOMonad.ma (modified)
	* src/common/SmallstepExec.ma (modified)

	Cost labelling doesn't affect interaction.


Thu, 28 Jun 2012 08:59:18 GMT boender [2133]
	* src/common/LabelledObjects.ma (modified)

	- moved does_not_occur_occur_absurd


Wed, 27 Jun 2012 17:14:32 GMT mulligan [2129]
	* src/ASM/AssemblyProof.ma (modified)
	* src/ASM/AssemblyProofSplit.ma (modified)
	* src/ASM/AssemblyProofSplitSplit.ma (modified)
	* src/ASM/Interpret.ma (modified)
	* src/common/StructuredTraces.ma (modified)

	Large changes from today trying to complete the main theorem.  Again
	:(


Wed, 27 Jun 2012 10:04:27 GMT campbell [2118]
	* src/Clight/labelSimulation.ma (modified)
	* src/common/SmallstepExec.ma (modified)

	Labelling preserves behaviour.


Wed, 27 Jun 2012 10:04:23 GMT campbell [2117]
	* src/common/Globalenvs.ma (modified)

	Workaround for bug in Matita.


Tue, 26 Jun 2012 15:30:41 GMT sacerdot [2111]
	* src/ASM/Arithmetic.ma (modified)
	* src/ASM/Assembly.ma (modified)
	* src/ASM/AssemblyProof.ma (modified)
	* src/ASM/Status.ma (modified)
	* src/ASM/Util.ma (modified)
	* src/common/Identifiers.ma (modified)

	Cleanup: lemmas/theorems/axioms moved to the right places.


Fri, 22 Jun 2012 12:07:38 GMT campbell [2107]
	* src/Clight/labelSimulation.ma (modified)
	* src/common/Globalenvs.ma (modified)

	Memory initialisation and program transformations.


Thu, 21 Jun 2012 15:21:04 GMT campbell [2105]
	* src/Clight/labelSimulation.ma (modified)
	* src/common/AST.ma (modified)
	* src/common/GenMem.ma (modified)
	* src/common/Globalenvs.ma (modified)

	Show some results about globalenvs and program transformations.


Thu, 21 Jun 2012 15:21:03 GMT campbell [2104]
	* src/common/PositiveMap.ma (modified)

	Fill in misc axiom.


Thu, 21 Jun 2012 15:21:02 GMT campbell [2103]
	* src/Clight/SimplifyCasts.ma (modified)
	* src/Clight/label.ma (modified)
	* src/Clight/labelSimulation.ma (modified)
	* src/Cminor/toRTLabs.ma (modified)
	* src/ERTL/ERTLToLTL.ma (modified)
	* src/LTL/LTLToLIN.ma (modified)
	* src/RTL/RTLTailcall.ma (modified)
	* src/RTL/RTLToERTL.ma (modified)
	* src/RTLabs/RTLabsToRTL.ma (modified)
	* src/RTLabs/RTLabsToRTL_paolo.ma (modified)
	* src/common/AST.ma (modified)
	* src/joint/Erasure.ma (modified)

	Make transform_*program take a more general transformation to make ...


Tue, 12 Jun 2012 08:52:37 GMT campbell [2044]
	* src/RTLabs/Traces.ma (modified)
	* src/RTLabs/semantics.ma (modified)
	* src/common/IOMonad.ma (modified)
	* src/common/StructuredTraces.ma (modified)

	PCs for RTLabs structured traces.


Fri, 08 Jun 2012 14:32:03 GMT sacerdot [2032]
	* src/ASM/ASM.ma (modified)
	* src/ASM/Arithmetic.ma (modified)
	* src/ASM/Assembly.ma (modified)
	* src/ASM/AssemblyProof.ma (modified)
	* src/ASM/AssemblyProofSplit.ma (modified)
	* src/ASM/Interpret.ma (modified)
	* src/ASM/Policy.ma (modified)
	* src/ASM/Status.ma (modified)
	* src/ASM/StatusProofs.ma (modified)
	* src/ASM/Util.ma (modified)
	* src/ASM/Vector.ma (modified)
	* src/ASM/WellLabeled.ma (modified)
	* src/Clight/Csem.ma (modified)
	* src/Clight/SimplifyCasts.ma (modified)
	* src/Clight/casts.ma (modified)
	* src/Cminor/toRTLabs.ma (modified)
	* src/RTL/RTLToERTL.ma (modified)
	* src/RTLabs/RTLabsToRTL.ma (modified)
	* src/RTLabs/RTLabsToRTL_paolo.ma (modified)
	* src/common/FrontEndOps.ma (modified)
	* src/common/FrontEndVal.ma (modified)
	* src/common/Integers.ma (modified)
	* src/common/Values.ma (modified)

	!! BEWARE: major commit !!

	1) [affects everybody]
	   split for ...


Thu, 31 May 2012 13:10:30 GMT campbell [2010]
	* src/common/Globalenvs.ma (modified)

	Make globalenvs use proper maps.