#
# ChangeLog for src/Clight/switchRemoval.ma
#
# Generated by Trac 1.2
# Mar 6, 2021, 6:45:09 PM

Wed, 03 Oct 2012 11:27:38 GMT garnier [2387]
	* src/Clight/switchRemoval.ma (modified)

	Revamped memory extensions, proved stuff on freeing blocks and on ...


Wed, 26 Sep 2012 16:14:38 GMT campbell [2353]
	* src/Clight/Cexec.ma (modified)
	* src/Clight/CexecComplete.ma (modified)
	* src/Clight/CexecEquiv.ma (modified)
	* src/Clight/CexecSound.ma (modified)
	* src/Clight/Csem.ma (modified)
	* src/Clight/Csyntax.ma (modified)
	* src/Clight/SimplifyCasts.ma (modified)
	* src/Clight/label.ma (modified)
	* src/Clight/labelSimulation.ma (modified)
	* src/Clight/switchRemoval.ma (modified)
	* src/Clight/test/goto-if.test.ma (modified)
	* src/Clight/test/sum.test.ma (modified)
	* src/Clight/toCminor.ma (modified)

	Put the post-loop cost label into the Clight while statement to get ...


Wed, 12 Sep 2012 10:36:46 GMT garnier [2332]
	* src/Clight/frontend_misc.ma (modified)
	* src/Clight/memoryInjections.ma (modified)
	* src/Clight/switchRemoval.ma (modified)
	* src/common/GenMem.ma (modified)

	Some progress on switch removal. Small fix in the definition of free, ...


Wed, 29 Aug 2012 21:21:49 GMT garnier [2304]
	* src/Clight/switchRemoval.ma (modified)

	Strengthened proof of associativity of bitvector addition. Some more ...


Fri, 24 Aug 2012 11:11:12 GMT garnier [2302]
	* src/Clight/switchRemoval.ma (modified)

	Finally proved associativity of addition on bitvectors. Rejoice.


Thu, 16 Aug 2012 17:01:18 GMT garnier [2298]
	* src/Clight/switchRemoval.ma (modified)

	WIP: converting switch removal from Z to bitvectors. Does not ...


Thu, 26 Jul 2012 15:02:52 GMT garnier [2271]
	* src/Clight/switchRemoval.ma (modified)

	Proof of correction for the semantics of expressions under memory ...


Wed, 25 Jul 2012 16:55:36 GMT garnier [2263]
	* src/Clight/Csem.ma (modified)
	* src/Clight/switchRemoval.ma (modified)

	Finished proving semantics preservation under memory injections for ...


Tue, 24 Jul 2012 18:12:00 GMT garnier [2255]
	* src/Clight/switchRemoval.ma (modified)

	Had to modify the definition of memory injections to prove that ...


Mon, 23 Jul 2012 17:31:11 GMT garnier [2234]
	* src/Clight/frontend_misc.ma (modified)
	* src/Clight/switchRemoval.ma (modified)

	Progress on proving semantics preservation under memory injections.


Fri, 20 Jul 2012 18:28:57 GMT garnier [2227]
	* src/Clight/switchRemoval.ma (modified)

	* New version of the switch removal algorithm, described at the top ...


Thu, 14 Jun 2012 08:30:21 GMT garnier [2076]
	* src/Clight/switchRemoval.ma (modified)

	First steps towards a simulation proof for switch removal.


Mon, 04 Jun 2012 14:13:24 GMT garnier [2016]
	* src/Clight/switchRemoval.ma (modified)

	Slight change in simplification strategy to better match the
	semantics


Thu, 03 May 2012 17:13:54 GMT garnier [1915]
	* src/Clight/switchRemoval.ma (modified)

	Correction of a typo in switchRemoval.


Mon, 09 Apr 2012 09:53:35 GMT campbell [1883]
	* src/Clight/switchRemoval.ma (added)
	* src/Clight/test/switcher.test.ma (modified)

	Ilias' switch removal code, plus a test.