diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-07-16 16:17:08 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-07-16 16:17:08 +0000 |
commit | a335e621aaa85a7f73b16c121261dbecf8e68340 (patch) | |
tree | 31312a22aafc7f66818c0c82f4c96e88ff391595 /Changelog | |
parent | 93b89122000e42ac57abc39734fdf05d3a89e83c (diff) |
In conditional expressions e1 ? e2 : e3, cast the results of e2 and e3 to the type of the whole conditional expression.
Replaced predicates "cast", "is_true" and "is_false" by functions "sem_cast" and "bool_val".
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1684 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'Changelog')
-rw-r--r-- | Changelog | 5 |
1 files changed, 5 insertions, 0 deletions
@@ -1,3 +1,8 @@ +- Fixed two omissions in the semantics of CompCert C (reported by Brian Campbell): + . Functions calls through a function pointer had undefined semantics. + . Conditional expressions "e1 ? e2 : e3" where e2 and e3 have different + types were missing a cast to their common type. + - Revised and strengthened the top-level statements of semantic preservation. In particular, we now show: . backward simulation for the whole compiler without assuming |