/*
 *
 * This file and its contents are the property of The MathWorks, Inc.
 * 
 * This file contains confidential proprietary information.
 * The reproduction, distribution, utilization or the communication
 * of this file or any part thereof is strictly prohibited.
 * Offenders will be held liable for the payment of damages.
 *
 * Copyright 1999-2012 The MathWorks, Inc.
 *
 */
// PST stub for class list
// from STL library.
// As for string stub, we made
// the choice to matter only about the
// number of elements contained
// in the list.

#ifndef PST_STL_LIST
#define PST_STL_LIST

#include <__polyspace__container.h>
#include <is_integer_type.h>

// macros undefined at the end of file
#define OUT_OF_RANGE(cond) assert (!(cond))
#define LENGTH_ERROR(cond) assert (!(cond))
#define VALID_RANGE(f,l) assert ((f!=0 && l!=0) && f<=l)
#define VALID_SIZE(s) assert(s <= PST_CONTAINER_MAX_SIZE)
#define VALID_SIZE_MAX(s,n) assert(s  <= PST_CONTAINER_MAX_SIZE - n)
#define VALID_SIZE_MIN(s,n) assert(s     >= n)
#define NON_NULL(p) assert(p != 0)
#define RESET_ELEMENTS()  { value_type* volatile random_element ; _pst_elements = new value_type(*random_element) ; } 
 // create "first" element
#define RESET_ELEMENTS_ON(p)  { value_type* volatile random_element ; p._pst_elements = new value_type(*random_element) ; } 
 // create "first" element

#define ADD_ELEMENT(t) { volatile int random_alias = 0 ; if (random_alias) _pst_elements = new value_type(t) ; }
#define ITERATOR_ELEMENT(i) i(_pst_elements)

namespace std {

#ifdef PST_VISUAL
#pragma pack(push, 8) /* push default value */
#endif


  template<class InputIterator, class value_type, __ps_bool is_int_type> struct __PST_LIST_ADD_ELEMENTS_T  { };
  template<class InputIterator, class value_type>                   struct __PST_LIST_ADD_ELEMENTS_T<InputIterator, value_type, __ps_false> 
  {
    static size_t add(InputIterator __first, InputIterator __last, value_type *&_pst_elements )
    {
      size_t nbelt = 0;

      // Valid range macro require < to be defined on InputIterator, thats not allways __ps_true
      //  if range is not valid, we should get a NTL above

      //VALID_RANGE(__first,__last);
      for (InputIterator tmp = __first; tmp != __last; ++tmp) 
      {
	ADD_ELEMENT(*tmp) ;
	nbelt++ ;
      }
      VALID_SIZE(nbelt) ;
      return nbelt;
    } ; 
  } ;

  // specialization for pointer
  template<class Pointed, class value_type>                   struct __PST_LIST_ADD_ELEMENTS_T<Pointed*, value_type, __ps_false> 
  {
    static size_t add(Pointed* __first, Pointed*  __last, value_type *&_pst_elements )
    {
      VALID_RANGE(__first,__last);
      VALID_SIZE(__last - __first);
      for (Pointed* tmp = __first; tmp != __last; ++tmp)  {  ADD_ELEMENT(*tmp) ; }
      return __last - __first;	
    } ; 
  } ;

  template<class InputIterator, class value_type>                   struct __PST_LIST_ADD_ELEMENTS_T<InputIterator, value_type, __ps_true> 
  { 
    static size_t add(InputIterator __first, InputIterator __last, value_type *&_pst_elements) 
    { 
      ADD_ELEMENT(__last) ;
      return __first;
    }
  } ;


PST_TEMPLATE_DECL_DEF_FOR_CONTAINER(T) 
class list { 

