Showing error 21

User: Jiri Slaby
Error type: Reachable Error Location
Error type description: A specified error location is reachable in some program path
File location: bitvector/soft_float_3_safe.c.cil.c
Line in file: 4
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC

Source: 

  1extern int nondet_int(void);
  2void __VERIFIER_assert(int cond) {
  3  if (!(cond)) {
  4    ERROR: goto ERROR;
  5  }
  6  return;
  7}
  8/* Generated by CIL v. 1.3.7 */
  9/* print_CIL_Input is true */
 10
 11unsigned int base2flt(unsigned int m , int e ) 
 12{ unsigned int res ;
 13  unsigned int __retres4 ;
 14
 15  {
 16  if (! m) {
 17    __retres4 = 0U;
 18    goto return_label;
 19  } else {
 20
 21  }
 22  if (m < 1U << 24U) {
 23    {
 24    while (1) {
 25      while_0_continue: /* CIL Label */ ;
 26      if (e <= -128) {
 27        __retres4 = 0U;
 28        goto return_label;
 29      } else {
 30
 31      }
 32      e = e - 1;
 33      m = m << 1U;
 34      if (m < 1U << 24U) {
 35
 36      } else {
 37        goto while_0_break;
 38      }
 39    }
 40    while_0_break: /* CIL Label */ ;
 41    }
 42  } else {
 43    {
 44    while (1) {
 45      while_1_continue: /* CIL Label */ ;
 46      if (m >= 1U << 25U) {
 47
 48      } else {
 49        goto while_1_break;
 50      }
 51      if (e >= 127) {
 52        __retres4 = 4294967295U;
 53        goto return_label;
 54      } else {
 55
 56      }
 57      e = e + 1;
 58      m = m >> 1U;
 59    }
 60    while_1_break: /* CIL Label */ ;
 61    }
 62  }
 63  m = m & ~ (1U << 24U);
 64  res = m | (unsigned int )((e + 128) << 24U);
 65  __retres4 = res;
 66  return_label: /* CIL Label */ 
 67  return (__retres4);
 68}
 69}
 70unsigned int addflt(unsigned int a , unsigned int b ) 
 71{ unsigned int res ;
 72  unsigned int ma ;
 73  unsigned int mb ;
 74  unsigned int delta ;
 75  int ea ;
 76  int eb ;
 77  unsigned int tmp ;
 78  unsigned int __retres10 ;
 79
 80  {
 81  if (a < b) {
 82    tmp = a;
 83    a = b;
 84    b = tmp;
 85  } else {
 86
 87  }
 88  if (! b) {
 89    __retres10 = a;
 90    goto return_label;
 91  } else {
 92
 93  }
 94  {
 95  ma = a & ((1U << 24U) - 1U);
 96  ea = (int )(a >> 24U) - 128;
 97  ma = ma | (1U << 24U);
 98  mb = b & ((1U << 24U) - 1U);
 99  eb = (int )(b >> 24U) - 128;
100  mb = mb | (1U << 24U);
101  __VERIFIER_assert(ea >= eb);
102  delta = ea - eb;
103  mb = mb >> delta;
104  }
105  if (! mb) {
106    __retres10 = a;
107    goto return_label;
108  } else {
109
110  }
111  ma = ma + mb;
112  if (ma & (1U << 25U)) {
113    if (ea == 127) {
114      __retres10 = 4294967295U;
115      goto return_label;
116    } else {
117
118    }
119    ea = ea + 1;
120    ma = ma >> 1U;
121  } else {
122
123  }
124  {
125  __VERIFIER_assert(ma < 1U << 25U);
126  ma = ma & ((1U << 24U) - 1U);
127  res = ma | (unsigned int )((ea + 128) << 24U);
128  }
129  __retres10 = res;
130  return_label: /* CIL Label */ 
131  return (__retres10);
132}
133}
134unsigned int mulflt(unsigned int a , unsigned int b ) 
135{ unsigned int res ;
136  unsigned int ma ;
137  unsigned int mb ;
138  unsigned long long accu ;
139  int ea ;
140  int eb ;
141  unsigned int tmp ;
142  unsigned int __retres10 ;
143
144  {
145  if (a < b) {
146    tmp = a;
147    a = b;
148    b = tmp;
149  } else {
150
151  }
152  if (! b) {
153    __retres10 = 0U;
154    goto return_label;
155  } else {
156
157  }
158  ma = a & ((1U << 24U) - 1U);
159  ea = (int )(a >> 24U) - 128;
160  ma = ma | (1U << 24U);
161  mb = b & ((1U << 24U) - 1U);
162  eb = (int )(b >> 24U) - 128;
163  mb = mb | (1U << 24U);
164  ea = ea + eb;
165  ea = ea + 24;
166  if (ea > 127) {
167    __retres10 = 4294967295U;
168    goto return_label;
169  } else {
170
171  }
172  if (ea < -128) {
173    __retres10 = 0U;
174    goto return_label;
175  } else {
176
177  }
178  accu = ma;
179  accu = accu * (unsigned long long )mb;
180  accu = accu >> 24U;
181  if (accu >= (unsigned long long )(1U << 25U)) {
182    if (ea == 127) {
183      __retres10 = 4294967295U;
184      goto return_label;
185    } else {
186
187    }
188    ea = ea + 1;
189    accu = accu >> 1U;
190    if (accu >= (unsigned long long )(1U << 25U)) {
191      __retres10 = 4294967295U;
192      goto return_label;
193    } else {
194
195    }
196  } else {
197
198  }
199  ma = accu;
200  ma = ma & ~ (1U << 24U);
201  res = ma | (unsigned int )((ea + 128) << 24U);
202  __retres10 = res;
203  return_label: /* CIL Label */ 
204  return (__retres10);
205}
206}
207int main(void) 
208{ unsigned int a ;
209  unsigned int ma ;
210  signed char ea ;
211  unsigned int b ;
212  unsigned int mb ;
213  signed char eb ;
214  unsigned int r_mul ;
215  unsigned int zero ;
216  unsigned int one ;
217  int sb ;
218  int tmp ;
219  int tmp___0 ;
220  int tmp___1 ;
221  int __retres16 ;
222
223  {
224  {
225  zero = base2flt(0, 0);
226  one = base2flt(1, 0);
227  a = base2flt(ma, ea);
228  b = base2flt(mb, eb);
229  r_mul = mulflt(a, b);
230  }
231  if (b < one) {
232    sb = -1;
233  } else {
234    if (b > one) {
235      tmp = 1;
236    } else {
237      tmp = 0;
238    }
239    sb = tmp;
240  }
241  if (sb == 0) {
242    if (r_mul < a) {
243      tmp___1 = -1;
244    } else {
245      if (r_mul > a) {
246        tmp___0 = 1;
247      } else {
248        tmp___0 = 0;
249      }
250      tmp___1 = tmp___0;
251    }
252    {
253    __VERIFIER_assert(tmp___1 == 0);
254    }
255  } else {
256
257  }
258  __retres16 = 0;
259  return (__retres16);
260}
261}
↑