digraph iCFG { 19 [label="19: DeclStmt \n *&foo_g:int =(2 + 10) [line 23]\n " shape="box"] 19 -> 18 ; 18 [label="18: DeclStmt \n *&foo_a:int =0 [line 24]\n " shape="box"] 18 -> 13 ; 17 [label="17: Return Stmt \n NULLIFY(&foo_a,false); [line 27]\n NULLIFY(&foo_g,false); [line 27]\n *&return:int =0 [line 27]\n APPLY_ABSTRACTION; [line 27]\n " shape="box"] 17 -> 11 ; 16 [label="16: Return Stmt \n n$1=*&foo_g:int [line 26]\n n$2=*&foo_a:int [line 26]\n *&return:int =(n$1 / n$2) [line 26]\n REMOVE_TEMPS(n$1,n$2); [line 26]\n NULLIFY(&foo_a,false); [line 26]\n NULLIFY(&foo_g,false); [line 26]\n APPLY_ABSTRACTION; [line 26]\n " shape="box"] 16 -> 11 ; 15 [label="15: Prune (false branch) \n PRUNE(((n$0 == 12) == 0), false); [line 25]\n REMOVE_TEMPS(n$0); [line 25]\n " shape="invhouse"] 15 -> 17 ; 14 [label="14: Prune (true branch) \n PRUNE(((n$0 == 12) != 0), true); [line 25]\n REMOVE_TEMPS(n$0); [line 25]\n " shape="invhouse"] 14 -> 16 ; 13 [label="13: BinaryOperatorStmt: EQ \n n$0=*&foo_g:int [line 25]\n " shape="box"] 13 -> 14 ; 13 -> 15 ; 12 [label="12: + \n NULLIFY(&foo_a,false); [line 25]\n NULLIFY(&foo_g,false); [line 25]\n " ] 12 -> 11 ; 11 [label="11: Exit test \n " color=yellow style=filled] 10 [label="10: Start test\nFormals: \nLocals: foo_a:int foo_g:int \n DECLARE_LOCALS(&return,&foo_a,&foo_g); [line 22]\n NULLIFY(&foo_a,false); [line 22]\n NULLIFY(&foo_g,false); [line 22]\n " color=yellow style=filled] 10 -> 19 ; 9 [label="9: DeclStmt \n *&foo_a:int =0 [line 13]\n NULLIFY(&foo_a,false); [line 13]\n " shape="box"] 9 -> 8 ; 8 [label="8: DeclStmt \n *&foo_b:int =1 [line 14]\n NULLIFY(&foo_b,false); [line 14]\n " shape="box"] 8 -> 7 ; 7 [label="7: DeclStmt \n *&foo_c:int =10 [line 15]\n NULLIFY(&foo_c,false); [line 15]\n " shape="box"] 7 -> 6 ; 6 [label="6: DeclStmt \n *&foo_d:int =11 [line 16]\n NULLIFY(&foo_d,false); [line 16]\n " shape="box"] 6 -> 5 ; 5 [label="5: DeclStmt \n *&foo_e:int =1 [line 17]\n NULLIFY(&foo_e,false); [line 17]\n " shape="box"] 5 -> 4 ; 4 [label="4: DeclStmt \n *&foo_f:int =2 [line 18]\n NULLIFY(&foo_f,false); [line 18]\n " shape="box"] 4 -> 3 ; 3 [label="3: DeclStmt \n *&foo_g:int =(2 + 10) [line 19]\n NULLIFY(&foo_g,false); [line 19]\n APPLY_ABSTRACTION; [line 19]\n " shape="box"] 3 -> 2 ; 2 [label="2: Exit main \n " color=yellow style=filled] 1 [label="1: Start main\nFormals: \nLocals: foo_g:int foo_f:int foo_e:int foo_d:int foo_c:int foo_b:int foo_a:int \n DECLARE_LOCALS(&return,&foo_g,&foo_f,&foo_e,&foo_d,&foo_c,&foo_b,&foo_a); [line 12]\n NULLIFY(&foo_a,false); [line 12]\n NULLIFY(&foo_b,false); [line 12]\n NULLIFY(&foo_c,false); [line 12]\n NULLIFY(&foo_d,false); [line 12]\n NULLIFY(&foo_e,false); [line 12]\n NULLIFY(&foo_f,false); [line 12]\n NULLIFY(&foo_g,false); [line 12]\n " color=yellow style=filled] 1 -> 9 ; }