#
# ChangeLog for src/joint/Joint.ma
#
# Generated by Trac 1.2
# Jan 22, 2021, 7:46:30 PM

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


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


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


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


Wed, 30 Jan 2013 18:25:39 GMT tranquil [2595]
	* src/joint/Joint.ma (modified)
	* src/joint/TranslateUtils.ma (modified)
	* src/joint/blocks.ma (modified)
	* src/joint/semantics.ma (modified)
	* src/joint/semantics_blocks.ma (modified)

	* dropped locals and exit from definition of joint_if_function
	* new ...


Wed, 19 Dec 2012 09:38:43 GMT piccolo [2562]
	* src/joint/Joint.ma (modified)
	* src/joint/Traces.ma (modified)
	* src/joint/linearise.ma (modified)
	* src/joint/semantics.ma (modified)

	linearise modified


Tue, 18 Dec 2012 16:03:29 GMT tranquil [2561]
	* src/joint/Joint.ma (modified)
	* src/joint/Traces.ma (modified)
	* src/joint/semantics.ma (modified)

	* moved CALL as different case than joint_seq: lots of broken code ...


Fri, 07 Dec 2012 19:37:51 GMT tranquil [2547]
	* src/joint/Joint.ma (modified)
	* src/joint/linearise.ma (modified)
	* src/joint/lineariseProof.ma (modified)

	going on in proof of linearise
	simplified by use of monadic ...


Thu, 06 Dec 2012 12:24:29 GMT tranquil [2537]
	* src/LIN/joint_LTL_LIN.ma (modified)
	* src/joint/Joint.ma (modified)
	* src/joint/semantics.ma (modified)

	rolled back changes on calls in joint. Now the save_frame parameter ...


Wed, 05 Dec 2012 17:57:16 GMT tranquil [2532]
	* src/joint/Joint.ma (modified)
	* src/joint/TranslateUtils.ma (modified)
	* src/joint/linearise.ma (modified)
	* src/joint/semantics.ma (modified)

	added FCOND in LIN, and rewritten linearise so that it never adds a ...


Sun, 25 Nov 2012 12:33:09 GMT tranquil [2490]
	* src/ERTL/ERTL.ma (modified)
	* src/ERTL/ERTLToLTL.ma (modified)
	* src/ERTL/liveness.ma (modified)
	* src/LIN/LINToASM.ma (modified)
	* src/LIN/joint_LTL_LIN.ma (modified)
	* src/LTL/LTLToLIN.ma (modified)
	* src/RTL/RTL.ma (modified)
	* src/RTL/RTLTailcall.ma (modified)
	* src/RTL/RTLToERTL.ma (modified)
	* src/RTLabs/RTLabsToRTL.ma (modified)
	* src/joint/Joint.ma (modified)

	switched back to Byte immediate (instead of beval ones)
	propagated ...


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


Tue, 06 Nov 2012 16:00:01 GMT tranquil [2437]
	* src/joint/BEMem.ma (modified)
	* src/joint/Joint.ma (modified)
	* src/joint/semantics.ma (modified)

	generalised calls to calls with pointers


Tue, 30 Oct 2012 15:23:09 GMT tranquil [2422]
	* src/joint/Joint.ma (modified)
	* src/joint/SemanticUtils.ma (modified)
	* src/joint/Traces.ma (modified)
	* src/joint/blocks.ma (modified)
	* src/joint/linearise.ma (modified)
	* src/joint/semantics.ma (modified)
	* src/joint/semantics_blocks.ma (modified)

	adapted joint to cl_call f


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


Tue, 13 Dec 2011 13:49:52 GMT sacerdot [1601]
	* src/ERTL/ERTLToLTL.ma (modified)
	* src/LIN/LIN.ma (modified)
	* src/LIN/semantics.ma (modified)
	* src/RTL/RTLToERTL.ma (modified)
	* src/RTLabs/RTLabsToRTL.ma (modified)
	* src/RTLabs/Traces.ma (modified)
	* src/RTLabs/semantics.ma (modified)
	* src/common/Errors.ma (modified)
	* src/common/IOMonad.ma (modified)
	* src/common/Identifiers.ma (modified)
	* src/common/PositiveMap.ma (modified)
	* src/common/StructuredTraces.ma (modified)
	* src/joint/BEValues.ma (modified)
	* src/joint/Joint.ma (modified)
	* src/joint/semantics.ma (modified)

	Files ported to new version of the standard library.


