Unsupported: return/return type mismatches

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1180 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 17 insertions, 2 deletions

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) ->