diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2021-02-23 12:45:59 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2021-02-23 12:59:43 +0000 |
| commit | c49caca4b5f0239b43610fbfe012d6ba0211b364 (patch) | |
| tree | d7e0a80528c04a8dc99ad436ba652ef31eaaeb1f | |
| parent | 48a9dcbdc968bcf05b4eec17b8c7fd471fb80240 (diff) | |
| download | compcert-c49caca4b5f0239b43610fbfe012d6ba0211b364.tar.gz compcert-c49caca4b5f0239b43610fbfe012d6ba0211b364.zip | |
No inline when no load and store are present
Acked-by: Yann Herklotz <git@yannherklotz.com>
| -rw-r--r-- | backend/Inliningaux.ml | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/backend/Inliningaux.ml b/backend/Inliningaux.ml index a2570da5..af633f19 100644 --- a/backend/Inliningaux.ml +++ b/backend/Inliningaux.ml @@ -85,8 +85,14 @@ let static_called_once id io = (* To be considered: heuristics based on size of function? *) +let arg_in_mem_op reg_list op = + match op with + | Istore _ | Iload _ -> true + | _ -> false + let should_inline (io: inlining_info) (id: ident) (f: coq_function) = if !Clflags.option_finline then begin - true + List.exists (arg_in_mem_op f.fn_params) + (PTree.elements f.fn_code |> List.map snd) end else false |