c - 类型检查和代码模式检测，Frama-C

我正在发现Frama-C软件，并且想知道是否有可能检测到某些代码模式，例如测试是否翻倍，或者例如对给定函数的调用总是跟在另一个函数之后。

或者也许使用变量名称，例如检查具有给定前缀named的变量是否属于某种类型。

您认为使用Frama-C(使用ACSL或开发新模块)是否可能？

非常感谢=)

最佳答案

检测一些代码模式，例如测试是否加倍

如果您的意思是内部if的条件始终为true的模式，因为它是外部if的结果，则GUI可以向您显示在值分析期间发现内部if的else分支不可访问。

举个简单的例子:

int x, y;

int main(int c){
  if (c == 2)
    {
      x = x * c;
      if (c == 2)
        {
          y = y * c;
        }
      else
        {
          y = y / c;
        }
    }
}

命令行是:

$ frama-c-gui -val t.c

只能凭经验使用。可以将通过执行路径分隔的冗余测试的声音检测器用作插件，以利用价值分析的结果，该执行路径没有修改涉及的变量。

对一个给定函数的调用总是跟随另一个。

使用Aoraï(这是Frama-C发行版中包含的(已编辑:)，尽管其网页声称有此功能)，这是可能的。 Aoraï生成与已表达的时间属性相对应的证明义务。证明这些义务或多或少是困难的。在某种程度上，Aoraï仅将验证时间属性的问题减少到另一个问题，在Frama-C中存在插件。

检查具有给定前缀named的变量是否属于某种类型。

这种类型的“编码标准”检查也可以实现为Frama-C插件。 Atos实现了一个名为Taster的插件来验证空客编码规则。