aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--caml/Cil2Csyntax.ml3
1 files changed, 2 insertions, 1 deletions
diff --git a/caml/Cil2Csyntax.ml b/caml/Cil2Csyntax.ml
index 126e88a5..5fc31820 100644
--- a/caml/Cil2Csyntax.ml
+++ b/caml/Cil2Csyntax.ml
@@ -708,7 +708,8 @@ let convertGFun fdec =
if v.vname = "main" then begin
match ret with
| Tint(_, _) -> ()
- | _ -> unsupported "the return type of main() must be an integer type"
+ | _ -> updateLoc v.vdecl;
+ unsupported "the return type of main() must be an integer type"
end;
Datatypes.Coq_pair
(intern_string v.vname,