[kernel] Parsing share/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing tests/syntax/multiple_decls_contracts.c (with preprocessing)
[kernel] Parsing tests/syntax/multiple_decls_contracts.c (with preprocessing)
[kernel] Parsing share/libc/string.h (with preprocessing)
tests/syntax/multiple_decls_contracts.c:10:[kernel] warning: dropping duplicate def'n of func strdup at tests/syntax/multiple_decls_contracts.c:10 in favor of that at tests/syntax/multiple_decls_contracts.c:10
/* Generated by Frama-C */
typedef int wchar_t;
typedef unsigned int size_t;
struct __fc_div_t {
   int quot ;
   int rem ;
};
typedef struct __fc_div_t div_t;
struct __fc_ldiv_t {
   long quot ;
   long rem ;
};
typedef struct __fc_ldiv_t ldiv_t;
struct __fc_lldiv_t {
   long long quot ;
   long long rem ;
};
typedef struct __fc_lldiv_t lldiv_t;
/*@
axiomatic MemCmp {
  logic ℤ memcmp{L1, L2}(char *s1, char *s2, ℤ n) 
    reads \at(*(s1 + (0 .. n - 1)),L1), \at(*(s2 + (0 .. n - 1)),L2);
  
  axiom memcmp_zero{L1, L2}:
    ∀ char *s1, char *s2;
    ∀ ℤ n;
      memcmp{L1, L2}(s1, s2, n) ≡ 0 ⇔
      (∀ ℤ i; 0 ≤ i < n ⇒ \at(*(s1 + i),L1) ≡ \at(*(s2 + i),L2));
  
  }
 */
/*@
axiomatic MemChr {
  logic 𝔹 memchr{L}(char *s, ℤ c, ℤ n) 
    reads *(s + (0 .. n - 1));
  
  axiom memchr_def{L}:
    ∀ char *s;
    ∀ ℤ c;
    ∀ ℤ n;
      memchr(s, c, n) ≡ \true ⇔
      (∃ int i; 0 ≤ i < n ∧ *(s + i) ≡ c);
  
  }
 */
/*@
axiomatic MemSet {
  logic 𝔹 memset{L}(char *s, ℤ c, ℤ n) 
    reads *(s + (0 .. n - 1));
  
  axiom memset_def{L}:
    ∀ char *s;
    ∀ ℤ c;
    ∀ ℤ n;
      memset(s, c, n) ≡ \true ⇔
      (∀ ℤ i; 0 ≤ i < n ⇒ *(s + i) ≡ c);
  
  }
 */
/*@
axiomatic StrLen {
  logic ℤ strlen{L}(char *s) 
    reads *(s + (0 ..));
  
  axiom strlen_pos_or_null{L}:
    ∀ char *s;
    ∀ ℤ i;
      0 ≤ i ∧ (∀ ℤ j; 0 ≤ j < i ⇒ *(s + j) ≢ '\000') ∧
      *(s + i) ≡ '\000' ⇒ strlen(s) ≡ i;
  
  axiom strlen_neg{L}:
    ∀ char *s;
      (∀ ℤ i; 0 ≤ i ⇒ *(s + i) ≢ '\000') ⇒ strlen(s) < 0;
  
  axiom strlen_before_null{L}:
    ∀ char *s;
    ∀ ℤ i; 0 ≤ i < strlen(s) ⇒ *(s + i) ≢ '\000';
  
  axiom strlen_at_null{L}:
    ∀ char *s; 0 ≤ strlen(s) ⇒ *(s + strlen(s)) ≡ '\000';
  
  axiom strlen_not_zero{L}:
    ∀ char *s;
    ∀ ℤ i;
      0 ≤ i ≤ strlen(s) ∧ *(s + i) ≢ '\000' ⇒ i < strlen(s);
  
  axiom strlen_zero{L}:
    ∀ char *s;
    ∀ ℤ i;
      0 ≤ i ≤ strlen(s) ∧ *(s + i) ≡ '\000' ⇒ i ≡ strlen(s);
  
  axiom strlen_sup{L}:
    ∀ char *s;
    ∀ ℤ i; 0 ≤ i ∧ *(s + i) ≡ '\000' ⇒ 0 ≤ strlen(s) ≤ i;
  
  axiom strlen_shift{L}:
    ∀ char *s;
    ∀ ℤ i; 0 ≤ i ≤ strlen(s) ⇒ strlen(s + i) ≡ strlen(s) - i;
  
  axiom strlen_create{L}:
    ∀ char *s;
    ∀ ℤ i; 0 ≤ i ∧ *(s + i) ≡ '\000' ⇒ 0 ≤ strlen(s) ≤ i;
  
  axiom strlen_create_shift{L}:
    ∀ char *s;
    ∀ ℤ i;
    ∀ ℤ k;
      0 ≤ k ≤ i ∧ *(s + i) ≡ '\000' ⇒ 0 ≤ strlen(s + k) ≤ i - k;
  
  axiom memcmp_strlen_left{L}:
    ∀ char *s1, char *s2;
    ∀ ℤ n;
      memcmp{L, L}(s1, s2, n) ≡ 0 ∧ strlen(s1) < n ⇒
      strlen(s1) ≡ strlen(s2);
  
  axiom memcmp_strlen_right{L}:
    ∀ char *s1, char *s2;
    ∀ ℤ n;
      memcmp{L, L}(s1, s2, n) ≡ 0 ∧ strlen(s2) < n ⇒
      strlen(s1) ≡ strlen(s2);
  
  axiom memcmp_strlen_shift_left{L}:
    ∀ char *s1, char *s2;
    ∀ ℤ k, ℤ n;
      memcmp{L, L}(s1, s2 + k, n) ≡ 0 ≤ k ∧ strlen(s1) < n ⇒
      0 ≤ strlen(s2) ≤ k + strlen(s1);
  
  axiom memcmp_strlen_shift_right{L}:
    ∀ char *s1, char *s2;
    ∀ ℤ k, ℤ n;
      memcmp{L, L}(s1 + k, s2, n) ≡ 0 ≤ k ∧ strlen(s2) < n ⇒
      0 ≤ strlen(s1) ≤ k + strlen(s2);
  
  }
 */
