#
# ChangeLog for src/correctness.ma
#
# Generated by Trac 1.2
# Apr 20, 2021, 12:45:01 PM

Sat, 23 Feb 2013 16:05:03 GMT campbell [2722]
	* src/Clight/Cexec.ma (modified)
	* src/Clight/CexecComplete.ma (modified)
	* src/Clight/CexecSound.ma (modified)
	* src/Clight/Csem.ma (modified)
	* src/Clight/SimplifyCasts.ma (modified)
	* src/Clight/labelSimulation.ma (modified)
	* src/Clight/switchRemoval.ma (modified)
	* src/Cminor/Cminor_semantics.ma (modified)
	* src/RTLabs/RTLabs_semantics.ma (modified)
	* src/common/Globalenvs.ma (modified)
	* src/common/Measurable.ma (modified)
	* src/correctness.ma (modified)

	It's easier to keep the real function identifier in front-end ...


Tue, 19 Feb 2013 11:23:50 GMT campbell [2677]
	* src/Clight/Cexec.ma (modified)
	* src/Clight/CexecComplete.ma (modified)
	* src/Clight/CexecEquiv.ma (modified)
	* src/Clight/CexecSound.ma (modified)
	* src/Clight/Clight_abstract.ma (modified)
	* src/Clight/Csem.ma (modified)
	* src/Clight/SimplifyCasts.ma (modified)
	* src/Clight/labelSimulation.ma (modified)
	* src/Clight/switchRemoval.ma (modified)
	* src/Cminor/Cminor_abstract.ma (modified)
	* src/Cminor/Cminor_semantics.ma (modified)
	* src/RTLabs/RTLabs_abstract.ma (modified)
	* src/RTLabs/RTLabs_semantics.ma (modified)
	* src/RTLabs/RTLabs_traces.ma (modified)
	* src/correctness.ma (modified)

	Retain the pointer for the function called in front-end call states ...


Wed, 06 Feb 2013 17:39:19 GMT campbell [2623]
	* src/correctness.ma (modified)

	Name change update.


Thu, 31 Jan 2013 11:06:58 GMT campbell [2596]
	* src/common/Measurable.ma (modified)
	* src/correctness.ma (modified)

	Use a simpler stack cost map, and then specialise to each semantics.


Sat, 01 Dec 2012 20:01:21 GMT mckinna [2513]
	* src/correctness.ma (modified)

	Minor tweaks. Simplified dependencies again.


Thu, 29 Nov 2012 17:38:37 GMT campbell [2506]
	* src/correctness.ma (modified)

	Use common definition of measurable.


Mon, 19 Nov 2012 16:13:21 GMT campbell [2475]
	* src/ASM/ASMCosts.ma (modified)
	* src/ASM/ASMCostsSplit.ma (modified)
	* src/RTLabs/semantics.ma (modified)
	* src/compiler.ma (modified)
	* src/correctness.ma (modified)

	Get compiler.ma and correctness.ma checking again.  Note that the ...


Mon, 22 Oct 2012 14:21:04 GMT campbell [2412]
	* src/correctness.ma (modified)

	Tidy up measurable definition a bit more.


Wed, 17 Oct 2012 16:45:20 GMT campbell [2399]
	* src/Clight/label.ma (modified)
	* src/compiler.ma (modified)
	* src/correctness.ma (modified)

	Fill in some details about the statement of correctness.


Fri, 07 Sep 2012 09:26:19 GMT campbell [2325]
	* src/Clight/abstract.ma (added)
	* src/correctness.ma (modified)

	Fill out some Clight bits and pieces in correctness.ma.


Wed, 05 Sep 2012 11:36:19 GMT campbell [2323]
	* src/correctness.ma (modified)

	Some correctness proof comments.


Tue, 04 Sep 2012 17:37:52 GMT campbell [2322]
	* src/correctness.ma (modified)

	Today's correctness groupthink.


Mon, 03 Sep 2012 14:33:33 GMT campbell [2320]
	* src/compiler.ma (modified)
	* src/correctness.ma (modified)

	Update compiler and correctness with labelling changes.


Wed, 18 Jul 2012 10:27:01 GMT campbell [2205]
	* src/LTL/LTLToLIN.ma (modified)
	* src/compiler.ma (modified)
	* src/correctness.ma (modified)

	Get correctness.ma type checking again.


Tue, 03 Jul 2012 09:30:37 GMT campbell [2150]
	* src/correctness.ma (modified)

	Add labelling result to the correctness file.


Mon, 28 May 2012 12:35:19 GMT campbell [2004]
	* src/correctness.ma (modified)

	Minor edits from discussion.


Mon, 28 May 2012 11:10:50 GMT campbell [2003]
	* src/correctness.ma (modified)

	Some discussion of correctness statements.


Fri, 25 May 2012 11:47:32 GMT campbell [2001]
	* src/ASM/ASMCostsSplit.ma (modified)
	* src/ASM/CostsProof.ma (modified)
	* src/compiler.ma (modified)
	* src/correctness.ma (modified)

	Get the compiler to output more.


Fri, 25 May 2012 07:18:04 GMT campbell [1996]
	* src/ASM/Interpret2.ma (modified)
	* src/correctness.ma (added)

	Work on correctness from yesterday.