result.res.oracle

tests/e-acsl-runtime/result.i:6:[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
        Y ∈ {1}
[value] computing for function f <- main.
        Called from PROJECT_FILE.i:252.
[value] computing for function __gmpz_init_set_si <- f <- main.
        Called from PROJECT_FILE.i:207.
PROJECT_FILE.i:75:[value] Function __gmpz_init_set_si: postcondition got status valid.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init <- f <- main.
        Called from PROJECT_FILE.i:208.
PROJECT_FILE.i:63:[value] Function __gmpz_init: postcondition got status valid.
[value] Done for function __gmpz_init
[value] computing for function __gmpz_sub <- f <- main.
        Called from PROJECT_FILE.i:209.
PROJECT_FILE.i:112:[value] Function __gmpz_sub: precondition got status valid.
PROJECT_FILE.i:113:[value] Function __gmpz_sub: precondition got status valid.
PROJECT_FILE.i:114:[value] Function __gmpz_sub: precondition got status valid.
[value] Done for function __gmpz_sub
[value] computing for function __gmpz_get_si <- f <- main.
        Called from PROJECT_FILE.i:210.
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 <- f <- main.
        Called from PROJECT_FILE.i:212.
[value] computing for function printf <- e_acsl_fail <- f <- main.
        Called from PROJECT_FILE.i:193.
[value] Done for function printf
[value] computing for function exit <- e_acsl_fail <- f <- 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 <- f <- main.
        Called from PROJECT_FILE.i:214.
PROJECT_FILE.i:85:[value] Function __gmpz_clear: precondition got status valid.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- f <- main.
        Called from PROJECT_FILE.i:215.
[value] Done for function __gmpz_clear
PROJECT_FILE.i:195:[value] Function f: postcondition got status valid.
[value] Recording results for f
[value] Done for function f
[value] computing for function g <- main.
        Called from PROJECT_FILE.i:253.
PROJECT_FILE.i:222:[value] Function g: postcondition got status valid.
[value] Recording results for g
[value] Done for function g
[value] computing for function h <- main.
        Called from PROJECT_FILE.i:254.
[value] computing for function __gmpz_init_set_si <- h <- main.
        Called from PROJECT_FILE.i:238.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_init_set_si <- h <- main.
        Called from PROJECT_FILE.i:239.
[value] Done for function __gmpz_init_set_si
[value] computing for function __gmpz_cmp <- h <- main.
        Called from PROJECT_FILE.i:240.
PROJECT_FILE.i:91:[value] Function __gmpz_cmp: precondition got status valid.
PROJECT_FILE.i:92:[value] Function __gmpz_cmp: precondition got status valid.
[value] Done for function __gmpz_cmp
[value] computing for function e_acsl_fail <- h <- main.
        Called from PROJECT_FILE.i:241.
[value] computing for function printf <- e_acsl_fail <- h <- main.
        Called from PROJECT_FILE.i:193.
[value] Done for function printf
[value] computing for function exit <- e_acsl_fail <- h <- 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 <- h <- main.
        Called from PROJECT_FILE.i:242.
[value] Done for function __gmpz_clear
[value] computing for function __gmpz_clear <- h <- main.
        Called from PROJECT_FILE.i:243.
[value] Done for function __gmpz_clear
PROJECT_FILE.i:229:[value] Function h: postcondition got status valid.
[value] Recording results for h
[value] Done for function h
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
[value] Values at end of function g:
[value] Values at end of function e_acsl_fail:
          NON TERMINATING FUNCTION
[value] Values at end of function f:
          x ∈ {0}
          e_acsl_1 ∈ {1}
          e_acsl_3 ∈ {1}
[value] Values at end of function h:
          __retres ∈ {0}
[value] Values at end of function main:
          __retres ∈ {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(x));
    assigns *x;  */
extern void __gmpz_init(__mpz_struct * /*[1]*/ x);
/*@ ensures \valid(\old(z));
    assigns *z;
    assigns *z \from n;  */
extern void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z, long n);
/*@ requires \valid(x);
    assigns *x;  */
extern void __gmpz_clear(__mpz_struct * /*[1]*/ x);
/*@ requires \valid(z1);
    requires \valid(z2);
    assigns \nothing;  */
extern int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
                      __mpz_struct const * /*[1]*/ z2);
/*@ requires \valid(z1);
    requires \valid(z2);
    requires \valid(z3);
    assigns *z1; 
*/
extern void __gmpz_sub(__mpz_struct * /*[1]*/ z1,
                       __mpz_struct const * /*[1]*/ z2,
                       __mpz_struct const * /*[1]*/ z3);
/*@ requires \valid(z);
    assigns \nothing;  */
extern long __gmpz_get_si(__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;
}

/*@ ensures \result ≡ (int)(\old(x)-\old(x));  */
int f(int x)
{
  int e_acsl_1;
  int e_acsl_3;
  e_acsl_3 = x;
  e_acsl_1 = x;
  x = 0;
  {
    mpz_t e_acsl_2;
    mpz_t e_acsl_4;
    int e_acsl_5;
    __gmpz_init_set_si((__mpz_struct *)(e_acsl_2),(long)e_acsl_1);
    __gmpz_init((__mpz_struct *)(e_acsl_4));
    __gmpz_sub((__mpz_struct *)(e_acsl_4),(__mpz_struct const *)(e_acsl_2),
               (__mpz_struct const *)(e_acsl_2));
    e_acsl_5 = (int)__gmpz_get_si((__mpz_struct const *)(e_acsl_4));
    if (! (x == e_acsl_5)) {
      e_acsl_fail((char *)"(\\result == (int)(\\old(x)-\\old(x)))");
    }
    __gmpz_clear((__mpz_struct *)(e_acsl_2));
    __gmpz_clear((__mpz_struct *)(e_acsl_4));
    return (x);
  }
  
}

int Y = 1;
/*@ ensures \result ≡ Y;  */
int g(int x)
{
  if (! (x == Y)) { e_acsl_fail((char *)"(\\result == Y)"); }
  return (x);
}

/*@ ensures \result ≡ 0;  */
int h(void)
{
  int __retres;
  __retres = 0;
  {
    mpz_t e_acsl_1;
    mpz_t e_acsl_2;
    int e_acsl_3;
    __gmpz_init_set_si((__mpz_struct *)(e_acsl_1),(long)__retres);
    __gmpz_init_set_si((__mpz_struct *)(e_acsl_2),(long)0);
    e_acsl_3 = __gmpz_cmp((__mpz_struct const *)(e_acsl_1),
                          (__mpz_struct const *)(e_acsl_2));
    if (! (e_acsl_3 == 0)) { e_acsl_fail((char *)"(\\result == 0)"); }
    __gmpz_clear((__mpz_struct *)(e_acsl_1));
    __gmpz_clear((__mpz_struct *)(e_acsl_2));
    return (__retres);
  }
  
}

int main(void)
{
  int __retres;
  f(1);
  g(Y);
  h();
  __retres = 0;
  return (__retres);
}