frama-c-base 20151002+magnesium+dfsg-1build1 / usr / share / frama-c / machdep.c

/****************************************************************************/
/*                                                                          */
/*  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 alignement 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
  }

  // __thread_is_keyword
  {
#ifdef THREAD_IS_KEYWORD
    printf("\t __thread_is_keyword = true;\n");
#else
    printf("\t __thread_is_keyword = 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);
}