在__e_acsl_assert文件中没有为所有给定的断言添加.i

Question

我对Frama很陌生。我特别需要使用e插件进行验证.我使用了first.i .i文件作为

int main(void) {

int x = 0;

/∗@ assert x == 0; ∗/

/∗@ assert x == 1; ∗/

return 0;

}

使用以下命令从first.i文件创建monitored_first.c文件。

$ frama-c -e-acsl first.i -then-last -print -ocode monitored_first.c

monitored_first.c中的主要函数如下所示。

int main(void)
{
  int __retres;
  __e_acsl_memory_init((int *)0,(char ***)0,8UL);
  int x = 0;
  __retres = 0;
  __e_acsl_memory_clean();
  return __retres;
}

它不是为e_acsl添加x==1断言。

我使用"e-acsl-gcc.sh“脚本进行了尝试，该脚本生成monitored_first.i文件。但monitored_first.i内部的主要功能与monitored_first.c中的相同。

$ e-acsl-gcc.sh -c -omonitored_first.i first.i

上面的命令生成两个可执行文件，“a.out.e-asl”和"a.out“。在ubuntu22.04中运行时，它还会生成以下警告：

 /home/amrutha/.opam/4.11.1/bin/frama-c -remove-unused-specified-functions -machdep gcc_x86_64 '-cpp-extra-args= -std=c99 -D_DEFAULT_SOURCE -D__NO_CTYPE -D__FC_MACHDEP_X86_64 ' -no-frama-c-stdlib first.i -e-acsl -e-acsl-share=/home/amrutha/.opam/4.11.1/bin/../share/frama-c/e-acsl -then-last -print -ocode monitored_first.i
[kernel] Parsing first.i (no preprocessing)
[e-acsl] beginning translation.
[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing)
/tmp/ppannot15ad34.c:362: warning: "__STDC_IEC_60559_BFP__" redefined
  362 | #define __STDC_IEC_60559_BFP__ 201404L
      | 
In file included from <command-line>:
/usr/include/stdc-predef.h:39: note: this is the location of the previous definition
   39 | #  define __STDC_IEC_60559_BFP__        201404L
      | 
/tmp/ppannot15ad34.c:363: warning: "__STDC_IEC_60559_COMPLEX__" redefined
  363 | #define __STDC_IEC_60559_COMPLEX__ 201404L
      | 
In file included from <command-line>:
/usr/include/stdc-predef.h:49: note: this is the location of the previous definition
   49 | #  define __STDC_IEC_60559_COMPLEX__    201404L
      | 
[e-acsl] translation done in project "e-acsl".
+ gcc -std=c99 -m64 -g -O2 -fno-builtin -fno-merge-constants -Wall -Wno-long-long -Wno-attributes -Wno-nonnull -Wno-undef -Wno-unused -Wno-unused-function -Wno-unused-result -Wno-unused-value -Wno-unused-function -Wno-unused-variable -Wno-unused-but-set-variable -Wno-implicit-function-declaration -Wno-empty-body first.i -o a.out
+ gcc -DE_ACSL_SEGMENT_MMODEL -std=c99 -m64 -g -O2 -fno-builtin -fno-merge-constants -Wall -Wno-long-long -Wno-attributes -Wno-nonnull -Wno-undef -Wno-unused -Wno-unused-function -Wno-unused-result -Wno-unused-value -Wno-unused-function -Wno-unused-variable -Wno-unused-but-set-variable -Wno-implicit-function-declaration -Wno-empty-body -I/home/amrutha/.opam/4.11.1/bin/../share/frama-c/e-acsl -o a.out.e-acsl monitored_first.i /home/amrutha/.opam/4.11.1/bin/../share/frama-c/e-acsl/e_acsl_rtl.c /home/amrutha/.opam/4.11.1/bin/../lib/frama-c/e-acsl/libeacsl-dlmalloc.a -lgmp -lm

在ubuntu20.04中没有任何警告，只有结束部分被显示。当运行./a.out.e-acsl时，它只是运行代码而没有任何消息，这是不应该的。预期的输出应该如下所示：

$ ./a.out.e-acsl
first.i: In function 'main'
first.i:4: Error: Assertion failed:
The failing predicate is:
x == 1.
Aborted (core dumped)
$ echo $?
134

我在ubuntu22.04中试用了opam版本2.1.2和Fragma-C25.0

和ubuntu 20.04与opam版本2.0.5和Fragma-C 25.0

Answer 1

同样的问题已经发布到Frama-C的公共bug跟踪上，原因似乎是ACSL注释中使用的非ASCII星号字符：∗而不是*。

我仍然不明白注释是如何解析的(我的编译器给出了语法错误)，但是用户似乎表示替换它们解决了问题。

无论如何，在类似的情况下，您可以使用Frama-C GUI打开解析的文件并检查Frama-C是否识别ACSL注释(它们应该出现在CIL规范化代码中)，或者尝试其他分析，例如运行frama-c -eva并检查它是否检测到注释。