|
280 | 280 |
|
281 | 281 | let cartesian_concat_paths (ps : cfg_path list) (qs : cfg_path list) : cfg_path list = List.concat (List.map (fun p -> List.map (fun q -> p @ q) qs) ps) |
282 | 282 |
|
283 | | -(* TODO: remove *) |
284 | | -let partition_if_next (if_next_n : (edge * node * cfg_path list) list): exp * (node * cfg_path list) * (node * cfg_path list) = |
285 | | - (* TODO: refactor *) |
286 | | - let exp = |
287 | | - match if_next_n with |
288 | | - | [] -> failwith "partition_if_next: empty" |
289 | | - | (Test (exp, _), _, _) :: xs -> |
290 | | - let all_tests_same_cond = |
291 | | - List.for_all |
292 | | - (function |
293 | | - | (Test (exp', _), _, _) -> Basetype.CilExp.equal exp exp' |
294 | | - | _ -> false) |
295 | | - xs |
296 | | - in |
297 | | - if all_tests_same_cond then exp |
298 | | - else failwith "partition_if_next: bad branches" |
299 | | - | _ -> failwith "partition_if_next: not Test edge" |
300 | | - in |
301 | | - let collapse_branch b = |
302 | | - let paths_for_b = List.filter (function |
303 | | - | (Test (_, b'), _, _) when b = b' -> true |
304 | | - | _ -> false) |
305 | | - if_next_n |
306 | | - in |
307 | | - match paths_for_b with |
308 | | - | [] -> failwith (if b then "partition_if_next: missing true-branch" else "partition_if_next: missing false-branch") |
309 | | - | (e, n, ps) :: rest -> (* TODO: rest is ignored, so this List.filter is almost a List.find, except it also checks if nodes are all same (for b) *) |
310 | | - let all_same_en = List.for_all (fun (e', n', _) -> Edge.equal e e' && Node.equal n n') paths_for_b in |
311 | | - if not all_same_en then failwith "partition_if_next: branch has differing (edge,node) pairs"; |
312 | | - (n, ps) |
313 | | - in |
314 | | - (exp, collapse_branch true, collapse_branch false) |
315 | | - |
316 | 283 | let partition_if_next if_next = |
317 | 284 | let (if_next_trues, if_next_falses) = List.partition (function |
318 | 285 | | (Test (_, b), _, _) -> b |
|
0 commit comments