问题标签 [frama-c]
For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.
frama-c - ACSL 规范中的命名常量
如何在 ACSL 规范中使用命名常量？这些常量要么是宏 ( #define MY_CONST ...) 要么是常量声明 ( const int MY_CONST ...)。前者不起作用，因为预处理器没有扩展宏（ACSL 规范是 C 注释），后者不起作用，因为常量被视为变量，因此某些证明失败。如果我用实际数字替换命名常量，规范就可以正常工作。
有没有人有处理命名常量的好主意？提前致谢
frama-c - 无法通过调用 ocamlyices 函数将插件加载到 frama-c
我正在尝试为 frama-c 开发一个插件。我确实构建了包含多个文件的应用程序，然后创建了makefile引用我需要的所有文件。
我可以使用make然后make install执行插件。当我在函数中调用ocamlyices库中的函数时出现我的问题...
我仍然可以进行 make 和 make install ，当我尝试执行时，出现以下错误：
所以它说当我添加对ocamlyices函数的调用时它是不兼容的。我在某处缺少任何选项/配置吗？
谢谢您的帮助。
最终解决方案如下所示：
变量 $(YICES) 定义为
frama-c - cil 从 vid 获取 varinfo
在旧版本中使用 Frama-c 程序时我有一些问题。它使用函数varinfo_from_vid ()来获取varinfo. 在更改日志中我看到它已被删除，可以使用 varinfo 索引的映射或哈希表来获取它。我不太了解，因为我是 cil 和 frama-c 的新手。这是否意味着我需要自己保留一个 ( vid, varinfo) 哈希表并将其传递给每个使用过的函数variunfo_from_vid()？或者还有其他方法可以做到这一点。如果有人有例子或建议，我将不胜感激。谢谢
frama-c - 如何为字符数组添加注释？
我是 Frama-C 的新手，我一直在寻找一些关于如何为 char 数组编写注释的注释。通常在示例中我看到他们使用整数。所以我不确定我写的是否正确。
我有这个功能：
我写了如下注释，但我不太确定：
frama-c - frama-c mingw __restrict__ 关键字
我是 Frama-C 的新手。我想在 Windows 环境下运行它。我的编译器是 gcc,mingw。
我已经尝试从价值分析教程中运行相同的示例，因为我遇到了库头文件的问题。
我发现由于限制关键字而无法运行 frama-c 。它在 string.h 文件中显示错误
当我手动将 #define限制添加到 SkeinProject 中的所有 *.c 文件时
一切正常。通过手工完成不是我想要的。
下一步是添加参数 -D__restrict__
我还生成了预编译的 *.i 文件，但错误仍然相同。
我能用它做什么？
c - Frama-C：Jessie 插件无法证明按位或安全（wrt 溢出）
我正在使用 Frama-C Nitrogen 来分析以下代码
和
不幸的是，Jessie 无法证明不存在整数溢出。特别是，无法证明以下条件（确保我正确解释了输出，那是哪种语言？我在哪里可以找到手册？）：
通过查看前面的几行，我们还得到：
Jessie 不应该能够在 H23 中推断出更强的属性吗？喜欢
在我看来，杰西将中间结果视为数学整数，因此忽略了无符号字符“提示”。
我还尝试了价值分析：
产生输出：
值分析正确计算了 c 的界限，但我不明白为什么 a 和 b 的结果是近似的（确定它们不应该是微不足道的吗？）
任何见解将不胜感激。
frama-c - 在 Frama-C 中使用影响分析
我尝试使用frama-c-gui并能够执行影响分析但我无法弄清楚我们如何传递需要在 Frama-C 的批处理模式下执行影响分析的语句编号。
c - Frama-C Neon 缺少 C 库文件？
我已经成功编译了 Frama-C Neon (Ubuntu) 以及 Why2、Why3 和 Coq。
在以前的版本（Nitrogen）中，可以通过定义一些符号来选择特定的堆模型，例如：
等等。
Frama-C Neon 用户手册建议包含该文件，share/malloc.c但我找不到它。
- Frama-C Nitrogen 包含
share/malloc.c和share/libc/stdlib.c（包括后者工作正常）； - Frama-C 氟 3
share/stdlib.c仅包含； - Frama-C Fluorine 2 均不含；
- Frama-C Neon 两者都不包含；
此外，Fluorine 3 更改日志列出了“添加缺少的 C 库文件”。
符号是否FRAMA_C_MALLOC_*已弃用，或者 Neon 源分布是否有些不完整？
ocaml - 小牛队的 Frama-C Gui 不起作用
有人在 Mavericks 上安装了 Frama-C 吗？因为不能安装或者不知道怎么安装（Gui版）！
我已经在我的电脑上安装了 ocaml，但是对于 Gui 版本，我需要安装这些库：Gtk、GtkSourceView、GnomeCanvas 和 Lablgtk2。
所以我看到了以前的帖子并做到了：
我在使用 frama-c 制作“make”时遇到问题，即：
我怎么能解决这个问题？
c - 为什么 frama-c 会产生语法错误？
这是一个从一个更大的程序减少的快速测试用例，该程序使用 frama-c NEON 产生语法错误：
frama-c 是否仅限于我在这里违反的 c99 的某个子集？