bts0672_link.1.res.oracle

[kernel] Parsing bts0672_link.c (with preprocessing)
[kernel] Parsing bts0672_link_2.c (with preprocessing)
/* 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;
 */
int Frama_C_nondet(int a, int b);

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