From 73729d23ac13275c0d28d23bc1b1f6056104e5d9 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Mon, 4 Sep 2006 15:08:29 +0000
Subject: Fusion de la branche "traces": - Ajout de traces d'evenements d'E/S
 dans les semantiques - Ajout constructions switch et allocation dynamique -
 Initialisation des variables globales - Portage Coq 8.1 beta Debut
 d'integration du front-end C: - Traduction Clight -> Csharpminor dans
 cfrontend/ - Modifications de Csharpminor et Globalenvs en consequence.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@72 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 caml/CMtypecheck.ml | 22 ++++++++++++++++++++--
 1 file changed, 20 insertions(+), 2 deletions(-)

(limited to 'caml/CMtypecheck.ml')

diff --git a/caml/CMtypecheck.ml b/caml/CMtypecheck.ml
index b6f94cb5..4e700d7a 100644
--- a/caml/CMtypecheck.ml
+++ b/caml/CMtypecheck.ml
@@ -5,6 +5,7 @@ open Datatypes
 open CList
 open Camlcoq
 open AST
+open Integers
 open Op
 open Cminor
 
@@ -95,6 +96,8 @@ let type_operation = function
   | Oundef -> [], newvar()
   | Ocast8signed -> [tint], tint
   | Ocast16signed -> [tint], tint
+  | Ocast8unsigned -> [tint], tint
+  | Ocast16unsigned -> [tint], tint
   | Oadd -> [tint;tint], tint
   | Oaddimm _ -> [tint], tint
   | Osub -> [tint;tint], tint
@@ -141,6 +144,8 @@ let name_of_operation = function
   | Oundef -> "undef"
   | Ocast8signed -> "cast8signed"
   | Ocast16signed -> "cast16signed"
+  | Ocast8unsigned -> "cast8unsigned"
+  | Ocast16unsigned -> "cast16unsigned"
   | Oadd -> "add"
   | Oaddimm n -> sprintf "addimm %ld" (camlint_of_coqint n)
   | Osub -> "sub"
@@ -282,6 +287,14 @@ let rec type_expr env lenv e =
       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
@@ -349,7 +362,7 @@ let rec env_of_vars idl =
   | Coq_nil -> []
   | Coq_cons(id1, idt) -> (id1, newvar()) :: env_of_vars idt
 
-let type_function (Coq_pair (id, f)) =
+let type_function id f =
   try
     type_stmt
        (env_of_vars f.fn_vars @ env_of_vars f.fn_params)
@@ -357,5 +370,10 @@ let type_function (Coq_pair (id, f)) =
   with Error s ->
     raise (Error (sprintf "In function %s:\n%s" (extern_atom id) s))
 
+let type_fundef (Coq_pair (id, fd)) =
+  match fd with
+  | Internal f -> type_function id f
+  | External ef -> ()
+
 let type_program p =
-  coqlist_iter type_function p.prog_funct; p
+  coqlist_iter type_fundef p.prog_funct; p
-- 
cgit