diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-01-23 13:33:33 +0100 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-01-23 13:33:33 +0100 |
commit | b5b681b7b55abb18165eaa907b04aefb9b0fddde (patch) | |
tree | 9c0a7df4b20ede85b54fe5c4e5d326fbf30a0013 /cfrontend/SimplLocals.v | |
parent | 12803784f2753863985d1030999469c18e01e0f1 (diff) | |
parent | f00b70b6a17fdfb4e8606df891f6becc8102ef12 (diff) | |
download | compcert-b5b681b7b55abb18165eaa907b04aefb9b0fddde.tar.gz compcert-b5b681b7b55abb18165eaa907b04aefb9b0fddde.zip |
Merge branch 'master' into dwarf
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 |}. |