如何证明Frama-C中整数是有限的

文章/答案/技术大牛

发布

1回答

frama-c

value. assert \is_finite(\add_double(a, b)); 但当我补充说： requires \is_finite(\add_double(a, b)); 然后它会得到未知的状态我觉得我犯了一个非常简单的错误，但我不知道它是什么！

浏览 19提问于2021-04-21得票数 1

回答已采纳

1回答

有什么方法可以丢弃frama-c创建的alt-ergo证明义务吗？

frama-c、alt-ergo

我目前正在使用frama-c，我想看看frama-c是如何对给予证明者(或证明助手)的各种证明义务进行编码的。在本例中，使用alt-ergo组合键。我想知道是否有任何特定的方法可以“转储”给alt-ergo的输入(假设alt-ergo是从frama-c调用的；即不是interop)？我想看看C程序属性的

浏览 15提问于2019-11-16得票数 1

1回答

使用frama-c引理检查无符号整数中的位不起作用

frama-c

使用frama-c时，我正在编写使用位字段来表示集合的代码。然后我想实现一个谓词来检查是否在"myset_t“中设置了一个位。这并没有像预期的那样工作(frama-c和alt-ergo能够证明关于这类集合的东西)，我可以产生一个简单的引理，它已经显示了我的问题。在我的安装(frama-c 21.1 Scandium)上，它不能自动证明以下简单的引理：

浏览 3提问于2020-08-02得票数 1

1回答

Frama-c可湿性粉剂和先决条件

static-analysis、frama-c

关于先决条件和Frama-c wp，我有两个问题：我假设主要功能对此有影响，但这是全貌吗？前提条件是否只有在函数主要时才是证明<

浏览 3提问于2021-03-30得票数 3

回答已采纳

2回答

Frama-C中的非确定值整数模型

frama-c

请告诉我，这是否是Frama中整数和无符号整数的非确定性值的正确模型？#include "/usr/local/share/frama-c/builtin.h" #include "/usr&

浏览 14提问于2015-02-11得票数 3

回答已采纳

1回答

杰茜插件不能证明按位或安全(w.r.t )。溢流)

c、overflow、frama-c、nitrogen、bitwise-or

-jessie test.cH24: integer_of_uint32(result8) = integer_of_uint8(b)H23: 0 <= integer_of_uint8(b) and

浏览 5提问于2014-04-21得票数 2

回答已采纳

1回答

C/frama-c与Spark-ada的等价性

frama-c、spark-ada、spark-2014

我正在研究Frama-c框架，我想知道C/Frama-c和Spark Ada之间是否有等价物。我知道比较这种不同的语言看起来很奇怪，但在阅读了、和一些SPARK的用户手册后，我很难猜测SPARK和C/Frama-c/ACSL是否提供了相同的证明健壮性和相同的代码可靠性。提前感谢您给出您的观点/经验！ PS:我是frama-c的新手，我对SPA

浏览 9提问于2018-05-24得票数 0

1回答

Frama-c，非确定性浮点值

c、frama-c

return x; float x = nondet_float(); some_error();}我希望得到这样的结果:如果x为NaN，则some_error()是可达的。所以我的问题是</

浏览 1提问于2017-09-17得票数 1

1回答

Why3无法通过cygwin在windows上运行验证程序。

frama-c、why3

在Windows环境下，我试图通过cvc4通过Why3使用Frama-c wp插件的Why3验证器。我的系统上安装了frama-c和why3。Wp插件生成与我的why3文件(C源文件具有ACSL规范)对应的.why格式(.why)文件，并使用以下命令： frama-c -wp -wp-print -wp-proof-trace -wp-out当我试图用以swap_Why3_ide.why为证明器的why3来证明生成<

浏览 7提问于2015-04-15得票数 2

回答已采纳

1回答

Frama-C处理无限循环吗？

frama-c

我试图证明变量的值总是增加的。//@ assert count > old_count;} Commit();} 然后我使用命令：frama-c我是不是遗漏了一些非常基本的东西？或者是Frama-C没有处理无限循环？

浏览 2提问于2018-06-25得票数 2

