#
# ChangeLog for src
#
# Generated by Trac 1.2
# Dec 13, 2019, 10:45:11 PM

Thu, 28 Feb 2013 16:56:55 GMT mckinna [2753]
	* src/compiler.ma (modified)

	Further tidying up thanks to Claudio's strong_decidable intervention; ...


Thu, 28 Feb 2013 13:36:34 GMT mckinna [2752]
	* src/compiler.ma (modified)

	Fixed TODO regarding length of list_instr
	Added ASM/CodeMemory.ma to ...


Thu, 28 Feb 2013 13:29:46 GMT mckinna [2751]
	* src/common/ErrorMessages.ma (modified)

	Added
	 | AssemblyTooLarge : ErrorMessage
	to complete compiler.ma


Thu, 28 Feb 2013 13:27:31 GMT mckinna [2750]
	* src/ASM/CodeMemory.ma (added)

	Miscellany on 2^16 bounds, memory, lemmas+definitions.

	Completes ...


Wed, 27 Feb 2013 21:46:05 GMT sacerdot [2745]
	* src/ASM/Policy.ma (modified)
	* src/compiler.ma (modified)

	1. Complexity of policy computation lowered from O(n^2) to O(n)
	2. ...


Wed, 27 Feb 2013 16:16:00 GMT sacerdot [2741]
	* src/ERTLptr/uses.ma (added)

	File used only by untrusted code.
	Implemented in Matita to exploit ...


Wed, 27 Feb 2013 15:37:31 GMT sacerdot [2739]
	* src/ERTLptr/ERTLptrToLTL.ma (modified)
	* src/ERTLptr/Interference.ma (modified)

	The graph colouring algorithm takes in input also the function.


Tue, 26 Feb 2013 18:37:41 GMT garnier [2737]
	* src/Clight/Clight_abstract.ma (modified)
	* src/Clight/toCminorCorrectness.ma (modified)
	* src/Cminor/Cminor_abstract.ma (modified)

	Commit of current proof state for Clight to Cminor translation.


Tue, 26 Feb 2013 14:31:40 GMT mckinna [2734]
	* src/Clight/switchRemoval.ma (modified)

	yet another puzzling automation failure, in the repaired case:
	"//" ...


Mon, 25 Feb 2013 22:03:20 GMT sacerdot [2732]
	* src/utilities/adt/register_table.ma (deleted)
	* src/utilities/adt/set_adt.ma (modified)
	* src/utilities/adt/set_table_adt.ma (deleted)
	* src/utilities/adt/table_adt.ma (deleted)

	Unused code removed.


Mon, 25 Feb 2013 20:42:12 GMT sacerdot [2728]
	* src/RTLabs/CostCheck.ma (modified)
	* src/RTLabs/RTLabs_traces.ma (modified)
	* src/utilities/listb_extra.ma (moved)

	listb.ma => listb_extra.ma  for extraction


Mon, 25 Feb 2013 17:43:44 GMT campbell [2727]
	* src/common/FEMeasurable.ma (modified)
	* src/common/Measurable.ma (modified)

	Remove a couple of redundant hypotheses.


Mon, 25 Feb 2013 11:11:39 GMT campbell [2726]
	* src/common/FEMeasurable.ma (modified)

	Show max stack preserved in FEMeasurable.


Mon, 25 Feb 2013 10:45:57 GMT campbell [2725]
	* src/common/FEMeasurable.ma (modified)
	* src/common/Measurable.ma (modified)

	Add observables to FEMeasurable proof; fix silly typo.


Sun, 24 Feb 2013 19:39:19 GMT campbell [2724]
	* src/RTLabs/CostCheck.ma (modified)
	* src/RTLabs/RTLabs_abstract.ma (modified)
	* src/RTLabs/RTLabs_traces.ma (modified)
	* src/common/ErrorMessages.ma (modified)
	* src/compiler.ma (modified)

	Add RTLabs cost labelling checks to compiler.ma.


Sat, 23 Feb 2013 16:05:04 GMT campbell [2723]
	* src/joint/TranslateUtils.ma (modified)

	Library name typo fixed.


