标签: frama-c

我在将frama-c看作是在OCaml中处理C头文件的一种方法(例如,用于生成语言绑定).它很有吸引力,因为它看起来像是一个记录良好且维护良好的项目.然而,经过大量的谷歌搜索和搜索文档后,我找不到任何适合此目的的东西.我只是错过了正确的方法,或者它是否超出了frama-c的范围？与其他一些插件相比,它似乎是一件相当简单的事情.

这是我的例子:

int in;
int sum(int n){
    int log_input = n;
    int log_global = in;
    return 0;
}

int main(){
    int n = Frama_C_interval(-10, 10);
    in = n;
    if (n > 0){
        sum(n + 4);
    }
    return 0;
}

我想要做的是在main中初始化时找到输入变量n的范围,从而得到函数sum.此示例中的正确范围是[1,10].

在示例中,我想将原始输入"保存"在全局值中,并通过将其分配到变量log_global中来重新引入它,从而发现导致到达函数的原始输入.在此示例上运行frama-c时,我们得到log_input的范围是[5,14],log_global的范围是[-10,10].我理解为什么会发生这种情况 - in的值设置在main的开头,并且不受对n的进一步操作的影响.

我想知道在frama-c中是否有一种简单的方法可以改变它？也许是对frama-c代码的一个简单修改？

我有一个不相关的想法是操纵main中的if语句:

if (in > 0){
    sum(in + 4);
}

我使用全局变量而不是n.这确实产生了正确的范围,但是这种解决方案不能很好地扩展到更复杂的功能和更深的调用堆栈.

我想用 Frama-c 和 WP 插件来表示，下面编写的 stringCompare 函数充当“它应该”的作用 - 即：给定相同的输入字符串，该函数返回 0 并且结果不同于 0如果字符串不相同。我已经注释了如下所示的相关函数，并希望能够证明 WP 生成的未经证实的目标，这怎么做？

我通过尝试运行带有注释的插件获得的输出可以在代码下方看到

#include <string.h>
#include <stdio.h>

/*@  
    requires validPointers: \valid_read(s1) && \valid_read(s2) ;
    requires validLengthS1: 100 >= strlen(s1) >= 0;
    requires validLengthS2: 100 >= strlen(s2) >= 0;
    assigns \nothing ;
    allocates \nothing ;  
    frees \nothing ;
    behavior allEqual:
        assumes \forall integer k; 0 <= k < n ==> s1[k] == s2[k];
        ensures \result == 0;
    behavior SomeDifferent:
        assumes \exists integer k; 0 <= k < n ==> …

我想知道是否可以使用 Frama-C 进行某种前向条件切片，并且我正在使用一些示例来了解如何实现这一目标。

我有一个简单的例子，它似乎导致切片不精确，我不明白为什么。这是我想要切片的函数：

int f(int a){\nint x;\nif(a == 0)\n    x = 0;\nelse if(a != 0)\n    x = 1;\nreturn x;\n}\n

如果我使用这个规范：

/*@ requires a == 0;\n  @ ensures \\old(a) == a;\n  @ ensures \\result == 0;\n*/\n

然后 Frama-C 使用“f -slice-return”标准和 f 作为入口点返回以下切片（这是精确的）：

/*@ ensures \\result \xe2\x89\xa1 0; */\nint f(void){\n  int x;\n  x = 0;\n  return x;\n}\n

但是当使用这个规范时：

/*@ requires a != 0;\n  @ ensures \\old(a) == a;\n  @ ensures \\result == 1;\n*/\n …

我正在尝试使用Frama-C来验证包含动态内存分配的C代码的安全属性.当前版本的ACSL规范语言(1.8)似乎能够表达很多关于动态分配的内存.但是,大部分内容尚未在Frama-C Neon中实现.

假设我们采用以下代码片段:

#include <stdlib.h>

/*@ requires \valid(p) && \valid(q) && \separated(p, q);
  @ ensures \valid(q);
  @*/
void test(char *p, char *q) {
  free(p);
}

