# # ChangeLog for src/Clight/Csem.ma # # Generated by Trac 1.2 # Jan 15, 2021, 7:53:07 PM Thu, 15 Nov 2012 17:12:57 GMT garnier [2468] * src/Clight/Cexec.ma (modified) * src/Clight/CexecComplete.ma (modified) * src/Clight/CexecInd.ma (modified) * src/Clight/CexecSound.ma (modified) * src/Clight/ClassifyOp.ma (modified) * src/Clight/Csem.ma (modified) * src/Clight/Csyntax.ma (modified) * src/Clight/MemProperties.ma (modified) * src/Clight/SimplifyCasts.ma (modified) * src/Clight/TypeComparison.ma (modified) * src/Clight/frontend_misc.ma (modified) * src/Clight/labelSimulation.ma (modified) * src/Clight/memoryInjections.ma (modified) * src/Clight/switchRemoval.ma (modified) * src/Clight/toCminor.ma (modified) * src/Cminor/initialisation.ma (modified) * src/common/AST.ma (modified) * src/common/Events.ma (modified) * src/common/FrontEndOps.ma (modified) * src/common/FrontEndVal.ma (modified) * src/common/Globalenvs.ma (modified) * src/common/IO.ma (modified) * src/common/Values.ma (modified) Floats are gone from the front-end. Some trace amount might remain in ... Tue, 06 Nov 2012 15:02:23 GMT campbell [2433] * src/Clight/Csem.ma (modified) Tidy up Clight pointer comparison. Tue, 06 Nov 2012 11:53:46 GMT garnier [2429] * src/Clight/Csem.ma (modified) * src/common/FrontEndMem.ma (modified) Restrict semantics of pointer comparison to what CompCert does - i.e. ... Tue, 06 Nov 2012 11:02:13 GMT campbell [2428] * 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/SimplifyCasts.ma (modified) * src/Clight/labelSimulation.ma (modified) * src/common/IOMonad.ma (modified) Tighten requirements on switch statements in Clight to only give ... Fri, 12 Oct 2012 13:33:53 GMT campbell [2395] * src/Clight/Csem.ma (modified) * src/Clight/test/endptr.test.ma (modified) * src/Clight/test/endptr2.c (added) * src/Clight/test/endptr2.c.ma (added) * src/Clight/test/endptr2.test.ma (copied) * src/Cminor/semantics.ma (modified) * src/RTLabs/semantics.ma (modified) * src/common/FrontEndMem.ma (modified) * src/common/FrontEndOps.ma (modified) Proper handling of comparison of pointers off-the-end of an object. ... Tue, 09 Oct 2012 13:10:07 GMT campbell [2391] * 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/SimplifyCasts.ma (modified) * src/Clight/label.ma (modified) * src/Clight/labelSimulation.ma (modified) * src/Clight/switchRemoval.ma (modified) * src/Clight/test/controlflow.c.ma (modified) * src/Clight/toCminor.ma (modified) Revert "Put the post-loop cost label into the Clight while statement ... Wed, 26 Sep 2012 16:14:38 GMT campbell [2353] * 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/SimplifyCasts.ma (modified) * src/Clight/label.ma (modified) * src/Clight/labelSimulation.ma (modified) * src/Clight/switchRemoval.ma (modified) * src/Clight/test/goto-if.test.ma (modified) * src/Clight/test/sum.test.ma (modified) * src/Clight/toCminor.ma (modified) Put the post-loop cost label into the Clight while statement to get ... Wed, 25 Jul 2012 16:55:36 GMT garnier [2263] * src/Clight/Csem.ma (modified) * src/Clight/switchRemoval.ma (modified) Finished proving semantics preservation under memory injections for ... Thu, 12 Jul 2012 12:56:50 GMT campbell [2177] * src/ASM/Arithmetic.ma (modified) * src/Clight/Csem.ma (modified) * src/common/FrontEndOps.ma (modified) Tidy up multiplication. Thu, 12 Jul 2012 11:28:28 GMT campbell [2176] * src/Clight/Cexec.ma (modified) * src/Clight/CexecComplete.ma (modified) * src/Clight/CexecSound.ma (modified) * src/Clight/ClassifyOp.ma (modified) * src/Clight/Csem.ma (modified) * src/Clight/Csyntax.ma (modified) * src/Clight/SimplifyCasts.ma (modified) * src/Clight/TypeComparison.ma (modified) * src/Clight/clightPrintMatita.ml (modified) * src/Clight/labelSimulation.ma (modified) * src/Clight/test/duff.c.ma (modified) * src/Clight/test/insertsort.c.ma (modified) * src/Clight/test/memorymodel.ma (modified) * src/Clight/test/null-op.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/RTL/semantics.ma (modified) * src/RTLabs/RTLabsToRTL.ma (modified) * src/RTLabs/semantics.ma (modified) * src/common/AST.ma (modified) * src/common/Animation.ma (modified) * src/common/ByteValues.ma (modified) * src/common/FrontEndOps.ma (modified) * src/common/FrontEndVal.ma (modified) * src/common/GenMem.ma (modified) * src/common/Globalenvs.ma (modified) * src/common/IO.ma (modified) * src/common/Pointers.ma (modified) * src/common/Values.ma (modified) * src/joint/BEMem.ma (modified) * src/joint/SemanticUtils.ma (modified) * src/joint/semantics.ma (modified) Remove memory spaces other than XData and Code; simplify pointers as ... Fri, 08 Jun 2012 14:32:03 GMT sacerdot [2032] * src/ASM/ASM.ma (modified) * src/ASM/Arithmetic.ma (modified) * src/ASM/Assembly.ma (modified) * src/ASM/AssemblyProof.ma (modified) * src/ASM/AssemblyProofSplit.ma (modified) * src/ASM/Interpret.ma (modified) * src/ASM/Policy.ma (modified) * src/ASM/Status.ma (modified) * src/ASM/StatusProofs.ma (modified) * src/ASM/Util.ma (modified) * src/ASM/Vector.ma (modified) * src/ASM/WellLabeled.ma (modified) * src/Clight/Csem.ma (modified) * src/Clight/SimplifyCasts.ma (modified) * src/Clight/casts.ma (modified) * src/Cminor/toRTLabs.ma (modified) * src/RTL/RTLToERTL.ma (modified) * src/RTLabs/RTLabsToRTL.ma (modified) * src/RTLabs/RTLabsToRTL_paolo.ma (modified) * src/common/FrontEndOps.ma (modified) * src/common/FrontEndVal.ma (modified) * src/common/Integers.ma (modified) * src/common/Values.ma (modified) !! BEWARE: major commit !! 1) [affects everybody] split for ... Thu, 24 May 2012 09:39:27 GMT campbell [1988] * src/Clight/Cexec.ma (modified) * src/Clight/CexecSound.ma (modified) * src/Clight/Csem.ma (modified) * src/Clight/test/memorymodel.ma (modified) * src/Cminor/semantics.ma (modified) * src/RTLabs/semantics.ma (modified) * src/common/GenMem.ma (modified) * src/common/Globalenvs.ma (modified) * src/common/Mem.ma (modified) * src/joint/BEGlobalenvs.ma (modified) * src/joint/BEMem.ma (modified) Abstraction of the memory contents in the memory models is no longer ... 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. Thu, 03 May 2012 15:53:10 GMT campbell [1914] * src/Clight/Csem.ma (modified) * src/Clight/test/goto-if.c (added) * src/Clight/test/goto-if.c.ma (added) * src/Clight/test/goto-if.test.ma (added) Fix bug in Clight semantics that misses goto-labels inside a cost ... Wed, 04 Apr 2012 16:48:25 GMT campbell [1874] * src/Clight/Cexec.ma (modified) * src/Clight/Csem.ma (modified) * src/Cminor/semantics.ma (modified) * src/RTLabs/semantics.ma (modified) * src/common/FrontEndVal.ma (modified) * src/common/Globalenvs.ma (modified) * src/common/Mem.ma (modified) * src/joint/BEValues.ma (modified) First cut at using back-end memory model throughout. Note the ... Wed, 04 Apr 2012 16:48:23 GMT campbell [1872] * src/Clight/ClassifyOp.ma (added) * src/Clight/Csem.ma (modified) * src/Clight/Csyntax.ma (modified) * src/Clight/SimplifyCasts.ma (modified) * src/Clight/TypeComparison.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/FrontEndOps.ma (modified) * src/common/Globalenvs.ma (modified) * src/common/Mem.ma (modified) * src/common/Values.ma (modified) Make binary operations in Cminor/RTLabs properly typed. A few extra ... 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 ... 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. Tue, 20 Sep 2011 17:11:41 GMT campbell [1231] * src/Clight/Cexec.ma (modified) * src/Clight/Csem.ma (modified) * src/common/Animation.ma (modified) * src/common/Globalenvs.ma (modified) * src/common/SmallstepExec.ma (modified) Change SmallstepExec so that states can depend on global information. ... Tue, 30 Aug 2011 14:09:20 GMT campbell [1147] * src/Clight/Cexec.ma (modified) * src/Clight/Csem.ma (modified) * src/Cminor/syntax.ma (modified) * src/RTLabs/syntax.ma (modified) Remove some obsolete commented out code, update a couple of comments. 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:55 GMT campbell [964] * src/Clight/Cexec.ma (modified) * src/Clight/Csem.ma (modified) Rest of cast fix. 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 ... 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 ... 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 ... 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, 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 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. Mon, 07 Mar 2011 18:00:08 GMT campbell [648] * Deliverables/D3.1/C-semantics/Csem.ma (modified) * Deliverables/D3.1/C-semantics/Integers.ma (modified) Oops, wrong bitvector negation.