# # ChangeLog for src/joint/SemanticUtils.ma # # Generated by Trac 1.2 # Apr 15, 2021, 7:33:01 AM Thu, 12 Jul 2012 11:28:28 GMT campbell [2176] * src/Clight/Cexec.ma (modified) * src/Clight/CexecComplete.ma (modified) * src/Clight/CexecSound.ma (modified) * src/Clight/ClassifyOp.ma (modified) * src/Clight/Csem.ma (modified) * src/Clight/Csyntax.ma (modified) * src/Clight/SimplifyCasts.ma (modified) * src/Clight/TypeComparison.ma (modified) * src/Clight/clightPrintMatita.ml (modified) * src/Clight/labelSimulation.ma (modified) * src/Clight/test/duff.c.ma (modified) * src/Clight/test/insertsort.c.ma (modified) * src/Clight/test/memorymodel.ma (modified) * src/Clight/test/null-op.c.ma (modified) * src/Clight/test/search.c.ma (modified) * src/Clight/test/sum.c.ma (modified) * src/Clight/toCminor.ma (modified) * src/Cminor/initialisation.ma (modified) * src/Cminor/semantics.ma (modified) * src/Cminor/syntax.ma (modified) * src/Cminor/toRTLabs.ma (modified) * src/RTL/semantics.ma (modified) * src/RTLabs/RTLabsToRTL.ma (modified) * src/RTLabs/semantics.ma (modified) * src/common/AST.ma (modified) * src/common/Animation.ma (modified) * src/common/ByteValues.ma (modified) * src/common/FrontEndOps.ma (modified) * src/common/FrontEndVal.ma (modified) * src/common/GenMem.ma (modified) * src/common/Globalenvs.ma (modified) * src/common/IO.ma (modified) * src/common/Pointers.ma (modified) * src/common/Values.ma (modified) * src/joint/BEMem.ma (modified) * src/joint/SemanticUtils.ma (modified) * src/joint/semantics.ma (modified) Remove memory spaces other than XData and Code; simplify pointers as ... 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 ... Sat, 22 Oct 2011 02:26:01 GMT sacerdot [1452] * src/joint/SemanticUtils.ma (modified) Bug fixed: labels MUST be represented as pointers whose block is the ... Sat, 22 Oct 2011 02:18:11 GMT sacerdot [1451] * src/ERTL/semantics.ma (modified) * src/LIN/joint_LTL_LIN_semantics.ma (modified) * src/LIN/semantics.ma (modified) * src/LTL/semantics.ma (modified) * src/RTL/semantics.ma (modified) * src/TODO (modified) * src/joint/SemanticUtils.ma (modified) * src/joint/semantics.ma (modified) * src/utilities/lists.ma (modified) 1. All axioms in LIN/semantics.ma closed 2. succ_pc and ... 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 ... Wed, 19 Oct 2011 09:30:24 GMT sacerdot [1408] * src/ERTL/semantics.ma (modified) * src/LIN/joint_LTL_LIN_semantics.ma (modified) * src/LIN/semantics.ma (modified) * src/RTL/semantics.ma (modified) * src/RTLabs/RTLabsToRTL.ma (modified) * src/joint/BEGlobalenvs.ma (added) * src/joint/SemanticUtils.ma (modified) * src/joint/semantics.ma (modified) 1. Added joint/BEGlobalenvs that is a modification of ... Mon, 17 Oct 2011 15:41:44 GMT sacerdot [1395] * src/common/GenMem.ma (modified) * src/common/Globalenvs.ma (modified) * src/joint/BEMem.ma (modified) * src/joint/BEValues.ma (modified) * src/joint/SemanticUtils.ma (modified) * src/joint/semantics.ma (modified) 1) New versions of pointer_of_beval/beval_of_pointer with a stricter ... Sun, 16 Oct 2011 23:40:13 GMT sacerdot [1385] * 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. fetch_result and pop_frame now takes the genv in input 2. ... Sun, 16 Oct 2011 17:42:25 GMT sacerdot [1384] * 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) * fetch_ra taken out of pop_frame again since it is used uniformly ... Fri, 14 Oct 2011 22:13:23 GMT sacerdot [1383] * src/LIN/joint_LTL_LIN_semantics.ma (modified) * src/LIN/semantics.ma (modified) * src/LTL/semantics.ma (modified) * src/joint/SemanticUtils.ma (modified) * src/joint/semantics.ma (modified) Potential bug fixed and bug found: the way pointers and labels are ... Fri, 14 Oct 2011 20:50:56 GMT sacerdot [1382] * src/LIN/joint_LTL_LIN_semantics.ma (modified) * src/LIN/semantics.ma (modified) * src/joint/SemanticUtils.ma (modified) * src/joint/semantics.ma (modified) - succ_pc generalized to return a res (necessary for LIN semantics) ... Tue, 11 Oct 2011 16:00:03 GMT sacerdot [1359] * src/ERTL/semantics.ma (modified) * src/LIN/semantics.ma (modified) * src/LTL/semantics.ma (modified) * src/RTL/semantics.ma (modified) * src/joint/BEValues.ma (modified) * src/joint/SemanticUtils.ma (modified) * src/joint/semantics.ma (modified) 1. more work on the RTL semantics 2. changes to joint/semantics to ... Fri, 07 Oct 2011 16:19:41 GMT sacerdot [1329] * src/ERTL/semantics.ma (modified) * src/joint/BEMem.ma (modified) * src/joint/SemanticUtils.ma (modified) * src/joint/semantics.ma (modified) 1. Definition of addresses moved to BEMem 2. Basic functions on ... Wed, 05 Oct 2011 21:36:03 GMT sacerdot [1302] * src/ERTL/semantics.ma (modified) * src/joint/SemanticUtils.ma (modified) ERTL/semantics.ma ported to joint/SemanticUtils (in progress) Wed, 05 Oct 2011 20:43:26 GMT sacerdot [1300] * src/RTL/semantics.ma (modified) * src/joint/SemanticUtils.ma (modified) More (graph) axioms implemented. Look at the comments marked with XXX ... Wed, 05 Oct 2011 19:53:29 GMT sacerdot [1299] * src/RTL/semantics.ma (modified) * src/joint/SemanticUtils.ma (added) Functions from RTL/semantics.ma generalized to work on every graph ...