diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2022-06-03 20:57:36 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2022-06-03 20:57:36 +0100 |
| commit | 6d1467f2054a54955f642fabf43e224f121cf8e3 (patch) | |
| tree | 51a29d2789262dc52ffae1f5fb69ea087bfbed22 /src/hls/Gible.v | |
| parent | db4da00aea8b51bc9d90d83f981b9163eec3c540 (diff) | |
| download | vericert-6d1467f2054a54955f642fabf43e224f121cf8e3.tar.gz vericert-6d1467f2054a54955f642fabf43e224f121cf8e3.zip | |
Working towards ElimCond proof
Diffstat (limited to 'src/hls/Gible.v')
| -rw-r--r-- | src/hls/Gible.v | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/hls/Gible.v b/src/hls/Gible.v index ea6bece..e50fdc0 100644 --- a/src/hls/Gible.v +++ b/src/hls/Gible.v @@ -587,11 +587,16 @@ type ~genv~ which was declared earlier. Definition max_reg_block (m: positive) (n: node) (i: B.t) := B.foldl max_reg_instr i m. + Definition max_pred_block (m: positive) (n: node) (i: B.t) := B.foldl max_pred_instr i m. + Definition max_reg_function (f: function) := Pos.max (PTree.fold max_reg_block f.(fn_code) 1%positive) (fold_left Pos.max f.(fn_params) 1%positive). + Definition max_pred_function (f: function) := + PTree.fold max_pred_block f.(fn_code) 1%positive. + Definition max_pc_function (f: function) : positive := PTree.fold (fun m pc i => |