# # ChangeLog for src/joint/Traces.ma # # Generated by Trac 1.2 # Mar 1, 2021, 3:33:58 PM Thu, 21 Feb 2013 17:03:46 GMT tranquil [2688] * src/ASM/Arithmetic.ma (modified) * src/ERTLptr/ERTLtoERTLptr.ma (modified) * src/joint/Joint.ma (modified) * src/joint/Traces.ma (modified) * src/joint/TranslateUtils.ma (modified) * src/joint/joint_semantics.ma (modified) * src/joint/semanticsUtils.ma (modified) * src/joint/semantics_blocks.ma (modified) * in Arithmeticcs.ma: commented include that breaks script in latest ... Tue, 19 Feb 2013 17:48:32 GMT tranquil [2681] * src/ERTL/ERTLToLTL.ma (modified) * src/ERTL/liveness.ma (modified) * src/ERTLptr/ERTLtoERTLptr.ma (modified) * src/RTL/RTL.ma (modified) * src/RTL/RTLToERTL.ma (modified) * src/joint/Joint.ma (modified) * src/joint/Traces.ma (modified) * src/joint/TranslateUtils.ma (modified) * src/joint/semanticsUtils.ma (modified) * improvements to the graph translation function * fixed passes up to LTL 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, 07 Feb 2013 14:24:50 GMT piccolo [2642] * src/joint/Traces.ma (modified) fixed joint/Traces after having posed block 0 to be Code Thu, 07 Feb 2013 13:15:51 GMT piccolo [2638] * src/ERTLptr/ERTLtoERTLptrOK.ma (modified) * src/joint/Traces.ma (modified) * src/joint/joint_semantics.ma (modified) Back-end fixes for last Garnier's commit that removes the regions ... Tue, 05 Feb 2013 12:36:31 GMT sacerdot [2601] * extracted (added) * extracted/PROBLEMS (added) * extracted/aSM.ml (added) * extracted/aSM.mli (added) * extracted/aSMCosts.ml (added) * extracted/aSMCosts.mli (added) * extracted/aSMCostsSplit.ml (added) * extracted/aSMCostsSplit.mli (added) * extracted/aST.ml (added) * extracted/aST.mli (added) * extracted/abstractStatus.ml (added) * extracted/abstractStatus.mli (added) * extracted/arithmetic.ml (added) * extracted/arithmetic.mli (added) * extracted/bitVector.ml (added) * extracted/bitVector.mli (added) * extracted/bitVectorTrie.ml (added) * extracted/bitVectorTrie.mli (added) * extracted/bitVectorZ.ml (added) * extracted/bitVectorZ.mli (added) * extracted/bool.ml (added) * extracted/bool.mli (added) * extracted/byteValues.ml (added) * extracted/byteValues.mli (added) * extracted/casts.ml (added) * extracted/casts.mli (added) * extracted/cexec.ml (added) * extracted/cexec.mli (added) * extracted/cexecInd.ml (added) * extracted/cexecInd.mli (added) * extracted/cexecSound.ml (added) * extracted/cexecSound.mli (added) * extracted/char.ml (added) * extracted/char.mli (added) * extracted/classifyOp.ml (added) * extracted/classifyOp.mli (added) * extracted/cminor_syntax.ml (added) * extracted/cminor_syntax.mli (added) * extracted/compiler.ml (added) * extracted/compiler.mli (added) * extracted/coqlib.ml (added) * extracted/coqlib.mli (added) * extracted/core_notation.ml (added) * extracted/core_notation.mli (added) * extracted/costLabel.ml (added) * extracted/costLabel.mli (added) * extracted/csem.ml (added) * extracted/csem.mli (added) * extracted/csyntax.ml (added) * extracted/csyntax.mli (added) * extracted/deqsets.ml (added) * extracted/deqsets.mli (added) * extracted/div_and_mod.ml (added) * extracted/div_and_mod.mli (added) * extracted/division.ml (added) * extracted/division.mli (added) * extracted/errors.ml (added) * extracted/errors.mli (added) * extracted/events.ml (added) * extracted/events.mli (added) * extracted/extra_bool.ml (added) * extracted/extra_bool.mli (added) * extracted/extralib.ml (added) * extracted/extralib.mli (added) * extracted/extranat.ml (added) * extracted/extranat.mli (added) * extracted/fetch.ml (added) * extracted/fetch.mli (added) * extracted/floats.ml (added) * extracted/floats.mli (added) * extracted/foldStuff.ml (added) * extracted/foldStuff.mli (added) * extracted/fresh.ml (added) * extracted/fresh.mli (added) * extracted/frontEndMem.ml (added) * extracted/frontEndMem.mli (added) * extracted/frontEndOps.ml (added) * extracted/frontEndOps.mli (added) * extracted/frontEndVal.ml (added) * extracted/frontEndVal.mli (added) * extracted/frontend_misc.ml (added) * extracted/frontend_misc.mli (added) * extracted/genMem.ml (added) * extracted/genMem.mli (added) * extracted/globalenvs.ml (added) * extracted/globalenvs.mli (added) * extracted/graphs.ml (added) * extracted/graphs.mli (added) * extracted/hide.ml (added) * extracted/hide.mli (added) * extracted/hints_declaration.ml (added) * extracted/hints_declaration.mli (added) * extracted/iO.ml (added) * extracted/iO.mli (added) * extracted/iOMonad.ml (added) * extracted/iOMonad.mli (added) * extracted/identifiers.ml (added) * extracted/identifiers.mli (added) * extracted/initialisation.ml (added) * extracted/initialisation.mli (added) * extracted/integers.ml (added) * extracted/integers.mli (added) * extracted/interpret.ml (added) * extracted/interpret.mli (added) * extracted/jmeq.ml (added) * extracted/jmeq.mli (added) * extracted/label.ml (added) * extracted/label.mli (added) * extracted/labelledObjects.ml (added) * extracted/labelledObjects.mli (added) * extracted/list.ml (added) * extracted/list.mli (added) * extracted/listb.ml (added) * extracted/listb.mli (added) * extracted/lists.ml (added) * extracted/lists.mli (added) * extracted/logic.ml (added) * extracted/logic.mli (added) * extracted/memProperties.ml (added) * extracted/memProperties.mli (added) * extracted/memoryInjections.ml (added) * extracted/memoryInjections.mli (added) * extracted/monad.ml (added) * extracted/monad.mli (added) * extracted/nat.ml (added) * extracted/nat.mli (added) * extracted/option.ml (added) * extracted/option.mli (added) * extracted/order.ml (added) * extracted/order.mli (added) * extracted/pointers.ml (added) * extracted/pointers.mli (added) * extracted/positive.ml (added) * extracted/positive.mli (added) * extracted/positiveMap.ml (added) * extracted/positiveMap.mli (added) * extracted/preIdentifiers.ml (added) * extracted/preIdentifiers.mli (added) * extracted/preamble.ml (added) * extracted/proper.ml (added) * extracted/proper.mli (added) * extracted/pts.ml (added) * extracted/pts.mli (added) * extracted/rTLabs_syntax.ml (added) * extracted/rTLabs_syntax.mli (added) * extracted/registers.ml (added) * extracted/registers.mli (added) * extracted/relations.ml (added) * extracted/relations.mli (added) * extracted/russell.ml (added) * extracted/russell.mli (added) * extracted/setoids.ml (added) * extracted/setoids.mli (added) * extracted/sets.ml (added) * extracted/sets.mli (added) * extracted/simplifyCasts.ml (added) * extracted/simplifyCasts.mli (added) * extracted/smallstep.ml (added) * extracted/smallstep.mli (added) * extracted/smallstepExec.ml (added) * extracted/smallstepExec.mli (added) * extracted/star.ml (added) * extracted/star.mli (added) * extracted/status.ml (added) * extracted/status.mli (added) * extracted/statusProofs.ml (added) * extracted/statusProofs.mli (added) * extracted/string.ml (added) * extracted/string.mli (added) * extracted/structuredTraces.ml (added) * extracted/structuredTraces.mli (added) * extracted/switchRemoval.ml (added) * extracted/switchRemoval.mli (added) * extracted/toCminor.ml (added) * extracted/toCminor.mli (added) * extracted/toRTLabs.ml (added) * extracted/toRTLabs.mli (added) * extracted/typeComparison.ml (added) * extracted/typeComparison.mli (added) * extracted/types.ml (added) * extracted/types.mli (added) * extracted/util.ml (added) * extracted/util.mli (added) * extracted/utilBranch.ml (added) * extracted/utilBranch.mli (added) * extracted/values.ml (added) * extracted/values.mli (added) * extracted/vector.ml (added) * extracted/vector.mli (added) * extracted/z.ml (added) * extracted/z.mli (added) * src/ASM/BitVector.ma (modified) * src/Clight/Clight_abstract.ma (moved) * src/Clight/toCminor.ma (modified) * src/Clight/toCminorCorrectness.ma (modified) * src/Clight/toCminorCorrectnessExpr.ma (modified) * src/Clight/toCminorOps.ma (modified) * src/Cminor/Cminor_abstract.ma (moved) * src/Cminor/Cminor_semantics.ma (moved) * src/Cminor/Cminor_syntax.ma (moved) * src/Cminor/initialisation.ma (modified) * src/Cminor/toRTLabs.ma (modified) * src/Cminor/toRTLabsCorrectness.ma (modified) * src/ERTL/ERTL_semantics.ma (moved) * src/ERTLptr/ERTLptr_semantics.ma (moved) * src/ERTLptr/ERTLtoERTLptrOK.ma (modified) * src/LIN/LIN_semantics.ma (moved) * src/LTL/LTL_semantics.ma (moved) * src/RTL/RTL_semantics.ma (moved) * src/RTLabs/CostCheck.ma (modified) * src/RTLabs/CostInj.ma (modified) * src/RTLabs/CostSpec.ma (modified) * src/RTLabs/MeasurableTraces.ma (modified) * src/RTLabs/RTLabsToRTL.ma (modified) * src/RTLabs/RTLabs_abstract.ma (moved) * src/RTLabs/RTLabs_semantics.ma (moved) * src/RTLabs/RTLabs_syntax.ma (moved) * src/RTLabs/RTLabs_traces.ma (moved) * src/RTLabs/debug.ma (modified) * src/RTLabs/import.ma (modified) * src/common/Globalenvs.ma (modified) * src/joint/Traces.ma (modified) * src/joint/joint_semantics.ma (moved) * src/joint/semanticsUtils.ma (modified) * src/joint/stacksize.ma (modified) * src/utilities/extra_bool.ma (moved) Extraction to ocaml is now working, with a couple of bugs left. One ... Thu, 24 Jan 2013 18:52:38 GMT piccolo [2590] * src/ERTL/semantics.ma (modified) * src/ERTLptr/ERTLtoERTLptrOK.ma (modified) * src/ERTLptr/semantics.ma (modified) * src/common/ExtraMonads.ma (modified) * src/common/PositiveMap.ma (modified) * src/common/extraGlobalenvs.ma (modified) * src/joint/Traces.ma (modified) * src/joint/semantics.ma (modified) added monad machineary for ERTL to ERTLptr translation ... Wed, 19 Dec 2012 09:38:43 GMT piccolo [2562] * src/joint/Joint.ma (modified) * src/joint/Traces.ma (modified) * src/joint/linearise.ma (modified) * src/joint/semantics.ma (modified) linearise modified Tue, 18 Dec 2012 16:03:29 GMT tranquil [2561] * src/joint/Joint.ma (modified) * src/joint/Traces.ma (modified) * src/joint/semantics.ma (modified) * moved CALL as different case than joint_seq: lots of broken code ... Fri, 14 Dec 2012 13:54:06 GMT tranquil [2556] * src/joint/Traces.ma (modified) * src/joint/lineariseProof.ma (modified) * src/joint/semantics.ma (modified) in joint semantics and traces: added a last popped calling address to ... Wed, 12 Dec 2012 13:43:03 GMT tranquil [2553] * src/common/StatusSimulation.ma (modified) * src/common/StructuredTraces.ma (modified) * src/joint/Traces.ma (modified) * src/joint/lineariseProof.ma (modified) as_classify changed to a partial function added a status for tailcalls Thu, 06 Dec 2012 12:39:23 GMT tranquil [2538] * src/joint/Traces.ma (modified) fixed Traces.ma after changes in joint/semantics.ma Tue, 04 Dec 2012 17:16:25 GMT tranquil [2529] * src/joint/Traces.ma (modified) * src/joint/linearise.ma (modified) * src/joint/lineariseProof.ma (modified) * src/joint/semantics.ma (modified) * src/joint/semanticsUtils.ma (modified) * src/joint/semantics_blocks.ma (modified) * src/utilities/monad.ma (modified) rewritten function handling in joint swapped call_rel with ret_rel ... Thu, 22 Nov 2012 17:40:31 GMT piccolo [2484] * src/joint/Traces.ma (modified) * src/joint/lineariseProof.ma (modified) * src/joint/semantics.ma (modified) fixed Traces and semantics added commutation record (not yet ... Tue, 20 Nov 2012 17:40:08 GMT piccolo [2481] * src/joint/Traces.ma (modified) * src/joint/linearise.ma (modified) * src/joint/lineariseProof.ma (modified) * src/joint/semantics.ma (modified) corrected some inconsistencies fixed some of lineariseProof Tue, 20 Nov 2012 12:41:58 GMT tranquil [2477] * src/common/StatusSimulation.ma (modified) * src/joint/Traces.ma (modified) status_simulation reformulated definition of joint_classify split up ... Fri, 16 Nov 2012 17:59:24 GMT tranquil [2473] * src/common/extraGlobalenvs.ma (added) * src/joint/Traces.ma (modified) * src/joint/linearise.ma (modified) * src/joint/semantics.ma (modified) put some generic stuff we need in the back end in extraGlobalenvs ... Thu, 15 Nov 2012 18:06:45 GMT tranquil [2470] * src/common/ByteValues.ma (modified) * src/joint/Traces.ma (modified) * src/joint/semantics.ma (modified) * src/joint/semanticsUtils.ma (modified) completely separated program counters from code pointers in joint ... Tue, 13 Nov 2012 10:30:23 GMT tranquil [2457] * src/common/StatusSimulation.ma (modified) * src/joint/Joint.ma (modified) * src/joint/Traces.ma (modified) * src/joint/semantics.ma (modified) * src/joint/semanticsUtils.ma (moved) rewritten function handling in joint swapped call_rel with ret_rel ... Thu, 08 Nov 2012 13:27:54 GMT tranquil [2443] * src/ERTL/ERTLToLTL.ma (modified) * src/LIN/LINToASM.ma (modified) * src/LIN/joint_LTL_LIN_semantics.ma (modified) * src/LIN/semantics.ma (modified) * src/LTL/semantics.ma (modified) * src/common/ByteValues.ma (modified) * src/joint/SemanticUtils.ma (modified) * src/joint/Traces.ma (modified) * src/joint/TranslateUtils.ma (modified) * src/joint/lineariseProof.ma (modified) * src/joint/semantics.ma (modified) * src/utilities/deqsets.ma (modified) * src/utilities/lists.ma (modified) changed joint's stack pointer and internal stack Wed, 07 Nov 2012 17:12:20 GMT piccolo [2442] * src/joint/Traces.ma (modified) * src/joint/lineariseProof.ma (added) Traces repaired. (By Paolo) Statement of lineariseProof in place. Tue, 30 Oct 2012 15:23:09 GMT tranquil [2422] * src/joint/Joint.ma (modified) * src/joint/SemanticUtils.ma (modified) * src/joint/Traces.ma (modified) * src/joint/blocks.ma (modified) * src/joint/linearise.ma (modified) * src/joint/semantics.ma (modified) * src/joint/semantics_blocks.ma (modified) adapted joint to cl_call f 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, 16 Jul 2012 14:59:09 GMT tranquil [2186] * src/RTL/RTL_paolo.ma (modified) * src/common/StructuredTraces.ma (modified) * src/joint/Joint_paolo.ma (modified) * src/joint/Traces.ma (moved) * src/joint/blocks.ma (modified) * src/joint/semantics_blocks.ma (modified) * src/joint/semantics_paolo.ma (modified) updated joint semantics Mon, 21 May 2012 17:04:21 GMT tranquil [1976] * src/ASM/CostsProof.ma (modified) * src/common/IOMonad.ma (modified) * src/common/StructuredTraces.ma (modified) * src/joint/Joint_paolo.ma (modified) * src/joint/as_semantics.ma (added) * src/joint/semantics_paolo.ma (modified) * src/utilities/bind_new.ma (added) * src/utilities/monad.ma (modified) * src/utilities/option.ma (modified) * src/utilities/permutations.ma (added) * src/utilities/state.ma (modified) * monads: just changed some defs, which had to be propagated in some ...