/*@
axiomatic StrCmp {
  logic ℤ strcmp{L}(char *s1, char *s2) 
    reads *(s1 + (0 .. strlen(s1))), *(s2 + (0 .. strlen(s2)));
  
  axiom strcmp_zero{L}:
    ∀ char *s1, char *s2;
      strcmp(s1, s2) ≡ 0 ⇔
      strlen(s1) ≡ strlen(s2) ∧
      (∀ ℤ i; 0 ≤ i ≤ strlen(s1) ⇒ *(s1 + i) ≡ *(s2 + i));
  
  }
 */
/*@
axiomatic StrNCmp {
  logic ℤ strncmp{L}(char *s1, char *s2, ℤ n) 
    reads *(s1 + (0 .. n - 1)), *(s2 + (0 .. n - 1));
  
  axiom strncmp_zero{L}:
    ∀ char *s1, char *s2;
    ∀ ℤ n;
      strncmp(s1, s2, n) ≡ 0 ⇔
      (strlen(s1) < n ∧ strcmp(s1, s2) ≡ 0) ∨
      (∀ ℤ i; 0 ≤ i < n ⇒ *(s1 + i) ≡ *(s2 + i));
  
  }
 */
/*@
axiomatic StrChr {
  logic 𝔹 strchr{L}(char *s, ℤ c) 
    reads *(s + (0 .. strlen(s)));
  
  axiom strchr_def{L}:
    ∀ char *s;
    ∀ ℤ c;
      strchr(s, c) ≡ \true ⇔
      (∃ ℤ i; 0 ≤ i ≤ strlen(s) ∧ *(s + i) ≡ c);
  
  }
 */
/*@
axiomatic WcsLen {
  logic ℤ wcslen{L}(wchar_t *s) 
    reads *(s + (0 ..));
  
  axiom wcslen_pos_or_null{L}:
    ∀ wchar_t *s;
    ∀ ℤ i;
      0 ≤ i ∧ (∀ ℤ j; 0 ≤ j < i ⇒ *(s + j) ≢ 0) ∧
      *(s + i) ≡ 0 ⇒ wcslen(s) ≡ i;
  
  axiom wcslen_neg{L}:
    ∀ wchar_t *s; (∀ ℤ i; 0 ≤ i ⇒ *(s + i) ≢ 0) ⇒ wcslen(s) < 0;
  
  axiom wcslen_before_null{L}:
    ∀ wchar_t *s;
    ∀ int i; 0 ≤ i < wcslen(s) ⇒ *(s + i) ≢ 0;
  
  axiom wcslen_at_null{L}:
    ∀ wchar_t *s; 0 ≤ wcslen(s) ⇒ *(s + wcslen(s)) ≡ 0;
  
  axiom wcslen_not_zero{L}:
    ∀ wchar_t *s;
    ∀ int i; 0 ≤ i ≤ wcslen(s) ∧ *(s + i) ≢ 0 ⇒ i < wcslen(s);
  
  axiom wcslen_zero{L}:
    ∀ wchar_t *s;
    ∀ int i; 0 ≤ i ≤ wcslen(s) ∧ *(s + i) ≡ 0 ⇒ i ≡ wcslen(s);
  
  axiom wcslen_sup{L}:
    ∀ wchar_t *s;
    ∀ int i; 0 ≤ i ∧ *(s + i) ≡ 0 ⇒ 0 ≤ wcslen(s) ≤ i;
  
  axiom wcslen_shift{L}:
    ∀ wchar_t *s;
    ∀ int i; 0 ≤ i ≤ wcslen(s) ⇒ wcslen(s + i) ≡ wcslen(s) - i;
  
  axiom wcslen_create{L}:
    ∀ wchar_t *s;
    ∀ int i; 0 ≤ i ∧ *(s + i) ≡ 0 ⇒ 0 ≤ wcslen(s) ≤ i;
  
  axiom wcslen_create_shift{L}:
    ∀ wchar_t *s;
    ∀ int i;
    ∀ int k;
      0 ≤ k ≤ i ∧ *(s + i) ≡ 0 ⇒ 0 ≤ wcslen(s + k) ≤ i - k;
  
  }
 */
