#
# ChangeLog for driver
#
# Generated by Trac 1.2
# Dec 9, 2019, 5:26:41 AM

Wed, 13 Mar 2013 23:04:08 GMT sacerdot [2868]
	* driver/backendPrinter.ml (modified)
	* extracted/eRTL_printer.ml (added)
	* extracted/eRTL_printer.mli (added)
	* extracted/eRTLptr_printer.ml (added)
	* extracted/eRTLptr_printer.mli (added)
	* src/ERTL/ERTL_printer.ma (added)
	* src/ERTLptr/ERTLptr_printer.ma (added)

	Pretty printing of ERTL and ERTLptr code.


Wed, 13 Mar 2013 13:27:55 GMT sacerdot [2864]
	* driver/backendPrinter.ml (modified)
	* driver/cerco.ml (modified)

	I must have drunk yesterday: all RTL passes are printed correctly; ...


Wed, 13 Mar 2013 01:02:57 GMT sacerdot [2860]
	* driver/backendPrinter.ml (modified)
	* driver/backendPrinter.mli (modified)
	* driver/cerco.ml (modified)
	* extracted/rTL_printer.ml (added)
	* extracted/rTL_printer.mli (added)
	* src/RTL/RTL_printer.ma (added)

	RTL printing, core dumps ATM


Wed, 13 Mar 2013 00:19:48 GMT sacerdot [2859]
	* driver/backendPrinter.ml (modified)
	* extracted/joint_printer.ml (modified)
	* src/joint/joint_printer.ma (modified)

	Pretty printing improved (now it always starts the visit from lbl 1).


Tue, 12 Mar 2013 23:52:16 GMT sacerdot [2858]
	* driver/backendPrinter.ml (modified)
	* extracted/joint_printer.ml (modified)
	* extracted/joint_printer.mli (modified)
	* extracted/lTL_printer.ml (modified)
	* extracted/lTL_printer.mli (modified)
	* src/LTL/LTL_printer.ma (modified)
	* src/joint/joint_printer.ma (modified)

	Trying to pretty print the code graph in visit order.
	Slightly ...


Tue, 12 Mar 2013 18:11:56 GMT sacerdot [2856]
	* driver/IntelHex.mli (modified)
	* driver/backendPrinter.ml (modified)
	* driver/build (modified)

	Pretty printing of LTL almost finished.


Tue, 12 Mar 2013 16:53:56 GMT sacerdot [2854]
	* driver/backendPrinter.ml (added)
	* driver/backendPrinter.mli (added)
	* driver/build (modified)
	* driver/cerco.ml (modified)
	* extracted/aSMCosts.ml (modified)
	* extracted/compiler.ml (modified)
	* extracted/eRTL.ml (modified)
	* extracted/eRTLptr.ml (modified)
	* extracted/eRTLptrToLTL.ml (modified)
	* extracted/interference.ml (modified)
	* extracted/joint.ml (modified)
	* extracted/joint_LTL_LIN.ml (modified)
	* extracted/joint_LTL_LIN_semantics.ml (modified)
	* extracted/joint_printer.ml (added)
	* extracted/joint_printer.mli (added)
	* extracted/lINToASM.ml (modified)
	* extracted/lTL_printer.ml (added)
	* extracted/lTL_printer.mli (added)
	* extracted/rTL.ml (modified)
	* extracted/rTLabsToRTL.ml (modified)
	* extracted/rTLabs_traces.ml (modified)
	* extracted/translateUtils.ml (modified)
	* extracted/translateUtils.mli (modified)

	Pretty printing of the LTL program.


Fri, 08 Mar 2013 22:45:29 GMT sacerdot [2834]
	* driver/build (modified)
	* driver/cerco.ml (modified)
	* driver/exec_all.ml (deleted)

	Execution integrated in the compiler, as it was in the prototype. ...


Fri, 08 Mar 2013 20:07:10 GMT sacerdot [2826]
	* driver/error.ml (modified)

	New error messages.


Thu, 07 Mar 2013 20:41:05 GMT sacerdot [2815]
	* driver/build (modified)
	* driver/exec.ml (deleted)

	exec superseded by exec_all


Thu, 07 Mar 2013 20:39:58 GMT sacerdot [2814]
	* driver/build (modified)
	* driver/frontend.ml (deleted)

	frontend superseded by execute_all


Thu, 07 Mar 2013 20:34:34 GMT sacerdot [2813]
	* driver/exec_all.ml (modified)

	RTLabs now printed too


Thu, 07 Mar 2013 13:01:40 GMT sacerdot [2805]
	* driver/exec_all.ml (modified)

	Now also prints the trace for the labelled Clight.


