diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-06-12 22:33:46 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-06-12 22:33:46 +0100 |
| commit | 41fd0d147730570747f8eb71f83e739c13fde0d1 (patch) | |
| tree | 954e86365b33a2b1bc123a73e8966614e9dfd046 | |
| parent | c70c6a548e9f2a047efceb8eb32b8ce12ff77650 (diff) | |
| download | compcert-kvx-41fd0d147730570747f8eb71f83e739c13fde0d1.tar.gz compcert-kvx-41fd0d147730570747f8eb71f83e739c13fde0d1.zip | |
fix: use more fuel (the fallback case was wrong)
| -rw-r--r-- | backend/RTLblockgen.v | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/backend/RTLblockgen.v b/backend/RTLblockgen.v index a4e9cdfd..591a24af 100644 --- a/backend/RTLblockgen.v +++ b/backend/RTLblockgen.v @@ -7,10 +7,13 @@ Require Import Errors. Local Open Scope error_monad_scope. +Definition extract_block_fuel := 10000%positive . + Fixpoint extract_block (cfg : RTL.code) (n : node) (previous : list RTLblock.instruction) (max_size : nat) : res block := match max_size with - | O => OK (mkblock (List.rev previous) (IBgoto n)) + | O => Error (Errors.msg "RTLblockgen.extract_block: not enough fuel") + (* THIS IS WRONG: OK (mkblock (List.rev previous) (IBgoto n)) *) | S max_size' => match cfg!(n) with | None => Error (Errors.msg "RTLblockgen.extract_block: unknown label") @@ -52,7 +55,7 @@ Fixpoint transl_code (cfg : RTL.code) (todo : list node) match previous!(label) with | Some _ => transl_code cfg rest previous max_iter' | None => - do block <- extract_block cfg label nil (300%nat); + do block <- extract_block cfg label nil (Pos.to_nat extract_block_fuel); transl_code cfg ((cfi_targets (blk_control block)) ++ rest) (PTree.set label block previous) max_iter' |