diff options
Diffstat (limited to 'arm/Conventions1.v')
| -rw-r--r-- | arm/Conventions1.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/arm/Conventions1.v b/arm/Conventions1.v index 45008bff..7016c1ee 100644 --- a/arm/Conventions1.v +++ b/arm/Conventions1.v @@ -641,3 +641,9 @@ Proof. unfold loc_arguments. destruct Archi.abi; reflexivity. Qed. + +(** ** Normalization of function results *) + +(** No normalization needed. *) + +Definition return_value_needs_normalization (t: rettype) := false. |