bug fix (boogie-org#529)

Author: shazqadeer

Source/Concurrency/LinearTypeChecker.cs

@@ -379,6 +379,8 @@ public override Implementation VisitImplementation(Implementation node)
     {
       if (civlTypeChecker.procToAtomicAction.ContainsKey(node.Proc) ||
           civlTypeChecker.procToIntroductionAction.ContainsKey(node.Proc) ||
+          civlTypeChecker.procToIsAbstraction.ContainsKey(node.Proc) ||
+          civlTypeChecker.procToIsInvariant.ContainsKey(node.Proc) ||
           civlTypeChecker.procToLemmaProc.ContainsKey(node.Proc))
       {
         return node;

Test/civl/inductive-sequentialization/PingPong.bpl

@@ -73,49 +73,18 @@ PING' (x:int, {:linear_in "pid"} pid:int)
 returns ({:pending_async "PING"} PAs:[PA]int)
 modifies ping_channel, pong_channel;
 {
-  assert x > 0;
-  assert pid == ping_id;
-  assert (forall m:int :: ping_channel[m] > 0 ==> m == x);
   assert (exists {:pool "INV"} m:int :: ping_channel[m] > 0) && (forall m:int :: pong_channel[m] == 0);
+  call PAs := PING(x, pid);
 
-  assume ping_channel[x] > 0;
-  ping_channel[x] := ping_channel[x] - 1;
-
-  if (*)
-  {
-    pong_channel[x+1] := pong_channel[x+1] + 1;
-    PAs := NoPAs()[PING(x+1, pid) := 1];
-  }
-  else
-  {
-    pong_channel[0] := pong_channel[0] + 1;
-    PAs := NoPAs();
-  }
 }
 
 procedure {:IS_abstraction}{:layer 2}
 PONG' (y:int, {:linear_in "pid"} pid:int)
 returns ({:pending_async "PONG"} PAs:[PA]int)
 modifies ping_channel, pong_channel;
 {
-  assert y > 0;
-  assert pid == pong_id;
-  assert (forall m:int :: pong_channel[m] > 0 ==> m == y || m == 0);
   assert (exists {:pool "INV"} m:int :: pong_channel[m] > 0) && (forall m:int :: ping_channel[m] == 0);
-
-  if (*)
-  {
-    assume pong_channel[y] > 0;
-    pong_channel[y] := pong_channel[y] - 1;
-    ping_channel[y] := ping_channel[y] + 1;
-    PAs := NoPAs()[PONG(y+1, pid) := 1];
-  }
-  else
-  {
-    assume pong_channel[0] > 0;
-    pong_channel[0] := pong_channel[0] - 1;
-    PAs := NoPAs();
-  }
+  call PAs := PONG(y, pid);
 }
 
 ////////////////////////////////////////////////////////////////////////////////

Test/civl/inductive-sequentialization/ProducerConsumer.bpl

@@ -125,22 +125,8 @@ CONSUMER' (x:int, {:linear_in "pid"} pid:int)
 returns ({:pending_async "CONSUMER"} PAs:[PA]int)
 modifies head;
 {
-  var x':int;
-
-  assert pid == cons_id;
-  assert head < tail && (C[head] == x || C[head] == 0);
-
-  assume head < tail;
-  x' := C[head];
-  head := head + 1;
-  if (x' != 0)
-  {
-    PAs := NoPAs()[CONSUMER(x'+1, pid) := 1];
-  }
-  else
-  {
-    PAs := NoPAs();
-  }
+  assert head < tail;
+  call PAs := CONSUMER(x, pid);
 }
 
 ////////////////////////////////////////////////////////////////////////////////