Sat, 23 Feb 2013 16:05:03 GMT campbell [2722]
	* src/Clight/Cexec.ma (modified)
	* src/Clight/CexecComplete.ma (modified)
	* src/Clight/CexecSound.ma (modified)
	* src/Clight/Csem.ma (modified)
	* src/Clight/SimplifyCasts.ma (modified)
	* src/Clight/labelSimulation.ma (modified)
	* src/Clight/switchRemoval.ma (modified)
	* src/Cminor/Cminor_semantics.ma (modified)
	* src/RTLabs/RTLabs_semantics.ma (modified)
	* src/common/Globalenvs.ma (modified)
	* src/common/Measurable.ma (modified)
	* src/correctness.ma (modified)

	It's easier to keep the real function identifier in front-end ...


Sat, 23 Feb 2013 11:03:13 GMT tranquil [2720]
	* src/common/BackEndOps.ma (modified)

	implemented back end ops that were still axioms


Sat, 23 Feb 2013 00:03:15 GMT sacerdot [2716]
	* src/RTLabs/CostCheck.ma (modified)
	* src/RTLabs/RTLabs_abstract.ma (modified)
	* src/RTLabs/RTLabs_traces.ma (modified)
	* src/joint/TranslateUtils.ma (modified)
	* src/utilities/deqsets_extra.ma (moved)

	utilities/deqsets.ma => utilities/deqsets_extra.ma for extraction


Fri, 22 Feb 2013 22:41:04 GMT sacerdot [2715]
	* src/BACKEND_BROKEN_FILES (modified)

	Policy.ma repaired


Fri, 22 Feb 2013 22:20:03 GMT sacerdot [2714]
	* src/ASM/PolicyStep.ma (modified)

	PolicyStep.ma repaired


Fri, 22 Feb 2013 21:39:26 GMT sacerdot [2713]
	* src/ASM/PolicyFront.ma (modified)
	* src/BACKEND_BROKEN_FILES (modified)

	PolicyFront.ma repaired


Fri, 22 Feb 2013 19:04:38 GMT tranquil [2712]
	* src/joint/Joint.ma (modified)
	* src/joint/linearise.ma (modified)

	changed some fields of joint_internal_function's invariant
	fixed ...


Fri, 22 Feb 2013 18:23:24 GMT sacerdot [2711]
	* src/BACKEND_BROKEN_FILES (modified)

	...


Fri, 22 Feb 2013 18:20:24 GMT sacerdot [2710]
	* src/ASM/ASMCosts.ma (modified)
	* src/ASM/Status.ma (modified)
	* src/ASM/WellLabeled.ma (modified)
	* src/BACKEND_BROKEN_FILES (modified)

	ASMCosts.ma repaired


Fri, 22 Feb 2013 18:17:44 GMT sacerdot [2709]
	* src/compiler.ma (modified)

	LINToAsm repaired


Fri, 22 Feb 2013 18:11:30 GMT tranquil [2708]
	* src/ASM/ASM.ma (modified)
	* src/LIN/LINToASM.ma (modified)
	* src/joint/TranslateUtils.ma (modified)
	* src/joint/linearise.ma (modified)
	* src/joint/semanticsUtils.ma (modified)
	* src/utilities/state.ma (modified)

	fixed linearise and LINToASM
	LINToASM has now correct transformation ...


Fri, 22 Feb 2013 17:45:10 GMT sacerdot [2707]
	* src/ASM/Assembly.ma (modified)

	Assembly repaired.


Fri, 22 Feb 2013 17:23:45 GMT mckinna [2706]
	* src/Clight/switchRemoval.ma (modified)

	repaired contentious broken automation
	at end of subgoal 9 of case ...


Fri, 22 Feb 2013 16:56:31 GMT sacerdot [2705]
	* src/ASM/ASM.ma (modified)
	* src/ASM/AbstractStatus.ma (modified)
	* src/ASM/Assembly.ma (modified)
	* src/ASM/Interpret.ma (modified)
	* src/BACKEND_BROKEN_FILES (modified)
	* src/compiler.ma (modified)

	More progress in ASM towards implementing the new pseudoinstructions.


Fri, 22 Feb 2013 14:53:48 GMT tranquil [2704]
	* src/ASM/ASM.ma (modified)

	moved JMP from instructions to preinstructions, and added ...


