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
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
68
69
70
71
72
73
74
|
(*module WhileLoop
type borrowed 'a = { cur: 'a ; fin: 'a }
(*
let cfg f [@cfg:stackify] () : () =
var a : int;
{ a <- 0; return () }
*)
let cfg nested_loops [@cfg:stackify] _x : ()
diverges
ensures { true }
=
var b : borrowed int;
{
goto BB0
}
BB0 {
switch (any bool)
| True -> goto BB1
| False -> goto BB2
end
}
BB1 {
b <- { b with cur = 0 };
goto BB0
}
BB2 {
assert { b.fin = b.cur };
return ()
}
end*)
module Decrement_Test
use mach.int.UInt32
use mach.int.Int
use mach.int.Int32
type borrowed 'a = { cur: 'a ; fin: 'a }
let cfg test [@cfg:stackify] (x : borrowed uint32) : ()
ensures { UInt32.to_int (x.fin) = 0 }
=
var _0 : ();
var x_1 : borrowed uint32 = x;
var _3 : bool;
var _4 : uint32;
{
goto BB0
}
BB0 {
goto BB1
}
BB1 {
invariant x { UInt32.to_int (x_1.cur) >= 0 };
_4 <- x_1.cur;
_3 <- _4 > (0 : uint32);
switch (_3)
| False -> goto BB3
| _ -> goto BB2
end
}
BB2 {
x_1 <- { x_1 with cur = ( x_1.cur - (1 : uint32)) };
goto BB1
}
BB3 {
assume { x_1.fin = x_1.cur };
return _0
}
end
|