Thu, 07 Mar 2013 12:55:14 GMT sacerdot [2804]
	* driver/build (modified)
	* driver/exec_all.ml (added)

	New executable exec_all. It contains a function to run and print all ...


Thu, 07 Mar 2013 11:56:37 GMT sacerdot [2798]
	* driver/error.ml (modified)

	New error message.


Wed, 06 Mar 2013 15:50:31 GMT campbell [2792]
	* driver/clightPrinter.ml (modified)

	Make instrumented output a little easier to read.


Wed, 06 Mar 2013 15:50:30 GMT campbell [2791]
	* driver/cerco.ml (modified)

	Remove dead code in driver.


Wed, 06 Mar 2013 14:48:20 GMT campbell [2790]
	* driver/clightFromC.ml (modified)

	Some null handling in conversion from CIL.


Wed, 06 Mar 2013 14:48:19 GMT campbell [2789]
	* driver/build (modified)
	* driver/cerco.ml (moved)
	* driver/clightPrinter.ml (modified)
	* driver/exec.ml (modified)
	* driver/frontend.ml (modified)
	* extracted/build (modified)

	Some changes to the driver to aid debugging.


Wed, 06 Mar 2013 14:48:18 GMT campbell [2788]
	* driver/compiler.ml (modified)

	Report compiler error


Wed, 06 Mar 2013 14:48:14 GMT campbell [2787]
	* driver/clightPrinter.ml (modified)
	* driver/clightPrinter.mli (modified)
	* driver/compiler.ml (modified)

	Output stack costs in driver.


Wed, 06 Mar 2013 01:59:22 GMT sacerdot [2780]
	* driver/IntelHex.ml (modified)
	* extracted/bitVector.ml (modified)
	* extracted/bitVector.mli (modified)

	Bug fixed: in BitVector.ma the functions bv_to_nat and nat_to_bv were ...


Tue, 05 Mar 2013 22:50:59 GMT sacerdot [2779]
	* driver/IntelHex.ml (modified)

	1. bug fixed in the use of vsplit
	2. major speed up (avoid detour ...


Tue, 05 Mar 2013 22:34:38 GMT sacerdot [2778]
	* driver/ASMPrinter.ml (added)
	* driver/ASMPrinter.mli (added)
	* driver/IntelHex.ml (added)
	* driver/IntelHex.mli (added)
	* driver/build (modified)
	* driver/compiler.ml (modified)

	Code to pretty-print the IntelHex output.
	At the moment the glue ...


Tue, 05 Mar 2013 20:53:01 GMT sacerdot [2776]
	* driver/compiler.ml (modified)

	The compiler now extracts also the stack cost model.


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 ...


Fri, 01 Mar 2013 18:56:34 GMT campbell [2759]
	* driver/clightPrinter.ml (modified)
	* driver/clightPrinter.mli (modified)
	* driver/compiler.ml (modified)
	* extracted/aSMCosts.ml (modified)

	Print out costs, with choice of style.
	Note small anti-assertion ...


Fri, 01 Mar 2013 18:55:27 GMT campbell [2758]
	* driver/build (modified)
	* driver/clightFromC.ml (modified)
	* driver/clightPrinter.ml (added)
	* driver/clightPrinter.mli (added)
	* driver/compiler.ml (modified)

	Adapt prototype's Clight printer.
	Doesn't use cost map yet.


Wed, 27 Feb 2013 21:48:27 GMT sacerdot [2747]
	* driver/compiler.ml (added)

	The compiler (frontend + backend)


Wed, 27 Feb 2013 21:45:27 GMT sacerdot [2744]
	* driver/build (modified)

	Build no longer fails.


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.


Thu, 07 Feb 2013 21:43:39 GMT sacerdot [2648]
	* driver/clightFromC.ml (modified)

	Back in sync with the extracted code.


Wed, 06 Feb 2013 22:43:31 GMT campbell [2636]
	* driver/build (modified)
	* driver/frontend.ml (added)
	* extracted/cminor_semantics.ml (added)
	* extracted/cminor_semantics.mli (added)
	* extracted/rTLabs_semantics.ml (added)
	* extracted/rTLabs_semantics.mli (added)

	Extracted front-end.


Wed, 06 Feb 2013 16:03:20 GMT campbell [2620]
	* driver (added)
	* driver/build (added)
	* driver/clightFromC.ml (added)
	* driver/clightParser.ml (added)
	* driver/clightParser.mli (added)
	* driver/exec.ml (added)
	* extracted/aSM.ml (modified)
	* extracted/build (added)
	* extracted/compiler.ml (modified)
	* extracted/floats.ml (modified)
	* extracted/floats.mli (modified)

	Sufficient hacking to run the extracted Clight semantics.