frama-c 相关问题

Frama-C是一个专门用于分析C源代码的开源工具套件。

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

[当我开始使用Frama-C进行C形式验证时，我试图正式验证如下编写的整数二进制对数函数：// @逻辑整数pow2（integer n）=（n == .. 。

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

回答 1 投票 2

如何使用Frama-C将变量类型保存到文件中

我正在尝试使用Frama-C在C程序中打印变量类型。我发现该信息在GUI中表示，如下图所示。但是，我找不到输出此内容的方法...

c static-analysis frama-c

回答 1 投票 1

为什么Frama-C v20.0钙不支持在非全局范围内重新定义typedef

我正在尝试分析以下C程序：#include typedef struct a {int x;字符}别名； int main（）{typedef struct b {int x;诠释} ...

c frama-c

回答 1 投票 0

ACSL逻辑结构声明不按参考手册的规定工作

我想有一种方法来描述包含抽象列表的逻辑/规范级别的结构。《 ACSL参考手册》第27页的示例2.2.7提出了一种解决方法，它是...

frama-c acsl

回答 1 投票 1

使用frama-c的递归Quicksort的形式证明

[作为作业，我决定尝试使用带有wp和rte插件的frama-c验证quicksort的实现（从此处获取并改编）。请注意，第一个最左端为0，最右端等于...

sorting quicksort frama-c formal-verification proof-of-correctness

回答 1 投票 3

Frama-c：如何使用va_list和va_arg证明可变参数的理由？

[当前，我使用的是Frama-C 19版，并在各种参数上苦苦挣扎。例如）#include #include void vars2（int n，va_list args）{for（...

variadic-functions specifications frama-c formal-verification preconditions

回答 1 投票 0

执行Frama-C中原始代码的死代码消除/切片

编辑：原始问题有不必要的细节，我有一个我在Frama-C中进行值分析的源文件，一些代码在标准化窗口中突出显示为死代码，没有原始代码...

frama-c

回答 2 投票 1

ACSL的函数证明，它检查数组是按升序还是降序排序

我正试图证明检查数组是按升序还是降序排序的函数的正确性。如果按降序排序，则行为是返回-1，如果...

c sorting frama-c formal-verification acsl

回答 1 投票 2

是否有任何方法可以转储frama-c创建的alt-ergo证明义务？

我目前正在与frama-c一起玩耍，我希望了解frama-c如何编码提供给证明者（或证明助手）的各种证明义务。在这种情况下，为alt-ergo。我是...

frama-c alt-ergo

回答 1 投票 1

在WP插件手柄工会和可以键入双关语？

我有一个双关类型例如工作，我想知道，如果WP或其他插件可以处理这个问题。到目前为止，我真的无法找到WP和工会什么，但他们似乎得到支持。这里是一个...

frama-c

回答 1 投票 1

为什么Frama-c的Eva插件在实际找到断言的反例时返回未知

我试图在函数内插入一个断言。这是我做的：void foo（int a）{// @ assert a == 1; } void main（）{foo（1）; FOO（2）;我希望得到一个无效的结果，但......

frama-c

回答 1 投票 3

EVA插件：如何通过temp变量检查“temp =（volatile unsigned short *）add”中的添加值

我试图通过以下示例中的temp变量检查“temp =（volatile unsigned short *）add”中的添加值：main（）{unsigned short add = 0x01; unsigned short val = ...

c frama-c

回答 1 投票 0

WP生成的Coq文件无法编译

我已经通过opam安装了frama-c（18.0）和coqide（8.9）（当然还有其他所需的依赖项，但这可能不是问题）。好吧，关键是我只是通过opam安装它，而不是......

coq frama-c

回答 1 投票 2

强制执行Frama-C中WP内存模型的假设

有没有办法强制执行WP内存模型的假设？考虑使用Frama-C验证以下两个函数：/ * @ requires \ valid（a）&& \ valid（b）; @确保A：* a = ......

frama-c

回答 1 投票 1

我可以跳过eva关于签名溢出的断言吗？

示例代码：void main（）{unsigned int x; x = 1U << 31; // OK x = 1 << 31; //签署溢出的回报; } frama-c-gui -eva main.c：void main（void）{unsigned int x; ...

frama-c

回答 1 投票 0

寻找在frama-c期间覆盖函数的想法

我正在寻找如何在不修改源代码的情况下覆盖函数的想法。就像我在原始源中有foo（）一样，我想用我自己的版本用相同的函数名覆盖它...

frama-c

回答 1 投票 1

当Eva没有报告任何错误时，如何将-werror错误与代码问题相关联？

Frama-C werror插件（https://github.com/sylvainnahas/framac-werror）在此代码中报告错误，但Eva未报告任何问题。我试过增加Frama-C的冗长度，但我还是......

frama-c

回答 1 投票 1

puts（NULL） - 为什么WP + RTE没有抱怨？

考虑一下这个小C文件：#include void f（void）{puts（NULL）;我正在运行像这样的Frama-C的WP和RTE插件：frama-c-gui puts.c -wp -rte -wp-rte我希望...

standard-library frama-c

回答 1 投票 2

如何在没有Internet连接的计算机上安装Frama-c

我试图在一台无法连接到互联网的计算机上安装Frama-c，因为安全性，但我可以使用USB将所需文件复制到此计算机。这个当前的操作系统......

ubuntu-16.04 frama-c

回答 1 投票 0

Frama-c：如何访问由value plugin分配的__malloc *变量

我从Frama-c开始，所以我不能很好地掌握它。我想使用Frama-c来实现指针别名分析器。除非我弄错了，在我看来，值插件不会给...

c pointers frama-c

回答 1 投票 1

frama-c 相关问题

最新问题