По поводу оценки времени исполнения
Frama-C работает на уровне C.Плагин Metrics может предоставить несколько метрик (например, количество операторов) для версии источника, очень близкой к исходной (-metrics -metrics-ast cabs), или для нормализованного источника (часто называемого Cil code *).1005 *), что он использует.Однако он не имеет никакого знания о коде сборки, поэтому не может предоставить точную информацию о времени выполнения на этом уровне.
Поскольку оптимизации компилятора влияют на генерацию кода, числа, указанные в Frama-C, могут быть или не бытьблизко к тому, что будет генерироваться компилятором, в зависимости от того, какие оптимизации включены, что известно о компиляторе и целевой архитектуре и т. д. В общем случае Frama-C не может дать никаких гарантий;в определенных ситуациях можно разработать плагины для предоставления некоторой этой информации (например, плагин Cost, упомянутый здесь , использует аннотации, чтобы попытаться сохранить некоторое соответствие между исходным и скомпилированным кодом, а затемиспользует их для предоставления некоторой информации о времени выполнения).
Относительно оценки объема памяти
Существует опция, -metrics-locals-size, которая делает приблизительную оценку стека памяти.использование функцией.Как и в предыдущем случае, это только оценка на основе исходного кода.Компиляторы могут распределять в стеке временные переменные для вычисления временных подвыражений или для различий в регистре, поэтому числа, заданные Frama-C, не могут использоваться при оценке стека в худшем случае.
Динамическое выделение памяти поддерживается вACSL, так что теоретически можно написать аннотации по этому поводу.Тем не менее, современные плагины не обеспечивают прямой способ справиться с этим точно;это может потребовать написания нового плагина или, по крайней мере, абстрактного домена для Eva.
Eva в настоящее время обрабатывает динамическое распределение, но, вероятно, недостаточно точно для оценки размера кучи интересным способом.Можно разработать абстрактный домен для Eva, который бы отслеживал эту информацию (добавляя malloc s и вычитая free s) и вычисляя overapproximation пространства кучи памяти, но это потребовало бывозможность ограничить количество итераций циклов, содержащих выделения (в противном случае верхняя граница была бы бесконечной).Точность зависит от сложности программы.
Для проверки во время выполнения плагин E-ACSL уже отслеживает использование некоторой информации стека / кучи (даже если она в настоящее время не экспортируется пользователю), поэтому вТеоретически можно написать утверждение, подобное //@ assert heap_size <= \old(heap_size) + 42;, и проверить его во время выполнения при запуске инструментированной программы.