#
# ChangeLog for src/Clight/labelSimulation.ma
#
# Generated by Trac 1.2
# Apr 23, 2021, 11:27:24 AM

Wed, 27 Jun 2012 10:04:27 GMT campbell [2118]
	* src/Clight/labelSimulation.ma (modified)
	* src/common/SmallstepExec.ma (modified)

	Labelling preserves behaviour.


Fri, 22 Jun 2012 12:07:38 GMT campbell [2107]
	* src/Clight/labelSimulation.ma (modified)
	* src/common/Globalenvs.ma (modified)

	Memory initialisation and program transformations.


Thu, 21 Jun 2012 15:21:04 GMT campbell [2105]
	* src/Clight/labelSimulation.ma (modified)
	* src/common/AST.ma (modified)
	* src/common/GenMem.ma (modified)
	* src/common/Globalenvs.ma (modified)

	Show some results about globalenvs and program transformations.


Thu, 21 Jun 2012 15:21:02 GMT campbell [2103]
	* src/Clight/SimplifyCasts.ma (modified)
	* src/Clight/label.ma (modified)
	* src/Clight/labelSimulation.ma (modified)
	* src/Cminor/toRTLabs.ma (modified)
	* src/ERTL/ERTLToLTL.ma (modified)
	* src/LTL/LTLToLIN.ma (modified)
	* src/RTL/RTLTailcall.ma (modified)
	* src/RTL/RTLToERTL.ma (modified)
	* src/RTLabs/RTLabsToRTL.ma (modified)
	* src/RTLabs/RTLabsToRTL_paolo.ma (modified)
	* src/common/AST.ma (modified)
	* src/joint/Erasure.ma (modified)

	Make transform_*program take a more general transformation to make ...


Tue, 12 Jun 2012 14:01:39 GMT campbell [2050]
	* src/Clight/labelSimulation.ma (modified)

	Limit some normalization that // doesn't seem to like.


Wed, 06 Jun 2012 16:24:43 GMT campbell [2019]
	* src/Clight/Cexec.ma (modified)
	* src/Clight/CexecInd.ma (added)
	* src/Clight/CexecSound.ma (modified)
	* src/Clight/SimplifyCasts.ma (modified)
	* src/Clight/labelSimulation.ma (modified)
	* src/compiler.ma (modified)

	Split out special induction principle for Clight from soundness file. ...


Thu, 31 May 2012 14:41:33 GMT garnier [2011]
	* src/Clight/SimplifyCasts.ma (modified)
	* src/Clight/labelSimulation.ma (modified)

	Minor cleanup.


Fri, 25 May 2012 09:01:49 GMT campbell [2000]
	* src/Clight/labelSimulation.ma (modified)

	Fix g.e. glitch in label simulation.


Thu, 24 May 2012 07:35:08 GMT campbell [1986]
	* src/Clight/Cexec.ma (modified)
	* src/Clight/Csem.ma (modified)
	* src/Clight/labelSimulation.ma (modified)
	* src/Cminor/semantics.ma (modified)
	* src/RTLabs/semantics.ma (modified)
	* src/common/Globalenvs.ma (modified)

	Get rid of unused abstraction of Globalenvs.


Wed, 16 May 2012 12:44:05 GMT campbell [1954]
	* src/Clight/labelSimulation.ma (modified)
	* src/common/Errors.ma (modified)

	Initial state is in the labelling simulation
	(modulo global envs ...


Wed, 09 May 2012 16:30:41 GMT campbell [1930]
	* src/Clight/CexecComplete.ma (modified)
	* src/Clight/labelSimulation.ma (modified)
	* src/common/IOMonad.ma (modified)
	* src/utilities/extralib.ma (modified)

	Tidy up labelling simulation stuff a bit.


Tue, 08 May 2012 13:41:43 GMT campbell [1922]
	* src/Clight/labelSimulation.ma (modified)

	Main labelling simulation proof complete.


Tue, 08 May 2012 09:16:18 GMT campbell [1920]
	* src/Clight/Csyntax.ma (modified)
	* src/Clight/labelSimulation.ma (modified)
	* src/RTLabs/semantics.ma (modified)
	* src/common/AST.ma (modified)
	* src/common/IOMonad.ma (modified)

	Most of the labelling simulation.  Still need to sort out switch ...


Fri, 20 Apr 2012 09:52:54 GMT campbell [1893]
	* src/Clight/labelSimulation.ma (modified)

	Show stronger result about labelling of expressions.


Fri, 13 Apr 2012 16:36:16 GMT campbell [1888]
	* src/Clight/label.ma (modified)
	* src/Clight/labelSimulation.ma (added)

	Show that labelling of expressions works ...
	after fixing it to ...