问寻找math.h函数的纯c版本(不支持协处理器)

EN

我必须使用一些(半自动)自动验证软件(CBMC (链接))，它是静态地工作在C源上。浮点是支持的，但没有所有的数学函数的定义。其尝试是检查，是否有可能用它来检查数字软件。

所以我需要这些功能。我正在寻找一些没有协处理器使用的math.h 定义(例如，sqrt，pow，RE余数，tan；int/float/double). )。

当我在一些linux发行版(可能现在是eglibc)附带的libc中查找它时，我总是达到这样的程度，例如，有一些处理器--本质意味着硬件sqrt函数。

第1部分:搜索软件实现

我需要的是一个具有以下特点的支持数学函数的图书馆：

• IEEE浮点是受支持的，但是一个纯粹在整数上操作的库也会更好，也许更好。
• 正确性是一个关键因素。(隐藏在某些源中的特殊情况的已知bug并不那么酷)。在IEEE-754 (例如sqrt规则)方面，结果也应该是正确的。
• 不使用协处理器呼叫。纯粹的软件。C是首选，但asm也应该是好的。

到目前为止，我还在搜索各种libc实现，特别是关于嵌入式系统的实现。我认为这些库大多针对可移植性和编译程序的大小，但很难判断它们是否使用了特定于处理器的指令。

• **fdlibm乍一看似乎有一些纯粹的软件定义。我会进一步检查这个。但是源代码中提到了一些But (代码不是标准的)。
• **新库似乎带来了相同的定义(基于seems的代码)。但我目前还不能确定这些软件版本是否总是被使用，所以可能有一些我目前还没有看到的协处理器调用(见第2部分)。
• **uClibc似乎与newlib具有相同的特性。

第2部分:理解这些实现的结构

• 谁能给我简要介绍一下这些数学图书馆的结构。他们如何分配不同的版本(例如，一个特定的协处理器)？
• 文件名中这些不同前缀的含义是什么。e_sqrt.c，k_sin，s_sin

我很高兴听到一些可能对我有用的库。我倾向于在需要时使用库，但在必要时，也可以查找一些单一的函数实现，并构建一个小型库。我不会使用math.h中定义的所有函数。

这和这的帖子说Java实现是基于/基于fdlibm的，这听起来就是这个库的发展方向。有更多关于这个图书馆的信息吗？

看来我有很多可能性，包括以下两种：

1. 使用glibc并在软件模式中编译.问题是，我不能使用任何自动系统检查工具(在配置中)。我必须手动提供所有的信息。是否有任何标志禁止使用fp协处理器和禁止simd操作？fp-没有应该是一个开始，那么如果它编译的话，它也在使用软浮动。我希望编译过程或多或少取决于主机的特定决定(比如arm.)。
2. 使用fdlibm (目前首选)。问题:我如何将我的程序链接到它？我需要像assert这样的非libm函数，但希望链接到我的fdlibm，而不是安装的system(因此-nodefaultlibs将禁止使用断言)。