了解FRAMA-C切片器结果
我想知道是否有可能使用Frama-C进行某种正向条件切片，我正在使用一些示例来了解如何实现这一点。 我有一个简单的例子，它似乎导致了不精确的切片，我不明白为什么。下面是我要分割的函数： int f(int a){ int x; if(a == 0) x = 0; else if(a != 0) x = 1; return x; } 如果我使用此规范： /*@
..
frama-c相关内容
将WhyML映射到SMT逻辑的确切机制
您好，自动扣款和验证黑客！ 为了更深入地了解 WhyML 如何为 ACSL 注释的 C 程序提供证明，我尝试手动“重现"Why3 对WhyML 程序所做的工作，同时将其转换为SMT 逻辑并将其提供给Z3 证明器. 假设我们有以下 C 片段: const int L = 3;int a[L] = {0};int i = 0;而 (i
..
Frama-C anagram 函数行为验证
我写了一个 C 函数来检查两个给定的字符串(C 风格)是否是字谜.我尝试用 Frama-C 验证它，但它无法验证函数的最终行为(其他规范有效).第一个进入超时(即使 WP 中的超时值非常高)，第二个是未知的. 代码如下: #include //@幽灵字符字母表[26] = {'a', 'b', 'c', 'd', 'e', 'f', 'g', 'h', 'i', 'j', 'k', 'l
..
使用 Frama-C 检查 C 代码的无效内存访问
我得到了这个 C 代码(代码的细节，包括可能的错误，不是很相关): int read_leb128(char **ptr, char *end) {整数 r = 0;整数 s = 0;字符 b;做 {if ((intptr_t)*ptr >= (intptr_t)end) (exit(1));b = *(*ptr)++;r += (b & (char)0x7f)
..
如何使用frama-c命令处理printf(& quot;和)和scanf(& amp;")?
我正在使用此代码生成C程序的控制流程图.对于除 printf 和 scanf 之类的内置功能以外的所有功能，它都可以正常工作.我可以在此代码中进行哪些更改以按原样输出内置函数? 打开Cil打开Cil_types放出print_stmt =功能|指令->！Ast_printer.d_instr我|返回_->Format.pp_print_string out“"|转到 _ ->F
..
用Frama-C分析一个简单的C ++程序
我从一个很棒的教程开始学习C ++，该教程位于 https://learnxinyminutes.com/docs/c++/，并希望在Frama-C中分析一个显示引用的最简单示例: 使用命名空间std;#include#includeint main(){字符串foo =“我是foo"；string bar =“我是酒吧";弦&fooRef = foo;/
..
如何在Frama-C中使用真实公理证明代码
我已从ACSL-by-Example的“内部产品"代码中将int类型更改为float(具有int类型的代码对我有用)，现在我无法证明循环不变式inner.我为inf和NaN添加了一些检查，但没有成功. #include "limits.h" /*@ predicate Unchanged{K,L}(float* a, integer first, integer last) =
..
具有Frama-C和Eva的动态阵列
在 https://stackoverflow.com/a/57116260/946226 中，我学习了如何验证功能 foo 在缓冲区上运行（由开始和结束指针给定）实际上只能读取它，但是会创建一个代表性的 main 调用它的函数： #include ＃定义N 100 字符测试[N]; extern char * foo（char *，char *）;
..
尽管有确凿的论断，但SMT证明者的产量仍然“未知"
假设我们有以下带有C注释的代码: #define L 3 int a[L] = {0}; /*@ requires \valid(a+(0..(L - 1))); ensures \forall int j; 0 (a[j] == j); */ int main() { int i = 0; /*@ loop assigns
..
ACSL后置条件中\ old的含义
我是Frama-C的新手用户，并且对断言有一些疑问 指针上方. 考虑以下涉及的C片段: 两个相关的数据结构Data and Handle，s.t.句柄有一个指向数据的指针； 数据中的“状态"字段，指示某些假设操作是否已完成 三个功能:init()，start_operation()和wait(); 使用上述方法的main()函数，其中包含6个断言(A1-A6) 现在，为什么
..
Frama-C:获取语句的值
我想开发一个Frama-C-Plugin，在其中获取当前语句的值. 借助此帖子 Frama-C插件开发:获得价值分析的结果我能够打印语句的值，但是指针并未以我需要的方式显示. 借助注释，我能够打印整个状态(不仅是语句的变量). 我可以结合这两个:获取语句的变量，但也可以使用取消引用的指针(值)吗? 例如，在语句x=1之后打印非指针将导致x -> {{ NULL -> {1}
..
如何在另一个插件中使用WP的结果?
我正在编写一个Frama-C插件，我想知道是否有可能从我的插件中使用WP获得最弱的先决条件，如果可以，那么到底是什么?过去，例如，我曾使用Db.Value在自己的插件中使用EVA插件的结果.是否有类似于WP的Db.Value的东西? 解决方案 WP插件在WP.mli文件中公开其API，该文件是通过收集组成Wp的更高级别模块的接口而生成的.您可以在src/plugins/wp/Wp.mli中
..
如何在Frama-c Value插件的Value.Eval_expr，Value.Eval_op等模块中使用函数
我正在尝试创建frama-c插件.该插件取决于Frama-c Value插件.我想在C源代码中获取并打印所有左值的值集.为此，我想使用Value.Eval_exprs，Value.Eval_op等可用的函数，例如Eval_exprs.lval_to_precise_loc. 不幸的是，我无法找到一种在插件中使用这些功能的方法.我尝试遵循Frama-c插件开发指南的4.10.1节(通过.mli
..
Frama-C插件开发:获得价值分析的结果
我正在使用Value-analysis开发适用于Frama-C的插件. 我只是想在每个语句后打印变量(值)的状态(我认为解决方案很简单，但我无法弄清楚). 我在访问者的vstmt_aux方法中使用Db.Value.get_stmt_state来获取当前状态. 现在如何获取变量的值? PS:我找到了这篇文章，但是它没有帮助，没有真正的解决方案，在描述的帮助下，我无法做到这一点: 解
..
如何用frama-c命令处理printf（""）和scanf（""）？
我使用这段代码来生成一个C程序的控制流图。除了内置函数（如 printf 和 scanf ）外，它对所有函数都可以正常工作。我可以在这段代码中更改以输出内置函数吗？ 打开Cil 打开Cil_types 让print_stmt出= 函数 | Instr i - > ！Ast_printer.d_instr out |返回_ - > Format.pp_print_string
..
什么是这是由邮资-C产生的圆节点的PDGS意义
我用的邮资-C的工具来分析下面的code。 INT主（INT ARGC，CHAR *的argv []） { INT I，一; 对于（I = 0; I＆小于100; I + = 1） { 一个= 0; 如果（A == 0） { 继续; } 其他
..