  // types
public:      
  typedef T value_type;
  typedef value_type* pointer;
  typedef const value_type* const_pointer;
  typedef value_type& reference;
  typedef const value_type& const_reference;
  typedef size_t size_type;
  typedef ptrdiff_t difference_type;

#if defined(__PST_STL_LIST_CONST_ITERATOR_DIFFER_ITERATOR__)
    typedef __pst__generic_iterator<bidirectional_iterator_tag, T> iterator;
    typedef __pst__generic_iterator<bidirectional_iterator_tag, const T> const_iterator;
    typedef __pst__reverse_iterator<const_iterator> const_reverse_iterator;
    typedef __pst__reverse_iterator<iterator> reverse_iterator;
#else
    // implementation choice : norm specify that list (and all sequence container) iterator
    //  should be at least forward_iterator; for list bidirectional_iterator seems more suitable
    typedef __pst__generic_iterator<bidirectional_iterator_tag, T> iterator;
    // implementation choice: const_iterator is the same as iterator, this avoids
    // the need for an implicit conversion from const_iterator to iterator
    typedef iterator const_iterator;
    typedef __pst__reverse_iterator<iterator> reverse_iterator;
    // implementation choice: const_reverse_iterator is the same as reverse_iterator, this avoids
    // the need for an implicit conversion from const_reverse_iterator to reverse_iterator
    typedef reverse_iterator const_reverse_iterator;
#endif /* #if defined(__PST_STL_LIST_CONST_ITERATOR_DIFFER_ITERATOR__) */

    typedef PST_ALLOCATOR allocator_type; 

    allocator_type get_allocator() const 
    { 
       PST_RETURN_STAT_FOR_GET_ALLOCATOR ;
    }
private:
    // the current number of elements 
    // contained in the list
  size_type _nbelt;
  pointer _pst_elements ;

public:
  // construct/copy/destroy

  // the default constructor
  // Post-condition : size() == 0
  __ps_explicit list(PST_ALLOCATOR_DECL1) 
  { 
    _nbelt=0;  
    RESET_ELEMENTS() ;
  }

  // Post : size() == __n
  list(size_type __n, const T& __value = T() PST_ALLOCATOR_DECL_LAST) {
    VALID_SIZE(__n);
    _nbelt = __n; 
    volatile int random = 0 ;
    RESET_ELEMENTS() ;
    while (random) _pst_elements = new value_type(__value) ; 
  }

  template <class _InputIterator>
  list(_InputIterator __first, _InputIterator __last PST_ALLOCATOR_DECL_LAST) {
    RESET_ELEMENTS() ;
    _nbelt = __PST_LIST_ADD_ELEMENTS_T<_InputIterator, value_type,
                                  __polyspace_is_int_type<_InputIterator>::is_int_type >::add(__first, 
                                                                                              __last,
										              _pst_elements ); 
  }



  list(const PST_TEMPLATE_CONTAINER_NAME1(list, T)& __x)
  { 
    _nbelt = __x.size(); 
    _pst_elements = new value_type(*__x._pst_elements) ; 
  }

  // Destructor

  ~list()
  {
    _nbelt = 0 ;
    _pst_elements = 0 ;
  }

  iterator begin() {
    return ITERATOR_ELEMENT(iterator) ;
  }

  const_iterator begin() const {
    return ITERATOR_ELEMENT(const_iterator) ;
  }

  iterator end() {
    return ITERATOR_ELEMENT(iterator) ;
  }

  const_iterator end() const {
    return ITERATOR_ELEMENT(const_iterator) ;
  }

  reverse_iterator rbegin() {
    return ITERATOR_ELEMENT(reverse_iterator) ;
  }

  const_reverse_iterator rbegin() const {
    return ITERATOR_ELEMENT(const_reverse_iterator) ;
  }

  reverse_iterator rend() {
    return ITERATOR_ELEMENT(reverse_iterator) ;
  }

  const_reverse_iterator rend() const {
    return ITERATOR_ELEMENT(const_reverse_iterator) ; 
  }
  
  __ps_bool empty() const { 
    return (size() == 0);
  }

  size_type size() const {
    return _nbelt;
  }

