[Question] Is it possible to get the specific values of all variables in a witness file in GraphML format?

[Chriszai]

I was trying to validate a java program, I can easily see the value of the value type in the witness file, but I can't see the return value of a call to a certain function, it's replaced by return_tmp.

The code I tested is shown below.

import java.util.Random;

public class test2 {

    public static void main(String[] args) {
        int x = 5;
        int i = new Random().nextInt();
            if(i >= 1000) assert i >= 1000 : "i is greater 1000 ";
    }
}

    <node id="15.402">
      <data key="invariant">anonlocal::1i = 5;</data>
      <data key="invariant.scope">java::test2.main:([Ljava/lang/String;)V</data>
    </node>

    <node id="26.421">
      <data key="invariant">anonlocal::2i = return_tmp1;</data>
      <data key="invariant.scope">java::test2.main:([Ljava/lang/String;)V</data>
    </node>

For instance, the value of int i is replaced by return_tmp1, could I get the exact value of the variable i which was created by random functiin in the witness file?