diff options
| author | Alasdair Armstrong | 2018-06-04 16:58:14 +0100 |
|---|---|---|
| committer | Alasdair Armstrong | 2018-06-04 16:58:14 +0100 |
| commit | 80384aeee9482b481b7c1d23a3155098c5d90d28 (patch) | |
| tree | 1dcbbd7dce63eff04adaa5eab169faed18fa2589 /src | |
| parent | 2c533959ae0bc96d5e648497a74a79e430d4feea (diff) | |
Fix bug with function return types in C backend
Diffstat (limited to 'src')
| -rw-r--r-- | src/c_backend.ml | 7 | ||||
| -rw-r--r-- | src/sail.ml | 4 |
2 files changed, 10 insertions, 1 deletions
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 |