diff options
| author | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2016-03-11 15:03:35 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2016-03-11 15:03:35 +0100 |
| commit | ab2905797cf196d792372e8794fe5a8f2116efd5 (patch) | |
| tree | 720dea76e912901797674c42ff1def422f4fe8e4 /cfrontend/SimplExpr.v | |
| parent | 18cb44c3db21f8b021e801f91f466712dc1697f8 (diff) | |
| parent | 513489eb97c2b99f5ad901a0f26b493e99bbec1a (diff) | |
| download | compcert-kvx-ab2905797cf196d792372e8794fe5a8f2116efd5.tar.gz compcert-kvx-ab2905797cf196d792372e8794fe5a8f2116efd5.zip | |
Merge pull request #90 from AbsInt/sem-casts
Make casts of pointers to _Bool semantically well defined
Diffstat (limited to 'cfrontend/SimplExpr.v')
| -rw-r--r-- | cfrontend/SimplExpr.v | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/cfrontend/SimplExpr.v b/cfrontend/SimplExpr.v index a5a6ad66..a3af8114 100644 --- a/cfrontend/SimplExpr.v +++ b/cfrontend/SimplExpr.v @@ -114,7 +114,7 @@ Fixpoint eval_simpl_expr (a: expr) : option val := | Ecast b ty => match eval_simpl_expr b with | None => None - | Some v => sem_cast v (typeof b) ty + | Some v => sem_cast v (typeof b) ty Mem.empty end | _ => None end. @@ -327,10 +327,10 @@ Fixpoint transl_expr (dst: destination) (a: Csyntax.expr) : mon (list statement let ty2 := Csyntax.typeof r2 in match dst with | For_val | For_set _ => - do t <- gensym ty2; + do t <- gensym ty1; ret (finish dst - (sl1 ++ sl2 ++ Sset t a2 :: make_assign a1 (Etempvar t ty2) :: nil) - (Ecast (Etempvar t ty2) ty1)) + (sl1 ++ sl2 ++ Sset t (Ecast a2 ty1) :: make_assign a1 (Etempvar t ty1) :: nil) + (Etempvar t ty1)) | For_effects => ret (sl1 ++ sl2 ++ make_assign a1 a2 :: nil, dummy_expr) @@ -342,12 +342,12 @@ Fixpoint transl_expr (dst: destination) (a: Csyntax.expr) : mon (list statement do (sl3, a3) <- transl_valof ty1 a1; match dst with | For_val | For_set _ => - do t <- gensym tyres; + do t <- gensym ty1; ret (finish dst (sl1 ++ sl2 ++ sl3 ++ - Sset t (Ebinop op a3 a2 tyres) :: - make_assign a1 (Etempvar t tyres) :: nil) - (Ecast (Etempvar t tyres) ty1)) + Sset t (Ecast (Ebinop op a3 a2 tyres) ty1) :: + make_assign a1 (Etempvar t ty1) :: nil) + (Etempvar t ty1)) | For_effects => ret (sl1 ++ sl2 ++ sl3 ++ make_assign a1 (Ebinop op a3 a2 tyres) :: nil, dummy_expr) |