/*@
axiomatic WcsCmp {
  logic ℤ wcscmp{L}(wchar_t *s1, wchar_t *s2) 
    reads *(s1 + (0 .. wcslen(s1))), *(s2 + (0 .. wcslen(s2)));
  
  axiom wcscmp_zero{L}:
    ∀ wchar_t *s1, wchar_t *s2;
      wcscmp(s1, s2) ≡ 0 ⇔
      wcslen(s1) ≡ wcslen(s2) ∧
      (∀ ℤ i; 0 ≤ i ≤ wcslen(s1) ⇒ *(s1 + i) ≡ *(s2 + i));
  
  }
 */
/*@
axiomatic WcsNCmp {
  logic ℤ wcsncmp{L}(wchar_t *s1, wchar_t *s2, ℤ n) 
    reads *(s1 + (0 .. n - 1)), *(s2 + (0 .. n - 1));
  
  axiom wcsncmp_zero{L}:
    ∀ wchar_t *s1, wchar_t *s2;
    ∀ ℤ n;
      wcsncmp(s1, s2, n) ≡ 0 ⇔
      (wcslen(s1) < n ∧ wcscmp(s1, s2) ≡ 0) ∨
      (∀ ℤ i; 0 ≤ i < n ⇒ *(s1 + i) ≡ *(s2 + i));
  
  }
 */
/*@ logic ℤ minimum(ℤ i, ℤ j) = i < j? i: j;
 */
/*@ logic ℤ maximum(ℤ i, ℤ j) = i < j? j: i;
 */
/*@
predicate valid_string{L}(char *s) =
  0 ≤ strlen(s) ∧ \valid(s + (0 .. strlen(s)));
 */
/*@
predicate valid_read_string{L}(char *s) =
  0 ≤ strlen(s) ∧ \valid_read(s + (0 .. strlen(s)));
 */
/*@
predicate valid_string_or_null{L}(char *s) = s ≡ \null ∨ valid_string(s);
 */
/*@
predicate valid_wstring{L}(wchar_t *s) =
  0 ≤ wcslen(s) ∧ \valid(s + (0 .. wcslen(s)));
 */
/*@
predicate valid_wstring_or_null{L}(wchar_t *s) =
  s ≡ \null ∨ valid_wstring(s);
 */
/*@ requires \valid_read((char *)s1 + (0 .. n - 1));
    requires \valid_read((char *)s2 + (0 .. n - 1));
    ensures
      \result ≡
      memcmp{Pre, Pre}((char *)\old(s1), (char *)\old(s2), \old(n));
    assigns \result;
    assigns \result
      \from *((char *)s1 + (0 .. n - 1)), *((char *)s2 + (0 .. n - 1));
 */
extern int memcmp(void const *s1, void const *s2, size_t n);

/*@ requires \valid_read((unsigned char *)s + (0 .. n - 1));
    assigns \result;
    assigns \result \from s, c, *((unsigned char *)s + (0 .. n - 1));
    
    behavior found:
      assumes memchr((char *)s, c, n) ≡ \true;
      ensures \base_addr(\result) ≡ \base_addr(\old(s));
      ensures (int)*((char *)\result) ≡ \old(c);
      ensures
        ∀ ℤ i;
          0 ≤ i < \old(n) ⇒
          *((unsigned char *)\old(s) + i) ≡ \old(c) ⇒
          \result ≤ \old(s) + i;
    
    behavior not_found:
      assumes ¬(memchr((char *)s, c, n) ≡ \true);
      ensures \result ≡ \null;
 */
