diff options
| author | Jonathan Protzenko | 2023-02-02 23:36:14 -0800 |
|---|---|---|
| committer | Son HO | 2023-06-04 21:44:33 +0200 |
| commit | 40e7df701d246faa453003374206014606ca6b6d (patch) | |
| tree | 4f4a199c90ce53937eae8ec4ecb9e0d1f7564a2c /compiler/ExtractBase.ml | |
| parent | dad646759a3ab9175c8797f144dec9d8e07b54b3 (diff) | |
WIP
Diffstat (limited to '')
| -rw-r--r-- | compiler/ExtractBase.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml index 77170b5b..98a29daf 100644 --- a/compiler/ExtractBase.ml +++ b/compiler/ExtractBase.ml @@ -168,6 +168,7 @@ type formatter = { int -> region_group_info option -> bool * int -> + bool -> string; (** Compute the name of a regular (non-assumed) function. @@ -187,6 +188,7 @@ type formatter = { The number of extracted backward functions if not necessarily equal to the number of region groups, because we may have filtered some of them. + - whether there is a body or not (indicates assumed function) TODO: use the fun id for the assumed functions. *) decreases_clause_name : @@ -774,7 +776,7 @@ let ctx_add_fun_decl (trans_group : bool * pure_fun_translation) in let name = ctx.fmt.fun_name def.basename def.num_loops def.loop_id num_rgs rg_info - (keep_fwd, num_backs) + (keep_fwd, num_backs) (def.body = None) in ctx_add (FunId (FromLlbc (A.Regular def_id, def.loop_id, def.back_id))) |