问题标签 [frama-c]

是否可以在 ACSL 中为通常在使用 -lm 编译时调用的函数实现规范，如 sqrt ？我将它用于 Frama-C 的插件 WP。

这是一个小例子来说明我想要做什么。

显然，如果我这样做 WP 会哭，因为当我在注释中使用 sqrt 时它不存在。

[内核] 用户错误：注释中未绑定函数 sqrt

所以我想定义一个抽象的 sqrt，但我的测试都没有工作：

对于这个，我看不到我可以放入什么（...），因为我想要一个抽象定义而不是重新实现整个 float sqrt。

而这个并不能解决我的问题：

函数 sqrt 的代码和规范都没有，从原型生成默认分配。

Using the Cil_datatypes module defined in the Frama-C API, I am trying to replace a term (Cil_datatype) with a new term in a predicate (Cil_datatype). To do that I need to map a predicate with a function that when it finds the term (or terms) replaces it there. How do you map over a predicate to replace a term?

我在编译最新版本的 Frama-C 时遇到问题。我做了什么：

一分钟后我明白了

我正在使用 gcc 4.8.1、Ubuntu 12.04、ocaml 3.12.1

更新： VERBOSEMAKE=yes make

VERBOSEMAKE 提供几乎相同的信息。

我正在尝试使用 Frama-C (Neon-20140301) 和 Alt-Ergo 的 WP 教程示例。我陷入了“不匹配算法”示例，而其他类似示例（例如“相等”和“查找”）没有问题。代码如下所示。后置条件 P0、P2 未放电。谁能告诉我这里有什么问题？

我试图做两件事

1. 根据条件获取动态后向切片。
2. 将切片语句映射回实际的源代码。

问题 1：Frama-C 返回的切片没有返回与标准相关的确切语句 - 主要是ifandelse语句。

问题 2：如何将切片语句映射回源代码？切片时程序会发生变化（例如：int a=9在切片代码中变成 2 个语句，int a;并且a = 9;。）我对切片没问题，但是我可以使用哪些信息将这些映射回源代码中的语句。

这是源代码。

我使用以下命令来获取切片。

我从 frama-c 得到的切片是：

问题 1：我没有得到切片中的ifandelse条件。我应该怎么做才能得到它们？

我期望以下切片：

问题2：
源代码有：int ip1 = 9;

但切片代码有：

如何将这 2 个切片语句映射回源代码语句。

我正在尝试使用 Frama-C 对代码进行切片。

源代码是

当我使用 Frama-C 对代码进行切片时，我得到以下信息。我不知道这个“未定义的序列”是什么意思。

感谢任何帮助解释为什么会发生这种情况。

首先，我将解释我想在这里做什么：给定一个 C 大程序，我想输出数据的生产者/消费者列表和函数的调用/被调用函数列表，其中数据是。

为此，我正在考虑在我自己的插件中使用什么来计算 frama-c 的某些模块，例如 dataflow.ml 或 callgraph.ml。

但是，当我阅读插件开发者文档时，我无法看到我们如何访问这些模块的数据。

在我自己的插件中，“open.cyl_type”是否足够？

此外，这是我的其他问题：

我尝试将 pdg 插件用于我的目的，但是当我调用它并显示“pdg graph computed”时，我该如何访问它？

有没有比官方网页更多的关于“影响”插件的文档，深入，它是如何工作的？（我不得不说我正处于项目前期阶段，并且我在 ubuntu 上安装了带有 apt-get 的 frama-c，并且我没有得到一个影响插件工作（我将通过编译源代码来查看))

顺便说一句，你认为我使用正确的方法来达到我的目的吗？

是否可以使用 Frama-c 检测内存泄漏或双重释放？我试图测试那个例子但是

我得到：

现在我正在使用版本：Neon-20140301 和从 Fluorine-20130601 复制的libc（顺便说一下，为什么从 Neon 版本中删除了 fc_runtime.c 和其他 *.c 文件？）

命令：

使用其他定义 (FRAMA_C_MALLOC_XXXX) 有效，但未检测到任何错误。

更新：其他示例

我有以下示例代码：

但是 Frama-C / Why3 无法证明代码中注释的“要求”之一。.Why 文件说明以下内容：

为了学习，我的问题是：

1）该前提条件有什么问题？

2）基于 .Why 文件中的输出，我应该采取什么方法来找出问题所在？

3）有人可以指点我学习如何调试我的函数合同的资源吗？

编辑：

我使用以下标志运行 Frama-c：“-wp -wp-rte -wp-fct f_mount_temp”我没有从其他地方调用这个 f_mount_temp。我运行 Frama-c 直接检查这个 f_mount_temp()。

现在对我来说更清楚了，它可能是导致先决条件失败的额外断言。处理的函数契约如下，注释指示每个断言的状态：

-wp-rfe 标志添加的内联断言是：

我试图将源代码与切片代码进行比较，但 frama-c 在解析时对代码进行了规范化，这使得切片代码语句与源代码语句不同。

是否可以使用 frama-c 预处理代码，以便当我使用标准对其进行切片时，可以将生成的切片语句与预处理语句进行比较？

谢谢。