Search:
Login
Preferences
Help/Guide
About Trac
Wiki
Timeline
Roadmap
Browse Source
View Tickets
Search
Context Navigation
View Latest Revision
source:
src
/
Clight
/
switchRemoval.ma
Revision Log Mode:
Stop on copy
Follow copies
Show only adds and deletes
View log starting at
and back to
Show at most
revisions per page.
Show full log messages
Legend:
Added
Modified
Copied or renamed
Diff
Rev
Age
Author
Log Message
(edit)
@2387
8 years
garnier
Revamped memory extensions, proved stuff on freeing blocks and on …
(edit)
@2353
8 years
campbell
Put the post-loop cost label into the Clight while statement to get …
(edit)
@2332
8 years
garnier
Some progress on switch removal. Small fix in the definition of free, …
(edit)
@2304
8 years
garnier
Strengthened proof of associativity of bitvector addition. Some more …
(edit)
@2302
8 years
garnier
Finally proved associativity of addition on bitvectors. Rejoice.
(edit)
@2298
8 years
garnier
WIP: converting switch removal from Z to bitvectors. Does not compile, …
(edit)
@2271
8 years
garnier
Proof of correction for the semantics of expressions under memory …
(edit)
@2263
8 years
garnier
Finished proving semantics preservation under memory injections for …
(edit)
@2255
8 years
garnier
Had to modify the definition of memory injections to prove that …
(edit)
@2234
8 years
garnier
Progress on proving semantics preservation under memory injections.
(edit)
@2227
9 years
garnier
* New version of the switch removal algorithm, described at the top of …
(edit)
@2076
9 years
garnier
First steps towards a simulation proof for switch removal.
(edit)
@2016
9 years
garnier
Slight change in simplification strategy to better match the semantics
(edit)
@1915
9 years
garnier
Correction of a typo in switchRemoval.
(add)
@1883
9 years
campbell
Ilias' switch removal code, plus a test.
Note:
See
TracRevisionLog
for help on using the revision log.
Download in other formats:
RSS Feed
ChangeLog