#
# ChangeLog for src/common/Pointers.ma
#
# Generated by Trac 1.2
# Jan 28, 2021, 1:30:32 PM

Thu, 19 Jul 2012 16:45:49 GMT campbell [2218]
	* src/RTLabs/CostSpec.ma (added)
	* src/RTLabs/Traces.ma (modified)
	* src/common/Pointers.ma (modified)

	Separate out cost properties required of RTLabs programs from the ...


Fri, 13 Jul 2012 17:59:43 GMT campbell [2185]
	* src/common/FrontEndMem.ma (modified)
	* src/common/GenMem.ma (modified)
	* src/common/Globalenvs.ma (modified)
	* src/common/Pointers.ma (modified)
	* src/joint/BEMem.ma (modified)
	* src/joint/semantics.ma (modified)

	Use bitvectors for offsets.


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, 06 Apr 2012 18:02:10 GMT tranquil [1882]
	* src/ASM/ASM.ma (modified)
	* src/ASM/Status.ma (modified)
	* src/ASM/Util.ma (modified)
	* src/RTL/RTL_paolo.ma (modified)
	* src/RTLabs/RTLabsToRTL_paolo.ma (modified)
	* src/RTLabs/semantics.ma (modified)
	* src/common/AST.ma (modified)
	* src/common/Errors.ma (modified)
	* src/common/Graphs.ma (modified)
	* src/common/IOMonad.ma (modified)
	* src/common/Identifiers.ma (modified)
	* src/common/LabelledObjects.ma (added)
	* src/common/Pointers.ma (modified)
	* src/common/PositiveMap.ma (modified)
	* src/joint/BEMem.ma (modified)
	* src/joint/Joint_paolo.ma (modified)
	* src/joint/TranslateUtils_paolo.ma (modified)
	* src/joint/blocks.ma (added)
	* src/joint/semanticsUtils_paolo.ma (modified)
	* src/joint/semantics_blocks.ma (added)
	* src/joint/semantics_paolo.ma (modified)
	* src/utilities/bindLists.ma (modified)
	* src/utilities/extralib.ma (modified)
	* src/utilities/lists.ma (modified)
	* src/utilities/monad.ma (modified)
	* src/utilities/option.ma (modified)
	* src/utilities/state.ma (modified)
	* src/utilities/trace.ma (modified)

	big update, alas incomplete:
	joint changed a bit, and all BE ...


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.


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.


Thu, 15 Sep 2011 13:04:22 GMT sacerdot [1215]
	* src/common/Pointers.ma (modified)
	* src/joint/semantics.ma (modified)

	1) Added shifting directly on pointers
	2) More temporary axioms closed.


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 ...