Line | |
---|

1 | |
---|

2 | |
---|

3 | let f_expr set locals e sub_exprs_res = |
---|

4 | let e_res = match e with |
---|

5 | | Clight.Expr (Clight.Evar id, _) -> |
---|

6 | StringTools.Set.mem id set && not (List.mem id locals) |
---|

7 | | _ -> false in |
---|

8 | List.fold_left (||) false (e_res :: sub_exprs_res) |
---|

9 | |
---|

10 | let f_stmt _ sub_exprs_res sub_stmts_res = |
---|

11 | List.fold_left (||) false (sub_exprs_res @ sub_stmts_res) |
---|

12 | |
---|

13 | let references_stmt set locals stmt = |
---|

14 | ClightFold.statement2 (f_expr set locals) f_stmt stmt |
---|

15 | |
---|

16 | let references_funct set (id, def) = match def with |
---|

17 | | Clight.Internal def -> |
---|

18 | let locals = List.map fst (def.Clight.fn_params @ def.Clight.fn_vars) in |
---|

19 | if references_stmt set locals def.Clight.fn_body then |
---|

20 | StringTools.Set.add id set |
---|

21 | else set |
---|

22 | | _ -> set |
---|

23 | |
---|

24 | let references set p = |
---|

25 | List.fold_left references_funct set p.Clight.prog_funct |
---|

26 | |
---|

27 | |
---|

28 | let unsupported_functions p = |
---|

29 | let rec fixpoint set = |
---|

30 | let set' = references set p in |
---|

31 | if StringTools.Set.equal set set' then set |
---|

32 | else fixpoint set' in |
---|

33 | fixpoint (StringTools.Set.of_list ["calloc" ; "memcpy"]) |
---|

34 | |
---|

35 | |
---|

36 | let remove_functions functions p = |
---|

37 | let f (id, _) = not (StringTools.Set.mem id functions) in |
---|

38 | let functs = List.filter f p.Clight.prog_funct in |
---|

39 | { p with Clight.prog_funct = functs } |
---|

40 | |
---|

41 | |
---|

42 | let simplify p = |
---|

43 | let unsupported = unsupported_functions p in |
---|

44 | remove_functions unsupported p |
---|

**Note:** See

TracBrowser
for help on using the repository browser.