Fri, 22 Feb 2013 14:31:50 GMT mckinna [2703]
	* src/common/CostLabel.ma (modified)

	now includes defn of costlabel_map


Fri, 22 Feb 2013 14:27:16 GMT sacerdot [2702]
	* src/ASM/UtilBranch.ma (modified)
	* src/compiler.ma (modified)
	* src/joint/linearise.ma (modified)

	1. proof closed in ASM/UtilBranch
	2. more passes integrated in the ...


Fri, 22 Feb 2013 13:30:43 GMT sacerdot [2701]
	* src/Clight/switchRemoval.ma (modified)

	Automation failure fixed by replacing with hand made proof.


Fri, 22 Feb 2013 13:12:24 GMT sacerdot [2700]
	* src/ASM/Arithmetic.ma (modified)
	* src/ASM/Policy.ma (modified)
	* src/ASM/Util.ma (modified)
	* src/ERTLptr/ERTLptrToLTL.ma (modified)
	* src/ERTLptr/Interference.ma (modified)
	* src/ERTLptr/liveness.ma (modified)
	* src/compiler.ma (modified)
	* src/utilities/fixpoints.ma (modified)

	1. exponential function dropped in favour of standard library
	2. ...


Fri, 22 Feb 2013 13:11:48 GMT mckinna [2699]
	* src/Clight/switchRemoval.ma (modified)

	simplified dependencies somewhat


Fri, 22 Feb 2013 12:11:50 GMT mckinna [2698]
	* src/Clight/memoryInjections.ma (modified)

	simplified dependencies


Fri, 22 Feb 2013 11:13:51 GMT sacerdot [2697]
	* src/ERTLptr/ERTLptrToLTL.ma (modified)
	* src/compiler.ma (modified)

	Compiler fixed to include the ERTLptrToLTL pass.


Fri, 22 Feb 2013 11:12:25 GMT sacerdot [2696]
	* src/ERTL/ERTLToERTLptr.ma (moved)

	I can't get this right... :-(


Fri, 22 Feb 2013 11:06:14 GMT sacerdot [2695]
	* src/ERTL/ERTLToERLptr.ma (moved)

	Renamed again.


Fri, 22 Feb 2013 10:53:32 GMT tranquil [2694]
	* src/ERTLptr/ERTLptrToLTL.ma (modified)

	completed ERTLptrToLTL


Fri, 22 Feb 2013 10:39:03 GMT sacerdot [2693]
	* src/BACKEND_BROKEN_FILES (modified)
	* src/ERTLptr/ERTLptrToLTL.ma (moved)
	* src/ERTLptr/Interference.ma (moved)
	* src/ERTLptr/liveness.ma (moved)
	* src/compiler.ma (modified)

	1. Stuff moved to correct places.
	2. ERTLptr pass added


Fri, 22 Feb 2013 10:27:15 GMT garnier [2692]
	* src/Clight/toCminorCorrectnessExpr.ma (modified)

	Add some more constraints in clight_cminor_data.


Fri, 22 Feb 2013 10:10:49 GMT sacerdot [2691]
	* src/ERTL/ERTLtoERTLptr.ma (moved)
	* src/ERTL/ERTLtoERTLptrOK.ma (moved)

	ERTLtoERTLptr* moved to the proper place


Thu, 21 Feb 2013 18:24:11 GMT campbell [2690]
	* src/common/FEMeasurable.ma (modified)

	Most of the measurable subtrace preservation proof done.


Thu, 21 Feb 2013 18:23:17 GMT tranquil [2689]
	* src/ERTL/ERTLToLTL.ma (modified)
	* src/ERTL/liveness.ma (modified)
	* src/RTL/RTLToERTL.ma (modified)
	* src/RTLabs/RTLabsToRTL.ma (modified)

	* fixed passes up to linearisation


Thu, 21 Feb 2013 17:03:46 GMT tranquil [2688]
	* src/ASM/Arithmetic.ma (modified)
	* src/ERTLptr/ERTLtoERTLptr.ma (modified)
	* src/joint/Joint.ma (modified)
	* src/joint/Traces.ma (modified)
	* src/joint/TranslateUtils.ma (modified)
	* src/joint/joint_semantics.ma (modified)
	* src/joint/semanticsUtils.ma (modified)
	* src/joint/semantics_blocks.ma (modified)

	* in Arithmeticcs.ma: commented include that breaks script in latest ...


