# # ChangeLog for src/ASM/I8051.ma # # Generated by Trac 1.2 # Feb 28, 2021, 3:17:43 PM 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 ... 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 ... Mon, 30 Jul 2012 11:05:55 GMT tranquil [2275] * src/ASM/I8051.ma (modified) * src/common/ByteValues.ma (modified) * src/common/ByteValues_paolo.ma (copied) * moved around some code (I8051.ma does not depend on ByteValues.ma ... Thu, 24 May 2012 08:22:52 GMT campbell [1987] * src/ASM/I8051.ma (modified) * src/common/ByteValues.ma (moved) * src/common/FrontEndVal.ma (modified) * src/joint/BEMem.ma (modified) Move BEValues to common to reflect their use in the memory model for ... 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 ... Tue, 13 Dec 2011 12:41:08 GMT sacerdot [1600] * src/ASM/BitVectorTrie.ma (modified) * src/ASM/Erase.ma (modified) * src/ASM/Fetch.ma (modified) * src/ASM/FoldStuff.ma (modified) * src/ASM/I8051.ma (modified) * src/ASM/Interpret.ma (modified) * src/ASM/JMCoercions.ma (deleted) * src/ASM/Status.ma (modified) * src/ASM/Util.ma (modified) * src/utilities/Compare.ma (deleted) * src/utilities/Coqlib.ma (modified) * src/utilities/deppair.ma (deleted) * src/utilities/lists.ma (deleted) * src/utilities/option.ma (deleted) * src/utilities/sigma.ma (deleted) utilities and ASM ported to the new standard library 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 ... Wed, 19 Oct 2011 14:43:49 GMT sacerdot [1416] * src/ASM/I8051.ma (modified) * src/joint/SemanticUtils.ma (modified) Maps from hardware registers to beval now implemented in ASM/I8051 ... Wed, 19 Oct 2011 14:22:52 GMT sacerdot [1415] * src/ASM/I8051.ma (modified) * src/ASM/I8051bis.ma (added) * src/ERTL/semantics.ma (modified) * src/LIN/joint_LTL_LIN_semantics.ma (modified) * src/RTL/semantics.ma (modified) * src/joint/SemanticUtils.ma (modified) * src/joint/semantics.ma (modified) 1. hwreg_store/retrieve no longer returns a res (but it is still ... Tue, 06 Sep 2011 13:49:31 GMT mulligan [1193] * src/ASM/I8051.ma (modified) * src/ASM/Util.ma (modified) * src/utilities/Colouring.ma (modified) * src/utilities/Interference.ma (modified) * src/utilities/RegisterSet.ma (modified) work on colouring algorithm halted as it can be axiomatised. now ... Mon, 05 Sep 2011 15:13:49 GMT mulligan [1187] * src/ASM/I8051.ma (modified) * src/ERTL/build.ma (modified) fixed build.ma Tue, 30 Aug 2011 14:02:37 GMT mulligan [1145] * src/ASM/I8051.ma (modified) * src/utilities/Interference.ma (modified) changed naming in i8051 of classes of registers to make them consistent Fri, 26 Aug 2011 17:38:59 GMT sacerdot [1119] * src/ASM/I8051.ma (modified) Type for evaluation of opaccs fixed (maybe wrongly: should it return ... Thu, 28 Jul 2011 15:26:06 GMT mulligan [1094] * src/ASM/I8051.ma (modified) * src/ASM/Util.ma (modified) * src/ERTL/liveness.ma (modified) some changes from today to do with liveness analyses 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 Mon, 18 Jul 2011 15:21:14 GMT mulligan [1075] * src/ASM/I8051.ma (modified) * src/ASM/Util.ma (modified) * src/RTL/RTLtoERTL.ma (modified) * src/utilities/RegisterSet.ma (modified) nearly completed rtl -> ertl pass removing all option types with dep. ... Fri, 15 Jul 2011 12:40:40 GMT mulligan [1071] * src/ASM/I8051.ma (modified) * src/ASM/Util.ma (modified) * src/ERTL/ERTL.ma (modified) * src/RTL/RTL.ma (modified) * src/RTL/RTLtoERTL.ma (modified) * src/RTLabs/RTLAbstoRTL.ma (modified) * src/RTLabs/syntax.ma (modified) changes the specific form that the added proofs take to use None, not ... Wed, 13 Jul 2011 15:12:10 GMT mulligan [1066] * src/ASM/I8051.ma (modified) * src/RTL/RTL.ma (modified) * src/RTLabs/RTLAbstoRTL.ma (modified) * src/utilities/Compare.ma (modified) changes from today Fri, 08 Jul 2011 10:17:14 GMT mulligan [1060] * src/ASM/I8051.ma (modified) * src/ASM/Util.ma (modified) * src/RTL/RTL.ma (modified) * src/RTLabs/RTLAbstoRTL.ma (modified) * src/common/AST.ma (modified) work from this morning and yesterday Wed, 27 Apr 2011 15:25:26 GMT mulligan [777] * src/ASM/I8051.ma (modified) * src/ASM/RegisterSet.ma (added) * src/ASM/Util.ma (modified) * src/ERTL/ERTL.ma (modified) * src/ERTL/Uses.ma (modified) * src/RTL/RTLtoERTL.ma (modified) * src/common/Registers.ma (modified) Lots of work on RTL to ERTL pass from today. 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, 08 Apr 2011 09:51:38 GMT mulligan [746] * src/ASM/I8051.ma (modified) * src/ASM/Util.ma (modified) * src/ERTL/Liveness.ma (modified) * src/ERTL/Uses.ma (modified) * src/ERTL/VariableSet.ma (added) * src/common/Graphs.ma (modified) * src/utilities/BitVectorTrieSet.ma (modified) Changes to bitvectortrieset: equality on sets. Added new file for ... Wed, 30 Mar 2011 12:03:05 GMT campbell [724] * src/ASM/Arithmetic.ma (modified) * src/ASM/BitVector.ma (modified) * src/ASM/I8051.ma (modified) More tractable version of bitvector_of_nat / nat_of_bitvector. 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.