diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2015-05-21 15:20:54 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2015-05-21 15:20:54 +0200 |
| commit | b686f8df572ea77c8832637bed4e4cd81f0931e2 (patch) | |
| tree | 49d7921708c2dbb874dd7b53d0d74d9416735cb2 /cfrontend/C2C.ml | |
| parent | 2a26429f28bea6356521135c632ddb9a8b11c018 (diff) | |
| download | compcert-b686f8df572ea77c8832637bed4e4cd81f0931e2.tar.gz compcert-b686f8df572ea77c8832637bed4e4cd81f0931e2.zip | |
Ctyping: better typing of conditional expressions.
Ctyping: define a typechecker for whole programs.
Csyntax: introduce the type "pre-program" (non-dependent).
C2C: use Ctyping.econdition instead of Ctyping.econdition'.
Note: Ctyping.typecheck_program could be used as the first step
in the verified compilation pipeline. Then, retyping would
no longer be performed in C2C. We keep it this way (for the time
being) because retyping errors are reported more precisely in C2C than
in Ctyping.
Diffstat (limited to 'cfrontend/C2C.ml')
| -rw-r--r-- | cfrontend/C2C.ml | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 6ecdb14e..a0e6b259 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -626,7 +626,6 @@ let ewrap = function error ("retyping error: " ^ string_of_errmsg msg); ezero let rec convertExpr env e = - (*let ty = convertTyp env e.etyp in*) match e.edesc with | C.EVar _ | C.EUnop((C.Oderef|C.Odot _|C.Oarrow _), _) @@ -734,9 +733,8 @@ let rec convertExpr env e = ewrap (Ctyping.eseqor (convertExpr env e1) (convertExpr env e2)) | C.EConditional(e1, e2, e3) -> - ewrap (Ctyping.econdition' (convertExpr env e1) - (convertExpr env e2) (convertExpr env e3) - (convertTyp env e.etyp)) + ewrap (Ctyping.econdition (convertExpr env e1) + (convertExpr env e2) (convertExpr env e3)) | C.ECast(ty1, e1) -> ewrap (Ctyping.ecast (convertTyp env ty1) (convertExpr env e1)) | C.ECompound(ty1, ie) -> |