diff options
author | Xavier Leroy <xavier.leroy@inria.fr> | 2015-01-23 09:33:59 +0100 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@inria.fr> | 2015-01-23 09:33:59 +0100 |
commit | d594c5da5e11fb10775c2b772961b8a2383887c7 (patch) | |
tree | 750ed5d4a0829519a258f3c12f7d518e53504487 /cfrontend/SimplLocals.v | |
parent | 1e97bb4f6297b6fa7949684e522a592aab754d99 (diff) | |
parent | 2dd864217cc864d44e828a4d14dd45668e4ab095 (diff) | |
download | compcert-d594c5da5e11fb10775c2b772961b8a2383887c7.tar.gz compcert-d594c5da5e11fb10775c2b772961b8a2383887c7.zip |
Merge branch 'named-structs'
- Switch CompCert C / Clight AST of composite types (structs and unions)
from a structural representation to a nominal representation,
closer to concrete syntax.
- This avoids algorithmic inefficiencies due to the structural representation.
- Closes PR#4.
- Smallstep: make small-step semantics more polymorphic in the type of the
global environment.
- Globalenvs: introduce Senv.t (symbol environments) as a restricted view
on Genv.t (full global environments).
- Events, Smallstep: use Senv instead of Genv to talk about global names.
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 |}. |