assigns_result.res.oracle

[kernel] Parsing tests/spec/assigns_result.i (no preprocessing)
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
  X ∈ {0}
  Y ∈ {0}
[eva] computing for function f <- main.
  Called from tests/spec/assigns_result.i:16.
[eva] using specification for function f
[eva] Done for function f
[eva] computing for function g <- main.
  Called from tests/spec/assigns_result.i:16.
[eva] using specification for function g
[eva] tests/spec/assigns_result.i:16: Warning: 
  cannot interpret assigns clause \exit_status
  (unsupported logic var \exit_status); effects will be ignored
[eva] Done for function g
[eva] Recording results for main
[eva] done for function main
[from] Computing for function main
[from] Computing for function f <-main
[from] Done for function f
[from] Computing for function g <-main
[from] tests/spec/assigns_result.i:16: Unable to extract assigns in g
[from] Done for function g
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
  These dependencies hold at termination for the executions that terminate:
[from] Function f:
  \result FROM ANYTHING(origin:Unknown)
[from] Function g:
  \result FROM X
[from] Function main:
  NO EFFECTS
[from] ====== END OF DEPENDENCIES ======
/* Generated by Frama-C */
int X;
int Y;
/*@ assigns \nothing; */
int f(void);

/*@ assigns \result;
    assigns \result \from X;
    assigns \exit_status \from Y; */
int g(void);

void main(void)
{
  f();
  g();
  return;
}