gen_mainargs.c

/* Generated by Frama-C */
struct __anonstruct___mpz_struct_1 {
   int _mp_alloc ;
   int _mp_size ;
   unsigned long *_mp_d ;
};
typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
typedef unsigned int size_t;
typedef int wchar_t;
/*@ requires predicate ≢ 0;
    assigns \nothing; */
extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
                                                           char *kind,
                                                           char *fct,
                                                           char *pred_txt,
                                                           int line);

/*@
model __mpz_struct { ℤ n };
*/
int random_counter __attribute__((__unused__));
unsigned long const rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */

/*@
axiomatic
  dynamic_allocation {
  predicate is_allocable{L}(size_t n) 
    reads __fc_heap_status;
  
  }
 */
/*@ ghost extern int __e_acsl_init; */

/*@ assigns \nothing; */
extern  __attribute__((__FC_BUILTIN__)) void __init_args(int argc_ref,
                                                         char **argv_ref);

/*@ assigns \result;
    assigns \result \from *((char *)ptr+(0 .. size-1)); */
extern  __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
                                                            size_t size);

/*@ assigns \nothing; */
extern  __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);

/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
    ensures \result ≡ 1 ⇒ \valid((char *)\old(ptr)+(0 .. \old(size)-1));
    assigns \result;
    assigns \result \from *((char *)ptr+(0 .. size-1));
 */
extern  __attribute__((__FC_BUILTIN__)) int __valid(void *ptr, size_t size);

/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
    ensures
      \result ≡ 1 ⇒ \valid_read((char *)\old(ptr)+(0 .. \old(size)-1));
    assigns \result;
    assigns \result \from *((char *)ptr+(0 .. size-1));
 */
extern  __attribute__((__FC_BUILTIN__)) int __valid_read(void *ptr,
                                                         size_t size);

/*@ ensures \result ≡ \block_length(\old(ptr));
    assigns \result;
    assigns \result \from ptr;
 */
extern  __attribute__((__FC_BUILTIN__)) size_t __block_length(void *ptr);

/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
    ensures
      \result ≡ 1 ⇒ \initialized((char *)\old(ptr)+(0 .. \old(size)-1));
    assigns \result;
    assigns \result \from *((char *)ptr+(0 .. size-1));
 */
extern  __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
                                                          size_t size);

/*@ ghost extern int __e_acsl_internal_heap; */

/*@ assigns __e_acsl_internal_heap;
    assigns __e_acsl_internal_heap \from __e_acsl_internal_heap;
 */
extern  __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);

/*@ ghost extern size_t __memory_size; */

/*@
predicate diffSize{L1, L2}(ℤ i) =
  \at(__memory_size,L1)-\at(__memory_size,L2) ≡ i;
 */
/*@
axiomatic
  MemCmp {
  logic ℤ memcmp{L}(char *s1, char *s2, ℤ n)
    
    reads *(s1+(0 .. n-1)), *(s2+(0 .. n-1));
  
  axiom
  memcmp_zero{L}:
                 ∀ char *s1, char *s2;
                   (∀ ℤ n;
                      memcmp{L}(s1, s2, n) ≡ 0 ⇔
                      (∀ ℤ i; 0 ≤ i ∧ i < n ⇒ *(s1+i) ≡ *(s2+i)));
  
  }
 */
/*@
axiomatic
  MemChr {
  logic 𝔹 memchr{L}(char *s, ℤ c, ℤ n) ;
  
  axiom
  memchr_def{L}:
                ∀ char *s;
                  (∀ ℤ c;
                     (∀ ℤ n;
                        memchr{L}(s, c, n) ≡ \true ⇔
                        (∃ int i; (0 ≤ i ∧ i < n) ∧ *(s+i) ≡ c)));
  
  }
 */
/*@
axiomatic
  MemSet {
  logic 𝔹 memset{L}(char *s, ℤ c, ℤ n) ;
  
  axiom
  memset_def{L}:
                ∀ char *s;
                  (∀ ℤ c;
                     (∀ ℤ n;
                        memset{L}(s, c, n) ≡ \true ⇔
                        (∀ ℤ i; 0 ≤ i ∧ i < n ⇒ *(s+i) ≡ c)));
  
  }
 */
