diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2016-03-02 10:35:21 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2016-03-02 10:35:21 +0100 |
| commit | 513489eb97c2b99f5ad901a0f26b493e99bbec1a (patch) | |
| tree | 42d5a8af0c7e5f56347bc668386eedb32428201f /cfrontend/Clight.v | |
| parent | d8740a489984f63864a8e4ff728fb7f3871ecb34 (diff) | |
| download | compcert-kvx-513489eb97c2b99f5ad901a0f26b493e99bbec1a.tar.gz compcert-kvx-513489eb97c2b99f5ad901a0f26b493e99bbec1a.zip | |
Make casts of pointers to _Bool semantically well defined (again).
In compCert 2.5 the semantics of pointer comparisons against the NULL pointer was made more accurate by making it undefined if the pointer is invalid (outside bounds). Technical difficulties prevented this change from being propagated to the semantics of casts from pointer types to the _Bool type, which involves an implicit pointer comparison against NULL. Hence, this kind of casts was temporarily given undefined semantics.
This commit makes pointer-to-_Bool casts semantically defined (again), provided the pointer is valid. This reinstates the equivalence between casts to _Bool and comparisons != 0. The technical difficulties mentioned above came from the translation of assignments in a value context in the SimplExpr pass. The pass was lightly modified to work around the issue.
Diffstat (limited to 'cfrontend/Clight.v')
| -rw-r--r-- | cfrontend/Clight.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/cfrontend/Clight.v b/cfrontend/Clight.v index 8722da69..086f4654 100644 --- a/cfrontend/Clight.v +++ b/cfrontend/Clight.v @@ -412,7 +412,7 @@ Inductive eval_expr: expr -> val -> Prop := eval_expr (Ebinop op a1 a2 ty) v | eval_Ecast: forall a ty v1 v, eval_expr a v1 -> - sem_cast v1 (typeof a) ty = Some v -> + sem_cast v1 (typeof a) ty m = Some v -> eval_expr (Ecast a ty) v | eval_Esizeof: forall ty1 ty, eval_expr (Esizeof ty1 ty) (Vint (Int.repr (sizeof ge ty1))) @@ -464,7 +464,7 @@ Inductive eval_exprlist: list expr -> typelist -> list val -> Prop := eval_exprlist nil Tnil nil | eval_Econs: forall a bl ty tyl v1 v2 vl, eval_expr a v1 -> - sem_cast v1 (typeof a) ty = Some v2 -> + sem_cast v1 (typeof a) ty m = Some v2 -> eval_exprlist bl tyl vl -> eval_exprlist (a :: bl) (Tcons ty tyl) (v2 :: vl). @@ -580,7 +580,7 @@ Inductive step: state -> trace -> state -> Prop := | step_assign: forall f a1 a2 k e le m loc ofs v2 v m', eval_lvalue e le m a1 loc ofs -> eval_expr e le m a2 v2 -> - sem_cast v2 (typeof a2) (typeof a1) = Some v -> + sem_cast v2 (typeof a2) (typeof a1) m = Some v -> assign_loc ge (typeof a1) m loc ofs v m' -> step (State f (Sassign a1 a2) k e le m) E0 (State f Sskip k e le m') @@ -647,7 +647,7 @@ Inductive step: state -> trace -> state -> Prop := E0 (Returnstate Vundef (call_cont k) m') | step_return_1: forall f a k e le m v v' m', eval_expr e le m a v -> - sem_cast v (typeof a) f.(fn_return) = Some v' -> + sem_cast v (typeof a) f.(fn_return) m = Some v' -> Mem.free_list m (blocks_of_env e) = Some m' -> step (State f (Sreturn (Some a)) k e le m) E0 (Returnstate v' (call_cont k) m') |