From 80384aeee9482b481b7c1d23a3155098c5d90d28 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Mon, 4 Jun 2018 16:58:14 +0100
Subject: Fix bug with function return types in C backend

---
 src/c_backend.ml | 7 ++++++-
 src/sail.ml      | 4 ++++
 2 files changed, 10 insertions(+), 1 deletion(-)

(limited to 'src')

diff --git a/src/c_backend.ml b/src/c_backend.ml
index 1371ad7d..1a150bb5 100644
--- a/src/c_backend.ml
+++ b/src/c_backend.ml
@@ -1564,8 +1564,13 @@ let compile_funcall ctx id args typ =
       setup := ifuncall (CL_id gs) id sargs ret_ctyp :: !setup;
       cleanup := iclear ret_ctyp gs :: !cleanup;
       fun ret -> iconvert ret final_ctyp gs ret_ctyp
+    else if is_stack_ctyp ret_ctyp && not (is_stack_ctyp final_ctyp) then
+      let gs = gensym () in
+      setup := idecl ret_ctyp gs :: !setup;
+      setup := ifuncall (CL_id gs) id sargs ret_ctyp :: !setup;
+      fun ret -> iconvert ret final_ctyp gs ret_ctyp
     else
-      assert false
+      c_error (Printf.sprintf "Funcall call type mismatch between %s and %s" (string_of_ctyp ret_ctyp) (string_of_ctyp final_ctyp))
   in
 
   (List.rev !setup, final_ctyp, call, !cleanup)
diff --git a/src/sail.ml b/src/sail.ml
index d6e8f972..c1ff267d 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -50,6 +50,8 @@
 
 open Process_file
 
+module Big_int = Nat_big_num
+
 let lib = ref ([] : string list)
 let opt_file_out : string option ref = ref None
 let opt_interactive = ref false
@@ -282,6 +284,8 @@ let main() =
          let open Elf_loader in
          let chan = open_out out in
          load_elf ~writer:(write_file chan) elf;
+         output_string chan "elf_entry\n";
+         output_string chan (Big_int.to_string !opt_elf_entry ^ "\n");
          close_out chan;
          exit 0
        end
-- 
cgit v1.2.3