#
# ChangeLog for src/Cminor
#
# Generated by Trac 1.2
# Dec 16, 2019, 3:46:20 AM

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.


Wed, 21 Sep 2011 14:25:36 GMT campbell [1238]
	* src/Clight/test/search.c.ma (modified)
	* src/Cminor/semantics.ma (modified)
	* src/RTLabs/semantics.ma (modified)

	Update Cminor and RTLabs to fit SmallstepExec changes.


Fri, 16 Sep 2011 17:16:44 GMT campbell [1226]
	* src/Clight/clightPrintMatita.ml (modified)
	* src/Clight/test/sum.c.ma (modified)
	* src/Clight/test/sum.test.ma (added)
	* src/Cminor/cminorMatitaPrinter.ml (modified)
	* src/Cminor/test/search.Cminor.ma (modified)
	* src/Cminor/test/search.test.ma (added)
	* src/RTLabs/RTLabsMatitaPrinter.ml (modified)
	* src/RTLabs/test/search.RTLabs.ma (modified)
	* src/RTLabs/test/search.test.ma (added)

	Adjust pretty printers for change in program records, try a test of
	each.


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


Wed, 31 Aug 2011 10:15:39 GMT campbell [1157]
	* src/Clight/clightPrintMatita.ml (modified)
	* src/Clight/test/duff.c.ma (modified)
	* src/Clight/test/factorial.c.ma (modified)
	* src/Cminor/cminorMatitaPrinter.ml (modified)
	* src/Cminor/test/search.Cminor.ma (modified)
	* src/RTLabs/RTLabsMatitaPrinter.ml (modified)
	* src/RTLabs/test/search.RTLabs.ma (modified)

	Update pretty printers and examples.


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


Fri, 15 Jul 2011 14:56:04 GMT campbell [1072]
	* src/Cminor/toRTLabs.ma (modified)
	* src/RTLabs/import.ma (modified)
	* src/common/Identifiers.ma (modified)

	Use not equals form of showing entry/exit labels.


Fri, 15 Jul 2011 10:56:48 GMT campbell [1070]
	* src/ASM/BitVectorTrie.ma (modified)
	* src/Cminor/toRTLabs.ma (modified)
	* src/RTLabs/syntax.ma (modified)
	* src/common/Identifiers.ma (modified)

	Show that entry and exit labels are in the RTLabs graph.


Tue, 05 Jul 2011 14:25:41 GMT campbell [1056]
	* src/Clight/label.ma (modified)
	* src/Cminor/toRTLabs.ma (modified)
	* src/RTLabs/import.ma (modified)
	* src/RTLabs/syntax.ma (modified)
	* src/common/Identifiers.ma (modified)

	Switch to delayed identifier error scheme.


Wed, 15 Jun 2011 14:15:57 GMT campbell [966]
	* src/Cminor/cminorMatitaPrinter.ml (modified)
	* src/Cminor/test/null-op.Cminor.ma (modified)
	* src/Cminor/test/search.Cminor.ma (modified)

	Update Cminor pretty printer and some examples.


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


Wed, 08 Jun 2011 11:14:55 GMT campbell [898]
	* src/Cminor/cminorMatitaPrinter.ml (modified)
	* src/Cminor/test/null-op.Cminor.ma (added)
	* src/Cminor/test/null-op.ma (deleted)
	* src/Cminor/test/search.Cminor.ma (added)
	* src/Cminor/test/search.ma (deleted)
	* src/Cminor/test/sum.ma (deleted)
	* src/RTLabs/RTLabsMatitaPrinter.ml (modified)
	* src/RTLabs/import.ma (modified)
	* src/RTLabs/test/search.RTLabs.ma (added)
	* src/RTLabs/test/sum.RTLabs.ma (added)

	Update pretty printers and examples.


Mon, 06 Jun 2011 14:28:07 GMT campbell [888]
	* src/Cminor/toRTLabs.ma (modified)
	* src/RTLabs/semantics.ma (modified)
	* src/RTLabs/syntax.ma (modified)

	Use simplified conditionals in RTLabs, following the prototype.


Mon, 06 Jun 2011 13:55:23 GMT campbell [887]
	* src/Cminor/initialisation.ma (modified)
	* src/Cminor/toRTLabs.ma (modified)
	* src/RTLabs/semantics.ma (modified)
	* src/RTLabs/syntax.ma (modified)

	Start bringing RTLabs into line with the prototype compiler:
	 - a ...


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:30 GMT campbell [879]
	* src/Clight/CexecComplete.ma (modified)
	* src/Clight/CexecSound.ma (modified)
	* src/Clight/Csyntax.ma (modified)
	* src/Cminor/semantics.ma (modified)
	* src/Cminor/test/factorial.ma (modified)
	* src/Cminor/test/null-op.ma (modified)
	* src/Cminor/test/search.ma (modified)
	* src/Cminor/test/sum-bad.ma (modified)
	* src/Cminor/test/sum.ma (modified)
	* src/Cminor/test/switcher.ma (modified)
	* src/RTLabs/semantics.ma (modified)
	* src/RTLabs/test/search.ma (modified)
	* src/RTLabs/test/sum.ma (modified)
	* src/common/AST.ma (modified)
	* src/common/Animation.ma (modified)
	* src/common/Events.ma (modified)
	* src/common/IO.ma (modified)

	Refine "AST" types to include size/signedness information.


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


