Модуль анализа стоимости и опции расширений

У меня есть вопросы по опциям модуля анализа стоимости и опциям расширений.

Использую команду: frama-c-gui -val -slevel 100 -plevel 300 -absolute-valid-range 0x00000000-0xffffffff -metrics -metrics-value-cover -scope-def-interproc -main MYMAIN CODE/*.c

  • В одном файле -metrics дайте мне 3 goto на функцию без, как goto вычисляется?

  • Что такое «Оценка покрытия = 100,0%» с -metrics-value-cover Я получаю значение от 80 до 100%, вначале я думал, что получу <100%, когда у меня был мертвый код, но у меня был мертвый код, когда я получил 100%, поэтому я думаю получить 100%, если проанализировать все функции в исходных файлах?

  • Полагаю, 157 stmts in analyzed functions, 148 stmts analyzed (94.3%) это означает, что у меня мертвый код на моем проекте, это что?

  • # P6 #
    # P7 #

Итак, мне нужно проверить все 62 предупреждения или только 32, полученных с помощью этих параметров?


frama-c
person user3675417    schedule 20.06.2014    source источник

Ответы (2)


arrow_upward
2
arrow_downward

В одном файле -metrics [вводит] 3 goto для функции [у которой их нет]

Конструкции C &&, || и break; могут быть «нормализованы» в конструкции goto.

Я полагаю, что 157 stmts в проанализированных функциях, 148 проанализированных stmts (94,3%), что означает, что у меня мертвый код в моем проекте, это так?

да. Для входных данных, видимых для анализа значений, доступны только 148 из 157 утверждений. Обратите внимание, что если, например, main() имеет аргументы argc и argv, абстрактные значения, построенные для этих аргументов, могут не охватывать все значения, которые следует учитывать. Лучший способ определить, действительно ли эти 9 операторов недоступны, - это посмотреть на них (они отображаются красным в графическом интерфейсе Frama-C).

С опцией -scope-def-interproc я получаю 32 предупреждения (62 без), но на веб-сайте мы можем прочитать (в документации по области применения)

Не очень понятно, о чем вы спрашиваете. Было бы полезно, если бы вы предоставили пример с полной информацией (исходный код, командная строка (-и)), чтобы можно было воспроизвести ваши шаги и прояснить значение отправленных сообщений для вас. Приведите небольшой сокращенный пример, если невозможно получить полный пример: также (почти) невозможно ответить вам с предоставленной до сих пор информацией.

person Pascal Cuoq    schedule 20.06.2014
comment
Спасибо за Ваш ответ. По команде -scope-def-interproc у меня может быть вопрос. Предупреждения, удаленные этой опцией, можно игнорировать, потому что анализ (с опцией) более точен, чем просто модуль анализа значений или по другой причине. - person user3675417; 23.06.2014
comment
Я не могу присоединиться к исходному коду, но использую следующие команды: я получаю 32 предупреждения с frama-c-gui -val -slevel 100 -plevel 300 -absolute-valid-range 0x00000000-0xffffffff -metrics -metrics-value-cover -scope-def-interproc -main MYMAIN CODE/*.c и 62 предупреждения с frama-c-gui -val -slevel 100 -plevel 300 -absolute-valid-range 0x00000000-0xffffffff -metrics -metrics-value-cover -main MYMAIN CODE/*.c - person user3675417; 23.06.2014

arrow_upward
2
arrow_downward

Что такое «Оценка покрытия = 100.0%» с -metrics-value-cover Я получаю значение от 80 до 100%, вначале я думал, что получу ‹100%, когда у меня был мертвый код, но у меня был мертвый код, когда я получил 100 %, так я думаю получить 100%, если проанализировать все функции в исходных файлах?

Возьмем пример.

[metrics] Value coverage statistics
      =========================
      Syntactically reachable functions = 3 (out of 3)
      Semantically reached functions = 1
      Coverage estimation = 33.3% 

      Unseen functions (2) =
        <tests/metrics/reach.c>: baz; foo;

Первая строка, Syntactically reachable functions, является чрезмерным приближением количества функций вашей программы, которые могут быть в конечном итоге вызваны, начиная с main. Например, функция, адрес которой никогда не используется и никогда не вызывается напрямую, не будет внутри этого набора.

Semantically reached functions - это количество функций вашей программы, действительно проанализированных анализом значений.

Coverage estimation - это соотношение между этими двумя числами. Для небольших программ, в которых доступны все функции, обычно 100%.

Unseen functions - это список функций, которые должны были быть достигнуты (синтаксически), но никогда не анализировались Value.

Обратите внимание, что ни одно из этих чисел не говорит об инструкциях, поэтому вы все равно можете получить 100% с мертвым кодом.

person byako    schedule 29.07.2014