|
|
|
@ -1,93 +1,156 @@
|
|
|
|
|
digraph iCFG {
|
|
|
|
|
24 [label="24: DeclStmt \n _fun_X_X(&x:class X *) [line 35]\n " shape="box"]
|
|
|
|
|
41 [label="41: BinaryOperatorStmt: Assign \n n$2=*&z:class Z * [line 67]\n *n$2.f:int =0 [line 67]\n REMOVE_TEMPS(n$2); [line 67]\n " shape="box"]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
24 -> 23 ;
|
|
|
|
|
23 [label="23: BinaryOperatorStmt: Assign \n *&x.y:class Y *=null [line 36]\n " shape="box"]
|
|
|
|
|
41 -> 40 ;
|
|
|
|
|
40 [label="40: Return Stmt \n n$0=*&z:class Z * [line 68]\n n$1=_fun_Z_getF(n$0:class Z *) [line 68]\n *&return:int =(1 / n$1) [line 68]\n REMOVE_TEMPS(n$0,n$1); [line 68]\n NULLIFY(&z,false); [line 68]\n APPLY_ABSTRACTION; [line 68]\n " shape="box"]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
23 -> 22 ;
|
|
|
|
|
22 [label="22: BinaryOperatorStmt: Assign \n *&x.f:int =0 [line 37]\n " shape="box"]
|
|
|
|
|
40 -> 39 ;
|
|
|
|
|
39 [label="39: Exit Z_ptr_div0 \n " color=yellow style=filled]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
22 -> 19 ;
|
|
|
|
|
22 -> 20 ;
|
|
|
|
|
21 [label="21: Return Stmt \n *&return:int =1 [line 39]\n NULLIFY(&x,false); [line 39]\n APPLY_ABSTRACTION; [line 39]\n " shape="box"]
|
|
|
|
|
38 [label="38: Start Z_ptr_div0\nFormals: z:class Z *\nLocals: \n DECLARE_LOCALS(&return); [line 63]\n " color=yellow style=filled]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
21 -> 16 ;
|
|
|
|
|
20 [label="20: Prune (false branch) \n n$1=*&x.y:class Y * [line 38]\n PRUNE((n$1 == 0), false); [line 38]\n REMOVE_TEMPS(n$1); [line 38]\n " shape="invhouse"]
|
|
|
|
|
38 -> 41 ;
|
|
|
|
|
37 [label="37: DeclStmt \n _fun_Z_Z(&z:class Z *) [line 58]\n " shape="box"]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
20 -> 18 ;
|
|
|
|
|
19 [label="19: Prune (true branch) \n n$1=*&x.y:class Y * [line 38]\n PRUNE((n$1 != 0), true); [line 38]\n REMOVE_TEMPS(n$1); [line 38]\n " shape="invhouse"]
|
|
|
|
|
37 -> 36 ;
|
|
|
|
|
36 [label="36: BinaryOperatorStmt: Assign \n *&z.f:int =0 [line 59]\n " shape="box"]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
19 -> 21 ;
|
|
|
|
|
18 [label="18: + \n " ]
|
|
|
|
|
36 -> 35 ;
|
|
|
|
|
35 [label="35: Return Stmt \n n$0=_fun_Z_getF(&z:class Z &) [line 60]\n *&return:int =(1 / n$0) [line 60]\n REMOVE_TEMPS(n$0); [line 60]\n NULLIFY(&z,false); [line 60]\n APPLY_ABSTRACTION; [line 60]\n " shape="box"]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
35 -> 34 ;
|
|
|
|
|
34 [label="34: Exit Z_div0 \n " color=yellow style=filled]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
33 [label="33: Start Z_div0\nFormals: \nLocals: z:class Z \n DECLARE_LOCALS(&return,&z); [line 57]\n " color=yellow style=filled]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
33 -> 37 ;
|
|
|
|
|
32 [label="32: DeclStmt \n _fun_X_X(&x:class X *) [line 48]\n " shape="box"]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
32 -> 31 ;
|
|
|
|
|
31 [label="31: BinaryOperatorStmt: Assign \n *&x.y:class Y *=null [line 49]\n " shape="box"]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
31 -> 30 ;
|
|
|
|
|
30 [label="30: BinaryOperatorStmt: Assign \n *&x.f:int =0 [line 50]\n " shape="box"]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
30 -> 27 ;
|
|
|
|
|
30 -> 28 ;
|
|
|
|
|
29 [label="29: Return Stmt \n *&return:int =1 [line 52]\n NULLIFY(&x,false); [line 52]\n APPLY_ABSTRACTION; [line 52]\n " shape="box"]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
29 -> 24 ;
|
|
|
|
|
28 [label="28: Prune (false branch) \n n$1=*&x.y:class Y * [line 51]\n PRUNE((n$1 == 0), false); [line 51]\n REMOVE_TEMPS(n$1); [line 51]\n " shape="invhouse"]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
28 -> 26 ;
|
|
|
|
|
27 [label="27: Prune (true branch) \n n$1=*&x.y:class Y * [line 51]\n PRUNE((n$1 != 0), true); [line 51]\n REMOVE_TEMPS(n$1); [line 51]\n " shape="invhouse"]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
27 -> 29 ;
|
|
|
|
|
26 [label="26: + \n " ]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
26 -> 25 ;
|
|
|
|
|
25 [label="25: Return Stmt \n n$0=_fun_X_getF(&x:class X &) [line 54]\n *&return:int =(1 / n$0) [line 54]\n REMOVE_TEMPS(n$0); [line 54]\n NULLIFY(&x,false); [line 54]\n APPLY_ABSTRACTION; [line 54]\n " shape="box"]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
25 -> 24 ;
|
|
|
|
|
24 [label="24: Exit X_Y_div0 \n " color=yellow style=filled]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
23 [label="23: Start X_Y_div0\nFormals: \nLocals: x:class X \n DECLARE_LOCALS(&return,&x); [line 47]\n " color=yellow style=filled]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
23 -> 32 ;
|
|
|
|
|
22 [label="22: BinaryOperatorStmt: Assign \n n$2=*&x:class X * [line 43]\n *n$2.f:int =0 [line 43]\n REMOVE_TEMPS(n$2); [line 43]\n " shape="box"]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
22 -> 21 ;
|
|
|
|
|
21 [label="21: Return Stmt \n n$0=*&x:class X * [line 44]\n n$1=_fun_X_getF(n$0:class X *) [line 44]\n *&return:int =(1 / n$1) [line 44]\n REMOVE_TEMPS(n$0,n$1); [line 44]\n NULLIFY(&x,false); [line 44]\n APPLY_ABSTRACTION; [line 44]\n " shape="box"]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
21 -> 20 ;
|
|
|
|
|
20 [label="20: Exit X_ptr_div0 \n " color=yellow style=filled]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
19 [label="19: Start X_ptr_div0\nFormals: x:class X *\nLocals: \n DECLARE_LOCALS(&return); [line 42]\n " color=yellow style=filled]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
19 -> 22 ;
|
|
|
|
|
18 [label="18: DeclStmt \n _fun_X_X(&x:class X *) [line 37]\n " shape="box"]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
18 -> 17 ;
|
|
|
|
|
17 [label="17: Return Stmt \n n$0=_fun_X_getF(&x:class X &) [line 41]\n *&return:int =(1 / n$0) [line 41]\n REMOVE_TEMPS(n$0); [line 41]\n NULLIFY(&x,false); [line 41]\n APPLY_ABSTRACTION; [line 41]\n " shape="box"]
|
|
|
|
|
17 [label="17: BinaryOperatorStmt: Assign \n *&x.f:int =0 [line 38]\n " shape="box"]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
17 -> 16 ;
|
|
|
|
|
16 [label="16: Exit X_Y_div0 \n " color=yellow style=filled]
|
|
|
|
|
16 [label="16: Return Stmt \n n$0=_fun_X_getF(&x:class X &) [line 39]\n *&return:int =(1 / n$0) [line 39]\n REMOVE_TEMPS(n$0); [line 39]\n NULLIFY(&x,false); [line 39]\n APPLY_ABSTRACTION; [line 39]\n " shape="box"]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
15 [label="15: Start X_Y_div0\nFormals: \nLocals: x:class X \n DECLARE_LOCALS(&return,&x); [line 34]\n " color=yellow style=filled]
|
|
|
|
|
16 -> 15 ;
|
|
|
|
|
15 [label="15: Exit X_div0 \n " color=yellow style=filled]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
15 -> 24 ;
|
|
|
|
|
14 [label="14: BinaryOperatorStmt: Assign \n n$2=*&x:class X * [line 30]\n *n$2.f:int =0 [line 30]\n REMOVE_TEMPS(n$2); [line 30]\n " shape="box"]
|
|
|
|
|
14 [label="14: Start X_div0\nFormals: \nLocals: x:class X \n DECLARE_LOCALS(&return,&x); [line 36]\n " color=yellow style=filled]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
14 -> 13 ;
|
|
|
|
|
13 [label="13: Return Stmt \n n$0=*&x:class X * [line 31]\n n$1=_fun_X_getF(n$0:class X *) [line 31]\n *&return:int =(1 / n$1) [line 31]\n REMOVE_TEMPS(n$0,n$1); [line 31]\n NULLIFY(&x,false); [line 31]\n APPLY_ABSTRACTION; [line 31]\n " shape="box"]
|
|
|
|
|
14 -> 18 ;
|
|
|
|
|
13 [label="13: Exit Z_Z \n " color=yellow style=filled]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
13 -> 12 ;
|
|
|
|
|
12 [label="12: Exit X_ptr_div0 \n " color=yellow style=filled]
|
|
|
|
|
12 [label="12: Start Z_Z\nFormals: this:class Z *\nLocals: \n DECLARE_LOCALS(&return); [line 28]\n NULLIFY(&this,false); [line 28]\n " color=yellow style=filled]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
11 [label="11: Start X_ptr_div0\nFormals: x:class X *\nLocals: \n DECLARE_LOCALS(&return); [line 29]\n " color=yellow style=filled]
|
|
|
|
|
12 -> 13 ;
|
|
|
|
|
11 [label="11: Return Stmt \n n$0=*&this:class Z * [line 30]\n n$1=*n$0.f:int [line 30]\n *&return:int =n$1 [line 30]\n REMOVE_TEMPS(n$0,n$1); [line 30]\n NULLIFY(&this,false); [line 30]\n APPLY_ABSTRACTION; [line 30]\n " shape="box"]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
11 -> 14 ;
|
|
|
|
|
10 [label="10: DeclStmt \n _fun_X_X(&x:class X *) [line 24]\n " shape="box"]
|
|
|
|
|
11 -> 10 ;
|
|
|
|
|
10 [label="10: Exit Z_getF \n " color=yellow style=filled]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
10 -> 9 ;
|
|
|
|
|
9 [label="9: BinaryOperatorStmt: Assign \n *&x.f:int =0 [line 25]\n " shape="box"]
|
|
|
|
|
9 [label="9: Start Z_getF\nFormals: this:class Z *\nLocals: \n DECLARE_LOCALS(&return); [line 30]\n " color=yellow style=filled]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
9 -> 8 ;
|
|
|
|
|
8 [label="8: Return Stmt \n n$0=_fun_X_getF(&x:class X &) [line 26]\n *&return:int =(1 / n$0) [line 26]\n REMOVE_TEMPS(n$0); [line 26]\n NULLIFY(&x,false); [line 26]\n APPLY_ABSTRACTION; [line 26]\n " shape="box"]
|
|
|
|
|
9 -> 11 ;
|
|
|
|
|
8 [label="8: DeclStmt \n n$0=*&z1:class Z * [line 25]\n *&z2:class Z *=n$0 [line 25]\n REMOVE_TEMPS(n$0); [line 25]\n NULLIFY(&z1,false); [line 25]\n NULLIFY(&z2,false); [line 25]\n APPLY_ABSTRACTION; [line 25]\n " shape="box"]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
8 -> 7 ;
|
|
|
|
|
7 [label="7: Exit X_div0 \n " color=yellow style=filled]
|
|
|
|
|
7 [label="7: Exit fun_with_Z \n " color=yellow style=filled]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
6 [label="6: Start X_div0\nFormals: \nLocals: x:class X \n DECLARE_LOCALS(&return,&x); [line 23]\n " color=yellow style=filled]
|
|
|
|
|
6 [label="6: Start fun_with_Z\nFormals: z1:class Z *\nLocals: z2:class Z * \n DECLARE_LOCALS(&return,&z2); [line 24]\n NULLIFY(&z2,false); [line 24]\n " color=yellow style=filled]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
6 -> 10 ;
|
|
|
|
|
6 -> 8 ;
|
|
|
|
|
5 [label="5: Exit X_X \n " color=yellow style=filled]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
4 [label="4: Start X_X\nFormals: this:class X *\nLocals: \n DECLARE_LOCALS(&return); [line 14]\n NULLIFY(&this,false); [line 14]\n " color=yellow style=filled]
|
|
|
|
|
4 [label="4: Start X_X\nFormals: this:class X *\nLocals: \n DECLARE_LOCALS(&return); [line 17]\n NULLIFY(&this,false); [line 17]\n " color=yellow style=filled]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
4 -> 5 ;
|
|
|
|
|
3 [label="3: Return Stmt \n n$0=*&this:class X * [line 16]\n n$1=*n$0.f:int [line 16]\n *&return:int =n$1 [line 16]\n REMOVE_TEMPS(n$0,n$1); [line 16]\n NULLIFY(&this,false); [line 16]\n APPLY_ABSTRACTION; [line 16]\n " shape="box"]
|
|
|
|
|
3 [label="3: Return Stmt \n n$0=*&this:class X * [line 19]\n n$1=*n$0.f:int [line 19]\n *&return:int =n$1 [line 19]\n REMOVE_TEMPS(n$0,n$1); [line 19]\n NULLIFY(&this,false); [line 19]\n APPLY_ABSTRACTION; [line 19]\n " shape="box"]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
3 -> 2 ;
|
|
|
|
|
2 [label="2: Exit X_getF \n " color=yellow style=filled]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
1 [label="1: Start X_getF\nFormals: this:class X *\nLocals: \n DECLARE_LOCALS(&return); [line 16]\n " color=yellow style=filled]
|
|
|
|
|
1 [label="1: Start X_getF\nFormals: this:class X *\nLocals: \n DECLARE_LOCALS(&return); [line 19]\n " color=yellow style=filled]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
1 -> 3 ;
|
|
|
|
|