#
# ChangeLog for src/Clight/CexecSound.ma
#
# Generated by Trac 1.2
# Apr 21, 2021, 5:41:09 AM

Tue, 21 Feb 2012 10:58:12 GMT campbell [1713]
	* 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/Cminor/semantics.ma (modified)
	* src/RTLabs/Traces.ma (modified)
	* src/RTLabs/semantics.ma (modified)

	Add a distinguished final state to the front-end languages to match ...


Wed, 01 Feb 2012 15:16:06 GMT campbell [1672]
	* src/Clight/CexecComplete.ma (modified)
	* src/Clight/CexecSound.ma (modified)
	* src/Clight/Csem.ma (modified)

	Matita now generates a couple of inversion lemmas that were manually ...


Tue, 17 Jan 2012 12:13:08 GMT tranquil [1647]
	* src/Clight/Cexec.ma (modified)
	* src/Clight/CexecSound.ma (modified)
	* src/common/Errors.ma (modified)
	* src/common/IOMonad.ma (modified)
	* src/utilities/bindLists.ma (modified)
	* src/utilities/lists.ma (modified)
	* src/utilities/monad.ma (modified)
	* src/utilities/option.ma (modified)
	* src/utilities/state.ma (modified)

	* corrected some notation problems
	* adapted Cligth with slight ...


Wed, 23 Nov 2011 17:03:07 GMT campbell [1545]
	* src/Clight/Cexec.ma (modified)
	* src/Clight/CexecComplete.ma (modified)
	* src/Clight/CexecSound.ma (modified)
	* src/Clight/Csem.ma (modified)
	* src/common/FrontEndOps.ma (modified)
	* src/common/Globalenvs.ma (modified)
	* src/common/Mem.ma (modified)
	* src/common/Pointers.ma (modified)
	* src/common/Values.ma (modified)

	Use pointer record in front-end.


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.


Wed, 16 Nov 2011 15:38:41 GMT sacerdot [1510]
	* src/Clight/CexecComplete.ma (modified)
	* src/Clight/CexecEquiv.ma (modified)
	* src/Clight/CexecSound.ma (modified)
	* src/common/Smallstep.ma (modified)
	* src/common/Values.ma (modified)

	All files ported to new dependent inversion.


Wed, 19 Oct 2011 09:54:13 GMT campbell [1410]
	* src/Clight/CexecSound.ma (modified)
	* src/Cminor/toRTLabs.ma (modified)
	* src/common/FrontEndOps.ma (modified)

	Remove a few old workarounds.


Tue, 11 Oct 2011 00:27:53 GMT sacerdot [1350]
	* src/Clight/CexecEquiv.ma (modified)
	* src/Clight/CexecSound.ma (modified)
	* src/Clight/TypeComparison.ma (modified)
	* src/common/AST.ma (modified)
	* src/utilities/extralib.ma (modified)

	Porting to latest destruct tactic.

	Note: the tactics has a few ...


Mon, 10 Oct 2011 15:16:11 GMT sacerdot [1342]
	* src/Clight/CexecSound.ma (modified)

	The new auto is much more powerful.


Mon, 10 Oct 2011 13:54:59 GMT sacerdot [1336]
	* src/Clight/CexecSound.ma (modified)

	Ported to new Matita destruct/inversion.
	One lemma fails at qed. ...


Wed, 21 Sep 2011 16:08:50 GMT campbell [1244]
	* src/Clight/Cexec.ma (modified)
	* src/Clight/CexecComplete.ma (modified)
	* src/Clight/CexecEquiv.ma (modified)
	* src/Clight/CexecSound.ma (modified)

	Sort out Clight semantics equivalence proof for new SmallstepExec.


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


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


Wed, 06 Jul 2011 11:29:58 GMT campbell [1058]
	* src/Clight/Cexec.ma (modified)
	* src/Clight/CexecComplete.ma (modified)
	* src/Clight/CexecSound.ma (modified)
	* src/Clight/Csem.ma (modified)
	* src/common/Identifiers.ma (modified)
	* src/common/Maps.ma (deleted)

	Evict CompCert Maps interface in favour of BitVectorTries.


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


