寻找一个纯c版本的math.h函数（没有协处理器支持）

我必须使用静态验证C源的一些（半）自动验证软件（CBMC（链接））。支持浮点，但没有所有数学函数的定义。尝试检查是否可以用它来检查数字软件。 所以我需要这些功能。我正在寻找一些没有使用协处理器的

math.h

定义（例如

sqrt

，

pow

，余数，

tan

;

int

/

float

/

double

）。 当我在一些Linux发行版附带的libc（也许现在是eglibc）中查找它时，我总是达到一个点，其中有一些处理器内在函数意味着硬件sqrt函数。 第1部分：搜索软件实现 我需要的是一个支持数学函数的库，具有以下特征： 支持IEEE浮点数，但纯粹基于整数运行的库也会很棒，也许更好。 正确性是一个关键因素。 （隐藏在某些来源的特殊情况的已知错误并不那么酷）。根据IEEE-754（例如sqrt的规则），结果也应该是正确的。 不使用协处理器调用。纯软件。 C是首选，但asm也应该没问题。 到目前为止，我搜索了各种libc实现，特别是有关嵌入式系统的实现。我认为这些库中的大多数都是针对编译程序的可移植性和大小，但很难说它们是否使用特定于处理器的指令。 ** fdlibm乍一看似乎有一些纯软件定义。我会进一步检查。但是在源代码中提到了一些错误（代码不是标准的）。 ** newlib似乎带来了相同的定义（基于sun microsystems的代码）。但是我现在不能肯定地说这些软件版本是否总是被使用，所以可能会有一些我目前看不到的协处理器调用（参见第2部分）。 ** uClibc似乎与newlib共享特征。 第2部分：了解这些实现的结构 有人能给我一些关于这些数学库结构的简短介绍。他们如何调度各种版本（例如特定的协处理器）？ 这些不同前缀在文件名中的含义是什么？

e_sqrt.c

，

k_sin

，

s_sin

？ 我很高兴听到一些对我有用的图书馆。我宁愿选择一个库，但是当它有必要时，也可以寻找一些单一的函数实现并构建一个小型库。我不会使用math.h中定义的所有函数。 这个和这个SO帖子都说Java Math Implementation是基于fdlibm的，这听起来这个库是可行的。有关这个库的更多信息的人我应该知道吗？ 似乎我有很多可能性，包括以下两个： 使用glibc并在软件模式下编译。问题是，我不能使用任何自动系统检查工具（在configure中）。我必须手动提供所有信息。是否有任何标志禁止使用fp-coprocessor并禁止simd操作？ fp-without应该是一个开头，然后如果编译它也使用soft-float。我希望编译过程或多或少依赖于主机的特定决策（如arm ......）。 使用fdlibm（目前首选）。问题：如何将程序链接到它？我需要像assert这样的非libm函数，但想要链接我的fdlibm而不是安装的system-libm（所以-nodefaultlibs将禁止使用assert）。