  size_type max_size() const {
    return PST_CONTAINER_MAX_SIZE;
  }
  
  reference front() { 
    return *(begin()); // too complicated ?
  }

  const_reference front() const { 
    return *(begin()); // too complicated ?
  }

  reference back() { 
    return *(begin()); // sementically __ps_false ... but correct for verifier with begin impl.
  }
  
  const_reference back() const {
    return *(begin()); // sementically __ps_false ... but correct for verifier with begin impl.
  }

  // swaps __x and *this
  void swap(PST_TEMPLATE_CONTAINER_NAME1(list, T)& x) {
    size_type n = _nbelt;
    _nbelt = x._nbelt;
    x._nbelt = n ;

    pointer tmp = x._pst_elements ;
    x._pst_elements = _pst_elements ;
    _pst_elements = tmp ; 
  }

  iterator insert(iterator __position, const T& __x) {
    NON_NULL(__position);
    VALID_SIZE_MAX(_nbelt,1);
    _nbelt++;
    ADD_ELEMENT(__x) ;
    return ITERATOR_ELEMENT(iterator) ;
  }

  void insert(iterator __pos, size_type __n, const T& __x) {
    NON_NULL(__pos);
    VALID_SIZE_MAX(_nbelt, __n);
    for (int i=0; i<__n; i++) ADD_ELEMENT(__x) ;
    _nbelt += __n;
  }

  template <class InputIterator>
  void insert(iterator position, InputIterator __first,
	      InputIterator __last) {
    size_t added = __PST_LIST_ADD_ELEMENTS_T<InputIterator, value_type,
                                        __polyspace_is_int_type<InputIterator>::is_int_type >::add(__first, 
                                                                                                   __last,
                                                                                                   _pst_elements ); 
    VALID_SIZE_MAX(_nbelt, added);
    _nbelt += added;
  }

  // Those two methods adds a single
  // element to the list controlled
  // by *this
  void push_front(const T& __x) {
    VALID_SIZE_MAX(_nbelt,1);
    _nbelt++;
    ADD_ELEMENT(__x) ;
  }

  // Those two methods add
  // one single element to the list
  // controlled by *this.
  void push_back(const T& __x) {
    VALID_SIZE_MAX(_nbelt,1);
    _nbelt++;
    ADD_ELEMENT(__x) ;
  }

  // This method erases the element
  // pointed to by __position.
  // the list contains one less element.

  iterator erase(iterator __position) {
    NON_NULL(__position);
    VALID_SIZE_MIN(_nbelt,1);
    _nbelt--;
    return ITERATOR_ELEMENT(iterator) ;
  }


  // This method erases all elements
  // contained in the range [__first, __last)
  // size() is decreased by (__last - __first).

  iterator erase(iterator __first, iterator __last) {
    VALID_RANGE(__first, __last);
    VALID_SIZE_MIN(_nbelt, (__last - __first));
    _nbelt -= __last - __first;
    return ITERATOR_ELEMENT(iterator) ;
  }

  // Post = size()==0
  void clear() 
  { 
    _nbelt = 0; 
    RESET_ELEMENTS() ;
  }

  // post : size() == __new_size
  void resize(size_type __new_size, const T& __x = T()){
    VALID_SIZE(__new_size);    
    _nbelt = __new_size;
    volatile int random = 0;
    while (random) ADD_ELEMENT(__x) ;
  }
  
  void pop_front() {
    VALID_SIZE_MIN(_nbelt,1);
    _nbelt--;
  }

  void pop_back() {
    VALID_SIZE_MIN(_nbelt,1);
    _nbelt--;
  }

  PST_TEMPLATE_CONTAINER_NAME1(list, T)& operator=(const PST_TEMPLATE_CONTAINER_NAME1(list, T)& __x) {
    _nbelt = __x.size();
    _pst_elements = new value_type(*(__x._pst_elements)) ;
    return *this;
  }

