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

Question

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

或者可能使用变量名称的东西，例如检查具有给定前缀命名的变量是否属于某种类型。

您认为 Frama-C 是否可行（使用 ACSL 或开发新模块）？

非常感谢 =)

Answer 1

检测一些代码模式，例如双重 if 测试

如果您的意思是一种模式，其中内部 if 的条件始终为真，因为它是外部 if 的结果，那么 GUI 已经可以向您显示else在值分析期间发现内部 if 的分支无法访问。

举个简单的例子：

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 插件，它（已编辑：）包含在 Frama-C 发行版中，尽管其网页声称。Aoraï 生成与已表达的时间属性相对应的证明义务。证明这些义务可能或多或少是困难的。在某种程度上，Aoraï 只是将验证时间属性的问题简化为另一个问题，Frama-C 中有插件。

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

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