#
# ChangeLog for src/Clight/toCminor.ma
#
# Generated by Trac 1.2
# Apr 19, 2021, 8:25:24 PM

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:36 GMT campbell [1630]
	* src/Clight/toCminor.ma (modified)
	* src/utilities/lists.ma (modified)

	Remainder of freshness in Clight to Cminor pass.


Mon, 19 Dec 2011 13:48:35 GMT campbell [1629]
	* src/Clight/fresh.ma (modified)
	* src/Clight/toCminor.ma (modified)

	Sort out most of the fresh names stuff in Clight to Cminor.


Mon, 19 Dec 2011 13:48:34 GMT campbell [1627]
	* src/Clight/toCminor.ma (modified)
	* src/common/Identifiers.ma (modified)

	Add some notions of freshness, and start using them for temporary ...


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 14:58:39 GMT sacerdot [1612]
	* src/Clight/toCminor.ma (modified)
	* src/RTLabs/import.ma (modified)

	All library ported to new Matita lib (finally).


Wed, 14 Dec 2011 13:30:39 GMT sacerdot [1608]
	* src/Clight/toCminor.ma (modified)
	* src/Cminor/initialisation.ma (modified)
	* src/common/Errors.ma (modified)

	Porting to new library still in progress.


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.


Fri, 18 Nov 2011 23:38:20 GMT sacerdot [1516]
	* src/ASM/BitVector.ma (modified)
	* src/ASM/BitVectorTrie.ma (modified)
	* src/ASM/BitVectorZ.ma (modified)
	* src/ASM/Status.ma (modified)
	* src/ASM/Util.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/casts.ma (modified)
	* src/Clight/toCminor.ma (modified)
	* src/Cminor/initialisation.ma (modified)
	* src/Cminor/semantics.ma (modified)
	* src/Cminor/toRTLabs.ma (modified)
	* src/RTL/RTLToERTL.ma (modified)
	* src/common/AST.ma (modified)
	* src/common/Events.ma (modified)
	* src/common/FrontEndOps.ma (modified)
	* src/common/GenMem.ma (modified)
	* src/common/Identifiers.ma (modified)
	* src/common/Integers.ma (modified)
	* src/common/Mem.ma (modified)
	* src/common/Pointers.ma (modified)
	* src/common/PositiveMap.ma (modified)
	* src/joint/BEValues.ma (modified)
	* src/joint/TranslateUtils.ma (modified)
	* src/utilities/extralib.ma (modified)
	* src/utilities/extranat.ma (modified)
	* src/utilities/lists.ma (modified)

	Ported to syntax of Matita 0.99.1.


Fri, 18 Nov 2011 12:03:14 GMT campbell [1515]
	* src/ASM/ASM.ma (modified)
	* src/ASM/Erase.ma (modified)
	* src/ASM/I8051.ma (modified)
	* src/ASM/Interpret.ma (modified)
	* src/ASM/Interpret2.ma (modified)
	* src/ASM/Status.ma (modified)
	* src/ASM/StatusProofs.ma (modified)
	* src/Clight/TypeComparison.ma (modified)
	* src/Clight/fresh.ma (modified)
	* src/Clight/label.ma (modified)
	* src/Clight/test/insertsort.test.ma (modified)
	* src/Clight/toCminor.ma (modified)
	* src/Cminor/toRTLabs.ma (modified)
	* src/ERTL/ERTLToLTL.ma (modified)
	* src/LIN/LINToASM.ma (modified)
	* src/LTL/LTLToLIN.ma (modified)
	* src/RTLabs/RTLabsToRTL.ma (modified)
	* src/common/Graphs.ma (modified)
	* src/common/Identifiers.ma (modified)
	* src/common/PositiveMap.ma (added)
	* src/common/PreIdentifiers.ma (modified)
	* src/joint/Erasure.ma (modified)
	* src/joint/SemanticUtils.ma (modified)
	* src/joint/TranslateUtils.ma (modified)
	* src/utilities/binary/positive.ma (modified)
	* src/utilities/extralib.ma (modified)
	* src/utilities/extranat.ma (modified)

	Add type of maps on positive binary numbers, and use them for ...


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


Tue, 11 Oct 2011 10:24:33 GMT campbell [1351]
	* src/Clight/toCminor.ma (modified)
	* src/Cminor/semantics.ma (modified)
	* src/common/Errors.ma (modified)
	* src/utilities/deppair.ma (modified)
	* src/utilities/lists.ma (modified)

	Tidy up some loose ends from the invariants branch merge.


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


Mon, 12 Sep 2011 14:20:57 GMT campbell [1207]
	* src/ASM/Arithmetic.ma (modified)
	* src/Clight/fresh.ma (added)
	* src/Clight/toCminor.ma (modified)

	Second part of fixing temporaries in Clight to Cminor stage.


Mon, 12 Sep 2011 14:20:57 GMT campbell [1206]
	* src/Clight/toCminor.ma (modified)

	First stage of fixing temporary generation in Clight/toCminor.ma.


Tue, 06 Sep 2011 15:20:19 GMT campbell [1194]
	* src/Clight/toCminor.ma (modified)

	Remove old, commented out code.


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


Tue, 19 Jul 2011 10:39:01 GMT campbell [1078]
	* src/Clight/toCminor.ma (modified)

	Implement stack allocation for parameters whose address is taken.


Wed, 15 Jun 2011 14:15:54 GMT campbell [962]
	* src/Clight/toCminor.ma (modified)
	* src/common/FrontEndOps.ma (modified)

	Casts should use source type's signedness, not the target's.


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:32 GMT campbell [882]
	* src/Clight/CexecSound.ma (modified)
	* src/Clight/TypeComparison.ma (modified)
	* src/Clight/toCminor.ma (modified)
	* src/RTLabs/import.ma (modified)
	* src/common/AST.ma (modified)
	* src/utilities/extralib.ma (modified)

	Fix up fragile proofs for current version of matita.


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


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