我无法证明2个循环不变量:
loop invariant \forall integer i; 0 <= i < (\at(n, Pre) - n) ==> ((char*)m2)[i] == \at(((char*)m1)[i], Pre);
loop invariant \forall integer i; 0 <= i < (\at(n, Pre) - n) ==> ((char*)m1)[i] == \at(((char*)m2)[i], Pre);
我猜测\对于阵列不起作用,正如我所料.
ACSL by Example(第68页,swap_ranges)中有一个类似的函数,它使用了这个函数,但是如上所述,它们无法用WP插件证明这个特定的函数.我在我的机器上试过它,实际上它无法证明相同的不变量.
完整代码
/*
* memswap()
*
* Swaps the contents of two nonoverlapping memory areas.
* This really could be done faster...
*/
#include "string.h"
/*@
requires n >= 1;
requires \valid(((char*)m1)+(0..n-1));
requires \valid(((char*)m2)+(0..n-1));
requires \separated(((char*)m1)+(0..n-1), ((char*)m2)+(0..n-1));
assigns ((char*)m1)[0..n-1]; …我不太了解slevelFramaC中的选项.任何人都可以解释更多关于如何与slevel用户断言(例如//@assert ...;)或状态相关的价值,以及导致状态数量上升的因素有哪些？
例如,我有一个程序,它不包含循环,但包含if..else分支,go to语句,并且在程序的某些点上也有一些用户断言,例如:
...
a = Frama_C_unsigned_int_interval(0, 100);
//@ assert a == 0 || a == 1 || a == 2 || a == 3 || ... || a == 100;
...
b = Frama_C_unsigned_int_interval(a, 200);
//@ assert b == 0 || b == 1 || b == 2 || b == 3 || ... || b == 200;
...在分析的输出中(我设置slevel为~100000),可能有一些像:Semantic level unrolling superposing up to …
我试图在Windows 7上运行Frama-C,但它没有用.
我已经阅读了你在这里写的所有提示和评论,但仍然没有用.
能有人解释安装过程是一种清晰简单的方法,我会感激不尽？
我是 Frama-C 的新手，我正在尝试验证 C 代码。该代码非常基本，但不知何故我无法验证它。
\n总之，我试图证明该函数或循环是否曾经运行过。为此，我在开始时为变量指定了一个值 (4)。在函数中，我将值更改为“5”，并且我尝试确保变量5位于末尾。
\n代码：
\n#include <stdio.h>\nint x=4;\n/*@\nensures x ==5;\n*/\nint abs(int val){\n\n int accept=0;\n int count=3;\n /*@\n loop invariant 0 <= count <= \\at(count, Pre);\n loop assigns accept,x,count; \n loop variant count;\n */\n while (count !=0){\n x=5;\n accept =1;\n count--;\n }\n return x;\n }\n我向 CLI 发出命令“frama-c-gui -wp -rte testp4.c”来启动 frama-c。
\n结果：\n Frama-1
\n但“*@ 确保 x \xe2\x89\xa1 5; */” 仍然未知。
\n有人可以帮我解决这个问题吗？如果我"x=5;"在 while 循环之外（返回之前）它会验证/*@ ensures x …
在frama-C中,当我加载源文件时,它会进行预处理,并执行自动纠错,如"自动类型转换",如下所示(int被类型化为浮动).
现在,我如何才能看到预处理后所做的所有更改.
是否有任何方法或日志文件或警告消息显示frama-c所做的所有更改.这是我的源代码:
int main() {
int a, b;
printf("Input two integers to divide\n");
scanf("%d%d", &a, &b);
printf("%d/%d = %.2f\n", a, b, a/(float)b);
}
这是我的frama-C预处理代码:
extern int (/* missing proto */ printf)();
extern int (/* missing proto */ scanf)();
int main(void) {
int a;
int b;
int __retres;
printf("Input two integers to divide\n");
scanf("%d%d", &a, &b);
printf("%d/%d = %.2f\n", a, b, (float)a/(float)b);
__retres =0;
return (__retres);
}
当我试图在Frama-c中运行我的简单代码时,我遇到了一些问题.我正在尝试创建一个指向数组结构的有效指针,并从我的函数返回此指针Stack_init.我不明白为什么Frama-c会返回此错误并且不能证明我的功能:
[kernel] preprocessing with "gcc -C -E -I. /home/federico/Desktop/simple_main_v2.c"
[kernel] warning: Neither code nor specification for function malloc, generating default assigns from the prototype
[wp] Collecting axiomatic usage
[wp] warning: Missing RTE guards
Desktop/simple_main_v2.c:28:[wp] warning: Cast with incompatible pointers types (source: sint8*) (target: sint32*)
[wp] 0 goal scheduled
我的目的是创建一个函数,返回一个没有前置条件的指针,后置条件是指针有效.
有人可以帮我理解我的错误在哪里吗？
/*
create_stack
Inputs: none
Outputs: S (a stack)
Preconditions: none
Postconditions: S is defined and empty
*/
/*@
ensures \valid(\result) && \result[0] == 0;
*/
int *Stack_Init()
{ …我有我的测试代码(研究WP循环不变量),它在数组单元格中添加两个长整数,每个数字的表示形式:
int main(int argc, const char * argv[]) {
char a[32], b[32];//size can be very big
memset(a, 0, sizeof(a));
memset(b, 0, sizeof(b));
scanf("%s %s", a, b);
unsigned int size1 = strlen(a);
unsigned int size2 = strlen(b);
//code to reverse a string. currently proved
reverse(a, size1);
reverse(b, size2);
for (unsigned int i = 0; i < size1; i++) a[i]-='0'; //move from chars to integers
for (unsigned int j = 0; j < size2; j++) b[j]-='0';
unsigned int maxsize = size1;
if …在以下示例代码中:
void kernel(int ni, int nj, int nk, float alpha, float *tmp, float *A, float *B) {
int i, j, k;
for (i = 0; i < ni; i++) {
for (j = 0; j < nj; j++) {
tmp[i * nj + j] = 0.0f;
for (k = 0; k < nk; ++k) {
tmp[i * nj + j] += alpha * A[i * nk + k] * B[k * nj + j];
}
}
}
}
我试图获得} …
我想探索Frama-C以应用基于断言的切片(使用ACSL表示法).我发现有几种不同版本的Frama-C具有一些不同的功能.我的问题是哪个版本最适合为Frama-C开发一个切片插件并操纵Frama-C创建的AST.