Skip to content

Commit 13c4b4b

Browse files
tautschnigtautschnig
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 13c4b4b

File tree

64 files changed

+177
-688
lines changed

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

+177
-688
lines changed

‎regression/cbmc-library/__builtin_fabs-01/main.c

Lines changed: 0 additions & 9 deletions
This file was deleted.

‎regression/cbmc-library/__builtin_fabs-01/test.desc

Lines changed: 0 additions & 8 deletions
This file was deleted.

‎regression/cbmc-library/__builtin_fabsf-01/main.c

Lines changed: 0 additions & 9 deletions
This file was deleted.

‎regression/cbmc-library/__builtin_fabsf-01/test.desc

Lines changed: 0 additions & 8 deletions
This file was deleted.

‎regression/cbmc-library/__builtin_fabsl-01/main.c

Lines changed: 0 additions & 9 deletions
This file was deleted.

‎regression/cbmc-library/__builtin_fabsl-01/test.desc

Lines changed: 0 additions & 8 deletions
This file was deleted.

‎regression/cbmc-library/__builtin_huge_val-01/main.c

Lines changed: 0 additions & 9 deletions
This file was deleted.

‎regression/cbmc-library/__builtin_huge_val-01/test.desc

Lines changed: 0 additions & 8 deletions
This file was deleted.

‎regression/cbmc-library/__builtin_huge_valf-01/main.c

Lines changed: 0 additions & 9 deletions
This file was deleted.

‎regression/cbmc-library/__builtin_huge_valf-01/test.desc

Lines changed: 0 additions & 8 deletions
This file was deleted.

0 commit comments

Comments
 (0)