# # ChangeLog for src/common/SmallstepExec.ma # # Generated by Trac 1.2 # Mar 4, 2021, 5:54:24 AM Tue, 13 Dec 2011 00:34:37 GMT sacerdot [1599] * src/ASM/Arithmetic.ma (modified) * src/ASM/BitVector.ma (modified) * src/ASM/JMCoercions.ma (modified) * src/ASM/Status.ma (modified) * src/ASM/String.ma (modified) * src/ASM/Util.ma (modified) * src/ASM/Vector.ma (modified) * src/Clight/Cexec.ma (modified) * src/Clight/Csyntax.ma (modified) * src/Clight/casts.ma (modified) * src/Clight/test/search.c.ma (modified) * src/Clight/test/sum.test.ma (modified) * src/Cminor/initialisation.ma (modified) * src/Cminor/toRTLabs.ma (modified) * src/common/AssocList.ma (modified) * src/common/Errors.ma (modified) * src/common/Events.ma (modified) * src/common/Floats.ma (modified) * src/common/Globalenvs.ma (modified) * src/common/IOMonad.ma (modified) * src/common/Mem.ma (modified) * src/common/SmallstepExec.ma (modified) * src/joint/BEGlobalenvs.ma (modified) * src/joint/TranslateUtils.ma (modified) * src/utilities/Coqlib.ma (modified) * src/utilities/adt/priority_set_adt.ma (modified) * src/utilities/adt/set_adt.ma (modified) * src/utilities/adt/table_adt.ma (modified) * src/utilities/binary/division.ma (modified) * src/utilities/extralib.ma (modified) * src/utilities/lists.ma (modified) * src/utilities/pair.ma (deleted) Start of merging of stuff into the standard library of Matita. Wed, 21 Sep 2011 09:57:20 GMT sacerdot [1233] * src/LIN/LIN.ma (modified) * src/LTL/LTL.ma (modified) * src/LTL/LTLToLIN.ma (modified) * src/RTL/semantics.ma (modified) * src/common/SmallstepExec.ma (modified) * src/joint/Joint.ma (modified) * src/joint/semantics.ma (modified) 1) Ported to Brian's new dependent type for fullexec 2) Universe ... 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. ... Thu, 15 Sep 2011 12:01:56 GMT sacerdot [1213] * src/common/AST.ma (modified) * src/common/Animation.ma (modified) * src/common/GenMem.ma (added) * src/common/Pointers.ma (added) * src/common/SmallstepExec.ma (modified) * src/common/Values.ma (modified) * src/joint/BEMem.ma (added) * src/joint/BEValues.ma (added) * src/joint/semantics.ma (modified) 1) New values (joint/BEValues.ma) and memory model for the back-ends ... Mon, 05 Sep 2011 11:11:48 GMT mulligan [1181] * src/common/SmallstepExec.ma (modified) changed smallstep exec in order to remove matita bug ... 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 ... Wed, 13 Apr 2011 16:52:10 GMT campbell [751] * src/Cminor (added) * src/Cminor/cminorMatitaPrinter.ml (added) * src/Cminor/semantics.ma (added) * src/Cminor/syntax.ma (added) * src/Cminor/test (added) * src/Cminor/test/factorial.ma (added) * src/Cminor/test/search.ma (added) * src/RTLabs/RTLabs-sem.ma (modified) * src/common/SmallstepExec.ma (modified) * src/common/Values.ma (modified) Initial version of the Cminor syntax and semantics. Fri, 01 Apr 2011 11:35:18 GMT campbell [731] * src/Clight/Cexec.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/RTLabs/RTLabs-sem.ma (modified) * src/RTLabs/test (added) * src/RTLabs/test/search.ma (added) * src/common/Animation.ma (moved) * src/common/IO.ma (added) * src/common/SmallstepExec.ma (modified) Common definition for animation semantics, and factor out IO definitions. 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:59:56 GMT campbell [695] * src/Clight/depends (deleted) * src/Clight/root (deleted) * src/RTLabs (moved) * src/common/Errors.ma (moved) * src/common/Events.ma (moved) * src/common/Floats.ma (moved) * src/common/FrontEndOps.ma (moved) * src/common/Globalenvs.ma (moved) * src/common/Graphs.ma (moved) * src/common/IOMonad.ma (moved) * src/common/Integers.ma (moved) * src/common/Maps.ma (moved) * src/common/Mem.ma (moved) * src/common/Registers.ma (moved) * src/common/Smallstep.ma (moved) * src/common/SmallstepExec.ma (moved) * src/common/Values.ma (moved) * src/utilities/Coqlib.ma (moved) * src/utilities/binary (moved) * src/utilities/extralib.ma (moved) Rearrange Clight files a bit - will try to make them work again soon... Fri, 18 Mar 2011 11:30:38 GMT campbell [694] * src/Clight (moved) Start moving Clight into common directory.