[kernel] Parsing share/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing tests/syntax/gnu-asm-aesni.c (with preprocessing)
tests/syntax/gnu-asm-aesni.c:85:[kernel] warning: Clobber list contain "memory" argument. Assuming no side-effect beyond those mentioned in output operands.
/* Generated by Frama-C */
typedef unsigned int size_t;
typedef int wchar_t;
typedef unsigned short byte;
union __anonunion_PROPERLY_ALIGNED_TYPE_1 {
   int a ;
   short b ;
   char c[1] ;
   long d ;
   float f ;
   double g ;
};
typedef union __anonunion_PROPERLY_ALIGNED_TYPE_1 PROPERLY_ALIGNED_TYPE;
union __anonunion_u1_3 {
   PROPERLY_ALIGNED_TYPE dummy ;
   byte keyschedule[14 + 1][4][4] ;
};
union __anonunion_u2_4 {
   PROPERLY_ALIGNED_TYPE dummy ;
   byte keyschedule[14 + 1][4][4] ;
};
struct __anonstruct_RIJNDAEL_context_2 {
   union __anonunion_u1_3 u1 ;
   union __anonunion_u2_4 u2 ;
   int rounds ;
   unsigned int decryption_prepared : 1 ;
   unsigned int use_aesni : 1 ;
};
typedef struct __anonstruct_RIJNDAEL_context_2 RIJNDAEL_context;
extern int volatile Frama_C_entropy_source __attribute__((__unused__,
                                                          __FRAMA_C_MODEL__));

/*@ requires \valid(p + (0 .. l - 1));
    ensures \initialized(\old(p) + (0 .. \old(l) - 1));
    assigns *(p + (0 .. l - 1)), Frama_C_entropy_source;
    assigns *(p + (0 .. l - 1)) \from Frama_C_entropy_source;
    assigns Frama_C_entropy_source \from Frama_C_entropy_source;
 */
extern void Frama_C_make_unknown(char *p, size_t l);

/*@ ensures \result ≡ \old(a) ∨ \result ≡ \old(b);
    assigns \result, Frama_C_entropy_source;
    assigns \result \from a, b, Frama_C_entropy_source;
    assigns Frama_C_entropy_source \from Frama_C_entropy_source;
 */
extern int Frama_C_nondet(int a, int b);

/*@ ensures \result ≡ \old(a) ∨ \result ≡ \old(b);
    assigns \result, Frama_C_entropy_source;
    assigns \result \from a, b, Frama_C_entropy_source;
    assigns Frama_C_entropy_source \from Frama_C_entropy_source;
 */
extern void *Frama_C_nondet_ptr(void *a, void *b);

/*@ requires min ≤ max;
    ensures \old(min) ≤ \result ≤ \old(max);
    assigns \result, Frama_C_entropy_source;
    assigns \result \from min, max, Frama_C_entropy_source;
    assigns Frama_C_entropy_source \from Frama_C_entropy_source;
 */
extern int Frama_C_interval(int min, int max);

/*@ requires min ≤ max;
    ensures \old(min) ≤ \result ≤ \old(max);
    assigns \result, Frama_C_entropy_source;
    assigns \result \from min, max, Frama_C_entropy_source;
    assigns Frama_C_entropy_source \from Frama_C_entropy_source;
 */
extern int Frama_C_interval_split(int min, int max);

/*@ requires min ≤ max;
    ensures \old(min) ≤ \result ≤ \old(max);
    assigns \result, Frama_C_entropy_source;
    assigns \result \from min, max, Frama_C_entropy_source;
    assigns Frama_C_entropy_source \from Frama_C_entropy_source;
 */
extern unsigned char Frama_C_unsigned_char_interval(unsigned char min,
                                                    unsigned char max);

/*@ requires min ≤ max;
    ensures \old(min) ≤ \result ≤ \old(max);
    assigns \result, Frama_C_entropy_source;
    assigns \result \from min, max, Frama_C_entropy_source;
    assigns Frama_C_entropy_source \from Frama_C_entropy_source;
 */
extern char Frama_C_char_interval(char min, char max);

