# # ChangeLog for Deliverables/D3.3 # # Generated by Trac 1.2 # Apr 18, 2021, 5:56:58 PM Fri, 14 Oct 2011 08:56:50 GMT campbell [1370] * Deliverables/D3.3/Report/report.tex (modified) D3.3: Added a subsection on the SmallstepExec.ma definitions, plus a ... Mon, 10 Oct 2011 16:18:10 GMT campbell [1346] * Deliverables/D3.2/Report/report.tex (modified) * Deliverables/D3.3/Report/report.tex (modified) Minor corrections and a paragraph of context in the abstract to ... Fri, 07 Oct 2011 10:28:46 GMT campbell [1317] * Deliverables/D3.2/Report/report.tex (modified) * Deliverables/D3.3/Report/report.tex (modified) Fix listings in D3.2/D3.3. Thu, 06 Oct 2011 16:45:54 GMT campbell [1311] * Deliverables/D3.3/id-lookup-branch (modified) * Deliverables/D3.3/id-lookup-branch/ASM (modified) * Deliverables/D3.3/id-lookup-branch/ASM/Arithmetic.ma (modified) * Deliverables/D3.3/id-lookup-branch/ASM/Util.ma (modified) * Deliverables/D3.3/id-lookup-branch/CHANGES (modified) * Deliverables/D3.3/id-lookup-branch/Clight/Cexec.ma (modified) * Deliverables/D3.3/id-lookup-branch/Clight/CexecComplete.ma (modified) * Deliverables/D3.3/id-lookup-branch/Clight/CexecEquiv.ma (modified) * Deliverables/D3.3/id-lookup-branch/Clight/CexecSound.ma (modified) * Deliverables/D3.3/id-lookup-branch/Clight/Csem.ma (modified) * Deliverables/D3.3/id-lookup-branch/Clight/Csyntax.ma (modified) * Deliverables/D3.3/id-lookup-branch/Clight/SimplifyCasts.ma (copied) * Deliverables/D3.3/id-lookup-branch/Clight/TypeComparison.ma (modified) * Deliverables/D3.3/id-lookup-branch/Clight/addRuntime.ma (copied) * Deliverables/D3.3/id-lookup-branch/Clight/clightPrintMatita.ml (modified) * Deliverables/D3.3/id-lookup-branch/Clight/fresh.ma (copied) * Deliverables/D3.3/id-lookup-branch/Clight/label.ma (modified) * Deliverables/D3.3/id-lookup-branch/Clight/test/castremoval.c (copied) * Deliverables/D3.3/id-lookup-branch/Clight/test/castremoval.c.ma (copied) * Deliverables/D3.3/id-lookup-branch/Clight/test/runtime.c (copied) * Deliverables/D3.3/id-lookup-branch/Clight/test/runtime.c.ma (copied) * Deliverables/D3.3/id-lookup-branch/Clight/test/runtime.test.ma (copied) * Deliverables/D3.3/id-lookup-branch/Clight/test/search.c.ma (modified) * Deliverables/D3.3/id-lookup-branch/Clight/test/sum.c.ma (modified) * Deliverables/D3.3/id-lookup-branch/Clight/test/sum.test.ma (copied) * Deliverables/D3.3/id-lookup-branch/Clight/toCminor.ma (modified) * Deliverables/D3.3/id-lookup-branch/Cminor/cminorMatitaPrinter.ml (modified) * Deliverables/D3.3/id-lookup-branch/Cminor/initialisation.ma (modified) * Deliverables/D3.3/id-lookup-branch/Cminor/semantics.ma (modified) * Deliverables/D3.3/id-lookup-branch/Cminor/syntax.ma (modified) * Deliverables/D3.3/id-lookup-branch/Cminor/test/search.Cminor.ma (modified) * Deliverables/D3.3/id-lookup-branch/Cminor/test/search.test.ma (copied) * Deliverables/D3.3/id-lookup-branch/Cminor/toRTLabs.ma (modified) * Deliverables/D3.3/id-lookup-branch/ERTL/ERTL.ma (modified) * Deliverables/D3.3/id-lookup-branch/ERTL/ERTLToLTL.ma (modified) * Deliverables/D3.3/id-lookup-branch/ERTL/Interference.ma (copied) * Deliverables/D3.3/id-lookup-branch/ERTL/build.ma (deleted) * Deliverables/D3.3/id-lookup-branch/ERTL/liveness.ma (modified) * Deliverables/D3.3/id-lookup-branch/ERTL/semantics.ma (modified) * Deliverables/D3.3/id-lookup-branch/ERTL/spill.ma (modified) * Deliverables/D3.3/id-lookup-branch/ERTL/uses.ma (deleted) * Deliverables/D3.3/id-lookup-branch/LIN/LIN.ma (modified) * Deliverables/D3.3/id-lookup-branch/LIN/LINToASM.ma (modified) * Deliverables/D3.3/id-lookup-branch/LTL/LTL.ma (modified) * Deliverables/D3.3/id-lookup-branch/LTL/LTLToLIN.ma (modified) * Deliverables/D3.3/id-lookup-branch/RTL/RTL.ma (modified) * Deliverables/D3.3/id-lookup-branch/RTL/RTLTailcall.ma (modified) * Deliverables/D3.3/id-lookup-branch/RTL/RTLinterpret.ma (deleted) * Deliverables/D3.3/id-lookup-branch/RTL/RTLtoERTL.ma (modified) * Deliverables/D3.3/id-lookup-branch/RTL/semantics.ma (modified) * Deliverables/D3.3/id-lookup-branch/RTLabs/RTLAbstoRTL.ma (modified) * Deliverables/D3.3/id-lookup-branch/RTLabs/RTLabsMatitaPrinter.ml (modified) * Deliverables/D3.3/id-lookup-branch/RTLabs/semantics.ma (modified) * Deliverables/D3.3/id-lookup-branch/RTLabs/syntax.ma (modified) * Deliverables/D3.3/id-lookup-branch/RTLabs/test/search.RTLabs.ma (modified) * Deliverables/D3.3/id-lookup-branch/RTLabs/test/search.test.ma (copied) * Deliverables/D3.3/id-lookup-branch/common/AST.ma (modified) * Deliverables/D3.3/id-lookup-branch/common/Animation.ma (modified) * Deliverables/D3.3/id-lookup-branch/common/CostLabel.ma (modified) * Deliverables/D3.3/id-lookup-branch/common/Errors.ma (modified) * Deliverables/D3.3/id-lookup-branch/common/GenMem.ma (copied) * Deliverables/D3.3/id-lookup-branch/common/Globalenvs.ma (modified) * Deliverables/D3.3/id-lookup-branch/common/Graphs.ma (modified) * Deliverables/D3.3/id-lookup-branch/common/IntValue.ma (deleted) * Deliverables/D3.3/id-lookup-branch/common/Pointers.ma (copied) * Deliverables/D3.3/id-lookup-branch/common/SmallstepExec.ma (modified) * Deliverables/D3.3/id-lookup-branch/common/Values.ma (modified) * Deliverables/D3.3/id-lookup-branch/joint/BEMem.ma (copied) * Deliverables/D3.3/id-lookup-branch/joint/BEValues.ma (copied) * Deliverables/D3.3/id-lookup-branch/joint/Joint.ma (modified) * Deliverables/D3.3/id-lookup-branch/joint/TranslateUtils.ma (copied) * Deliverables/D3.3/id-lookup-branch/joint/semantics.ma (modified) * Deliverables/D3.3/id-lookup-branch/utilities/Colouring.ma (deleted) * Deliverables/D3.3/id-lookup-branch/utilities/IdentifierTools.ma (deleted) * Deliverables/D3.3/id-lookup-branch/utilities/Interference.ma (deleted) * Deliverables/D3.3/id-lookup-branch/utilities/UnionFind.ma (deleted) * Deliverables/D3.3/id-lookup-branch/utilities/adt (copied) * Deliverables/D3.3/id-lookup-branch/utilities/sigma.ma (copied) Merge trunk to invariants branch, sorting out the handling of ... Mon, 26 Sep 2011 10:41:45 GMT campbell [1267] * Deliverables/D3.3/Report/report.tex (modified) Other bits and pieces for D3.3. Mon, 26 Sep 2011 09:29:19 GMT campbell [1265] * Deliverables/D3.3/Report/report.tex (modified) Revisions to D3.3. Wed, 21 Sep 2011 10:14:51 GMT campbell [1235] * Deliverables/D3.2 (added) * Deliverables/D3.2/Report (added) * Deliverables/D3.2/Report/report.bib (added) * Deliverables/D3.2/Report/report.tex (added) * Deliverables/D3.3/Report/report.tex (modified) Some basic material for D3.2, but not yet finished. Wed, 21 Sep 2011 10:14:43 GMT campbell [1234] * Deliverables/D3.3/Report (added) * Deliverables/D3.3/Report/report.bib (added) * Deliverables/D3.3/Report/report.tex (added) Add (rather brief) draft of D3.3. Wed, 07 Sep 2011 10:10:27 GMT campbell [1197] * Deliverables/D3.3/id-lookup-branch (modified) * Deliverables/D3.3/id-lookup-branch/ASM (modified) * Deliverables/D3.3/id-lookup-branch/ASM/I8051.ma (modified) * Deliverables/D3.3/id-lookup-branch/ASM/Util.ma (modified) * Deliverables/D3.3/id-lookup-branch/Clight/clightPrintMatita.ml (modified) * Deliverables/D3.3/id-lookup-branch/Clight/test/duff.c.ma (modified) * Deliverables/D3.3/id-lookup-branch/Clight/test/factorial.c.ma (modified) * Deliverables/D3.3/id-lookup-branch/Clight/toCminor.ma (modified) * Deliverables/D3.3/id-lookup-branch/Cminor/cminorMatitaPrinter.ml (modified) * Deliverables/D3.3/id-lookup-branch/Cminor/test/search.Cminor.ma (modified) * Deliverables/D3.3/id-lookup-branch/ERTL/ERTL.ma (modified) * Deliverables/D3.3/id-lookup-branch/ERTL/ERTLToLTL.ma (modified) * Deliverables/D3.3/id-lookup-branch/ERTL/ERTLToLTLI.ma (deleted) * Deliverables/D3.3/id-lookup-branch/ERTL/build.ma (modified) * Deliverables/D3.3/id-lookup-branch/ERTL/liveness.ma (modified) * Deliverables/D3.3/id-lookup-branch/ERTL/semantics.ma (modified) * Deliverables/D3.3/id-lookup-branch/ERTL/uses.ma (modified) * Deliverables/D3.3/id-lookup-branch/LIN/JointLTLLIN.ma (deleted) * Deliverables/D3.3/id-lookup-branch/LIN/LIN.ma (modified) * Deliverables/D3.3/id-lookup-branch/LIN/LINToASM.ma (modified) * Deliverables/D3.3/id-lookup-branch/LTL/LTL.ma (modified) * Deliverables/D3.3/id-lookup-branch/LTL/LTLToLIN.ma (modified) * Deliverables/D3.3/id-lookup-branch/RTLabs/RTLabsMatitaPrinter.ml (modified) * Deliverables/D3.3/id-lookup-branch/RTLabs/test/search.RTLabs.ma (modified) * Deliverables/D3.3/id-lookup-branch/acc-matita-printers.patch (copied) * Deliverables/D3.3/id-lookup-branch/common/SmallstepExec.ma (modified) * Deliverables/D3.3/id-lookup-branch/joint (copied) * Deliverables/D3.3/id-lookup-branch/utilities/BitVectorTrieMap.ma (copied) * Deliverables/D3.3/id-lookup-branch/utilities/Colouring.ma (copied) * Deliverables/D3.3/id-lookup-branch/utilities/Fix.ma (copied) * Deliverables/D3.3/id-lookup-branch/utilities/Interference.ma (modified) * Deliverables/D3.3/id-lookup-branch/utilities/RegisterSet.ma (modified) * Deliverables/D3.3/id-lookup-branch/utilities/lists.ma (modified) Merge trunk to branch. Tue, 30 Aug 2011 16:55:12 GMT campbell [1153] * Deliverables/D3.3/id-lookup-branch (modified) * Deliverables/D3.3/id-lookup-branch/ASM (modified) * Deliverables/D3.3/id-lookup-branch/ASM/ASM.ma (modified) * Deliverables/D3.3/id-lookup-branch/ASM/I8051.ma (modified) * Deliverables/D3.3/id-lookup-branch/CHANGES (modified) * Deliverables/D3.3/id-lookup-branch/Clight/Cexec.ma (modified) * Deliverables/D3.3/id-lookup-branch/Clight/CexecSound.ma (modified) * Deliverables/D3.3/id-lookup-branch/Clight/Csem.ma (modified) * Deliverables/D3.3/id-lookup-branch/Clight/Csyntax.ma (modified) * Deliverables/D3.3/id-lookup-branch/Clight/test/insertsort.c.ma (modified) * Deliverables/D3.3/id-lookup-branch/Clight/test/search.c.ma (modified) * Deliverables/D3.3/id-lookup-branch/Clight/test/sum.c.ma (modified) * Deliverables/D3.3/id-lookup-branch/Clight/toCminor.ma (modified) * Deliverables/D3.3/id-lookup-branch/Cminor/initialisation.ma (modified) * Deliverables/D3.3/id-lookup-branch/Cminor/semantics.ma (modified) * Deliverables/D3.3/id-lookup-branch/Cminor/syntax.ma (modified) * Deliverables/D3.3/id-lookup-branch/Cminor/toRTLabs.ma (modified) * Deliverables/D3.3/id-lookup-branch/ERTL/ERTL.ma (modified) * Deliverables/D3.3/id-lookup-branch/ERTL/ERTLToLTL.ma (modified) * Deliverables/D3.3/id-lookup-branch/ERTL/ERTLToLTLI.ma (modified) * Deliverables/D3.3/id-lookup-branch/ERTL/build.ma (copied) * Deliverables/D3.3/id-lookup-branch/ERTL/liveness.ma (modified) * Deliverables/D3.3/id-lookup-branch/ERTL/semantics.ma (copied) * Deliverables/D3.3/id-lookup-branch/ERTL/spill.ma (copied) * Deliverables/D3.3/id-lookup-branch/ERTL/uses.ma (copied) * Deliverables/D3.3/id-lookup-branch/LIN/JointLTLLIN.ma (modified) * Deliverables/D3.3/id-lookup-branch/LIN/LINToASM.ma (modified) * Deliverables/D3.3/id-lookup-branch/LTL/LTLToLIN.ma (modified) * Deliverables/D3.3/id-lookup-branch/RTL/RTL.ma (modified) * Deliverables/D3.3/id-lookup-branch/RTL/RTLtoERTL.ma (modified) * Deliverables/D3.3/id-lookup-branch/RTL/semantics.ma (copied) * Deliverables/D3.3/id-lookup-branch/RTLabs/semantics.ma (modified) * Deliverables/D3.3/id-lookup-branch/RTLabs/syntax.ma (modified) * Deliverables/D3.3/id-lookup-branch/common/AST.ma (modified) * Deliverables/D3.3/id-lookup-branch/common/Errors.ma (modified) * Deliverables/D3.3/id-lookup-branch/common/Globalenvs.ma (modified) * Deliverables/D3.3/id-lookup-branch/common/Registers.ma (modified) * Deliverables/D3.3/id-lookup-branch/utilities/Interference.ma (copied) Merge trunk into branch. Mon, 29 Aug 2011 15:45:04 GMT campbell [1135] * Deliverables/D3.3/id-lookup-branch/Cminor/semantics.ma (modified) Add invariants to Cminor semantics to rule out some failures. Mon, 29 Aug 2011 15:45:03 GMT campbell [1134] * Deliverables/D3.3/id-lookup-branch/ASM/BitVectorTrie.ma (modified) * Deliverables/D3.3/id-lookup-branch/common/Identifiers.ma (modified) * Deliverables/D3.3/id-lookup-branch/utilities/option.ma (modified) Extra results for non-failing map updates. Mon, 29 Aug 2011 15:45:02 GMT campbell [1133] * Deliverables/D3.3/id-lookup-branch/utilities/deppair.ma (added) * Deliverables/D3.3/id-lookup-branch/utilities/pair.ma (added) Add missing utilities files Wed, 24 Aug 2011 15:12:10 GMT campbell [1109] * Deliverables/D3.3/id-lookup-branch (modified) * Deliverables/D3.3/id-lookup-branch/ASM (modified) * Deliverables/D3.3/id-lookup-branch/ASM/Assembly.ma (modified) * Deliverables/D3.3/id-lookup-branch/ERTL/ERTL.ma (modified) * Deliverables/D3.3/id-lookup-branch/ERTL/ERTLToLTLI.ma (modified) * Deliverables/D3.3/id-lookup-branch/ERTL/liveness.ma (modified) * Deliverables/D3.3/id-lookup-branch/LIN/JointLTLLIN.ma (modified) * Deliverables/D3.3/id-lookup-branch/RTL/RTL.ma (modified) * Deliverables/D3.3/id-lookup-branch/RTL/RTLtoERTL.ma (modified) Update branch. Wed, 10 Aug 2011 15:17:58 GMT campbell [1105] * Deliverables/D3.3/id-lookup-branch/Cminor/toRTLabs.ma (modified) * Deliverables/D3.3/id-lookup-branch/RTLabs/syntax.ma (modified) * Deliverables/D3.3/id-lookup-branch/common/Identifiers.ma (modified) * Deliverables/D3.3/id-lookup-branch/utilities/lists.ma (modified) Show that RTLabs graphs are closed on branch (i.e., all labels in ... Wed, 10 Aug 2011 15:17:55 GMT campbell [1104] * Deliverables/D3.3/id-lookup-branch/Cminor/syntax.ma (modified) * Deliverables/D3.3/id-lookup-branch/Cminor/toRTLabs.ma (modified) * Deliverables/D3.3/id-lookup-branch/common/Identifiers.ma (modified) A little more tidying. Thu, 04 Aug 2011 11:55:53 GMT campbell [1102] * Deliverables/D3.3/id-lookup-branch/Clight/toCminor.ma (modified) * Deliverables/D3.3/id-lookup-branch/Cminor/initialisation.ma (modified) * Deliverables/D3.3/id-lookup-branch/Cminor/semantics.ma (modified) * Deliverables/D3.3/id-lookup-branch/Cminor/toRTLabs.ma (modified) * Deliverables/D3.3/id-lookup-branch/common/Errors.ma (modified) * Deliverables/D3.3/id-lookup-branch/utilities/extralib.ma (modified) * Deliverables/D3.3/id-lookup-branch/utilities/lists.ma (modified) Tidy up branch Wed, 03 Aug 2011 15:18:17 GMT campbell [1101] * Deliverables/D3.3/id-lookup-branch/Cminor/initialisation.ma (modified) * Deliverables/D3.3/id-lookup-branch/Cminor/toRTLabs.ma (modified) Label preservation in Cminor initialisation and RTLabs translation ... Wed, 03 Aug 2011 15:18:15 GMT campbell [1100] * Deliverables/D3.3/id-lookup-branch/Clight/toCminor.ma (modified) Finally show that labels in generated Cminor programs are properly ... Wed, 03 Aug 2011 12:48:11 GMT campbell [1098] * Deliverables/D3.3/id-lookup-branch (modified) * Deliverables/D3.3/id-lookup-branch/ASM (modified) * Deliverables/D3.3/id-lookup-branch/ASM/I8051.ma (modified) * Deliverables/D3.3/id-lookup-branch/ASM/Util.ma (modified) * Deliverables/D3.3/id-lookup-branch/ERTL/liveness.ma (modified) Merge branch with trunk Wed, 03 Aug 2011 11:04:49 GMT campbell [1097] * Deliverables/D3.3/id-lookup-branch/Clight/toCminor.ma (modified) * Deliverables/D3.3/id-lookup-branch/Cminor/syntax.ma (modified) Checkpoint labels work on branch again. Wed, 03 Aug 2011 11:04:48 GMT campbell [1096] * Deliverables/D3.3/id-lookup-branch/Clight/toCminor.ma (modified) * Deliverables/D3.3/id-lookup-branch/Cminor/syntax.ma (modified) Checkpoint part way through adding proper C label checking to the branch. Wed, 03 Aug 2011 11:04:45 GMT campbell [1095] * Deliverables/D3.3/id-lookup-branch/Cminor/toRTLabs.ma (modified) Make add_exprs total (on branch). Thu, 28 Jul 2011 10:15:09 GMT campbell [1093] * Deliverables/D3.3/id-lookup-branch (modified) * Deliverables/D3.3/id-lookup-branch/ASM (modified) * Deliverables/D3.3/id-lookup-branch/common/Identifiers.ma (modified) Merge a bit more. Thu, 28 Jul 2011 10:14:17 GMT campbell [1091] * Deliverables/D3.3/id-lookup-branch (modified) * Deliverables/D3.3/id-lookup-branch/ASM (modified) * Deliverables/D3.3/id-lookup-branch/ASM/I8051.ma (modified) * Deliverables/D3.3/id-lookup-branch/ERTL/ERTLToLTL.ma (modified) * Deliverables/D3.3/id-lookup-branch/ERTL/liveness.ma (copied) * Deliverables/D3.3/id-lookup-branch/LIN/JointLTLLIN.ma (modified) * Deliverables/D3.3/id-lookup-branch/LTL/LTL.ma (modified) * Deliverables/D3.3/id-lookup-branch/RTL/RTL.ma (modified) * Deliverables/D3.3/id-lookup-branch/RTL/RTLinterpret.ma (copied) Merge trunk into id-lookup-branch Mon, 25 Jul 2011 12:58:10 GMT campbell [1087] * Deliverables/D3.3/id-lookup-branch/Clight/toCminor.ma (modified) * Deliverables/D3.3/id-lookup-branch/Cminor/initialisation.ma (modified) * Deliverables/D3.3/id-lookup-branch/Cminor/syntax.ma (modified) * Deliverables/D3.3/id-lookup-branch/Cminor/toRTLabs.ma (modified) * Deliverables/D3.3/id-lookup-branch/utilities/lists.ma (modified) Experimental branch where lookups of local variables in Cminor code ... Mon, 25 Jul 2011 10:41:36 GMT campbell [1086] * Deliverables/D3.3/id-lookup-branch (copied) Branch for experimenting with identifier binding guarantees. Tue, 24 May 2011 12:27:43 GMT campbell [830] * Deliverables/D3.3/Cminor-experiment/initialisation.ma (moved) * Deliverables/D3.3/Cminor-experiment/toRTLabs.ma (moved) Move files that accidentally ended up in the root of the repository. Fri, 06 May 2011 09:45:27 GMT campbell [787] * Deliverables/D3.3/Cminor-experiment/semantics.ma (modified) * Deliverables/D3.3/Cminor-experiment/syntax.ma (modified) Update experimental version of Cminor semantics. Fri, 15 Apr 2011 14:26:23 GMT campbell [755] * Deliverables/D3.3 (added) * Deliverables/D3.3/Cminor-experiment (added) * Deliverables/D3.3/Cminor-experiment/README (added) * Deliverables/D3.3/Cminor-experiment/be.agda (added) * Deliverables/D3.3/Cminor-experiment/semantics.ma (copied) * Deliverables/D3.3/Cminor-experiment/syntax.ma (copied) * Deliverables/D3.3/Cminor-experiment/test (copied) * Deliverables/D3.3/Cminor-experiment/test/search.ma (modified) An experimental branch of the Cminor semantics.