Frama-c断言

Question

最近，我一直在使用frama-c，我遇到了一个有点令人困惑的问题。

我用frama-c编写了一个非常简单的程序，即：

void main(void)
{
    int a = 3;
    int b = 4;
    /*@ assert a == b;*/
}

我希望GUI中的断言是无效的--在frama-c中，这是用红色子弹表示的，但是frama-c说，根据值(假设下)，这个断言是无效的，这是用橘红色子弹表示的。

我的问题是，为什么frama-c会说这个断言在假设下是无效的？

可能的假设是什么？

我之所以问这个问题，是因为我的程序非常简单，在我的程序中找不到任何与断言相关的假设或依赖，我想frama-c应该只是说断言无效。

Answer 1

查看假设下证明的属性的依赖性的另一种方法是在命令行上使用Report插件：

$frama -val c.c -then -report

[report] Computing properties status...

--------------------------------------------------------------------------------
--- Properties of Function 'main'
--------------------------------------------------------------------------------

[  Alarm  ] Assertion (file c.c, line 5)
            By Value, with pending:
             - Unreachable program point (file c.c, line 5)

--------------------------------------------------------------------------------
--- Status Report Summary
--------------------------------------------------------------------------------
     1 Alarm emitted
     1 Total
--------------------------------------------------------------------------------

挂起的信息列出了完成验证所需的所有属性。对于由值/Eva插件发出的法规，发出的唯一依赖项总是可达的依赖项。

(这实际上是误导的: n属性的状态实际上取决于k

Answer 2

如果使用Frama安装配置了graphviz (即配置Frama时可用，无论是手动配置还是通过opam配置)，则可以双击“属性”面板中的属性，然后打开一个窗口，该属性的依赖关系图如下：

​

​

在它中，我们可以看到一个属性所使用的所有假设，因此我们看到所提到的“假设下”是断言的可达性。Eva (value插件)计算可达状态的过近似，因此它不能证明给定的状态是可达的，只能证明它是不可达的。

目前，唯一能够明确证明可达状态的插件是PathCrawler。然而，在实践中，这很少是一个问题。