diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-02-19 16:24:28 +0100 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-02-19 16:24:28 +0100 |
commit | e51ffb6c1d9411515facc5e97a4e8dba5d8b55ab (patch) | |
tree | 80a7fc8212d28712365082e1a2a2d0fa28cedad3 /cfrontend/SimplLocals.v | |
parent | c130f4936bad11fd6dab3a5d142b870d2a5f650c (diff) | |
parent | b0eb1dfc9fd7b15c556c49101390d882b0f00f8a (diff) | |
download | compcert-e51ffb6c1d9411515facc5e97a4e8dba5d8b55ab.tar.gz compcert-e51ffb6c1d9411515facc5e97a4e8dba5d8b55ab.zip |
Merge branch 'master' into no-shell
Diffstat (limited to 'cfrontend/SimplLocals.v')
-rw-r--r-- | cfrontend/SimplLocals.v | 18 |
1 files changed, 13 insertions, 5 deletions
diff --git a/cfrontend/SimplLocals.v b/cfrontend/SimplLocals.v index 9c529280..52ee8377 100644 --- a/cfrontend/SimplLocals.v +++ b/cfrontend/SimplLocals.v @@ -48,8 +48,8 @@ Definition make_cast (a: expr) (tto: type) : expr := | cast_case_f2f => a | cast_case_s2s => a | cast_case_l2l => a - | cast_case_struct _ _ _ _ => a - | cast_case_union _ _ _ _ => a + | cast_case_struct _ _ => a + | cast_case_union _ _ => a | cast_case_void => a | _ => Ecast a tto end. @@ -70,6 +70,8 @@ Fixpoint simpl_expr (cenv: compilenv) (a: expr) : expr := | Ebinop op a1 a2 ty => Ebinop op (simpl_expr cenv a1) (simpl_expr cenv a2) ty | Ecast a1 ty => Ecast (simpl_expr cenv a1) ty | Efield a1 fld ty => Efield (simpl_expr cenv a1) fld ty + | Esizeof _ _ => a + | Ealignof _ _ => a end. Definition simpl_exprlist (cenv: compilenv) (al: list expr) : list expr := @@ -170,6 +172,8 @@ Fixpoint addr_taken_expr (a: expr): VSet.t := | Ebinop op a1 a2 ty => VSet.union (addr_taken_expr a1) (addr_taken_expr a2) | Ecast a1 ty => addr_taken_expr a1 | Efield a1 fld ty => addr_taken_expr a1 + | Esizeof _ _ => VSet.empty + | Ealignof _ _ => VSet.empty end. Fixpoint addr_taken_exprlist (l: list expr) : VSet.t := @@ -247,6 +251,10 @@ Definition transf_fundef (fd: fundef) : res fundef := end. Definition transf_program (p: program) : res program := - AST.transform_partial_program transf_fundef p. - - + do p1 <- AST.transform_partial_program transf_fundef p; + OK {| prog_defs := AST.prog_defs p1; + prog_public := AST.prog_public p1; + prog_main := AST.prog_main p1; + prog_types := prog_types p; + prog_comp_env := prog_comp_env p; + prog_comp_env_eq := prog_comp_env_eq p |}. |