From d6d7700a5018f1cbdd1b6635374cab94835e2e3d Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Fri, 26 Jul 2019 15:49:59 +0200
Subject: [PATCH] [Libc] Define bit_test in new __fc_integer.h
---
headers/header_spec.txt | 1 +
share/libc/__fc_integer.h | 36 ++++++++++++++++++++
src/kernel_internals/typing/logic_builtin.ml | 3 +-
tests/libc/oracle/fc_libc.2.res.oracle | 1 +
tests/libc/oracle/fc_libc.5.res.oracle | 1 +
5 files changed, 40 insertions(+), 2 deletions(-)
create mode 100644 share/libc/__fc_integer.h
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 166fbddd62c..59c6054d6c1 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -202,6 +202,7 @@ share/libc/__fc_define_wchar_t.h: CEA_LGPL
share/libc/__fc_define_wint_t.h: CEA_LGPL
share/libc/__fc_gcc_builtins.h: CEA_LGPL
share/libc/__fc_inet.h: CEA_LGPL
+share/libc/__fc_integer.h: CEA_LGPL
share/libc/__fc_machdep.h: CEA_LGPL
share/libc/__fc_machdep_linux_shared.h: CEA_LGPL
share/libc/__fc_runtime.c: CEA_LGPL
diff --git a/share/libc/__fc_integer.h b/share/libc/__fc_integer.h
new file mode 100644
index 00000000000..1dc5b29c85e
--- /dev/null
+++ b/share/libc/__fc_integer.h
@@ -0,0 +1,36 @@
+/**************************************************************************/
+/* */
+/* This file is part of Frama-C. */
+/* */
+/* Copyright (C) 2007-2019 */
+/* CEA (Commissariat à l'énergie atomique et aux énergies */
+/* alternatives) */
+/* */
+/* you can redistribute it and/or modify it under the terms of the GNU */
+/* Lesser General Public License as published by the Free Software */
+/* Foundation, version 2.1. */
+/* */
+/* It is distributed in the hope that it will be useful, */
+/* but WITHOUT ANY WARRANTY; without even the implied warranty of */
+/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */
+/* GNU Lesser General Public License for more details. */
+/* */
+/* See the GNU Lesser General Public License version 2.1 */
+/* for more details (enclosed in the file licenses/LGPLv2.1). */
+/* */
+/**************************************************************************/
+
+
+#ifndef Frama_C_INTEGER
+#define Frama_C_INTEGER
+#include "features.h"
+__PUSH_FC_STDLIB
+
+/*@
+
+ logic boolean bit_test(integer x, integer pos) = (boolean)(x & (1<<pos));
+
+ */
+
+__POP_FC_STDLIB
+#endif
diff --git a/src/kernel_internals/typing/logic_builtin.ml b/src/kernel_internals/typing/logic_builtin.ml
index 355bb752958..ae1a73a9713 100644
--- a/src/kernel_internals/typing/logic_builtin.ml
+++ b/src/kernel_internals/typing/logic_builtin.ml
@@ -161,8 +161,7 @@ let init =
"\\pointer_comparable", [], [], [("p1", fun_ptr);
("p2", object_ptr)];
"\\pointer_comparable", [], [], [("p1", object_ptr);
- ("p2", fun_ptr)];
- "\\bit_test", [], [], ["x", Linteger; "pos", Linteger] ;
+ ("p2", fun_ptr)];
];
(* functions *)
List.iter
diff --git a/tests/libc/oracle/fc_libc.2.res.oracle b/tests/libc/oracle/fc_libc.2.res.oracle
index fc16d42e535..e85ef1cf9e1 100644
--- a/tests/libc/oracle/fc_libc.2.res.oracle
+++ b/tests/libc/oracle/fc_libc.2.res.oracle
@@ -36,6 +36,7 @@
[kernel] Parsing share/libc/__fc_define_wint_t.h (with preprocessing)
[kernel] Parsing share/libc/__fc_gcc_builtins.h (with preprocessing)
[kernel] Parsing share/libc/__fc_inet.h (with preprocessing)
+[kernel] Parsing share/libc/__fc_integer.h (with preprocessing)
[kernel] Parsing share/libc/__fc_machdep.h (with preprocessing)
skipping share/libc/__fc_machdep_linux_shared.h
[kernel] Parsing share/libc/__fc_select.h (with preprocessing)
diff --git a/tests/libc/oracle/fc_libc.5.res.oracle b/tests/libc/oracle/fc_libc.5.res.oracle
index e69de29bb2d..73dac90425a 100644
--- a/tests/libc/oracle/fc_libc.5.res.oracle
+++ b/tests/libc/oracle/fc_libc.5.res.oracle
@@ -0,0 +1 @@
+#include "__fc_integer.h"
--
GitLab