From be0b1872bf2ad36df9b0c7a0ffa63b9e77fa769b Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 18 Feb 2020 16:57:17 +0100 Subject: 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. --- exportclight/ExportClight.ml | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) (limited to 'exportclight') 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 "@[(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) -- cgit