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 /backend/SplitLong.vp | |
parent | fecf2472ee5c2f6da25eb1ea340e0f07dcdaec69 (diff) | |
download | compcert-3c605199ab0d096cd66ba671a4e23eac9e79bbc2.tar.gz compcert-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 'backend/SplitLong.vp')
0 files changed, 0 insertions, 0 deletions