我想查询Frama-C中的值分析插件以获取其值的说明.对于每个数组,它返回整个数组的值范围.例如,如果指令是array[i] = 1;,我从值分析插件得到result = {1}for array[i].现在,例如array[i],我想i从值分析中获取变量名称及其值.
下面是我的代码示例
class print_VA_result out = object
inherit Visitor.frama_c_inplace
(**..*)
method vstmt_aux s =
if Db.Value.is_computed () then
match s.skind with
| Instr i ->
begin
match i with
| Set(lval,_,_) ->
print_value lval s
|_ -> "<>"
...
有人可以帮我这个吗？非常感谢提前.
如何在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的氮版本,但是"请以root身份解压缩归档文件"要求我执行不可能的操作.我没有root帐户,永远不会给一个(这些机器都属于大学).完全可以在任何你喜欢的地方安装gcc和clang; 为什么Frama-C想要进/？
我再次对一个简单的验证工作感到困惑,这一次是在使用WP插件的Frama-C(Sodium)中,因为我无法让Jessie在uni工作站上工作(在由管理人员/团队安装的过程中) .)我一直在阅读'ACSL by example'和手册.虽然我认为这个例子很简单,但很快就能正确行事.在使用Dafny和Whiley验证相同的算法后,我可能会变得有点污点.
#include <stdio.h>
// A linear search over a sorted array looking for a given element.
/*@ requires len > 0;
@ requires \valid( ls+ ( 0..(len - 1) ) );
@ requires \forall size_t k; 0 <= k < (len - 1) ==> ls[k] <= ls[k + 1];
@ assigns \nothing;
@ behavior found:
@ assumes \exists size_t k; 0 <= k < len && ls[k] == item;
@ ensures \result >= 0;
@ behavior nfound: …如何frama-c -wp从wp手册验证示例- 一个简单的swap函数(swap.c):
/* @ requires \valid(a) && \valid(b);
@ ensures A: *a == \old(*b);
@ ensures B: *b == \old(*a);
@ assigns *a,*b;
@*/
void swap(int * a, int * b);
void swap(int * a, int * b) {
int tmp = * a;
*a = *b;
*b = tmp;
return ;
}
调用
$ frama -c -wp -wp-rte swap.c
得到:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing swap.c (with preprocessing)
[wp] Running …有没有一种方法可以使用Frama-Cslicing插件为特定的C assert语句计算切片？
例如，给出以下代码：
int main() {
double a=3;
double b=4;
double c=123;
assert(b>=0);
double d=a/b;
c=a;
return 0;
}
我想得到以下切片assert(b>=0);：
int main() {
double b=4;
assert(b>=0);
return 0;
}
我正在使用价值分析为Frama-C制作插件.我只想在每个语句之后打印变量(值)的状态(我认为解决方案很容易安静,但我无法弄明白).
我在访问者Db.Value.get_stmt_state的vstmt_aux方法中获得了当前状态.
我现在如何获得变量的值？
PS:我发现这篇文章,但它没有帮助,没有真正的解决方案,并且在描述的帮助下我无法做到: 如何在Value.Eval_expr,Value.Eval_op等模块中使用函数Frama-c Value插件
我是一名学生，目前正在尝试使用 cppcheck 和 frama-c 分析 C 中 OPC Ua 协议的参考实现。我的目标不是进行非常专门的测试，而是进行一些通用/基本测试，以查看代码是否存在一些明显问题。
该项目可以在这里找到
我正在使用 Ubuntu 19.10 和 Frama-C 版本 20.0 (Calcium) 运行 VM。
我执行的步骤如下：
git clone https://github.com/open62541/open62541.git
cmake -DCMAKE_EXPORT_COMPILE_COMMANDS=1 /path/to/source
frama-c -json-compilation-database /path/to/compile_commands.json
到目前为止，一切都按预期工作，没有错误。
但是现在我无法理解如何继续。我是否需要单独对所有文件进行分析，还是可以像使用 cppcheck 一样投入整个项目？
一般来说，我将如何处理这个问题？我是否需要逐步分析所有文件？
例如我试过：
frama-c -json-compilation-database /path/to/compilation_commands.json -val /path/to/open62541/src/
返回：
[kernel] Parsing src (with preprocessing)
gcc: warning: /path/to/open62541/src/: linker input file unused because linking not done
[kernel] User Error: cannot find entry point `main'.
Please use option `-main' for specifying a valid entry point.
[kernel] …我正在尝试使用 Frama-c 测试一个函数：
/*@
ensures \result >= x && \result >= y;
ensures \result == x || \result == y;
*/
int max( int x, int y){
return (x>y) ? x : y;
}
安装完所有要求后：OPAM、why3、alt-ergo 每当我执行frama-c -wp fct.c我收到：
[kernel] Parsing fct.c (with preprocessing)
[wp] Warning: Missing RTE guards
[wp] User Error: Prover 'alt-ergo' not found in why3.conf
[wp] Goal typed_max_ensures : not tried
[wp] Goal typed_max_ensures_2 : not tried
[wp] User Error: Deferred error message was emitted during …我正在使用Frama-C来计算C程序的一部分.我希望切片程序看起来像没有代码转换的原始程序.但是在生成的切片中,我总是有goto语句和标签.我使用命令:
frama-c -no-simplify-cfg -main test -slice-assert test test.c -then-on 'Slicing export' -print -ocode result.c
我在Cygwin的Windows机器上从最新的Oxygen版本编译了Frama-C.
使用Cil_datatypesFrama-C API中定义的模块,我试图用谓词(Cil_datatype)中的新术语替换术语(Cil_datatype).要做到这一点,我需要使用一个函数映射一个谓词,当它找到术语(或术语)替换它时.如何映射谓词来替换术语？