# # ChangeLog for src/compiler.ma # # Generated by Trac 1.2 # Mar 6, 2021, 1:40:23 PM Fri, 22 Feb 2013 10:39:03 GMT sacerdot [2693] * src/BACKEND_BROKEN_FILES (modified) * src/ERTLptr/ERTLptrToLTL.ma (moved) * src/ERTLptr/Interference.ma (moved) * src/ERTLptr/liveness.ma (moved) * src/compiler.ma (modified) 1. Stuff moved to correct places. 2. ERTLptr pass added Thu, 07 Feb 2013 20:22:22 GMT sacerdot [2645] * src/ASM/ASM.ma (modified) * src/ASM/BitVector.ma (modified) * src/ASM/Char.ma (deleted) * src/ASM/I8051.ma (modified) * src/BACKEND_BROKEN_FILES (added) * src/Clight/Cexec.ma (modified) * src/Clight/Csyntax.ma (modified) * src/Clight/TypeComparison.ma (modified) * src/Clight/test/addptrcharboth.test.ma (modified) * src/Clight/test/badconditional.test.ma (modified) * src/Clight/test/controlflow.test.ma (modified) * src/Clight/test/endptr.test.ma (modified) * src/Clight/test/endptr2.test.ma (modified) * src/Clight/test/forcont.test.ma (modified) * src/Clight/test/goto-if.test.ma (modified) * src/Clight/test/implicit.test.ma (modified) * src/Clight/test/implicitcond.test.ma (modified) * src/Clight/test/sum.test.ma (modified) * src/Clight/test/trivial.test.ma (modified) * src/Clight/toCminor.ma (modified) * src/Cminor/Cminor_semantics.ma (modified) * src/Cminor/Cminor_syntax.ma (modified) * src/ERTL/ERTL.ma (modified) * src/ERTLptr/ERTLptr.ma (modified) * src/ERTLptr/ERTLtoERTLptrOK.ma (modified) * src/LIN/joint_LTL_LIN.ma (modified) * src/LIN/joint_LTL_LIN_semantics.ma (modified) * src/RTL/RTL_semantics.ma (modified) * src/RTLabs/RTLabs_semantics.ma (modified) * src/RTLabs/import.ma (modified) * src/common/AST.ma (modified) * src/common/Animation.ma (modified) * src/common/BackEndOps.ma (modified) * src/common/ByteValues.ma (modified) * src/common/CostLabel.ma (modified) * src/common/ErrorMessages.ma (added) * src/common/Errors.ma (modified) * src/common/Globalenvs.ma (modified) * src/common/Graphs.ma (modified) * src/common/IO.ma (modified) * src/common/Identifiers.ma (modified) * src/common/PreIdentifiers.ma (modified) * src/common/Registers.ma (modified) * src/common/Values.ma (modified) * src/compiler.ma (modified) * src/joint/Joint.ma (modified) * src/joint/String.ma (moved) * src/joint/Traces.ma (modified) * src/joint/joint_semantics.ma (modified) * src/joint/semanticsUtils.ma (modified) 1. some broken back-end files repaires, several still to go 2. the ... Tue, 15 Jan 2013 14:45:28 GMT mckinna [2581] * src/compiler.ma (modified) commented out back end entirely until knock-on effects of changes to ... Sat, 01 Dec 2012 19:36:52 GMT mckinna [2512] * src/compiler.ma (modified) Simplified dependencies on ASM, to allow rollback to when ... Thu, 29 Nov 2012 19:12:34 GMT mckinna [2508] * src/ASM/ASMCostsSplit.ma (modified) * src/common/StructuredTraces.ma (modified) * src/compiler.ma (modified) more tweaks. compiler and correctness still build. Thu, 29 Nov 2012 14:37:22 GMT mckinna [2505] * src/Clight/label.ma (modified) * src/RTLabs/RTLabsToRTL.ma (modified) * src/compiler.ma (modified) Cleaned up compiler.ma; some refactoring/additional code needed in ... Tue, 27 Nov 2012 16:59:25 GMT mckinna [2497] * src/compiler.ma (modified) Simplified dependencies on ASM; knock-on from changes in ASM/*.ma Mon, 26 Nov 2012 17:24:20 GMT mckinna [2494] * src/compiler.ma (modified) Removed BJC's axiomatisation of rtlabs_to_rtl, now that ... Mon, 26 Nov 2012 10:52:51 GMT campbell [2492] * src/compiler.ma (modified) Reduce axiomatisation in compiler.ma. Mon, 19 Nov 2012 16:13:21 GMT campbell [2475] * src/ASM/ASMCosts.ma (modified) * src/ASM/ASMCostsSplit.ma (modified) * src/RTLabs/semantics.ma (modified) * src/compiler.ma (modified) * src/correctness.ma (modified) Get compiler.ma and correctness.ma checking again. Note that the ... Wed, 17 Oct 2012 16:45:20 GMT campbell [2399] * src/Clight/label.ma (modified) * src/compiler.ma (modified) * src/correctness.ma (modified) Fill in some details about the statement of correctness. Mon, 03 Sep 2012 14:33:33 GMT campbell [2320] * src/compiler.ma (modified) * src/correctness.ma (modified) Update compiler and correctness with labelling changes. Mon, 03 Sep 2012 11:16:29 GMT campbell [2319] * src/Clight/label.ma (modified) * src/Clight/labelSimulation.ma (modified) * src/Clight/labelSpecification.ma (modified) * src/Cminor/initialisation.ma (modified) * src/Cminor/toRTLabs.ma (modified) * src/common/AST.ma (modified) * src/common/Globalenvs.ma (modified) * src/compiler.ma (modified) Generate per-program cost labels rather than per-function ones, and ... Thu, 02 Aug 2012 15:04:38 GMT campbell [2291] * src/compiler.ma (modified) Disable switch removal in compiler.ma for now. 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 ... Tue, 24 Jul 2012 17:40:22 GMT campbell [2253] * src/Clight/test/goto-if.test.ma (modified) * src/Clight/test/sum.test.ma (modified) * src/Cminor/toRTLabs.ma (modified) * src/compiler.ma (modified) Cminor to RTLabs is now a total function. Wed, 18 Jul 2012 10:27:01 GMT campbell [2205] * src/LTL/LTLToLIN.ma (modified) * src/compiler.ma (modified) * src/correctness.ma (modified) Get correctness.ma type checking again. Wed, 27 Jun 2012 09:46:36 GMT sacerdot [2116] * src/compiler.ma (modified) load_code_memory will be moved into Fetch.ma in the next commit. ... Wed, 06 Jun 2012 16:24:43 GMT campbell [2019] * src/Clight/Cexec.ma (modified) * src/Clight/CexecInd.ma (added) * src/Clight/CexecSound.ma (modified) * src/Clight/SimplifyCasts.ma (modified) * src/Clight/labelSimulation.ma (modified) * src/compiler.ma (modified) Split out special induction principle for Clight from soundness file. ... Fri, 25 May 2012 11:47:32 GMT campbell [2001] * src/ASM/ASMCostsSplit.ma (modified) * src/ASM/CostsProof.ma (modified) * src/compiler.ma (modified) * src/correctness.ma (modified) Get the compiler to output more. 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 ... Thu, 24 May 2012 14:24:55 GMT campbell [1991] * src/Clight/test/search.c.ma (modified) * src/Clight/test/search.test.ma (added) * src/compiler.ma (added) Put the front end transformations together and make an example use it.