summaryrefslogtreecommitdiff
path: root/Test/test1/Frame1.bpl
blob: 469f43ba1c8d3ba3134f4a0c4494a405db09083c (plain)
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
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
var g0: int;
var g1: int;

var h0: [ref, name]int;
var h1: [ref, name]int;

const X: name;

procedure P(a: ref, hh: [ref, name]int) returns (b: int, hout: [ref, name]any);
  modifies h1, g0;

implementation P(a: ref, hh: [ref, name]int)
               returns (b: int, hout: [ref, name]any) {
  start:
    g0 := 5;
    g1 := 6;  // error: g1 is not in modifies clause
    a := null;  // error: in-parameters are not mutable 
    b := 12;
    goto next;
  next:
    havoc g0;
    havoc g1;  // error: g1 is not in modifies clause
    havoc a;  // error: in-parameters are not mutable
    havoc b;
    goto more;
  more:
    hh[a,X] := 101;  // error: in-parameter (hh) is not mutable
    h0[a,X] := 102;  // error: h0 is not in modifies clause
    h1[a,X] := 103;
    hh := h0;  // error: in-parameter is not mutable
    h0 := h1;  // error: h0 is not in modifies clause
    h1 := hh;
    havoc hh;  // error: in-parameter is not mutable
    havoc h0;  // error: h0 is not in modifies clause
    havoc h1;
    return;
}

procedure PX();
  modifies h1, g0;

procedure PY()
  modifies h1, g0;
{
  start:
    call PX();
    call PY();
    return;
}

procedure PZ()
  modifies h1;
{
  start:
    call PX();  // error: PX has larger frame than PZ
    return;
}

procedure Q() returns (x: int, y: int, h: [ref, name]int)
{
  start:
    return;
}

procedure QCallerBad()
{
  start:
    call g0, g1, h0 := Q();
    return;
}

procedure QCallerGood()
  modifies g0, h0;
{
  var t: int;

  start:
    call t, g0, h0 := Q();
    return;
}

procedure MismatchedTypes(x: int);

implementation MismatchedTypes(x: bool)  // error
{
  start:
    return;
}
implementation MismatchedTypes(y: bool)  // error (this time with a different name for the formal)
{
  start:
    return;
}


type ref, name, any;
const null : ref;