diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2017-06-12 09:16:10 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2017-06-12 09:16:10 +0200 |
| commit | 446cff1087ffe40d9b19b616162212ca83677515 (patch) | |
| tree | 59ff4611eb11ea7eaccadf0e703baf2696ddb7ce /Changelog | |
| parent | e1de6a1c3c5cbf4c6551d3442e3c4e49145709fb (diff) | |
| download | compcert-kvx-446cff1087ffe40d9b19b616162212ca83677515.tar.gz compcert-kvx-446cff1087ffe40d9b19b616162212ca83677515.zip | |
clightgen: add option -normalize to ensure that memory loads never occur "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
Diffstat (limited to 'Changelog')
0 files changed, 0 insertions, 0 deletions