Fri, 13 May 2011 11:10:23 GMT campbell [797]
	* src/Clight/Cexec.ma (modified)
	* src/Clight/CexecComplete.ma (modified)
	* src/Clight/CexecEquiv.ma (modified)
	* src/Clight/CexecSound.ma (modified)
	* src/Clight/Csyntax.ma (modified)
	* src/Clight/test/insertsort.ma (modified)
	* src/Clight/test/io.ma (modified)
	* src/Clight/test/io2.ma (modified)
	* src/Cminor/semantics.ma (modified)
	* src/Cminor/test/sum-bad.ma (modified)
	* src/Cminor/toRTLabs.ma (modified)
	* src/RTLabs/debug.ma (modified)
	* src/RTLabs/import.ma (modified)
	* src/RTLabs/semantics.ma (modified)
	* src/common/Animation.ma (modified)
	* src/common/Errors.ma (modified)
	* src/common/Globalenvs.ma (modified)
	* src/common/IO.ma (modified)
	* src/common/IOMonad.ma (modified)
	* src/common/Identifiers.ma (modified)
	* src/common/PreIdentifiers.ma (added)
	* src/common/SmallstepExec.ma (modified)
	* src/common/Values.ma (modified)

	Add error messages wherever the error monad is used.
	Sticks to ...


Tue, 10 May 2011 15:50:09 GMT campbell [790]
	* src/Cminor/toRTLabs.ma (modified)
	* src/common/Mem.ma (modified)

	A little tidying: get rid of requirement for jmeq in Mem.ma, remove ...


Thu, 28 Apr 2011 08:55:49 GMT campbell [780]
	* src/Cminor/toRTLabs.ma (modified)
	* src/utilities/lists.ma (modified)

	Properly update set of registers that are used for pointers in Cminor ...


Wed, 27 Apr 2011 09:47:40 GMT campbell [776]
	* src/Clight/Csem.ma (modified)
	* src/Clight/test/null-op.c (added)
	* src/Clight/test/null-op.ma (added)
	* src/Cminor/cminorMatitaPrinter.ml (modified)
	* src/Cminor/test/null-op.ma (added)

	Fix up some minor null pointer issues in Clight.
	Add corresponding ...


Fri, 22 Apr 2011 15:09:34 GMT campbell [772]
	* src/Cminor/toRTLabs.ma (modified)

	Implement proper support for RTLabs addressing modes.


Fri, 22 Apr 2011 13:21:28 GMT campbell [771]
	* src/Cminor/test/switcher.ma (modified)
	* src/Cminor/toRTLabs.ma (modified)

	Implement switch statements in Cminor -> RTLabs phase


Fri, 22 Apr 2011 11:49:13 GMT campbell [770]
	* src/Clight/test/switcher.c (added)
	* src/Clight/test/switcher.ma (added)
	* src/Cminor/test/switcher.ma (added)

	Clight and Cminor examples for switch statement.


Fri, 22 Apr 2011 11:49:12 GMT campbell [768]
	* src/Cminor/test/factorial.ma (modified)
	* src/Cminor/test/search.ma (modified)
	* src/Cminor/test/sum.ma (modified)

	Make Cminor tests test translation to RTLabs.


Fri, 22 Apr 2011 09:48:04 GMT campbell [767]
	* src/Cminor/toRTLabs.ma (modified)

	Use variable shadowing as a poor man's state monad in cminor to ...


Thu, 21 Apr 2011 17:24:04 GMT campbell [766]
	* src/Cminor/toRTLabs.ma (modified)
	* src/RTLabs/semantics.ma (modified)
	* src/utilities/lists.ma (added)

	Most of the Cminor to RTLabs stage.

	Is buggy, generates inefficient ...


Wed, 20 Apr 2011 15:38:58 GMT campbell [764]
	* src/ASM/Util.ma (modified)
	* src/Cminor/toRTLabs.ma (added)
	* src/RTLabs/syntax.ma (modified)
	* src/common/AST.ma (modified)
	* src/common/Errors.ma (modified)

	Start Cminor to RTLabs phase.

	Includes some syntax for matching ...


Tue, 19 Apr 2011 10:22:32 GMT campbell [761]
	* src/ASM/BitVectorTrie.ma (modified)
	* src/Cminor/semantics.ma (modified)
	* src/Cminor/test/sum-bad.ma (added)
	* src/RTLabs/RTLabs-sem.ma (modified)
	* src/common/Identifiers.ma (modified)
	* src/utilities/Coqlib.ma (modified)
	* src/utilities/option.ma (added)

	Enforce the use of declared identifiers/registers in Cminor/RTLabs.


Tue, 19 Apr 2011 10:22:31 GMT campbell [760]
	* src/Cminor/semantics.ma (modified)

	Fix tailcall continuations in Cminor.


Mon, 18 Apr 2011 10:33:35 GMT campbell [758]
	* src/Clight/test/sum.c (added)
	* src/Clight/test/sum.ma (added)
	* src/Cminor/cminorMatitaPrinter.ml (modified)
	* src/Cminor/initialisation.ma (added)
	* src/Cminor/test/sum.c (added)
	* src/Cminor/test/sum.ma (added)
	* src/common/Globalenvs.ma (modified)

	Implement replacement of global var initialisation data by code in ...


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.