/*@
axiomatic
  StrLen {
  logic ℤ strlen{L}(char *s) ;
  
  axiom
  strlen_pos_or_null{L}:
                        ∀ char *s;
                          (∀ ℤ i;
                             (0 ≤ i ∧
                              (∀ ℤ j;
                                 0 ≤ j ∧ j < i ⇒ *(s+j) ≢ '\000'))
                             ∧ *(s+i) ≡ '\000' ⇒ strlen{L}(s) ≡ i);
  
  axiom
  strlen_neg{L}:
                ∀ char *s;
                  (∀ ℤ i; 0 ≤ i ⇒ *(s+i) ≢ '\000') ⇒
                  strlen{L}(s) < 0;
  
  axiom
  strlen_before_null{L}:
                        ∀ char *s;
                          (∀ ℤ i;
                             0 ≤ i ∧ i < strlen{L}(s) ⇒
                             *(s+i) ≢ '\000');
  
  axiom
  strlen_at_null{L}:
                    ∀ char *s;
                      0 ≤ strlen{L}(s) ⇒ *(s+strlen{L}(s)) ≡ '\000';
  
  axiom
  strlen_not_zero{L}:
                     ∀ char *s;
                       (∀ ℤ i;
                          (0 ≤ i ∧ i ≤ strlen{L}(s)) ∧
                          *(s+i) ≢ '\000' ⇒ i < strlen{L}(s));
  
  axiom
  strlen_zero{L}:
                 ∀ char *s;
                   (∀ ℤ i;
                      (0 ≤ i ∧ i ≤ strlen{L}(s)) ∧ *(s+i) ≡ '\000'
                      ⇒ i ≡ strlen{L}(s));
  
  axiom
  strlen_sup{L}:
                ∀ char *s;
                  (∀ ℤ i;
                     0 ≤ i ∧ *(s+i) ≡ '\000' ⇒
                     0 ≤ strlen{L}(s) ∧ strlen{L}(s) ≤ i);
  
  axiom
  strlen_shift{L}:
                  ∀ char *s;
                    (∀ ℤ i;
                       0 ≤ i ∧ i ≤ strlen{L}(s) ⇒
                       strlen{L}(s+i) ≡ strlen{L}(s)-i);
  
  axiom
  strlen_create{L}:
                   ∀ char *s;
                     (∀ ℤ i;
                        0 ≤ i ∧ *(s+i) ≡ '\000' ⇒
                        0 ≤ strlen{L}(s) ∧ strlen{L}(s) ≤ i);
  
  axiom
  strlen_create_shift{L}:
                         ∀ char *s;
                           (∀ ℤ i;
                              (∀ ℤ k;
                                 (0 ≤ k ∧ k ≤ i) ∧ *(s+i) ≡ '\000'
                                 ⇒
                                 0 ≤ strlen{L}(s+k) ∧
                                 strlen{L}(s+k) ≤ i-k));
  
  axiom
  memcmp_strlen_left{L}:
                        ∀ char *s1, char *s2;
                          (∀ ℤ n;
                             memcmp{L}(s1, s2, n) ≡ 0 ∧ strlen{L}(s1) < n
                             ⇒ strlen{L}(s1) ≡ strlen{L}(s2));
  
  axiom
  memcmp_strlen_right{L}:
                         ∀ char *s1, char *s2;
                           (∀ ℤ n;
                              memcmp{L}(s1, s2, n) ≡ 0 ∧
                              strlen{L}(s2) < n ⇒
                              strlen{L}(s1) ≡ strlen{L}(s2));
  
  axiom
  memcmp_strlen_shift_left{L}:
                              ∀ char *s1, char *s2;
                                (∀ ℤ k, ℤ n;
                                   (memcmp{L}(s1, s2+k, n) ≡ 0 ∧ 0 ≤ k)
                                   ∧ strlen{L}(s1) < n ⇒
                                   0 ≤ strlen{L}(s2) ∧
                                   strlen{L}(s2) ≤ k+strlen{L}(s1));
  
  axiom
  memcmp_strlen_shift_right{L}:
                               ∀ char *s1, char *s2;
                                 (∀ ℤ k, ℤ n;
                                    (memcmp{L}(s1+k, s2, n) ≡ 0 ∧ 0 ≤ k)
                                    ∧ strlen{L}(s2) < n ⇒
                                    0 ≤ strlen{L}(s1) ∧
                                    strlen{L}(s1) ≤ k+strlen{L}(s2));
  
  }
 */
