Frama-c无法证明Allan Blanchard的教程中的verify.c
Frama-C是一种开源的源代码静态分析工具，用于进行C和C++程序的验证和验证。它可以帮助开发人员发现和修复代码中的错误、漏洞和不良实践，提高软件的质量和安全性。
在Allan Blanchard的教程中，他提到了一个名为verify.c的文件，但是Frama-C无法证明该文件。这意味着Frama-C无法通过静态分析来验证和证明verify.c文件中的代码的正确性。
Frama-C的优势在于其强大的静态分析能力，可以检测出代码中的潜在问题，如空指针解引用、缓冲区溢出、未初始化变量等。它还提供了一些高级功能，如符号执行、模型检查和代码覆盖率分析，以帮助开发人员更好地理解和改进他们的代码。
Frama-C的应用场景包括软件开发、安全审计、代码重构和代码维护等。它可以帮助开发人员在早期发现和解决问题，减少后期的调试和修复工作量。同时，它还可以用于教学和研究领域，帮助学生和研究人员深入了解程序分析和验证的原理和方法。
腾讯云提供了一系列与云计算相关的产品和服务，其中包括云服务器、云数据库、云存储等。这些产品可以帮助用户快速搭建和部署基于云计算的应用，提供高可用性、可扩展性和安全性。具体的产品介绍和链接地址可以在腾讯云官方网站上找到。
相关·内容
我正在尝试从Allan Blanchard的中学习frama-c，但我在验证教程中建议的安装时遇到了问题。作者提供了一个带有ACSL注释的，所有这些frama C都应该能够证明。但是，当我运行命令(frama-c-gui -wp -rte main.c)时，我得到以下结果：
我通过opam (2.0.4版)将frama-c (22.0版)安装在ocaml-base-piler.4.11.1交换机上。当我安装它的时候，我遇到了Why3无法检测Alt-Ergo的问题，我最终手动编辑了~/why3.config。我在这里提到它，尽管我不确定它是否与前面提到的问题有关。
浏览 8提问于2021-02-15得票数 2
回答已采纳
1回答
对于Frama和WP插件，用户如何断言程序中的某个点是不可到达的？
寻找这样的东西：
//@ assert \unreachable;
浏览 4提问于2022-09-27得票数 1
2回答
最近，我一直在使用frama-c，我遇到了一个有点令人困惑的问题。
我用frama-c编写了一个非常简单的程序，即：
void main(void)
{
int a = 3;
int b = 4;
/*@ assert a == b;*/
}
我希望GUI中的断言是无效的--在frama-c中，这是用红色子弹表示的，但是frama-c说，根据值(假设下)，这个断言是无效的，这是用橘红色子弹表示的。
我的问题是，为什么frama-c会说这个断言在假设下是无效的？
可能的假设是什么？
我之所以问这个问题，是因为我的程序非常简单，在我的程序中找不到任何与断言相关的假设或依赖，
浏览 0提问于2018-06-18得票数 2
回答已采纳
我目前正在使用frama-c，我想看看frama-c是如何对给予证明者(或证明助手)的各种证明义务进行编码的。在本例中，使用alt-ergo组合键。
我想知道是否有任何特定的方法可以“转储”给alt-ergo的输入(假设alt-ergo是从frama-c调用的；即不是interop)？
我想看看C程序属性的证明义务是如何用alt-ergo的“本机”输入语言编码的。任何帮助都将不胜感激。
浏览 15提问于2019-11-16得票数 1
1回答
在下面的最小示例中(从Allan Blanchard的优秀教程-第3.2.3.3节副作用中略为修改)：
int h = 42;
/*@
requires \valid(a) && \valid(b);
requires \valid_read(a) && \valid_read(b);
ensures *a == \old(*b) && *b == \old(*a);
*/
void swap( int *a, int *b) {
int tmp = *a;
*a = *b;
*b = tmp;
}
//
浏览 5提问于2022-06-30得票数 2
回答已采纳
我正在验证Frama+ WP的一个简单程序。
#include <string.h>
/*@
requires valid_read_string(s);
assigns \result \from indirect:s[0..];
ensures \result == strlen(s);
*/
size_t get_len(const char *s) {
return strlen(s);
}
int main() {
static const char foo[4] = { 'H&#
浏览 4提问于2021-03-28得票数 3
回答已采纳
2回答
我应该如何像下面这样的方法来证明代码的正确性，为了避免一些低效率，它依赖于模块化算法？
#include <stdint.h>
uint32_t my_add(uint32_t a, uint32_t b) {
uint32_t r = a + b;
if (r < a)
return UINT32_MAX;
return r;
}
我试验过WP的"int“模型，但是，如果我正确理解，该模型将配置POs中逻辑整数的语义，而不是C代码的正式模型。例如，在使用"int“模型时，WP和RTE插件仍然需要并为上面的无符号添加注
浏览 2提问于2013-08-02得票数 5
回答已采纳
关于先决条件和Frama-c wp，我有两个问题：
？Frama-c如何证明先决条件？-c什么时候尝试证明先决条件?
我之所以问这些问题，是因为有时候frama-c wp甚至没有尝试证明，有时它成功地证明了前提条件，有时它失败了，例如在第一个屏幕截图中，证明没有被尝试过。
但在第二张截图中，我们试图证明，但失败了。
我假设主要功能对此有影响，但这是全貌吗？前提条件是否只有在函数主要时才是证明的对象？
浏览 3提问于2021-03-30得票数 3
回答已采纳
1回答
我使用frama-C WP，并希望调试我的ACSL注释(以理解为什么验证者说我“不知道”)。我有一些绿色或橙色的结果。我打开why3集成开发环境，看到生成的脚本。然后，我从列表中选择一个理论/目标，并能够启动Alt-Ergo或Coq IDE。我想在Coq IDE中使用生成的代码。我看到一些公理，然后是定理WP，然后，举个例子：
intros a a_1 i_3 i_2 i_1 i t_2 t_1 t t_8 t_7 t_6 t_5 t_4 t_3 a_4 a_3 a_2 x
x_1 x_2 x_3 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h
浏览 2提问于2017-08-26得票数 2
使用frama-c时，我正在编写使用位字段来表示集合的代码。说这样的话：
typedef uint32_t myset_t;
#define EMPTY_SET UINT32_C(0)
#define FULL_SET UINT32_C(0x0ffffff)
所以我只使用32位无符号整数的最低n位。然后我想实现一个谓词来检查是否在"myset_t“中设置了一个位。这并没有像预期的那样工作(frama-c和alt-ergo能够证明关于这类集合的东西)，我可以产生一个简单的引理，它已经显示了我的问题。在我的安装(frama-c 21.1 Scandium)上，它不能自动证明以下简
浏览 3提问于2020-08-02得票数 1
我是frama-c的新手。我做了一些教程，并希望构建一个微小的现实世界应用程序。我没走多远，因为我遇到了一个困扰我的警告。
这就是我要验证的程序：
#include <unistd.h>
/*@
assigns __fc_fds[0];
ensures \result == 0;
*/
int main()
{
char s[] = "hello\n";
(void)write(1, (const void*)s, 6);
return 0;
}
我运行以下命令来验证它：
frama-c -wp -wp-rte -wp-timeout 1 ma
浏览 4提问于2022-10-03得票数 0
回答已采纳
1回答
我刚刚建立了安装从Opam软件包管理，并试图学习如何使用价值分析，从教程的frama-c网站。我目前无法使用builtin.c文件，它不在我的共享文件夹中，我也无法弄清楚如何使用-val(如果这是合适的话)。
有什么办法能让这一切顺利进行吗？
我安装了Frama的20151002版本。
谢谢你的帮助！！
浏览 2提问于2016-04-22得票数 1
回答已采纳
1回答
整数对数使用什么循环不变量？
、、、、
当我使用Frama-C进行C语言正式验证的第一步时，我正在尝试正式验证一个整数二进制对数函数，如下所示：
//@ logic integer pow2(integer n) = (n == 0)? 1 : 2 * pow2(n - 1);
/*@
requires n > 0;
assigns \nothing;
ensures pow2(\result) <= \old(n) < pow2(\result + 1);
*/
unsigned int log2(size_t n)
{
unsigned int res = 0;
wh
浏览 18提问于2020-02-11得票数 3
回答已采纳
我是Frama-c的新手，我想知道这个简单的例子有什么问题：
/*@ requires \valid(array+(0..length-1))
@ ensures \forall integer k; 0 <= k < length ==> array[k] == 0;
@ assigns array[0..length-1];
*/
void fill(int array[], int length){
/*@ loop invariant 0 <= i <= length;
@ loop invariant \forall integer k;
浏览 0提问于2013-05-23得票数 4
回答已采纳
1回答
我使用Frama氮来分析以下代码
#include "/usr/share/frama-c/builtin.h"
int test()
{
const unsigned char a = Frama_C_interval(0, 255);
const unsigned char b = Frama_C_interval(0, 255);
const unsigned int c = ((unsigned int)a) | ((unsigned int)b);
return 0;
}
使用
frama-c -jessie test.c
不幸的是
浏览 5提问于2014-04-21得票数 2
回答已采纳
以下是swap示例表单WP插件教程；
/*@ requires \valid(a) && \valid(b);
@ ensures A: *a == \old(*b) ;
@ ensures B: *b == \old(*a) ;
@ assigns *a,*b ;
@*/
void swap(int *a, int *b)
{
int tmp;
tmp = *a;
*a = *b;
*b = tmp;
return;
}
这是我用coq在上面运行frama的结果；
frama-c -wp -wp-rte -wp-proof coq swap.c
[ker
浏览 5提问于2016-04-13得票数 2
回答已采纳
模型变量在Frama-C手册中描述(在规范和“实现”版本中)。
然而，我无法解析一个简单的片段，例如手册中的片段。
//@ model set<integer > forbidden = \empty;
甚至是
//@ model integer x = 0;
导致解析错误。
模型变量真的受支持吗？如果是这样，我做错了什么？我使用的frama-c版本是MacOS上的氮气。
谢谢，爱德华多
浏览 2提问于2012-04-26得票数 1
回答已采纳
我正在尝试使用Frama-C打印C程序中的变量类型。我发现此信息在GUI中表示，如下图所示。但是，我无法找到将此信息输出到文件的方法。您能建议我使用Frama-c执行此任务的方法吗？
浏览 10提问于2020-02-09得票数 2
回答已采纳
我想不出有什么办法来证明foo的赋值子句。我尝试了assigns var;，因为foo()间接地修改了全局var变量，但它不起作用。有没有办法为本地p变量获取assigns子句或从a()返回位置?代码如下：
int var;
//@ assigns \nothing;
int *a(){
return &var;
}
//@ assigns *p;
void b(int* p){
*p = 1;
}
//@ assigns \nothing;
void foo(){
int *p = a();
b(p);
}
//@ assigns var;
void main
浏览 0提问于2018-11-02得票数 1
回答已采纳
Frama-C错误插件()在这段代码中报告了一个错误，但是Eva没有报告任何问题。我已经尝试增加Frama-C的冗长，但我仍然看不出问题出在哪里。我在MacOS10.13.6上运行通过opam安装的Frama-C18.0 (Argon)。
#include <stdio.h>
#include <stdbool.h>
#include <stdlib.h>
#define MY_ASSERT(must_be_true__) \
(void)((must_be_true__) ? (void)0 : my_assert_crash())
void my_a
浏览 20提问于2019-04-21得票数 1
回答已采纳
我试图证明变量的值总是增加的。我写了以下代码：
void Commit() {
int count = 1;
//@ ghost int old_count = 0;
while (1) {
//@ ghost old_count = count;
count++;
//@ assert count > old_count;
}
}
int main () {
Commit();
return 0;
}
然后我使用命令：frama-c -val file.c，但是断言状态仍然未知。我是不是
浏览 2提问于2018-06-25得票数 2
2回答
在ACSL中定义的归纳谓词上可以使用归纳吗？
请考虑中的以下示例
struct List {
int value;
struct List* next;
};
/*@ inductive reachable{L}(struct List* root, struct List* to) {
@ case empty{L}: \forall struct List* l; reachable(l, l);
@ case non_empty{L}: \forall struct List *l1,*l2;
@ \valid(l1) && r
浏览 4提问于2015-09-08得票数 1
回答已采纳
我对Frama很陌生。我想在Windows环境下运行它。我的编辑是gcc。
我尝试运行相同的例子，从价值分析教程，我有一个问题的库头文件。
我发现不可能运行frama，因为限制关键字。它显示了字符串.h文件中的错误
void * __cdecl memcpy(void * __restrict__ _Dst,const void * __restrict__ _Src,size_t _Size) __MINGW_ATTRIB_DEPRECATED_SEC_WARN;
当我手动添加#定义时，将限制为SkeinProject中的所有*.c文件
schneier.com/code/skein_N
浏览 2提问于2014-04-18得票数 2
回答已采纳
我是新来的。我正在尝试使用rte插件生成注释。通过查看链接1，我尝试使用以下命令生成注释：
frama-c -rte -rte-未签名-ovtest.c
其中我的test.c包含
int main(void){
signed char cx, cy, cz;
cz = cx + cy;
return 0;
}
我从2节2.1.2中复制了代码。我希望rte将生成以下注释并修改test.c文件：
/*@ assert rte: signed_overflow: -2147483648 <= (int)cx+(int)cy; */
/*@ assert rte: signed_ov
浏览 0提问于2019-07-13得票数 1
回答已采纳
1回答
我正在尝试用Frama-C的WP插件来证明一些C代码，下面的例子有问题：
typedef unsigned char uint8_t;
const uint8_t globalStringArray[] = "demo";
const int STRING_LEN = 5;
/*@ requires \valid(src) && \valid(dest) && len < 32 ; */
void copyMemory(uint8_t * src, uint8_t * dest, unsigned int len);
/*@ req
浏览 3提问于2015-10-06得票数 1
我想对以下程序进行切片：
int main() {
int j;
if (j) {
ERROR:
/*@ slice pragma ctrl; */
goto ERROR;
}
return 0;
}
目前，Frama-C在读取j之后停止探索路径，导致ERROR标签被切掉：
$ frama-c test.c -slice-pragma main -then-on 'Slicing export' -print
[...]
test.c:3:[kernel] warning: accessing uninitialized left-value:
浏览 0提问于2014-05-07得票数 1
1回答
作为示例，我使用以下函数：
float nondet_float(){
float x;
return x;
}
int main(){
float x = nondet_float();
if(isnan(x)){
some_error();
}
}
我想知道如何使用frama-c来模拟非确定性浮点数。
我想要的是，变量x，被认为是任何可能的浮点值，包括-inf，+inf和NaN。
我希望得到这样的结果:如果x为NaN，则some_error()是可达的。
所以我的问题是：
如何模拟不确定的浮点数？如何测试某些函数调用的可达性？
浏览 1提问于2017-09-17得票数 1
我是frama-c的新手。所以我为我的问题提前道歉。
我想做一个插件，它将修改源代码，克隆一些函数，插入一些函数调用，我希望我的插件生成第二个文件，其中将包含输入文件的修改版本。
我想知道是否可以使用frama-c生成一个新的文件c。例如，Sparecode和语义常量折叠插件的结果直接显示在终端上，而不是以文件形式显示。所以我想知道Frama-c是否具有写入文件的功能，而不是将分析结果发送到标准输出。
当然，我们可以将frama-c的输出重定向到file.c。例如，在本例中，对于插件scf，value的结果在那里，我发现frama-c用while替换了例如" for“循环。
但我希望的
浏览 10提问于2018-01-06得票数 0
1回答
我试图在ubuntu上安装frama-c，按照这里的说明，在安装了所有必要的软件包并给出最终命令opam install -j 1 frama-c之后，结果是
The following actions will be performed:
∗ install conf-gtksourceview 2 [required by frama-c]
∗ install conf-gnomecanvas 2 [required by frama-c]
∗ install conf-gmp 1
浏览 3提问于2017-06-02得票数 1
回答已采纳
1回答
我安装了Frama钠(20150201) + Jessie插件，我正在尝试复制ACSL参考手册中提供的示例。但是我不能使用Jessie库函数(比如\strlen)，因为每次我使用其中一个函数时，都会收到以下错误：
[kernel] user error: unbound function \strlen in annotation.
这是代码：
/*@
requires \base_addr(src) != \base_addr(dest);
requires \strlen(src) >= 0;
*/
char *strcpy ( char * dest , c
浏览 5提问于2015-08-04得票数 2
回答已采纳
我已经安装了frama-c和why3，但当我尝试启动frama-c时，jessie3出现错误。
frama-c -verbose 2
[kernel] warning: cannot load plug-in `Jessie3' (incompatible with Neon-20140301).
The exact failure is: error loading shared library:
/usr/local/lib/framac/plugins/Jessie3.cmxs: undefined symbol: camlGzip
我没有找到任何关于camlGzip的信息，所以
浏览 1提问于2014-10-29得票数 1
我是Frama-C的新手，我想正确地学习ACSL语法。我有一个虚拟示例，而Jessie插件无法验证nr9和12行。我是否遗漏了什么？要验证的函数(equal)将检查两个数组(a和b)在每个索引上是否具有相同的值：
/*@
requires \valid_range(a,0,n-1);
requires \valid_range(b,0,n-1);
requires n >= 0;
requires i >= 0 && i <= n;
assigns i;
behavior all_equal:
浏览 3提问于2013-04-18得票数 3
1回答
我有一个大约37行长的ACSL谓词(谓词返回传递的结构是否处于有效状态)。它是&&d的一系列条件。
当我断言谓词时：
//@ assert MyPredicate(myArg);
而且验证失败了，我不知道&&的哪些条件失败了。
如何知道谓词的哪一部分失败？
当验证失败时，我用frama-c-gui -wp -wp-rte myfile.c打开C文件。我更经常使用相同的args运行frama-c，但我使用GUI来帮助调查故障。
$ frama-c-gui --version
24.0 (Chromium)
如果谓词永远不会改变，我可能可以手动将它分解成单独的/*@
浏览 4提问于2022-09-18得票数 3
回答已采纳
拿着这根绳子
bob.ted.dave.allan::james.fred: hello.dave
我需要将.的每次出现替换为#，直到我碰到单数":“不停留在名称空间'::‘但只是":”
因此，在上面的字符串中，最终结果将是bob#ted#dave#allan::james#fred: hello.dave
现在我有了。它匹配字符串中的所有点，但无法将其锚定在单个":“上。
浏览 1提问于2019-03-07得票数 0
请告诉我，这是否是Frama中整数和无符号整数的非确定性值的正确模型？
/* Suppose Frama-C is installed in /usr/local -default prefix */
#include "/usr/local/share/frama-c/builtin.h"
#include "/usr/local/share/frama-c/libc/limits.h"
...
#define nondet_int() Frama_C_interval(INT_MIN, INT_MAX)
#define nondet_uint() Fr
浏览 14提问于2015-02-11得票数 3
回答已采纳
我能够使用Frama证明以下程序，这是令人惊讶的，因为1)断言是假的，2)循环不变量不保持(数组a持有1's非2's)。我是不是漏掉了什么？
/*@ requires \valid(a+ (0..9)) && \valid(b+ (0..9));
*/
void test_foo(int *a, char *b) {
int i = 0;
/*@ loop invariant \forall int j; 0 <= j < i ==> a[j] == 2;
loop invariant \forall int j; 0
浏览 1提问于2016-01-19得票数 2
回答已采纳
我使用以下命令在Ubuntu 14.04上安装了Frama-c：
sudo apt-get install frama-c
但是，当我使用以下命令打开frama-c的GUI时：
frama-c-gui
我找不到左侧窗口的“影响分析”插件。
此图显示了当前可用的Frama-c插件：
我也参考了，但找不到任何链接供我下载或安装影响分析插件。
如何启用和使用Ubuntu14.04的影响分析？
浏览 8提问于2017-09-26得票数 3
回答已采纳
1回答
使用插件时出错
、、、
考虑到插件被认为处于开发的“早期阶段”，也许我现在运气不好。但想知道是否还有其他人遇到过这样的问题：
navarre@navarre-t400:~/code/c$ frama-c max.cpp
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing max.cpp (external front-end)
: CommandLine Error: Option 'asm-macro-max-nesting-depth' reg
浏览 1提问于2017-08-12得票数 1
回答已采纳
我已经成功地安装了frama-c-硅使用opam的说明，但当我想升级到磷，opam不工作。
我用了命令：
opam pin add frama-c下载/frama-c-磷20170501.tar.gz
它说：
[NOTE] Package frama-c is already path-pinned to
/home/talos/Downloads/frama-c-Phosphorus-20170501.tar.gz.
This will erase any previous custom definition.
Proceed ? [Y/n] y
[fr
浏览 3提问于2017-06-04得票数 0
在某些情况下，例如当使用Eva的抽象域时，加载会话总是会发出表单的警告：
[kernel] Warning: 1 state in saved file ignored. It is invalid in this Frama-C configuration.
例如，下面是如何使用一个简单的C文件来再现它，该文件只包含一个main函数(int main() {})：
frama-c main.c -eva -eva-domains gauges -save framac.sav
frama-c -load framac.sav
当使用frama-c-script make-template生成
浏览 5提问于2021-06-16得票数 0
回答已采纳
1回答
首先，如果这不是问这个问题的正确地方，我想道歉，但我知道这里有多好的社区精神，从我在堆栈溢出。
我对数据库世界非常陌生，但我希望创建一个应用程序，该应用程序将使用后台数据库来保存data.The应用程序，它将成为一个行动计划创建者，并将保存大量数据，但我不知道如何设计我的数据库。因此，我寻求一些帮助。
我将对数据库使用MySQL，对应用程序使用Java。
设计：
我试着打印出我希望这个设计是怎样的，但最后我混淆了自己的意思，所以我猜到我在这里解释是没有运气的。因此，以下是我将努力实现的每一项行动计划的形象：
📷
我希望这能有所帮助，但为了进一步解释，每个行动计划都有其中一个(我知道我需要运行某
浏览 0提问于2014-06-25得票数 0
回答已采纳
如何在Mac上安装当前的Frama-C版本及其必备组件？
我已经知道了Frama-C，另一所大学的一位同事推荐了它。
我之前曾尝试安装Frama-C，但失败得很糟糕。这位同事评论说，他也有过同样的经历。好吧，时代不同了。
frama-c.com下载页面没有任何平台的当前(Flourine 3)版本的二进制文件的链接。指向安装说明的链接会将我带到一个页面，上面显示要下载自动安装程序。什么自动安装程序？
有针对旧版本Mac的说明，但遵循这些说明并不起作用；按照说明加载一组必备组件会产生无法安装下一个必备组件(gtksourceview)的状态。
当然，我检查了较旧的版本，我看到Mac OS X
浏览 9提问于2013-08-08得票数 4
如何使frama-c -wp验证来自的示例--一个简单的swap函数(swap.c)：
/* @ requires \valid(a) && \valid(b);
@ ensures A: *a == \old(*b);
@ ensures B: *b == \old(*a);
@ assigns *a,*b;
@*/
void swap(int * a, int * b);
void swap(int * a, int * b) {
int tmp = * a;
*a = *b;
*b = tmp;
return ;
浏览 4提问于2015-09-04得票数 3
回答已采纳
1回答
我试着用二维数组来验证一个程序，但是在赋值子句中遇到了一个问题。
在示例代码上，我可以证明init_2D_2函数中的赋值子句。
但是，我未能在主要功能中证明相同的赋值子句。
主函数只调用init_2D_2，所以我认为赋值应该是正确的。
有人能告诉我为什么夫人-c不能证明吗？
#include <stdio.h>
#include <stdlib.h>
#include <stdbool.h>
#include <assert.h>
#define size 5
#define page 10
/*@
re
浏览 3提问于2022-09-05得票数 1
回答已采纳
我从Frama-c得到一个向后切片，但看起来它是一个静态切片，而不是动态切片。
在frama-c中有一个特定的选项来获得一个动态的向后切片吗？
浏览 2提问于2014-10-25得票数 1
我正在使用Cil_types用frama-c开发一个插件。这个插件默认接受C程序的AST作为输入(Cil_types.file)。我想获取此文件的名称，但使用Cil_types无法获取。是否可以通过其他方式获取此信息？
浏览 0提问于2014-03-10得票数 2
我安装了frama镁版，使用说明提供了。在安装和执行Cygwin打印的Frama版本为：frama-c -version的命令Magnesium-20151002时，我没有发现任何错误。但是，当我在一个非常小的例子中执行-wp插件时，对于使用alt-ergo的目标，我会得到以下错误：
1 [main] frama-c 8168 child_info_fork::abort: unable to map C:\cygwin\usr\local\lib\frama-c\plugins\Users.cmxs, Win32 error 998 1 [main] frama-c 7956 child
浏览 4提问于2016-04-26得票数 5
回答已采纳
我正在尝试使用取自网页https://frama-c.com/acsl_tutorial_index.html的归纳谓词的示例 #include <stddef.h>
#include <stdlib.h>
typedef struct _list { int element; struct _list* next; } list;
/*@ inductive reachable{L} (list* root, list* node) {
case root_reachable{L}:
\forall list* root;
浏览 42提问于2019-09-27得票数 1
回答已采纳
我正在研究Frama-c框架，我想知道C/Frama-c和Spark Ada之间是否有等价物。我知道比较这种不同的语言看起来很奇怪，但在阅读了、和一些SPARK的用户手册后，我很难猜测SPARK和C/Frama-c/ACSL是否提供了相同的证明健壮性和相同的代码可靠性。
提前感谢您给出您的观点/经验！
PS:我是frama-c的新手，我对SPARK编程了解不多。
浏览 9提问于2018-05-24得票数 0
扫码
添加站长 进交流群
领取专属 10元无门槛券
手把手带您无忧上云
相关资讯
热门标签
云服务器
ICP备案
对象存储
腾讯会议
实时音视频活动推荐
腾讯云开发者