extern void *memchr(void const *s, int c, size_t n);

/*@ requires valid_dst: \valid((char *)dest + (0 .. n - 1));
    requires valid_src: \valid_read((char *)src + (0 .. n - 1));
    requires
      \separated((char *)dest + (0 .. n - 1), (char *)src + (0 .. n - 1));
    ensures
      memcmp{Post, Pre}((char *)\old(dest), (char *)\old(src), \old(n)) ≡ 0;
    ensures \result ≡ \old(dest);
    assigns *((char *)dest + (0 .. n - 1)), \result;
    assigns *((char *)dest + (0 .. n - 1))
      \from *((char *)src + (0 .. n - 1));
    assigns \result \from dest;
 */
extern void *memcpy(void *dest, void const *src, size_t n);

/*@ requires valid_dst: \valid((char *)dest + (0 .. n - 1));
    requires valid_src: \valid_read((char *)src + (0 .. n - 1));
    ensures
      memcmp{Post, Pre}((char *)\old(dest), (char *)\old(src), \old(n)) ≡ 0;
    ensures \result ≡ \old(dest);
    assigns *((char *)dest + (0 .. n - 1)), \result;
    assigns *((char *)dest + (0 .. n - 1))
      \from *((char *)src + (0 .. n - 1));
    assigns \result \from dest;
 */
extern void *memmove(void *dest, void const *src, size_t n);

/*@ requires \valid((char *)s + (0 .. n - 1));
    ensures memset((char *)\old(s), \old(c), \old(n)) ≡ \true;
    ensures \result ≡ \old(s);
    assigns *((char *)s + (0 .. n - 1)), \result;
    assigns *((char *)s + (0 .. n - 1)) \from c;
    assigns \result \from s;
 */
extern void *memset(void *s, int c, size_t n);

/*@ requires valid_string_src: valid_read_string(s);
    ensures \result ≡ strlen(\old(s));
    assigns \result;
    assigns \result \from *(s + (0 ..));
 */
extern size_t strlen(char const *s);

/*@ requires valid_string_src: valid_read_string(s);
    ensures \result ≡ strlen(\old(s)) ∨ \result ≡ \old(n);
    assigns \result;
    assigns \result \from *(s + (0 ..));
 */
extern size_t strnlen(char const *s, size_t n);

/*@ requires valid_string_s1: valid_read_string(s1);
    requires valid_string_s2: valid_read_string(s2);
    ensures \result ≡ strcmp(\old(s1), \old(s2));
    assigns \result;
    assigns \result \from *(s1 + (0 ..)), *(s2 + (0 ..));
 */
extern int strcmp(char const *s1, char const *s2);

/*@ requires valid_string_s1: valid_read_string(s1);
    requires valid_string_s2: valid_read_string(s2);
    ensures \result ≡ strncmp(\old(s1), \old(s2), \old(n));
    assigns \result;
    assigns \result \from *(s1 + (0 .. n - 1)), *(s2 + (0 .. n - 1));
 */
extern int strncmp(char const *s1, char const *s2, size_t n);

/*@ requires valid_string_s1: valid_read_string(s1);
    requires valid_string_s2: valid_read_string(s2);
    assigns \result;
    assigns \result \from *(s1 + (0 ..)), *(s2 + (0 ..));
 */
extern int strcoll(char const *s1, char const *s2);

/*@ requires valid_string_src: valid_read_string(s);
    assigns \result;
    assigns \result \from s, *(s + (0 ..)), c;
    
    behavior found:
      assumes strchr(s, c) ≡ \true;
      ensures (int)*\result ≡ \old(c);
      ensures \base_addr(\result) ≡ \base_addr(\old(s));
      ensures \old(s) ≤ \result < \old(s) + strlen(\old(s));
      ensures valid_read_string(\result);
      ensures ∀ char *p; \old(s) ≤ p < \result ⇒ (int)*p ≢ \old(c);
    
    behavior not_found:
      assumes ¬(strchr(s, c) ≡ \true);
      ensures \result ≡ \null;
    
    behavior default:
      ensures
        \result ≡ \null ∨ \base_addr(\result) ≡ \base_addr(\old(s));
 */
extern char *strchr(char const *s, int c);

/*@ requires valid_string_src: valid_read_string(s);
    assigns \result;
    assigns \result \from s, *(s + (0 ..)), c;
    
    behavior found:
      assumes strchr(s, c) ≡ \true;
      ensures (int)*\result ≡ \old(c);
      ensures \base_addr(\result) ≡ \base_addr(\old(s));
      ensures valid_read_string(\result);
    
    behavior not_found:
      assumes ¬(strchr(s, c) ≡ \true);
      ensures \result ≡ \null;
    
    behavior default:
      ensures
        \result ≡ \null ∨ \base_addr(\result) ≡ \base_addr(\old(s));
 */
