fix(cfg-builder): self-loops

The assignment originated from a PHI value should be always inserted
after the assume inserted by execEdge.

This fixes issue #94.

Note that this commit reverts commit cbab732.

Unfortunately, I do not remember the reason for that commit and it did
not include any test case.

lib/Clam/CfgBuilder.cc

@@ -4380,13 +4380,10 @@ void CfgBuilderImpl::buildCfg() {
       v.visit(const_cast<BasicBlock &>(*dst));
 
       if (tmp_mid_bb) {
-	if (&B == dst) {
-	  // If a self-loop then insert the assignments from PHI nodes
-	  // *before* the assume statements from execEdge.
-	  mid_bb->copy_front(*tmp_mid_bb);
-	} else {
-	  mid_bb->copy_back(*tmp_mid_bb);	  
-	} 
+	// We always insert the assignments from PHI nodes after the
+	// assume statements from execEdge.  Even if we are inside a
+	// self-loop.
+	mid_bb->copy_back(*tmp_mid_bb);	  
       }
     }
 

tests/simple/test-issue-94.c

@@ -0,0 +1,16 @@
+// RUN: %clam --crab-dom=zones --crab-check=assert "%s" 2>&1 | OutputCheck -l debug %s
+// CHECK: ^0  Number of total safe checks$
+// CHECK: ^0  Number of total error checks$
+// CHECK: ^1  Number of total warning checks$
+
+extern void __VERIFIER_assume(int);
+extern void __CRAB_assert(int);
+extern int __VERIFIER_nondet_int(void);
+
+int main() {
+  const int MAX = __VERIFIER_nondet_int();
+  __VERIFIER_assume(MAX <= 1);
+  for (int i = MAX - 1; i >= 0; i--) {
+  }
+  __CRAB_assert(MAX <= 0);
+}