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/Csem.v | |
| parent | 2cf153d684a48ed7ab910c77d9d98b4c9da3fe2e (diff) | |
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/Csem.v')
| -rw-r--r-- | cfrontend/Csem.v | 15 |
1 files changed, 10 insertions, 5 deletions
diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v index 5e4f4e3..2213912 100644 --- a/cfrontend/Csem.v +++ b/cfrontend/Csem.v @@ -564,6 +564,16 @@ Inductive eval_expr: expr -> val -> Prop := eval_expr a2 v2 -> sem_binary_operation op v1 (typeof a1) v2 (typeof a2) m = Some v -> eval_expr (Expr (Ebinop op a1 a2) ty) v + | eval_Econdition_true: forall a1 a2 a3 ty v1 v2, + eval_expr a1 v1 -> + is_true v1 (typeof a1) -> + eval_expr a2 v2 -> + eval_expr (Expr (Econdition a1 a2 a3) ty) v2 + | eval_Econdition_false: forall a1 a2 a3 ty v1 v3, + eval_expr a1 v1 -> + is_false v1 (typeof a1) -> + eval_expr a3 v3 -> + eval_expr (Expr (Econdition a1 a2 a3) ty) v3 | eval_Eorbool_1: forall a1 a2 ty v1, eval_expr a1 v1 -> is_true v1 (typeof a1) -> @@ -604,11 +614,6 @@ with eval_lvalue: expr -> block -> int -> Prop := | eval_Ederef: forall a ty l ofs, eval_expr a (Vptr l ofs) -> eval_lvalue (Expr (Ederef a) ty) l ofs - | eval_Eindex: forall a1 a2 ty v1 v2 l ofs, - eval_expr a1 v1 -> - eval_expr a2 v2 -> - sem_add v1 (typeof a1) v2 (typeof a2) = Some (Vptr l ofs) -> - eval_lvalue (Expr (Eindex a1 a2) ty) l ofs | eval_Efield_struct: forall a i ty l ofs id fList delta, eval_lvalue a l ofs -> typeof a = Tstruct id fList -> |