Refine the type of function results in AST.signature

Before it was "option typ".  Now it is a proper inductive type
that can also express small integer types (8/16-bit unsigned/signed integers).

One benefit is that external functions get more precise types that
control better their return values.  As a consequence,
the CompCert C type preservation property now holds unconditionally,
without extra typing hypotheses on external functions.

1 files changed, 10 insertions, 2 deletions

diff --git a/exportclight/ExportClight.ml b/exportclight/ExportClight.ml
index d86e137a..c9d6fced 100644
--- a/exportclight/ExportClight.ml
+++ b/exportclight/ExportClight.ml
@@ -18,7 +18,7 @@
 open Format
 open Camlcoq
 open AST
-open Ctypes
+open! Ctypes
 open Cop
 open Clight
 
@@ -221,6 +221,14 @@ let asttype p t =
       | AST.Tany32 -> "AST.Tany32"
       | AST.Tany64 -> "AST.Tany64")
 
+let astrettype p = function
+  | AST.Tret t -> asttype p t
+  | AST.Tvoid -> fprintf p "AST.Tvoid"
+  | AST.Tint8signed -> fprintf p "AST.Tint8signed"
+  | AST.Tint8unsigned -> fprintf p "AST.Tint8unsigned"
+  | AST.Tint16signed -> fprintf p "AST.Tint16signed"
+  | AST.Tint16unsigned -> fprintf p "AST.Tint16unsigned"
+
 let name_of_chunk = function
   | Mint8signed -> "Mint8signed"
   | Mint8unsigned -> "Mint8unsigned"
@@ -236,7 +244,7 @@ let name_of_chunk = function
 let signatur p sg =
   fprintf p "@[<hov 2>(mksignature@ %a@ %a@ %a)@]"
      (print_list asttype) sg.sig_args
-     (print_option asttype) sg.sig_res
+     astrettype sg.sig_res
      callconv sg.sig_cc
 
 let assertions = ref ([]: (string * typ list) list)