Tue, 07 Jun 2011 14:53:53 GMT campbell [891]
	* src/ASM/BitVectorZ.ma (modified)
	* src/Clight/Cexec.ma (modified)
	* src/Clight/CexecComplete.ma (modified)
	* src/Clight/CexecEquiv.ma (modified)
	* src/Clight/CexecSound.ma (modified)
	* src/Clight/TypeComparison.ma (modified)
	* src/common/Mem.ma (modified)
	* src/common/Smallstep.ma (modified)
	* src/common/Values.ma (modified)
	* src/utilities/binary/Z.ma (modified)
	* src/utilities/binary/positive.ma (modified)
	* src/utilities/extralib.ma (modified)

	Revise proofs affected by recent matita change.


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: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, 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, 07 Apr 2011 16:53:59 GMT campbell [744]
	* src/ASM/Arithmetic.ma (modified)
	* src/ASM/BitVector.ma (modified)
	* src/ASM/Vector.ma (modified)
	* src/Clight/AST.ma (modified)
	* src/Clight/Cexec.ma (modified)
	* src/Clight/CexecSound.ma (modified)
	* src/Clight/Csem.ma (modified)
	* src/Clight/Csyntax.ma (modified)
	* src/RTLabs/RTLabs-sem.ma (modified)
	* src/common/FrontEndOps.ma (modified)
	* src/common/Globalenvs.ma (modified)
	* src/common/Integers.ma (modified)
	* src/common/Mem.ma (modified)
	* src/common/Values.ma (modified)
	* src/utilities/Coqlib.ma (modified)
	* src/utilities/extranat.ma (added)

	Evict Coq-style integers from common/Integers.ma.

	Make more ...


Wed, 23 Mar 2011 13:28:55 GMT campbell [708]
	* src/Clight/Cexec.ma (modified)
	* src/Clight/CexecComplete.ma (modified)
	* src/Clight/CexecEquiv.ma (modified)
	* src/Clight/CexecSound.ma (modified)

	Use a more normalize-friendly definition of clight_exec to make the ...


Fri, 18 Mar 2011 15:28:26 GMT campbell [700]
	* src/ASM/BitVector.ma (modified)
	* src/ASM/BitVectorZ.ma (modified)
	* src/ASM/Vector.ma (modified)
	* src/Clight/AST.ma (modified)
	* src/Clight/Animation.ma (modified)
	* src/Clight/Cexec.ma (modified)
	* src/Clight/CexecComplete.ma (modified)
	* src/Clight/CexecEquiv.ma (modified)
	* src/Clight/CexecSound.ma (modified)
	* src/Clight/CostLabel.ma (modified)
	* src/Clight/Csem.ma (modified)
	* src/Clight/Csyntax.ma (modified)
	* src/common/Events.ma (modified)
	* src/common/Floats.ma (modified)
	* src/common/Globalenvs.ma (modified)
	* src/common/IOMonad.ma (modified)
	* src/common/Integers.ma (modified)
	* src/common/Maps.ma (modified)
	* src/common/Mem.ma (modified)
	* src/common/Smallstep.ma (modified)
	* src/common/SmallstepExec.ma (modified)
	* src/common/Values.ma (modified)

	Get Clight semantics going again (except for problems CexecEquiv that ...


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

	Start moving Clight into common directory.


Fri, 11 Feb 2011 15:45:38 GMT campbell [500]
	* Deliverables/D3.1/C-semantics/Cexec.ma (modified)
	* Deliverables/D3.1/C-semantics/CexecComplete.ma (modified)
	* Deliverables/D3.1/C-semantics/CexecSound.ma (modified)
	* Deliverables/D3.1/C-semantics/Csem.ma (modified)
	* Deliverables/D3.1/C-semantics/Globalenvs.ma (modified)
	* Deliverables/D3.1/C-semantics/Mem.ma (modified)
	* Deliverables/D3.1/C-semantics/Values.ma (modified)

	Use dependent pointer type to ensure that the representation is ...