diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2022-03-10 16:50:47 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2022-03-10 16:50:47 +0100 |
| commit | 5987aafe3bf6b6382f0a90c9209a7c79be1cab3c (patch) | |
| tree | aa7fde39512393270b8a8d8076823aab5da0baa8 | |
| parent | c68661bd1eb5565e1272e039d7c2fa34086abf90 (diff) | |
| download | compcert-kvx-5987aafe3bf6b6382f0a90c9209a7c79be1cab3c.tar.gz compcert-kvx-5987aafe3bf6b6382f0a90c9209a7c79be1cab3c.zip | |
Small fixes to make extraction pass
| -rw-r--r-- | cparser/GCC.mli | 20 | ||||
| -rw-r--r-- | dune | 1 | ||||
| -rw-r--r-- | verilog/Machregsaux.ml | 2 | ||||
| -rw-r--r-- | verilog/Machregsaux.mli | 3 |
4 files changed, 6 insertions, 20 deletions
diff --git a/cparser/GCC.mli b/cparser/GCC.mli deleted file mode 100644 index 0163c98e..00000000 --- a/cparser/GCC.mli +++ /dev/null @@ -1,20 +0,0 @@ -(* *********************************************************************) -(* *) -(* 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 GNU Lesser General Public License as *) -(* published by the Free Software Foundation, either version 2.1 of *) -(* the License, or (at your option) any later version. *) -(* This file is also distributed under the terms of the *) -(* INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -(* GCC built-ins and attributes *) - -val builtins: Builtins.t -val attributes: (string * Cutil.attribute_class) list @@ -0,0 +1 @@ +(dirs :standard \ aarch64 arm x86_32 riscV powerpc extraction x86 x86_64 kvx) diff --git a/verilog/Machregsaux.ml b/verilog/Machregsaux.ml index 840943e7..46d08290 100644 --- a/verilog/Machregsaux.ml +++ b/verilog/Machregsaux.ml @@ -18,3 +18,5 @@ let class_of_type = function | AST.Tint | AST.Tlong -> 0 | AST.Tfloat | AST.Tsingle -> 1 | AST.Tany32 | AST.Tany64 -> assert false + +let nr_regs = [| 29; 32 |] diff --git a/verilog/Machregsaux.mli b/verilog/Machregsaux.mli index 01b0f9fd..23ac1c9a 100644 --- a/verilog/Machregsaux.mli +++ b/verilog/Machregsaux.mli @@ -15,3 +15,6 @@ val is_scratch_register: string -> bool val class_of_type: AST.typ -> int + +(* Number of registers in each class *) +val nr_regs : int array |