From e37d620f5b9b05e16563545cba9c538f8d31c746 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 17 Sep 2006 08:59:43 +0000 Subject: Bug dans le traitement des fonctions variadiques. Tolerer les chaines litterales dans les initialiseurs. Forcer evaluation gauche-droite pour avoir les erreurs et warnings dans l'ordre du source. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@103 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- caml/Cil2Csyntax.ml | 79 ++++++++++++++++++++++++++++++++++++----------------- 1 file changed, 54 insertions(+), 25 deletions(-) diff --git a/caml/Cil2Csyntax.ml b/caml/Cil2Csyntax.ml index c0e4837f..afd5077a 100644 --- a/caml/Cil2Csyntax.ml +++ b/caml/Cil2Csyntax.ml @@ -139,24 +139,24 @@ let globals_for_strings globs = let stub_function_table = Hashtbl.create 47 let register_stub_function name tres targs = + let rec letters_of_type = function + | Tnil -> [] + | Tcons(Tfloat _, tl) -> "f" :: letters_of_type tl + | Tcons(_, tl) -> "i" :: letters_of_type tl in + let stub_name = + name ^ "$" ^ String.concat "" (letters_of_type targs) in try - Hashtbl.find stub_function_table name + (stub_name, Hashtbl.find stub_function_table stub_name) with Not_found -> - let rec letters_of_type = function - | Tnil -> [] - | Tcons(Tfloat _, tl) -> "f" :: letters_of_type tl - | Tcons(_, tl) -> "i" :: letters_of_type tl in - let stub_name = - name ^ "$" ^ String.concat "" (letters_of_type targs) in let rec types_of_types = function | Tnil -> Tnil | Tcons(Tfloat _, tl) -> Tcons(Tfloat F64, types_of_types tl) | Tcons(_, tl) -> Tcons(Tpointer Tvoid, types_of_types tl) in let stub_type = Tfunction (types_of_types targs, tres) in - Hashtbl.add stub_function_table name (stub_name, stub_type); + Hashtbl.add stub_function_table stub_name stub_type; (stub_name, stub_type) -let declare_stub_function name (stub_name, stub_type) = +let declare_stub_function stub_name stub_type = match stub_type with | Tfunction(targs, tres) -> Datatypes.Coq_pair(intern_string stub_name, @@ -547,14 +547,20 @@ let rec processInstrList l = match l with | [] -> Sskip | [s] -> convertInstr s - | s :: l -> Ssequence (convertInstr s, processInstrList l) + | s :: l -> + let cs = convertInstr s in + let cl = processInstrList l in + Ssequence (cs, cl) (** Convert a [Cil.stmt list] into a [CabsCoq.statement] *) let rec processStmtList = function | [] -> Sskip | [s] -> convertStmt s - | s :: l -> Ssequence (convertStmt s, processStmtList l) + | s :: l -> + let cs = convertStmt s in + let cl = processStmtList l in + Ssequence (cs, cl) (** Return the list of the constant expressions in a label list @@ -691,7 +697,8 @@ let rec initDataLen accu = function | Init_int32 _ -> 4l | Init_float32 _ -> 4l | Init_float64 _ -> 8l - | Init_space n -> camlint_of_z n in + | Init_space n -> camlint_of_z n + | Init_pointer _ -> 4l in initDataLen (Int32.add sz accu) il (** Convert a [Cil.init] into a list of [AST.init_data] prepended to @@ -703,6 +710,7 @@ let rec initDataLen accu = function type init_constant = | ICint of int64 * intsize | ICfloat of float * floatsize + | ICstring of string | ICnone let rec extract_constant e = @@ -711,6 +719,8 @@ let rec extract_constant e = ICint(n, fst (convertIkind ikind)) | Const (CReal(n, fkind, _)) -> ICfloat(n, convertFkind fkind) + | Const (CStr s) -> + ICstring s | CastE (ty, e1) -> begin match extract_constant e1, convertTyp ty with | ICfloat(n, _), Tfloat sz -> @@ -719,6 +729,8 @@ let rec extract_constant e = ICfloat(Int64.to_float n, sz) | ICint(n, sz), Tpointer _ -> ICint(n, sz) + | ICstring s, (Tint _ | Tpointer _) -> + ICstring s | _, _ -> ICnone end @@ -729,6 +741,14 @@ let rec extract_constant e = end | _ -> ICnone +let init_data_of_string s = + let id = ref CList.Coq_nil in + for i = String.length s - 1 downto 0 do + let n = coqint_of_camlint(Int32.of_int(Char.code s.[i])) in + id := CList.Coq_cons(Init_int8 n, !id) + done; + !id + let rec convertInit init k = match init with | SingleInit e -> @@ -743,6 +763,8 @@ let rec convertInit init k = CList.Coq_cons(Init_float32 n, k) | ICfloat(n, F64) -> CList.Coq_cons(Init_float64 n, k) + | ICstring s -> + CList.Coq_cons(Init_pointer(init_data_of_string s), k) | ICnone -> unsupported "this kind of expression is not supported in global initializers" end @@ -816,13 +838,12 @@ let convertExtFun v = let rec processGlobals = function | [] -> (CList.Coq_nil, CList.Coq_nil) | g :: l -> - let (fList, vList) as rem = processGlobals l in match g with - | GType _ -> rem (* typedefs are unrolled... *) - | GCompTag _ -> rem - | GCompTagDecl _ -> rem - | GEnumTag _ -> rem (* enum constants are folded... *) - | GEnumTagDecl _ -> rem + | GType _ -> processGlobals l (* typedefs are unrolled... *) + | GCompTag _ -> processGlobals l + | GCompTagDecl _ -> processGlobals l + | GEnumTag _ -> processGlobals l (* enum constants are folded... *) + | GEnumTagDecl _ -> processGlobals l | GVarDecl (v, loc) -> updateLoc(loc); (* Functions become external declarations, @@ -830,26 +851,34 @@ let rec processGlobals = function variables become uninitialized variables *) begin match Cil.unrollType v.vtype with | TFun (tres, Some targs, false, _) -> - (CList.Coq_cons (convertExtFun v, fList), vList) + let fn = convertExtFun v in + let (fList, vList) = processGlobals l in + (CList.Coq_cons (fn, fList), vList) | TFun (tres, _, _, _) -> - rem + processGlobals l | _ -> - (fList, CList.Coq_cons (convertExtVar v, vList)) + let var = convertExtVar v in + let (fList, vList) = processGlobals l in + (fList, CList.Coq_cons (var, vList)) end | GVar (v, init, loc) -> updateLoc(loc); - (fList, CList.Coq_cons (convertGVar v init, vList)) + let var = convertGVar v init in + let (fList, vList) = processGlobals l in + (fList, CList.Coq_cons (var, vList)) | GFun (fdec, loc) -> updateLoc(loc); - (CList.Coq_cons (convertGFun fdec, fList), vList) + let fn = convertGFun fdec in + let (fList, vList) = processGlobals l in + (CList.Coq_cons (fn, fList), vList) | GAsm (_, loc) -> updateLoc(loc); unsupported "inline assembly" | GPragma (_, loc) -> updateLoc(loc); warning "#pragma directive ignored"; - rem - | GText _ -> rem (* comments are ignored *) + processGlobals l + | GText _ -> processGlobals l (* comments are ignored *) (** Eliminate forward declarations of globals that are defined later *) -- cgit