/*@
axiomatic
  StrCmp {
  logic ℤ strcmp{L}(char *s1, char *s2) ;
  
  axiom
  strcmp_zero{L}:
                 ∀ char *s1, char *s2;
                   strcmp{L}(s1, s2) ≡ 0 ⇔
                   strlen{L}(s1) ≡ strlen{L}(s2) ∧
                   (∀ ℤ i;
                      0 ≤ i ∧ i ≤ strlen{L}(s1) ⇒ *(s1+i) ≡ *(s2+i));
  
  }
 */
/*@
axiomatic
  StrNCmp {
  logic ℤ strncmp{L}(char *s1, char *s2, ℤ n) ;
  
  axiom
  strncmp_zero{L}:
                  ∀ char *s1, char *s2;
                    (∀ ℤ n;
                       strncmp{L}(s1, s2, n) ≡ 0 ⇔
                       (strlen{L}(s1) < n ∧ strcmp{L}(s1, s2) ≡ 0) ∨
                       (∀ ℤ i; 0 ≤ i ∧ i < n ⇒ *(s1+i) ≡ *(s2+i)));
  
  }
 */
/*@
axiomatic
  StrChr {
  logic 𝔹 strchr{L}(char *s, ℤ c) ;
  
  axiom
  strchr_def{L}:
                ∀ char *s;
                  (∀ ℤ c;
                     strchr{L}(s, c) ≡ \true ⇔
                     (∃ ℤ i;
                        (0 ≤ i ∧ i ≤ strlen{L}(s)) ∧ *(s+i) ≡ c));
  
  }
 */
/*@
axiomatic
  WcsLen {
  logic ℤ wcslen{L}(wchar_t *s) ;
  
  axiom
  wcslen_pos_or_null{L}:
                        ∀ wchar_t *s;
                          (∀ ℤ i;
                             (0 ≤ i ∧
                              (∀ ℤ j; 0 ≤ j ∧ j < i ⇒ *(s+j) ≢ 0))
                             ∧ *(s+i) ≡ 0 ⇒ wcslen{L}(s) ≡ i);
  
  axiom
  wcslen_neg{L}:
                ∀ wchar_t *s;
                  (∀ ℤ i; 0 ≤ i ⇒ *(s+i) ≢ 0) ⇒ wcslen{L}(s) < 0;
  
  axiom
  wcslen_before_null{L}:
                        ∀ wchar_t *s;
                          (∀ int i;
                             0 ≤ i ∧ i < wcslen{L}(s) ⇒ *(s+i) ≢ 0);
  
  axiom
  wcslen_at_null{L}:
                    ∀ wchar_t *s;
                      0 ≤ wcslen{L}(s) ⇒ *(s+wcslen{L}(s)) ≡ 0;
  
  axiom
  wcslen_not_zero{L}:
                     ∀ wchar_t *s;
                       (∀ int i;
                          (0 ≤ i ∧ i ≤ wcslen{L}(s)) ∧ *(s+i) ≢ 0
                          ⇒ i < wcslen{L}(s));
  
  axiom
  wcslen_zero{L}:
                 ∀ wchar_t *s;
                   (∀ int i;
                      (0 ≤ i ∧ i ≤ wcslen{L}(s)) ∧ *(s+i) ≡ 0 ⇒
                      i ≡ wcslen{L}(s));
  
  axiom
  wcslen_sup{L}:
                ∀ wchar_t *s;
                  (∀ int i;
                     0 ≤ i ∧ *(s+i) ≡ 0 ⇒
                     0 ≤ wcslen{L}(s) ∧ wcslen{L}(s) ≤ i);
  
  axiom
  wcslen_shift{L}:
                  ∀ wchar_t *s;
                    (∀ int i;
                       0 ≤ i ∧ i ≤ wcslen{L}(s) ⇒
                       wcslen{L}(s+i) ≡ wcslen{L}(s)-i);
  
  axiom
  wcslen_create{L}:
                   ∀ wchar_t *s;
                     (∀ int i;
                        0 ≤ i ∧ *(s+i) ≡ 0 ⇒
                        0 ≤ wcslen{L}(s) ∧ wcslen{L}(s) ≤ i);
  
  axiom
  wcslen_create_shift{L}:
                         ∀ wchar_t *s;
                           (∀ int i;
                              (∀ int k;
                                 (0 ≤ k ∧ k ≤ i) ∧ *(s+i) ≡ 0 ⇒
                                 0 ≤ wcslen{L}(s+k) ∧
                                 wcslen{L}(s+k) ≤ i-k));
  
  }
 */
