|
|
@ -3,11 +3,11 @@ digraph iCFG {
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
195 -> 186 ;
|
|
|
|
195 -> 186 ;
|
|
|
|
194 [label="194: Prune (false branch) \n PRUNE(((n$3 == 0) == 0), false); [line 194]\n APPLY_ABSTRACTION; [line 194]\n " shape="invhouse"]
|
|
|
|
194 [label="194: Prune (false branch) \n PRUNE(((n$3 == 0) == 0), false); [line 194]\n REMOVE_TEMPS(n$3); [line 194]\n APPLY_ABSTRACTION; [line 194]\n " shape="invhouse"]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
194 -> 184 ;
|
|
|
|
194 -> 184 ;
|
|
|
|
193 [label="193: Prune (true branch) \n PRUNE(((n$3 == 0) != 0), true); [line 194]\n " shape="invhouse"]
|
|
|
|
193 [label="193: Prune (true branch) \n PRUNE(((n$3 == 0) != 0), true); [line 194]\n REMOVE_TEMPS(n$3); [line 194]\n " shape="invhouse"]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
193 -> 192 ;
|
|
|
|
193 -> 192 ;
|
|
|
@ -15,7 +15,7 @@ digraph iCFG {
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
192 -> 184 ;
|
|
|
|
192 -> 184 ;
|
|
|
|
191 [label="191: Switch_stmt \n n$2=*&SIL_temp_conditional___n$0:int [line 193]\n *&value:int =n$2 [line 193]\n n$3=*&value:int [line 193]\n NULLIFY(&SIL_temp_conditional___n$0); [line 193]\n NULLIFY(&value); [line 193]\n " shape="box"]
|
|
|
|
191 [label="191: Switch_stmt \n n$2=*&SIL_temp_conditional___n$0:int [line 193]\n *&value:int =n$2 [line 193]\n n$3=*&value:int [line 193]\n REMOVE_TEMPS(n$2); [line 193]\n NULLIFY(&SIL_temp_conditional___n$0); [line 193]\n NULLIFY(&value); [line 193]\n " shape="box"]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
191 -> 193 ;
|
|
|
|
191 -> 193 ;
|
|
|
@ -45,7 +45,7 @@ digraph iCFG {
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
185 -> 191 ;
|
|
|
|
185 -> 191 ;
|
|
|
|
184 [label="184: Return Stmt \n *&return:int =0 [line 197]\n REMOVE_TEMPS(n$2,n$3); [line 197]\n APPLY_ABSTRACTION; [line 197]\n " shape="box"]
|
|
|
|
184 [label="184: Return Stmt \n *&return:int =0 [line 197]\n APPLY_ABSTRACTION; [line 197]\n " shape="box"]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
184 -> 183 ;
|
|
|
|
184 -> 183 ;
|
|
|
@ -60,11 +60,11 @@ digraph iCFG {
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
181 -> 180 ;
|
|
|
|
181 -> 180 ;
|
|
|
|
180 [label="180: Switch_stmt \n *&value:int =7 [line 187]\n n$0=*&value:int [line 187]\n NULLIFY(&value); [line 187]\n " shape="box"]
|
|
|
|
180 [label="180: Switch_stmt \n *&value:int =7 [line 187]\n n$0=*&value:int [line 187]\n REMOVE_TEMPS(n$0); [line 187]\n NULLIFY(&value); [line 187]\n " shape="box"]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
180 -> 179 ;
|
|
|
|
180 -> 179 ;
|
|
|
|
179 [label="179: Return Stmt \n *&return:int =0 [line 188]\n REMOVE_TEMPS(n$0); [line 188]\n APPLY_ABSTRACTION; [line 188]\n " shape="box"]
|
|
|
|
179 [label="179: Return Stmt \n *&return:int =0 [line 188]\n APPLY_ABSTRACTION; [line 188]\n " shape="box"]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
179 -> 178 ;
|
|
|
|
179 -> 178 ;
|
|
|
@ -79,11 +79,11 @@ digraph iCFG {
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
176 -> 175 ;
|
|
|
|
176 -> 175 ;
|
|
|
|
175 [label="175: Switch_stmt \n n$0=*&value:int [line 181]\n NULLIFY(&value); [line 181]\n " shape="box"]
|
|
|
|
175 [label="175: Switch_stmt \n n$0=*&value:int [line 181]\n REMOVE_TEMPS(n$0); [line 181]\n NULLIFY(&value); [line 181]\n " shape="box"]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
175 -> 174 ;
|
|
|
|
175 -> 174 ;
|
|
|
|
174 [label="174: Return Stmt \n *&return:int =0 [line 182]\n REMOVE_TEMPS(n$0); [line 182]\n APPLY_ABSTRACTION; [line 182]\n " shape="box"]
|
|
|
|
174 [label="174: Return Stmt \n *&return:int =0 [line 182]\n APPLY_ABSTRACTION; [line 182]\n " shape="box"]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
174 -> 173 ;
|
|
|
|
174 -> 173 ;
|
|
|
@ -103,7 +103,7 @@ digraph iCFG {
|
|
|
|
|
|
|
|
|
|
|
|
170 -> 165 ;
|
|
|
|
170 -> 165 ;
|
|
|
|
170 -> 166 ;
|
|
|
|
170 -> 166 ;
|
|
|
|
169 [label="169: Prune (true branch) \n PRUNE(((n$3 == 0) != 0), true); [line 161]\n NULLIFY(&value); [line 161]\n " shape="invhouse"]
|
|
|
|
169 [label="169: Prune (true branch) \n PRUNE(((n$3 == 0) != 0), true); [line 161]\n REMOVE_TEMPS(n$3); [line 161]\n NULLIFY(&value); [line 161]\n " shape="invhouse"]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
169 -> 168 ;
|
|
|
|
169 -> 168 ;
|
|
|
@ -120,7 +120,7 @@ digraph iCFG {
|
|
|
|
|
|
|
|
|
|
|
|
166 -> 160 ;
|
|
|
|
166 -> 160 ;
|
|
|
|
166 -> 161 ;
|
|
|
|
166 -> 161 ;
|
|
|
|
165 [label="165: Prune (true branch) \n PRUNE(((n$3 == 1) != 0), true); [line 164]\n " shape="invhouse"]
|
|
|
|
165 [label="165: Prune (true branch) \n PRUNE(((n$3 == 1) != 0), true); [line 164]\n REMOVE_TEMPS(n$3); [line 164]\n " shape="invhouse"]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
165 -> 164 ;
|
|
|
|
165 -> 164 ;
|
|
|
@ -141,15 +141,15 @@ digraph iCFG {
|
|
|
|
|
|
|
|
|
|
|
|
161 -> 158 ;
|
|
|
|
161 -> 158 ;
|
|
|
|
161 -> 159 ;
|
|
|
|
161 -> 159 ;
|
|
|
|
160 [label="160: Prune (true branch) \n PRUNE(((n$3 == 2) != 0), true); [line 170]\n APPLY_ABSTRACTION; [line 170]\n " shape="invhouse"]
|
|
|
|
160 [label="160: Prune (true branch) \n PRUNE(((n$3 == 2) != 0), true); [line 170]\n REMOVE_TEMPS(n$3); [line 170]\n APPLY_ABSTRACTION; [line 170]\n " shape="invhouse"]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
160 -> 150 ;
|
|
|
|
160 -> 150 ;
|
|
|
|
159 [label="159: Prune (false branch) \n PRUNE(((n$3 == 3) == 0), false); [line 171]\n APPLY_ABSTRACTION; [line 171]\n " shape="invhouse"]
|
|
|
|
159 [label="159: Prune (false branch) \n PRUNE(((n$3 == 3) == 0), false); [line 171]\n REMOVE_TEMPS(n$3); [line 171]\n APPLY_ABSTRACTION; [line 171]\n " shape="invhouse"]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
159 -> 150 ;
|
|
|
|
159 -> 150 ;
|
|
|
|
158 [label="158: Prune (true branch) \n PRUNE(((n$3 == 3) != 0), true); [line 171]\n APPLY_ABSTRACTION; [line 171]\n " shape="invhouse"]
|
|
|
|
158 [label="158: Prune (true branch) \n PRUNE(((n$3 == 3) != 0), true); [line 171]\n REMOVE_TEMPS(n$3); [line 171]\n APPLY_ABSTRACTION; [line 171]\n " shape="invhouse"]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
158 -> 150 ;
|
|
|
|
158 -> 150 ;
|
|
|
@ -183,7 +183,7 @@ digraph iCFG {
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
151 -> 157 ;
|
|
|
|
151 -> 157 ;
|
|
|
|
150 [label="150: DeclStmt \n *&a:int =0 [line 174]\n REMOVE_TEMPS(n$3); [line 174]\n NULLIFY(&a); [line 174]\n APPLY_ABSTRACTION; [line 174]\n " shape="box"]
|
|
|
|
150 [label="150: DeclStmt \n *&a:int =0 [line 174]\n NULLIFY(&a); [line 174]\n APPLY_ABSTRACTION; [line 174]\n " shape="box"]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
150 -> 146 ;
|
|
|
|
150 -> 146 ;
|
|
|
@ -224,7 +224,7 @@ digraph iCFG {
|
|
|
|
|
|
|
|
|
|
|
|
141 -> 137 ;
|
|
|
|
141 -> 137 ;
|
|
|
|
141 -> 138 ;
|
|
|
|
141 -> 138 ;
|
|
|
|
140 [label="140: Prune (true branch) \n PRUNE(((n$0 == 0) != 0), true); [line 142]\n " shape="invhouse"]
|
|
|
|
140 [label="140: Prune (true branch) \n PRUNE(((n$0 == 0) != 0), true); [line 142]\n REMOVE_TEMPS(n$0); [line 142]\n " shape="invhouse"]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
140 -> 139 ;
|
|
|
|
140 -> 139 ;
|
|
|
@ -237,7 +237,7 @@ digraph iCFG {
|
|
|
|
|
|
|
|
|
|
|
|
138 -> 132 ;
|
|
|
|
138 -> 132 ;
|
|
|
|
138 -> 133 ;
|
|
|
|
138 -> 133 ;
|
|
|
|
137 [label="137: Prune (true branch) \n PRUNE(((n$0 == 1) != 0), true); [line 145]\n " shape="invhouse"]
|
|
|
|
137 [label="137: Prune (true branch) \n PRUNE(((n$0 == 1) != 0), true); [line 145]\n REMOVE_TEMPS(n$0); [line 145]\n " shape="invhouse"]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
137 -> 136 ;
|
|
|
|
137 -> 136 ;
|
|
|
@ -258,15 +258,15 @@ digraph iCFG {
|
|
|
|
|
|
|
|
|
|
|
|
133 -> 130 ;
|
|
|
|
133 -> 130 ;
|
|
|
|
133 -> 131 ;
|
|
|
|
133 -> 131 ;
|
|
|
|
132 [label="132: Prune (true branch) \n PRUNE(((n$0 == 2) != 0), true); [line 150]\n APPLY_ABSTRACTION; [line 150]\n " shape="invhouse"]
|
|
|
|
132 [label="132: Prune (true branch) \n PRUNE(((n$0 == 2) != 0), true); [line 150]\n REMOVE_TEMPS(n$0); [line 150]\n APPLY_ABSTRACTION; [line 150]\n " shape="invhouse"]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
132 -> 128 ;
|
|
|
|
132 -> 128 ;
|
|
|
|
131 [label="131: Prune (false branch) \n PRUNE(((n$0 == 3) == 0), false); [line 151]\n APPLY_ABSTRACTION; [line 151]\n " shape="invhouse"]
|
|
|
|
131 [label="131: Prune (false branch) \n PRUNE(((n$0 == 3) == 0), false); [line 151]\n REMOVE_TEMPS(n$0); [line 151]\n APPLY_ABSTRACTION; [line 151]\n " shape="invhouse"]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
131 -> 128 ;
|
|
|
|
131 -> 128 ;
|
|
|
|
130 [label="130: Prune (true branch) \n PRUNE(((n$0 == 3) != 0), true); [line 151]\n APPLY_ABSTRACTION; [line 151]\n " shape="invhouse"]
|
|
|
|
130 [label="130: Prune (true branch) \n PRUNE(((n$0 == 3) != 0), true); [line 151]\n REMOVE_TEMPS(n$0); [line 151]\n APPLY_ABSTRACTION; [line 151]\n " shape="invhouse"]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
130 -> 128 ;
|
|
|
|
130 -> 128 ;
|
|
|
@ -275,7 +275,7 @@ digraph iCFG {
|
|
|
|
|
|
|
|
|
|
|
|
129 -> 140 ;
|
|
|
|
129 -> 140 ;
|
|
|
|
129 -> 141 ;
|
|
|
|
129 -> 141 ;
|
|
|
|
128 [label="128: Return Stmt \n *&return:int =0 [line 154]\n REMOVE_TEMPS(n$0); [line 154]\n APPLY_ABSTRACTION; [line 154]\n " shape="box"]
|
|
|
|
128 [label="128: Return Stmt \n *&return:int =0 [line 154]\n APPLY_ABSTRACTION; [line 154]\n " shape="box"]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
128 -> 127 ;
|
|
|
|
128 -> 127 ;
|
|
|
@ -306,7 +306,7 @@ digraph iCFG {
|
|
|
|
|
|
|
|
|
|
|
|
121 -> 117 ;
|
|
|
|
121 -> 117 ;
|
|
|
|
121 -> 118 ;
|
|
|
|
121 -> 118 ;
|
|
|
|
120 [label="120: Prune (true branch) \n PRUNE(((n$2 == 0) != 0), true); [line 122]\n " shape="invhouse"]
|
|
|
|
120 [label="120: Prune (true branch) \n PRUNE(((n$2 == 0) != 0), true); [line 122]\n REMOVE_TEMPS(n$2); [line 122]\n " shape="invhouse"]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
120 -> 119 ;
|
|
|
|
120 -> 119 ;
|
|
|
@ -319,7 +319,7 @@ digraph iCFG {
|
|
|
|
|
|
|
|
|
|
|
|
118 -> 112 ;
|
|
|
|
118 -> 112 ;
|
|
|
|
118 -> 113 ;
|
|
|
|
118 -> 113 ;
|
|
|
|
117 [label="117: Prune (true branch) \n PRUNE(((n$2 == 1) != 0), true); [line 125]\n " shape="invhouse"]
|
|
|
|
117 [label="117: Prune (true branch) \n PRUNE(((n$2 == 1) != 0), true); [line 125]\n REMOVE_TEMPS(n$2); [line 125]\n " shape="invhouse"]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
117 -> 116 ;
|
|
|
|
117 -> 116 ;
|
|
|
@ -340,15 +340,15 @@ digraph iCFG {
|
|
|
|
|
|
|
|
|
|
|
|
113 -> 110 ;
|
|
|
|
113 -> 110 ;
|
|
|
|
113 -> 111 ;
|
|
|
|
113 -> 111 ;
|
|
|
|
112 [label="112: Prune (true branch) \n PRUNE(((n$2 == 2) != 0), true); [line 130]\n APPLY_ABSTRACTION; [line 130]\n " shape="invhouse"]
|
|
|
|
112 [label="112: Prune (true branch) \n PRUNE(((n$2 == 2) != 0), true); [line 130]\n REMOVE_TEMPS(n$2); [line 130]\n APPLY_ABSTRACTION; [line 130]\n " shape="invhouse"]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
112 -> 102 ;
|
|
|
|
112 -> 102 ;
|
|
|
|
111 [label="111: Prune (false branch) \n PRUNE(((n$2 == 3) == 0), false); [line 131]\n APPLY_ABSTRACTION; [line 131]\n " shape="invhouse"]
|
|
|
|
111 [label="111: Prune (false branch) \n PRUNE(((n$2 == 3) == 0), false); [line 131]\n REMOVE_TEMPS(n$2); [line 131]\n APPLY_ABSTRACTION; [line 131]\n " shape="invhouse"]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
111 -> 102 ;
|
|
|
|
111 -> 102 ;
|
|
|
|
110 [label="110: Prune (true branch) \n PRUNE(((n$2 == 3) != 0), true); [line 131]\n APPLY_ABSTRACTION; [line 131]\n " shape="invhouse"]
|
|
|
|
110 [label="110: Prune (true branch) \n PRUNE(((n$2 == 3) != 0), true); [line 131]\n REMOVE_TEMPS(n$2); [line 131]\n APPLY_ABSTRACTION; [line 131]\n " shape="invhouse"]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
110 -> 102 ;
|
|
|
|
110 -> 102 ;
|
|
|
@ -382,7 +382,7 @@ digraph iCFG {
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
103 -> 109 ;
|
|
|
|
103 -> 109 ;
|
|
|
|
102 [label="102: Return Stmt \n *&return:int =0 [line 134]\n REMOVE_TEMPS(n$2); [line 134]\n APPLY_ABSTRACTION; [line 134]\n " shape="box"]
|
|
|
|
102 [label="102: Return Stmt \n *&return:int =0 [line 134]\n APPLY_ABSTRACTION; [line 134]\n " shape="box"]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
102 -> 101 ;
|
|
|
|
102 -> 101 ;
|
|
|
@ -401,19 +401,19 @@ digraph iCFG {
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
98 -> 97 ;
|
|
|
|
98 -> 97 ;
|
|
|
|
97 [label="97: Call _fun_printf \n n$4=_fun_printf(\"(out)HELLO WORLD!\":char *) [line 108]\n REMOVE_TEMPS(n$4); [line 108]\n " shape="box"]
|
|
|
|
97 [label="97: Call _fun_printf \n n$4=_fun_printf(\"(out)HELLO WORLD!\":char *) [line 108]\n " shape="box"]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
97 -> 96 ;
|
|
|
|
97 -> 96 ;
|
|
|
|
96 [label="96: BinaryOperatorStmt: Assign \n n$3=*&value:int [line 109]\n *&x:int =(n$3 + 1) [line 109]\n REMOVE_TEMPS(n$3); [line 109]\n APPLY_ABSTRACTION; [line 109]\n " shape="box"]
|
|
|
|
96 [label="96: BinaryOperatorStmt: Assign \n n$3=*&value:int [line 109]\n *&x:int =(n$3 + 1) [line 109]\n APPLY_ABSTRACTION; [line 109]\n " shape="box"]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
96 -> 88 ;
|
|
|
|
96 -> 88 ;
|
|
|
|
95 [label="95: Prune (false branch) \n PRUNE(((n$1 == 0) == 0), false); [line 111]\n APPLY_ABSTRACTION; [line 111]\n " shape="invhouse"]
|
|
|
|
95 [label="95: Prune (false branch) \n PRUNE(((n$1 == 0) == 0), false); [line 111]\n REMOVE_TEMPS(n$1); [line 111]\n APPLY_ABSTRACTION; [line 111]\n " shape="invhouse"]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
95 -> 88 ;
|
|
|
|
95 -> 88 ;
|
|
|
|
94 [label="94: Prune (true branch) \n PRUNE(((n$1 == 0) != 0), true); [line 111]\n " shape="invhouse"]
|
|
|
|
94 [label="94: Prune (true branch) \n PRUNE(((n$1 == 0) != 0), true); [line 111]\n REMOVE_TEMPS(n$1); [line 111]\n " shape="invhouse"]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
94 -> 93 ;
|
|
|
|
94 -> 93 ;
|
|
|
@ -439,7 +439,7 @@ digraph iCFG {
|
|
|
|
|
|
|
|
|
|
|
|
89 -> 90 ;
|
|
|
|
89 -> 90 ;
|
|
|
|
89 -> 91 ;
|
|
|
|
89 -> 91 ;
|
|
|
|
88 [label="88: + \n REMOVE_TEMPS(n$1); [line 105]\n " ]
|
|
|
|
88 [label="88: + \n " ]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
88 -> 89 ;
|
|
|
|
88 -> 89 ;
|
|
|
@ -462,11 +462,11 @@ digraph iCFG {
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
83 -> 82 ;
|
|
|
|
83 -> 82 ;
|
|
|
|
82 [label="82: Call _fun_printf \n n$4=_fun_printf(\"(out)HELLO WORLD!\":char *) [line 82]\n REMOVE_TEMPS(n$4); [line 82]\n " shape="box"]
|
|
|
|
82 [label="82: Call _fun_printf \n n$4=_fun_printf(\"(out)HELLO WORLD!\":char *) [line 82]\n " shape="box"]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
82 -> 81 ;
|
|
|
|
82 -> 81 ;
|
|
|
|
81 [label="81: BinaryOperatorStmt: Assign \n n$3=*&value:int [line 83]\n *&x:int =(n$3 + 1) [line 83]\n REMOVE_TEMPS(n$3); [line 83]\n APPLY_ABSTRACTION; [line 83]\n " shape="box"]
|
|
|
|
81 [label="81: BinaryOperatorStmt: Assign \n n$3=*&value:int [line 83]\n *&x:int =(n$3 + 1) [line 83]\n APPLY_ABSTRACTION; [line 83]\n " shape="box"]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
81 -> 78 ;
|
|
|
|
81 -> 78 ;
|
|
|
@ -475,7 +475,7 @@ digraph iCFG {
|
|
|
|
|
|
|
|
|
|
|
|
80 -> 75 ;
|
|
|
|
80 -> 75 ;
|
|
|
|
80 -> 76 ;
|
|
|
|
80 -> 76 ;
|
|
|
|
79 [label="79: Prune (true branch) \n PRUNE(((n$0 == 0) != 0), true); [line 84]\n APPLY_ABSTRACTION; [line 84]\n " shape="invhouse"]
|
|
|
|
79 [label="79: Prune (true branch) \n PRUNE(((n$0 == 0) != 0), true); [line 84]\n REMOVE_TEMPS(n$0); [line 84]\n APPLY_ABSTRACTION; [line 84]\n " shape="invhouse"]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
79 -> 78 ;
|
|
|
|
79 -> 78 ;
|
|
|
@ -492,7 +492,7 @@ digraph iCFG {
|
|
|
|
|
|
|
|
|
|
|
|
76 -> 70 ;
|
|
|
|
76 -> 70 ;
|
|
|
|
76 -> 71 ;
|
|
|
|
76 -> 71 ;
|
|
|
|
75 [label="75: Prune (true branch) \n PRUNE(((n$0 == 1) != 0), true); [line 90]\n APPLY_ABSTRACTION; [line 90]\n " shape="invhouse"]
|
|
|
|
75 [label="75: Prune (true branch) \n PRUNE(((n$0 == 1) != 0), true); [line 90]\n REMOVE_TEMPS(n$0); [line 90]\n APPLY_ABSTRACTION; [line 90]\n " shape="invhouse"]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
75 -> 74 ;
|
|
|
|
75 -> 74 ;
|
|
|
@ -513,15 +513,15 @@ digraph iCFG {
|
|
|
|
|
|
|
|
|
|
|
|
71 -> 68 ;
|
|
|
|
71 -> 68 ;
|
|
|
|
71 -> 69 ;
|
|
|
|
71 -> 69 ;
|
|
|
|
70 [label="70: Prune (true branch) \n PRUNE(((n$0 == 2) != 0), true); [line 96]\n APPLY_ABSTRACTION; [line 96]\n " shape="invhouse"]
|
|
|
|
70 [label="70: Prune (true branch) \n PRUNE(((n$0 == 2) != 0), true); [line 96]\n REMOVE_TEMPS(n$0); [line 96]\n APPLY_ABSTRACTION; [line 96]\n " shape="invhouse"]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
70 -> 65 ;
|
|
|
|
70 -> 65 ;
|
|
|
|
69 [label="69: Prune (false branch) \n PRUNE(((n$0 == 3) == 0), false); [line 97]\n " shape="invhouse"]
|
|
|
|
69 [label="69: Prune (false branch) \n PRUNE(((n$0 == 3) == 0), false); [line 97]\n REMOVE_TEMPS(n$0); [line 97]\n " shape="invhouse"]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
69 -> 67 ;
|
|
|
|
69 -> 67 ;
|
|
|
|
68 [label="68: Prune (true branch) \n PRUNE(((n$0 == 3) != 0), true); [line 97]\n APPLY_ABSTRACTION; [line 97]\n " shape="invhouse"]
|
|
|
|
68 [label="68: Prune (true branch) \n PRUNE(((n$0 == 3) != 0), true); [line 97]\n REMOVE_TEMPS(n$0); [line 97]\n APPLY_ABSTRACTION; [line 97]\n " shape="invhouse"]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
68 -> 65 ;
|
|
|
|
68 -> 65 ;
|
|
|
@ -534,7 +534,7 @@ digraph iCFG {
|
|
|
|
|
|
|
|
|
|
|
|
66 -> 79 ;
|
|
|
|
66 -> 79 ;
|
|
|
|
66 -> 80 ;
|
|
|
|
66 -> 80 ;
|
|
|
|
65 [label="65: Return Stmt \n *&return:int =0 [line 100]\n REMOVE_TEMPS(n$0); [line 100]\n APPLY_ABSTRACTION; [line 100]\n " shape="box"]
|
|
|
|
65 [label="65: Return Stmt \n *&return:int =0 [line 100]\n APPLY_ABSTRACTION; [line 100]\n " shape="box"]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
65 -> 64 ;
|
|
|
|
65 -> 64 ;
|
|
|
@ -554,7 +554,7 @@ digraph iCFG {
|
|
|
|
|
|
|
|
|
|
|
|
61 -> 57 ;
|
|
|
|
61 -> 57 ;
|
|
|
|
61 -> 58 ;
|
|
|
|
61 -> 58 ;
|
|
|
|
60 [label="60: Prune (true branch) \n PRUNE(((n$0 == 0) != 0), true); [line 63]\n " shape="invhouse"]
|
|
|
|
60 [label="60: Prune (true branch) \n PRUNE(((n$0 == 0) != 0), true); [line 63]\n REMOVE_TEMPS(n$0); [line 63]\n " shape="invhouse"]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
60 -> 59 ;
|
|
|
|
60 -> 59 ;
|
|
|
@ -567,7 +567,7 @@ digraph iCFG {
|
|
|
|
|
|
|
|
|
|
|
|
58 -> 52 ;
|
|
|
|
58 -> 52 ;
|
|
|
|
58 -> 53 ;
|
|
|
|
58 -> 53 ;
|
|
|
|
57 [label="57: Prune (true branch) \n PRUNE(((n$0 == 1) != 0), true); [line 66]\n " shape="invhouse"]
|
|
|
|
57 [label="57: Prune (true branch) \n PRUNE(((n$0 == 1) != 0), true); [line 66]\n REMOVE_TEMPS(n$0); [line 66]\n " shape="invhouse"]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
57 -> 56 ;
|
|
|
|
57 -> 56 ;
|
|
|
@ -588,15 +588,15 @@ digraph iCFG {
|
|
|
|
|
|
|
|
|
|
|
|
53 -> 50 ;
|
|
|
|
53 -> 50 ;
|
|
|
|
53 -> 51 ;
|
|
|
|
53 -> 51 ;
|
|
|
|
52 [label="52: Prune (true branch) \n PRUNE(((n$0 == 2) != 0), true); [line 71]\n APPLY_ABSTRACTION; [line 71]\n " shape="invhouse"]
|
|
|
|
52 [label="52: Prune (true branch) \n PRUNE(((n$0 == 2) != 0), true); [line 71]\n REMOVE_TEMPS(n$0); [line 71]\n APPLY_ABSTRACTION; [line 71]\n " shape="invhouse"]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
52 -> 48 ;
|
|
|
|
52 -> 48 ;
|
|
|
|
51 [label="51: Prune (false branch) \n PRUNE(((n$0 == 3) == 0), false); [line 72]\n APPLY_ABSTRACTION; [line 72]\n " shape="invhouse"]
|
|
|
|
51 [label="51: Prune (false branch) \n PRUNE(((n$0 == 3) == 0), false); [line 72]\n REMOVE_TEMPS(n$0); [line 72]\n APPLY_ABSTRACTION; [line 72]\n " shape="invhouse"]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
51 -> 48 ;
|
|
|
|
51 -> 48 ;
|
|
|
|
50 [label="50: Prune (true branch) \n PRUNE(((n$0 == 3) != 0), true); [line 72]\n APPLY_ABSTRACTION; [line 72]\n " shape="invhouse"]
|
|
|
|
50 [label="50: Prune (true branch) \n PRUNE(((n$0 == 3) != 0), true); [line 72]\n REMOVE_TEMPS(n$0); [line 72]\n APPLY_ABSTRACTION; [line 72]\n " shape="invhouse"]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
50 -> 48 ;
|
|
|
|
50 -> 48 ;
|
|
|
@ -605,7 +605,7 @@ digraph iCFG {
|
|
|
|
|
|
|
|
|
|
|
|
49 -> 60 ;
|
|
|
|
49 -> 60 ;
|
|
|
|
49 -> 61 ;
|
|
|
|
49 -> 61 ;
|
|
|
|
48 [label="48: Return Stmt \n *&return:int =0 [line 75]\n REMOVE_TEMPS(n$0); [line 75]\n APPLY_ABSTRACTION; [line 75]\n " shape="box"]
|
|
|
|
48 [label="48: Return Stmt \n *&return:int =0 [line 75]\n APPLY_ABSTRACTION; [line 75]\n " shape="box"]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
48 -> 47 ;
|
|
|
|
48 -> 47 ;
|
|
|
@ -624,11 +624,11 @@ digraph iCFG {
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
44 -> 43 ;
|
|
|
|
44 -> 43 ;
|
|
|
|
43 [label="43: Call _fun_printf \n n$4=_fun_printf(\"(out)HELLO WORLD!\":char *) [line 39]\n REMOVE_TEMPS(n$4); [line 39]\n " shape="box"]
|
|
|
|
43 [label="43: Call _fun_printf \n n$4=_fun_printf(\"(out)HELLO WORLD!\":char *) [line 39]\n " shape="box"]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
43 -> 42 ;
|
|
|
|
43 -> 42 ;
|
|
|
|
42 [label="42: BinaryOperatorStmt: Assign \n n$3=*&value:int [line 40]\n *&x:int =(n$3 + 1) [line 40]\n REMOVE_TEMPS(n$3); [line 40]\n APPLY_ABSTRACTION; [line 40]\n " shape="box"]
|
|
|
|
42 [label="42: BinaryOperatorStmt: Assign \n n$3=*&value:int [line 40]\n *&x:int =(n$3 + 1) [line 40]\n APPLY_ABSTRACTION; [line 40]\n " shape="box"]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
42 -> 39 ;
|
|
|
|
42 -> 39 ;
|
|
|
@ -637,7 +637,7 @@ digraph iCFG {
|
|
|
|
|
|
|
|
|
|
|
|
41 -> 36 ;
|
|
|
|
41 -> 36 ;
|
|
|
|
41 -> 37 ;
|
|
|
|
41 -> 37 ;
|
|
|
|
40 [label="40: Prune (true branch) \n PRUNE(((n$0 == 0) != 0), true); [line 41]\n APPLY_ABSTRACTION; [line 41]\n " shape="invhouse"]
|
|
|
|
40 [label="40: Prune (true branch) \n PRUNE(((n$0 == 0) != 0), true); [line 41]\n REMOVE_TEMPS(n$0); [line 41]\n APPLY_ABSTRACTION; [line 41]\n " shape="invhouse"]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
40 -> 39 ;
|
|
|
|
40 -> 39 ;
|
|
|
@ -654,7 +654,7 @@ digraph iCFG {
|
|
|
|
|
|
|
|
|
|
|
|
37 -> 31 ;
|
|
|
|
37 -> 31 ;
|
|
|
|
37 -> 32 ;
|
|
|
|
37 -> 32 ;
|
|
|
|
36 [label="36: Prune (true branch) \n PRUNE(((n$0 == 1) != 0), true); [line 47]\n APPLY_ABSTRACTION; [line 47]\n " shape="invhouse"]
|
|
|
|
36 [label="36: Prune (true branch) \n PRUNE(((n$0 == 1) != 0), true); [line 47]\n REMOVE_TEMPS(n$0); [line 47]\n APPLY_ABSTRACTION; [line 47]\n " shape="invhouse"]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
36 -> 35 ;
|
|
|
|
36 -> 35 ;
|
|
|
@ -675,15 +675,15 @@ digraph iCFG {
|
|
|
|
|
|
|
|
|
|
|
|
32 -> 29 ;
|
|
|
|
32 -> 29 ;
|
|
|
|
32 -> 30 ;
|
|
|
|
32 -> 30 ;
|
|
|
|
31 [label="31: Prune (true branch) \n PRUNE(((n$0 == 2) != 0), true); [line 53]\n APPLY_ABSTRACTION; [line 53]\n " shape="invhouse"]
|
|
|
|
31 [label="31: Prune (true branch) \n PRUNE(((n$0 == 2) != 0), true); [line 53]\n REMOVE_TEMPS(n$0); [line 53]\n APPLY_ABSTRACTION; [line 53]\n " shape="invhouse"]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
31 -> 26 ;
|
|
|
|
31 -> 26 ;
|
|
|
|
30 [label="30: Prune (false branch) \n PRUNE(((n$0 == 3) == 0), false); [line 54]\n " shape="invhouse"]
|
|
|
|
30 [label="30: Prune (false branch) \n PRUNE(((n$0 == 3) == 0), false); [line 54]\n REMOVE_TEMPS(n$0); [line 54]\n " shape="invhouse"]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
30 -> 28 ;
|
|
|
|
30 -> 28 ;
|
|
|
|
29 [label="29: Prune (true branch) \n PRUNE(((n$0 == 3) != 0), true); [line 54]\n APPLY_ABSTRACTION; [line 54]\n " shape="invhouse"]
|
|
|
|
29 [label="29: Prune (true branch) \n PRUNE(((n$0 == 3) != 0), true); [line 54]\n REMOVE_TEMPS(n$0); [line 54]\n APPLY_ABSTRACTION; [line 54]\n " shape="invhouse"]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
29 -> 26 ;
|
|
|
|
29 -> 26 ;
|
|
|
@ -696,7 +696,7 @@ digraph iCFG {
|
|
|
|
|
|
|
|
|
|
|
|
27 -> 40 ;
|
|
|
|
27 -> 40 ;
|
|
|
|
27 -> 41 ;
|
|
|
|
27 -> 41 ;
|
|
|
|
26 [label="26: Return Stmt \n *&return:int =0 [line 57]\n REMOVE_TEMPS(n$0); [line 57]\n APPLY_ABSTRACTION; [line 57]\n " shape="box"]
|
|
|
|
26 [label="26: Return Stmt \n *&return:int =0 [line 57]\n APPLY_ABSTRACTION; [line 57]\n " shape="box"]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
26 -> 25 ;
|
|
|
|
26 -> 25 ;
|
|
|
@ -715,11 +715,11 @@ digraph iCFG {
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
22 -> 21 ;
|
|
|
|
22 -> 21 ;
|
|
|
|
21 [label="21: Call _fun_printf \n n$7=_fun_printf(\"(out)HELLO WORLD!\":char *) [line 17]\n REMOVE_TEMPS(n$7); [line 17]\n " shape="box"]
|
|
|
|
21 [label="21: Call _fun_printf \n n$7=_fun_printf(\"(out)HELLO WORLD!\":char *) [line 17]\n " shape="box"]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
21 -> 20 ;
|
|
|
|
21 -> 20 ;
|
|
|
|
20 [label="20: BinaryOperatorStmt: Assign \n n$6=*&value:int [line 18]\n *&x:int =(n$6 + 1) [line 18]\n REMOVE_TEMPS(n$6); [line 18]\n APPLY_ABSTRACTION; [line 18]\n " shape="box"]
|
|
|
|
20 [label="20: BinaryOperatorStmt: Assign \n n$6=*&value:int [line 18]\n *&x:int =(n$6 + 1) [line 18]\n APPLY_ABSTRACTION; [line 18]\n " shape="box"]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
20 -> 17 ;
|
|
|
|
20 -> 17 ;
|
|
|
@ -728,7 +728,7 @@ digraph iCFG {
|
|
|
|
|
|
|
|
|
|
|
|
19 -> 15 ;
|
|
|
|
19 -> 15 ;
|
|
|
|
19 -> 16 ;
|
|
|
|
19 -> 16 ;
|
|
|
|
18 [label="18: Prune (true branch) \n PRUNE(((n$2 == 0) != 0), true); [line 19]\n APPLY_ABSTRACTION; [line 19]\n " shape="invhouse"]
|
|
|
|
18 [label="18: Prune (true branch) \n PRUNE(((n$2 == 0) != 0), true); [line 19]\n REMOVE_TEMPS(n$2); [line 19]\n APPLY_ABSTRACTION; [line 19]\n " shape="invhouse"]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
18 -> 17 ;
|
|
|
|
18 -> 17 ;
|
|
|
@ -741,7 +741,7 @@ digraph iCFG {
|
|
|
|
|
|
|
|
|
|
|
|
16 -> 12 ;
|
|
|
|
16 -> 12 ;
|
|
|
|
16 -> 13 ;
|
|
|
|
16 -> 13 ;
|
|
|
|
15 [label="15: Prune (true branch) \n PRUNE(((n$2 == 1) != 0), true); [line 22]\n " shape="invhouse"]
|
|
|
|
15 [label="15: Prune (true branch) \n PRUNE(((n$2 == 1) != 0), true); [line 22]\n REMOVE_TEMPS(n$2); [line 22]\n " shape="invhouse"]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
15 -> 14 ;
|
|
|
|
15 -> 14 ;
|
|
|
@ -749,11 +749,11 @@ digraph iCFG {
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
14 -> 4 ;
|
|
|
|
14 -> 4 ;
|
|
|
|
13 [label="13: Prune (false branch) \n PRUNE(((n$2 == 2) == 0), false); [line 25]\n " shape="invhouse"]
|
|
|
|
13 [label="13: Prune (false branch) \n PRUNE(((n$2 == 2) == 0), false); [line 25]\n REMOVE_TEMPS(n$2); [line 25]\n " shape="invhouse"]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
13 -> 10 ;
|
|
|
|
13 -> 10 ;
|
|
|
|
12 [label="12: Prune (true branch) \n PRUNE(((n$2 == 2) != 0), true); [line 25]\n APPLY_ABSTRACTION; [line 25]\n " shape="invhouse"]
|
|
|
|
12 [label="12: Prune (true branch) \n PRUNE(((n$2 == 2) != 0), true); [line 25]\n REMOVE_TEMPS(n$2); [line 25]\n APPLY_ABSTRACTION; [line 25]\n " shape="invhouse"]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
12 -> 11 ;
|
|
|
|
12 -> 11 ;
|
|
|
@ -770,7 +770,7 @@ digraph iCFG {
|
|
|
|
|
|
|
|
|
|
|
|
9 -> 18 ;
|
|
|
|
9 -> 18 ;
|
|
|
|
9 -> 19 ;
|
|
|
|
9 -> 19 ;
|
|
|
|
8 [label="8: Call _fun_printf \n n$1=_fun_printf(\"(after_switch)HELLO WORLD!\":char *) [line 30]\n REMOVE_TEMPS(n$1,n$2); [line 30]\n APPLY_ABSTRACTION; [line 30]\n " shape="box"]
|
|
|
|
8 [label="8: Call _fun_printf \n n$1=_fun_printf(\"(after_switch)HELLO WORLD!\":char *) [line 30]\n REMOVE_TEMPS(n$1); [line 30]\n APPLY_ABSTRACTION; [line 30]\n " shape="box"]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
8 -> 4 ;
|
|
|
|
8 -> 4 ;
|
|
|
|