bts0672_link.0.res.oracle

[kernel] Parsing bts0672_link.c (with preprocessing)
[kernel] Parsing bts0672_link_2.c (with preprocessing)
[kernel:typing:implicit-function-declaration] bts0672_link_2.c:10: Warning: 
  Calling undeclared function Frama_C_nondet. Old style K&R code?
/* Generated by Frama-C */
int Frama_C_entropy_source;
/*@ predicate foo(ℤ x) = \true;
 */
/*@ ensures foo(\result);
    assigns \result, Frama_C_entropy_source;
    assigns \result \from a, b, Frama_C_entropy_source;
    assigns Frama_C_entropy_source \from Frama_C_entropy_source;
 */
extern int Frama_C_nondet(int a, int b);

void main(void)
{
  int x = Frama_C_nondet(0,59);
  return;
}