1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
|
[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;
}
|
