at.res.oracle

tests/e-acsl-runtime/at.i:32:[e-acsl] warning: missing guard for ensuring that q is a valid memory access
tests/e-acsl-runtime/at.i:32:[e-acsl] warning: missing guard for ensuring that p+\at(*q,L1) is a valid pointer
tests/e-acsl-runtime/at.i:32:[e-acsl] warning: missing guard for ensuring that p+\at(*q,L1) is a valid memory access
tests/e-acsl-runtime/at.i:34:[e-acsl] warning: missing guard for ensuring that q is a valid memory access
tests/e-acsl-runtime/at.i:34:[e-acsl] warning: missing guard for ensuring that p+\at(*q,L1) is a valid pointer
tests/e-acsl-runtime/at.i:34:[e-acsl] warning: missing guard for ensuring that p+\at(*q,L1) is a valid memory access
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
        A ∈ {0}
PROJECT_FILE.i:310:[value] Assertion got status valid.
[value] computing for function e_acsl_assert <- main.
        Called from PROJECT_FILE.i:311.
PROJECT_FILE.i:221:[value] Function e_acsl_assert: precondition got status valid.
[value] Recording results for e_acsl_assert
[value] Done for function e_acsl_assert
[value] computing for function f <- main.
        Called from PROJECT_FILE.i:315.
PROJECT_FILE.i:247:[value] Assertion got status valid.
[value] computing for function e_acsl_assert <- f <- main.
        Called from PROJECT_FILE.i:248.
[value] Recording results for e_acsl_assert
[value] Done for function e_acsl_assert
PROJECT_FILE.i:250:[value] Assertion got status unknown.
[value] computing for function e_acsl_assert <- f <- main.
        Called from PROJECT_FILE.i:251.
[value] Recording results for e_acsl_assert
[value] Done for function e_acsl_assert
PROJECT_FILE.i:253:[value] Assertion got status valid.
[value] computing for function e_acsl_assert <- f <- main.
        Called from PROJECT_FILE.i:255.
[value] Recording results for e_acsl_assert
[value] Done for function e_acsl_assert
PROJECT_FILE.i:257:[value] Assertion got status unknown.
[value] computing for function e_acsl_assert <- f <- main.
        Called from PROJECT_FILE.i:258.
[value] Recording results for e_acsl_assert
[value] Done for function e_acsl_assert
[value] computing for function e_acsl_assert <- f <- main.
        Called from PROJECT_FILE.i:262.
[value] Recording results for e_acsl_assert
[value] Done for function e_acsl_assert
PROJECT_FILE.i:231:[value] Function f: postcondition got status valid.
[value] Recording results for f
[value] Done for function f
PROJECT_FILE.i:316:[value] Assertion got status unknown.
[value] computing for function e_acsl_assert <- main.
        Called from PROJECT_FILE.i:317.
[value] Recording results for e_acsl_assert
[value] Done for function e_acsl_assert
PROJECT_FILE.i:319:[value] Assertion got status unknown.
[value] computing for function e_acsl_assert <- main.
        Called from PROJECT_FILE.i:320.
[value] Recording results for e_acsl_assert
[value] Done for function e_acsl_assert
PROJECT_FILE.i:323:[value] Assertion got status unknown.
[value] computing for function e_acsl_assert <- main.
        Called from PROJECT_FILE.i:324.
[value] Recording results for e_acsl_assert
[value] Done for function e_acsl_assert
[value] computing for function g <- main.
        Called from PROJECT_FILE.i:327.
PROJECT_FILE.i:284:[value] Assertion got status unknown.
[value] computing for function e_acsl_assert <- g <- main.
        Called from PROJECT_FILE.i:285.
[value] Recording results for e_acsl_assert
[value] Done for function e_acsl_assert
PROJECT_FILE.i:289:[value] Assertion got status unknown.
[value] computing for function e_acsl_assert <- g <- main.
        Called from PROJECT_FILE.i:291.
[value] Recording results for e_acsl_assert
[value] Done for function e_acsl_assert
[value] Recording results for g
[value] Done for function g
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
[value] Values at end of function e_acsl_assert:
[value] Values at end of function f:
          A ∈ {3}
          __e_acsl ∈ {0}
          __e_acsl_2 ∈ {1}
          __e_acsl_3 ∈ {2}
          __e_acsl_4 ∈ {0}
          __e_acsl_5 ∈ {0}
          __e_acsl_6 ∈ {3}
[value] Values at end of function g:
          A ∈ {4}
          __e_acsl ∈ {0}
          __e_acsl_2 ∈ {2}
          __e_acsl_3 ∈ {0}
          __e_acsl_4 ∈ {2}
          x ∈ {1}
          t[0] ∈ {2}
           [1] ∈ {3}
