From 780ad9d001af651a49d7470e963ed9a49ee11a4c Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 19 Jul 2019 19:49:46 +0200 Subject: various fixes --- mppa_k1c/CBuiltins.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'mppa_k1c/CBuiltins.ml') diff --git a/mppa_k1c/CBuiltins.ml b/mppa_k1c/CBuiltins.ml index 2f80c90f..09a9ba97 100644 --- a/mppa_k1c/CBuiltins.ml +++ b/mppa_k1c/CBuiltins.ml @@ -18,11 +18,11 @@ open C let builtins = { - Builtins.typedefs = [ + builtin_typedefs = [ "__builtin_va_list", TPtr(TVoid [], []) ]; (* The builtin list is inspired from the GCC file builtin_k1.h *) - Builtins.functions = [ (* Some builtins are commented out because their opcode is not present (yet?) *) + builtin_functions = [ (* Some builtins are commented out because their opcode is not present (yet?) *) (* BCU Instructions *) "__builtin_k1_await", (TVoid [], [], false); (* DONE *) "__builtin_k1_barrier", (TVoid [], [], false); (* DONE *) -- cgit