extern char *strrchr(char const *s, int c);

/*@ requires valid_string_src: valid_read_string(s);
    requires valid_string_reject: valid_read_string(reject);
    ensures 0 ≤ \result ≤ strlen(\old(s));
    assigns \result;
    assigns \result \from *(s + (0 ..)), *(reject + (0 ..));
 */
extern size_t strcspn(char const *s, char const *reject);

/*@ requires valid_string_src: valid_read_string(s);
    requires valid_string_accept: valid_read_string(accept);
    ensures 0 ≤ \result ≤ strlen(\old(s));
    assigns \result;
    assigns \result \from *(s + (0 ..)), *(accept + (0 ..));
 */
extern size_t strspn(char const *s, char const *accept);

/*@ requires valid_string_src: valid_read_string(s);
    requires valid_string_accept: valid_read_string(accept);
    ensures
      \result ≡ (char *)0 ∨ \base_addr(\result) ≡ \base_addr(\old(s));
    assigns \result;
    assigns \result \from s, *(s + (0 ..)), *(accept + (0 ..));
 */
extern char *strpbrk(char const *s, char const *accept);

/*@ requires valid_string_haystack: valid_read_string(haystack);
    requires valid_string_needle: valid_read_string(needle);
    ensures
      \result ≡ (char *)0 ∨
      (\subset(\result, \old(haystack) + (0 ..)) ∧ \valid_read(\result) ∧
       memcmp{Pre, Pre}(\result, \old(needle), strlen(\old(needle))) ≡ 0);
    assigns \result;
    assigns \result \from haystack, *(haystack + (0 ..)), *(needle + (0 ..));
 */
extern char *strstr(char const *haystack, char const *needle);

/*@ requires valid_string_src: valid_string_or_null(s);
    requires valid_string_delim: valid_read_string(delim);
    ensures
      \result ≡ \null ∨ \base_addr(\result) ≡ \base_addr(\old(s));
    assigns \result;
    assigns \result \from s, *(s + (0 ..)), *(delim + (0 ..));
 */
extern char *strtok(char *s, char const *delim);

/*@ requires valid_string_src: \valid(stringp) ∧ valid_string(*stringp);
    requires valid_string_delim: valid_read_string(delim);
    assigns *stringp, \result;
    assigns *stringp \from *(delim + (..)), *(*(stringp + (..)));
    assigns \result \from *(delim + (..)), *(*(stringp + (..)));
 */
extern char *strsep(char **stringp, char const *delim);

/*@ ensures valid_read_string(\result);
    assigns \result;
    assigns \result \from errnum;
 */
extern char *strerror(int errnum);

/*@ requires valid_string_src: valid_read_string(src);
    requires room_string: \valid(dest + (0 .. strlen(src)));
    ensures strcmp(\old(dest), \old(src)) ≡ 0;
    ensures \result ≡ \old(dest);
    assigns *(dest + (0 .. strlen{Old}(src))), \result;
    assigns *(dest + (0 .. strlen{Old}(src)))
      \from *(src + (0 .. strlen{Old}(src)));
    assigns \result \from dest;
 */
extern char *strcpy(char *dest, char const *src);

/*@ requires valid_string_src: valid_read_string(src);
    requires room_nstring: \valid(dest + (0 .. n - 1));
    ensures \result ≡ \old(dest);
    ensures \initialized(\old(dest) + (0 .. \old(n) - 1));
    assigns *(dest + (0 .. n - 1)), \result;
    assigns *(dest + (0 .. n - 1)) \from *(src + (0 .. n - 1));
    assigns \result \from dest;
    
    behavior complete:
      assumes strlen(src) < n;
      ensures strcmp(\old(dest), \old(src)) ≡ 0;
    
    behavior partial:
      assumes n ≤ strlen(src);
      ensures memcmp{Post, Post}(\old(dest), \old(src), \old(n)) ≡ 0;
 */
extern char *strncpy(char *dest, char const *src, size_t n);

/*@ requires valid_string_src: valid_read_string(src);
    requires valid_string_dst: valid_string(dest);
    requires room_string: \valid(dest + (0 .. strlen(dest) + strlen(src)));
    ensures strlen(\old(dest)) ≡ \old(strlen(dest) + strlen(src));
    ensures \result ≡ \old(dest);
    assigns *(dest +
              (strlen{Old}(dest) .. strlen{Old}(dest) + strlen{Old}(src))),
            \result;
    assigns
    *(dest + (strlen{Old}(dest) .. strlen{Old}(dest) + strlen{Old}(src)))
      \from *(src + (0 .. strlen{Old}(src)));
    assigns \result \from dest;
 */
