From feaa6b09d9aadffd552736e00543d0309d3eabeb Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Tue, 18 Dec 2018 15:28:11 +0100
Subject: [PATCH] [Aorai] Add aorai.h header file to be able to
Frama_C_show_each states variables.
---
Makefile | 2 +-
headers/header_spec.txt | 1 +
share/libc/aorai/aorai.h | 33 ++++++++++++++++++++++++++
src/plugins/aorai/aorai_utils.ml | 15 +++++++++++-
tests/libc/oracle/fc_libc.2.res.oracle | 1 +
tests/libc/oracle/fc_libc.5.res.oracle | 1 +
6 files changed, 51 insertions(+), 2 deletions(-)
create mode 100644 share/libc/aorai/aorai.h
diff --git a/Makefile b/Makefile
index 0f4ac62279f..930b19a61c5 100644
--- a/Makefile
+++ b/Makefile
@@ -191,7 +191,7 @@ THEME_ICONS_FLAT:= \
$(addprefix share/theme/flat/,$(THEME_ICON_NAMES))
ROOT_LIBC_DIR:= share/libc
-LIBC_SUBDIRS:= sys netinet net arpa
+LIBC_SUBDIRS:= sys netinet net arpa aorai
LIBC_DIR:= $(ROOT_LIBC_DIR) $(addprefix $(ROOT_LIBC_DIR)/,$(LIBC_SUBDIRS))
LIBC_FILES:= \
$(wildcard share/*.h share/*.c) \
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index d1b383e76b2..69a036f5610 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -208,6 +208,7 @@ share/libc/__fc_runtime.c: CEA_LGPL
share/libc/__fc_select.h: CEA_LGPL
share/libc/__fc_string_axiomatic.h: CEA_LGPL
share/libc/alloca.h: CEA_LGPL
+share/libc/aorai/aorai.h: CEA_LGPL
share/libc/arpa/inet.h: CEA_LGPL
share/libc/assert.c: CEA_LGPL
share/libc/assert.h: CEA_LGPL
diff --git a/share/libc/aorai/aorai.h b/share/libc/aorai/aorai.h
new file mode 100644
index 00000000000..b2f5eeb733f
--- /dev/null
+++ b/share/libc/aorai/aorai.h
@@ -0,0 +1,33 @@
+/**************************************************************************/
+/* */
+/* This file is part of Frama-C. */
+/* */
+/* Copyright (C) 2007-2020 */
+/* 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 __FC_AORAI
+#define __FC_AORAI
+
+/*@ ghost extern int aorai_CurStates; */
+/*@ ghost extern int aorai_StatesHistory1; */
+/*@ ghost extern int aorai_StatesHistory2; */
+/*@ ghost extern int aorai_StatesHistory3; */
+/*@ ghost extern int aorai_StatesHistory4; */
+
+
+#endif
diff --git a/src/plugins/aorai/aorai_utils.ml b/src/plugins/aorai/aorai_utils.ml
index 274932dd15c..14530aceb21 100644
--- a/src/plugins/aorai/aorai_utils.ml
+++ b/src/plugins/aorai/aorai_utils.ml
@@ -680,6 +680,7 @@ let add_global glob = globals_queue := glob :: !globals_queue
let add_gvar ?init vi =
let initinfo = {Cil_types.init} in
vi.vghost <- true;
+ vi.vstorage <- NoStorage;
add_global (GVar(vi,initinfo,vi.vdecl));
Globals.Vars.add vi initinfo;
set_varinfo vi.vname vi
@@ -688,7 +689,19 @@ let add_gvar_zeroinit vi =
add_gvar ~init:(Cil.makeZeroInit ~loc:(CurrentLoc.get()) vi.vtype) vi
let mk_gvar ?init ~ty name =
- let vi = Cil.makeGlobalVar name ty in
+ (* See if the variable is already declared *)
+ let vi =
+ try
+ let ty' = typeAddAttributes [Attr ("ghost", [])] ty in
+ let vi = Globals.Vars.find_from_astinfo name VGlobal in
+ if not (Cil_datatype.Typ.equal vi.vtype ty') then
+ Aorai_option.abort "Global %s is declared with type %a instead of %a"
+ name Cil_printer.pp_typ vi.vtype Cil_printer.pp_typ ty';
+ Globals.Vars.remove vi;
+ vi
+ with Not_found ->
+ Cil.makeGlobalVar name ty
+ in
add_gvar ?init vi
let mk_gvar_scalar ~init ?(ty = Cil.typeOf init) name =
diff --git a/tests/libc/oracle/fc_libc.2.res.oracle b/tests/libc/oracle/fc_libc.2.res.oracle
index b1e1247a436..852a3378808 100644
--- a/tests/libc/oracle/fc_libc.2.res.oracle
+++ b/tests/libc/oracle/fc_libc.2.res.oracle
@@ -42,6 +42,7 @@ skipping share/libc/__fc_machdep_linux_shared.h
[kernel] Parsing share/libc/__fc_select.h (with preprocessing)
[kernel] Parsing share/libc/__fc_string_axiomatic.h (with preprocessing)
[kernel] Parsing share/libc/alloca.h (with preprocessing)
+[kernel] Parsing share/libc/aorai/aorai.h (with preprocessing)
[kernel] Parsing share/libc/arpa/inet.h (with preprocessing)
[kernel] Parsing share/libc/assert.h (with preprocessing)
[kernel] Parsing share/libc/byteswap.h (with preprocessing)
diff --git a/tests/libc/oracle/fc_libc.5.res.oracle b/tests/libc/oracle/fc_libc.5.res.oracle
index 73dac90425a..3c89feea03b 100644
--- a/tests/libc/oracle/fc_libc.5.res.oracle
+++ b/tests/libc/oracle/fc_libc.5.res.oracle
@@ -1 +1,2 @@
#include "__fc_integer.h"
+#include "aorai/aorai.h"
--
GitLab