diff --git a/Makefile b/Makefile index 28451af1bde84efb01405623c879d8b6e484c148..6f81e3247d49e8e5aeb35f01ff837af880223858 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 851b5ea6c501d1c94e0741beed7d7c86e9624e9e..d4749f980bdb0fbd931b0c583d2f3026afbfd2ff 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 0fc464a048d289bc5fbfd637d31e02ec362bb32a..7162412e2f9847ccc2bfc14236e81e051e4a53f1 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 9da4452f3ffd01473f61840f8a2f2bccbfe50a23..865406c581f36242819527b53db1098cb81074e8 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 "$@"