1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
|
[kernel] Parsing share/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing tests/syntax/bts0672_link.c (with preprocessing)
[kernel] Parsing tests/syntax/bts0672_link_2.c (with preprocessing)
tests/syntax/bts0672_link_2.c:10:[kernel] 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;
x = Frama_C_nondet(0,59);
return;
}
|
