Commit 1a355b6
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
1 file changed
+3
-3
lines changed| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
758 | 758 | | |
759 | 759 | | |
760 | 760 | | |
761 | | - | |
| 761 | + | |
762 | 762 | | |
763 | 763 | | |
764 | 764 | | |
| |||
835 | 835 | | |
836 | 836 | | |
837 | 837 | | |
838 | | - | |
| 838 | + | |
839 | 839 | | |
840 | 840 | | |
841 | 841 | | |
| |||
906 | 906 | | |
907 | 907 | | |
908 | 908 | | |
909 | | - | |
| 909 | + | |
910 | 910 | | |
911 | 911 | | |
912 | 912 | | |
| |||
0 commit comments