/*
 *
 * Copyright 1999-2013 The MathWorks, Inc.
 *
 */

#if (defined(__PST_IAR_COMPILER__) && !defined(__PST_NO_IAR_STUBS__))

/* iar stubs */

#endif /* defined(__PST_IAR_COMPILER__) && !defined(__PST_NO_IAR_STUBS__) */



#if (defined(__PST_KEIL_COMPILER__) && !defined(__PST_NO_KEIL_STUBS__))

#define PST_STUB_KEIL_DEF(ret, func, args) ret func args

/* Optimized stubs for the standard Keil library */

#if defined(__polyspace_xmalloc) && !defined(__polyspace_no_xmalloc)
#include <stdlib.h>

#undef PST_STUB_C_DEF_BEGIN
#undef RETURN
#if CUSTOM_STUB_TYPE(xmalloc, 1)
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_CUSTOM_TYPE_1
#define RETURN(x) RETURN_CUSTOM_TYPE(xmalloc, x)
#else
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_STD_TYPE_1
#define RETURN(x) return (x)
#endif
PST_STUB_C_DEF_BEGIN(PST_STUB_KEIL_DEF, void*, xmalloc, unsigned long, size, NO_VARARGS, )
{
	RETURN(malloc(size));
}
PST_STUB_C_DEF_END
#define __polyspace_no_xmalloc
#endif

#if defined(__polyspace_xrealloc) && !defined(__polyspace_no_xrealloc)
#include <stdlib.h>

#undef PST_STUB_C_DEF_BEGIN
#undef RETURN
#if CUSTOM_STUB_TYPE(xrealloc, 2)
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_CUSTOM_TYPE_2
#define RETURN(x) RETURN_CUSTOM_TYPE(xrealloc, x)
#else
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_STD_TYPE_2
#define RETURN(x) return (x)
#endif
PST_STUB_C_DEF_BEGIN(PST_STUB_KEIL_DEF, void*, xrealloc, void*, p, unsigned long, size, NO_VARARGS, )
{
	RETURN(realloc(p, size));
}
PST_STUB_C_DEF_END
#define __polyspace_no_xrealloc
#endif

#if defined(__polyspace_xcalloc) && !defined(__polyspace_no_xcalloc)
#include <stdlib.h>

#undef PST_STUB_C_DEF_BEGIN
#undef RETURN
#if CUSTOM_STUB_TYPE(xcalloc, 2)
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_CUSTOM_TYPE_2
#define RETURN(x) RETURN_CUSTOM_TYPE(xcalloc, x)
#else
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_STD_TYPE_2
#define RETURN(x) return (x)
#endif
PST_STUB_C_DEF_BEGIN(PST_STUB_KEIL_DEF, void*, xcalloc, unsigned long, size, unsigned long, len, NO_VARARGS, )
{
	RETURN(xcalloc(size, len));
}
PST_STUB_C_DEF_END
#define __polyspace_no_xcalloc
#endif

#if defined(__polyspace_xfree) && !defined(__polyspace_no_xfree)
#include <stdlib.h>

#undef PST_STUB_C_DEF_BEGIN
#undef RETURN
#if CUSTOM_STUB_TYPE(xfree, 1)
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_CUSTOM_TYPE_1
#define RETURN(x) RETURN_CUSTOM_TYPE(xfree, x)
#else
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_STD_TYPE_1
#define RETURN(x) return (x)
#endif
PST_STUB_C_DEF_BEGIN(PST_STUB_KEIL_DEF, void, xfree, void*, p, NO_VARARGS, )
{
	free(p);
}
PST_STUB_C_DEF_END
#define __polyspace_no_xfree
#endif

/* define some macros ... */ 
/* no needed in C++ since done in __polyspace__std_decls.h */
#define PST_STUB_C_DEF(func_return,func_name,func_args) func_return func_name func_args


//memcmp
#if defined(__polyspace_memcmp) && !defined(__polyspace_no_memcmp)
#if !defined(POLYSPACE_INSTRUMENT)
#if !defined(NO_CHECKS_INLINING) && !defined(__polyspace_no_inlined_memcmp)
#pragma POLYSPACE_INLINE_CHECKS "memcmp"
#endif /* !NO_CHECKS_INLINING */
#if defined(PST_HAS_STRING_H) || (!defined __cplusplus)
#include <string.h>
#endif
#undef memcmp
#undef PST_STUB_C_DEF_BEGIN
#undef RETURN
#if CUSTOM_STUB_TYPE(memcmp, 3)
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_CUSTOM_TYPE_3
#define RETURN(x) RETURN_CUSTOM_TYPE(memcmp, x)
#else
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_STD_TYPE_3
#define RETURN(x) return (x)
#endif
PST_STUB_C_DEF_BEGIN(PST_STUB_C_DEF, int, memcmp,  void *, s1, void *, s2, unsigned int, n, NO_VARARGS, __PST_THROW) {
  RETURN(_polyspace_random_int());
}
PST_STUB_C_DEF_END
#pragma POLYSPACE_POLYMORPHIC "memcmp"
#else
#pragma POLYSPACE_NO_INSTRUMENT "memcmp"
#endif
#define __polyspace_no_memcmp
#endif /* __polyspace_memcmp */

//fmemcmp
#if defined(__polyspace_fmemcmp) && !defined(__polyspace_no_fmemcmp)
#if !defined(POLYSPACE_INSTRUMENT)
#if !defined(NO_CHECKS_INLINING) && !defined(__polyspace_no_inlined_fmemcmp)
#pragma POLYSPACE_INLINE_CHECKS "fmemcmp"
#endif /* !NO_CHECKS_INLINING */
#if defined(PST_HAS_STRING_H) || (!defined __cplusplus)
#include <string.h>
#endif
#undef fmemcmp
#undef PST_STUB_C_DEF_BEGIN
#undef RETURN
#if CUSTOM_STUB_TYPE(fmemcmp, 3)
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_CUSTOM_TYPE_3
#define RETURN(x) RETURN_CUSTOM_TYPE(fmemcmp, x)
#else
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_STD_TYPE_3
#define RETURN(x) return (x)
#endif
PST_STUB_C_DEF_BEGIN(PST_STUB_C_DEF, int, fmemcmp,  void *, s1, void *, s2, unsigned int, n, NO_VARARGS, __PST_THROW) {
    RETURN(memcmp(s1, s2, n));
}
PST_STUB_C_DEF_END
#pragma POLYSPACE_POLYMORPHIC "fmemcmp"
#else
#pragma POLYSPACE_NO_INSTRUMENT "fmemcmp"
#endif
#define __polyspace_no_fmemcmp
#endif /* __polyspace_fmemcmp */

//hmemcmp
#if defined(__polyspace_hmemcmp) && !defined(__polyspace_no_hmemcmp)
#if !defined(POLYSPACE_INSTRUMENT)
#if !defined(NO_CHECKS_INLINING) && !defined(__polyspace_no_inlined_hmemcmp)
#pragma POLYSPACE_INLINE_CHECKS "hmemcmp"
#endif /* !NO_CHECKS_INLINING */
#if defined(PST_HAS_STRING_H) || (!defined __cplusplus)
#include <string.h>
#endif
#undef hmemcmp
#undef PST_STUB_C_DEF_BEGIN
#undef RETURN
#if CUSTOM_STUB_TYPE(hmemcmp, 3)
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_CUSTOM_TYPE_3
#define RETURN(x) RETURN_CUSTOM_TYPE(hmemcmp, x)
#else
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_STD_TYPE_3
#define RETURN(x) return (x)
#endif
PST_STUB_C_DEF_BEGIN(PST_STUB_C_DEF, int, hmemcmp,  void *, s1, void *, s2, unsigned int, n, NO_VARARGS, __PST_THROW) {
    RETURN(memcmp(s1, s2, n));
}
PST_STUB_C_DEF_END
#pragma POLYSPACE_POLYMORPHIC "hmemcmp"
#else
#pragma POLYSPACE_NO_INSTRUMENT "hmemcmp"
#endif
#define __polyspace_no_hmemcmp
#endif /* __polyspace_hmemcmp */




//xmemcmp
#if defined(__polyspace_xmemcmp) && !defined(__polyspace_no_xmemcmp)
#if !defined(POLYSPACE_INSTRUMENT)
#if !defined(NO_CHECKS_INLINING) && !defined(__polyspace_no_inlined_xmemcmp)
#pragma POLYSPACE_INLINE_CHECKS "xmemcmp"
#endif /* !NO_CHECKS_INLINING */
#if defined(PST_HAS_STRING_H) || (!defined __cplusplus)
#include <string.h>
#endif
#undef xmemcmp
#undef PST_STUB_C_DEF_BEGIN
#undef RETURN
#if CUSTOM_STUB_TYPE(xmemcmp, 3)
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_CUSTOM_TYPE_3
#define RETURN(x) RETURN_CUSTOM_TYPE(xmemcmp, x)
#else
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_STD_TYPE_3
#define RETURN(x) return (x)
#endif
PST_STUB_C_DEF_BEGIN(PST_STUB_C_DEF, int, xmemcmp,  void *, s1, void *, s2, unsigned long, n, NO_VARARGS, __PST_THROW) {
    RETURN(memcmp(s1, s2, n));
}
PST_STUB_C_DEF_END
#pragma POLYSPACE_POLYMORPHIC "xmemcmp"
#else
#pragma POLYSPACE_NO_INSTRUMENT "xmemcmp"
#endif
#define __polyspace_no_xmemcmp
#endif /* __polyspace_xmemcmp */

#if ((defined(__polyspace_memcpy) && !defined(__polyspace_no_memcpy)) ||\
     (defined(__polyspace_memmove) && !defined(__polyspace_no_memmove)))
#include <string.h>

#undef PST_STUB_C_DEF_BEGIN
#undef RETURN
#if CUSTOM_STUB_TYPE(memcpy, 3)
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_CUSTOM_TYPE_3
#define RETURN(x) RETURN_CUSTOM_TYPE(memcpy, x)
#else
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_STD_TYPE_3
#define RETURN(x) return (x)
#endif

#ifdef __C51__
PST_STUB_C_DEF_BEGIN(PST_STUB_KEIL_DEF, void*, memcpy, void*, s1, void*, s2, int, n, NO_VARARGS, )
#else
PST_STUB_C_DEF_BEGIN(PST_STUB_KEIL_DEF, void*, memcpy, void*, s1, void*, s2, unsigned int, n, NO_VARARGS, )
#endif
{
#ifdef __C51__
  int i;
#else
  unsigned int i;
#endif
  char *p, *q;
  p = (char *)s1;
  q = (char *)s2;
  for (i=0; i<n; i++)
    p[i] = q[i];
  RETURN(s1);
}
PST_STUB_C_DEF_END
#define __polyspace_no_memcpy
#endif

#if ((defined(__polyspace_fmemcpy) && !defined(__polyspace_no_fmemcpy)) ||\
     (defined(__polyspace_fmemmove) && !defined(__polyspace_no_fmemmove)))
#include <string.h>

#undef PST_STUB_C_DEF_BEGIN
#undef RETURN
#if CUSTOM_STUB_TYPE(fmemcpy, 2)
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_CUSTOM_TYPE_2
#define RETURN(x) RETURN_CUSTOM_TYPE(fmemcpy, x)
#else
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_STD_TYPE_2
#define RETURN(x) return (x)
#endif
PST_STUB_C_DEF_BEGIN(PST_STUB_KEIL_DEF, void*, fmemcpy, void*, s1, void*, s2, unsigned int, n, NO_VARARGS, )
{
  unsigned int i;
  char *p, *q;
  p = (char *)s1;
  q = (char *)s2;
  for (i=0; i<n; i++)
    p[i] = q[i];
  RETURN(s1);
}
PST_STUB_C_DEF_END
#define __polyspace_no_fmemcpy
#endif

#if defined(__polyspace_hmemcpy) && !defined(__polyspace_no_hmemcpy)
#include <string.h>

#undef PST_STUB_C_DEF_BEGIN
#undef RETURN
#if CUSTOM_STUB_TYPE(hmemcpy, 3)
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_CUSTOM_TYPE_3
#define RETURN(x) RETURN_CUSTOM_TYPE(hmemcpy, x)
#else
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_STD_TYPE_3
#define RETURN(x) return (x)
#endif
PST_STUB_C_DEF_BEGIN(PST_STUB_KEIL_DEF, void*, hmemcpy, void*, s1, void*, s2, unsigned int, n, NO_VARARGS, )
{
  unsigned int i;
  char *p, *q;
  p = (char *)s1;
  q = (char *)s2;
  for (i=0; i<n; i++)
    p[i] = q[i];
  RETURN(s1);
}
PST_STUB_C_DEF_END
#define __polyspace_no_hmemcpy
#endif

#if ((defined(__polyspace_xmemcpy) && !defined(__polyspace_no_xmemcpy)) ||\
     (defined(__polyspace_xmemmove) && !defined(__polyspace_no_xmemmove)))
#include <string.h>


#undef PST_STUB_C_DEF_BEGIN
#undef RETURN
#if CUSTOM_STUB_TYPE(xmemcpy, 3)
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_CUSTOM_TYPE_3
#define RETURN(x) RETURN_CUSTOM_TYPE(xmemcpy, x)
#else
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_STD_TYPE_3
#define RETURN(x) return (x)
#endif
PST_STUB_C_DEF_BEGIN(PST_STUB_KEIL_DEF, void*, xmemcpy, void*, s1, void*, s2, unsigned long, n, NO_VARARGS, )
{
  unsigned long i;
  char *p, *q;
  p = (char *)s1;
  q = (char *)s2;
  for (i=0; i<n; i++)
    p[i] = q[i];
  RETURN(s1);
}
PST_STUB_C_DEF_END
#define __polyspace_no_xmemcpy
#endif

#if defined(__polyspace_strcpy) && !defined(__polyspace_no_strcpy)
#include <string.h>

#undef PST_STUB_C_DEF_BEGIN
#undef RETURN
#if CUSTOM_STUB_TYPE(strcpy, 2)
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_CUSTOM_TYPE_2
#define RETURN(x) RETURN_CUSTOM_TYPE(strcpy, x)
#else
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_STD_TYPE_2
#define RETURN(x) return (x)
#endif
PST_STUB_C_DEF_BEGIN(PST_STUB_KEIL_DEF, signed char*, strcpy, signed char*, s1, signed char*, s2, NO_VARARGS, )
{
  int i;
  int s2_len=0;
  while (s2[s2_len] != 0) s2_len++; /* s2_len = strlen(s2) */
  for (i = 0; i < s2_len; i++)
    s1[i] = s2[i];
 
  s1[i] = 0;
  RETURN(s1);
}
PST_STUB_C_DEF_END
#define __polyspace_no_strcpy
#endif

#if defined(__polyspace_fstrcpy) && !defined(__polyspace_no_fstrcpy)
#include <string.h>

#undef PST_STUB_C_DEF_BEGIN
#undef RETURN
#if CUSTOM_STUB_TYPE(fstrcpy, 2)
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_CUSTOM_TYPE_2
#define RETURN(x) RETURN_CUSTOM_TYPE(fstrcpy, x)
#else
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_STD_TYPE_2
#define RETURN(x) return (x)
#endif
PST_STUB_C_DEF_BEGIN(PST_STUB_KEIL_DEF, signed char*, fstrcpy, signed char*, s1, signed char*, s2, NO_VARARGS, )
{
  int i;
  int s2_len=0;
  while (s2[s2_len] != 0) s2_len++; /* s2_len = strlen(s2) */
  for (i = 0; i < s2_len; i++)
    s1[i] = s2[i];

  s1[i] = 0;
  RETURN(s1);
}
PST_STUB_C_DEF_END
#define __polyspace_no_fstrcpy
#endif

#if defined(__polyspace_hstrcpy) && !defined(__polyspace_no_hstrcpy)
#include <string.h>

#undef PST_STUB_C_DEF_BEGIN
#undef RETURN
#if CUSTOM_STUB_TYPE(hstrcpy, 2)
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_CUSTOM_TYPE_2
#define RETURN(x) RETURN_CUSTOM_TYPE(hstrcpy, x)
#else
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_STD_TYPE_2
#define RETURN(x) return (x)
#endif
PST_STUB_C_DEF_BEGIN(PST_STUB_KEIL_DEF, signed char*, hstrcpy, signed char*, s1, signed char, *s2, NO_VARARGS, )
{
  int i;
  int s2_len=0;
  while (s2[s2_len] != 0) s2_len++; /* s2_len = strlen(s2) */
  for (i = 0; i < s2_len; i++)
    s1[i] = s2[i];

  s1[i] = 0;
  RETURN(s1);
}
PST_STUB_C_DEF_END
#define __polyspace_no_hstrcpy
#endif

#if defined(__polyspace_xstrcpy) && !defined(__polyspace_no_xstrcpy)
#include <string.h>

#undef PST_STUB_C_DEF_BEGIN
#undef RETURN
#if CUSTOM_STUB_TYPE(xstrcpy, 2)
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_CUSTOM_TYPE_2
#define RETURN(x) RETURN_CUSTOM_TYPE(xstrcpy, x)
#else
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_STD_TYPE_2
#define RETURN(x) return (x)
#endif
PST_STUB_C_DEF_BEGIN(PST_STUB_KEIL_DEF, signed char*, xstrcpy, signed char*, s1, signed char*, s2, NO_VARARGS, )
{
  int i;
  int s2_len=0;
  while (s2[s2_len] != 0) s2_len++; /* s2_len = strlen(s2) */
  for (i = 0; i < s2_len; i++)
    s1[i] = s2[i];

  s1[i] = 0;
  RETURN(s1);
}
PST_STUB_C_DEF_END
#define __polyspace_no_xstrcpy
#endif

#if defined(__polyspace_strcmp) && !defined(__polyspace_no_strcmp)
#include <string.h>

#undef PST_STUB_C_DEF_BEGIN
#undef RETURN
#if CUSTOM_STUB_TYPE(strcmp, 2)
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_CUSTOM_TYPE_2
#define RETURN(x) RETURN_CUSTOM_TYPE(strcmp, x)
#else
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_STD_TYPE_2
#define RETURN(x) return (x)
#endif
PST_STUB_C_DEF_BEGIN(PST_STUB_KEIL_DEF, int, strcmp, signed char*, s1, signed char*, s2, NO_VARARGS, )
{
  int i, res;
  int l1=0, l2=0;
  while (s1[l1] != 0) l1++; /* l1 = strlen(s1) */
  while (s2[l2] != 0) l2++; /* l2 = strlen(s2) */
  if (l1 >= l2)
    {
      for (i=0; i < l2; i++)
        if ((res = (((unsigned char)s1[i]) - ((unsigned char)s2[i]))) != 0) {
#ifndef __polyspace_static_types_for_stubs
#pragma polyspace_check_info returned_value_numeric
#endif
          RETURN(res);
#ifndef __polyspace_static_types_for_stubs
#pragma polyspace_check_info
#endif
        }
    }
  else
    {
      for (i=0; i < l1; i++)
        if ((res = (((unsigned char)s1[i]) - ((unsigned char)s2[i]))) != 0) {
#ifndef __polyspace_static_types_for_stubs
#pragma polyspace_check_info returned_value_numeric
#endif
          RETURN(res);
#ifndef __polyspace_static_types_for_stubs
#pragma polyspace_check_info
#endif
        }
    }
 
  if (l1 < l2) {
#ifndef __polyspace_static_types_for_stubs
#pragma polyspace_check_info returned_value_numeric
#endif
    RETURN(-1);
#ifndef __polyspace_static_types_for_stubs
#pragma polyspace_check_info
#endif
  }

  if (l1 > l2) {
#ifndef __polyspace_static_types_for_stubs
#pragma polyspace_check_info returned_value_numeric
#endif
    RETURN(1);
#ifndef __polyspace_static_types_for_stubs
#pragma polyspace_check_info
#endif
  }

#ifndef __polyspace_static_types_for_stubs
#pragma polyspace_check_info returned_value_numeric
#endif
  RETURN(0);
#ifndef __polyspace_static_types_for_stubs
#pragma polyspace_check_info
#endif
}
PST_STUB_C_DEF_END
#define __polyspace_no_strcmp
#endif

#if defined(__polyspace_fstrcmp) && !defined(__polyspace_no_fstrcmp)
#include <string.h>

#undef PST_STUB_C_DEF_BEGIN
#undef RETURN
#if CUSTOM_STUB_TYPE(fstrcmp, 2)
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_CUSTOM_TYPE_2
#define RETURN(x) RETURN_CUSTOM_TYPE(fstrcmp, x)
#else
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_STD_TYPE_2
#define RETURN(x) return (x)
#endif
PST_STUB_C_DEF_BEGIN(PST_STUB_KEIL_DEF, int, fstrcmp, signed char*, s1, signed char*, s2, NO_VARARGS, )
{
  int i, res;
  int l1=0, l2=0;
  while (s1[l1] != 0) l1++; /* l1 = strlen(s1) */
  while (s2[l2] != 0) l2++; /* l2 = strlen(s2) */
  if (l1 >= l2)
    {
      for (i=0; i < l2; i++)
        if ((res = (((unsigned char)s1[i]) - ((unsigned char)s2[i]))) != 0) {
#ifndef __polyspace_static_types_for_stubs
#pragma polyspace_check_info returned_value_numeric
#endif
          RETURN(res);
#ifndef __polyspace_static_types_for_stubs
#pragma polyspace_check_info
#endif
        }
    }
  else
    {
      for (i=0; i < l1; i++)
        if ((res = (((unsigned char)s1[i]) - ((unsigned char)s2[i]))) != 0) {
#ifndef __polyspace_static_types_for_stubs
#pragma polyspace_check_info returned_value_numeric
#endif
          RETURN(res);
#ifndef __polyspace_static_types_for_stubs
#pragma polyspace_check_info
#endif
        }
    }

  if (l1 < l2) {
#ifndef __polyspace_static_types_for_stubs
#pragma polyspace_check_info returned_value_numeric
#endif
    RETURN(-1);
#ifndef __polyspace_static_types_for_stubs
#pragma polyspace_check_info
#endif
  }

  if (l1 > l2) {
#ifndef __polyspace_static_types_for_stubs
#pragma polyspace_check_info returned_value_numeric
#endif
    RETURN(1);
#ifndef __polyspace_static_types_for_stubs
#pragma polyspace_check_info
#endif
  }
  
#ifndef __polyspace_static_types_for_stubs
#pragma polyspace_check_info returned_value_numeric
#endif
    RETURN(0);
#ifndef __polyspace_static_types_for_stubs
#pragma polyspace_check_info
#endif
}
PST_STUB_C_DEF_END
#define __polyspace_no_fstrcmp
#endif

#if defined(__polyspace_hstrcmp) && !defined(__polyspace_no_hstrcmp)
#include <string.h>

#undef PST_STUB_C_DEF_BEGIN
#undef RETURN
#if CUSTOM_STUB_TYPE(hstrcmp, 2)
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_CUSTOM_TYPE_2
#define RETURN(x) RETURN_CUSTOM_TYPE(hstrcmp, x)
#else
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_STD_TYPE_2
#define RETURN(x) return (x)
#endif
PST_STUB_C_DEF_BEGIN(PST_STUB_KEIL_DEF, int, hstrcmp, signed char*, s1, signed char*, s2, NO_VARARGS, )
{
  int i, res;
  int l1=0, l2=0;
  while (s1[l1] != 0) l1++; /* l1 = strlen(s1) */
  while (s2[l2] != 0) l2++; /* l2 = strlen(s2) */
  if (l1 >= l2)
    {
      for (i=0; i < l2; i++)
        if ((res = (((unsigned char)s1[i]) - ((unsigned char)s2[i]))) != 0) {
#ifndef __polyspace_static_types_for_stubs
#pragma polyspace_check_info returned_value_numeric
#endif
          RETURN(res);
#ifndef __polyspace_static_types_for_stubs
#pragma polyspace_check_info
#endif
        }
    }
  else
    {
      for (i=0; i < l1; i++)
        if ((res = (((unsigned char)s1[i]) - ((unsigned char)s2[i]))) != 0) {
#ifndef __polyspace_static_types_for_stubs
#pragma polyspace_check_info returned_value_numeric
#endif
          RETURN(res);
#ifndef __polyspace_static_types_for_stubs
#pragma polyspace_check_info
#endif
        }
    }

  if (l1 < l2) {
#ifndef __polyspace_static_types_for_stubs
#pragma polyspace_check_info returned_value_numeric
#endif
    RETURN(-1);
#ifndef __polyspace_static_types_for_stubs
#pragma polyspace_check_info
#endif
  }

  if (l1 > l2) {
#ifndef __polyspace_static_types_for_stubs
#pragma polyspace_check_info returned_value_numeric
#endif
    RETURN(1);
#ifndef __polyspace_static_types_for_stubs
#pragma polyspace_check_info
#endif
  }

#ifndef __polyspace_static_types_for_stubs
#pragma polyspace_check_info returned_value_numeric
#endif
  RETURN(0);
#ifndef __polyspace_static_types_for_stubs
#pragma polyspace_check_info
#endif
}
PST_STUB_C_DEF_END
#define __polyspace_no_hstrcmp
#endif

#if defined(__polyspace_xstrcmp) && !defined(__polyspace_no_xstrcmp)
#include <string.h>

#undef PST_STUB_C_DEF_BEGIN
#undef RETURN
#if CUSTOM_STUB_TYPE(xstrcmp, 2)
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_CUSTOM_TYPE_2
#define RETURN(x) RETURN_CUSTOM_TYPE(xstrcmp, x)
#else
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_STD_TYPE_2
#define RETURN(x) return (x)
#endif
PST_STUB_C_DEF_BEGIN(PST_STUB_KEIL_DEF, int, xstrcmp, signed char*, s1, signed char*, s2, NO_VARARGS, )
{
  int i, res;
  int l1=0, l2=0;
  while (s1[l1] != 0) l1++; /* l1 = strlen(s1) */
  while (s2[l2] != 0) l2++; /* l2 = strlen(s2) */
  if (l1 >= l2)
    {
      for (i=0; i < l2; i++)
        if ((res = (((unsigned char)s1[i]) - ((unsigned char)s2[i]))) != 0) {
#ifndef __polyspace_static_types_for_stubs
#pragma polyspace_check_info returned_value_numeric
#endif
          RETURN(res);
#ifndef __polyspace_static_types_for_stubs
#pragma polyspace_check_info
#endif
        }
    }
  else
    {
      for (i=0; i < l1; i++)
        if ((res = (((unsigned char)s1[i]) - ((unsigned char)s2[i]))) != 0) {
#ifndef __polyspace_static_types_for_stubs
#pragma polyspace_check_info returned_value_numeric
#endif
          RETURN(res);
#ifndef __polyspace_static_types_for_stubs
#pragma polyspace_check_info
#endif
        }
    }

  if (l1 < l2) {
#ifndef __polyspace_static_types_for_stubs
#pragma polyspace_check_info returned_value_numeric
#endif
    RETURN(-1);
#ifndef __polyspace_static_types_for_stubs
#pragma polyspace_check_info
#endif
  }

  if (l1 > l2) {
#ifndef __polyspace_static_types_for_stubs
#pragma polyspace_check_info returned_value_numeric
#endif
    RETURN(1);
#ifndef __polyspace_static_types_for_stubs
#pragma polyspace_check_info
#endif
  }

#ifndef __polyspace_static_types_for_stubs
#pragma polyspace_check_info returned_value_numeric
#endif
  RETURN(0);
#ifndef __polyspace_static_types_for_stubs
#pragma polyspace_check_info
#endif
}
PST_STUB_C_DEF_END
#define __polyspace_no_xstrcmp
#endif

#if defined(__polyspace_vprintf) && !defined(__polyspace_no_vprintf)
#include <stdio.h>
#include <stdarg.h>

#undef PST_STUB_C_DEF_BEGIN
#undef RETURN
#if CUSTOM_STUB_TYPE(vprintf, 2)
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_CUSTOM_TYPE_2
#define RETURN(x) RETURN_CUSTOM_TYPE(vprintf, x)
#else
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_STD_TYPE_2
#define RETURN(x) return (x)
#endif
PST_STUB_C_DEF_BEGIN(PST_STUB_KEIL_DEF, int, vprintf, const signed char*, format, signed char*, ap, NO_VARARGS, )
{
  volatile int random = _polyspace_random_int();
#ifndef __polyspace_static_types_for_stubs
#pragma polyspace_check_info returned_value_numeric
#endif
  RETURN(random);
#ifndef __polyspace_static_types_for_stubs
#pragma polyspace_check_info
#endif
}
PST_STUB_C_DEF_END
#define __polyspace_no_vprintf
#endif

#if defined(__polyspace_vsprintf) && !defined(__polyspace_no_vsprintf)
#include <stdio.h>
#include <stdarg.h>


#undef PST_STUB_C_DEF_BEGIN
#undef RETURN
#if CUSTOM_STUB_TYPE(vsprintf, 3)
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_CUSTOM_TYPE_3
#define RETURN(x) RETURN_CUSTOM_TYPE(vsprintf, x)
#else
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_STD_TYPE_3
#define RETURN(x) return (x)
#endif

#ifdef __C51__
PST_STUB_C_DEF_BEGIN(PST_STUB_KEIL_DEF, int, vsprintf, char*, s, const char*, format, char*, ap, NO_VARARGS, )
#else
PST_STUB_C_DEF_BEGIN(PST_STUB_KEIL_DEF, int, vsprintf, signed char*, s, const signed char*, format, signed char*, ap, NO_VARARGS, )
#endif
{
  volatile int random = _polyspace_random_int();
  int i;
  for (i=0; i < random; i++) {
    s[i] = random;
  }
#ifndef __polyspace_static_types_for_stubs
#pragma polyspace_check_info returned_value_numeric
#endif
  RETURN(random);
#ifndef __polyspace_static_types_for_stubs
#pragma polyspace_check_info
#endif
}
PST_STUB_C_DEF_END
#define __polyspace_no_vsprintf
#endif

#if defined(__polyspace_sprintf) && !defined(__polyspace_no_sprintf)
#include <stdio.h>
#include <stdarg.h>


#undef PST_STUB_C_DEF_BEGIN
#undef RETURN
#if CUSTOM_STUB_TYPE(sprintf, 2)
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_CUSTOM_TYPE_2
#define RETURN(x) RETURN_CUSTOM_TYPE(sprintf, x)
#else
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_STD_TYPE_2
#define RETURN(x) return (x)
#endif

#ifdef __C51__
PST_STUB_C_DEF_BEGIN(PST_STUB_KEIL_DEF, int, sprintf, char*, s, const char*, format, HAS_VARARGS, )
#else
PST_STUB_C_DEF_BEGIN(PST_STUB_KEIL_DEF, int, sprintf, signed char*, s, const signed char*, format, HAS_VARARGS, )
#endif
{
  volatile int random = _polyspace_random_int();
  int i;
  for (i=0; i < random; i++) {
    s[i] = random;
  }
#ifndef __polyspace_static_types_for_stubs
#pragma polyspace_check_info returned_value_numeric
#endif
  RETURN(random);
#ifndef __polyspace_static_types_for_stubs
#pragma polyspace_check_info
#endif
}
PST_STUB_C_DEF_END
#define __polyspace_no_sprintf
#endif

#if defined(__polyspace_gets) && !defined(__polyspace_no_gets)

#undef PST_STUB_C_DEF_BEGIN
#undef RETURN
#if CUSTOM_STUB_TYPE(gets, 2)
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_CUSTOM_TYPE_2
#define RETURN(x) RETURN_CUSTOM_TYPE(gets, x)
#else
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_STD_TYPE_2
#define RETURN(x) return (x)
#endif
PST_STUB_C_DEF_BEGIN(PST_STUB_KEIL_DEF, signed char*, gets, signed char*, s, unsigned int, max, NO_VARARGS, )
{
  volatile int random;
  volatile char random_char;
  int n, i;
  if (random)
    RETURN(0); /* case of read error */

  n = random;
  assert(n < max);
  for (i=0; i < n; i++) /* write in s (we have no control on the number of char written) */

    s[i] = random_char;
  s[n] = 0; /* terminate by null char */
  RETURN(s);
}
PST_STUB_C_DEF_END
#define __polyspace_no_gets
#endif



//atof
#if defined(__polyspace_atof) && !defined(__polyspace_no_atof)
#if !defined(POLYSPACE_INSTRUMENT)
#if !defined(NO_CHECKS_INLINING) && !defined(__polyspace_no_inlined_atof)
#pragma POLYSPACE_INLINE_CHECKS "atof"
#endif /* !NO_CHECKS_INLINING */
#if defined(PST_HAS_STRING_H) || (!defined __cplusplus)
#include <string.h>
#endif
#undef atof
#undef PST_STUB_C_DEF_BEGIN
#undef RETURN
#if CUSTOM_STUB_TYPE(atof, 1)
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_CUSTOM_TYPE_1
#define RETURN(x) RETURN_CUSTOM_TYPE(atof, x)
#else
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_STD_TYPE_1
#define RETURN(x) return (x)
#endif
PST_STUB_C_DEF_BEGIN(PST_STUB_C_DEF, double, atof,  void *, s, NO_VARARGS, __PST_THROW) {
  /*
    The 'atof' function converts the initial portion of the string pointed
    to by 's' to 'double' representation.
  */
  volatile double random = 0;
  /*
    The 'atof' function returns the converted value.
  */
  RETURN(random);
}
PST_STUB_C_DEF_END
#pragma POLYSPACE_POLYMORPHIC "atof"
#else
#pragma POLYSPACE_NO_INSTRUMENT "atof"
#endif
#define __polyspace_no_atof
#endif /* __polyspace_atof */

//atoi
#if defined(__polyspace_atoi) && !defined(__polyspace_no_atoi)
#if !defined(POLYSPACE_INSTRUMENT)
#if !defined(NO_CHECKS_INLINING) && !defined(__polyspace_no_inlined_atoi)
#pragma POLYSPACE_INLINE_CHECKS "atoi"
#endif /* !NO_CHECKS_INLINING */
#if defined(PST_HAS_STRING_H) || (!defined __cplusplus)
#include <string.h>
#endif
#undef atoi
#undef PST_STUB_C_DEF_BEGIN
#undef RETURN
#if CUSTOM_STUB_TYPE(atoi, 1)
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_CUSTOM_TYPE_1
#define RETURN(x) RETURN_CUSTOM_TYPE(atoi, x)
#else
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_STD_TYPE_1
#define RETURN(x) return (x)
#endif
PST_STUB_C_DEF_BEGIN(PST_STUB_C_DEF, int, atoi,  void *, s, NO_VARARGS, __PST_THROW) {
  /*
    The 'atoi' function converts the initial portion of the string pointed to
    by 's' to 'int' representation.
  */
  /*
    The 'atoi' function returns the converted value.
  */
  RETURN(_polyspace_random_int());
}
PST_STUB_C_DEF_END
#pragma POLYSPACE_POLYMORPHIC "atoi"
#else
#pragma POLYSPACE_NO_INSTRUMENT "atoi"
#endif
#define __polyspace_no_atoi
#endif /* __polyspace_atoi */

//atol
#if defined(__polyspace_atol) && !defined(__polyspace_no_atol)
#if !defined(POLYSPACE_INSTRUMENT)
#if !defined(NO_CHECKS_INLINING) && !defined(__polyspace_no_inlined_atol)
#pragma POLYSPACE_INLINE_CHECKS "atol"
#endif /* !NO_CHECKS_INLINING */
#if defined(PST_HAS_STRING_H) || (!defined __cplusplus)
#include <string.h>
#endif
#undef atol
#undef PST_STUB_C_DEF_BEGIN
#undef RETURN
#if CUSTOM_STUB_TYPE(atol, 1)
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_CUSTOM_TYPE_1
#define RETURN(x) RETURN_CUSTOM_TYPE(atol, x)
#else
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_STD_TYPE_1
#define RETURN(x) return (x)
#endif
PST_STUB_C_DEF_BEGIN(PST_STUB_C_DEF, long, atol,  void *, s, NO_VARARGS, __PST_THROW) {
  RETURN(_polyspace_random_long());
}
PST_STUB_C_DEF_END
#pragma POLYSPACE_POLYMORPHIC "atol"
#else
#pragma POLYSPACE_NO_INSTRUMENT "atol"
#endif
#define __polyspace_no_atol
#endif /* __polyspace_atol */


#if defined(__polyspace_strlen) && !defined(__polyspace_no_strlen)
#include <string.h>


#undef PST_STUB_C_DEF_BEGIN
#undef RETURN
#if CUSTOM_STUB_TYPE(strlen, 1)
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_CUSTOM_TYPE_1
#define RETURN(x) RETURN_CUSTOM_TYPE(strlen, x)
#else
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_STD_TYPE_1
#define RETURN(x) return (x)
#endif

#ifdef __C51__
PST_STUB_C_DEF_BEGIN(PST_STUB_KEIL_DEF, int, strlen, char*, s, NO_VARARGS, )
#else
PST_STUB_C_DEF_BEGIN(PST_STUB_KEIL_DEF, size_t, strlen, signed char*, s, NO_VARARGS, )
#endif
{
#ifdef __C51__
  int i=0;
#else
  size_t i=0;
#endif
  while (s[i] != 0) {
    i++;
  }
#ifndef __polyspace_static_types_for_stubs
#pragma polyspace_check_info returned_value_numeric
#endif
  RETURN(i);
#ifndef __polyspace_static_types_for_stubs
#pragma polyspace_check_info
#endif

}
PST_STUB_C_DEF_END
#define __polyspace_no_strlen
#endif

#if defined(__polyspace_fstrlen) && !defined(__polyspace_no_fstrlen)
#include <string.h>

#undef PST_STUB_C_DEF_BEGIN
#undef RETURN
#if CUSTOM_STUB_TYPE(fstrlen, 1)
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_CUSTOM_TYPE_1
#define RETURN(x) RETURN_CUSTOM_TYPE(fstrlen, x)
#else
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_STD_TYPE_1
#define RETURN(x) return (x)
#endif
PST_STUB_C_DEF_BEGIN(PST_STUB_KEIL_DEF, size_t, fstrlen, signed char*, s, NO_VARARGS, )
{
  size_t i=0;
  while (s[i] != 0) {
    i++;
  }
#ifndef __polyspace_static_types_for_stubs
#pragma polyspace_check_info returned_value_numeric
#endif
  RETURN(i);
#ifndef __polyspace_static_types_for_stubs
#pragma polyspace_check_info
#endif
}
PST_STUB_C_DEF_END
#define __polyspace_no_fstrlen
#endif

#if defined(__polyspace_memset) && !defined(__polyspace_no_memset)
#include <string.h>


#undef PST_STUB_C_DEF_BEGIN
#undef RETURN
#if CUSTOM_STUB_TYPE(memset, 3)
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_CUSTOM_TYPE_3
#define RETURN(x) RETURN_CUSTOM_TYPE(memset, x)
#else
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_STD_TYPE_3
#define RETURN(x) return (x)
#endif

#ifdef __C51__
PST_STUB_C_DEF_BEGIN(PST_STUB_KEIL_DEF, void*, memset, void*, s, char, c, int, n, NO_VARARGS, )
#else
PST_STUB_C_DEF_BEGIN(PST_STUB_KEIL_DEF, void*, memset, void*, s, signed char, c, unsigned int, n, NO_VARARGS, )
#endif
{
#ifdef __C51__
  int i;
  char *p;
  p = (char *)s;
#else
  unsigned int i;
  signed char *p;
  p = (signed char *)s;
#endif
  for(i=0; i < n; i++)
    p[i] = c;
  RETURN(s);
}
PST_STUB_C_DEF_END
#define __polyspace_no_memset
#endif

#if defined(__polyspace_fmemset) && !defined(__polyspace_no_fmemset)
#include <string.h>

#undef PST_STUB_C_DEF_BEGIN
#undef RETURN
#if CUSTOM_STUB_TYPE(fmemset, 3)
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_CUSTOM_TYPE_3
#define RETURN(x) RETURN_CUSTOM_TYPE(fmemset, x)
#else
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_STD_TYPE_3
#define RETURN(x) return (x)
#endif
PST_STUB_C_DEF_BEGIN(PST_STUB_KEIL_DEF, void*, fmemset, void*, s, signed char, c, unsigned int, n, NO_VARARGS, )
{
  unsigned int i;
  signed char *p;
  p = (signed char *)s;
  for(i=0; i < n; i++)
    p[i] = c;
  RETURN(s);
}
PST_STUB_C_DEF_END
#define __polyspace_no_fmemset
#endif

#if defined(__polyspace_xmemset) && !defined(__polyspace_no_xmemset)
#include <string.h>

#undef PST_STUB_C_DEF_BEGIN
#undef RETURN
#if CUSTOM_STUB_TYPE(xmemset, 3)
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_CUSTOM_TYPE_3
#define RETURN(x) RETURN_CUSTOM_TYPE(xmemset, x)
#else
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_STD_TYPE_3
#define RETURN(x) return (x)
#endif
PST_STUB_C_DEF_BEGIN(PST_STUB_KEIL_DEF, void*, xmemset, void*, s, signed char, c, unsigned long, n, NO_VARARGS, )
{
  unsigned long i;
  signed char *p;
  p = (signed char *)s;
  for(i=0; i < n; i++)
    p[i] = c;
  RETURN(s);
}
PST_STUB_C_DEF_END
#define __polyspace_no_xmemset
#endif

#if defined(__polyspace_memmove) && !defined(__polyspace_no_memmove)
extern char _polyspace_memmove_tmp[];
#include <string.h>

#undef PST_STUB_C_DEF_BEGIN
#undef RETURN
#if CUSTOM_STUB_TYPE(memmove, 3)
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_CUSTOM_TYPE_3
#define RETURN(x) RETURN_CUSTOM_TYPE(memmove, x)
#else
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_STD_TYPE_3
#define RETURN(x) return (x)
#endif
PST_STUB_C_DEF_BEGIN(PST_STUB_KEIL_DEF, void*, memmove, void*, s1, void*, s2, unsigned int, n, NO_VARARGS, )
{
  memcpy(_polyspace_memmove_tmp, s2, n);
  memcpy(s1, _polyspace_memmove_tmp, n);
  RETURN(s1);
}
PST_STUB_C_DEF_END
#define __polyspace_no_memmove
#endif

#if defined(__polyspace_fmemmove) && !defined(__polyspace_no_fmemmove)
extern char _polyspace_memmove_tmp[];
#include <string.h>

#undef PST_STUB_C_DEF_BEGIN
#undef RETURN
#if CUSTOM_STUB_TYPE(fmemmove, 3)
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_CUSTOM_TYPE_3
#define RETURN(x) RETURN_CUSTOM_TYPE(fmemmove, x)
#else
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_STD_TYPE_3
#define RETURN(x) return (x)
#endif
PST_STUB_C_DEF_BEGIN(PST_STUB_KEIL_DEF, void*, fmemmove, void*, s1, void*, s2, unsigned int, n, NO_VARARGS, )
{
  fmemcpy(_polyspace_memmove_tmp, s2, n);
  fmemcpy(s1, _polyspace_memmove_tmp, n);
  RETURN(s1);
}
PST_STUB_C_DEF_END
#define __polyspace_no_fmemmove
#endif

#if defined(__polyspace_xmemmove) && !defined(__polyspace_no_xmemmove)
extern char _polyspace_memmove_tmp[];
#include <string.h>

#undef PST_STUB_C_DEF_BEGIN
#undef RETURN
#if CUSTOM_STUB_TYPE(xmemmove, 3)
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_CUSTOM_TYPE_3
#define RETURN(x) RETURN_CUSTOM_TYPE(xmemmove, x)
#else
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_STD_TYPE_3
#define RETURN(x) return (x)
#endif
PST_STUB_C_DEF_BEGIN(PST_STUB_KEIL_DEF, void*, xmemmove, void*, s1, void*, s2, unsigned long, n, NO_VARARGS, )
{
  xmemcpy(_polyspace_memmove_tmp, s2, n);
  xmemcpy(s1, _polyspace_memmove_tmp, n);
  RETURN(s1);
}
PST_STUB_C_DEF_END
#define __polyspace_no_xmemmove
#endif

#if defined(__polyspace_strncpy) && !defined(__polyspace_no_strncpy)
#include <string.h>

#undef PST_STUB_C_DEF_BEGIN
#undef RETURN
#if CUSTOM_STUB_TYPE(strncpy, 3)
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_CUSTOM_TYPE_3
#define RETURN(x) RETURN_CUSTOM_TYPE(strncpy, x)
#else
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_STD_TYPE_3
#define RETURN(x) return (x)
#endif
PST_STUB_C_DEF_BEGIN(PST_STUB_KEIL_DEF, signed char*, strncpy, signed char*, s1, signed char*, s2, unsigned int, n, NO_VARARGS, )
{
  unsigned int i, s2_len=0;
  while (s2[s2_len] != 0) s2_len++; /* s2_len = strlen(s2) */
  for (i = 0; i < n ; i++) {
    if (i < s2_len)
      s1[i] = s2[i];
    else
      s1[i] = 0;
  }
  RETURN(s1);
}
PST_STUB_C_DEF_END
#define __polyspace_no_strncpy
#endif

#if defined(__polyspace_fstrncpy) && !defined(__polyspace_no_fstrncpy)
#include <string.h>

#undef PST_STUB_C_DEF_BEGIN
#undef RETURN
#if CUSTOM_STUB_TYPE(fstrncpy, 3)
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_CUSTOM_TYPE_3
#define RETURN(x) RETURN_CUSTOM_TYPE(fstrncpy, x)
#else
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_STD_TYPE_3
#define RETURN(x) return (x)
#endif
PST_STUB_C_DEF_BEGIN(PST_STUB_KEIL_DEF, signed char*, fstrncpy, signed char*, s1, signed char*, s2, unsigned int, n, NO_VARARGS, )
{
  unsigned int i, s2_len=0;
  while (s2[s2_len] != 0) s2_len++; /* s2_len = strlen(s2) */
  for (i = 0; i < n ; i++) {
    if (i < s2_len)
      s1[i] = s2[i];
    else
      s1[i] = 0;
  }
  RETURN(s1);
}
PST_STUB_C_DEF_END
#define __polyspace_no_fstrncpy
#endif

#if defined(__polyspace_strcat) && !defined(__polyspace_no_strcat)

#undef PST_STUB_C_DEF_BEGIN
#undef RETURN
#if CUSTOM_STUB_TYPE(strcat, 2)
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_CUSTOM_TYPE_2
#define RETURN(x) RETURN_CUSTOM_TYPE(strcat, x)
#else
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_STD_TYPE_2
#define RETURN(x) return (x)
#endif
PST_STUB_C_DEF_BEGIN(PST_STUB_KEIL_DEF, signed char*, strcat, signed char*, s1, signed char*, s2, NO_VARARGS, )
{
  int i=0, j=0, k;
  while (s1[i] != 0) i++; /* i = strlen(s1) */
  while (s2[j] != 0) j++; /* j = strlen(s2) */
  for (k = 0; k < j; k++)
    s1[i + k] = s2[k];
  RETURN(s1);
}
PST_STUB_C_DEF_END
#define __polyspace_no_strcat
#endif

#if defined(__polyspace_fstrcat) && !defined(__polyspace_no_fstrcat)

#undef PST_STUB_C_DEF_BEGIN
#undef RETURN
#if CUSTOM_STUB_TYPE(fstrcat, 2)
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_CUSTOM_TYPE_2
#define RETURN(x) RETURN_CUSTOM_TYPE(fstrcat, x)
#else
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_STD_TYPE_2
#define RETURN(x) return (x)
#endif
PST_STUB_C_DEF_BEGIN(PST_STUB_KEIL_DEF, signed char*, fstrcat, signed char*, s1, signed char*, s2, NO_VARARGS, )
{
  int i=0, j=0, k;
  while (s1[i] != 0) i++; /* i = strlen(s1) */
  while (s2[j] != 0) j++; /* j = strlen(s2) */
  for (k = 0; k < j; k++)
    s1[i + k] = s2[k];
  RETURN(s1);
}
PST_STUB_C_DEF_END
#define __polyspace_no_fstrcat
#endif

#if defined(__polyspace_strncat) && !defined(__polyspace_no_strncat)
#include <string.h>

#undef PST_STUB_C_DEF_BEGIN
#undef RETURN
#if CUSTOM_STUB_TYPE(strncat, 3)
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_CUSTOM_TYPE_3
#define RETURN(x) RETURN_CUSTOM_TYPE(strncat, x)
#else
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_STD_TYPE_3
#define RETURN(x) return (x)
#endif
PST_STUB_C_DEF_BEGIN(PST_STUB_KEIL_DEF, signed char*, strncat, signed char*, s1, signed char*, s2, unsigned int, n, NO_VARARGS, )
{
  unsigned int i, s1_len=0, s2_len=0;
  while (s1[s1_len] != 0) s1_len++; /* s1_len = strlen(s1) */
  while (s2[s2_len] != 0) s2_len++; /* s2_len = strlen(s2) */
  for (i = 0; i < s2_len && i < n; i++)
    s1[s1_len + i] = s2[i];
  s1[i] = 0;
  RETURN(s1);
}
PST_STUB_C_DEF_END
#define __polyspace_no_strncat
#endif

#if defined(__polyspace_fstrncat) && !defined(__polyspace_no_fstrncat)
#include <string.h>

#undef PST_STUB_C_DEF_BEGIN
#undef RETURN
#if CUSTOM_STUB_TYPE(fstrncat, 3)
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_CUSTOM_TYPE_3
#define RETURN(x) RETURN_CUSTOM_TYPE(fstrncat, x)
#else
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_STD_TYPE_3
#define RETURN(x) return (x)
#endif
PST_STUB_C_DEF_BEGIN(PST_STUB_KEIL_DEF, signed char*, fstrncat, signed char*, s1, signed char*, s2, unsigned int, n, NO_VARARGS, )
{
  unsigned int i, s1_len=0, s2_len=0;
  while (s1[s1_len] != 0) s1_len++; /* s1_len = strlen(s1) */
  while (s2[s2_len] != 0) s2_len++; /* s2_len = strlen(s2) */
  for (i = 0; i < s2_len && i < n; i++)
    s1[s1_len + i] = s2[i];
  s1[i] = 0;
  RETURN(s1);
}
PST_STUB_C_DEF_END
#define __polyspace_no_fstrncat
#endif

#if defined(__polyspace_strncmp) && !defined(__polyspace_no_strncmp)
#include <string.h>

#undef PST_STUB_C_DEF_BEGIN
#undef RETURN
#if CUSTOM_STUB_TYPE(strncmp, 3)
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_CUSTOM_TYPE_3
#define RETURN(x) RETURN_CUSTOM_TYPE(strncmp, x)
#else
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_STD_TYPE_3
#define RETURN(x) return (x)
#endif
PST_STUB_C_DEF_BEGIN(PST_STUB_KEIL_DEF, int, strncmp, signed char*, s1, signed char*, s2, unsigned int, n, NO_VARARGS, )
{
  unsigned int i;
  int res;
  unsigned int l1=0, l2=0;
  while (s1[l1] != 0) l1++; /* l1 = strlen(s1) */
  while (s2[l2] != 0) l2++; /* l2 = strlen(s2) */
  if (l1 >= l2)
    {
      for (i=0; i < l2; i++)
	if ((res = (((unsigned char)*s1) - ((unsigned char)*s2))) || (i == n-1)) {
#ifndef __polyspace_static_types_for_stubs
#pragma polyspace_check_info returned_value_numeric
#endif
          RETURN(res);
#ifndef __polyspace_static_types_for_stubs
#pragma polyspace_check_info
#endif
        }

    }
  else
    {
      for (i=0; i < l1; i++)
	if ((res = (((unsigned char)*s1) - ((unsigned char)*s2))) || (i == n-1)) {
#ifndef __polyspace_static_types_for_stubs
#pragma polyspace_check_info returned_value_numeric
#endif
          RETURN(res);
#ifndef __polyspace_static_types_for_stubs
#pragma polyspace_check_info
#endif
        }
    }
  
  if (l1 < l2) {
#ifndef __polyspace_static_types_for_stubs
#pragma polyspace_check_info returned_value_numeric
#endif
    RETURN(-1);
#ifndef __polyspace_static_types_for_stubs
#pragma polyspace_check_info
#endif
  }
  
  if (l1 > l2) {
#ifndef __polyspace_static_types_for_stubs
#pragma polyspace_check_info returned_value_numeric
#endif
    RETURN(1);
#ifndef __polyspace_static_types_for_stubs
#pragma polyspace_check_info
#endif
  }

#ifndef __polyspace_static_types_for_stubs
#pragma polyspace_check_info returned_value_numeric
#endif
    RETURN(0);
#ifndef __polyspace_static_types_for_stubs
#pragma polyspace_check_info
#endif
}
PST_STUB_C_DEF_END
#define __polyspace_no_strncmp
#endif

#if defined(__polyspace_fstrncmp) && !defined(__polyspace_no_fstrncmp)
#include <string.h>

#undef PST_STUB_C_DEF_BEGIN
#undef RETURN
#if CUSTOM_STUB_TYPE(fstrncmp, 3)
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_CUSTOM_TYPE_3
#define RETURN(x) RETURN_CUSTOM_TYPE(fstrncmp, x)
#else
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_STD_TYPE_3
#define RETURN(x) return (x)
#endif
PST_STUB_C_DEF_BEGIN(PST_STUB_KEIL_DEF, int, fstrncmp, signed char*, s1, signed char*, s2, unsigned int, n, NO_VARARGS, )
{
  unsigned int i;
  int res;
  unsigned int l1=0, l2=0;
  while (s1[l1] != 0) l1++; /* l1 = strlen(s1) */
  while (s2[l2] != 0) l2++; /* l2 = strlen(s2) */
  if (l1 >= l2)
    {
      for (i=0; i < l2; i++)
	if ((res = (((unsigned char)*s1) - ((unsigned char)*s2))) || (i == n-1)) {
#ifndef __polyspace_static_types_for_stubs
#pragma polyspace_check_info returned_value_numeric
#endif
          RETURN(res);
#ifndef __polyspace_static_types_for_stubs
#pragma polyspace_check_info
#endif
        }
    }
  else
    {
      for (i=0; i < l1; i++)
	if ((res = (((unsigned char)*s1) - ((unsigned char)*s2))) || (i == n-1)) {
#ifndef __polyspace_static_types_for_stubs
#pragma polyspace_check_info returned_value_numeric
#endif
          RETURN(res);
#ifndef __polyspace_static_types_for_stubs
#pragma polyspace_check_info
#endif
        }
    }
  
  if (l1 < l2) {
#ifndef __polyspace_static_types_for_stubs
#pragma polyspace_check_info returned_value_numeric
#endif
    RETURN(-1);
#ifndef __polyspace_static_types_for_stubs
#pragma polyspace_check_info
#endif
  }
  
  if (l1 > l2) {
#ifndef __polyspace_static_types_for_stubs
#pragma polyspace_check_info returned_value_numeric
#endif
    RETURN(1);
#ifndef __polyspace_static_types_for_stubs
#pragma polyspace_check_info
#endif
  }
  
#ifndef __polyspace_static_types_for_stubs
#pragma polyspace_check_info returned_value_numeric
#endif
  RETURN(0);
#ifndef __polyspace_static_types_for_stubs
#pragma polyspace_check_info
#endif
}
PST_STUB_C_DEF_END
#define __polyspace_no_fstrncmp
#endif

#if defined(__polyspace_memchr) && !defined(__polyspace_no_memchr)
#include <string.h>

#undef PST_STUB_C_DEF_BEGIN
#undef RETURN
#if CUSTOM_STUB_TYPE(memchr, 3)
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_CUSTOM_TYPE_3
#define RETURN(x) RETURN_CUSTOM_TYPE(memchr, x)
#else
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_STD_TYPE_3
#define RETURN(x) return (x)
#endif
PST_STUB_C_DEF_BEGIN(PST_STUB_KEIL_DEF, void*, memchr, void*, s, signed int, c, unsigned int, n, NO_VARARGS, )
{
  unsigned int i;
  signed char *p;

  p = (signed char*)s;
  for (i=0; i<n; i++)
    if (p[i] == c)
      RETURN(p + i);

  RETURN((void*)0);
}
PST_STUB_C_DEF_END
#define __polyspace_no_memchr
#endif

#if defined(__polyspace_fmemchr) && !defined(__polyspace_no_fmemchr)
#include <string.h>

#undef PST_STUB_C_DEF_BEGIN
#undef RETURN
#if CUSTOM_STUB_TYPE(fmemchr, 3)
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_CUSTOM_TYPE_3
#define RETURN(x) RETURN_CUSTOM_TYPE(fmemchr, x)
#else
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_STD_TYPE_3
#define RETURN(x) return (x)
#endif
PST_STUB_C_DEF_BEGIN(PST_STUB_KEIL_DEF, void*, fmemchr, void*, s, signed int, c, unsigned int, n, NO_VARARGS, )
{
  unsigned int i;
  signed char *p;

  p = (signed char*)s;
  for (i=0; i<n; i++)
    if (p[i] == c)
      RETURN(p + i);

  RETURN((void*)0);
}
PST_STUB_C_DEF_END
#define __polyspace_no_fmemchr
#endif

#if defined(__polyspace_xmemchr) && !defined(__polyspace_no_xmemchr)
#include <string.h>

#undef PST_STUB_C_DEF_BEGIN
#undef RETURN
#if CUSTOM_STUB_TYPE(xmemchr, 3)
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_CUSTOM_TYPE_3
#define RETURN(x) RETURN_CUSTOM_TYPE(xmemchr, x)
#else
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_STD_TYPE_3
#define RETURN(x) return (x)
#endif
PST_STUB_C_DEF_BEGIN(PST_STUB_KEIL_DEF, void*, xmemchr, void*, s, signed int, c, unsigned long, n, NO_VARARGS, )
{
  unsigned long i;
  signed char *p;

  p = (signed char*)s;
  for (i=0; i<n; i++)
    if (p[i] == c)
      RETURN(p + i);

  RETURN((void*)0);
}
PST_STUB_C_DEF_END
#define __polyspace_no_xmemchr
#endif

#if defined(__polyspace_strchr) && !defined(__polyspace_no_strchr)

#undef PST_STUB_C_DEF_BEGIN
#undef RETURN
#if CUSTOM_STUB_TYPE(strchr, 2)
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_CUSTOM_TYPE_2
#define RETURN(x) RETURN_CUSTOM_TYPE(strchr, x)
#else
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_STD_TYPE_2
#define RETURN(x) return (x)
#endif
PST_STUB_C_DEF_BEGIN(PST_STUB_KEIL_DEF, signed char*, strchr, signed char*, s, signed char, c, NO_VARARGS, )
{
  unsigned int i, length=0;
  while (s[length] != 0) length++; /* length = strlen(s) */
  length++; /* length = strlen(s) + 1 */
  for (i=0; i<length; i++)
    if (s[i] == c) RETURN((signed char*)(s+i));

  RETURN(0);
}
PST_STUB_C_DEF_END
#define __polyspace_no_strchr
#endif

#if defined(__polyspace_fstrchr) && !defined(__polyspace_no_fstrchr)

#undef PST_STUB_C_DEF_BEGIN
#undef RETURN
#if CUSTOM_STUB_TYPE(fstrchr, 2)
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_CUSTOM_TYPE_2
#define RETURN(x) RETURN_CUSTOM_TYPE(fstrchr, x)
#else
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_STD_TYPE_2
#define RETURN(x) return (x)
#endif
PST_STUB_C_DEF_BEGIN(PST_STUB_KEIL_DEF, signed char*, fstrchr, signed char*, s, signed char, c, NO_VARARGS, )
{
  unsigned int i, length=0;
  while (s[length] != 0) length++; /* length = strlen(s) */
  length++; /* length = strlen(s) + 1 */
  for (i=0; i<length; i++)
    if (s[i] == c) RETURN((signed char*)(s+i));

  RETURN(0);
}
PST_STUB_C_DEF_END
#define __polyspace_no_fstrchr
#endif




//strcspn
#if defined(__polyspace_strcspn) && !defined(__polyspace_no_strcspn)
#if !defined(POLYSPACE_INSTRUMENT)
#if !defined(NO_CHECKS_INLINING) && !defined(__polyspace_no_inlined_strcspn)
#pragma POLYSPACE_INLINE_CHECKS "strcspn"
#endif /* !NO_CHECKS_INLINING */
#if defined(PST_HAS_STRING_H) || (!defined __cplusplus)
#include <string.h>
#endif
#undef strcspn
#undef PST_STUB_C_DEF_BEGIN
#undef RETURN
#if CUSTOM_STUB_TYPE(strcspn, 2)
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_CUSTOM_TYPE_2
#define RETURN(x) RETURN_CUSTOM_TYPE(strcspn, x)
#else
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_STD_TYPE_2
#define RETURN(x) return (x)
#endif
PST_STUB_C_DEF_BEGIN(PST_STUB_C_DEF, int, strcspn, signed char *, s1, signed char *, s2, NO_VARARGS, __PST_THROW)
{
  /*
    The 'strcspn' function computes the length of the maximum initial segment
    of the string pointed to by 's1' which consists entirely of characters not
    from the string pointed to by 's2'.
  */
  /*
    The 'strcspn' function returns the length of the segment.
  */
  RETURN(_polyspace_random_int());
}
PST_STUB_C_DEF_END
#pragma POLYSPACE_POLYMORPHIC "strcspn"
#else
#pragma POLYSPACE_NO_INSTRUMENT "strcspn"
#endif
#define __polyspace_no_strcspn
#endif /* __polyspace_strcspn */

//fstrcspn
#if defined(__polyspace_fstrcspn) && !defined(__polyspace_no_fstrcspn)
#if !defined(POLYSPACE_INSTRUMENT)
#if !defined(NO_CHECKS_INLINING) && !defined(__polyspace_no_inlined_fstrcspn)
#pragma POLYSPACE_INLINE_CHECKS "fstrcspn"
#endif /* !NO_CHECKS_INLINING */
#if defined(PST_HAS_STRING_H) || (!defined __cplusplus)
#include <string.h>
#endif
#undef fstrcspn
#undef PST_STUB_C_DEF_BEGIN
#undef RETURN
#if CUSTOM_STUB_TYPE(fstrcspn, 2)
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_CUSTOM_TYPE_2
#define RETURN(x) RETURN_CUSTOM_TYPE(fstrcspn, x)
#else
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_STD_TYPE_2
#define RETURN(x) return (x)
#endif
PST_STUB_C_DEF_BEGIN(PST_STUB_C_DEF, int, fstrcspn, signed char *, s1, signed char *, s2, NO_VARARGS, __PST_THROW)
{
    RETURN(strcspn(s1,s1));
}
PST_STUB_C_DEF_END
#pragma POLYSPACE_POLYMORPHIC "fstrcspn"
#else
#pragma POLYSPACE_NO_INSTRUMENT "fstrcspn"
#endif
#define __polyspace_no_fstrcspn
#endif /* __polyspace_fstrcspn */

#if defined(__polyspace_strpbrk) && !defined(__polyspace_no_strpbrk)

#undef PST_STUB_C_DEF_BEGIN
#undef RETURN
#if CUSTOM_STUB_TYPE(strpbrk, 2)
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_CUSTOM_TYPE_2
#define RETURN(x) RETURN_CUSTOM_TYPE(strpbrk, x)
#else
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_STD_TYPE_2
#define RETURN(x) return (x)
#endif
PST_STUB_C_DEF_BEGIN(PST_STUB_KEIL_DEF, signed char*, strpbrk, signed char*, s1, signed char*, s2, NO_VARARGS, )
{
  volatile int random;

  if (random) RETURN(0);

  RETURN((signed char*)(s1 + random));
}
PST_STUB_C_DEF_END
#define __polyspace_no_strpbrk
#endif

#if defined(__polyspace_fstrpbrk) && !defined(__polyspace_no_fstrpbrk)

#undef PST_STUB_C_DEF_BEGIN
#undef RETURN
#if CUSTOM_STUB_TYPE(fstrpbrk, 2)
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_CUSTOM_TYPE_2
#define RETURN(x) RETURN_CUSTOM_TYPE(fstrpbrk, x)
#else
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_STD_TYPE_2
#define RETURN(x) return (x)
#endif
PST_STUB_C_DEF_BEGIN(PST_STUB_KEIL_DEF, signed char*, fstrpbrk, signed char*, s1, signed char*, s2, NO_VARARGS, )
{
  volatile int random;

  if (random) RETURN(0);

  RETURN((signed char*)(s1 + random));
}
PST_STUB_C_DEF_END
#define __polyspace_no_fstrpbrk
#endif

#if defined(__polyspace_strrchr) && !defined(__polyspace_no_strrchr)

#undef PST_STUB_C_DEF_BEGIN
#undef RETURN
#if CUSTOM_STUB_TYPE(strrchr, 2)
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_CUSTOM_TYPE_2
#define RETURN(x) RETURN_CUSTOM_TYPE(strrchr, x)
#else
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_STD_TYPE_2
#define RETURN(x) return (x)
#endif
PST_STUB_C_DEF_BEGIN(PST_STUB_KEIL_DEF, signed char*, strrchr, signed char*, s, signed char, c, NO_VARARGS, )
{
  volatile int random;

  if (random) RETURN(0);

  RETURN((signed char*)(s + random));
}
PST_STUB_C_DEF_END
#define __polyspace_no_strrchr
#endif

#if defined(__polyspace_fstrrchr) && !defined(__polyspace_no_fstrrchr)

#undef PST_STUB_C_DEF_BEGIN
#undef RETURN
#if CUSTOM_STUB_TYPE(fstrrchr, 2)
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_CUSTOM_TYPE_2
#define RETURN(x) RETURN_CUSTOM_TYPE(fstrrchr, x)
#else
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_STD_TYPE_2
#define RETURN(x) return (x)
#endif
PST_STUB_C_DEF_BEGIN(PST_STUB_KEIL_DEF, signed char*, fstrrchr, signed char*, s, signed char, c, NO_VARARGS, )
{
  volatile int random;

  if (random) RETURN(0);

  RETURN((signed char*)(s + random));
}
PST_STUB_C_DEF_END
#define __polyspace_no_fstrrchr
#endif



//strspn
#if defined(__polyspace_strspn) && !defined(__polyspace_no_strspn)
#if !defined(POLYSPACE_INSTRUMENT)
#if !defined(NO_CHECKS_INLINING) && !defined(__polyspace_no_inlined_strspn)
#pragma POLYSPACE_INLINE_CHECKS "strspn"
#endif /* !NO_CHECKS_INLINING */
#if defined(PST_HAS_STRING_H) || (!defined __cplusplus)
#include <string.h>
#endif
#undef strspn
#undef PST_STUB_C_DEF_BEGIN
#undef RETURN
#if CUSTOM_STUB_TYPE(strspn, 2)
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_CUSTOM_TYPE_2
#define RETURN(x) RETURN_CUSTOM_TYPE(strspn, x)
#else
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_STD_TYPE_2
#define RETURN(x) return (x)
#endif
PST_STUB_C_DEF_BEGIN(PST_STUB_C_DEF, int, strspn, signed char *, s1, signed char *, s2, NO_VARARGS, __PST_THROW)
{
  size_t len = 0;
  size_t i;
  /*
    The 'strspn' function computes the length of the maximum initial segment
    of the string pointed to by 's1' which consists entirely of characters
    from the string pointed to by 's2'.
  */

  len = __ps_builtin_strlen(s1);
  /*
    The 'strspn' function returns the length of the segment.
  */
  i = _polyspace_random_size_t();
  APPLY_CONSTRAINT(i <= len);
  RETURN(i);
}
PST_STUB_C_DEF_END
#pragma POLYSPACE_POLYMORPHIC "strspn"
#else
#pragma POLYSPACE_NO_INSTRUMENT "strspn"
#endif
#define __polyspace_no_strspn
#endif /* __polyspace_strspn */

//fstrspn
#if defined(__polyspace_fstrspn) && !defined(__polyspace_no_fstrspn)
#if !defined(POLYSPACE_INSTRUMENT)
#if !defined(NO_CHECKS_INLINING) && !defined(__polyspace_no_inlined_fstrspn)
#pragma POLYSPACE_INLINE_CHECKS "fstrspn"
#endif /* !NO_CHECKS_INLINING */
#if defined(PST_HAS_STRING_H) || (!defined __cplusplus)
#include <string.h>
#endif
#undef fstrspn
#undef PST_STUB_C_DEF_BEGIN
#undef RETURN
#if CUSTOM_STUB_TYPE(fstrspn, 2)
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_CUSTOM_TYPE_2
#define RETURN(x) RETURN_CUSTOM_TYPE(fstrspn, x)
#else
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_STD_TYPE_2
#define RETURN(x) return (x)
#endif
PST_STUB_C_DEF_BEGIN(PST_STUB_C_DEF, int, fstrspn, signed char *, s1, signed char *, s2, NO_VARARGS, __PST_THROW)
{
  RETURN(strspn(s1,s2));
}
PST_STUB_C_DEF_END
#pragma POLYSPACE_POLYMORPHIC "fstrspn"
#else
#pragma POLYSPACE_NO_INSTRUMENT "fstrspn"
#endif
#define __polyspace_no_fstrspn
#endif /* __polyspace_fstrspn */


#if defined(__polyspace_strstr) && !defined(__polyspace_no_strstr)

#undef PST_STUB_C_DEF_BEGIN
#undef RETURN
#if CUSTOM_STUB_TYPE(strstr, 2)
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_CUSTOM_TYPE_2
#define RETURN(x) RETURN_CUSTOM_TYPE(strstr, x)
#else
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_STD_TYPE_2
#define RETURN(x) return (x)
#endif
PST_STUB_C_DEF_BEGIN(PST_STUB_KEIL_DEF, signed char*, strstr, signed char*, s1, signed char*, s2, NO_VARARGS, )
{
  volatile int random;

  if (random) RETURN(0);

  RETURN((signed char*)(s1 + random));
}
PST_STUB_C_DEF_END
#define __polyspace_no_strstr
#endif

#if defined(__polyspace_toupper) && !defined(__polyspace_no_toupper)

#undef PST_STUB_C_DEF_BEGIN
#undef RETURN
#if CUSTOM_STUB_TYPE(toupper, 1)
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_CUSTOM_TYPE_1
#define RETURN(x) RETURN_CUSTOM_TYPE(toupper, x)
#else
#define PST_STUB_C_DEF_BEGIN PST_STUB_C_STD_TYPE_1
#define RETURN(x) return (x)
#endif
PST_STUB_C_DEF_BEGIN(PST_STUB_KEIL_DEF, unsigned char, toupper, unsigned char, c, NO_VARARGS, )
{
	if (c >= 'a' && c <= 'z') {
#ifndef __polyspace_static_types_for_stubs
#pragma polyspace_check_info returned_value_numeric
#endif
		RETURN(c - 'a' + 'A');
#ifndef __polyspace_static_types_for_stubs
#pragma polyspace_check_info 
#endif
        } else {
#ifndef __polyspace_static_types_for_stubs
#pragma polyspace_check_info returned_value_numeric
#endif
	  RETURN(c);
#ifndef __polyspace_static_types_for_stubs
#pragma polyspace_check_info 
#endif
        }
}
PST_STUB_C_DEF_END
#define __polyspace_no_toupper
#endif

#endif /* defined(__PST_KEIL_COMPILER__) && !defined(__PST_NO_KEIL_STUBS__) */