How to inspect the diff.txt?

[grandnew]

After running the example, I got the following diff.txt:

[INFO] Start preprocessing the input bitcode ... 
[WARN] base64_encode_block contains irreducible loops!
[WARN] base64_decode_block contains irreducible loops!
[INFO] Start preprocessing the input bitcode ... Done!
[INFO] Z3 version: 4.8.16.0 b0605a9d364d4d89e42713dd60baec604981aea2 NOTFOUND
[INFO] Lifting the protocol...
[INFO] Step 1: Abstract interpreting the code...
[INFO] Processing pardiff_main_message@0
[INFO] Processing  parse_packet@0
[INFO] Processing   babel_get_if_nfo.408@0
[INFO] >Returning   babel_get_if_nfo.408@0
[INFO] Processing   babel_packet_examin@0
[INFO] Processing    select.6@0
[INFO] >Returning    select.6@0
[INFO] Processing    select.6@1
[INFO] >Returning    select.6@1
[INFO] Processing    select.6@2
[INFO] >Returning    select.6@2
[INFO] Processing    select.6@3
[INFO] >Returning    select.6@3
[INFO] >Returning   babel_packet_examin@0
[INFO] Processing   babel_get_if_nfo.408@1
[INFO] >Returning   babel_get_if_nfo.408@1
[INFO] Processing   babel_get_if_nfo.408@2
[INFO] >Returning   babel_get_if_nfo.408@2
[INFO] Processing   parse_update_subtlv@0
[WARN] Try to memcpy the message buff of a variable length!
[WARN] Try to memcpy the message buff of a variable length!
[INFO] >Returning   parse_update_subtlv@0
[INFO] Processing   network_address@0
[INFO] >Returning   network_address@0
[INFO] Processing   network_address@1
[INFO] >Returning   network_address@1
[INFO] Processing   is_interface_ll_address@0
[INFO] Processing    if_up@0
[INFO] Processing     if_is_operative@0
[INFO] >Returning     if_is_operative@0
[INFO] Processing     babel_get_if_nfo.20@0
[INFO] >Returning     babel_get_if_nfo.20@0
[INFO] >Returning    if_up@0
[INFO] >Returning   is_interface_ll_address@0
[INFO] Processing   parse_ihu_subtlv@0
[INFO] >Returning   parse_ihu_subtlv@0
[INFO] Processing   parse_hello_subtlv@0
[INFO] >Returning   parse_hello_subtlv@0
[INFO] Processing   babel_get_if_nfo.408@3
[INFO] >Returning   babel_get_if_nfo.408@3
[INFO] Processing   babel_get_if_nfo.408@4
[INFO] >Returning   babel_get_if_nfo.408@4
[INFO] Processing   babel_get_if_nfo.408@5
[INFO] >Returning   babel_get_if_nfo.408@5
[INFO] Processing   parse_update_subtlv@1
[WARN] Try to memcpy the message buff of a variable length!
[WARN] Try to memcpy the message buff of a variable length!
[INFO] >Returning   parse_update_subtlv@1
[INFO] Processing   network_address@2
[INFO] >Returning   network_address@2
[INFO] Processing   network_address@3
[INFO] >Returning   network_address@3
[INFO] Processing   is_interface_ll_address@1
[INFO] Processing    if_up@1
[INFO] Processing     if_is_operative@1
[INFO] >Returning     if_is_operative@1
[INFO] Processing     babel_get_if_nfo.20@1
[INFO] >Returning     babel_get_if_nfo.20@1
[INFO] >Returning    if_up@1
[INFO] >Returning   is_interface_ll_address@1
[INFO] Processing   parse_ihu_subtlv@1
[INFO] >Returning   parse_ihu_subtlv@1
[INFO] Processing   parse_hello_subtlv@1
[INFO] >Returning   parse_hello_subtlv@1
[INFO] Processing   valid_rtt@0
[INFO] >Returning   valid_rtt@0
[INFO] >Returning  parse_packet@0
[INFO] >Returning pardiff_main_message@0
[INFO] Step 1: Abstract interpreting the code takes 229s!
[INFO] Step 2: Executing on the slice...
[INFO] Slice Size: 788
[INFO] Slice Size: 424
[INFO] Step 2: Executing on the slice takes 313ms!
[INFO] Step 3: Generating BNF...
[INFO] Slice Size: 1997
[INFO] Slice Size: 172
[INFO] Step 3: Generating BNF takes 453ms!
[INFO] Lifting the protocol takes 230s!
[INFO] Start preprocessing the diff of two programs 
[INFO] Start to get BNF for the first implementation ... Done!
[INFO] Start preprocessing the input bitcode ... 
[INFO] Start preprocessing the input bitcode ... Done!
[INFO] Z3 version: 4.8.16.0 b0605a9d364d4d89e42713dd60baec604981aea2 NOTFOUND
[INFO] Lifting the protocol...
[INFO] Step 1: Abstract interpreting the code...
[INFO] Processing pardiff_main_message@0
[INFO] Processing  parse_packet@0
[INFO] Processing   ae_is_v4@0
[INFO] >Returning   ae_is_v4@0
[INFO] Processing   v4tov6@0
[INFO] >Returning   v4tov6@0
[INFO] Processing   ae_is_v4@1
[INFO] >Returning   ae_is_v4@1
[INFO] Processing   v4mapped@0
[INFO] >Returning   v4mapped@0
[INFO] Processing   ae_is_v4@2
[INFO] >Returning   ae_is_v4@2
[INFO] Processing   ae_is_v4@3
[INFO] >Returning   ae_is_v4@3
[INFO] Processing   v4tov6@1
[INFO] >Returning   v4tov6@1
[INFO] Processing   ae_is_v4@4
[INFO] >Returning   ae_is_v4@4
[INFO] Processing   v4mapped@1
[INFO] >Returning   v4mapped@1
[INFO] Processing   ae_is_v4@5
[INFO] >Returning   ae_is_v4@5
[INFO] Processing   v4tov6@2
[INFO] >Returning   v4tov6@2
[INFO] Processing   ae_is_v4@6
[INFO] >Returning   ae_is_v4@6
[INFO] Processing   ae_is_v4@7
[INFO] >Returning   ae_is_v4@7
[INFO] Processing   ae_is_v4@8
[INFO] >Returning   ae_is_v4@8
[INFO] Processing   v4mapped@2
[INFO] >Returning   v4mapped@2
[INFO] Processing   parse_other_subtlv@0
[INFO] >Returning   parse_other_subtlv@0
[INFO] Processing   parse_other_subtlv@1
[INFO] >Returning   parse_other_subtlv@1
[INFO] Processing   interface_ll_address@0
[INFO] >Returning   interface_ll_address@0
[INFO] Processing   parse_other_subtlv@2
[INFO] >Returning   parse_other_subtlv@2
[INFO] Processing   parse_other_subtlv@3
[INFO] >Returning   parse_other_subtlv@3
[INFO] Processing   valid_rtt@0
[INFO] >Returning   valid_rtt@0
[INFO] >Returning  parse_packet@0
[INFO] >Returning pardiff_main_message@0
[INFO] Step 1: Abstract interpreting the code takes 21s!
[INFO] Step 2: Executing on the slice...
[INFO] Slice Size: 1743
[INFO] Slice Size: 882
[INFO] Step 2: Executing on the slice takes 1s!
[INFO] Step 3: Generating BNF...
[INFO] Slice Size: 5848
[INFO] Slice Size: 228
[INFO] Step 3: Generating BNF takes 242ms!
[INFO] Lifting the protocol takes 22s!
[INFO] Start preprocessing the diff of two programs 
[INFO] Start to get BNF for the first implementation ... Done!
[INFO] Start to get BNF for the second implementation ... Done!
[INFO] Start to get BNF for the first implementation ... Done!
[INFO] Generate FSM1...
[INFO] Generate FSM1 takes 112s!
[INFO] Generate FSM2...
[INFO] Generate FSM2 takes 11s!
[INFO] FSM diff...
[INFO] FSM diff takes 6s!

Is this right? How to inspect these results?

[grandnew]

@zmw12306 Hi?

[zmw12306]

The log you show is just a summary of the ParDiff execution. In the complete diff.txt, there should be something like: "start to bisimulation
start new group:
start new group:
start new group:
diff: in F1 not in F2: while compair state_3 and state_2626: state_3 -> state_23:2 ≤ B[2]B[3] && 2 + B[5] ≤ B[2]B[3] && NOT(4 + B[5] ≤ B[2]B[3]) && NOT(B[2]B[3] ≤ 2 + B[5]) && 4 + B[2]B[3] ≤ len
... " That's the diff detected by bisimulation.

[grandnew]

@zmw12306 Hi, thanks for the reply. But the complete diff.txt I got is shown as above. I didn't get the content you mentioned.

Are there any additional instructions I need to conduct, apart from those described in the README?