diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2008-09-27 08:57:55 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2008-09-27 08:57:55 +0000 |
| commit | ec6d00d94bcb1a0adc5c698367634b5e2f370c6e (patch) | |
| tree | 2e66a3c9211e2952cdfb50374c76baea6fa68eec /cfrontend/Ctyping.v | |
| parent | 2cf153d684a48ed7ab910c77d9d98b4c9da3fe2e (diff) | |
| download | compcert-kvx-ec6d00d94bcb1a0adc5c698367634b5e2f370c6e.tar.gz compcert-kvx-ec6d00d94bcb1a0adc5c698367634b5e2f370c6e.zip | |
Clight: ajout Econdition, suppression Eindex.
caml/PrintCsyntax.ml: afficher les formes a[b] et a->fld.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@789 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'cfrontend/Ctyping.v')
| -rw-r--r-- | cfrontend/Ctyping.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/cfrontend/Ctyping.v b/cfrontend/Ctyping.v index b4dd2904..c03552c6 100644 --- a/cfrontend/Ctyping.v +++ b/cfrontend/Ctyping.v @@ -56,9 +56,9 @@ Inductive wt_expr: expr -> Prop := | wt_Ecast: forall e ty ty', wt_expr e -> wt_expr (Expr (Ecast ty' e) ty) - | wt_Eindex: forall e1 e2 ty, - wt_expr e1 -> wt_expr e2 -> - wt_expr (Expr (Eindex e1 e2) ty) + | wt_Econdition: forall e1 e2 e3 ty, + wt_expr e1 -> wt_expr e2 -> wt_expr e3 -> + wt_expr (Expr (Econdition e1 e2 e3) ty) | wt_Eandbool: forall e1 e2 ty, wt_expr e1 -> wt_expr e2 -> wt_expr (Expr (Eandbool e1 e2) ty) @@ -296,7 +296,7 @@ with typecheck_exprdescr (a: Csyntax.expr_descr) (ty: type) {struct a} : bool := | Csyntax.Eunop op b => typecheck_expr b | Csyntax.Ebinop op b c => typecheck_expr b && typecheck_expr c | Csyntax.Ecast ty b => typecheck_expr b - | Csyntax.Eindex b c => typecheck_expr b && typecheck_expr c + | Csyntax.Econdition b c d => typecheck_expr b && typecheck_expr c && typecheck_expr d | Csyntax.Eandbool b c => typecheck_expr b && typecheck_expr c | Csyntax.Eorbool b c => typecheck_expr b && typecheck_expr c | Csyntax.Esizeof ty => true |