Showing error 22

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_4_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
Show full sources