Fri, 28 Oct 2011 13:05:07 GMT mulligan [1471]
	* src/joint/Joint.ma (modified)
	* src/joint/ProofUtils.ma (modified)

	finished erasure and generalised so as to work on arbitrary joint ...


Fri, 14 Oct 2011 20:25:03 GMT sacerdot [1380]
	* src/LIN/joint_LTL_LIN_semantics.ma (added)
	* src/LIN/semantics.ma (modified)
	* src/LTL/semantics.ma (modified)
	* src/joint/Joint.ma (modified)

	LTL and LIN semantics factorized out in joint_LTL_LIN_semantics.ma. ...


Wed, 28 Sep 2011 21:50:32 GMT sacerdot [1282]
	* src/ERTL/ERTLToLTL.ma (modified)
	* src/ERTL/Interference.ma (modified)
	* src/ERTL/build.ma (deleted)
	* src/ERTL/liveness.ma (modified)
	* src/LIN/LINToASM.ma (modified)
	* src/LTL/LTLToLIN.ma (modified)
	* src/RTL/RTLTailcall.ma (modified)
	* src/RTL/RTLtoERTL.ma (modified)
	* src/RTLabs/RTLAbstoRTL.ma (modified)
	* src/joint/Joint.ma (modified)
	* src/joint/TranslateUtils.ma (modified)

	Cosmetic change: names of joint statements/instructions shortened and ...


Wed, 28 Sep 2011 00:43:37 GMT sacerdot [1280]
	* src/ERTL/ERTL.ma (modified)
	* src/LTL/LTL.ma (modified)
	* src/RTL/RTL.ma (modified)
	* src/RTL/RTLtoERTL.ma (modified)
	* src/RTLabs/RTLAbstoRTL.ma (modified)
	* src/joint/Joint.ma (modified)
	* src/joint/TranslateUtils.ma (added)

	Some progress in the porting of RTLAbstoRTL to the joint syntax:

	1) ...


Mon, 26 Sep 2011 16:07:47 GMT sacerdot [1275]
	* src/ERTL/ERTLToLTL.ma (modified)
	* src/ERTL/liveness.ma (modified)
	* src/ERTL/uses.ma (deleted)
	* src/LIN/LINToASM.ma (modified)
	* src/RTL/RTL.ma (modified)
	* src/RTL/RTLTailcall.ma (modified)
	* src/RTL/RTLtoERTL.ma (modified)
	* src/joint/Joint.ma (modified)

	RTL ported to joint syntax, but:

	1. bug discovered: opaccs should ...


Mon, 26 Sep 2011 14:24:32 GMT mulligan [1271]
	* src/ERTL/ERTLToLTL.ma (modified)
	* src/ERTL/liveness.ma (modified)
	* src/ERTL/uses.ma (modified)
	* src/LTL/LTL.ma (modified)
	* src/joint/Joint.ma (modified)

	finished, kind of


Mon, 26 Sep 2011 13:59:28 GMT sacerdot [1270]
	* src/ERTL/ERTL.ma (modified)
	* src/LIN/LIN.ma (modified)
	* src/LIN/LINToASM.ma (modified)
	* src/LTL/LTL.ma (modified)
	* src/RTL/RTL.ma (modified)
	* src/RTL/RTLTailcall.ma (modified)
	* src/RTL/RTLtoERTL.ma (modified)
	* src/joint/Joint.ma (modified)

	Making RTL syntax an instance of Joint.


Fri, 23 Sep 2011 13:04:20 GMT mulligan [1260]
	* src/ERTL/ERTLToLTL.ma (modified)
	* src/ERTL/liveness.ma (modified)
	* src/ERTL/uses.ma (modified)
	* src/joint/Joint.ma (modified)
	* src/utilities/extralib.ma (modified)
	* src/utilities/sigma.ma (added)

	commit for csc


Thu, 22 Sep 2011 14:23:05 GMT sacerdot [1255]
	* src/joint/Joint.ma (modified)

	Major mistake fixed: op1 and op2 were assuming the source and dest ...


Thu, 22 Sep 2011 14:16:06 GMT sacerdot [1254]
	* src/ERTL/ERTL.ma (modified)
	* src/RTL/RTLtoERTL.ma (modified)
	* src/joint/Joint.ma (modified)

	More progress towards porting of RTLtoERTL to joint syntax.


