diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-04-17 13:27:48 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-04-17 13:27:48 +0000 |
| commit | d1cdc0496d7d52e3ab91554dbf53fcc0e7f244eb (patch) | |
| tree | 4fb435a847b0a1f1fd0afc93eb718c459e2aa0d6 /cfrontend | |
| parent | ed39cb168c0ca6c979db9059d39213d4f2a59eb5 (diff) | |
| download | compcert-d1cdc0496d7d52e3ab91554dbf53fcc0e7f244eb.tar.gz compcert-d1cdc0496d7d52e3ab91554dbf53fcc0e7f244eb.zip | |
Various clean-upsv1.4
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1033 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'cfrontend')
| -rw-r--r-- | cfrontend/Cil2Csyntax.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/cfrontend/Cil2Csyntax.ml b/cfrontend/Cil2Csyntax.ml index e9feb534..efaf42e4 100644 --- a/cfrontend/Cil2Csyntax.ml +++ b/cfrontend/Cil2Csyntax.ml @@ -557,11 +557,11 @@ let makeFuncall1 tyfun (Expr(_, tlhs) as elhs) efun eargs = | TFun (t, _, _, _) -> let tres = convertTyp t in if tlhs = tres then - Scall(Datatypes.Some elhs, efun, eargs) + Scall(Some elhs, efun, eargs) else begin let tmp = make_temp t in let elhs' = Expr(Evar tmp, tres) in - Ssequence(Scall(Datatypes.Some elhs', efun, eargs), + Ssequence(Scall(Some elhs', efun, eargs), Sassign(elhs, Expr(Ecast(tlhs, elhs'), tlhs))) end | _ -> internal_error "wrong type for function in call" @@ -590,7 +590,7 @@ let rec processInstrList l = | Call (None, e, eList, loc) -> updateLoc(loc); let (efun, params) = convertExpFuncall e eList in - Scall(Datatypes.None, efun, params) + Scall(None, efun, params) | Call (Some lv, e, eList, loc) -> updateLoc(loc); let (efun, params) = convertExpFuncall e eList in @@ -679,8 +679,8 @@ and convertStmt s = | Return (eOpt, loc) -> updateLoc(loc); let eOpt' = match eOpt with - | None -> Datatypes.None - | Some e -> Datatypes.Some (convertExp e) + | None -> None + | Some e -> Some (convertExp e) in Sreturn eOpt' | Goto (_, loc) -> |