From 2705efe2f6627c709e6a387fc820580e23a124a7 Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Tue, 21 Sep 2021 17:00:48 +0200
Subject: [PATCH] [Eva] api: Do not insert header into Eva.mli
---
Makefile | 5 ++---
headers/header_spec.txt | 2 +-
src/plugins/value/Eva.mli | 22 ----------------------
src/plugins/value/gen-api.sh | 15 ---------------
4 files changed, 3 insertions(+), 41 deletions(-)
diff --git a/Makefile b/Makefile
index 28451af1bde..6f81e3247d4 100644
--- a/Makefile
+++ b/Makefile
@@ -930,16 +930,15 @@ PLUGIN_TYPES_CMO:=$(VALUE_TYPES)
PLUGIN_TYPES_TODOC:=$(addsuffix .mli,$(VALUE_TYPES))
# Eva API
-API_HEADER := headers/open-source/CEA_LGPL_OR_PROPRIETARY
API_MLI := $(addprefix $(PLUGIN_DIR)/, \
utils/results.mli utils/value_results.mli value_parameters.mli \
legacy/eval_terms.mli utils/unit_tests.mli utils/eva_annotations.mli \
eval.mli domains/cvalue/builtins.mli)
-$(PLUGIN_DIR)/Eva.mli: $(PLUGIN_DIR)/gen-api.sh Makefile $(API_HEADER) $(API_MLI)
+$(PLUGIN_DIR)/Eva.mli: $(PLUGIN_DIR)/gen-api.sh Makefile $(API_MLI)
$(PRINT_MAKING) $@
$(RM) $@ $@.tmp
- $< $(API_HEADER) $(API_MLI) > $@.tmp
+ $< $(API_MLI) > $@.tmp
$(CHMOD_RO) $@.tmp
$(MV) $@.tmp $@
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 851b5ea6c50..d4749f980bd 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -1315,7 +1315,7 @@ src/plugins/users/users_register.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/users/users_register.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/.merlin: .ignore
src/plugins/value/Changelog_non_free: .ignore
-src/plugins/value/Eva.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/Eva.mli: .ignore
src/plugins/value/alarmset.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/alarmset.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/api/general_requests.ml: CEA_LGPL_OR_PROPRIETARY
diff --git a/src/plugins/value/Eva.mli b/src/plugins/value/Eva.mli
index 0fc464a048d..7162412e2f9 100644
--- a/src/plugins/value/Eva.mli
+++ b/src/plugins/value/Eva.mli
@@ -1,25 +1,3 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2021 *)
-(* 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). *)
-(* *)
-(**************************************************************************)
-
(* This file is generated. Do not edit. *)
module Results: sig
diff --git a/src/plugins/value/gen-api.sh b/src/plugins/value/gen-api.sh
index 9da4452f3ff..865406c581f 100755
--- a/src/plugins/value/gen-api.sh
+++ b/src/plugins/value/gen-api.sh
@@ -1,20 +1,5 @@
#!/bin/bash -eu
-header=$1
-shift
-
-IFS='' # for read to keep spaces
-
-printf '('
-printf '%0.1s' '*'{1..74}
-printf ')\n'
-while read -r line
-do
- printf '(* %-68s *)\n' $line
-done < $header
-printf '('
-printf '%0.1s' '*'{1..74}
-printf ')\n\n'
printf '(* This file is generated. Do not edit. *)\n\n'
for i in "$@"
--
GitLab