diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2016-10-06 11:01:34 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2016-10-06 11:01:34 +0200 |
| commit | 3c605199ab0d096cd66ba671a4e23eac9e79bbc2 (patch) | |
| tree | 93e52e7505a47dd1e08db105d24c7fcd66097829 /runtime/x86_64 | |
| parent | fecf2472ee5c2f6da25eb1ea340e0f07dcdaec69 (diff) | |
| download | compcert-kvx-3c605199ab0d096cd66ba671a4e23eac9e79bbc2.tar.gz compcert-kvx-3c605199ab0d096cd66ba671a4e23eac9e79bbc2.zip | |
Regression: handling of integer + pointer in CompCert C
During the experiments, the integer + pointer cases was removed from the semantics of the C addition operator. The idea was to turn integer + pointer into pointer + integer during elaboration, but it was not implemented.
On second thoughts, we can restore the integer + pointer cases in the formal semantics of CompCert C at low cost. This is what this commit does.
Diffstat (limited to 'runtime/x86_64')
0 files changed, 0 insertions, 0 deletions