Test/snapshots/Snapshots41.v1.bpl


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

procedure {:checksum "0"} M(x: int);
implementation {:id "M"} {:checksum "1"} M(x: int)
{
assert x < 20 || 10 <= x;  // always true
  
       assert x < 10;  // error
  call Other(x);  // error: precondition violation
  assert x == 7;  // error: this is a new error in v1
}


       procedure {:checksum "10"} Other(y: int);
         requires 0 <= y;
       implementation {:id "Other"} {:checksum "11"} Other(y: int)
       {
       }


procedure {:checksum "20"} Posty() returns (z: int);
  ensures 2 <= z;  // error: postcondition violation
implementation {:id "Posty"} {:checksum "21"} Posty() returns (z: int)
{
  var t: int;
  t := 20;
  if (t < z) {
    assert true;  // this is a new assert
  } else {  // the postcondition violation occurs on this 'else' branch
  }
}

  procedure   {:checksum "30"} NoChangeWhazzoeva(u: int);
  implementation {:id "NoChangeWhazzoeva"} {:checksum "3"} NoChangeWhazzoeva(u: int)
  {
       assert u != 53;  // error
  }

procedure {:checksum "40"} NoChangeAndCorrect();
implementation {:id "NoChangeAndCorrect"} {:checksum "41"} NoChangeAndCorrect() { assert true; }