extern char *strcat(char *dest, char const *src);

/*@ requires
      valid_string_src:
        valid_read_string(src) ∨ \valid_read(src + (0 .. n - 1));
    requires valid_string_dst: valid_string(dest);
    requires room_string: \valid(dest + (strlen(dest) .. strlen(dest) + n));
    ensures \result ≡ \old(dest);
    assigns *(dest + (strlen{Old}(dest) .. strlen{Old}(dest) + n)), \result;
    assigns *(dest + (strlen{Old}(dest) .. strlen{Old}(dest) + n))
      \from *(src + (0 .. n));
    assigns \result \from dest;
    
    behavior complete:
      assumes valid_read_string(src) ∧ strlen(src) ≤ n;
      ensures strlen(\old(dest)) ≡ \old(strlen(dest) + strlen(src));
      assigns *(dest +
                (strlen{Old}(dest) .. strlen{Old}(dest) + strlen{Old}(src))),
              \result;
      assigns
      *(dest + (strlen{Old}(dest) .. strlen{Old}(dest) + strlen{Old}(src)))
        \from *(src + (0 .. strlen{Old}(src)));
      assigns \result \from dest;
    
    behavior partial:
      assumes ¬(valid_read_string(src) ∧ strlen(src) ≤ n);
      ensures strlen(\old(dest)) ≡ \old(strlen(dest)) + \old(n);
      assigns *(dest + (strlen{Old}(dest) .. strlen{Old}(dest) + n)),
              \result;
      assigns *(dest + (strlen{Old}(dest) .. strlen{Old}(dest) + n))
        \from *(src + (0 .. strlen{Old}(src)));
      assigns \result \from dest;
 */
extern char *strncat(char *dest, char const *src, size_t n);

/*@ requires valid_dest: \valid(dest + (0 .. n - 1));
    requires valid_string_src: valid_read_string(src);
    assigns *(dest + (0 .. n - 1)), \result;
    assigns *(dest + (0 .. n - 1)) \from *(src + (0 ..)), n;
    assigns \result \from dest;
 */
extern size_t strxfrm(char *dest, char const *src, size_t n);

char *strdup(char const *str);

/*@ requires valid_string_src: valid_read_string(s);
    ensures
      \valid(\result + (0 .. minimum(strlen(\old(s)), \old(n)))) ∧
      valid_string(\result) ∧ strlen(\result) ≤ \old(n) ∧
      strncmp(\result, \old(s), \old(n)) ≡ 0;
    assigns \nothing;
 */
extern char *strndup(char const *s, size_t n);

/*@ requires \valid((char *)s + (0 .. n - 1));
    assigns *((char *)s + (0 .. n - 1));
    assigns *((char *)s + (0 .. n - 1)) \from \nothing;
 */
extern void bzero(void *s, size_t n);

/*@ assigns \result;
    assigns \result \from *(nptr + (..)); */
extern double atof(char const *nptr);

/*@ assigns \result;
    assigns \result \from *(nptr + (..)); */
extern int atoi(char const *nptr);

/*@ assigns \result;
    assigns \result \from *(nptr + (..)); */
extern long atol(char const *nptr);

/*@ assigns \result;
    assigns \result \from *(nptr + (..)); */
extern long long atoll(char const *nptr);

/*@ assigns \result, *endptr;
    assigns \result \from *(nptr + (0 ..));
    assigns *endptr \from nptr, *(nptr + (0 ..));
 */
extern double strtod(char const *nptr, char **endptr);

/*@ assigns \result, *endptr;
    assigns \result \from *(nptr + (0 ..));
    assigns *endptr \from nptr, *(nptr + (0 ..));
 */
extern float strtof(char const *nptr, char **endptr);

/*@ assigns \result, *endptr;
    assigns \result \from *(nptr + (0 ..));
    assigns *endptr \from nptr, *(nptr + (0 ..));
 */
extern long double strtold(char const *nptr, char **endptr);

