From 571a9c7bad15bc8f99a20499287921f2e3b8ad87 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Mon, 23 Oct 2006 09:01:33 +0000
Subject: [PATCH] Verification du type de retour de main()
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@126 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
caml/Cil2Csyntax.ml | 18 ++++++++----------
1 file changed, 8 insertions(+), 10 deletions(-)
diff --git a/caml/Cil2Csyntax.ml b/caml/Cil2Csyntax.ml
index c41ddeb96..126e88a5b 100644
--- a/caml/Cil2Csyntax.ml
+++ b/caml/Cil2Csyntax.ml
@@ -32,7 +32,6 @@ let const0 = Expr (Econst_int (coqint_of_camlint Int32.zero), constInt32)
(** Global variables *)
let currentLocation = ref Cil.locUnknown
-let mainFound = ref false
let currentGlobalPrefix = ref ""
let stringNum = ref 0 (* number of next global for string literals *)
let stringTable = Hashtbl.create 47
@@ -706,10 +705,14 @@ let convertGFun fdec =
let args = map_coqlist convertVarinfoParam fdec.sformals in (* parameters*)
let varList = map_coqlist convertVarinfo fdec.slocals in (* local vars *)
let s = processStmtList fdec.sbody.bstmts in (* function body *)
- if v.vname = "main" then mainFound := true;
- Datatypes.Coq_pair
- (intern_string v.vname,
- Internal { fn_return=ret; fn_params=args; fn_vars=varList; fn_body=s })
+ if v.vname = "main" then begin
+ match ret with
+ | Tint(_, _) -> ()
+ | _ -> unsupported "the return type of main() must be an integer type"
+ end;
+ Datatypes.Coq_pair
+ (intern_string v.vname,
+ Internal { fn_return=ret; fn_params=args; fn_vars=varList; fn_body=s })
(** Auxiliary for [convertInit] *)
@@ -933,11 +936,6 @@ let convertFile f =
| Some fdec -> CList.Coq_cons (convertGFun fdec, funList')
| None -> funList' in
let defList' = globals_for_strings defList in
-(***
- if not !mainFound then (* no main function *)
- warning "program has no main function! (you should \
- probably have used ccomp's -nomain option)\n";
-***)
{ AST.prog_funct = funList'';
AST.prog_vars = defList';
AST.prog_main = intern_string "main" }
--
GitLab