Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | Correct typo in Clightnorm.ml (#285) | Alix Trieu | 2019-03-27 | 1 | -1/+1 |
| | | | | In the `Sswitch` case, the original expression was used instead of the result of `norm_expr`. | ||||
* | clightgen: add option -normalize to ensure that memory loads never occur ↵ | Xavier Leroy | 2017-06-12 | 1 | -0/+166 |
"deep" inside expressions For example, with this option, tmp = *(x + 0) + *(x + 1) in the original Clight is rewritten to tmp1 = *(x + 0) tmp2 = *(x + 1) tmp = tmp1 + tmp2 with two temporaries tmp1 and tmp2 introduced to name the intermediate results of memory loads. Squashed commit of the following: commit 3fb69dae567b1305383b74ce1707945f91369a46 commit 0071654b77a239c00bcbb92a5845447b2c4e9d2a commit c220ed303d9f3f36cc03c347a77b065a9362c0e7 |