1回答

整数对数使用什么循环不变量？

c、frama-c、formal-verification、loop-invariant、proof-of-correctness

当我使用Frama-C进行C语言正式验证的第一步时，我正在尝试正式验证一个整数二进制对数函数，如下所示：//@ logic integer pow2(integer n) = (n == 0)?+res; }

浏览 18提问于2020-02-11得票数 3

回答已采纳

1回答

验证无无符号整数回绕

frama-c

Frama-c似乎允许无符号整数数学回绕，而它假设有符号整数数学不会溢出，这需要稍后使用-wp-rte标志进行验证。(我个人使用的是Frama-C 20.0钙。)valid_example_struct_one{L}(struct example_struct ex_struct) =*/ 显然，由于无符号整数数学上的回绕，上面的谓词总是正确

浏览 37提问于2020-05-04得票数 1

回答已采纳

1回答

切片时将多个参数传递给C文件

slice、frama-c、program-slicing

我在源代码a.c中的main方法接受两个参数:一个是文件名，另一个是整数。我是这样运行的：但是当我尝试在frama-c中使用切片时 frama-c a.c filename1.txt 3 -slice-......当我输入filename1.txt_3并在代码中单独提取它们时，我也尝试了其他选项，但即使这样，frama-c<

浏览 1提问于2014-10-07得票数 0

1回答

如何在coq中证明why3生成的脚本？

coq、frama-c、coqide、why3

我使用frama-C WP，并希望调试我的ACSL注释(以理解为什么验证者说我“不知道”)。我有一些绿色或橙色的结果。我打开why3集成开发环境，看到生成的脚本。我想在Coq IDE中使用生成的代码。我看到一些公理，然后是定理WP，然后，举个例子：x当我在Coq中“转到末尾”时，我看到一个错误“试图保存不完整的<

浏览 2提问于2017-08-26得票数 2

1回答

如何断言一个点是不可到达的？

c、frama-c、acsl

对于Frama和WP插件，用户如何断言程序中的某个点是不可到达的？//@ assert \unreachable;

浏览 4提问于2022-09-27得票数 1

1回答

无法证明assign子句-Frama C

frama-c

我是Frama-c的新手，我想知道这个简单的例子有什么问题：@ ensures \forall integer k;variant length - i; for(int i = 0; i < length; i++){ }在这个例子中，Frama-c (WP + Value)不能证明</em

浏览 0提问于2013-05-23得票数 4

回答已采纳

1回答

Frama-c无法证明指针比较的事实

frama-c

assert(p <= q-1);void g(int a, int b) assert(a <= b-1);使用alt-ergo，frama-c成功地证明了g()中的断言成立，但未能证明与f()相同。

浏览 29提问于2018-08-14得票数 1

回答已采纳

2回答

Frama-c执行时间和堆内存界限证明

frama-c

Frama-C是否提供了任何工具来证明函数的运行时特征，例如执行时间(可能是指令计数)和堆内存空间(计数为分配的字节)？

浏览 7提问于2018-06-10得票数 0

1回答

Frama-C中局部变量的赋值子句

frama-c

我正在尝试使用frama-c验证下面的代码 *p = 8;//@ assigns \nothing; int *p = new_value(); } prover无法证明main赋值\ not，这是合理的，因为main通过函数f分配给*p。但是，由于p是局部变量，不能在注释中访问，所以我应该如何声明in \assigns子句。

浏览 4提问于2014-10-27得票数 5

回答已采纳

2回答

依赖无符号整数溢出的代码的校对？

frama-c、alt-ergo

我应该如何像下面这样的方法来证明代码的正确性，为了避免一些低效率，它依赖于模块化算法？int“模型，但是，如果我正确理解，该模型将配置POs中逻辑整数的语义，而不是C代码的正式模型。在这种情况下，我是否可以添加注释，规定语句或基本块的逻辑模型，这样我就可以告诉Frama特定编译器是如何实际解释语句的？如果是这样的话，我可以使用其他的验证技术，比如

浏览 2提问于2013-08-02得票数 5

回答已采纳

点击加载更多