/*@
axiomatic
  WcsCmp {
  logic ℤ wcscmp{L}(wchar_t *s1, wchar_t *s2) ;
  
  axiom
  wcscmp_zero{L}:
                 ∀ wchar_t *s1, wchar_t *s2;
                   wcscmp{L}(s1, s2) ≡ 0 ⇔
                   wcslen{L}(s1) ≡ wcslen{L}(s2) ∧
                   (∀ ℤ i;
                      0 ≤ i ∧ i ≤ wcslen{L}(s1) ⇒ *(s1+i) ≡ *(s2+i));
  
  }
 */
/*@
axiomatic
  WcsNCmp {
  logic ℤ wcsncmp{L}(wchar_t *s1, wchar_t *s2, ℤ n) ;
  
  axiom
  wcsncmp_zero{L}:
                  ∀ wchar_t *s1, wchar_t *s2;
                    (∀ ℤ n;
                       wcsncmp{L}(s1, s2, n) ≡ 0 ⇔
                       (wcslen{L}(s1) < n ∧ wcscmp{L}(s1, s2) ≡ 0) ∨
                       (∀ ℤ i; 0 ≤ i ∧ 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{L}(s) ∧ \valid{L}(s+(0 .. strlen{L}(s)));
 */
/*@
predicate valid_string_or_null{L}(char *s) =
  s ≡ \null ∨ valid_string{L}(s);
 */
/*@
predicate valid_wstring{L}(wchar_t *s) =
  0 ≤ wcslen{L}(s) ∧ \valid{L}(s+(0 .. wcslen{L}(s)));
 */
/*@
predicate valid_wstring_or_null{L}(wchar_t *s) =
  s ≡ \null ∨ valid_wstring{L}(s);
 */
/*@ requires valid_string_src: valid_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_string(s);
    ensures \result ≡ strlen(\old(s));
    assigns \result;
    assigns \result \from *(s+(0 ..));
 */
size_t __e_acsl_strlen(char const *s)
{
  size_t __retres;
  __store_block((void *)(& s),8U);
  __retres = strlen(s);
  __delete_block((void *)(& s));
  return __retres;
}

