# # ChangeLog for extracted/graphs.mli # # Generated by Trac 1.2 # Jan 23, 2021, 4:32:18 PM Sat, 23 Feb 2013 00:16:55 GMT sacerdot [2717] * extracted/aSM.ml (modified) * extracted/aSM.mli (modified) * extracted/aSMCosts.ml (modified) * extracted/aSMCosts.mli (modified) * extracted/aSMCostsSplit.ml (modified) * extracted/aSMCostsSplit.mli (modified) * extracted/aST.ml (modified) * extracted/aST.mli (modified) * extracted/abstractStatus.ml (modified) * extracted/abstractStatus.mli (modified) * extracted/arithmetic.ml (modified) * extracted/arithmetic.mli (modified) * extracted/assembly.ml (added) * extracted/assembly.mli (added) * extracted/assocList.ml (added) * extracted/assocList.mli (added) * extracted/backEndOps.ml (added) * extracted/backEndOps.mli (added) * extracted/bindLists.ml (added) * extracted/bindLists.mli (added) * extracted/bind_new.ml (added) * extracted/bind_new.mli (added) * extracted/bitVectorTrie.ml (modified) * extracted/bitVectorTrieSet.ml (added) * extracted/bitVectorTrieSet.mli (added) * extracted/bitVectorZ.ml (modified) * extracted/bitVectorZ.mli (modified) * extracted/blocks.ml (added) * extracted/blocks.mli (added) * extracted/byteValues.ml (modified) * extracted/byteValues.mli (modified) * extracted/casts.ml (modified) * extracted/casts.mli (modified) * extracted/cexec.ml (modified) * extracted/cexec.mli (modified) * extracted/cexecInd.ml (modified) * extracted/cexecInd.mli (modified) * extracted/cexecSound.ml (modified) * extracted/cexecSound.mli (modified) * extracted/classifyOp.ml (modified) * extracted/classifyOp.mli (modified) * extracted/cminor_syntax.ml (modified) * extracted/cminor_syntax.mli (modified) * extracted/compiler.ml (modified) * extracted/compiler.mli (modified) * extracted/costLabel.ml (modified) * extracted/costLabel.mli (modified) * extracted/csem.ml (modified) * extracted/csem.mli (modified) * extracted/csyntax.ml (modified) * extracted/csyntax.mli (modified) * extracted/deqsets.ml (modified) * extracted/deqsets_extras.ml (added) * extracted/deqsets_extras.mli (added) * extracted/division.ml (modified) * extracted/eRTL.ml (added) * extracted/eRTL.mli (added) * extracted/eRTLToERTLptr.ml (added) * extracted/eRTLToERTLptr.mli (added) * extracted/eRTLptr.ml (added) * extracted/eRTLptr.mli (added) * extracted/eRTLptrToLTL.ml (added) * extracted/eRTLptrToLTL.mli (added) * extracted/errorMessages.ml (modified) * extracted/errorMessages.mli (modified) * extracted/errors.ml (modified) * extracted/events.ml (modified) * extracted/events.mli (modified) * extracted/exp.ml (added) * extracted/exp.mli (added) * extracted/fetch.ml (modified) * extracted/fetch.mli (modified) * extracted/fixpoints.ml (added) * extracted/fixpoints.mli (added) * extracted/fresh.ml (modified) * extracted/fresh.mli (modified) * extracted/frontEndMem.ml (modified) * extracted/frontEndMem.mli (modified) * extracted/frontEndOps.ml (modified) * extracted/frontEndOps.mli (modified) * extracted/frontEndVal.ml (modified) * extracted/frontEndVal.mli (modified) * extracted/frontend_misc.ml (modified) * extracted/frontend_misc.mli (modified) * extracted/genMem.ml (modified) * extracted/genMem.mli (modified) * extracted/globalenvs.ml (modified) * extracted/globalenvs.mli (modified) * extracted/graphs.ml (modified) * extracted/graphs.mli (modified) * extracted/i8051.ml (added) * extracted/i8051.mli (added) * extracted/iO.ml (modified) * extracted/iO.mli (modified) * extracted/iOMonad.ml (modified) * extracted/identifiers.ml (modified) * extracted/initialisation.ml (modified) * extracted/initialisation.mli (modified) * extracted/integers.ml (modified) * extracted/integers.mli (modified) * extracted/interference.ml (added) * extracted/interference.mli (added) * extracted/interpret.ml (modified) * extracted/interpret.mli (modified) * extracted/joint.ml (added) * extracted/joint.mli (added) * extracted/joint_LTL_LIN.ml (added) * extracted/joint_LTL_LIN.mli (added) * extracted/lIN.ml (added) * extracted/lIN.mli (added) * extracted/lINToASM.ml (added) * extracted/lINToASM.mli (added) * extracted/lTL.ml (added) * extracted/lTL.mli (added) * extracted/lTLToLIN.ml (added) * extracted/lTLToLIN.mli (added) * extracted/label.ml (modified) * extracted/label.mli (modified) * extracted/linearise.ml (added) * extracted/linearise.mli (added) * extracted/liveness.ml (added) * extracted/liveness.mli (added) * extracted/memProperties.ml (modified) * extracted/memProperties.mli (modified) * extracted/memoryInjections.ml (modified) * extracted/memoryInjections.mli (modified) * extracted/pointers.ml (modified) * extracted/pointers.mli (modified) * extracted/policy.ml (added) * extracted/policy.mli (added) * extracted/policyFront.ml (added) * extracted/policyFront.mli (added) * extracted/policyStep.ml (added) * extracted/policyStep.mli (added) * extracted/positiveMap.ml (modified) * extracted/positiveMap.mli (modified) * extracted/preIdentifiers.ml (modified) * extracted/rTL.ml (added) * extracted/rTL.mli (added) * extracted/rTLToERTL.ml (added) * extracted/rTLToERTL.mli (added) * extracted/rTLabsToRTL.ml (added) * extracted/rTLabsToRTL.mli (added) * extracted/rTLabs_syntax.ml (modified) * extracted/rTLabs_syntax.mli (modified) * extracted/registerSet.ml (added) * extracted/registerSet.mli (added) * extracted/set_adt.ml (added) * extracted/set_adt.mli (added) * extracted/simplifyCasts.ml (modified) * extracted/simplifyCasts.mli (modified) * extracted/smallstep.ml (modified) * extracted/smallstep.mli (modified) * extracted/smallstepExec.ml (modified) * extracted/smallstepExec.mli (modified) * extracted/state.ml (added) * extracted/state.mli (added) * extracted/status.ml (modified) * extracted/status.mli (modified) * extracted/statusProofs.ml (modified) * extracted/statusProofs.mli (modified) * extracted/structuredTraces.ml (modified) * extracted/structuredTraces.mli (modified) * extracted/switchRemoval.ml (modified) * extracted/switchRemoval.mli (modified) * extracted/toCminor.ml (modified) * extracted/toCminor.mli (modified) * extracted/toRTLabs.ml (modified) * extracted/toRTLabs.mli (modified) * extracted/translateUtils.ml (added) * extracted/translateUtils.mli (added) * extracted/typeComparison.ml (modified) * extracted/typeComparison.mli (modified) * extracted/util.ml (modified) * extracted/util.mli (modified) * extracted/utilBranch.ml (modified) * extracted/utilBranch.mli (modified) * extracted/values.ml (modified) * extracted/values.mli (modified) * extracted/z.ml (modified) Extracted code for the whole compiler. The space cost model is not ... Thu, 07 Feb 2013 21:43:49 GMT sacerdot [2649] * extracted/aSM.ml (modified) * extracted/aSM.mli (modified) * extracted/aSMCosts.ml (modified) * extracted/aSMCosts.mli (modified) * extracted/aSMCostsSplit.ml (modified) * extracted/aSMCostsSplit.mli (modified) * extracted/aST.ml (modified) * extracted/aST.mli (modified) * extracted/abstractStatus.ml (modified) * extracted/abstractStatus.mli (modified) * extracted/arithmetic.ml (modified) * extracted/arithmetic.mli (modified) * extracted/bitVector.ml (modified) * extracted/bitVector.mli (modified) * extracted/bitVectorTrie.ml (modified) * extracted/bitVectorTrie.mli (modified) * extracted/bitVectorZ.ml (modified) * extracted/bitVectorZ.mli (modified) * extracted/byteValues.ml (modified) * extracted/byteValues.mli (modified) * extracted/casts.ml (modified) * extracted/casts.mli (modified) * extracted/cexec.ml (modified) * extracted/cexec.mli (modified) * extracted/cexecInd.ml (modified) * extracted/cexecInd.mli (modified) * extracted/cexecSound.ml (modified) * extracted/cexecSound.mli (modified) * extracted/char.ml (deleted) * extracted/char.mli (deleted) * extracted/classifyOp.ml (modified) * extracted/classifyOp.mli (modified) * extracted/cminor_semantics.ml (modified) * extracted/cminor_semantics.mli (modified) * extracted/cminor_syntax.ml (modified) * extracted/cminor_syntax.mli (modified) * extracted/compiler.ml (modified) * extracted/compiler.mli (modified) * extracted/costLabel.ml (modified) * extracted/costLabel.mli (modified) * extracted/csem.ml (modified) * extracted/csem.mli (modified) * extracted/csyntax.ml (modified) * extracted/csyntax.mli (modified) * extracted/deqsets.ml (modified) * extracted/division.ml (modified) * extracted/errorMessages.ml (added) * extracted/errorMessages.mli (added) * extracted/errors.ml (modified) * extracted/errors.mli (modified) * extracted/events.ml (modified) * extracted/events.mli (modified) * extracted/fetch.ml (modified) * extracted/fetch.mli (modified) * extracted/floats.ml (deleted) * extracted/floats.mli (deleted) * extracted/fresh.ml (modified) * extracted/fresh.mli (modified) * extracted/frontEndMem.ml (modified) * extracted/frontEndMem.mli (modified) * extracted/frontEndOps.ml (modified) * extracted/frontEndOps.mli (modified) * extracted/frontEndVal.ml (modified) * extracted/frontEndVal.mli (modified) * extracted/frontend_misc.ml (modified) * extracted/frontend_misc.mli (modified) * extracted/genMem.ml (modified) * extracted/genMem.mli (modified) * extracted/globalenvs.ml (modified) * extracted/globalenvs.mli (modified) * extracted/graphs.ml (modified) * extracted/graphs.mli (modified) * extracted/iO.ml (modified) * extracted/iO.mli (modified) * extracted/iOMonad.ml (modified) * extracted/iOMonad.mli (modified) * extracted/identifiers.ml (modified) * extracted/identifiers.mli (modified) * extracted/initialisation.ml (modified) * extracted/initialisation.mli (modified) * extracted/integers.ml (modified) * extracted/integers.mli (modified) * extracted/interpret.ml (modified) * extracted/interpret.mli (modified) * extracted/label.ml (modified) * extracted/label.mli (modified) * extracted/labelledObjects.ml (modified) * extracted/labelledObjects.mli (modified) * extracted/list.ml (modified) * extracted/list.mli (modified) * extracted/memProperties.ml (modified) * extracted/memProperties.mli (modified) * extracted/memoryInjections.ml (modified) * extracted/memoryInjections.mli (modified) * extracted/monad.ml (modified) * extracted/pointers.ml (modified) * extracted/pointers.mli (modified) * extracted/positiveMap.ml (modified) * extracted/preIdentifiers.ml (modified) * extracted/preIdentifiers.mli (modified) * extracted/rTLabs_semantics.ml (modified) * extracted/rTLabs_semantics.mli (modified) * extracted/rTLabs_syntax.ml (modified) * extracted/rTLabs_syntax.mli (modified) * extracted/registers.ml (modified) * extracted/registers.mli (modified) * extracted/simplifyCasts.ml (modified) * extracted/simplifyCasts.mli (modified) * extracted/smallstep.ml (modified) * extracted/smallstep.mli (modified) * extracted/smallstepExec.ml (modified) * extracted/smallstepExec.mli (modified) * extracted/status.ml (modified) * extracted/status.mli (modified) * extracted/statusProofs.ml (modified) * extracted/statusProofs.mli (modified) * extracted/string.ml (modified) * extracted/string.mli (modified) * extracted/structuredTraces.ml (modified) * extracted/structuredTraces.mli (modified) * extracted/switchRemoval.ml (modified) * extracted/switchRemoval.mli (modified) * extracted/toCminor.ml (modified) * extracted/toCminor.mli (modified) * extracted/toRTLabs.ml (modified) * extracted/toRTLabs.mli (modified) * extracted/typeComparison.ml (modified) * extracted/typeComparison.mli (modified) * extracted/utilBranch.ml (modified) * extracted/utilBranch.mli (modified) * extracted/values.ml (modified) * extracted/values.mli (modified) * extracted/z.ml (modified) ... 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 ...