抑制 Frama-C 价值分析日志中的 [value] 消息

Question

我想使用 Frama-C（批处理模式）中 Value 插件的分析结果来进一步评估函数中的变量。但是，输出似乎很大，有很多 [value] 标签，我需要的只是来自 [value] ====== VALUES COMPUTED ====== 的部分，每个函数末尾都有计算值。 Frama-C 是否支持允许我这样做的选项？

Answer 1

您可能会发现命令行选项 frama-c -no-val-show-initial-state -no-val-show-progress … 使输出更符合您的口味。

当使用后一个选项时，您可能会喜欢 -val-print-callstacks，它会在每次发出消息时打印消息对应的调用堆栈，因为该上下文从日志中的前几行不再可用。

为了说明，Frama-C在回答时的开发版本默认显示如下消息：

int x;

/*@ assigns x; */
void f(void);

void g(int y) {
  f();
  x += y;
}

int main(void) {
  g(1);
}

正在使用 frama-c -val t.c 进行分析：

[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
  x ∈ {0}
[value] computing for function g <- main.
        Called from t.c:12.
[value] computing for function f <- g <- main.
        Called from t.c:7.
[value] using specification for function f
t.c:3:[value] warning: no \from part for clause 'assigns x;' of function f
[value] Done for function f
t.c:8:[kernel] warning: signed overflow. assert x+y ≤ 2147483647;
[value] Recording results for g
[value] Done for function g
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
[value] Values at end of function g:
  x ∈ [-2147483647..2147483647]
[value] Values at end of function main:
  x ∈ [-2147483647..2147483647]
  __retres ∈ {0}

正在使用 frama-c -val t.c -no-val-show-initial-state -no-val-show-progress 进行分析：

[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
[value] using specification for function f
t.c:3:[value] warning: no \from part for clause 'assigns x;' of function f
t.c:8:[kernel] warning: signed overflow. assert x+y ≤ 2147483647;
[value] done for function main
[value] ====== VALUES COMPUTED ======
[value] Values at end of function g:
  x ∈ [-2147483647..2147483647]
[value] Values at end of function main:
  x ∈ [-2147483647..2147483647]
  __retres ∈ {0}

加上选项-val-show-callstack表示第8行的告警，上下文如下：

t.c:8:[kernel] warning: signed overflow. assert x+y ≤ 2147483647;
                  stack: g :: t.c:12 <- main

抑制 Frama-C 价值分析日志中的 [value] 消息

Suppress [value] messages in the log of Frama-C's Value Analysis

frama-c