  void assign(size_type __n, const T& __val) {
    VALID_SIZE(__n);
    _nbelt = __n;
    volatile int random = 0;
    while (random) ADD_ELEMENT(__val) ;
  }

  template <class _InputIterator>
  void assign(_InputIterator __first, _InputIterator __last) {
    RESET_ELEMENTS() ;
    _nbelt = __PST_LIST_ADD_ELEMENTS_T<_InputIterator, value_type,
                                  __polyspace_is_int_type<_InputIterator>::is_int_type >::add(__first,
                                                                                              __last,
                                                                                              _pst_elements );
  }

  // move all elements of x
  // to *this, before position __position.
  // Pre : &x != this
  // Post : __x.empty()==__ps_true
  void splice(iterator __position, list& __x) {
    NON_NULL(__position);
    assert(&__x != this);
    VALID_SIZE_MAX(_nbelt, __x.size());
    _nbelt += __x.size();
    ADD_ELEMENT(*__x._pst_elements) ;
    __x = list();
  }

  // moves element from x pointed to by __i
  // to *this at position __position.
  // the result is unchanged if __position == i 
  // or __position == ++i
  // Post : x  has one less element.

  void splice(iterator __position, list& __x, iterator __i) {
    NON_NULL(__position);
    NON_NULL(__i);
    if (__position != __i && __position!= __i+1) {
      VALID_SIZE_MAX(_nbelt,1);
      VALID_SIZE_MIN(__x._nbelt,1);
      _nbelt++;
      ADD_ELEMENT(*__x._pst_elements) ;/* copy potentielle de tous les objets */
      __x._nbelt--;
    }
  }

  // moves elements in range [__first, __last) from x 
  // to *this, before __position.
  // Pre :  [__first, __last) is a valid range

  void splice(iterator __position, list& __x, iterator __first, iterator __last) {
    NON_NULL(__position);
    VALID_RANGE(__first, __last);
    VALID_SIZE_MAX(_nbelt, (__last - __first));
    VALID_SIZE_MIN(__x._nbelt, (__last - __first));
    _nbelt += __last - __first;
    ADD_ELEMENT(*__x._pst_elements) ;
    __x._nbelt -= __last - __first;
  }
  
  // Removes every ocurrence
  // of __value in the list controlled
  // by *this. So we cannot predict
  // the value of size(), but it can only
  // be smaller.

  void remove(const T& __value) {
    volatile size_type nb_removed = (size_type)0;
    VALID_SIZE_MIN(_nbelt, nb_removed);
    _nbelt -= nb_removed;
  }

  // Erases all the elements in the list
  // referred by a list iterator i for
  // which the following condition holds: pred(*i) != __ps_false.
  template<class Predicate>
  void remove_if(Predicate pred) {
    value_type* volatile elt ;
    __ps_bool b = pred( *(value_type*) elt);
    volatile size_type nb_removed = (size_type)0;
    VALID_SIZE_MIN(_nbelt, nb_removed);
    _nbelt -= nb_removed;	
  }	

  // Removes all but first elements
  // from every consecutive group of
  // equal elements referred to by
  // iterator i in the range [first + 1, last)
  // So we cannot predict what size() will be.
  // We only know that we'll have size() <= size()
  void unique() {
    volatile size_type nb_removed = (size_type)0;

    // the number of elements removed
    // cannot be greater that the number
    // of elements contained in the list.
    assert(nb_removed < _nbelt);
    _nbelt -= nb_removed;
    
  }
  
  template <class BinaryPredicate> void unique(BinaryPredicate binary_pred) {
    volatile size_type nb_removed = (size_type)0;

    // the number of elements removed
    // cannot be greater that the number
    // of elements contained in the list.
    assert(nb_removed < _nbelt);
    _nbelt -= nb_removed;
  }

