Может ли frama-c получить диапазон переменных перед конкретным программным кодом

Question

int main()
{
    int B = 1;
    int x = rand()%10+1;
    int x1 = rand()%10+1;
    int A = 1;
    while((B <= 5))
    {
            B++;
            A++;  
            if(B == x)
            {
                return 0;
            }
    }
    task(A) //The variable A passes in the range of values before the task function
    A = -2;
    return 0;
}
/*How can I use frama-c to get the range of A at task code if I want to get the range of A at task statement position instead of the range of A at the end of the program execution*/

Как я могу использовать frama-c для получения диапазона A в коде задачи, если я хочу получить диапазон A в позиции оператора задачи вместо диапазона A в конце выполнения программы

Answer 1

Если я хорошо понимаю ваш вопрос, вы хотели бы знать интервал изменения A при конкретном утверждении.Я предполагаю, что вы полагаетесь на плагин Eva, так как это тип информации, которую обычно дает Eva (по крайней мере, если я правильно интерпретирую «вместо диапазона A в конце выполнения программы»)).

Есть две возможности.Первый - использовать программный API Eva, а именно модуль Db.Value.Это требует знания OCaml и чтения Руководства разработчика Frama-C , но является наиболее гибким и стабильным способом доступа к информации.Вкратце, Db.Value.get_state, как следует из его названия, вернет абстрактное состояние, вычисленное после запуска анализатора Eva, для оператора, заданного в качестве аргумента, в то время как Db.Value.eval_expr, с учетом абстрактного состояния и выражения, вычислитабстрактное значение выражения в соответствующем состоянии.

Вторая возможность - использовать семейство встроенных функций Frama_C_show_each_*: всякий раз, когда Eva встречает функцию, имя которой начинается с Frama_C_show_each_, она будет печататься настандарт выводит абстрактное значение аргументов, переданных функции в текущем абстрактном состоянии.Следовательно, добавление Frama_C_show_each_A(A); перед вызовом task(A) даст вам, наряду с frama-c -eva test.i, среди прочего

[eva] test.i:19: Frama_C_show_each_A: [1..2147483647]

Обратите внимание, что я изменил ваш код по порядкучтобы он работал правильно с Frama-C:

• добавлен прототип extern int rand(void); и extern void task(int);
• добавлен ';'после task(A)

Пожалуйста, убедитесь, что вы предоставили минимальный, полный и поддающийся проверке пример с вашими вопросами , это делает их намного, намного проще, ответить на