[value] Values at end of function main:
          A ∈ {4}
          __retres ∈ {0}
          x ∈ {1}
          t[0] ∈ {2}
           [1] ∈ {3}
          __e_acsl ∈ {0}
          __e_acsl_2 ∈ {1}
          __e_acsl_3 ∈ {0}
/* Generated by Frama-C */
/*@ terminates \false;
    ensures \false;
    assigns \nothing;  */
extern void exit(int status);
/*@ assigns \nothing;  */
extern int printf(char const * , ...);
/*@ requires predicate ≢ 0;  */
void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
{
  if (! predicate) {
    printf("%s failed at line %d.\nThe failing predicate is:\n%s.\n",kind,
           line,pred_txt);
    exit(1);
  }
  return;
}

int A = 0;
/*@ ensures \at(A,Post) ≡ 3;  */
void f(void)
{
  int __e_acsl;
  int __e_acsl_2;
  int __e_acsl_3;
  int __e_acsl_4;
  int __e_acsl_5;
  int __e_acsl_6;
  __e_acsl_4 = A;
  __e_acsl = A;
  A = 1;
  F: __e_acsl_5 = __e_acsl_4;
  __e_acsl_2 = A;
  A = 2;
  /*@ assert \at(A,Pre) ≡ 0; */ ;
  e_acsl_assert(__e_acsl == 0,(char *)"Assertion",
                (char *)"(\\at(A,Pre) == 0)",13);
  /*@ assert \at(A,F) ≡ 1; */ ;
  e_acsl_assert(__e_acsl_2 == 1,(char *)"Assertion",
                (char *)"(\\at(A,F) == 1)",14);
  /*@ assert \at(A,Here) ≡ 2; */ ;
  __e_acsl_3 = A;
  e_acsl_assert(__e_acsl_3 == 2,(char *)"Assertion",
                (char *)"(\\at(A,Here) == 2)",15);
  /*@ assert \at(\at(A,Pre),F) ≡ 0; */ ;
  e_acsl_assert(__e_acsl_5 == 0,(char *)"Assertion",
                (char *)"(\\at(\\at(A,Pre),F) == 0)",16);
  A = 3;
  __e_acsl_6 = A;
  e_acsl_assert(__e_acsl_6 == 3,(char *)"Postcondition",
                (char *)"(\\at(A,Post) == 3)",9);
  return;
}

void g(int *p, int *q)
{
  int __e_acsl;
  int __e_acsl_2;
  int __e_acsl_3;
  int __e_acsl_4;
  *p = 0;
  *(p + 1) = 1;
  *q = 0;
  L1: __e_acsl_3 = *q;
  __e_acsl = *q;
  *p = 2;
  *(p + 1) = 3;
  *q = 1;
  L2: __e_acsl_2 = *(p + __e_acsl);
  A = 4;
  /*@ assert \at(*(p+\at(*q,L1)),L2) ≡ 2; */ ;
  e_acsl_assert(__e_acsl_2 == 2,(char *)"Assertion",
                (char *)"(\\at(*(p+\\at(*q,L1)),L2) == 2)",32);
  L3: 
  /*@ assert \at(*(p+\at(*q,L1)),Here) ≡ 2; */ ;
  __e_acsl_4 = *(p + __e_acsl_3);
  e_acsl_assert(__e_acsl_4 == 2,(char *)"Assertion",
                (char *)"(\\at(*(p+\\at(*q,L1)),Here) == 2)",34);
  return;
}

int main(void)
{
  int __retres;
  int x;
  int t[2];
  int __e_acsl;
  long long __e_acsl_2;
  int __e_acsl_3;
  x = 0;
  L: __e_acsl_3 = x;
  __e_acsl_2 = (long long)x + (long long)1;
  __e_acsl = x;
  /*@ assert x ≡ 0; */ ;
  e_acsl_assert(x == 0,(char *)"Assertion",(char *)"(x == 0)",45);
  x = 1;
  x = 2;
  f();
  /*@ assert \at(x,L) ≡ 0; */ ;
  e_acsl_assert(__e_acsl == 0,(char *)"Assertion",(char *)"(\\at(x,L) == 0)",
                50);
  /*@ assert \at(x+1,L) ≡ 1; */ ;
  e_acsl_assert(__e_acsl_2 == (long long)1,(char *)"Assertion",
                (char *)"(\\at(x+1,L) == 1)",51);
  /*@ assert \at(x,L)+1 ≡ 1; */ ;
  e_acsl_assert((long long)__e_acsl_3 + (long long)1 == (long long)1,
                (char *)"Assertion",(char *)"(\\at(x,L)+1 == 1)",52);
  g(t,& x);
  __retres = 0;
  return (__retres);
}