blob: e1ae938c3c16d61a7c2736129a80c60173868f13 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
// RUN: %boogie "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
procedure p() returns ($r: int);
ensures |{ $bb0: return ($r == 1); }|;
implementation p() returns ($x: int)
{
$x := 1;
return;
}
procedure q()
ensures |{ var $b: bool; $0: $b := true; goto $1; $1: return $b; }|;
{
}
|
