1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
|
[kernel] Parsing share/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing tests/syntax/ptr_null_cmp_bts1027.i (no preprocessing)
/* Generated by Frama-C */
/*@ behavior normal:
assumes r ≢ \null ∧ ¬(x ≢ 0.);
ensures \result ≡ 0;
behavior f:
assumes ¬(r ≢ \null) ∨ x ≢ 0.;
ensures \result ≡ -1;
*/
int max(int *r, double x)
{
int __retres;
if (! r) {
__retres = -1;
goto return_label;
}
else
if (x) {
__retres = -1;
goto return_label;
}
__retres = 0;
return_label: return __retres;
}
|
