#
# ChangeLog for src/Cminor/syntax.ma
#
# Generated by Trac 1.2
# Apr 21, 2021, 5:32:50 PM

Tue, 24 Jul 2012 17:40:21 GMT campbell [2252]
	* src/Clight/toCminor.ma (modified)
	* src/Cminor/initialisation.ma (modified)
	* src/Cminor/syntax.ma (modified)
	* src/Cminor/toRTLabs.ma (modified)

	Use the return statement invariant.  Restructure the invariants for ...


Tue, 24 Jul 2012 17:40:21 GMT campbell [2251]
	* 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)

	Add new invariant to Cminor that return typs should be respected.


Tue, 24 Jul 2012 17:40:13 GMT campbell [2249]
	* src/Clight/toCminor.ma (modified)
	* src/Cminor/initialisation.ma (modified)
	* src/Cminor/syntax.ma (modified)

	Tweak Cminor invariant to be slightly more readable/extendable.


Mon, 23 Jul 2012 12:05:10 GMT campbell [2232]
	* 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)

	Remove unused block structure in Cminor.


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


Wed, 04 Apr 2012 16:48:27 GMT campbell [1878]
	* 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/RTLabs/semantics.ma (modified)
	* src/RTLabs/syntax.ma (modified)
	* src/common/FrontEndOps.ma (modified)

	Enforce typing of constants in front-end, plus binops for RTLabs.


Wed, 04 Apr 2012 16:48:23 GMT campbell [1872]
	* src/Clight/ClassifyOp.ma (added)
	* src/Clight/Csem.ma (modified)
	* src/Clight/Csyntax.ma (modified)
	* src/Clight/SimplifyCasts.ma (modified)
	* src/Clight/TypeComparison.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/RTLabs/semantics.ma (modified)
	* src/RTLabs/syntax.ma (modified)
	* src/common/AST.ma (modified)
	* src/common/FrontEndOps.ma (modified)
	* src/common/Globalenvs.ma (modified)
	* src/common/Mem.ma (modified)
	* src/common/Values.ma (modified)

	Make binary operations in Cminor/RTLabs properly typed.
	A few extra ...


Thu, 09 Feb 2012 12:22:28 GMT campbell [1680]
	* src/Cminor/semantics.ma (modified)
	* src/Cminor/syntax.ma (modified)
	* src/Cminor/toRTLabs.ma (modified)
	* src/RTLabs/semantics.ma (modified)
	* src/RTLabs/syntax.ma (modified)

	Comment out unused tailcalls in Cminor and RTLabs.
	(They would be a ...


Mon, 19 Dec 2011 13:48:37 GMT campbell [1631]
	* src/Clight/toCminor.ma (modified)
	* src/Cminor/initialisation.ma (modified)
	* src/Cminor/syntax.ma (modified)
	* src/Cminor/toRTLabs.ma (modified)
	* src/common/Identifiers.ma (modified)
	* src/utilities/lists.ma (modified)

	Use fact that type environments in Cminor have distinct variables to ...


Mon, 19 Dec 2011 13:48:33 GMT campbell [1626]
	* 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/RTLabs/syntax.ma (modified)
	* src/common/Errors.ma (modified)
	* src/utilities/lists.ma (added)

	Add extra type safety in front end.  NB: critical freshness parts ...


Wed, 14 Dec 2011 12:18:30 GMT sacerdot [1605]
	* src/Clight/CexecEquiv.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)

	Porting to last standard library of Matita.


Tue, 13 Dec 2011 16:37:40 GMT sacerdot [1603]
	* src/Clight/Cexec.ma (modified)
	* src/Clight/CexecComplete.ma (modified)
	* src/Cminor/semantics.ma (modified)
	* src/Cminor/syntax.ma (modified)
	* src/Cminor/toRTLabs.ma (modified)

	More proofs ported to new lib.


Fri, 14 Oct 2011 08:56:45 GMT campbell [1369]
	* 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/RTLabs/semantics.ma (modified)
	* src/RTLabs/syntax.ma (modified)
	* src/common/FrontEndOps.ma (modified)
	* src/common/Values.ma (modified)

	Put type information into front-end unary ops.
	Slight change to ...


Fri, 07 Oct 2011 10:26:39 GMT campbell [1316]
	* src (modified)
	* src/ASM (modified)
	* src/ASM/BitVectorTrie.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/RTLabs/syntax.ma (modified)
	* src/common/Errors.ma (modified)
	* src/common/Identifiers.ma (modified)
	* src/utilities/deppair.ma (copied)
	* src/utilities/extralib.ma (modified)
	* src/utilities/lists.ma (modified)
	* src/utilities/option.ma (modified)
	* src/utilities/pair.ma (copied)

	Merge in id-lookup-branch to trunk.


Fri, 16 Sep 2011 16:39:05 GMT sacerdot [1224]
	* src/Clight/CexecSound.ma (modified)
	* src/Clight/Csyntax.ma (modified)
	* src/Clight/SimplifyCasts.ma (modified)
	* src/Clight/label.ma (modified)
	* src/Clight/test/search.c.ma (modified)
	* src/Clight/toCminor.ma (modified)
	* src/Cminor/initialisation.ma (modified)
	* src/Cminor/syntax.ma (modified)
	* src/Cminor/toRTLabs.ma (modified)
	* src/LIN/LIN.ma (modified)
	* src/LTL/LTLToLIN.ma (modified)
	* src/RTLabs/RTLAbstoRTL.ma (modified)
	* src/RTLabs/syntax.ma (modified)
	* src/common/AST.ma (modified)
	* src/common/Globalenvs.ma (modified)
	* src/common/IntValue.ma (deleted)

	Type of programs in common/AST made more dependent.
	In particular, ...