/*@ requires min ≤ max;
    ensures \old(min) ≤ \result ≤ \old(max);
    assigns \result, Frama_C_entropy_source;
    assigns \result \from min, max, Frama_C_entropy_source;
    assigns Frama_C_entropy_source \from Frama_C_entropy_source;
 */
extern unsigned short Frama_C_unsigned_short_interval(unsigned short min,
                                                      unsigned short max);

/*@ requires min ≤ max;
    ensures \old(min) ≤ \result ≤ \old(max);
    assigns \result, Frama_C_entropy_source;
    assigns \result \from min, max, Frama_C_entropy_source;
    assigns Frama_C_entropy_source \from Frama_C_entropy_source;
 */
extern short Frama_C_short_interval(short min, short max);

/*@ requires min ≤ max;
    ensures \old(min) ≤ \result ≤ \old(max);
    assigns \result, Frama_C_entropy_source;
    assigns \result \from min, max, Frama_C_entropy_source;
    assigns Frama_C_entropy_source \from Frama_C_entropy_source;
 */
extern unsigned int Frama_C_unsigned_int_interval(unsigned int min,
                                                  unsigned int max);

/*@ requires min ≤ max;
    ensures \old(min) ≤ \result ≤ \old(max);
    assigns \result, Frama_C_entropy_source;
    assigns \result \from min, max, Frama_C_entropy_source;
    assigns Frama_C_entropy_source \from Frama_C_entropy_source;
 */
extern int Frama_C_int_interval(int min, int max);

/*@ requires min ≤ max;
    ensures \old(min) ≤ \result ≤ \old(max);
    assigns \result, Frama_C_entropy_source;
    assigns \result \from min, max, Frama_C_entropy_source;
    assigns Frama_C_entropy_source \from Frama_C_entropy_source;
 */
extern unsigned long Frama_C_unsigned_long_interval(unsigned long min,
                                                    unsigned long max);

/*@ requires min ≤ max;
    ensures \old(min) ≤ \result ≤ \old(max);
    assigns \result, Frama_C_entropy_source;
    assigns \result \from min, max, Frama_C_entropy_source;
    assigns Frama_C_entropy_source \from Frama_C_entropy_source;
 */
extern long Frama_C_long_interval(long min, long max);

/*@ requires min ≤ max;
    ensures \old(min) ≤ \result ≤ \old(max);
    assigns \result, Frama_C_entropy_source;
    assigns \result \from min, max, Frama_C_entropy_source;
    assigns Frama_C_entropy_source \from Frama_C_entropy_source;
 */
extern unsigned long long Frama_C_unsigned_long_long_interval(unsigned long long min,
                                                              unsigned long long max);

/*@ requires min ≤ max;
    ensures \old(min) ≤ \result ≤ \old(max);
    assigns \result, Frama_C_entropy_source;
    assigns \result \from min, max, Frama_C_entropy_source;
    assigns Frama_C_entropy_source \from Frama_C_entropy_source;
 */
extern long long Frama_C_long_long_interval(long long min, long long max);

/*@ requires \is_finite(min) ∧ \is_finite(max);
    requires min ≤ max;
    ensures \is_finite(\result) ∧ \old(min) ≤ \result ≤ \old(max);
    assigns \result, Frama_C_entropy_source;
    assigns \result \from min, max, Frama_C_entropy_source;
    assigns Frama_C_entropy_source \from Frama_C_entropy_source;
 */
extern float Frama_C_float_interval(float min, float max);

/*@ requires \is_finite(min) ∧ \is_finite(max);
    requires min ≤ max;
    ensures \is_finite(\result) ∧ \old(min) ≤ \result ≤ \old(max);
    assigns \result, Frama_C_entropy_source;
    assigns \result \from min, max, Frama_C_entropy_source;
    assigns Frama_C_entropy_source \from Frama_C_entropy_source;
 */
extern double Frama_C_double_interval(double min, double max);

/*@ 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 *Frama_C_memcpy(void *dest, void const *src, size_t n);

/*@ assigns *((char *)p + (0 .. s - 1)), \result;
    assigns *((char *)p + (0 .. s - 1)) \from c;
    assigns \result \from p;
 */
extern void *Frama_C_memset(void *p, int c, size_t s);

