diff options
Diffstat (limited to 'cfrontend/Csyntax.v')
| -rw-r--r-- | cfrontend/Csyntax.v | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/cfrontend/Csyntax.v b/cfrontend/Csyntax.v index 8b98556..ea1bd86 100644 --- a/cfrontend/Csyntax.v +++ b/cfrontend/Csyntax.v @@ -177,6 +177,7 @@ with labeled_statements : Type := (**r cases of a [switch] *) Record function : Type := mkfunction { fn_return: type; + fn_callconv: calling_convention; fn_params: list (ident * type); fn_vars: list (ident * type); fn_body: statement @@ -190,17 +191,17 @@ Definition var_names (vars: list(ident * type)) : list ident := Inductive fundef : Type := | Internal: function -> fundef - | External: external_function -> typelist -> type -> fundef. + | External: external_function -> typelist -> type -> calling_convention -> fundef. (** The type of a function definition. *) Definition type_of_function (f: function) : type := - Tfunction (type_of_params (fn_params f)) (fn_return f). + Tfunction (type_of_params (fn_params f)) (fn_return f) (fn_callconv f). Definition type_of_fundef (f: fundef) : type := match f with | Internal fd => type_of_function fd - | External id args res => Tfunction args res + | External id args res cc => Tfunction args res cc end. (** ** Programs *) |