int main(void) {
  char *p = (char *) malloc(10);
  char *q = (char *) malloc(10);

  test(p, q);

  return 0;
}

因此,main分配两块内存,并将指针传递给它们进行功能测试.测试释放p指向的块,但不释放q指向的块.假设我想证明在测试结束时,指针q仍然有效.我该怎么办？

似乎我必须自己建模堆:axiomatize一些谓词谈论堆,并使用它们来指定malloc和free,模仿ACSL的未实现部分.最简单的方法是什么,以便我可以验证上面的例子？

我正在尝试使用frama-c验证以下代码

/*@ ensures \result != \null; 
  @ assigns \nothing;
  @*/
extern int *new_value();

//@ assigns *p;
void f(int* p){
  *p = 8;
}
//@ assigns \nothing;
int main(void){
 int *p = new_value(); 
 f(p);
}

证明者无法证明主要指定\没有,这是有道理的,因为主要通过函数f分配给*p .但是,我应该如何在\ assigns子句中声明,因为p是局部变量,并且无法在注释中访问.

我正在尝试创建一个frama-c插件.这个插件取决于Frama-c Value插件.我想获取并打印C源代码中所有左值的值集.为了做到这一点,我想使用Value.Eval_exprs,Value.Eval_op等中可用的函数Eval_exprs.lval_to_precise_loc.

不幸的是我无法找到在我的插件中使用这些功能的方法.我尝试按照Frama-c插件开发指南的4.10.1节(通过.mli文件注册)中提到的步骤添加PLUGIN_DEPENDENCIES:=Value到我的Makefile中,但我注意到该Value.mli文件为空,并且没有通过此文件公开任何功能.之后我查看db.ml了kernel目录中的文件,找不到任何可用于访问Eval_exprs,Eval_op等中可用功能的模块.

有没有办法从其他插件访问Value插件的这些功能？

我需要使用frama-c值分析插件来分析一些项目。这些项目使用 CMake 构建基础设施作为它们的构建系统。

我使用 frama-c 分别分析每个文件。这样，入口点的信息就会丢失。更准确地说，frama-c 需要一个不包含“main”函数的文件的入口点，因此覆盖所有函数并在项目的单个文件中选择最佳入口点是一项挑战。

我的问题是，有没有一种方法可以将整个项目作为一个整体（而不是逐个文件）运行 frama-c ？

我对 Frama-C 18.0 版（Argon）的行为有些困惑。

鉴于以下程序：

#include <assert.h>
#include <limits.h>


/*@ requires order: min <= max;
    assigns \result \from min, max;
    ensures result_bounded: min <= \result <= max ;
 */
extern int Frama_C_interval(int min, int max);


int main() {

  int i,j;

  i = Frama_C_interval(INT_MIN, INT_MAX);

  j = i;

  assert(j == i);

  return 0;
}

我希望可以很容易地用任何跟踪平等的抽象域来证明这个断言。但是，调用

框架-c -eva -eva-equality-domain -eva-polka-equalities foo.c

给出：

[eva] Warning: The Apron domains binding is experimental.
[kernel] Parsing stupid_test.c (with preprocessing)
[eva] Analyzing a complete application starting at …

在查看代码库时，我发现了一段特定的代码，它触发了关于“越界访问”的警告。查看代码后，我看不到报告访问的发生方式 - 并试图最小化代码以创建可重现的示例。然后，我使用我可以访问的两个商业静态分析器以及开源 Frama-C 检查了这个示例。

他们三个人都看到相同的“越界”访问权限。

我不。我们来看一下：

 3  extern int checker(int id);
 4  extern int checker2(int id);
 5  
 6  int compute(int *q)
 7  {
 8      int res = 0, status;
 9  
10      status = checker2(12);
11      if (!status) {
12          status = 1;
13          *q = 2;
14          for(int i=0; i<2 && 0!=status; i++) {
15              if (checker(i)) {
16                  res = i;
17                  status=checker2(i);
18              }
19          }
20      }
21      if (!status)
22          *q = res;
23      return …