Commit f21087cc authored by Patrick Baudin's avatar Patrick Baudin Committed by Julien Signoles
Browse files

[headers] compilation mode:

  internal: use of hdrck for targets headers, check-headers and src-distrib
  external: reviewed target headers
parent 56bc07be
(**************************************************************************)
(* *)
(* This file is part of Frama-C. *)
(* This file is part of the Frama-C's E-ACSL plug-in. *)
(* *)
(* Copyright (C) 2007-2018 *)
(* Copyright (C) 2012-2018 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
......
##########################################################################
# #
# This file is part of Frama-C. #
# This file is part of the Frama-C's E-ACSL plug-in. #
# #
# Copyright (C) 2007-2018 #
# Copyright (C) 2012-2018 #
# CEA (Commissariat à l'énergie atomique et aux énergies #
# alternatives) #
# #
......@@ -349,12 +349,19 @@ e-acsl-distrib-check:
# Header #
##########
EACSL_CEA_LGPL_BARE= *.ml *.mli Makefile.in configure.ac share/e-acsl/*.[ch] \
share/e-acsl/*/*.[ch] scripts/*.sh tests/print.ml man/e-acsl-gcc.sh.1
EACSL_CEA_LGPL=$(addprefix $(EACSL_PLUGIN_DIR)/, $(EACSL_CEA_LGPL_BARE))
ifneq ("$(FRAMAC_INTERNAL)","yes")
EACSL_SPARETIMELABS=$(EACSL_PLUGIN_DIR)/share/e-acsl/e_acsl_printf.h
EACSL_SHARE_BARE= share/e-acsl/*.[ch] share/e-acsl/*/*.[ch]
EACSL_SHARE=$(addprefix $(EACSL_PLUGIN_DIR)/, $(EACSL_SHARE_BARE))
EACSL_CEA_SHARE=$(filter-out $(EACSL_SPARETIMELABS), $(wildcard $(EACSL_SHARE)))
EACSL_CEA_LGPL_BARE= *.ml *.mli Makefile.in configure.ac \
scripts/*.sh tests/print.ml man/e-acsl-gcc.sh.1
EACSL_CEA_LGPL=$(addprefix $(EACSL_PLUGIN_DIR)/, $(EACSL_CEA_LGPL_BARE)) \
$(EACSL_CEA_SHARE)
# Files without header. contrib files keep their own header.
EACSL_NOHEADER_BARE=INSTALL README VERSION license/* \
doc/Changelog doc/doxygen/doxygen.cfg.in .depend tests/test_config.in \
......@@ -362,23 +369,24 @@ EACSL_NOHEADER_BARE=INSTALL README VERSION license/* \
EACSL_NOHEADER=$(addprefix $(EACSL_PLUGIN_DIR)/, $(EACSL_NOHEADER_BARE))
ifeq ("$(FRAMAC_INTERNAL)","yes")
CEA_LGPL_HEADER=$(FRAMAC_ROOT_SRCDIR)/headers/open-source/CEA_LGPL
# EACSL does not use hdrck mechanism
HEADER_EXCEPTIONS+=\
$(wildcard $(EACSL_CEA_LGPL) $(EACSL_SPARETIMELABS) $(EACSL_NOHEADER))
else
CEA_LGPL_HEADER=$(EACSL_PLUGIN_DIR)/license/CEA_LGPL
endif
# valid values: open-source, close-source
EACSL_HEADERS?=open-source
headers::
@echo "Applying Headers..."
@echo "Applying $(EACSL_HEADERS) Headers..."
headache -c $(EACSL_PLUGIN_DIR)/license/headache_config.txt \
-h $(CEA_LGPL_HEADER) $(EACSL_CEA_LGPL)
-h $(EACSL_PLUGIN_DIR)/headers/$(EACSL_HEADERS)/CEA_LGPL_OR_PROPRIETARY.E_ACSL \
$(EACSL_CEA_LGPL)
headache -c $(EACSL_PLUGIN_DIR)/license/headache_config.txt \
-h $(EACSL_PLUGIN_DIR)/license/SPARETIMELABS \
-h $(EACSL_PLUGIN_DIR)/headers/$(EACSL_HEADERS)/MODIFIED_SPARETIMELABS \
$(EACSL_SPARETIMELABS)
headache -c $(EACSL_PLUGIN_DIR)/license/headache_config.txt \
-h $(EACSL_PLUGIN_DIR)/headers/$(EACSL_HEADERS)/MODIFIED_DLMALLOC \
$(EACSL_PLUGIN_DIR)/contrib/libdlmalloc/dlmalloc.c
headache -c $(EACSL_PLUGIN_DIR)/license/headache_config.txt \
-h $(EACSL_PLUGIN_DIR)/headers/$(EACSL_HEADERS)/MODIFIED_LIB_GMP \
$(EACSL_PLUGIN_DIR)/contrib/libgmp/mini-gmp.[ch]
endif
################
# Generic part #
......
(**************************************************************************)
(* *)
(* This file is part of Frama-C. *)
(* This file is part of the Frama-C's E-ACSL plug-in. *)
(* *)
(* Copyright (C) 2007-2018 *)
(* Copyright (C) 2012-2018 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
......
(**************************************************************************)
(* *)
(* This file is part of Frama-C. *)
(* This file is part of the Frama-C's E-ACSL plug-in. *)
(* *)
(* Copyright (C) 2007-2018 *)
(* Copyright (C) 2012-2018 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
......
##########################################################################
# #
# This file is part of Frama-C. #
# This file is part of the Frama-C's E-ACSL plug-in. #
# #
# Copyright (C) 2007-2018 #
# Copyright (C) 2012-2018 #
# CEA (Commissariat à l'énergie atomique et aux énergies #
# alternatives) #
# #
......
/*
This is a version (aka dlmalloc) of malloc/free/realloc written by
Doug Lea and released to the public domain, as explained at
http://creativecommons.org/publicdomain/zero/1.0/ Send questions,
comments, complaints, performance data, etc to dl@cs.oswego.edu
* Version 2.8.6 Wed Aug 29 06:57:58 2012 Doug Lea
Note: There may be an updated version of this malloc obtainable at
ftp://gee.cs.oswego.edu/pub/misc/malloc.c
Check before installing!
* This file has been modified by CEA for use together with Runtime Library
/**************************************************************************/
/* */
/* This is a version (aka dlmalloc) of malloc/free/realloc written by */
/* Doug Lea and released to the public domain, as explained at */
/* http://creativecommons.org/publicdomain/zero/1.0/ Send questions, */
/* comments, complaints, performance data, etc to dl@cs.oswego.edu */
/* */
/* Version 2.8.6 Wed Aug 29 06:57:58 2012 Doug Lea */
/* Note: There may be an updated version of this malloc obtainable at */
/* ftp://gee.cs.oswego.edu/pub/misc/malloc.c */
/* Check before installing! */
/* */
/* File modified by CEA (Commissariat à l'énergie atomique et aux */
/* énergies alternatives). */
/* */
/**************************************************************************/
/* This file has been modified by CEA for use together with Runtime Library
of the E-ACSL plugin of Frama-C.
The changes introduced by CEA are limited to the following modifications:
* Added declaration/definition of mspace_least_addr function
* Added functionality to modify prefix of `mspace_...` functions
* Added functionality to modify prefix of `mspace_...` functions. */
* Quickstart
/* Quickstart
This library is all in one file to simplify the most common usage:
ftp it, compile it (-O3), and link it into another program. All of
......
/* mini-gmp, a minimalistic implementation of a GNU GMP subset.
Contributed to the GNU project by Niels Möller
Copyright 1991-1997, 1999-2015 Free Software Foundation, Inc.
This file is part of the GNU MP Library.
The GNU MP Library is free software; you can redistribute it and/or modify
it under the terms of either:
* the GNU Lesser General Public License as published by the Free
Software Foundation; either version 3 of the License, or (at your
option) any later version.
or
* the GNU General Public License as published by the Free Software
Foundation; either version 2 of the License, or (at your option) any
later version.
or both in parallel, as here.
The GNU MP Library 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 General Public License
for more details.
You should have received copies of the GNU General Public License and the
GNU Lesser General Public License along with the GNU MP Library. If not,
see https://www.gnu.org/licenses/. */
/********************************************************************************/
/* */
/* mini-gmp, a minimalistic implementation of a GNU GMP subset. */
/* */
/* Contributed to the GNU project by Niels Möller */
/* */
/* Copyright 1991-1997, 1999-2015 Free Software Foundation, Inc. */
/* */
/* This file is part of the GNU MP Library. */
/* */
/* The GNU MP Library is free software; you can redistribute it and/or modify */
/* it under the terms of either: */
/* */
/* * the GNU Lesser General Public License as published by the Free */
/* Software Foundation; either version 3 of the License, or (at your */
/* option) any later version. */
/* */
/* or */
/* */
/* * the GNU General Public License as published by the Free Software */
/* Foundation; either version 2 of the License, or (at your option) any */
/* later version. */
/* */
/* or both in parallel, as here. */
/* */
/* The GNU MP Library 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 General Public License */
/* for more details. */
/* */
/* You should have received copies of the GNU General Public License and the */
/* GNU Lesser General Public License along with the GNU MP Library. If not, */
/* see https://www.gnu.org/licenses/. */
/* */
/* File modified by CEA (Commissariat à l'énergie atomique et aux */
/* énergies alternatives). */
/* */
/********************************************************************************/
/* NOTE: All functions in this file which are not declared in
mini-gmp.h are internal, and are not intended to be compatible
......
/* mini-gmp, a minimalistic implementation of a GNU GMP subset.
Copyright 2011-2015 Free Software Foundation, Inc.
This file is part of the GNU MP Library.
The GNU MP Library is free software; you can redistribute it and/or modify
it under the terms of either:
* the GNU Lesser General Public License as published by the Free
Software Foundation; either version 3 of the License, or (at your
option) any later version.
or
* the GNU General Public License as published by the Free Software
Foundation; either version 2 of the License, or (at your option) any
later version.
or both in parallel, as here.
The GNU MP Library 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 General Public License
for more details.
You should have received copies of the GNU General Public License and the
GNU Lesser General Public License along with the GNU MP Library. If not,
see https://www.gnu.org/licenses/. */
/********************************************************************************/
/* */
/* mini-gmp, a minimalistic implementation of a GNU GMP subset. */
/* */
/* Contributed to the GNU project by Niels Möller */
/* */
/* Copyright 1991-1997, 1999-2015 Free Software Foundation, Inc. */
/* */
/* This file is part of the GNU MP Library. */
/* */
/* The GNU MP Library is free software; you can redistribute it and/or modify */
/* it under the terms of either: */
/* */
/* * the GNU Lesser General Public License as published by the Free */
/* Software Foundation; either version 3 of the License, or (at your */
/* option) any later version. */
/* */
/* or */
/* */
/* * the GNU General Public License as published by the Free Software */
/* Foundation; either version 2 of the License, or (at your option) any */
/* later version. */
/* */
/* or both in parallel, as here. */
/* */
/* The GNU MP Library 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 General Public License */
/* for more details. */
/* */
/* You should have received copies of the GNU General Public License and the */
/* GNU Lesser General Public License along with the GNU MP Library. If not, */
/* see https://www.gnu.org/licenses/. */
/* */
/* File modified by CEA (Commissariat à l'énergie atomique et aux */
/* énergies alternatives). */
/* */
/********************************************************************************/
/* About mini-gmp: This is a minimal implementation of a subset of the
GMP interface. It is intended for inclusion into applications which
......
(**************************************************************************)
(* *)
(* This file is part of Frama-C. *)
(* This file is part of the Frama-C's E-ACSL plug-in. *)
(* *)
(* Copyright (C) 2007-2018 *)
(* Copyright (C) 2012-2018 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
......
(**************************************************************************)
(* *)
(* This file is part of Frama-C. *)
(* This file is part of the Frama-C's E-ACSL plug-in. *)
(* *)
(* Copyright (C) 2007-2018 *)
(* Copyright (C) 2012-2018 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
......
(**************************************************************************)
(* *)
(* This file is part of Frama-C. *)
(* This file is part of the Frama-C's E-ACSL plug-in. *)
(* *)
(* Copyright (C) 2007-2018 *)
(* Copyright (C) 2012-2018 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
......
(**************************************************************************)
(* *)
(* This file is part of Frama-C. *)
(* This file is part of the Frama-C's E-ACSL plug-in. *)
(* *)
(* Copyright (C) 2007-2018 *)
(* Copyright (C) 2012-2018 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
......
(**************************************************************************)
(* *)
(* This file is part of Frama-C. *)
(* This file is part of the Frama-C's E-ACSL plug-in. *)
(* *)
(* Copyright (C) 2007-2018 *)
(* Copyright (C) 2012-2018 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
......
(**************************************************************************)
(* *)
(* This file is part of Frama-C. *)
(* This file is part of the Frama-C's E-ACSL plug-in. *)
(* *)
(* Copyright (C) 2007-2018 *)
(* Copyright (C) 2012-2018 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
......
(**************************************************************************)
(* *)
(* This file is part of Frama-C. *)
(* This file is part of the Frama-C's E-ACSL plug-in. *)
(* *)
(* Copyright (C) 2007-2018 *)
(* Copyright (C) 2012-2018 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
......
(**************************************************************************)
(* *)
(* This file is part of Frama-C. *)
(* This file is part of the Frama-C's E-ACSL plug-in. *)
(* *)
(* Copyright (C) 2007-2018 *)
(* Copyright (C) 2012-2018 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
......
(**************************************************************************)
(* *)
(* This file is part of Frama-C. *)
(* This file is part of the Frama-C's E-ACSL plug-in. *)
(* *)
(* Copyright (C) 2007-2018 *)
(* Copyright (C) 2012-2018 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
......
(**************************************************************************)
(* *)
(* This file is part of Frama-C. *)
(* This file is part of the Frama-C's E-ACSL plug-in. *)
(* *)
(* Copyright (C) 2007-2018 *)
(* Copyright (C) 2012-2018 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
......
(**************************************************************************)
(* *)
(* This file is part of Frama-C. *)
(* This file is part of the Frama-C's E-ACSL plug-in. *)
(* *)
(* Copyright (C) 2007-2018 *)
(* Copyright (C) 2012-2018 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
......
(**************************************************************************)
(* *)
(* This file is part of Frama-C. *)
(* This file is part of the Frama-C's E-ACSL plug-in. *)
(* *)
(* Copyright (C) 2007-2018 *)
(* Copyright (C) 2012-2018 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment