# # ChangeLog for src/Clight/switchRemoval.ma # # Generated by Trac 1.2 # Mar 1, 2021, 12:01:01 AM 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.