/*@ assigns \result, *endptr;
    assigns \result
      \from (indirect: nptr), (indirect: *(nptr + (0 ..))), (indirect: base);
    assigns *endptr
      \from nptr, (indirect: *(nptr + (0 ..))), (indirect: endptr),
            (indirect: base);
    
    behavior null_endptr:
      assumes endptr ≡ \null;
      assigns \result;
      assigns \result
        \from (indirect: nptr), (indirect: *(nptr + (0 ..))),
              (indirect: base);
    
    behavior nonnull_endptr:
      assumes endptr ≢ \null;
      requires \valid(endptr);
      ensures \initialized(\old(endptr));
      ensures \subset(*\old(endptr), \old(nptr) + (0 ..));
      assigns \result, *endptr;
      assigns \result
        \from (indirect: nptr), (indirect: *(nptr + (0 ..))),
              (indirect: base);
      assigns *endptr
        \from nptr, (indirect: *(nptr + (0 ..))), (indirect: endptr),
              (indirect: base);
    
    complete behaviors nonnull_endptr, null_endptr;
    disjoint behaviors nonnull_endptr, null_endptr;
 */
extern long strtol(char const *nptr, char **endptr, int base);

/*@ assigns \result, *endptr;
    assigns \result \from *(nptr + (0 ..)), base;
    assigns *endptr \from nptr, *(nptr + (0 ..)), base;
 */
extern long long strtoll(char const *nptr, char **endptr, int base);

/*@ assigns \result, *endptr;
    assigns \result \from *(nptr + (0 ..)), base;
    assigns *endptr \from nptr, *(nptr + (0 ..)), base;
 */
extern unsigned long strtoul(char const *nptr, char **endptr, int base);

/*@ assigns \result, *endptr;
    assigns \result \from *(nptr + (0 ..)), base;
    assigns *endptr \from nptr, *(nptr + (0 ..)), base;
 */
extern unsigned long long strtoull(char const *nptr, char **endptr, int base);

/*@ ghost
  int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__)); */
unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ensures 0 ≤ \result ≤ __fc_rand_max;
    assigns \result, __fc_random_counter;
    assigns \result \from __fc_random_counter;
    assigns __fc_random_counter \from __fc_random_counter;
 */
extern int rand(void);

/*@ assigns __fc_random_counter;
    assigns __fc_random_counter \from seed; */
extern void srand(unsigned int seed);

/*@ requires nmemb * size ≤ 4294967295U; */
extern void *calloc(size_t nmemb, size_t size);

/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */

/*@
axiomatic dynamic_allocation {
  predicate is_allocable{L}(size_t n) 
    reads __fc_heap_status;
  
  }
 */
/*@ assigns __fc_heap_status, \result;
    assigns __fc_heap_status \from size, __fc_heap_status;
    assigns \result \from (indirect: size), (indirect: __fc_heap_status);
    allocates \result;
    
    behavior allocation:
      assumes is_allocable(size);
      ensures \fresh{Old, Here}(\result,\old(size));
      assigns __fc_heap_status, \result;
      assigns __fc_heap_status \from size, __fc_heap_status;
      assigns \result \from (indirect: size), (indirect: __fc_heap_status);
    
    behavior no_allocation:
      assumes ¬is_allocable(size);
      ensures \result ≡ \null;
      assigns \result;
      assigns \result \from \nothing;
      allocates \nothing;
    
    complete behaviors no_allocation, allocation;
    disjoint behaviors no_allocation, allocation;
 */
extern void *malloc(size_t size);

/*@ assigns __fc_heap_status;
    assigns __fc_heap_status \from __fc_heap_status;
    frees p;
    
    behavior deallocation:
      assumes p ≢ \null;
      requires freeable: \freeable(p);
      ensures \allocable(\old(p));
      assigns __fc_heap_status;
      assigns __fc_heap_status \from __fc_heap_status;
    
    behavior no_deallocation:
      assumes p ≡ \null;
      assigns \nothing;
      allocates \nothing;
    
    complete behaviors no_deallocation, deallocation;
    disjoint behaviors no_deallocation, deallocation;
 */
extern void free(void *p);

/*@ requires ptr ≡ \null ∨ \freeable(ptr);
    assigns __fc_heap_status, \result;
    assigns __fc_heap_status \from __fc_heap_status;
    assigns \result \from size, ptr, __fc_heap_status;
    frees ptr;
    allocates \result;
    
    behavior alloc:
      assumes is_allocable(size);
      ensures \fresh{Old, Here}(\result,\old(size));
      assigns \result;
      assigns \result \from size, __fc_heap_status;
      allocates \result;
    
    behavior dealloc:
      assumes ptr ≢ \null;
      assumes is_allocable(size);
      requires \freeable(ptr);
      ensures \allocable(\old(ptr));
      ensures \result ≡ \null ∨ \freeable(\result);
      frees ptr;
    
    behavior fail:
      assumes ¬is_allocable(size);
      ensures \result ≡ \null;
      assigns \result;
      assigns \result \from size, __fc_heap_status;
      allocates \nothing;
    
    complete behaviors fail, dealloc, alloc;
    disjoint behaviors alloc, fail;
    disjoint behaviors dealloc, fail;
 */
