# # ChangeLog for src/common/Values.ma # # Generated by Trac 1.2 # Jan 17, 2021, 7:12:39 AM 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. Fri, 14 Oct 2011 08:56:45 GMT campbell [1369] * 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/FrontEndOps.ma (modified) * src/common/Values.ma (modified) Put type information into front-end unary ops. Slight change to ... Mon, 10 Oct 2011 17:22:13 GMT campbell [1347] * src/common/Values.ma (modified) Remove obsolete definitions. Mon, 10 Oct 2011 14:10:32 GMT sacerdot [1339] * src/common/Values.ma (modified) Automation is now stronger. 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 ... 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 [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, 08 Apr 2011 12:06:46 GMT campbell [747] * src/Clight/AST.ma (deleted) * src/Clight/Csyntax.ma (modified) * src/RTLabs/RTLabs-syntax.ma (modified) * src/common/AST.ma (modified) * src/common/CostLabel.ma (modified) * src/common/Globalenvs.ma (modified) * src/common/Integers.ma (modified) * src/common/Maps.ma (modified) * src/common/Values.ma (modified) * src/utilities/Coqlib.ma (modified) Merge the two AST files together (although some definitions still ... 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 ... Tue, 29 Mar 2011 15:54:37 GMT campbell [718] * src/Clight/AST.ma (modified) * src/Clight/Animation.ma (modified) * src/Clight/Cexec.ma (modified) * src/Clight/Csyntax.ma (modified) * src/RTLabs/RTLabs-sem.ma (modified) * src/common/Mem.ma (modified) * src/common/Values.ma (modified) Add an AST type (i.e., intermediate language type) for pointers. 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.