From d0ed98b8fd61a88cf8e9514015a8f2419fd59575 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Thu, 19 Nov 2009 13:02:54 +0000
Subject: Unsupported: return/return type mismatches

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1180 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 cfrontend/Cil2Csyntax.ml | 19 +++++++++++++++++--
 1 file changed, 17 insertions(+), 2 deletions(-)

(limited to 'cfrontend/Cil2Csyntax.ml')

diff --git a/cfrontend/Cil2Csyntax.ml b/cfrontend/Cil2Csyntax.ml
index 70252354..e5690aac 100644
--- a/cfrontend/Cil2Csyntax.ml
+++ b/cfrontend/Cil2Csyntax.ml
@@ -378,6 +378,14 @@ let cache_address ty e (f: expr -> statement) =
               f (Expr(Ederef(Expr(Evar t, typ)), ty)))
   end
 
+let current_function_return_type() =
+  match !current_function with
+  | None -> assert false
+  | Some f ->
+      match f.svar.vtype with
+      | TFun(ty_ret, ty_args, _, _) -> ty_ret
+      | _ -> assert false
+
 (** Detect and report GCC's __builtin_ functions *)
 
 let check_builtin s =
@@ -915,9 +923,16 @@ and convertStmtKind = function
         processInstrList iList
     | Return (eOpt, loc) ->
         updateLoc(loc);
+        let ty_ret = current_function_return_type() in
         let eOpt' = match eOpt with
-          | None -> None
-          | Some e -> Some (convertExp e)
+          | None -> 
+              if isVoidType ty_ret
+              then None
+              else unsupported ("`return' without a value in function with non-void return type")
+          | Some e -> 
+              if isVoidType ty_ret
+              then unsupported ("`return' with a value in function returning void")
+              else Some (convertExp e)
         in 
           Sreturn eOpt'
     | Goto (sref, loc) ->
-- 
cgit