l4/pkg/ferret/include/gcc_instrument.h

   1 /**
   2  * \file   ferret/include/gcc_instrument.h
   3  * \brief  Support functions for gcc-function-level instrumentation
   4  *
   5  * \date   2007-10-09
   6  * \author Martin Pohlack  <mp26@os.inf.tu-dresden.de>
   7  */
   8 /*
   9  * (c) 2007-2009 Technische Universität Dresden
  10  * This file is part of TUD:OS and distributed under the terms of the
  11  * GNU General Public License 2.
  12  * Please see the COPYING-GPL-2 file for details.
  13  */
  14 #ifndef __FERRET_INCLUDE_GCC_INSTRUMENT_H
  15 #define __FERRET_INCLUDE_GCC_INSTRUMENT_H
  16
  17 #include <l4/sys/types.h>
  18
  19 /* Set function pointer for get_threadid-function and create sensor.
  20  */
  21 L4_CV void ferret_gcc_instrument_init(void *(*alloc)(size_t s),
  22                                       l4_threadid_t (*myself)(void))
  23     __attribute__ ((no_instrument_function));
  24
  25 #endif