term.res.oracle 1.16 KB
Newer Older
1
# frama-c -wp [...]
2
3
4
5
[kernel] Parsing tests/bugs/term.cpp (external front-end)
Now output intermediate result
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
6
7
8
9
10
[wp] [CFG] Goal Z2m2_terminates : Valid (Trivial)
[wp] [CFG] Goal Z2m3_terminates : Valid (Trivial)
[wp] [CFG] Goal Z2m4_terminates : Valid (Trivial)
[wp] [CFG] Goal Z3m3a_terminates : Valid (Trivial)
[wp] [CFG] Goal Z3m3b_terminates : Valid (Trivial)
11
12
[wp] 3 goals scheduled
[wp] [Qed] Goal typed_Z2m2_ensures : Valid
Allan Blanchard's avatar
Allan Blanchard committed
13
14
[wp] [Qed] Goal typed_Z2m3_c_ensures : Valid
[wp] [Qed] Goal typed_Z3m3a_c_ensures : Valid
15
[wp] Proved goals:    8 / 8
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
  Qed:             3
/* Generated by Frama-C */
/*@ behavior c:
      requires \true; */
void m1(void)
{
  return;
}

/*@ requires \true;
    terminates \true;
    ensures \true; */
void m2(void)
{
  return;
}

/*@ terminates \true;
    
    behavior c:
      requires \true;
      ensures \true; */
void m3(void)
{
  return;
}

/*@ requires \true;
    terminates \true;
    
    behavior c:
      requires \true;
      ensures \true;
 */
void m3a(void)
{
  return;
}

/*@ terminates \true; */
void m3b(void)
{
  return;
}

/*@ terminates \true; */
void m4(void)
{
  return;
}