bug in references comparison

[m-carrasco]

This code is generated by contractor-net instrumentation. I'm sorry I can't provide a smaller piece code. However it seems quite similar to #8 .

Hopefully this bug produced a boogie code that did not typed (using TinyBCT)

DLL: Queue.zip
password: analysis-net

TAC

Method:

System.Collections2.Queue.STATE$System_Collections2_Queue_ctorSystem_Int32~System_Collections2_Queue_ctorSystem_Int32~STATE$System_Collections2_Queue_EnqueueSystem_Object

Check label L_00C9

  parameter Queue this;
  parameter Int32 capacity;

  local Boolean local_0;
  local Object[] $r2;
  local Object $r3;
  local Boolean $r4;
  local String $r5;
  local Int32 $r7;
  local Int32 $r8;
  local Boolean $r9;
  local Boolean $r10;
  local Boolean $r11;
  local String $r12;
  local Int32 $r14;
  local Int32 $r15;
  local Boolean $r21;
  local Int32 $r17;
  local Int32 $r18;
  local Boolean $r19;
  local Boolean $r20;
  local String $r22;
  local Int32 local_1;
  local Int32 local_2;
  local Single local_3;
  local Int32 $r28;
  local ArgumentOutOfRangeException $r32;
  local Double $r30;
  local Double $r31;
  local Double $r37;
  local Double $r38;
  local ArgumentOutOfRangeException $r34;
  local Object[] $r41;
  local Int32 $r43;
  local Int32 $r45;
  local Int32 $r47;
  local Single $r50;
  local Single $r51;
  local Int32 $r52;
  local InvalidOperationException local_4;
  local ArgumentOutOfRangeException local_5;
  local Object[] $r54;
  local Object $r55;
  local Boolean local_6;
  local Int32 $r61;
  local Int32 $r62;
  local Boolean $r63;
  local Boolean $r64;
  local Boolean $r65;
  local Boolean $r66;
  local Boolean local_7;
  local Int32 $r70;
  local Int32 $r71;
  local Boolean $r80;
  local Int32 $r76;
  local Int32 $r77;
  local Boolean $r78;
  local Boolean $r79;
  local Boolean $r81;
  local Boolean local_8;
  local Int32 $r83;
  local Int32 $r84;
  local Boolean $r85;
  local Boolean $r86;
  local Boolean $r87;
  local Boolean $r88;
  local String $r93;

  L_0000:  nop;
           Contract::Ensures(local_0);
           $r2 = this._array;
           $r3 = null;
           $r4 = $r2 != $r3;
           $r5 = "Type invariant";
           Contract::Assume($r4, $r5);
           $r7 = this._size;
           $r8 = 0;
           $r9 = $r7 < $r8;
           $r10 = false;
           $r11 = $r9 == $r10;
           $r12 = "Type invariant";
           Contract::Assume($r11, $r12);
           $r14 = this._growFactor;
           $r15 = 1;
           if $r14 >= $r15 goto L_003B;
  B_0004:  $r21 = false;
           goto L_0048;
  L_003B:  nop;
           $r17 = this._growFactor;
           $r18 = 10;
           $r19 = $r17 > $r18;
           $r20 = false;
           $r21 = $r19 == $r20;
  L_0048:  $r22 = "Type invariant";
           Contract::Assume($r21, $r22);
           local_1 = 0;
           local_2 = 0;
  L_0056:  try;
  B_0007:  try;
           local_3 = 2;
           Queue::init_default_values(this);
           $r28 = 0;
           if capacity >= $r28 goto L_006C;
  B_0009:  $r32 = new ArgumentOutOfRangeException;
           ArgumentOutOfRangeException::.ctor($r32);
           throw $r32;
  L_006C:  nop;
           $r30 = local_3 as Double;
           $r31 = 1;
           if $r30 < $r31 goto L_0086;
  L_0079:  nop;
           $r37 = local_3 as Double;
           $r38 = 10;
           if $r37 <= $r38 goto L_008C;
  L_0086:  $r34 = new ArgumentOutOfRangeException;
           ArgumentOutOfRangeException::.ctor($r34);
           throw $r34;
  L_008C:  nop;
           $r41 = new Object[capacity];
           this._array = $r41;
           $r43 = 0;
           this._head = $r43;
           $r45 = 0;
           this._tail = $r45;
           $r47 = 0;
           this._size = $r47;
           $r50 = 100;
           $r51 = local_3 * $r50;
           $r52 = $r51 as Int32;
           this._growFactor = $r52;
           goto L_00C9;
  L_00BD:  catch InvalidOperationException local_4;
           local_1 = 1;
           goto L_00C9;
  L_00C3:  catch ArgumentOutOfRangeException local_5;
           local_1 = 2;
           goto L_00C9;
  L_00C9:  nop;
           $r54 = this._array; 
           $r55 = null;
           if $r54 > $r55 goto L_00D5; // <-------- WRONG OPERATOR! 
  B_0011:  local_6 = true;
           goto L_00E4;
  L_00D5:  nop;
           $r61 = this._size;
           $r62 = 0;
           $r63 = $r61 < $r62;
           $r64 = false;
           $r65 = $r63 == $r64;
           $r66 = false;
           local_6 = $r65 == $r66;
  L_00E4:  nop;
           if local_6 == false goto L_00ED;
  B_0014:  local_7 = true;
           goto L_0109;
  L_00ED:  nop;
           $r70 = this._growFactor;
           $r71 = 1;
           if $r70 >= $r71 goto L_00F9;
  B_0017:  $r80 = false;
           goto L_0106;
  L_00F9:  nop;
           $r76 = this._growFactor;
           $r77 = 10;
           $r78 = $r76 > $r77;
           $r79 = false;
           $r80 = $r78 == $r79;
  L_0106:  $r81 = false;
           local_7 = $r80 == $r81;
  L_0109:  nop;
           if local_1 == local_2 goto L_0112;
  B_001A:  local_8 = true;
           goto L_0121;
  L_0112:  nop;
           $r83 = this._size;
           $r84 = 0;
           $r85 = $r83 > $r84;
           $r86 = false;
           $r87 = $r85 == $r86;
           $r88 = false;
           local_8 = $r87 == $r88;
  L_0121:  nop;
           if local_8 == false goto L_012A;
  B_001D:  local_0 = true;
           goto L_012C;
  L_012A:  local_0 = local_7;
  L_012C:  nop;
           $r93 = "Negated target state invariant";
           Contract::Assert(local_0, $r93);
           return;

try L_0056 to L_00BD catch InvalidOperationException handler L_00BD to L_00C3
try L_0056 to L_00BD catch ArgumentOutOfRangeException handler L_00C3 to L_00C9