cast.res.oracle

tests/e-acsl-runtime/cast.i:17:[e-acsl] warning: missing guard for ensuring that the given integer is C-representable
tests/e-acsl-runtime/cast.i:18:[e-acsl] warning: missing guard for ensuring that the given integer is C-representable
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
PROJECT_FILE.i:202:[value] Assertion got status valid.
[value] computing for function __gmpz_init_set_str <- main.
        Called from PROJECT_FILE.i:206.
PROJECT_FILE.i:79:[value] Function __gmpz_init_set_str: postcondition got status valid.
[value] Done for function __gmpz_init_set_str
[value] computing for function __gmpz_get_si <- main.
        Called from PROJECT_FILE.i:207.
PROJECT_FILE.i:138:[value] Function __gmpz_get_si: precondition got status valid.
[value] Done for function __gmpz_get_si
[value] computing for function e_acsl_fail <- main.
        Called from PROJECT_FILE.i:208.
[value] computing for function printf <- e_acsl_fail <- main.
        Called from PROJECT_FILE.i:193.
[value] Done for function printf
[value] computing for function exit <- e_acsl_fail <- main.
        Called from PROJECT_FILE.i:193.
PROJECT_FILE.i:183:[value] Function exit: postcondition got status invalid.
[value] Done for function exit
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
[value] computing for function __gmpz_clear <- main.
        Called from PROJECT_FILE.i:209.
PROJECT_FILE.i:85:[value] Function __gmpz_clear: precondition got status valid.
[value] Done for function __gmpz_clear
PROJECT_FILE.i:213:[value] Assertion got status valid.
[value] computing for function __gmpz_init_set_str <- main.
        Called from PROJECT_FILE.i:217.
[value] Done for function __gmpz_init_set_str
[value] computing for function __gmpz_get_ui <- main.
        Called from PROJECT_FILE.i:218.
PROJECT_FILE.i:142:[value] Function __gmpz_get_ui: precondition got status valid.
[value] Done for function __gmpz_get_ui
[value] computing for function e_acsl_fail <- main.
        Called from PROJECT_FILE.i:220.
[value] computing for function printf <- e_acsl_fail <- main.
        Called from PROJECT_FILE.i:193.
[value] Done for function printf
[value] computing for function exit <- e_acsl_fail <- main.
        Called from PROJECT_FILE.i:193.
[value] Done for function exit
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
[value] computing for function __gmpz_clear <- main.
        Called from PROJECT_FILE.i:222.
[value] Done for function __gmpz_clear
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
[value] Values at end of function e_acsl_fail:
          NON TERMINATING FUNCTION
[value] Values at end of function main:
          __retres ∈ {0}
          x ∈ {0}
          y ∈ {0}
/* 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 mpz_t[1];
/*@ ensures \valid(\old(z));
    assigns *z;  */
extern int __gmpz_init_set_str(__mpz_struct * /*[1]*/ z, char const *str,
                               int base);
/*@ requires \valid(x);
    assigns *x;  */
extern void __gmpz_clear(__mpz_struct * /*[1]*/ x);
/*@ requires \valid(z);
    assigns \nothing;  */
extern long __gmpz_get_si(__mpz_struct const * /*[1]*/ z);
/*@ requires \valid(z);
    assigns \nothing;  */
extern unsigned long __gmpz_get_ui(__mpz_struct const * /*[1]*/ z);
/*@ terminates \false;
    ensures \false;
    assigns \nothing;  */
extern void exit(int status);
/*@ assigns \nothing;  */
extern int printf(char const * , ...);
void e_acsl_fail(char *msg)
{
  printf("%s\n",msg);
  exit(1);
  return;
}

int main(void)
{
  int __retres;
  long x;
  int y;
  x = (long)0;
  y = 0;
  /*@ assert y ≢ (int)0xfffffffffffffff; */ ;
  {
    mpz_t e_acsl_1;
    int e_acsl_2;
    __gmpz_init_set_str((__mpz_struct *)(e_acsl_1),"1152921504606846975",10);
    e_acsl_2 = (int)__gmpz_get_si((__mpz_struct const *)(e_acsl_1));
    if (! (y != e_acsl_2)) {
      e_acsl_fail((char *)"(y != (int)0xfffffffffffffff)");
    }
    __gmpz_clear((__mpz_struct *)(e_acsl_1));
  }
  
  /*@ assert (unsigned int)y ≢ (unsigned int)0xfffffffffffffff; */ ;
  {
    mpz_t e_acsl_3;
    unsigned int e_acsl_4;
    __gmpz_init_set_str((__mpz_struct *)(e_acsl_3),"1152921504606846975",10);
    e_acsl_4 = (unsigned int)__gmpz_get_ui((__mpz_struct const *)(e_acsl_3));
    if (! ((unsigned int)y != e_acsl_4)) {
      e_acsl_fail((char *)"((unsigned int)y != (unsigned int)0xfffffffffffffff)");
    }
    __gmpz_clear((__mpz_struct *)(e_acsl_3));
  }
  
  __retres = 0;
  return (__retres);
}