Tue, 30 Aug 2011 14:09:20 GMT campbell [1147]
	* src/Clight/Cexec.ma (modified)
	* src/Clight/Csem.ma (modified)
	* src/Cminor/syntax.ma (modified)
	* src/RTLabs/syntax.ma (modified)

	Remove some obsolete commented out code, update a couple of comments.


Tue, 30 Aug 2011 10:47:18 GMT campbell [1139]
	* src/Clight/Cexec.ma (modified)
	* src/Clight/CexecSound.ma (modified)
	* src/Clight/Csem.ma (modified)
	* src/Clight/Csyntax.ma (modified)
	* src/Clight/test/insertsort.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/RTLabs/semantics.ma (modified)
	* src/RTLabs/syntax.ma (modified)
	* src/common/AST.ma (modified)
	* src/common/Globalenvs.ma (modified)

	Shift init_data out of generic program record so that it only appears ...


Wed, 15 Jun 2011 14:15:52 GMT campbell [961]
	* src/ASM/Arithmetic.ma (modified)
	* src/ASM/BitVector.ma (modified)
	* src/ASM/Vector.ma (modified)
	* 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/Csyntax.ma (modified)
	* src/Clight/casts.ma (modified)
	* src/Clight/label.ma (modified)
	* src/Clight/test/memorymodel.ma (modified)
	* src/Clight/test/search.ma (modified)
	* src/Clight/test/sum.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/RTLabs/semantics.ma (modified)
	* src/common/AST.ma (modified)
	* src/common/Animation.ma (modified)
	* src/common/Events.ma (modified)
	* src/common/Floats.ma (modified)
	* src/common/FrontEndOps.ma (modified)
	* src/common/Globalenvs.ma (modified)
	* src/common/IO.ma (modified)
	* src/common/Integers.ma (modified)
	* src/common/Values.ma (modified)
	* src/utilities/extranat.ma (modified)

	Use precise bitvector sizes throughout the front end, rather than ...


Mon, 06 Jun 2011 11:27:59 GMT campbell [886]
	* src/Clight/toCminor.ma (modified)
	* src/Cminor/semantics.ma (modified)
	* src/Cminor/syntax.ma (modified)

	Put types into parameter and variable lists in Cminor.
	Temporarily ...


Fri, 03 Jun 2011 15:35:31 GMT campbell [881]
	* src/Clight/test/io.ma (modified)
	* src/Clight/test/sum.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/common/AST.ma (modified)

	Sort out regions in Cminor to fix Clight to Cminor translation of
	Ederef.


Fri, 03 Jun 2011 15:35:31 GMT campbell [880]
	* src/Clight/Cexec.ma (modified)
	* src/Clight/TypeComparison.ma (added)
	* 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/common/AST.ma (modified)

	Add type information into Cminor.
	As a result, the Clight to Cminor ...


Fri, 03 Jun 2011 15:35:27 GMT campbell [878]
	* src/Cminor/syntax.ma (modified)
	* src/ERTL/ERTL.ma (modified)
	* src/LIN/LIN.ma (modified)
	* src/RTL/RTL.ma (modified)
	* src/RTLabs/import.ma (modified)
	* src/RTLabs/syntax.ma (modified)

	Removal of manually inserted record projections.


Thu, 19 May 2011 13:06:42 GMT campbell [816]
	* src/CHANGES (modified)
	* src/Clight/Csem.ma (modified)
	* src/Clight/Csyntax.ma (modified)
	* src/Clight/test/search.ma (modified)
	* src/Clight/toCminor.ma (added)
	* src/Cminor/cminorMatitaPrinter.ml (modified)
	* src/Cminor/semantics.ma (modified)
	* src/Cminor/syntax.ma (modified)
	* src/Cminor/test/factorial.ma (modified)
	* src/Cminor/test/search.ma (modified)
	* src/Cminor/test/switcher.ma (modified)
	* src/Cminor/toRTLabs.ma (modified)
	* src/RTLabs/RTLabsMatitaPrinter.ml (modified)
	* src/RTLabs/import.ma (modified)
	* src/RTLabs/semantics.ma (modified)
	* src/RTLabs/syntax.ma (modified)
	* src/RTLabs/test/search.ma (modified)
	* src/common/Identifiers.ma (modified)
	* src/utilities/lists.ma (modified)

	Clight to Cminor compilation, modulo switch statements, temporary ...


Wed, 13 Apr 2011 16:52:10 GMT campbell [751]
	* src/Cminor (added)
	* src/Cminor/cminorMatitaPrinter.ml (added)
	* src/Cminor/semantics.ma (added)
	* src/Cminor/syntax.ma (added)
	* src/Cminor/test (added)
	* src/Cminor/test/factorial.ma (added)
	* src/Cminor/test/search.ma (added)
	* src/RTLabs/RTLabs-sem.ma (modified)
	* src/common/SmallstepExec.ma (modified)
	* src/common/Values.ma (modified)

	Initial version of the Cminor syntax and semantics.