Skip to content

Commit 1a355b6

Browse files
committed
C library: make all branches of sqrt{,f,l} explicitly return
Makes GCC happier when doing library validation. Our C front-end would implicitly generate nondet return values of the correct type, so this does not actually change any verification behaviour.
1 parent d984199 commit 1a355b6

File tree

1 file changed

+3
-3
lines changed

1 file changed

+3
-3
lines changed

src/ansi-c/library/math.c

+3-3
Original file line numberDiff line numberDiff line change
@@ -758,7 +758,7 @@ float sqrtf(float f)
758758
case FE_TOWARDZERO :
759759
return (f - lowerSquare == 0.0f) ? lower : upper; break;
760760
default:;
761-
//assert(0);
761+
return __VERIFIER_nondet_float();
762762
}
763763

764764
}
@@ -835,7 +835,7 @@ double sqrt(double d)
835835
case FE_TOWARDZERO:
836836
return (d - lowerSquare == 0.0) ? lower : upper; break;
837837
default:;
838-
//assert(0);
838+
return __VERIFIER_nondet_double();
839839
}
840840

841841
}
@@ -906,7 +906,7 @@ long double sqrtl(long double d)
906906
case FE_TOWARDZERO:
907907
return (d - lowerSquare == 0.0l) ? lower : upper; break;
908908
default:;
909-
//assert(0);
909+
return __VERIFIER_nondet_long_double();
910910
}
911911

912912
}

0 commit comments

Comments
 (0)