# # ChangeLog for src/Clight/CexecEquiv.ma # # Generated by Trac 1.2 # Jan 16, 2021, 1:33:39 PM Wed, 14 Dec 2011 12:18:30 GMT sacerdot [1605] * src/Clight/CexecEquiv.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) Porting to last standard library of Matita. Fri, 25 Nov 2011 17:12:47 GMT campbell [1566] * src/Clight/CexecComplete.ma (modified) * src/Clight/CexecEquiv.ma (modified) * src/common/PositiveMap.ma (modified) Pacify changes to destruct tactic. Mon, 21 Nov 2011 12:06:01 GMT sacerdot [1521] * src/ASM/BitVector.ma (modified) * src/ASM/BitVectorTrie.ma (modified) * src/ASM/Status.ma (modified) * src/Clight/CexecComplete.ma (modified) * src/Clight/CexecEquiv.ma (modified) * src/Cminor/toRTLabs.ma (modified) * src/RTLabs/RTLabsToRTL.ma (modified) * src/joint/TranslateUtils.ma (modified) * src/utilities/binary/Z.ma (modified) Syntax change in Matita: change what where => change where what. 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. Tue, 11 Oct 2011 10:45:16 GMT sacerdot [1352] * src/Clight/CexecEquiv.ma (modified) * src/Clight/TypeComparison.ma (modified) * src/Cminor/semantics.ma (modified) * src/ERTL/ERTLToLTL.ma (modified) * src/RTL/RTLToERTL.ma (modified) * src/RTLabs/RTLabsToRTL.ma (modified) * src/joint/TranslateUtils.ma (modified) * src/joint/semantics.ma (modified) This commit is made necessary by the last Matita change. Inclusion ... 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:47:15 GMT sacerdot [1344] * src/Clight/CexecEquiv.ma (modified) Ported to new destruct. 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. Thu, 15 Sep 2011 13:33:09 GMT campbell [1216] * src/Clight/CexecEquiv.ma (modified) Update Clight semantics equivalence proof to match changes in ... 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, 13 May 2011 11:10:23 GMT campbell [798] * src/Clight/CexecEquiv.ma (modified) Fix usual matita tactic mistake. 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 ... Fri, 01 Apr 2011 12:52:30 GMT campbell [732] * src/Clight/CexecEquiv.ma (modified) Fixups for CexecEquiv due to earlier changes in SmallstepExec.ma 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 ... Mon, 21 Mar 2011 17:27:22 GMT campbell [702] * src/Clight/Cexec.ma (modified) * src/Clight/CexecEquiv.ma (modified) * src/RTLabs/RTLabs-sem.ma (modified) * src/RTLabs/RTLabs-syntax.ma (modified) * src/common/FrontEndOps.ma (modified) * src/common/Graphs.ma (modified) * src/common/Registers.ma (modified) * src/common/SmallstepExec.ma (modified) Refine small-step executable semantics abstraction a little. Some ... 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. Wed, 09 Feb 2011 10:49:17 GMT campbell [487] * Deliverables/D3.1/C-semantics/AST.ma (modified) * Deliverables/D3.1/C-semantics/Animation.ma (modified) * Deliverables/D3.1/C-semantics/Cexec.ma (modified) * Deliverables/D3.1/C-semantics/CexecComplete.ma (modified) * Deliverables/D3.1/C-semantics/CexecEquiv.ma (modified) * Deliverables/D3.1/C-semantics/CexecSound.ma (modified) * Deliverables/D3.1/C-semantics/Coqlib.ma (modified) * Deliverables/D3.1/C-semantics/CostLabel.ma (modified) * Deliverables/D3.1/C-semantics/Csem.ma (modified) * Deliverables/D3.1/C-semantics/Csyntax.ma (modified) * Deliverables/D3.1/C-semantics/Errors.ma (modified) * Deliverables/D3.1/C-semantics/Events.ma (modified) * Deliverables/D3.1/C-semantics/Floats.ma (modified) * Deliverables/D3.1/C-semantics/Globalenvs.ma (modified) * Deliverables/D3.1/C-semantics/IOMonad.ma (modified) * Deliverables/D3.1/C-semantics/Integers.ma (modified) * Deliverables/D3.1/C-semantics/Maps.ma (modified) * Deliverables/D3.1/C-semantics/Mem.ma (modified) * Deliverables/D3.1/C-semantics/Smallstep.ma (modified) * Deliverables/D3.1/C-semantics/Values.ma (modified) * Deliverables/D3.1/C-semantics/binary/Z.ma (modified) * Deliverables/D3.1/C-semantics/binary/positive.ma (modified) * Deliverables/D3.1/C-semantics/extralib.ma (modified) Port Clight semantics to the new-new matita syntax.