diff options
author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2020-02-18 16:57:17 +0100 |
---|---|---|
committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2020-02-21 13:29:39 +0100 |
commit | be0b1872bf2ad36df9b0c7a0ffa63b9e77fa769b (patch) | |
tree | 0d54cce547d12567d7e9e9f2c4d650e5a1b94b39 /exportclight | |
parent | a9eaf4897c825093aba2137ff76e56bfbf1e72d5 (diff) | |
download | compcert-be0b1872bf2ad36df9b0c7a0ffa63b9e77fa769b.tar.gz compcert-be0b1872bf2ad36df9b0c7a0ffa63b9e77fa769b.zip |
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.
Diffstat (limited to 'exportclight')
-rw-r--r-- | exportclight/ExportClight.ml | 12 |
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) |