# # ChangeLog for src/joint/TranslateUtils.ma # # Generated by Trac 1.2 # Jan 24, 2021, 1:28:23 PM Wed, 30 Jan 2013 18:25:39 GMT tranquil [2595] * src/joint/Joint.ma (modified) * src/joint/TranslateUtils.ma (modified) * src/joint/blocks.ma (modified) * src/joint/semantics.ma (modified) * src/joint/semantics_blocks.ma (modified) * dropped locals and exit from definition of joint_if_function * new ... Mon, 17 Dec 2012 13:35:30 GMT tranquil [2557] * src/joint/TranslateUtils.ma (modified) minor modification of commented (for now) proof of correctness of ... Wed, 05 Dec 2012 17:57:16 GMT tranquil [2532] * src/joint/Joint.ma (modified) * src/joint/TranslateUtils.ma (modified) * src/joint/linearise.ma (modified) * src/joint/semantics.ma (modified) added FCOND in LIN, and rewritten linearise so that it never adds a ... Thu, 08 Nov 2012 13:27:54 GMT tranquil [2443] * src/ERTL/ERTLToLTL.ma (modified) * src/LIN/LINToASM.ma (modified) * src/LIN/joint_LTL_LIN_semantics.ma (modified) * src/LIN/semantics.ma (modified) * src/LTL/semantics.ma (modified) * src/common/ByteValues.ma (modified) * src/joint/SemanticUtils.ma (modified) * src/joint/Traces.ma (modified) * src/joint/TranslateUtils.ma (modified) * src/joint/lineariseProof.ma (modified) * src/joint/semantics.ma (modified) * src/utilities/deqsets.ma (modified) * src/utilities/lists.ma (modified) changed joint's stack pointer and internal stack Thu, 02 Aug 2012 13:18:11 GMT tranquil [2286] * src/ASM/I8051.ma (modified) * src/ASM/Util.ma (modified) * src/ASM/Vector.ma (modified) * src/ERTL/ERTL.ma (modified) * src/ERTL/ERTLToLTL.ma (modified) * src/ERTL/ERTLToLTL_paolo.ma (deleted) * src/ERTL/ERTL_paolo.ma (deleted) * src/ERTL/Interference.ma (modified) * src/ERTL/Interference_paolo.ma (deleted) * src/ERTL/liveness.ma (modified) * src/ERTL/liveness_paolo.ma (deleted) * src/ERTL/semantics.ma (modified) * src/ERTL/semantics_paolo.ma (deleted) * src/LIN/LIN.ma (modified) * src/LIN/LINToASM.ma (modified) * src/LIN/LIN_paolo.ma (deleted) * src/LIN/joint_LTL_LIN.ma (modified) * src/LIN/joint_LTL_LIN_paolo.ma (deleted) * src/LIN/joint_LTL_LIN_semantics.ma (modified) * src/LIN/joint_LTL_LIN_semantics_paolo.ma (deleted) * src/LIN/semantics.ma (modified) * src/LIN/semantics_paolo.ma (deleted) * src/LTL/LTL.ma (modified) * src/LTL/LTLToLIN.ma (modified) * src/LTL/LTLToLIN_paolo.ma (deleted) * src/LTL/LTL_paolo.ma (deleted) * src/LTL/semantics.ma (modified) * src/LTL/semantics_paolo.ma (deleted) * src/RTL/RTL.ma (modified) * src/RTL/RTLTailcall.ma (modified) * src/RTL/RTLTailcall_paolo.ma (deleted) * src/RTL/RTLToERTL.ma (modified) * src/RTL/RTLToERTL_paolo.ma (deleted) * src/RTL/RTL_paolo.ma (deleted) * src/RTL/semantics.ma (modified) * src/RTL/semantics_paolo.ma (deleted) * src/RTLabs/RTLabsToRTL.ma (modified) * src/RTLabs/RTLabsToRTL_paolo.ma (deleted) * src/common/AST.ma (modified) * src/common/BackEndOps.ma (added) * src/common/ByteValues.ma (modified) * src/common/ByteValues_paolo.ma (deleted) * src/common/FrontEndVal.ma (modified) * src/common/Registers.ma (modified) * src/compiler.ma (modified) * src/joint/BEMem.ma (modified) * src/joint/Joint.ma (modified) * src/joint/Joint_paolo.ma (deleted) * src/joint/SemanticUtils.ma (modified) * src/joint/Traces.ma (modified) * src/joint/TranslateUtils.ma (modified) * src/joint/TranslateUtils_paolo.ma (deleted) * src/joint/blocks.ma (modified) * src/joint/linearise.ma (modified) * src/joint/semantics.ma (modified) * src/joint/semanticsUtils_paolo.ma (deleted) * src/joint/semantics_paolo.ma (deleted) * src/utilities/extranat.ma (modified) Big update! * merge of all _paolo variants * reorganised some ... Thu, 24 May 2012 17:18:35 GMT campbell [1995] * src/ERTL/liveness.ma (modified) * src/LIN/LINToASM.ma (modified) * src/RTL/RTLToERTL.ma (modified) * src/RTLabs/RTLabsToRTL.ma (modified) * src/compiler.ma (modified) * src/joint/TranslateUtils.ma (modified) Overall compiler definition; bits and pieces to make everything ... 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. Mon, 21 Nov 2011 12:06:01 GMT sacerdot [1521] * src/ASM/BitVector.ma (modified) * src/ASM/BitVectorTrie.ma (modified) * src/ASM/Status.ma (modified) * src/Clight/CexecComplete.ma (modified) * src/Clight/CexecEquiv.ma (modified) * src/Cminor/toRTLabs.ma (modified) * src/RTLabs/RTLabsToRTL.ma (modified) * src/joint/TranslateUtils.ma (modified) * src/utilities/binary/Z.ma (modified) Syntax change in Matita: change what where => change where what. 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. Fri, 18 Nov 2011 12:03:14 GMT campbell [1515] * src/ASM/ASM.ma (modified) * src/ASM/Erase.ma (modified) * src/ASM/I8051.ma (modified) * src/ASM/Interpret.ma (modified) * src/ASM/Interpret2.ma (modified) * src/ASM/Status.ma (modified) * src/ASM/StatusProofs.ma (modified) * src/Clight/TypeComparison.ma (modified) * src/Clight/fresh.ma (modified) * src/Clight/label.ma (modified) * src/Clight/test/insertsort.test.ma (modified) * src/Clight/toCminor.ma (modified) * src/Cminor/toRTLabs.ma (modified) * src/ERTL/ERTLToLTL.ma (modified) * src/LIN/LINToASM.ma (modified) * src/LTL/LTLToLIN.ma (modified) * src/RTLabs/RTLabsToRTL.ma (modified) * src/common/Graphs.ma (modified) * src/common/Identifiers.ma (modified) * src/common/PositiveMap.ma (added) * src/common/PreIdentifiers.ma (modified) * src/joint/Erasure.ma (modified) * src/joint/SemanticUtils.ma (modified) * src/joint/TranslateUtils.ma (modified) * src/utilities/binary/positive.ma (modified) * src/utilities/extralib.ma (modified) * src/utilities/extranat.ma (modified) Add type of maps on positive binary numbers, and use them for ... Tue, 11 Oct 2011 10:45:16 GMT sacerdot [1352] * src/Clight/CexecEquiv.ma (modified) * src/Clight/TypeComparison.ma (modified) * src/Cminor/semantics.ma (modified) * src/ERTL/ERTLToLTL.ma (modified) * src/RTL/RTLToERTL.ma (modified) * src/RTLabs/RTLabsToRTL.ma (modified) * src/joint/TranslateUtils.ma (modified) * src/joint/semantics.ma (modified) This commit is made necessary by the last Matita change. Inclusion ... Mon, 03 Oct 2011 06:35:23 GMT sacerdot [1284] * src/RTL/RTLtoERTL.ma (modified) * src/joint/TranslateUtils.ma (modified) Bugs fixed: fresh_label changes the label universe, but this was not ... Fri, 30 Sep 2011 01:12:40 GMT sacerdot [1283] * src/RTL/RTLtoERTL.ma (modified) * src/RTLabs/RTLAbstoRTL.ma (modified) * src/joint/TranslateUtils.ma (modified) Bad programming practice removed: change_label is no longer required ... Wed, 28 Sep 2011 21:50:32 GMT sacerdot [1282] * src/ERTL/ERTLToLTL.ma (modified) * src/ERTL/Interference.ma (modified) * src/ERTL/build.ma (deleted) * src/ERTL/liveness.ma (modified) * src/LIN/LINToASM.ma (modified) * src/LTL/LTLToLIN.ma (modified) * src/RTL/RTLTailcall.ma (modified) * src/RTL/RTLtoERTL.ma (modified) * src/RTLabs/RTLAbstoRTL.ma (modified) * src/joint/Joint.ma (modified) * src/joint/TranslateUtils.ma (modified) Cosmetic change: names of joint statements/instructions shortened and ... Wed, 28 Sep 2011 00:43:37 GMT sacerdot [1280] * src/ERTL/ERTL.ma (modified) * src/LTL/LTL.ma (modified) * src/RTL/RTL.ma (modified) * src/RTL/RTLtoERTL.ma (modified) * src/RTLabs/RTLAbstoRTL.ma (modified) * src/joint/Joint.ma (modified) * src/joint/TranslateUtils.ma (added) Some progress in the porting of RTLAbstoRTL to the joint syntax: 1) ...