| Commit message (Collapse) | Author | Age | Files | Lines | |
|---|---|---|---|---|---|
| * | 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 | |||||
 |
index : compcert | |
| CompCert fork with minor modifications for Vericert. |
| aboutsummaryrefslogtreecommitdiffstats |