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 /cfrontend/Ctypes.v | |
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 'cfrontend/Ctypes.v')
-rw-r--r-- | cfrontend/Ctypes.v | 19 |
1 files changed, 16 insertions, 3 deletions
diff --git a/cfrontend/Ctypes.v b/cfrontend/Ctypes.v index bfc5daa9..664a60c5 100644 --- a/cfrontend/Ctypes.v +++ b/cfrontend/Ctypes.v @@ -732,8 +732,21 @@ Definition typ_of_type (t: type) : AST.typ := | Tpointer _ _ | Tarray _ _ _ | Tfunction _ _ _ | Tstruct _ _ | Tunion _ _ => AST.Tptr end. -Definition opttyp_of_type (t: type) : option AST.typ := - if type_eq t Tvoid then None else Some (typ_of_type t). +Definition rettype_of_type (t: type) : AST.rettype := + match t with + | Tvoid => AST.Tvoid + | Tint I32 _ _ => AST.Tint + | Tint I8 Signed _ => AST.Tint8signed + | Tint I8 Unsigned _ => AST.Tint8unsigned + | Tint I16 Signed _ => AST.Tint16signed + | Tint I16 Unsigned _ => AST.Tint16unsigned + | Tint IBool _ _ => AST.Tint8unsigned + | Tlong _ _ => AST.Tlong + | Tfloat F32 _ => AST.Tsingle + | Tfloat F64 _ => AST.Tfloat + | Tpointer _ _ => AST.Tptr + | Tarray _ _ _ | Tfunction _ _ _ | Tstruct _ _ | Tunion _ _ => AST.Tvoid + end. Fixpoint typlist_of_typelist (tl: typelist) : list AST.typ := match tl with @@ -742,7 +755,7 @@ Fixpoint typlist_of_typelist (tl: typelist) : list AST.typ := end. Definition signature_of_type (args: typelist) (res: type) (cc: calling_convention): signature := - mksignature (typlist_of_typelist args) (opttyp_of_type res) cc. + mksignature (typlist_of_typelist args) (rettype_of_type res) cc. (** * Construction of the composite environment *) |