#
# ChangeLog for src/Clight/test
#
# Generated by Trac 1.2
# Apr 19, 2021, 1:55:14 AM

Thu, 17 Nov 2011 15:50:46 GMT campbell [1513]
	* src/Clight/test/castremoval.c.ma (modified)
	* src/Clight/test/castremoval.test.ma (added)
	* src/Clight/test/duff.c.ma (modified)
	* src/Clight/test/duff.test.ma (added)
	* src/Clight/test/factorial.c.ma (modified)
	* src/Clight/test/factorial.test.ma (added)
	* src/Clight/test/insertsort.c.ma (modified)
	* src/Clight/test/insertsort.test.ma (added)
	* src/Clight/test/null-op.c.ma (modified)
	* src/Clight/test/null-op.test.ma (added)
	* src/Clight/test/switcher.c.ma (modified)
	* src/Clight/test/switcher.test.ma (added)

	Fix up Clight examples.


Mon, 10 Oct 2011 10:41:50 GMT campbell [1332]
	* src/Clight/test/sum.test.ma (modified)

	Summation example updated (needs computational K).


Mon, 26 Sep 2011 16:14:56 GMT campbell [1276]
	* src/Clight/addRuntime.ma (added)
	* src/Clight/test/runtime.c (added)
	* src/Clight/test/runtime.c.ma (added)
	* src/Clight/test/runtime.test.ma (added)

	Support for replacing operations with runtime support functions in ...


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


Thu, 08 Sep 2011 14:04:07 GMT campbell [1198]
	* src/CHANGES (modified)
	* src/Clight/SimplifyCasts.ma (added)
	* src/Clight/TypeComparison.ma (modified)
	* src/Clight/test/castremoval.c (added)
	* src/Clight/test/castremoval.c.ma (added)
	* src/Clight/test/sum.c.ma (modified)

	Clight cast removal (NB: quite different from the prototype).


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


Thu, 16 Jun 2011 11:32:19 GMT campbell [978]
	* src/Clight/test/duff.ma (deleted)
	* src/Clight/test/factorial.c.ma (moved)
	* src/Clight/test/io.ma (deleted)
	* src/Clight/test/io2.ma (deleted)
	* src/Clight/test/search.c.ma (added)
	* src/Clight/test/switcher.c.ma (moved)

	Update remaining Clight examples.


Wed, 15 Jun 2011 14:15:56 GMT campbell [965]
	* src/Clight/clightPrintMatita.ml (modified)
	* src/Clight/test/duff.c.ma (added)
	* src/Clight/test/insertsort.c (modified)
	* src/Clight/test/insertsort.c.ma (added)
	* src/Clight/test/insertsort.ma (deleted)
	* src/Clight/test/null-op.c.ma (moved)
	* src/Clight/test/search.ma (deleted)
	* src/Clight/test/sum.c.ma (moved)

	Update some Clight 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 ...


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.


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


Thu, 28 Apr 2011 14:43:50 GMT campbell [781]
	* src/Clight/label.ma (added)
	* src/Clight/test/insertsort.ma (modified)
	* src/common/Events.ma (modified)

	Implement labelling pass for Clight.


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


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


Tue, 12 Apr 2011 10:32:32 GMT campbell [748]
	* src/Clight/test/search.ma (modified)

	Change example statement for easier testing.


Fri, 01 Apr 2011 11:35:18 GMT campbell [731]
	* src/Clight/Cexec.ma (modified)
	* src/Clight/test/duff.ma (modified)
	* src/Clight/test/factorial.ma (modified)
	* src/Clight/test/insertsort.ma (modified)
	* src/Clight/test/io.ma (modified)
	* src/Clight/test/io2.ma (modified)
	* src/Clight/test/search.ma (modified)
	* src/RTLabs/RTLabs-sem.ma (modified)
	* src/RTLabs/test (added)
	* src/RTLabs/test/search.ma (added)
	* src/common/Animation.ma (moved)
	* src/common/IO.ma (added)
	* src/common/SmallstepExec.ma (modified)

	Common definition for animation semantics, and factor out IO
	definitions.


Wed, 30 Mar 2011 16:47:35 GMT campbell [726]
	* src/ASM/BitVector.ma (modified)
	* src/ASM/BitVectorTrie.ma (modified)
	* src/ASM/Vector.ma (modified)
	* src/Clight/AST.ma (modified)
	* src/Clight/CexecComplete.ma (modified)
	* src/Clight/test/duff.ma (modified)
	* src/Clight/test/factorial.ma (modified)
	* src/Clight/test/insertsort.ma (modified)
	* src/Clight/test/io.ma (modified)
	* src/Clight/test/io2.ma (modified)
	* src/Clight/test/search.ma (modified)
	* src/RTLabs/import.ma (modified)
	* src/common/Graphs.ma (modified)
	* src/common/Registers.ma (modified)

	Change identifiers to Words in Clight and RTLabs semantics.


Wed, 30 Mar 2011 14:16:08 GMT campbell [725]
	* src/Clight/Cexec.ma (modified)
	* src/Clight/Csem.ma (modified)
	* src/Clight/Csyntax.ma (modified)
	* src/Clight/test/duff.ma (modified)
	* src/Clight/test/factorial.ma (modified)
	* src/Clight/test/insertsort.ma (modified)
	* src/Clight/test/io.ma (modified)
	* src/Clight/test/io2.ma (modified)
	* src/Clight/test/search.ma (modified)
	* src/Clight/test/transform1.ma (modified)

	Do some light manual disambiguation to make Clight examples go ...


Tue, 29 Mar 2011 15:54:36 GMT campbell [717]
	* src/Clight/Csem.ma (modified)
	* src/Clight/test/duff.ma (modified)
	* src/Clight/test/factorial.ma (modified)
	* src/Clight/test/funptr.ma (deleted)
	* src/Clight/test/insertsort.ma (added)
	* src/Clight/test/io.c.ma (deleted)
	* src/Clight/test/io.ma (added)
	* src/Clight/test/io2.c.ma (deleted)
	* src/Clight/test/io2.ma (added)
	* src/Clight/test/memorymodel.ma (modified)
	* src/Clight/test/search.c (added)
	* src/Clight/test/search.ma (added)
	* src/Clight/test/transform1.ma (modified)
	* src/Clight/test/trivial.ma (deleted)

	Clean up Clight examples; better temporary definition of multiply.


Fri, 18 Mar 2011 11:30:38 GMT campbell [694]
	* src/Clight (moved)

	Start moving Clight into common directory.


Fri, 11 Feb 2011 16:45:08 GMT campbell [502]
	* Deliverables/D3.1/C-semantics/Csem.ma (modified)
	* Deliverables/D3.1/C-semantics/test/ptrbool.c (added)

	Fix not on nulls on Clight.