extern void *realloc(void *ptr, size_t size);

/*@ ensures \false;
    assigns \nothing; */
extern void abort(void);

/*@ assigns \result;
    assigns \result \from \nothing; */
extern int atexit(void (*func)(void));

/*@ assigns \result;
    assigns \result \from \nothing; */
extern int at_quick_exit(void (*func)(void));

/*@ ensures \false;
    assigns \nothing; */
extern  __attribute__((__noreturn__)) void exit(int status);

/*@ ensures \false;
    assigns \nothing; */
extern  __attribute__((__noreturn__)) void _Exit(int status);

/*@ ensures \result ≡ \null ∨ \valid(\result);
    assigns \result;
    assigns \result \from name;
 */
extern char *getenv(char const *name);

/*@ ensures \false;
    assigns \nothing; */
extern  __attribute__((__noreturn__)) void quick_exit(int status);

/*@ assigns \result;
    assigns \result \from *(string + (..)); */
extern int system(char const *string);

/*@ assigns *((char *)\result + (..));
    assigns *((char *)\result + (..))
      \from *((char *)key + (..)), *((char *)base + (..)), nmemb, size,
            *compar;
 */
extern void *bsearch(void const *key, void const *base, size_t nmemb,
                     size_t size, int (*compar)(void const *, void const *));

/*@ assigns *((char *)base + (..));
    assigns *((char *)base + (..))
      \from *((char *)base + (..)), nmemb, size, *compar;
 */
extern void qsort(void *base, size_t nmemb, size_t size,
                  int (*compar)(void const *, void const *));

/*@ requires abs_representable: (int)(-j) ≡ -j;
    assigns \result;
    assigns \result \from j;
 */
extern int abs(int j);

/*@ requires abs_representable: (long)(-j) ≡ -j;
    assigns \result;
    assigns \result \from j;
 */
extern long labs(long j);

/*@ requires abs_representable: (long long)(-j) ≡ -j;
    assigns \result;
    assigns \result \from j;
 */
extern long long llabs(long long j);

/*@ assigns \result;
    assigns \result \from numer, denom; */
extern div_t div(int numer, int denom);

/*@ assigns \result;
    assigns \result \from numer, denom; */
extern ldiv_t ldiv(long numer, long denom);

/*@ assigns \result;
    assigns \result \from numer, denom; */
extern lldiv_t lldiv(long long numer, long long denom);

/*@ assigns \result;
    assigns \result \from *(s + (0 ..)), n; */
extern int mblen(char const *s, size_t n);

/*@ assigns \result, *(pwc + (0 .. n - 1));
    assigns \result \from *(s + (0 .. n - 1)), n;
    assigns *(pwc + (0 .. n - 1)) \from *(s + (0 .. n - 1)), n;
 */
extern int mbtowc(wchar_t *pwc, char const *s, size_t n);

/*@ assigns \result, *(s + (0 ..));
    assigns \result \from wc;
    assigns *(s + (0 ..)) \from wc;
 */
extern int wctomb(char *s, wchar_t wc);

/*@ assigns \result, *(pwcs + (0 .. n - 1));
    assigns \result \from *(s + (0 .. n - 1)), n;
    assigns *(pwcs + (0 .. n - 1)) \from *(s + (0 .. n - 1)), n;
 */
extern size_t mbstowcs(wchar_t *pwcs, char const *s, size_t n);

/*@ assigns \result, *(s + (0 .. n - 1));
    assigns \result \from *(pwcs + (0 .. n - 1)), n;
    assigns *(s + (0 .. n - 1)) \from *(pwcs + (0 .. n - 1)), n;
 */
extern size_t wcstombs(char *s, wchar_t const *pwcs, size_t n);

/*@ requires valid_string_src: valid_read_string(str);
    ensures
      \valid(\result + (0 .. strlen(\old(str)))) ∧
      strcmp(\result, \old(str)) ≡ 0;
    assigns \nothing;
 */
char *strdup(char const *str)
{
  char *__retres;
  if (str != (char const *)0) {
    register char *copy;
    char *tmp_0;
    size_t tmp;
    tmp = strlen(str);
    tmp_0 = (char *)malloc(tmp + (size_t)1);
    copy = tmp_0;
    if (copy != (char *)0) {
      char *tmp_1;
      tmp_1 = strcpy(copy,str);
      __retres = tmp_1;
      goto return_label;
    }
  }
  __retres = (char *)0;
  return_label: return __retres;
}