Frama-C是一个专门用于分析C源代码的开源工具套件。
我正在尝试验证 musl libc memchr 的修改版本，它使用类型双关优化：它查找缓冲区前缀中的值，直到它与 sizeof(size_t) 对齐，然后使用
我目前正在使用 Frama-C 和 from 插件来获取变量之间的依赖关系。如果数组的多个元素具有相同的依赖关系，则会输出如下摘要：...
使用 frama-c 理解 `pointer_comparable`
我正在尝试使用 frama-c 通过指针比较来验证部分 C 代码。 但我不明白如何使用 \pointer_comparable 谓词。 根据 acsl 文档，\
我想知道为像 sizeof T[n] 这样的东西添加基本支持会有多困难（据我所知，这是用于可变长度数组的显式 C 构造），以便在 dy...
我正在尝试用 Frama-C 验证上述内容。从手册来看，Frama-C 似乎不太适合 malloc 和函数指针。我想知道我的验证中是否遗漏了一些内容
尝试使用 Frama-C 的 WP 证明器时，请传入以下内容： frama-c -lib-entry -main foo -wp foo.c 我收到错误：[wp] 用户错误：主入口点函数“foo”是（潜在...
刚刚安装了 Frama-C 28.1（镍），看来 Frama-C 甚至无法为我证明开箱即用的未签名加法。 给定文件 file.c： #包括 /*@ @分配 某事；...
我正在使用Frama-C验证以下程序并尝试在验证过程中获取程序状态。例如，我尝试在下面的代码中打印P0。 需要 x <= y; ensures x =...
在 macOS 上安装 Frama-C (23)、Why3 和 Coq 后，我运行了命令 rm -f ~/.why3.conf ; Why3 配置检测 显示以下消息 找到了 Prover Coq 版本 8.10.2，但没有 Why3 库
我是一位新的 Frama-C 用户，我正在尝试证明一个大型项目的某些属性。我看到一个特定的证明失败了，并尝试将问题减少到最小的可重现示例，并且......
运行 frama-c-gui 时，我想增加其字体大小（用于教程、课程、演示、视频等），以确保文本在大房间中可见。我该怎么办？
我想在 frama-c GUI 中更改为浅色模式，该模式以深色模式打开。 以为可以通过写来完成 frama-c-gui -gui-theme 如本教程中所示，但出现以下错误： [
我在 frama C 中的函数证明方面遇到问题。我用于证明的代码如下所示： #包括 /*@ 要求 len>=0 && alid(arr + (0 .. len-1...
在以下代码上运行命令 frama-c test.c -rte -eva -eva-slevel 1 然后 -wp 时，我得到以下结果： Frama-c 24：没有错误 Frama-c 25/26：unrea 中溢出...
环境：24.0（铬） 命令：frama-c -wp -wp-legacy xx.c #包括 整数 r; /*@ 需要 alid_read(a + (0 .. length-1)) && length > 0; 分配 r； 确保口头...
导出 FRAMA-C/WP 发送到求解器的 SAT/SMT 方程
是否可以导出或记录由 FRAMA-C/WP 和 Why3 生成的 SAT/SMT 方程，发送到 SAT-SMT 求解器（如 Alt-Ergo 或 Z3）？ 如果使用求解器 Z3（例如 vi...
我很好奇Frama-C是否已经使用Frama-C或其他验证框架进行了正式验证，因为Frama-C中的错误可能会导致Frama-C go验证的程序出现错误...
我不明白为什么frama-c不能证明这部分的shell排序算法。我将 Astraver 与 Alt-Ergo 2.4.3 和 CVC v1.8 结合使用，它们将最后一个循环中的条件标记为证明过程...
Frama-C 的 IDE/工作流程？ （特别是对于 WP 插件）
TL;DR：你们如何使用WP插件？ （你使用什么前端、构建工具等？你的工作流程是什么？） Frama-C 附带 frama-c-gui，这是一个可以帮助开发人员导航和分析 cod 的 GUI...
Frama-c似乎允许无符号整数数学做wrap-around，同时它假设有符号整数数学不会溢出，这需要以后用-wp-rte标志来证明。(我个人是 ...