我必须使用一些静态处理 C 源代码的（半）自动验证软件（CBMC （链接） ）。支持浮点，但没有所有数学函数的定义。尝试检查是否可以用它检查数字软件。
所以我需要这些功能。我正在寻找一些math.h不使用协处理器的定义（例如sqrt，、、pow余数、tan；int// float）double。
当我在一些 linux 发行版（可能是现在的 eglibc）附带的 libc 中寻找它时，我总是达到一个点，其中有一些处理器内在特性，例如硬件 sqrt 函数。
第 1 部分：搜索软件实现
我需要的是一个支持具有以下特征的数学函数的库：
- 支持 IEEE 浮点数，但纯粹基于整数运行的库也会很棒，也许更好。
- 正确性是一个关键因素。（隐藏在某些来源中的特殊情况的已知错误并不那么酷）。根据 IEEE-754（例如 sqrt 规则），结果也应该是正确的。
- 不使用协处理器调用。纯软件。C 是首选，但 asm 也应该没问题。
到目前为止，我搜索了一些 libc 实现，尤其是关于嵌入式系统的实现。我认为这些库中的大多数都针对已编译程序的可移植性和大小，但很难判断它们是否使用了特定于处理器的指令。
- ** fdlibm 乍一看似乎有一些纯软件定义。我将进一步检查。但是源代码中提到了一些错误（代码不是标准的）。
- ** newlib似乎带来了相同的定义（基于 sun 微系统的代码）。但目前我不能确定是否始终使用这些软件版本，因此可能有一些我目前看不到的协处理器调用（见第 2 部分）。
- ** uClibc似乎与 newlib 共享该特性。
第 2 部分：了解这些实现的结构
有人能给我简要介绍一下这些数学库的结构吗？他们如何分派各种版本（例如特定的协处理器）？
文件名中这些不同前缀的含义是什么。
e_sqrt.c,k_sin,s_sin?
我很高兴听到一些对我有用的库。我更喜欢自带库，但有必要的时候，也可以找一些单一的函数实现，搭建一个小库。我不会使用 math.h 中定义的所有函数。
这个和这个SO-posts 说 Java 数学实现是/是基于fdlibm的，这听起来这个库是要走的路。我应该知道有关此库的更多信息的人吗？
似乎我有很多可能性，包括以下两种：
- 使用 glibc 并在软件模式下编译。问题是，我不能使用任何自动系统检查工具（在配置中）。我必须手动提供所有信息。是否有任何标志禁止使用 fp 协处理器和禁止 simd 操作？fp-without 应该是一个开始，然后如果它编译它也使用软浮点。我希望编译过程或多或少取决于主机的特定决定（如 arm ...）。
- 使用 fdlibm（目前首选）。问题：如何将我的程序链接到它？我需要像 assert 这样的非 libm 函数，但想要链接到我的 fdlibm 而不是已安装的 system-libm（因此 -nodefaultlibs 将禁止使用 assert）。