Подавить сообщения [значение] в журнале анализа стоимости Frama-C.

Вы можете обнаружить, что параметры командной строки 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