  void merge(list& x)
  { 
    VALID_SIZE_MAX(_nbelt, x.size());
    _nbelt += x.size();
    ADD_ELEMENT(*x._pst_elements) ;
    // suppress elements from x
    x._nbelt= 0;
    RESET_ELEMENTS_ON(x) ;
  }

  template <class Compare> void merge(list& x, Compare comp) {
    VALID_SIZE_MAX(_nbelt, x.size());
    _nbelt += x.size();
    ADD_ELEMENT(*x._pst_elements) ;
    // suppress elements from x
    x._nbelt= 0;
    RESET_ELEMENTS_ON(x) ;
  }

  // Sorts the elements of the list, 
  // it doesn't affect its number
  // if elements.
  void sort()
  {}

  template <class Compare> void sort(Compare comp) {}

  // Reverses all elements 
  // and so doesn't affect
  // the number of elements
  void reverse() 
  {}

};

PST_TEMPLATE_DECL_FOR_CONTAINER1(class T)
inline __ps_bool operator==(const PST_TEMPLATE_CONTAINER_NAME1(list, T)& __x,
                       const PST_TEMPLATE_CONTAINER_NAME1(list, T)& __y){
  
  if (__x.size() != __y.size())
    return __ps_false;
  volatile __ps_bool b = true;
  return b;
}

PST_TEMPLATE_DECL_FOR_CONTAINER1(class T)
inline __ps_bool operator<(const PST_TEMPLATE_CONTAINER_NAME1(list, T)& __x,
                      const PST_TEMPLATE_CONTAINER_NAME1(list, T)& __y){
  volatile __ps_bool b = false;
  return b;
}

PST_TEMPLATE_DECL_FOR_CONTAINER1(class T)
__ps_bool operator!=(const PST_TEMPLATE_CONTAINER_NAME1(list, T)& x, const PST_TEMPLATE_CONTAINER_NAME1(list, T)& y) {
  volatile __ps_bool b = false;
  if (x.size() != y.size())
      return __ps_true;
  return b;
}

PST_TEMPLATE_DECL_FOR_CONTAINER1(class T)
__ps_bool operator>(const PST_TEMPLATE_CONTAINER_NAME1(list, T)& x, const PST_TEMPLATE_CONTAINER_NAME1(list, T)& y) {
  volatile __ps_bool b = false;
  return b;
}

PST_TEMPLATE_DECL_FOR_CONTAINER1(class T)
__ps_bool operator>=(const PST_TEMPLATE_CONTAINER_NAME1(list, T)& x, const PST_TEMPLATE_CONTAINER_NAME1(list, T)& y) {
  volatile __ps_bool b = false;
  return b;
}


PST_TEMPLATE_DECL_FOR_CONTAINER1(class T)
__ps_bool operator<=(const PST_TEMPLATE_CONTAINER_NAME1(list, T)& x, const PST_TEMPLATE_CONTAINER_NAME1(list, T)& y) {
  volatile __ps_bool b = false;
  return b;
}


PST_TEMPLATE_DECL_FOR_CONTAINER1(class T)
inline void 
swap(PST_TEMPLATE_CONTAINER_NAME1(list, T)& __x, PST_TEMPLATE_CONTAINER_NAME1(list, T)& __y)
{
   __x.swap(__y);
}

#ifdef PST_VISUAL
#pragma pack(pop) /* pop back to previous value */
#endif

} // end namespace std

#ifdef __PST_IMPLICIT_USING_STD
/* Implicitly include a using directive for the STD namespace when this
   preprocessing flag is TRUE. */
using namespace std;
#endif /* ifdef __PST_IMPLICIT_USING_STD */

// undef macros defined in this file
#undef OUT_OF_RANGE
#undef LENGTH_ERROR
#undef VALID_RANGE
#undef VALID_SIZE
#undef VALID_SIZE_MAX
#undef VALID_SIZE_MIN
#undef NON_NULL
#undef ADD_ELEMENT
#undef RESET_ELEMENT
#undef ITERATOR_ELEMENT

#endif /* PST_STL_LIST */