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

Question

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

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

您认为使用 Frama-C 有可能吗(使用 ACSL 或通过开发新模块)？

非常感谢 =)

Answer 1

to detect some code pattern such as a doubled if tests

如果您指的是一种模式，其中内部 if 的条件始终为真，因为它是外部 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

这只能试探性地使用。用于冗余测试的声音检测器由执行路径分隔，其中所涉及的变量未被修改，可以利用值分析的结果作为插件实现。

that a call to a given function is always followed by another.

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

check if a variable with a given prefixed named belongs to a certain type.

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