Thu, 21 Feb 2013 15:20:19 GMT tranquil [2687]
	* src/joint/semanticsUtils.ma (modified)

	* polished some interfaces


Thu, 21 Feb 2013 14:34:29 GMT mckinna [2686]
	* src/Clight/toCminor.ma (modified)

	two minor modifications to assist disambiguation of "lookup"

	file ...


Thu, 21 Feb 2013 10:38:36 GMT campbell [2685]
	* src/common/FEMeasurable.ma (modified)
	* src/common/Measurable.ma (modified)
	* src/common/SmallstepExec.ma (modified)

	Progress on measurable trace preservation: prefix preserves ...


Thu, 21 Feb 2013 09:32:17 GMT sacerdot [2684]
	* src/ASM/Arithmetic.ma (modified)

	...


Wed, 20 Feb 2013 17:41:46 GMT tranquil [2683]
	* src/joint/semanticsUtils.ma (modified)

	proof of properties of b_graph_program_transform (with an open axiom)


Tue, 19 Feb 2013 18:24:20 GMT campbell [2682]
	* src/Clight/labelSimulation.ma (modified)
	* src/common/Executions.ma (modified)
	* src/common/SmallstepExec.ma (modified)

	Don't apply inv in after_n_steps to last state.


Tue, 19 Feb 2013 17:48:32 GMT tranquil [2681]
	* src/ERTL/ERTLToLTL.ma (modified)
	* src/ERTL/liveness.ma (modified)
	* src/ERTLptr/ERTLtoERTLptr.ma (modified)
	* src/RTL/RTL.ma (modified)
	* src/RTL/RTLToERTL.ma (modified)
	* src/joint/Joint.ma (modified)
	* src/joint/Traces.ma (modified)
	* src/joint/TranslateUtils.ma (modified)
	* src/joint/semanticsUtils.ma (modified)

	* improvements to the graph translation function
	* fixed passes up to LTL


Tue, 19 Feb 2013 15:36:52 GMT mckinna [2680]
	* src/Clight/switchRemoval.ma (modified)

	proofs which previously succeeded fail, thanks to fold on ...


Tue, 19 Feb 2013 14:15:41 GMT mckinna [2679]
	* src/ASM/ASMCosts.ma (modified)

	Further tweak to Brian's changes: no normalization reqd at all!


Tue, 19 Feb 2013 11:23:52 GMT campbell [2678]
	* etc/campbell/dev-notes/2013-02-19-single-source-step-simulations.txt (added)
	* src/common/FEMeasurable.ma (modified)

	Switch to single source step simulations for front-end measurable ...


Tue, 19 Feb 2013 11:23:50 GMT campbell [2677]
	* src/Clight/Cexec.ma (modified)
	* src/Clight/CexecComplete.ma (modified)
	* src/Clight/CexecEquiv.ma (modified)
	* src/Clight/CexecSound.ma (modified)
	* src/Clight/Clight_abstract.ma (modified)
	* src/Clight/Csem.ma (modified)
	* src/Clight/SimplifyCasts.ma (modified)
	* src/Clight/labelSimulation.ma (modified)
	* src/Clight/switchRemoval.ma (modified)
	* src/Cminor/Cminor_abstract.ma (modified)
	* src/Cminor/Cminor_semantics.ma (modified)
	* src/RTLabs/RTLabs_abstract.ma (modified)
	* src/RTLabs/RTLabs_semantics.ma (modified)
	* src/RTLabs/RTLabs_traces.ma (modified)
	* src/correctness.ma (modified)

	Retain the pointer for the function called in front-end call states ...


Tue, 19 Feb 2013 11:23:49 GMT campbell [2676]
	* src/ASM/ASMCosts.ma (modified)

	Less aggressive normalisation in ASMCosts to prevent memory blowup.


