add auxfile

71d69df1 · David Monniaux · ac7b7bd5 · 71d69df1
Commit 71d69df1 authored Apr 27, 2021 by David Monniaux
Hide whitespace changes
Inline Side-by-side

Showing with 17 additions and 0 deletions

aarch64/Machregsaux.mli aarch64/Machregsaux.mli +17 -0

No files found.
--- a/aarch64/Machregsaux.mli
+++ b/aarch64/Machregsaux.mli
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** Auxiliary functions on machine registers *)
+
+val is_scratch_register: string -> bool
+
+val class_of_type: AST.typ -> int