Frama-C Plugin-Development: Getting the values of value analysis of different calls

139 views Asked by At

I am developing a Frama-C-Plugin this should print the values of the variables after each statement. In the Frama-C-Gui, in the tab Values, I can see the values of the analysis over the whole program, and after different function calls (with the parameters of the function).

enter image description here

I now want to get the values AFTER each function-call (not the "all"-line, but the "main"-line.

Here is my program that I used for the screenshot:

void swap (int *a, int *b){
    int tmp = *a;
    *a = *b;
    *b = tmp;
    return;
}
int main (void){
    int a=1;
    int b=2;
    swap (&a, &b);

    a = 3;
    b = 4;
    swap (&a, &b);
}

Is this possible? How can I access these values?

PS: I've asked a related question, which already prints the "all"-part (and values BEFORE the statement), see this link: Frama-C Plugin development: Getting result of value-analysis

Is there a similar solution?

1

There are 1 answers

0
Thomas Böhm On

Thanks to the edit of the answer of the mentioned question, the solution can be found at the following site: Frama-C Plugin development: Getting result of value-analysis