Mon, 18 Feb 2013 17:26:22 GMT tranquil [2675]
	* src/ERTLptr/ERTLtoERTLptr.ma (modified)
	* src/joint/TranslateUtils.ma (modified)
	* src/joint/semanticsUtils.ma (modified)

	* a generic graph program transformation


Mon, 18 Feb 2013 16:48:19 GMT tranquil [2674]
	* src/ERTL/ERTL_semantics.ma (modified)
	* src/ERTLptr/ERTLptr.ma (modified)
	* src/ERTLptr/ERTLtoERTLptr.ma (modified)
	* src/RTLabs/RTLabsToRTL.ma (modified)
	* src/joint/TranslateUtils.ma (modified)
	* src/joint/blocks.ma (modified)
	* src/joint/semanticsUtils.ma (modified)
	* src/joint/semantics_blocks.ma (modified)

	* another change in block definition
	* RTLabs -> RTL and ERTL -> ...


Mon, 18 Feb 2013 12:18:02 GMT tranquil [2673]
	* src/ASM/Arithmetic.ma (modified)
	* src/ASM/Util.ma (modified)
	* src/common/PositiveMap.ma (modified)

	corrected some compilation errors (that might depend on some matita ...


Sat, 16 Feb 2013 17:49:13 GMT sacerdot [2672]
	* src/ASM/ASMCosts.ma (modified)
	* src/ASM/Arithmetic.ma (modified)

	One less axiom on bitvectors.


Sat, 16 Feb 2013 16:12:02 GMT sacerdot [2671]
	* src/ASM/CostsProof.ma (modified)

	simplification


Fri, 15 Feb 2013 10:27:59 GMT campbell [2670]
	* src/common/FEMeasurable.ma (modified)
	* src/common/Measurable.ma (modified)
	* src/utilities/extranat.ma (modified)

	Clean up from recent commits.


Fri, 15 Feb 2013 10:27:58 GMT campbell [2669]
	* src/common/FEMeasurable.ma (modified)
	* src/common/Measurable.ma (modified)
	* src/common/SmallstepExec.ma (modified)

	Tweak exec_steps output; show that simulations extend to measurable ...


Fri, 15 Feb 2013 10:27:56 GMT campbell [2668]
	* src/Clight/test/trivial.test.ma (modified)
	* src/common/ErrorMessages.ma (modified)
	* src/common/FEMeasurable.ma (modified)
	* src/common/Measurable.ma (modified)
	* src/common/SmallstepExec.ma (modified)

	Intermediate measurable proof check-in before I change its traces
	again.


Thu, 14 Feb 2013 18:10:23 GMT garnier [2667]
	* src/Clight/Clight_abstract.ma (modified)
	* src/Clight/toCminorCorrectness.ma (modified)
	* src/Clight/toCminorCorrectnessExpr.ma (modified)

	Clight to Cminor, statements: some cases down. Subset of the ...


Thu, 14 Feb 2013 10:49:48 GMT piccolo [2666]
	* src/ERTL/ERTL_semantics.ma (modified)
	* src/ERTLptr/ERTLptr_semantics.ma (modified)
	* src/ERTLptr/ERTLtoERTLptrOK.ma (modified)
	* src/joint/blocks.ma (modified)

	bug fixed in blocks.ma


Thu, 14 Feb 2013 09:01:35 GMT sacerdot [2665]
	* src/ASM/ASMCostsSplit.ma (modified)

	...


Wed, 13 Feb 2013 23:01:13 GMT sacerdot [2664]
	* src/ASM/ASMCosts.ma (modified)

	Tailcall case implemented (it does not happen ATM).


Tue, 12 Feb 2013 18:40:11 GMT piccolo [2663]
	* src/ERTLptr/ERTLtoERTLptrOK.ma (modified)

	some minor modifications to ERTLtoERTLptr


Tue, 12 Feb 2013 17:56:41 GMT piccolo [2662]
	* src/ERTLptr/ERTLtoERTLptrOK.ma (modified)

	Towards a very generalized lemma that summarizes all of Paolo's
	results.


Tue, 12 Feb 2013 02:26:37 GMT sacerdot [2661]
	* src/BACKEND_BROKEN_FILES (modified)
	* src/joint/stacksize.ma (modified)

	stacksize "repaired" by "considering" tailcalls
	Some daemons added ...


Tue, 12 Feb 2013 02:06:22 GMT sacerdot [2660]
	* src/BACKEND_BROKEN_FILES (modified)

	...


Tue, 12 Feb 2013 01:47:18 GMT sacerdot [2659]
	* src/BACKEND_BROKEN_FILES (modified)
	* src/RTL/RTLTailcall.ma (deleted)
	* src/RTL/RTLToERTL.ma (modified)

	Tailcall elimination no longer necessary:
	 1. the back-end is almost ...


Tue, 12 Feb 2013 01:43:21 GMT sacerdot [2658]
	* src/BACKEND_BROKEN_FILES (modified)

	...


Tue, 12 Feb 2013 01:41:22 GMT sacerdot [2657]
	* src/ASM/ASMCostsSplit.ma (modified)
	* src/ASM/CostsProof.ma (modified)

	Cost proof fully repaired. It was broken by the definitions used in ...


Mon, 11 Feb 2013 17:58:13 GMT sacerdot [2656]
	* src/ASM/ASMCosts.ma (modified)
	* src/ASM/CostsProof.ma (modified)
	* src/BACKEND_BROKEN_FILES (modified)

	Ported to tailcalls (currently nothing is classified as a tailcall).


Mon, 11 Feb 2013 15:52:37 GMT tranquil [2655]
	* src/joint/Joint.ma (modified)
	* src/joint/joint_semantics.ma (modified)
	* src/joint/semantics_blocks.ma (modified)

	new step in code semantic lemma


Fri, 08 Feb 2013 19:54:32 GMT garnier [2654]
	* src/Clight/memoryInjections.ma (modified)

	Memory injections in a coherent state.


Fri, 08 Feb 2013 12:45:22 GMT sacerdot [2653]
	* src/ASM/Policy.ma (modified)
	* src/ASM/PolicyFront.ma (modified)

	...


Fri, 08 Feb 2013 10:49:55 GMT sacerdot [2652]
	* src/ASM/Policy.ma (modified)
	* src/ASM/PolicyFront.ma (modified)
	* src/ASM/PolicyStep.ma (modified)

	String type changed definition.


Fri, 08 Feb 2013 10:13:07 GMT sacerdot [2651]
	* src/ASM/Assembly.ma (modified)

	Type String changed.


Thu, 07 Feb 2013 21:10:51 GMT sacerdot [2647]
	* src/ASM/ASM.ma (modified)
	* src/joint/String.ma (modified)

	Stupid typo fixed.


Thu, 07 Feb 2013 20:44:29 GMT sacerdot [2646]
	* src/common/ErrorMessages.ma (modified)
	* src/common/PreIdentifiers.ma (modified)

	A tag was classified as an error message. Fixed.


Thu, 07 Feb 2013 20:22:22 GMT sacerdot [2645]
	* src/ASM/ASM.ma (modified)
	* src/ASM/BitVector.ma (modified)
	* src/ASM/Char.ma (deleted)
	* src/ASM/I8051.ma (modified)
	* src/BACKEND_BROKEN_FILES (added)
	* src/Clight/Cexec.ma (modified)
	* src/Clight/Csyntax.ma (modified)
	* src/Clight/TypeComparison.ma (modified)
	* src/Clight/test/addptrcharboth.test.ma (modified)
	* src/Clight/test/badconditional.test.ma (modified)
	* src/Clight/test/controlflow.test.ma (modified)
	* src/Clight/test/endptr.test.ma (modified)
	* src/Clight/test/endptr2.test.ma (modified)
	* src/Clight/test/forcont.test.ma (modified)
	* src/Clight/test/goto-if.test.ma (modified)
	* src/Clight/test/implicit.test.ma (modified)
	* src/Clight/test/implicitcond.test.ma (modified)
	* src/Clight/test/sum.test.ma (modified)
	* src/Clight/test/trivial.test.ma (modified)
	* src/Clight/toCminor.ma (modified)
	* src/Cminor/Cminor_semantics.ma (modified)
	* src/Cminor/Cminor_syntax.ma (modified)
	* src/ERTL/ERTL.ma (modified)
	* src/ERTLptr/ERTLptr.ma (modified)
	* src/ERTLptr/ERTLtoERTLptrOK.ma (modified)
	* src/LIN/joint_LTL_LIN.ma (modified)
	* src/LIN/joint_LTL_LIN_semantics.ma (modified)
	* src/RTL/RTL_semantics.ma (modified)
	* src/RTLabs/RTLabs_semantics.ma (modified)
	* src/RTLabs/import.ma (modified)
	* src/common/AST.ma (modified)
	* src/common/Animation.ma (modified)
	* src/common/BackEndOps.ma (modified)
	* src/common/ByteValues.ma (modified)
	* src/common/CostLabel.ma (modified)
	* src/common/ErrorMessages.ma (added)
	* src/common/Errors.ma (modified)
	* src/common/Globalenvs.ma (modified)
	* src/common/Graphs.ma (modified)
	* src/common/IO.ma (modified)
	* src/common/Identifiers.ma (modified)
	* src/common/PreIdentifiers.ma (modified)
	* src/common/Registers.ma (modified)
	* src/common/Values.ma (modified)
	* src/compiler.ma (modified)
	* src/joint/Joint.ma (modified)
	* src/joint/String.ma (moved)
	* src/joint/Traces.ma (modified)
	* src/joint/joint_semantics.ma (modified)
	* src/joint/semanticsUtils.ma (modified)

	1. some broken back-end files repaires, several still to go
	2. the ...


Thu, 07 Feb 2013 15:42:54 GMT campbell [2644]
	* src/common/FEMeasurable.ma (modified)

	Commit some work on FEMeasurable before trying to do something nicer ...


Thu, 07 Feb 2013 15:03:37 GMT sacerdot [2643]
	* src/ASM/Erase.ma (deleted)

	We are not proving erasure, so this is dead code.


Thu, 07 Feb 2013 14:24:50 GMT piccolo [2642]
	* src/joint/Traces.ma (modified)

	fixed joint/Traces after having posed block 0 to be Code


Thu, 07 Feb 2013 14:15:56 GMT piccolo [2641]
	* src/common/Pointers.ma (modified)
	* src/joint/joint_semantics.ma (modified)

	defined dummy block code equals to 0


Thu, 07 Feb 2013 14:13:41 GMT tranquil [2640]
	* src/RTL/RTL.ma (modified)
	* src/RTLabs/RTLabsToRTL.ma (modified)

	updated RTL and RTLabs to RTL translation


Thu, 07 Feb 2013 14:07:14 GMT sacerdot [2639]
	* src/joint/Erasure.ma (deleted)

	We are not going to prove erasure. Thus this becomes dead code.


Thu, 07 Feb 2013 13:15:51 GMT piccolo [2638]
	* src/ERTLptr/ERTLtoERTLptrOK.ma (modified)
	* src/joint/Traces.ma (modified)
	* src/joint/joint_semantics.ma (modified)

	Back-end fixes for last Garnier's commit that removes the regions ...


Wed, 06 Feb 2013 17:39:21 GMT campbell [2624]
	* src/Cminor/initialisation.ma (modified)
	* src/common/AST.ma (modified)
	* src/common/Floats.ma (deleted)
	* src/common/Globalenvs.ma (modified)

	Properly evict unused and axiomatised Floats.


Wed, 06 Feb 2013 17:39:19 GMT campbell [2623]
	* src/correctness.ma (modified)

	Name change update.


Wed, 06 Feb 2013 16:03:19 GMT campbell [2619]
	* src/Clight/test/addptrcharboth.test.ma (modified)
	* src/Clight/test/badconditional.test.ma (modified)
	* src/Clight/test/controlflow.test.ma (modified)
	* src/Clight/test/endptr.test.ma (modified)
	* src/Clight/test/endptr2.test.ma (modified)
	* src/Clight/test/forcont.test.ma (modified)
	* src/Clight/test/goto-if.test.ma (modified)
	* src/Clight/test/implicit.test.ma (modified)
	* src/Clight/test/implicitcond.test.ma (modified)
	* src/Clight/test/search.test.ma (modified)
	* src/Clight/test/sum.test.ma (modified)
	* src/Clight/test/trivial.test.ma (modified)

	Update some test cases.


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, ...