int main(int argc, char **argv)
{
  int __retres;
  int i;
  __init_args(argc,argv);
  /*@ assert \valid(&argc); */
  {
    int __e_acsl_valid;
    __store_block((void *)(& argc),4U);
    __store_block((void *)(& argv),8U);
    __e_acsl_valid = __valid((void *)(& argc),(size_t)sizeof(int));
    e_acsl_assert(__e_acsl_valid,(char *)"Assertion",(char *)"main",
                  (char *)"\\valid(&argc)",12);
  }
  /*@ assert \valid(&argv); */
  {
    int __e_acsl_valid_2;
    __e_acsl_valid_2 = __valid((void *)(& argv),(size_t)sizeof(char **));
    e_acsl_assert(__e_acsl_valid_2,(char *)"Assertion",(char *)"main",
                  (char *)"\\valid(&argv)",13);
  }
  /*@ assert ∀ int k; 0 ≤ k ∧ k < argc ⇒ \valid(argv+k); */
  {
    int __e_acsl_forall;
    int __e_acsl_k;
    __e_acsl_forall = 1;
    __e_acsl_k = 0;
    while (1) {
      if (__e_acsl_k < argc) ; else break;
      {
        int __e_acsl_valid_3;
        __e_acsl_valid_3 = __valid((void *)(argv + __e_acsl_k),
                                   (size_t)sizeof(char *));
        if (__e_acsl_valid_3) ;
        else {
          __e_acsl_forall = 0;
          goto e_acsl_end_loop1;
        }
      }
      __e_acsl_k ++;
    }
    e_acsl_end_loop1: ;
    e_acsl_assert(__e_acsl_forall,(char *)"Assertion",(char *)"main",
                  (char *)"\\forall int k; 0 <= k && k < argc ==> \\valid(argv+k)",
                  14);
  }
  /*@ assert \block_length(argv) ≡ (argc+1)*sizeof(char *); */
  {
    unsigned long __e_acsl_block_length;
    __e_acsl_block_length = (unsigned long)__block_length((void *)argv);
    e_acsl_assert(__e_acsl_block_length == (unsigned long)(((long)argc + (long)1) * 8L),
                  (char *)"Assertion",(char *)"main",
                  (char *)"\\block_length(argv) == (argc+1)*sizeof(char *)",
                  15);
  }
  /*@ assert *(argv+argc) ≡ \null; */
  {
    int __e_acsl_valid_read;
    __e_acsl_valid_read = __valid_read((void *)(argv + argc),
                                       (size_t)sizeof(char *));
    e_acsl_assert(__e_acsl_valid_read,(char *)"RTE",(char *)"main",
                  (char *)"mem_access: \\valid_read(argv+argc)",17);
    e_acsl_assert(*(argv + argc) == (void *)0,(char *)"Assertion",
                  (char *)"main",(char *)"*(argv+argc) == \\null",17);
  }
  /*@ assert ¬\valid(*(argv+argc)); */
  {
    int __e_acsl_initialized;
    int __e_acsl_and;
    __e_acsl_initialized = __initialized((void *)(argv + argc),
                                         (size_t)sizeof(char *));
    if (__e_acsl_initialized) {
      int __e_acsl_valid_read_2;
      int __e_acsl_valid_4;
      __e_acsl_valid_read_2 = __valid_read((void *)(argv + argc),
                                           (size_t)sizeof(char *));
      e_acsl_assert(__e_acsl_valid_read_2,(char *)"RTE",(char *)"main",
                    (char *)"mem_access: \\valid_read(argv+argc)",18);
      __e_acsl_valid_4 = __valid((void *)*(argv + argc),(size_t)sizeof(char));
      __e_acsl_and = __e_acsl_valid_4;
    }
    else __e_acsl_and = 0;
    e_acsl_assert(! __e_acsl_and,(char *)"Assertion",(char *)"main",
                  (char *)"!\\valid(*(argv+argc))",18);
  }
  i = 0;
  while (i < argc) {
    {
      int len;
      size_t tmp;
      tmp = __e_acsl_strlen((char const *)*(argv + i));
      len = (int)tmp;
      /*@ assert \valid(*(argv+i)); */
      {
        int __e_acsl_initialized_2;
        int __e_acsl_and_2;
        __e_acsl_initialized_2 = __initialized((void *)(argv + i),
                                               (size_t)sizeof(char *));
        if (__e_acsl_initialized_2) {
          int __e_acsl_valid_read_3;
          int __e_acsl_valid_5;
          __e_acsl_valid_read_3 = __valid_read((void *)(argv + i),
                                               (size_t)sizeof(char *));
          e_acsl_assert(__e_acsl_valid_read_3,(char *)"RTE",(char *)"main",
                        (char *)"mem_access: \\valid_read(argv+i)",21);
          __e_acsl_valid_5 = __valid((void *)*(argv + i),
                                     (size_t)sizeof(char));
          __e_acsl_and_2 = __e_acsl_valid_5;
        }
        else __e_acsl_and_2 = 0;
        e_acsl_assert(__e_acsl_and_2,(char *)"Assertion",(char *)"main",
                      (char *)"\\valid(*(argv+i))",21);
      }
      /*@ assert ∀ int k; 0 ≤ k ∧ k ≤ len ⇒ \valid(*(argv+i)+k); */
      {
        int __e_acsl_forall_2;
        long __e_acsl_k_2;
        __e_acsl_forall_2 = 1;
        __e_acsl_k_2 = (long)0;
        while (1) {
          if (__e_acsl_k_2 <= (long)len) ; else break;
          {
            int __e_acsl_valid_read_4;
            int __e_acsl_valid_6;
            __e_acsl_valid_read_4 = __valid_read((void *)(argv + i),
                                                 (size_t)sizeof(char *));
            e_acsl_assert(__e_acsl_valid_read_4,(char *)"RTE",(char *)"main",
                          (char *)"mem_access: \\valid_read(argv+i)",22);
            __e_acsl_valid_6 = __valid((void *)(*(argv + i) + __e_acsl_k_2),
                                       (size_t)sizeof(char));
            if (__e_acsl_valid_6) ;
            else {
              __e_acsl_forall_2 = 0;
              goto e_acsl_end_loop2;
            }
          }
          __e_acsl_k_2 ++;
        }
        e_acsl_end_loop2: ;
        e_acsl_assert(__e_acsl_forall_2,(char *)"Assertion",(char *)"main",
                      (char *)"\\forall int k; 0 <= k && k <= len ==> \\valid(*(argv+i)+k)",
                      22);
      }
    }
    i ++;
  }
  __retres = 0;
  __delete_block((void *)(& argc));
  __delete_block((void *)(& argv));
  __e_acsl_memory_clean();
  return __retres;
}