# # ChangeLog for src/RTLabs/RTLabsToRTL_paolo.ma # # Generated by Trac 1.2 # Apr 10, 2021, 11:38:41 PM Thu, 19 Jul 2012 16:13:54 GMT tranquil [2217] * src/ERTL/ERTL_paolo.ma (modified) * src/LIN/joint_LTL_LIN_paolo.ma (modified) * src/LIN/joint_LTL_LIN_semantics_paolo.ma (added) * src/LIN/semantics_paolo.ma (added) * src/LTL/semantics_paolo.ma (added) * src/RTL/RTLToERTL_paolo.ma (modified) * src/RTL/RTL_paolo.ma (modified) * src/RTL/semantics_paolo.ma (modified) * src/RTLabs/RTLabsToRTL_paolo.ma (modified) * src/joint/Joint_paolo.ma (modified) * src/joint/TranslateUtils_paolo.ma (modified) * src/joint/semantics_paolo.ma (modified) * collapsed step_params, unserialized_params, funct_params and ... Thu, 19 Jul 2012 12:42:02 GMT tranquil [2214] * src/ERTL/ERTLToLTL_paolo.ma (modified) * src/ERTL/ERTL_paolo.ma (modified) * src/ERTL/liveness_paolo.ma (modified) * src/LIN/LIN_paolo.ma (modified) * src/LIN/joint_LTL_LIN_paolo.ma (modified) * src/LTL/LTL_paolo.ma (modified) * src/RTL/RTLTailcall_paolo.ma (modified) * src/RTL/RTLToERTL_paolo.ma (modified) * src/RTL/RTL_paolo.ma (modified) * src/RTLabs/RTLabsToRTL_paolo.ma (modified) * src/joint/Joint_paolo.ma (modified) * src/joint/TranslateUtils_paolo.ma (modified) * src/joint/blocks.ma (modified) * src/joint/linearise.ma (modified) * src/joint/semanticsUtils_paolo.ma (modified) * src/joint/semantics_paolo.ma (modified) * changed order of parameters of joint_internal_function and genv in ... Wed, 18 Jul 2012 11:26:43 GMT tranquil [2208] * src/ERTL/ERTLToLTL_paolo.ma (modified) * src/ERTL/ERTL_paolo.ma (modified) * src/ERTL/liveness_paolo.ma (modified) * src/ERTL/semantics_paolo.ma (added) * src/LIN/joint_LTL_LIN_paolo.ma (modified) * src/LTL/LTL_paolo.ma (modified) * src/RTL/RTLToERTL_paolo.ma (modified) * src/RTL/RTL_paolo.ma (modified) * src/RTLabs/RTLabsToRTL_paolo.ma (modified) * src/joint/Joint_paolo.ma (modified) * src/joint/semanticsUtils_paolo.ma (modified) * moving some code around * changed immediates to hold beval in ... Fri, 06 Jul 2012 15:53:01 GMT tranquil [2162] * src/ERTL/ERTL_paolo.ma (added) * src/RTL/RTLTailcall_paolo.ma (added) * src/RTL/RTLToERTL_paolo.ma (added) * src/RTLabs/RTLabsToRTL_paolo.ma (modified) * src/joint/Joint_paolo.ma (modified) * src/joint/TranslateUtils_paolo.ma (modified) * yet another correction to joint * added functions adding prologues ... Fri, 06 Jul 2012 09:25:43 GMT tranquil [2155] * src/RTL/RTL_paolo.ma (modified) * src/RTLabs/RTLabsToRTL_paolo.ma (modified) * src/common/Identifiers.ma (modified) * src/joint/Joint_paolo.ma (modified) * src/joint/TranslateUtils_paolo.ma (modified) * src/joint/blocks.ma (modified) * src/utilities/bindLists.ma (modified) updates to blocks and RTLabs to RTL translation (which sidesteps ... Thu, 21 Jun 2012 15:21:02 GMT campbell [2103] * src/Clight/SimplifyCasts.ma (modified) * src/Clight/label.ma (modified) * src/Clight/labelSimulation.ma (modified) * src/Cminor/toRTLabs.ma (modified) * src/ERTL/ERTLToLTL.ma (modified) * src/LTL/LTLToLIN.ma (modified) * src/RTL/RTLTailcall.ma (modified) * src/RTL/RTLToERTL.ma (modified) * src/RTLabs/RTLabsToRTL.ma (modified) * src/RTLabs/RTLabsToRTL_paolo.ma (modified) * src/common/AST.ma (modified) * src/joint/Erasure.ma (modified) Make transform_*program take a more general transformation to make ... Fri, 08 Jun 2012 14:32:03 GMT sacerdot [2032] * src/ASM/ASM.ma (modified) * src/ASM/Arithmetic.ma (modified) * src/ASM/Assembly.ma (modified) * src/ASM/AssemblyProof.ma (modified) * src/ASM/AssemblyProofSplit.ma (modified) * src/ASM/Interpret.ma (modified) * src/ASM/Policy.ma (modified) * src/ASM/Status.ma (modified) * src/ASM/StatusProofs.ma (modified) * src/ASM/Util.ma (modified) * src/ASM/Vector.ma (modified) * src/ASM/WellLabeled.ma (modified) * src/Clight/Csem.ma (modified) * src/Clight/SimplifyCasts.ma (modified) * src/Clight/casts.ma (modified) * src/Cminor/toRTLabs.ma (modified) * src/RTL/RTLToERTL.ma (modified) * src/RTLabs/RTLabsToRTL.ma (modified) * src/RTLabs/RTLabsToRTL_paolo.ma (modified) * src/common/FrontEndOps.ma (modified) * src/common/FrontEndVal.ma (modified) * src/common/Integers.ma (modified) * src/common/Values.ma (modified) !! BEWARE: major commit !! 1) [affects everybody] split for ... 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 ... Fri, 13 Jan 2012 14:08:55 GMT tranquil [1644] * src/RTL/RTL_paolo.ma (modified) * src/RTLabs/RTLabsToRTL_paolo.ma (modified) * src/joint/Joint_paolo.ma (modified) minor changes Fri, 13 Jan 2012 11:23:30 GMT tranquil [1643] * src/RTL/RTL_paolo.ma (modified) * src/RTL/semantics_paolo.ma (modified) * src/RTLabs/RTLabsToRTL_paolo.ma (modified) * src/joint/Joint_paolo.ma (modified) * src/joint/TranslateUtils_paolo.ma (modified) * src/joint/semantics_paolo.ma (modified) * some changes in everything * separated extensions in sequential ... Wed, 11 Jan 2012 16:41:45 GMT tranquil [1640] * src/RTL/RTL_paolo.ma (modified) * src/RTLabs/RTLabsToRTL_paolo.ma (modified) * src/common/AST.ma (modified) * src/common/Errors.ma (modified) * src/common/IOMonad.ma (modified) * src/joint/Joint_paolo.ma (modified) * src/joint/TranslateUtils_paolo.ma (modified) * src/joint/semantics_paolo.ma (added) * src/utilities/monad.ma (modified) * src/utilities/option.ma (modified) * src/utilities/proper.ma (modified) * finished fork of semantics.ma * unification of Errors under the ... Mon, 09 Jan 2012 11:38:32 GMT tranquil [1636] * src/RTL/RTL_paolo.ma (modified) * src/RTLabs/RTLabsToRTL_paolo.ma (modified) * src/utilities/bindLists.ma (modified) * added coercions to arguments (in RTL) and notation for ops (for the ... Fri, 06 Jan 2012 23:33:17 GMT tranquil [1635] * Deliverables/D2.2/8051/src/RTLabs/RTLabsToRTL.ml (modified) * src/ASM/BitVector.ma (modified) * src/ASM/I8051.ma (modified) * src/RTL/RTL_paolo.ma (added) * src/RTLabs/RTLabsToRTL_paolo.ma (added) * src/common/Graphs.ma (modified) * src/common/Identifiers.ma (modified) * src/joint/Joint_paolo.ma (added) * src/joint/TranslateUtils_paolo.ma (added) * src/utilities/bindLists.ma (added) * src/utilities/monad.ma (added) * src/utilities/option.ma (added) * src/utilities/proper.ma (added) * src/utilities/setoids.ma (added) * src/utilities/state.ma (added) * src/utilities/trace.ma (added) * lists with binders and monads * Joint.ma and other temprarily ...