Thu, 22 Sep 2011 12:49:18 GMT sacerdot [1252]
	* src/ERTL/ERTL.ma (modified)
	* src/LTL/LTL.ma (modified)
	* src/RTL/RTLtoERTL.ma (modified)
	* src/joint/Joint.ma (modified)

	graph_params added to joint/Joint.ma, together with useful common ...


Thu, 22 Sep 2011 10:02:35 GMT sacerdot [1250]
	* src/ERTL/ERTLToLTL.ma (modified)
	* src/ERTL/liveness.ma (modified)
	* src/ERTL/uses.ma (modified)
	* src/LIN/LIN.ma (modified)
	* src/LTL/LTLToLIN.ma (modified)
	* src/RTL/RTLtoERTL.ma (modified)
	* src/joint/Joint.ma (modified)
	* src/joint/semantics.ma (modified)
	* src/utilities/extralib.ma (modified)

	1. Sigma types projections moved to utilities/extralib.ma
	2. ...


Thu, 22 Sep 2011 00:50:44 GMT sacerdot [1246]
	* src/LIN/LIN.ma (modified)
	* src/LTL/LTL.ma (modified)
	* src/LTL/LTLToLIN.ma (modified)
	* src/joint/Joint.ma (modified)
	* src/joint/semantics.ma (modified)

	Yet another change to Joint.ma to accomodate all passes.
	The ...


Wed, 21 Sep 2011 20:22:13 GMT sacerdot [1245]
	* src/LIN/LINToASM.ma (modified)
	* src/RTL/RTLtoERTL.ma (modified)
	* src/joint/Joint.ma (modified)

	RTLtoERTL and LINToASM: porting to new Joint data type in progress. ...


Wed, 21 Sep 2011 13:56:54 GMT sacerdot [1236]
	* src/LIN/LIN.ma (modified)
	* src/LTL/LTLToLIN.ma (modified)
	* src/joint/Joint.ma (modified)

	LTLToLin.ma completed (up to a couple of daemons used to provide dead ...


Wed, 21 Sep 2011 09:57:20 GMT sacerdot [1233]
	* src/LIN/LIN.ma (modified)
	* src/LTL/LTL.ma (modified)
	* src/LTL/LTLToLIN.ma (modified)
	* src/RTL/semantics.ma (modified)
	* src/common/SmallstepExec.ma (modified)
	* src/joint/Joint.ma (modified)
	* src/joint/semantics.ma (modified)

	1) Ported to Brian's new dependent type for fullexec
	2) Universe ...


Mon, 19 Sep 2011 14:52:40 GMT mulligan [1228]
	* src/ERTL/build.ma (modified)
	* src/joint/Joint.ma (modified)

	some more changes


Thu, 15 Sep 2011 16:05:31 GMT sacerdot [1220]
	* src/ERTL/ERTL.ma (modified)
	* src/joint/Joint.ma (modified)
	* src/joint/semantics.ma (modified)

	ERTL ported to the new joint syntax.


Mon, 05 Sep 2011 11:23:20 GMT mulligan [1182]
	* src/joint/Joint.ma (modified)
	* src/joint/semantics.ma (modified)

	changes to semantics: removing parameterised "next" element in joint ...


Sat, 03 Sep 2011 02:17:48 GMT sacerdot [1176]
	* src/joint/Joint.ma (modified)
	* src/joint/semantics.ma (modified)

	...


Fri, 02 Sep 2011 12:51:20 GMT mulligan [1171]
	* src/ERTL/ERTL.ma (modified)
	* src/ERTL/ERTLToLTL.ma (modified)
	* src/LIN/LIN.ma (modified)
	* src/LTL/LTL.ma (modified)
	* src/LTL/LTLToLIN.ma (modified)
	* src/joint/Joint.ma (modified)

	changes made on claudio's request: changed order of nesting in the ...


Fri, 02 Sep 2011 09:57:45 GMT sacerdot [1169]
	* src/joint/Joint.ma (modified)

	JointRTLtoLIN moved to Joint


Fri, 02 Sep 2011 08:35:54 GMT mulligan [1167]
	* src/LIN/LIN.ma (modified)
	* src/joint/Joint.ma (moved)

	...


Fri, 02 Sep 2011 08:35:24 GMT mulligan [1166]
	* src/ERTL/ERTLToLTL.ma (modified)
	* src/LIN/LIN.ma (modified)
	* src/LTL/LTL.ma (modified)
	* src/LTL/LTLToLIN.ma (modified)
	* src/joint (added)
	* src/joint/JointLTLLIN.ma (moved)

	moved joint ltl lin files into their own directory.  more changes to ...