diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2006-09-11 16:03:02 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2006-09-11 16:03:02 +0000 |
commit | be43363d309cea62731e04ad10dddf3ecafcacd1 (patch) | |
tree | f66c346d51df74d6b6ee34f654178a44250a33c8 /cfrontend/Cshmgen.v | |
parent | 5e8237152cad0cf08d3eea0d5de8cd8bc499df69 (diff) | |
download | compcert-be43363d309cea62731e04ad10dddf3ecafcacd1.tar.gz compcert-be43363d309cea62731e04ad10dddf3ecafcacd1.zip |
Revu traitement des structures et unions recursives. Dans Cshmgen, meilleure compilation de exit_if_false.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@94 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'cfrontend/Cshmgen.v')
-rw-r--r-- | cfrontend/Cshmgen.v | 19 |
1 files changed, 10 insertions, 9 deletions
diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v index 5585416b..aaec07d8 100644 --- a/cfrontend/Cshmgen.v +++ b/cfrontend/Cshmgen.v @@ -41,8 +41,9 @@ Definition var_kind_of_type (ty: type): option var_kind := | Tpointer _ => Some(Vscalar Mint32) | Tarray _ _ => Some(Varray (Csyntax.sizeof ty)) | Tfunction _ _ => None - | Tstruct fList => Some(Varray (Csyntax.sizeof ty)) - | Tunion fList => Some(Varray (Csyntax.sizeof ty)) + | Tstruct _ fList => Some(Varray (Csyntax.sizeof ty)) + | Tunion _ fList => Some(Varray (Csyntax.sizeof ty)) + | Tcomp_ptr _ => Some(Vscalar Mint32) end. (** ** Csharpminor constructors *) @@ -359,13 +360,13 @@ Fixpoint transl_expr (a: Csyntax.expr) {struct a} : option expr := Some(make_intconst (Int.repr (Csyntax.sizeof ty))) | Expr (Csyntax.Efield b i) ty => match typeof b with - | Tstruct fld => + | Tstruct _ fld => do tb <- transl_lvalue b; do ofs <- field_offset i fld; make_load (make_binop Oadd tb (make_intconst (Int.repr ofs))) ty - | Tunion fld => + | Tunion _ fld => do tb <- transl_lvalue b; make_load tb ty | _ => None @@ -389,11 +390,11 @@ with transl_lvalue (a: Csyntax.expr) {struct a} : option expr := make_add tb (typeof b) tc (typeof c) | Expr (Csyntax.Efield b i) ty => match typeof b with - | Tstruct fld => + | Tstruct _ fld => do tb <- transl_lvalue b; do ofs <- field_offset i fld; Some (make_binop Oadd tb (make_intconst (Int.repr ofs))) - | Tunion fld => + | Tunion _ fld => transl_lvalue b | _ => None end @@ -430,9 +431,9 @@ Definition is_variable (e: Csyntax.expr) : option ident := Definition exit_if_false (e: Csyntax.expr) : option stmt := do te <- transl_expr e; Some(Sifthenelse - (make_notbool te (typeof e)) - (Sexit 0%nat) - Sskip). + (make_boolean te (typeof e)) + Sskip + (Sexit 0%nat)). (* [transl_statement nbrk ncnt s] returns a Csharpminor statement that performs the same computations as the CabsCoq statement [s]. |