/*@ requires \false;
    assigns \nothing; */
extern  __attribute__((__noreturn__)) void Frama_C_abort(void);

/*@ assigns \result;
    assigns \result \from p; */
extern size_t Frama_C_offset(void const *p);

/*@
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);

/*@ requires valid_string_src: valid_read_string(s);
    ensures
      \valid(\result + (0 .. strlen(\old(s)))) ∧
      strcmp(\result, \old(s)) ≡ 0;
    assigns \nothing;
 */
extern char *strdup(char const *s);

/*@ 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);

__inline static void do_aesni_enc(RIJNDAEL_context const *ctx,
                                  unsigned char *b, unsigned char const *a)
{
  /*@ assigns *b;
      assigns *b \from *a, ctx->u1.keyschedule, ctx->rounds; */
  __asm__ volatile (
    "movdqu %[src], %%xmm0\n\t"
    "movdqa (%[key]), %%xmm1\n\t"
    "pxor   %%xmm1, %%xmm0\n\t"
    "movdqa 0x10(%[key]), %%xmm1\n\t"
    ".byte 0x66, 0x0f, 0x38, 0xdc, 0xc1\n\t"
    "movdqa 0x20(%[key]), %%xmm1\n\t"
    ".byte 0x66, 0x0f, 0x38, 0xdc, 0xc1\n\t"
    "movdqa 0x30(%[key]), %%xmm1\n\t"
    ".byte 0x66, 0x0f, 0x38, 0xdc, 0xc1\n\t"
    "movdqa 0x40(%[key]), %%xmm1\n\t"
    ".byte 0x66, 0x0f, 0x38, 0xdc, 0xc1\n\t"
    "movdqa 0x50(%[key]), %%xmm1\n\t"
    ".byte 0x66, 0x0f, 0x38, 0xdc, 0xc1\n\t"
    "movdqa 0x60(%[key]), %%xmm1\n\t"
    ".byte 0x66, 0x0f, 0x38, 0xdc, 0xc1\n\t"
    "movdqa 0x70(%[key]), %%xmm1\n\t"
    ".byte 0x66, 0x0f, 0x38, 0xdc, 0xc1\n\t"
    "movdqa 0x80(%[key]), %%xmm1\n\t"
    ".byte 0x66, 0x0f, 0x38, 0xdc, 0xc1\n\t"
    "movdqa 0x90(%[key]), %%xmm1\n\t"
    ".byte 0x66, 0x0f, 0x38, 0xdc, 0xc1\n\t"
    "movdqa 0xa0(%[key]), %%xmm1\n\t"
    "cmpl $10, %[rounds]\n\t"
    "jz .Lenclast%=\n\t"
    ".byte 0x66, 0x0f, 0x38, 0xdc, 0xc1\n\t"
    "movdqa 0xb0(%[key]), %%xmm1\n\t"
    ".byte 0x66, 0x0f, 0x38, 0xdc, 0xc1\n\t"
    "movdqa 0xc0(%[key]), %%xmm1\n\t"
    "cmpl $12, %[rounds]\n\t"
    "jz .Lenclast%=\n\t"
    ".byte 0x66, 0x0f, 0x38, 0xdc, 0xc1\n\t"
    "movdqa 0xd0(%[key]), %%xmm1\n\t"
    ".byte 0x66, 0x0f, 0x38, 0xdc, 0xc1\n\t"
    "movdqa 0xe0(%[key]), %%xmm1\n"
    ".Lenclast%=:\n\t"
    ".byte 0x66, 0x0f, 0x38, 0xdd, 0xc1\n\t"
    "movdqu %%xmm0, %[dst]\n"
    : [dst] "=m" (*b)
    : [src] "m" (*a), [key] "r" (ctx->u1.keyschedule),
      [rounds] "r" (ctx->rounds)
    : "cc", "memory"
    );
  return;
}

extern int ( /* missing proto */ Frama_C_dump_each)();

