# # ChangeLog for src/LIN # # Generated by Trac 1.2 # Jan 22, 2021, 12:02:41 PM Fri, 07 Oct 2011 13:32:07 GMT sacerdot [1324] * src/ERTL/semantics.ma (modified) * src/LIN/semantics.ma (modified) * src/LTL/semantics.ma (modified) * src/RTL/semantics.ma (modified) * src/joint/semantics.ma (modified) The semantics of extended statements must also consider the label ... Thu, 06 Oct 2011 20:35:29 GMT sacerdot [1312] * src/ERTL/semantics.ma (modified) * src/LIN/semantics.ma (modified) * src/LTL/semantics.ma (modified) * src/joint/semantics.ma (modified) Type of frame operations (pop_frame/save_frame) generalized to take ... Wed, 05 Oct 2011 23:24:52 GMT sacerdot [1304] * src/LIN/semantics.ma (added) Work in progress. 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 21:08:37 GMT sacerdot [1281] * src/ERTL/ERTLToLTL.ma (modified) * src/LIN/LIN.ma (modified) * src/LTL/LTL.ma (modified) * src/RTLabs/RTLAbstoRTL.ma (modified) * src/joint/semantics.ma (modified) Porting of all transformation to the joint syntax practically ... Mon, 26 Sep 2011 16:07:47 GMT sacerdot [1275] * src/ERTL/ERTLToLTL.ma (modified) * src/ERTL/liveness.ma (modified) * src/ERTL/uses.ma (deleted) * src/LIN/LINToASM.ma (modified) * src/RTL/RTL.ma (modified) * src/RTL/RTLTailcall.ma (modified) * src/RTL/RTLtoERTL.ma (modified) * src/joint/Joint.ma (modified) RTL ported to joint syntax, but: 1. bug discovered: opaccs should ... Mon, 26 Sep 2011 13:59:28 GMT sacerdot [1270] * src/ERTL/ERTL.ma (modified) * src/LIN/LIN.ma (modified) * src/LIN/LINToASM.ma (modified) * src/LTL/LTL.ma (modified) * src/RTL/RTL.ma (modified) * src/RTL/RTLTailcall.ma (modified) * src/RTL/RTLtoERTL.ma (modified) * src/joint/Joint.ma (modified) Making RTL syntax an instance of Joint. Mon, 26 Sep 2011 12:52:22 GMT sacerdot [1268] * src/LIN/LINToASM.ma (modified) * src/common/AST.ma (modified) * src/common/CostLabel.ma (modified) * src/utilities/IdentifierTools.ma (deleted) 1) AST/Identifier.ma no longer used, utilities/IdentifierTools no ... Fri, 23 Sep 2011 16:44:20 GMT sacerdot [1264] * src/LIN/LIN.ma (modified) * src/LIN/LINToASM.ma (modified) Almost ported to new Joint syntax. Thu, 22 Sep 2011 10:02:35 GMT sacerdot [1250] * src/ERTL/ERTLToLTL.ma (modified) * src/ERTL/liveness.ma (modified) * src/ERTL/uses.ma (modified) * src/LIN/LIN.ma (modified) * src/LTL/LTLToLIN.ma (modified) * src/RTL/RTLtoERTL.ma (modified) * src/joint/Joint.ma (modified) * src/joint/semantics.ma (modified) * src/utilities/extralib.ma (modified) 1. Sigma types projections moved to utilities/extralib.ma 2. ... Thu, 22 Sep 2011 00:50:44 GMT sacerdot [1246] * src/LIN/LIN.ma (modified) * src/LTL/LTL.ma (modified) * src/LTL/LTLToLIN.ma (modified) * src/joint/Joint.ma (modified) * src/joint/semantics.ma (modified) Yet another change to Joint.ma to accomodate all passes. The ... Wed, 21 Sep 2011 20:22:13 GMT sacerdot [1245] * src/LIN/LINToASM.ma (modified) * src/RTL/RTLtoERTL.ma (modified) * src/joint/Joint.ma (modified) RTLtoERTL and LINToASM: porting to new Joint data type in progress. ... Wed, 21 Sep 2011 13:56:54 GMT sacerdot [1236] * src/LIN/LIN.ma (modified) * src/LTL/LTLToLIN.ma (modified) * src/joint/Joint.ma (modified) LTLToLin.ma completed (up to a couple of daemons used to provide dead ... Wed, 21 Sep 2011 09:57:20 GMT sacerdot [1233] * src/LIN/LIN.ma (modified) * src/LTL/LTL.ma (modified) * src/LTL/LTLToLIN.ma (modified) * src/RTL/semantics.ma (modified) * src/common/SmallstepExec.ma (modified) * src/joint/Joint.ma (modified) * src/joint/semantics.ma (modified) 1) Ported to Brian's new dependent type for fullexec 2) Universe ... Fri, 16 Sep 2011 16:39:05 GMT sacerdot [1224] * src/Clight/CexecSound.ma (modified) * src/Clight/Csyntax.ma (modified) * src/Clight/SimplifyCasts.ma (modified) * src/Clight/label.ma (modified) * src/Clight/test/search.c.ma (modified) * src/Clight/toCminor.ma (modified) * src/Cminor/initialisation.ma (modified) * src/Cminor/syntax.ma (modified) * src/Cminor/toRTLabs.ma (modified) * src/LIN/LIN.ma (modified) * src/LTL/LTLToLIN.ma (modified) * src/RTLabs/RTLAbstoRTL.ma (modified) * src/RTLabs/syntax.ma (modified) * src/common/AST.ma (modified) * src/common/Globalenvs.ma (modified) * src/common/IntValue.ma (deleted) Type of programs in common/AST made more dependent. In particular, ... Mon, 05 Sep 2011 11:31:54 GMT mulligan [1183] * src/ERTL/ERTL.ma (modified) * src/LIN/LIN.ma (modified) * src/LTL/LTL.ma (modified) removed parameterised label types in the three lowest level languages Mon, 05 Sep 2011 09:58:58 GMT mulligan [1179] * src/ERTL/ERTLToLTL.ma (modified) * src/LIN/LIN.ma (modified) * src/LIN/LINToASM.ma (modified) * src/LTL/LTL.ma (modified) changes to ertl, ltl and lin to use new notion of joint params. ertl ... Fri, 02 Sep 2011 12:51:20 GMT mulligan [1171] * src/ERTL/ERTL.ma (modified) * src/ERTL/ERTLToLTL.ma (modified) * src/LIN/LIN.ma (modified) * src/LTL/LTL.ma (modified) * src/LTL/LTLToLIN.ma (modified) * src/joint/Joint.ma (modified) changes made on claudio's request: changed order of nesting in the ... Fri, 02 Sep 2011 09:36:15 GMT sacerdot [1168] * src/ERTL/ERTL.ma (modified) * src/ERTL/ERTLToLTL.ma (modified) * src/LIN/LIN.ma (modified) * src/LIN/LINToASM.ma (modified) * src/LTL/LTL.ma (modified) Joint statements parameterized over a record. Fri, 02 Sep 2011 08:35:54 GMT mulligan [1167] * src/LIN/LIN.ma (modified) * src/joint/Joint.ma (moved) ... Fri, 02 Sep 2011 08:35:24 GMT mulligan [1166] * src/ERTL/ERTLToLTL.ma (modified) * src/LIN/LIN.ma (modified) * src/LTL/LTL.ma (modified) * src/LTL/LTLToLIN.ma (modified) * src/joint (added) * src/joint/JointLTLLIN.ma (moved) moved joint ltl lin files into their own directory. more changes to ... Thu, 01 Sep 2011 14:53:01 GMT mulligan [1164] * src/LIN/JointLTLLIN.ma (modified) * src/LIN/LIN.ma (modified) * src/LTL/LTL.ma (modified) * src/LTL/LTLToLIN.ma (modified) ltl to lin working again, more changes to joint syntax Thu, 01 Sep 2011 14:23:42 GMT mulligan [1163] * src/ERTL/ERTL.ma (modified) * src/ERTL/ERTLToLTL.ma (modified) * src/ERTL/semantics.ma (modified) * src/LIN/JointLTLLIN.ma (modified) * src/LIN/LIN.ma (modified) * src/LTL/LTL.ma (modified) even more streamlining and fixes to get things type checking Wed, 31 Aug 2011 16:24:03 GMT mulligan [1161] * src/ASM/Util.ma (modified) * src/ERTL/ERTL.ma (modified) * src/ERTL/ERTLToLTL.ma (modified) * src/ERTL/semantics.ma (modified) * src/LIN/JointLTLLIN.ma (modified) * src/LTL/LTL.ma (modified) changes from today: merged ertl, ltl and lin into one datatype to ... Tue, 30 Aug 2011 14:22:54 GMT mulligan [1149] * src/LIN/LINToASM.ma (modified) * src/LTL/LTLToLIN.ma (modified) * src/RTL/RTLtoERTL.ma (modified) * src/RTLabs/RTLAbstoRTL.ma (modified) changes to get everything type checking again after changing names of ... Mon, 29 Aug 2011 15:30:25 GMT mulligan [1132] * src/LIN/JointLTLLIN.ma (modified) * src/LIN/LIN.ma (modified) * src/LTL/LTL.ma (modified) reunified ltl and lin instruction type, removing lifting in ltl and ... Wed, 24 Aug 2011 17:08:49 GMT mulligan [1112] * src/ASM/ASM.ma (modified) * src/LIN/LINToASM.ma (modified) got lin > asm stuff working Wed, 24 Aug 2011 16:45:01 GMT mulligan [1110] * src/ERTL/ERTLToLTL.ma (modified) * src/LIN/JointLTLLIN.ma (modified) * src/LIN/LIN.ma (modified) * src/LTL/LTL.ma (modified) * src/LTL/LTLToLIN.ma (modified) changes to get ltl to lin pass to work properly Wed, 24 Aug 2011 13:04:20 GMT mulligan [1108] * src/ERTL/ERTLToLTLI.ma (modified) * src/LIN/JointLTLLIN.ma (modified) changes to get ertltoltli to compile Wed, 27 Jul 2011 15:50:25 GMT mulligan [1089] * src/ASM/I8051.ma (modified) * src/LIN/JointLTLLIN.ma (modified) * src/LTL/LTL.ma (modified) * src/RTL/RTL.ma (modified) * src/RTL/RTLinterpret.ma (added) more changes from earlier in the week Wed, 20 Jul 2011 15:17:38 GMT mulligan [1082] * src/ERTL/ERTL.ma (modified) * src/ERTL/ERTLToLTL.ma (modified) * src/ERTL/ERTLToLTLI.ma (added) * src/ERTL/Liveness.ma (modified) * src/ERTL/Uses.ma (modified) * src/LIN/JointLTLLIN.ma (modified) * src/LTL/LTL.ma (modified) * src/common/Graphs.ma (modified) work from today on ertl -> ltl pass Fri, 03 Jun 2011 15:35:27 GMT campbell [878] * src/Cminor/syntax.ma (modified) * src/ERTL/ERTL.ma (modified) * src/LIN/LIN.ma (modified) * src/RTL/RTL.ma (modified) * src/RTLabs/import.ma (modified) * src/RTLabs/syntax.ma (modified) Removal of manually inserted record projections. Mon, 18 Apr 2011 10:30:53 GMT mulligan [757] * src/ASM/ASM.ma (modified) * src/ASM/Assembly.ma (modified) * src/ASM/I8051.ma (modified) * src/ASM/Interpret.ma (modified) * src/ASM/Status.ma (modified) * src/ERTL/ERTLToLTL.ma (modified) * src/LIN/JointLTLLIN.ma (modified) * src/LIN/LIN.ma (modified) * src/LIN/LINToASM.ma (modified) * src/LTL/LTL.ma (modified) * src/LTL/LTLToLIN.ma (modified) * src/common/AST.ma (modified) * src/common/CostLabel.ma (modified) * src/common/Identifiers.ma (modified) * src/common/Registers.ma (modified) Lots more fixing to get both front and backends using same ... Fri, 01 Apr 2011 14:14:28 GMT mulligan [734] * src/LIN/LINToASM.ma (modified) Fixed lin2asm. Fri, 01 Apr 2011 14:09:51 GMT mulligan [733] * src/ERTL (added) * src/ERTL/Build.ma (added) * src/ERTL/ERTL.ma (added) * src/ERTL/ERTLToLTL.ma (added) * src/ERTL/Liveness.ma (added) * src/LIN/JointLTLLIN.ma (added) * src/LTL/Branch.ma (added) * src/LTL/LTLToLIN.ma (modified) * src/LTL/LTLToLINI.ma (deleted) * src/utilities/UnionFind.ma (added) Fixed partial commit. Wed, 30 Mar 2011 10:34:25 GMT mulligan [723] * src/CHANGES (modified) * src/LIN/LIN.ma (modified) * src/LIN/LINToASM.ma (modified) * src/LTL/LTL.ma (modified) * src/LTL/LTLToLIN.ma (modified) Added dependent type internalising the invariant that LIN function ... Tue, 29 Mar 2011 16:32:47 GMT mulligan [722] * src/ASM/ASM.ma (modified) * src/LIN/LIN.ma (modified) * src/LIN/LINToASM.ma (modified) * src/LTL/LTL.ma (modified) * src/LTL/LTLToLIN.ma (modified) * src/LTL/LTLToLINI.ma (modified) * src/common/AST.ma (modified) Committing changes from today. Several files do not typecheck. Tue, 29 Mar 2011 10:24:45 GMT mulligan [714] * src/ASM/ASM.ma (modified) * src/LIN/LIN.ma (modified) * src/LTL/LTL.ma (modified) * src/LTL/LTLToLIN.ma (added) * src/common/AST.ma (modified) Work on translation from LTL to LIN. Fri, 18 Mar 2011 13:53:25 GMT mulligan [699] * src/LIN/LIN.ma (modified) * src/LIN/LINToASM.ma (modified) * src/common/AST.ma (modified) * src/common/CostLabel.ma (modified) * src/utilities/IdentifierTools.ma (added) * src/utilities/StringTools.ma (deleted) More or less finished formalisation of LIN. Fri, 18 Mar 2011 12:47:53 GMT mulligan [698] * src/ASM/ASM.ma (modified) * src/ASM/Arithmetic.ma (modified) * src/ASM/BitVector.ma (modified) * src/ASM/BitVectorTrie.ma (modified) * src/ASM/Fetch.ma (modified) * src/ASM/I8051.ma (modified) * src/ASM/Interpret.ma (modified) * src/ASM/Status.ma (modified) * src/ASM/String.ma (modified) * src/ASM/Util.ma (modified) * src/ASM/Vector.ma (modified) * src/LIN/LIN.ma (modified) * src/LIN/LINToASM.ma (modified) * src/common/AST.ma (modified) * src/common/CostLabel.ma (modified) * src/utilities/BitVectorTrieSet.ma (modified) * src/utilities/StringTools.ma (modified) Commit with changes to files to get our files to typecheck. Fri, 18 Mar 2011 12:01:58 GMT mulligan [696] * src/ASM/I8051.ma (added) * src/LIN/LIN.ma (modified) * src/LIN/LINToASM.ma (modified) * src/root (added) Added missing I8051 file and completed most of LIN formalisation. Fri, 18 Mar 2011 10:36:15 GMT mulligan [691] * src/LIN/LINToASM.ma (copied) * src/common (copied) * src/utilities (copied) More movement of files within the repository. Fri, 18 Mar 2011 10:31:32 GMT mulligan [688] * Deliverables/D4.1/Demo-March-2011 (deleted) * Deliverables/D4.2-4.3/LIN/LinToAsm.ma (deleted) * src (added) * src/ASM (moved) * src/LIN (moved) * src/LIN/LIN.ma (copied) Fixed local conflicts. Restructured svn repository. Thu, 10 Feb 2011 14:28:59 GMT mulligan [491] * Deliverables/D4.2-4.3/ASM (added) * Deliverables/D4.2-4.3/ASM/I8051.ma (added) * Deliverables/D4.2-4.3/LIN (added) * Deliverables/D4.2-4.3/LIN/LIN.ma (added) * Deliverables/D4.2-4.3/LIN/LinToAsm.ma (added) * Deliverables/D4.2-4.3/common (added) * Deliverables/D4.2-4.3/common/AST.ma (added) * Deliverables/D4.2-4.3/common/CostLabel.ma (added) * Deliverables/D4.2-4.3/utilities (added) * Deliverables/D4.2-4.3/utilities/BitVectorTrieSet.ma (added) * Deliverables/D4.2-4.3/utilities/Compare.ma (added) * Deliverables/D4.2-4.3/utilities/StringTools.ma (added) Initial commit of (part)-formalisation of LIN intermediate language.