0

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?

Community
  • 1
  • 1
Thomas Böhm
  • 1,456
  • 1
  • 15
  • 27
  • 1
    I believe I might have answered this in your other question. If so, it might be worth closing this one (although I'd recommend adding the screenshot to the other question with a comment such as "... just like the GUI does, as in this panel", since it's often nice to have some pictures as examples). – anol Mar 22 '16 at 19:32
  • By the way, ideally, by looking at the source code (`src/plugins/value/gui_eval.ml`, in this case), it should be possible to infer at least part of the code (e.g. `Db.Value.get_stmt_state_callstack` in this example, used in lines 231 and 235), but I agree that it is often too cumbersome to do so. Still, it's worth having that in mind, since it can give some tips on which functions to search for in the API. – anol Mar 22 '16 at 19:36

1 Answers1

0

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

Community
  • 1
  • 1
Thomas Böhm
  • 1,456
  • 1
  • 15
  • 27