Search code examples
cframa-c

Whether frama-c can get the range of variables before a particular program code

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*/

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

Solution

  • If I understand your question well, you would like to know the interval of variation of A at a specific statement. I assume that you're are relying on the Eva plug-in, as it is the kind of information that is typically given by Eva (at least if I interpret well "instead of the range of A at the end of the program execution").

    There are two possibilities. The first one is to use the programmatic API of Eva, namely the Db.Value module. This requires knowledge of OCaml and reading the Frama-C developer manual, but is the most flexible and stable way to access the information. Briefly speaking, Db.Value.get_state will, as its name suggests, return the abstract state computed after a run of the Eva analyzer, for the statement given as argument, while Db.Value.eval_expr, will, given an abstract state and an expression, compute the abstract value of the expression in the corresponding state.

    The second possibility is to use the Frama_C_show_each_* family of built-in functions: whenever Eva encounters a function whose name starts with Frama_C_show_each_, it will print on the standard output the abstract value of the arguments given to the function in the current abstract state. Hence, adding Frama_C_show_each_A(A); before the call to task(A) will give you, with frama-c -eva test.i, among other things

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

    Note that I've modified your code in order to let it run properly with Frama-C:

    • added prototype extern int rand(void); and extern void task(int);
    • added a ';' after task(A)

    Please ensure that you provide a minimal, complete and verifiable example with your questions, this makes them much, much, easier to answer