diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2007-08-28 12:57:58 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2007-08-28 12:57:58 +0000 |
commit | c48b9097201dc9a1e326acdbce491fe16cab01e6 (patch) | |
tree | 53335d9dcb4aead3ec1f42e4138e87649640edd0 /caml/CMtypecheck.ml | |
parent | 2b89ae94ffb6dc56fa780acced8ab7ad0afbb3b5 (diff) | |
download | compcert-c48b9097201dc9a1e326acdbce491fe16cab01e6.tar.gz compcert-c48b9097201dc9a1e326acdbce491fe16cab01e6.zip |
Fusion de la branche restr-cminor. En Clight, C#minor et Cminor, les expressions sont maintenant pures et les appels de fonctions sont des statements. Ajout de semantiques coinductives pour la divergence en Clight, C#minor, Cminor. Preuve de preservation semantique pour les programmes qui divergent.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@409 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'caml/CMtypecheck.ml')
-rw-r--r-- | caml/CMtypecheck.ml | 76 |
1 files changed, 40 insertions, 36 deletions
diff --git a/caml/CMtypecheck.ml b/caml/CMtypecheck.ml index 495ded0c..9277829c 100644 --- a/caml/CMtypecheck.ml +++ b/caml/CMtypecheck.ml @@ -206,30 +206,6 @@ let rec type_expr env lenv e = (name_of_chunk chunk) s)) end; type_chunk chunk - | Estore(chunk, e1, e2) -> - let te1 = type_expr env lenv e1 in - let te2 = type_expr env lenv e2 in - begin try - unify tint te1; - unify (type_chunk chunk) te2 - with Error s -> - raise (Error (sprintf "In store %s:\n%s" - (name_of_chunk chunk) s)) - end; - te1 - | Ecall(sg, e1, el) -> - let te1 = type_expr env lenv e1 in - let tel = type_exprlist env lenv el in - begin try - unify tint te1; - unify_list (ty_of_sig_args sg.sig_args) tel - with Error s -> - raise (Error (sprintf "In call:\n%s" s)) - end; - begin match sg.sig_res with - | None -> tint (*???*) - | Some t -> ty_of_typ t - end | Econdition(e1, e2, e3) -> type_condexpr env lenv e1; let te2 = type_expr env lenv e2 in @@ -240,25 +216,19 @@ let rec type_expr env lenv e = raise (Error (sprintf "In conditional expression:\n%s" s)) end; te2 +(* | Elet(e1, e2) -> let te1 = type_expr env lenv e1 in let te2 = type_expr env (te1 :: lenv) e2 in te2 | Eletvar n -> type_letvar lenv n - | Ealloc e -> - let te = type_expr env lenv e in - begin try - unify tint te - with Error s -> - raise (Error (sprintf "In alloc:\n%s" s)) - end; - tint +*) and type_exprlist env lenv el = match el with - | Enil -> [] - | Econs (e1, et) -> + | Coq_nil -> [] + | Coq_cons (e1, et) -> let te1 = type_expr env lenv e1 in let tet = type_exprlist env lenv et in (te1 :: tet) @@ -274,8 +244,6 @@ and type_condexpr env lenv e = let rec type_stmt env blk ret s = match s with | Sskip -> () - | Sexpr e -> - ignore (type_expr env [] e) | Sassign(id, e1) -> let tid = type_var env id in let te1 = type_expr env [] e1 in @@ -284,6 +252,42 @@ let rec type_stmt env blk ret s = with Error s -> raise (Error (sprintf "In assignment to %s:\n%s" (extern_atom id) s)) end + | Sstore(chunk, e1, e2) -> + let te1 = type_expr env [] e1 in + let te2 = type_expr env [] e2 in + begin try + unify tint te1; + unify (type_chunk chunk) te2 + with Error s -> + raise (Error (sprintf "In store %s:\n%s" + (name_of_chunk chunk) s)) + end + | Scall(optid, sg, e1, el) -> + let te1 = type_expr env [] e1 in + let tel = type_exprlist env [] el in + begin try + unify tint te1; + unify_list (ty_of_sig_args sg.sig_args) tel; + let ty_res = + match sg.sig_res with + | None -> tint (*???*) + | Some t -> ty_of_typ t in + begin match optid with + | None -> () + | Some id -> unify (type_var env id) ty_res + end + with Error s -> + raise (Error (sprintf "In call:\n%s" s)) + end + | Salloc(id, e) -> + let tid = type_var env id in + let te = type_expr env [] e in + begin try + unify tint te; + unify tint tid + with Error s -> + raise (Error (sprintf "In alloc:\n%s" s)) + end | Sseq(s1, s2) -> type_stmt env blk ret s1; type_stmt env blk ret s2 |