void encrypt_aesni(void)
{
  RIJNDAEL_context ctx;
  unsigned char b[64];
  unsigned char a_init[64];
  unsigned char a[64];
  unsigned char test;
  int i;
  int j;
  int k;
  a_init[0] = (unsigned char)0x85;
  a_init[1] = (unsigned char)0x50;
  a_init[2] = (unsigned char)0x43;
  a_init[3] = (unsigned char)0xda;
  a_init[4] = (unsigned char)0x06;
  a_init[5] = (unsigned char)0x99;
  a_init[6] = (unsigned char)0xd8;
  a_init[7] = (unsigned char)0x3b;
  a_init[8] = (unsigned char)0x65;
  a_init[9] = (unsigned char)0xf7;
  a_init[10] = (unsigned char)0x1d;
  a_init[11] = (unsigned char)0xf7;
  a_init[12] = (unsigned char)0x95;
  a_init[13] = (unsigned char)0xd4;
  a_init[14] = (unsigned char)0x34;
  a_init[15] = (unsigned char)0x5d;
  a_init[16] = (unsigned char)0x6e;
  a_init[17] = (unsigned char)0x21;
  a_init[18] = (unsigned char)0x01;
  a_init[19] = (unsigned char)0xba;
  a_init[20] = (unsigned char)0x2a;
  a_init[21] = (unsigned char)0xbd;
  a_init[22] = (unsigned char)0x7f;
  a_init[23] = (unsigned char)0xab;
  a_init[24] = (unsigned char)0xa7;
  a_init[25] = (unsigned char)0x6d;
  a_init[26] = (unsigned char)0xe7;
  a_init[27] = (unsigned char)0xcd;
  a_init[28] = (unsigned char)0x72;
  a_init[29] = (unsigned char)0xcf;
  a_init[30] = (unsigned char)0xce;
  a_init[31] = (unsigned char)0xa1;
  a_init[32] = (unsigned char)0xa7;
  a_init[33] = (unsigned char)0x4a;
  a_init[34] = (unsigned char)0xb8;
  a_init[35] = (unsigned char)0x12;
  a_init[36] = (unsigned char)0xef;
  a_init[37] = (unsigned char)0x2d;
  a_init[38] = (unsigned char)0x6b;
  a_init[39] = (unsigned char)0xd5;
  a_init[40] = (unsigned char)0xdc;
  a_init[41] = (unsigned char)0x09;
  a_init[42] = (unsigned char)0xb9;
  a_init[43] = (unsigned char)0xdd;
  a_init[44] = (unsigned char)0x09;
  a_init[45] = (unsigned char)0x27;
  a_init[46] = (unsigned char)0x7c;
  a_init[47] = (unsigned char)0x86;
  a_init[48] = (unsigned char)0x35;
  a_init[49] = (unsigned char)0x60;
  a_init[50] = (unsigned char)0x99;
  a_init[51] = (unsigned char)0xea;
  a_init[52] = (unsigned char)0x72;
  a_init[53] = (unsigned char)0xbb;
  a_init[54] = (unsigned char)0x93;
  a_init[55] = (unsigned char)0x9e;
  a_init[56] = (unsigned char)0x9e;
  a_init[57] = (unsigned char)0x16;
  a_init[58] = (unsigned char)0x7b;
  a_init[59] = (unsigned char)0xd4;
  a_init[60] = (unsigned char)0x8c;
  a_init[61] = (unsigned char)0x81;
  a_init[62] = (unsigned char)0x8a;
  a_init[63] = (unsigned char)0x53;
  memcpy((void *)(a),(void const *)(a_init),
         (unsigned int)64 * sizeof(unsigned char));
  i = 0;
  while (i < 14 + 1) {
    j = 0;
    while (j < 4) {
      k = 0;
      while (k < 4) {
        Frama_C_make_unknown((char *)(& ctx.u1.keyschedule[i][j][k]),
                             sizeof(byte));
        k ++;
      }
      j ++;
    }
    i ++;
  }
  ctx.rounds = 12;
  ctx.use_aesni = (unsigned int)1;
  do_aesni_enc((RIJNDAEL_context const *)(& ctx),b,
               (unsigned char const *)(a));
  test = (unsigned char)0x00U;
  i = 0;
  while (i < 64) {
    test = (unsigned char)((int)test ^ (int)b[i]);
    i ++;
  }
  Frama_C_dump_each();
  return;
}