Commit 9ba065d
committed
Math library models: add missing *BSD variants, cleanup
BSD systems appear to use `__` prefixed variants of several functions.
Define these as needed. Also, avoid handling some GCC-style
`__builtin_`-prefixed functions via models when others are done directly
in the type checker: do all of them in the type checker.1 parent 48490fb commit 9ba065d
File tree
64 files changed
+168
-685
lines changed- regression/cbmc-library
- __builtin_fabs-01
- __builtin_fabsf-01
- __builtin_fabsl-01
- __builtin_huge_val-01
- __builtin_huge_valf-01
- __builtin_huge_vall-01
- __builtin_inf-01
- __builtin_inff-01
- __builtin_infl-01
- __builtin_isinf-01
- __builtin_isinff-01
- __builtin_isnan-01
- __builtin_isnanf-01
- __fpclassify-01
- __isinf-01
- __isinff-01
- __isinfl-01
- __isnan-01
- __isnanf-01
- __isnanl-01
- __isnormalf-01
- __signbit-01
- __signbitf-01
- _isnan-01
- isfinite-01
- isinf-01
- isinff-01
- isinfl-01
- isnanf-01
- isnanl-01
- isnormal-01
- signbit-01
- src/ansi-c
- library
Some content is hidden
Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.
64 files changed
+168
-685
lines changedThis file was deleted.
This file was deleted.
This file was deleted.
This file was deleted.
This file was deleted.
This file was deleted.
This file was deleted.
This file was deleted.
This file was deleted.
This file was deleted.
0 commit comments