diff --git a/.for_devel b/.for_devel deleted file mode 100644 index 10bb4fd07ff59e924e4d738a163e9d73fcfbd27b..0000000000000000000000000000000000000000 --- a/.for_devel +++ /dev/null @@ -1,6 +0,0 @@ -This file activates the compilation of Frama-C in developer mode - - - enable warnings and warn-error - - create .merlin file - - create links in ./share to plugin share directory for - the bin/frama-c* script diff --git a/.make-clean b/.make-clean deleted file mode 100644 index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000 diff --git a/.make-clean-stamp b/.make-clean-stamp deleted file mode 100644 index 7f8f011eb73d6043d2e6db9d2c101195ae2801f2..0000000000000000000000000000000000000000 --- a/.make-clean-stamp +++ /dev/null @@ -1 +0,0 @@ -7 diff --git a/config.h.in b/config.h.in deleted file mode 100644 index 6b4ecb3b94b32ea22203921153fb7c955df56a84..0000000000000000000000000000000000000000 --- a/config.h.in +++ /dev/null @@ -1,55 +0,0 @@ -/**************************************************************************/ -/* */ -/* This file is part of Frama-C. */ -/* */ -/* Copyright (C) 2007-2022 */ -/* 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). */ -/* */ -/**************************************************************************/ - -#undef HAVE_WCHAR_T - -#undef HAVE_STDLIB_H - -#undef HAVE_STRINGS_H - -#undef HAVE_SYS_TIME_H - -#undef HAVE_UNISTD_H - -#undef HAVE_CONST - -#undef HAVE_INLINE - -#undef HAVE_TIME_H - -#undef HAVE_MEMCP - -#undef HAVE_MKDIR - -#undef HAVE_SELECT - -#undef HAVE_SOCKET - -#undef TYPE_SIZE_T - -#undef TYPE_WCHAR_T - -#undef TYPE_PTRDIFF_T - -#undef HAVE_BUILTIN_VA_LIST - -#undef UNDERSCORE_NAME diff --git a/share/machdep.c b/share/machdep.c deleted file mode 100644 index cd0035e3314d8bf929f5a2902bb0299b65a4a4d1..0000000000000000000000000000000000000000 --- a/share/machdep.c +++ /dev/null @@ -1,364 +0,0 @@ -/****************************************************************************/ -/* */ -/* Copyright (C) 2001-2003 */ -/* George C. Necula <necula@cs.berkeley.edu> */ -/* Scott McPeak <smcpeak@cs.berkeley.edu> */ -/* Wes Weimer <weimer@cs.berkeley.edu> */ -/* Ben Liblit <liblit@cs.berkeley.edu> */ -/* All rights reserved. */ -/* */ -/* Redistribution and use in source and binary forms, with or without */ -/* modification, are permitted provided that the following conditions */ -/* are met: */ -/* */ -/* 1. Redistributions of source code must retain the above copyright */ -/* notice, this list of conditions and the following disclaimer. */ -/* */ -/* 2. Redistributions in binary form must reproduce the above copyright */ -/* notice, this list of conditions and the following disclaimer in the */ -/* documentation and/or other materials provided with the distribution. */ -/* */ -/* 3. The names of the contributors may not be used to endorse or */ -/* promote products derived from this software without specific prior */ -/* written permission. */ -/* */ -/* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS */ -/* "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT */ -/* LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS */ -/* FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE */ -/* COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, */ -/* INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, */ -/* BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; */ -/* LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER */ -/* CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT */ -/* LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN */ -/* ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE */ -/* POSSIBILITY OF SUCH DAMAGE. */ -/* */ -/* File modified by CEA (Commissariat à l'énergie atomique et aux */ -/* énergies alternatives) */ -/* and INRIA (Institut National de Recherche en Informatique */ -/* et Automatique). */ -/****************************************************************************/ - -#include "../config.h" -#include <stdio.h> - -#ifdef HAVE_STDLIB_H -#include <stdlib.h> -#endif - -#ifdef HAVE_WCHAR_H -#include <wchar.h> -#endif - -#define COMPILER "other" - -#ifdef __TURBOC__ -#define LONGLONG long long -#define CONST_STRING_LITERALS "false" -#define VERSION __TURBOC__ -#define VERSION_MAJOR 0 -#define VERSION_MINOR 0 -#endif - -#ifdef __GNUC__ -#define LONGLONG long long -#define CONST_STRING_LITERALS "true" -#define VERSION __VERSION__ -#define VERSION_MAJOR __GNUC__ -#define VERSION_MINOR __GNUC_MINOR__ -#undef COMPILER -#define COMPILER "gcc" -#endif - -#ifdef _MSVC -#define LONGLONG __int64 -#define CONST_STRING_LITERALS "false" -#define VERSION "Microsoft C" -#define VERSION_MAJOR (_MSC_VER / 100) -#define VERSION_MINOR (_MSC_VER % 100) -#undef COMPILER -#define COMPILER "msvc" -#endif - -#ifndef __TURBOC__ -#ifndef __GNUC__ -#ifndef _MSVC -#error "Please define one of __TURBOC__ __GNUC__ _MSVC." -#endif -#endif -#endif - -/* The type for the machine dependency structure is generated from the - Makefile */ -int main() { - fprintf(stderr, "Generating machine dependency information for CIL\n"); - - printf("(* Generated by code in %s *)\n", __FILE__); - printf("open Cil_types\n"); - printf("let mach = {\n"); - // printf("\t version_major = %d;\n", VERSION_MAJOR); - // printf("\t version_minor = %d;\n", VERSION_MINOR); -#ifdef __TURBOC__ - printf("\t version = \"%d\";\n", VERSION); -#else - printf("\t version = \"%s\";\n", VERSION); -#endif - // Size of certain types - printf("\t sizeof_short = %lu;\n", sizeof(short)); - printf("\t sizeof_int = %lu;\n", sizeof(int)); - printf("\t sizeof_long = %lu;\n", sizeof(long)); - printf("\t sizeof_longlong = %lu;\n", sizeof(LONGLONG)); - printf("\t sizeof_ptr = %lu;\n", sizeof(int *)); - printf("\t sizeof_float = %lu;\n", sizeof(float)); - printf("\t sizeof_double = %lu;\n", sizeof(double)); - printf("\t sizeof_longdouble = %lu;\n", sizeof(long double)); - printf("\t sizeof_void = %lu;\n", -#ifdef __TURBOC__ - 0 -#else - sizeof(void) -#endif -); - printf("\t sizeof_fun = %lu;\n", -#ifdef __GNUC__ - sizeof(main) -#else - 0 -#endif - ); - // definition of size_t - { - printf("\t size_t = \"%s\";\n", TYPE_SIZE_T); - printf("\t wchar_t = \"%s\";\n", TYPE_WCHAR_T); - printf("\t ptrdiff_t = \"%s\";\n", TYPE_PTRDIFF_T); - } - - // The alignment of a short - { - struct shortstruct { - char c; - short s; - }; - printf("\t alignof_short = %z;\n", - (size_t)(&((struct shortstruct*)0)->s)); - } - - // The alignment of an int - { - struct intstruct { - char c; - int i; - }; - printf("\t alignof_int = %z;\n", - (size_t)(&((struct intstruct*)0)->i)); - } - - // The alignment of a long - { - struct longstruct { - char c; - long l; - }; - printf("\t alignof_long = %z;\n", - (size_t)(&((struct longstruct*)0)->l)); - } - - // The alignment of long long - { - struct longlong { - char c; - LONGLONG ll; - }; - printf("\t alignof_longlong = %z;\n", - (size_t)(&((struct longlong*)0)->ll)); - } - - // The alignment of a ptr - { - struct ptrstruct { - char c; - int * p; - }; - printf("\t alignof_ptr = %z;\n", - (size_t)(&((struct ptrstruct*)0)->p)); - } - - // Unnamed members - { - struct S0 - { - int; - // If you are reading this, it's probably because your C compiler - // rejected the above. Good for you! It is not allowed by C99. - // See discussion thread at: - // http://lists.cs.uiuc.edu/pipermail/c-semantics/2011-August/thread.html - // You can comment out this block. - int f1; - }; - if (sizeof(struct S0) != 2*sizeof(int)) - { - printf("(* WARNING: This compiler handles unnamed struct members\n"); - printf(" differently from Frama-C.\n"); - printf(" To be analyzed correctly, your programs must *NOT* use\n"); - printf(" this language extension. *)\n"); - } - } - - // long long bit-fields - { - struct LLS - { - long long int f:2; - // If you are reading this, it's probably because your C compiler - // rejected the above. Good for you! It is only allowed by C99 - // as an extension. - // You can comment out this block. - } lls; - if (sizeof(1 + lls.f) != sizeof(int)) - { - printf("(* WARNING: This compiler handles long long bit-fields\n"); - printf(" differently from Frama-C.\n"); - printf(" To be analyzed correctly, your programs must *NOT* use\n"); - printf(" this language extension. *)\n"); - } - } - - // The alignment of a float - { - struct floatstruct { - char c; - float f; - }; - printf("\t alignof_float = %z;\n", - (size_t)(&((struct floatstruct*)0)->f)); - } - - // The alignment of double - { - struct s1 { - char c; - double d; - }; - printf("\t alignof_double = %z;\n", - (size_t)(&((struct s1*)0)->d)); - } - - // The alignment of long double - { - struct s1 { - char c; - long double ld; - }; - printf("\t alignof_longdouble = %z;\n", - (size_t)(&((struct s1*)0)->ld)); - } - - printf("\t alignof_str = %lu;\n", -#ifdef __GNUC__ - __alignof("a string") -#else - 0 -#endif - ); - - printf("\t alignof_fun = %lu;\n", -#ifdef __GNUC__ - __alignof(main) -#else - 0 -#endif - ); - - // The alignment of char array - { - struct s1 { - char c; - char ca[2]; - }; - // printf("\t alignof_char_array = %lu;\n", - // (int)(&((struct s1*)0)->ca)); - } - - /* The alignment of an __aligned__ type */ - { -#ifdef __TURBOC__ - printf("\t alignof_aligned = 8;\n"); -#else - char __attribute__((aligned)) c; - long double __attribute__((aligned)) ld; - if (__alignof(c) != __alignof(ld)) { - printf("(*__attribute__((aligned)) has a different effect \ - on different types. alignments may be computed \ - incorrectly.*)\n"); - }; - printf("\t alignof_aligned = %lu;\n",__alignof(c)); -#endif - } - - - // Whether char is unsigned - printf("\t char_is_unsigned = %s;\n", - ((char)0xff) > 0 ? "true" : "false"); - - // Whether int bit-field is unsigned - { - union { - signed int init ; - struct { - int width8 : 8; - } sign ; - } bitfield; - - bitfield.init=-1; - printf("\t (* int_bitfield_is_unsigned = %s; *)\n", - (bitfield.sign.width8 > 0 ? "true" : "false")); - if (bitfield.sign.width8 > 0) { - // 'int width8 : 8' is an unsigned bit-field. - printf("(* WARNING: This compiler handles int bit-fields\n"); - printf(" differently from Frama-C.\n"); - printf(" To be analyzed correctly, your programs must *NOT* use\n"); - printf(" 'int' bit-fields, but 'unsigned int' bit-fields. *)\n"); - } - } - - // Whether string literals contain constant characters - puts("\t const_string_literals = " CONST_STRING_LITERALS ";"); - - // endianity - { - int e = 0x11223344; - printf("\t little_endian = %s;\n", - (0x44 == *(char*)&e) ? "true" : - ((0x11 == *(char*)&e) ? "false" : (exit(1), "false"))); - } - - // __builtin_val_list - { -#ifdef HAVE_BUILTIN_VA_LIST - printf("\t has__builtin_va_list = true;\n"); -#else - printf("\t has__builtin_va_list = false;\n"); -#endif - } - - // underscore_name - { -#ifdef UNDERSCORE_NAME - printf("\t underscore_name = true;\n"); -#else - printf("\t underscore_name = false;\n"); -#endif - } - - // compiler - { - printf("\t compiler = \"" COMPILER "\""); - } - - - printf("}\n"); - - exit(0); -}