diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-07-19 18:59:44 +0200 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-07-19 18:59:44 +0200 |
commit | 4c379d48b35e7c8156f3953fede31d5e47faf8ca (patch) | |
tree | fa19eb30178fcf74b0768d9f5df4017ab6afc770 /mppa_k1c/Builtins1.v | |
parent | 3b79923a6c9fa8c76916df1eecfdecd7ae2124a5 (diff) | |
download | compcert-kvx-4c379d48b35e7c8156f3953fede31d5e47faf8ca.tar.gz compcert-kvx-4c379d48b35e7c8156f3953fede31d5e47faf8ca.zip |
helpers broke compilation
Diffstat (limited to 'mppa_k1c/Builtins1.v')
-rw-r--r-- | mppa_k1c/Builtins1.v | 33 |
1 files changed, 33 insertions, 0 deletions
diff --git a/mppa_k1c/Builtins1.v b/mppa_k1c/Builtins1.v new file mode 100644 index 00000000..f6e643d2 --- /dev/null +++ b/mppa_k1c/Builtins1.v @@ -0,0 +1,33 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, Collège de France and Inria Paris *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the GNU General Public License as published by *) +(* the Free Software Foundation, either version 2 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. *) +(* *) +(* *********************************************************************) + +(** Platform-specific built-in functions *) + +Require Import String Coqlib. +Require Import AST Integers Floats Values. +Require Import Builtins0. + +Inductive platform_builtin : Type := . + +Local Open Scope string_scope. + +Definition platform_builtin_table : list (string * platform_builtin) := + nil. + +Definition platform_builtin_sig (b: platform_builtin) : signature := + match b with end. + +Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (proj_sig_res (platform_builtin_sig b)) := + match b with end. |