# # ChangeLog for driver/error.ml # # Generated by Trac 1.2 # Mar 3, 2021, 10:26:09 AM Tue, 26 Mar 2013 15:51:40 GMT sacerdot [2960] * driver/cerco.ml (modified) * driver/error.ml (modified) * extracted/compiler.ml (modified) * extracted/eRTL.ml (modified) * extracted/eRTLptr.ml (modified) * extracted/eRTLptrToLTL.ml (modified) * extracted/eRTLptr_semantics.ml (modified) * extracted/errorMessages.ml (modified) * extracted/errorMessages.mli (modified) * extracted/interference.ml (modified) * extracted/joint_LTL_LIN_semantics.ml (modified) * extracted/joint_fullexec.ml (modified) * extracted/joint_fullexec.mli (modified) * extracted/joint_semantics.ml (modified) * extracted/joint_semantics.mli (modified) * extracted/lIN.ml (modified) * extracted/lINToASM.ml (modified) * extracted/lTL.ml (modified) * extracted/policy.ml (modified) * extracted/rTL.ml (modified) * extracted/rTL_semantics.ml (modified) * extracted/rTL_semantics.mli (modified) * extracted/rTLabsToRTL.ml (modified) * extracted/semantics.ml (modified) * extracted/semanticsUtils.ml (modified) * extracted/semanticsUtils.mli (modified) * extracted/semantics_blocks.ml (deleted) * extracted/semantics_blocks.mli (deleted) * extracted/toCminor.ml (modified) * extracted/toCminor.mli (modified) * extracted/traces.ml (modified) * extracted/traces.mli (modified) New extraction, it diverges in RTL execution now. Fri, 08 Mar 2013 20:07:10 GMT sacerdot [2826] * driver/error.ml (modified) New error messages. Thu, 07 Mar 2013 11:56:37 GMT sacerdot [2798] * driver/error.ml (modified) New error message. Mon, 04 Mar 2013 09:03:33 GMT sacerdot [2773] * driver/clightFromC.ml (modified) * driver/clightPrinter.ml (modified) * driver/error.ml (modified) * driver/exec.ml (modified) * driver/frontend.ml (modified) * extracted/PROBLEMS (modified) * 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 (modified) * extracted/assembly.mli (modified) * extracted/assocList.ml (modified) * extracted/backEndOps.ml (modified) * extracted/backEndOps.mli (modified) * extracted/bigops.ml (added) * extracted/bigops.mli (added) * extracted/bindLists.ml (modified) * extracted/bindLists.mli (modified) * extracted/bind_new.ml (modified) * extracted/bitVector.ml (modified) * extracted/bitVector.mli (modified) * extracted/bitVectorTrie.ml (modified) * extracted/bitVectorTrie.mli (modified) * extracted/bitVectorTrieSet.ml (modified) * extracted/bitVectorTrieSet.mli (modified) * extracted/bitVectorZ.ml (modified) * extracted/bitVectorZ.mli (modified) * extracted/blocks.ml (modified) * extracted/blocks.mli (modified) * extracted/build (modified) * extracted/byteValues.ml (modified) * extracted/byteValues.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_semantics.ml (deleted) * extracted/cminor_semantics.mli (deleted) * extracted/cminor_syntax.ml (modified) * extracted/cminor_syntax.mli (modified) * extracted/compiler.ml (modified) * extracted/compiler.mli (modified) * extracted/costCheck.ml (modified) * extracted/costCheck.mli (modified) * extracted/costInj.ml (modified) * extracted/costInj.mli (modified) * extracted/costLabel.ml (modified) * extracted/costLabel.mli (modified) * extracted/costMisc.ml (modified) * extracted/costMisc.mli (modified) * extracted/costSpec.ml (modified) * extracted/costSpec.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 (deleted) * extracted/deqsets_extras.mli (deleted) * extracted/division.ml (modified) * extracted/eRTL.ml (modified) * extracted/eRTL.mli (modified) * extracted/eRTLToERTLptr.ml (modified) * extracted/eRTLToERTLptr.mli (modified) * extracted/eRTLptr.ml (modified) * extracted/eRTLptr.mli (modified) * extracted/eRTLptrToLTL.ml (modified) * extracted/eRTLptrToLTL.mli (modified) * extracted/errorMessages.ml (modified) * extracted/errorMessages.mli (modified) * extracted/errors.ml (modified) * extracted/events.ml (modified) * extracted/events.mli (modified) * extracted/executions.ml (modified) * extracted/executions.mli (modified) * extracted/extralib.ml (modified) * extracted/extralib.mli (modified) * extracted/extranat.ml (modified) * extracted/extranat.mli (modified) * extracted/fetch.ml (modified) * extracted/fetch.mli (modified) * extracted/fixpoints.ml (modified) * extracted/fixpoints.mli (modified) * extracted/foldStuff.ml (modified) * 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/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 (modified) * extracted/i8051.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/interference.ml (modified) * extracted/interference.mli (modified) * extracted/interpret.ml (modified) * extracted/interpret.mli (modified) * extracted/jmeq.ml (modified) * extracted/joint.ml (modified) * extracted/joint.mli (modified) * extracted/joint_LTL_LIN.ml (modified) * extracted/joint_LTL_LIN.mli (modified) * extracted/lIN.ml (modified) * extracted/lIN.mli (modified) * extracted/lINToASM.ml (modified) * extracted/lINToASM.mli (modified) * extracted/lTL.ml (modified) * extracted/lTL.mli (modified) * extracted/lTLToLIN.ml (modified) * extracted/lTLToLIN.mli (modified) * extracted/label.ml (modified) * extracted/label.mli (modified) * extracted/labelledObjects.ml (modified) * extracted/labelledObjects.mli (modified) * extracted/linearise.ml (modified) * extracted/linearise.mli (modified) * extracted/list.ml (modified) * extracted/list.mli (modified) * extracted/listb.ml (modified) * extracted/listb.mli (modified) * extracted/lists.ml (modified) * extracted/lists.mli (modified) * extracted/liveness.ml (modified) * extracted/liveness.mli (modified) * extracted/memProperties.ml (modified) * extracted/memProperties.mli (modified) * extracted/memoryInjections.ml (modified) * extracted/memoryInjections.mli (modified) * extracted/monad.ml (modified) * extracted/monad.mli (modified) * extracted/option.ml (modified) * extracted/option.mli (modified) * extracted/pointers.ml (modified) * extracted/pointers.mli (modified) * extracted/policy.ml (modified) * extracted/policy.mli (modified) * extracted/policyFront.ml (modified) * extracted/policyFront.mli (modified) * extracted/policyStep.ml (modified) * extracted/policyStep.mli (modified) * extracted/positive.ml (modified) * extracted/positive.mli (modified) * extracted/positiveMap.ml (modified) * extracted/positiveMap.mli (modified) * extracted/preIdentifiers.ml (modified) * extracted/rTL.ml (modified) * extracted/rTL.mli (modified) * extracted/rTLToERTL.ml (modified) * extracted/rTLToERTL.mli (modified) * extracted/rTLabsToRTL.ml (modified) * extracted/rTLabsToRTL.mli (modified) * extracted/rTLabs_abstract.ml (modified) * extracted/rTLabs_abstract.mli (modified) * extracted/rTLabs_semantics.ml (modified) * extracted/rTLabs_semantics.mli (modified) * extracted/rTLabs_syntax.ml (modified) * extracted/rTLabs_syntax.mli (modified) * extracted/rTLabs_traces.ml (modified) * extracted/rTLabs_traces.mli (modified) * extracted/registerSet.ml (modified) * extracted/registerSet.mli (modified) * extracted/setoids.ml (modified) * extracted/setoids.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/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 (modified) * extracted/translateUtils.mli (modified) * extracted/typeComparison.ml (modified) * extracted/typeComparison.mli (modified) * extracted/types.ml (modified) * extracted/types.mli (modified) * extracted/untrusted/build.ml (modified) * extracted/untrusted/compute_fixpoints.ml (modified) * extracted/untrusted/glue.ml (modified) * extracted/untrusted/set_adt.ml (modified) * extracted/uses.ml (modified) * extracted/uses.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/vector.ml (modified) * extracted/vector.mli (modified) * extracted/z.ml (modified) * extracted/z.mli (modified) 1. everything extracted again after all bugs in Matita's extraction ... Mon, 25 Feb 2013 20:51:36 GMT sacerdot [2729] * driver/error.ml (modified) More errors recognized Sat, 23 Feb 2013 16:05:02 GMT campbell [2721] * driver/build (modified) * driver/error.ml (added) * driver/exec.ml (modified) * driver/frontend.ml (modified) Give the real error in the driver.