Frama-C是一个专门用于分析C源代码的开源工具套件。
我在 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标志来证明。(我个人是 ...
frama-c slicing插件似乎会丢弃使用过的堆栈值。
问题描述 我正在开发一个frama-c插件，使用slicing插件作为库来删除自动生成的代码中未使用的部分。不幸的是，slicing插件掉了一堆 ...
我相信我错过了一些明显的东西，但我已经尝试了很多，我还没有设法找到问题的根源。我是按照Frama-C的acsl指南来做的。有这个介绍...
在加载.C文件时，Frama-C报告 "外部链接规范中的无效鬼魂"。
我对Frama-C非常陌生，所以也许我错过了一些明显的东西。当我试图加载我的项目文件时，Frama-C在Console窗口中报告了以下错误，并停止处理[kernel]...
Frama-C在加载.C文件时报告“外部链接规范中的无效重影”
我对Frama-C非常陌生，所以也许我缺少明显的东西。当我尝试加载我的项目文件（其中包括一些.C文件）时，Frama-C在控制台窗口中报告以下错误，并停止...
我尝试了ACSL手册中的列表示例（第37页上的示例2.23，在“功能合同”部分中，但我隐藏了incr_list的实现并更改了返回类型。完整资料如下。 ...
我经常在其他正式规范中使用集合的基数，我想知道是否可以在带有WP frama-c插件的ACSL中使用它。例如，对我来说，假设假设card（...
我是一名学生，目前正在尝试使用cppcheck和frama-c分析C中OPC Ua协议的参考实现。我的目标不是进行非常专门的测试，而是进行一些常规/ ...] >>
我有一个简单的矩阵转置函数，我想用后置条件进行验证，以使matrix_transpose（matrix_transpose（original_matrix）== original_matrix的语法是什么...
我如何将frama-c CLI代码映射到原始c语句？以及如何找到frama-c的api的文档？
我正在尝试在原始代码的语句级别使用frama-c获取程序依赖图（PDG）。但是，frama-c中的“ pdg”插件会在已解析代码的节点级别上打印PDG。由于...
我正在尝试在原始代码的语句级别使用frama-c获取程序依赖图（PDG）。但是，frama-c中的“ pdg”插件会在已解析代码的节点级别上打印PDG。由于...
我已经安装了frama-c和why3，但是当我尝试启动frama-c时，出现jessie3错误。 frama-c -verbose 2 [kernel]警告：无法加载插件“ Jessie3”（与Neon-20140301不兼容）。 ...
[当我开始使用Frama-C进行C形式验证时，我试图正式验证如下编写的整数二进制对数函数：// @逻辑整数pow2（integer n）=（n == .. 。