# # ChangeLog for src/Clight/Csem.ma # # Generated by Trac 1.2 # Jan 18, 2021, 9:29:59 PM 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.