问题标签 [frama-c]

在没有 main 函数的 C 文件上运行 Frama-C 时，出现错误。是否有任何选项可以对此类 C 文件运行 Frama-C 值分析？

在下文中，当相关的 C 代码被注释掉时，行为 neg_limit 的后置条件如何被证明为真？

正如预期的那样，Safety->check 算术溢出之一是不可证明的，但似乎 neg_limit 也应该是不可证明的。

背景：我正在使用 Frama-C-Boron、Jessie 以及通过 gWhy、Alt-Ergo 来学习如何编写规范并证明函数符合它们。任何关于规范策略、工具等的线索测试、RTFMing 等也值得赞赏。到目前为止，我正在阅读 ACSL 1.7 实施手册（比 -Boron 的更新）和 Jessie 教程和参考。手动的。

谢谢！

这是第一个后置条件的 gWhy 目标：

第二个：

我应该如何证明如下代码的正确性，为了避免效率低下，它依赖于模运算？

我已经尝试过 WP 的“int”模型，但是，如果我理解正确，该模型配置了 PO 中逻辑整数的语义，而不是 C 代码的正式模型。例如，当使用“int”模型时，WP 和 RTE 插件仍然需要并为上面的无符号加法注入溢出断言 PO。

在这种情况下，我是否可以为语句或基本块添加规定逻辑模型的注释，以便我可以告诉 Frama-C 特定编译器如何实际解释语句？如果是这样，我可以使用其他验证技术来处理已定义但经常导致缺陷的行为，如无符号环绕、编译器定义的行为、非标准行为（内联组件？）等，然后证明周围的代码。我正在描绘类似于（但比）更强大的“断言修复”，用于通知某些静态分析器某些属性在它们无法为自己派生属​​性时保持不变。

我正在使用 Frama-C Fluorine-20130601，作为参考，使用 alt-ergo 95.1。

如何在 Mac 上安装当前的 Frama-C 版本及其先决条件？

我有一台运行 Mac OS X 10.6.8 的笔记本电脑和一台运行 Mac OS X 10.7.5 的台式机，我可以在上面安装软件。我还可以访问运行 Mac OS X 10.8 的机器实验室，如果我问得好，我们的技术支持人员会在上面安装东西。

我有一个学生对程序分析感兴趣，需要一些我们有机会理解和添加的东西。我已经知道 Frama-C，另一所大学的同事推荐了它。

我之前曾尝试安装 Frama-C，但惨遭失败。同事评论说他也有同样的经历。嗯，时代变了。所以我访问了 Frama-C 网站，比以往任何时候都更加深刻和渴望拥有它，并开始着手。

frama-c.com 下载页面没有指向任何平台的当前 (Flourine 3) 版本的任何二进制文件的链接。安装说明的链接将我带到一个说下载自动安装程序的页面。什么自动安装程序？

有旧版 Mac OS X 的说明，但按照这些说明没有用；按照指示加载一组先决条件会产生下一个先决条件（gtksourceview）不会安装的状态。

当然，我检查了较旧的版本，发现有 Mac OS X Leopard 的 Nitrogen 版本，但是“请将存档解压缩为 /​​ 中的根目录”要求我执行不可能的操作。我没有 root 帐户，也永远不会得到一个（机器都属于大学）。完全可以在任何你喜欢的地方安装 gcc 和 clang；为什么 Frama-C 想要在 / 中？

我的 Frama-C 插件使用makeGlobalVar ~logic:true name type. 这些 varinfo 在 AST 中不存在（它们是目标程序中分配函数调用结果的占位符，在分析期间“动态”创建）。如果我的插件注意不在这些 varinfo 上保留任何强指针，它们是否有机会被垃圾收集？或者它们是否注册在具有强指针的数据结构中？如果是这样，是否有可能使该数据结构变弱？OCaml 没有在其他语言的文献中发现的各种弱数据结构，但没有什么是定期显式通过清理空存根无法解决的问题。

现在想想，我什至可能不必创建 varinfo。不过现在换插件有点晚了。我使用的 varinfo 是 C 类型的名称和表示形式。函数makeGlobalVar为名称提供了唯一性保证，我想这很好，只要它不会在过程中创建指向它或它的一部分的强指针。

语境：

假设您正在编写一个 C 解释器来执行调用malloc()和free(). 如果目标程序没有内存泄漏（它释放它分配的所有内容并且从不持有太多内存），您希望解释器的行为相同。

当我尝试使用默认逻辑标签 LoopEntry 和 LoopCurrent 时，我遇到了一些麻烦。这是一个简单的示例，我使用的不同证明者（alt-ergo、coq、cvc3、z3）无法证明：

特别是，第一和第二不变量没有被证明（其他没有问题）。现在，如果我通过在 i 的声明/定义之后添加标签“label”来修改这个简单的示例，并且如果我引用该标签，并通过 Here 更改 LoopCurrent （这给出了这个片段：

)

现在一切都被证明了。

我发现有关 Acsl 默认逻辑标签的文档很容易理解，并且我希望第一个示例被证明为第二个示例。你能解释一下问题出在哪里吗？

袋鼠

PS1：在循环子句中使用 Pre 时指的是什么？第一次循环迭代或上一次迭代之前的状态？？

PS2：我正在使用 Frama-C Fluorine，但也许我没有为每个小更新进行升级

我正在发现 Frama-C 软件，我想知道是否有可能检测到某些代码模式，例如双重 if 测试，或者例如对给定函数的调用总是后面跟着另一个。

或者可能使用变量名称的东西，例如检查具有给定前缀命名的变量是否属于某种类型。

您认为 Frama-C 是否可行（使用 ACSL 或开发新模块）？

非常感谢 =)

我无法区分 ACSL 中的各种前置条件和后置条件。据我所知，要求、终止和假设出现在前置条件中，并在后置条件中确保和分配。但在哪一组休息，如减少等？

任何机构都可以帮助我弄清楚吗？提前致谢

I want to explore Frama-C to apply Assertion-based Slicing (using ACSL notation). I have found that there are several different versions of Frama-C with some different features. My question is which version is best suited to develop a a slicing plugin to Frama-C and to manipulate the AST created by Frama-C.

我正在尝试在 mac os x 10.9 中安装最新版本的 frama-c(Fluorine 3)。使用 brew 我能够满足 frama-c 的先决条件（Gtk、GtkSourceView、GnomeCanvas 和 Lablgtk2）

配置文件的结果如下：

它似乎满足了所有必要的先决条件。但是在运行 make 时出现以下错误：

谁能告诉我我做错了什么？