aboutsummaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2022-05-31 02:07:54 +0100
committerYann Herklotz <git@yannherklotz.com>2022-05-31 02:07:54 +0100
commit68ab5fb3aa207fa4907fd67ba2751c59fb5e1ce2 (patch)
tree0d8579d46a6312df9895fd56e5894b73da82caf4 /src
parenta8aef8ab043500f10cfb82ee5d86efedba50cae4 (diff)
downloadvericert-68ab5fb3aa207fa4907fd67ba2751c59fb5e1ce2.tar.gz
vericert-68ab5fb3aa207fa4907fd67ba2751c59fb5e1ce2.zip
Do not remove dependencies from control-flow
Diffstat (limited to 'src')
-rw-r--r--src/hls/Schedule.ml7
1 files changed, 6 insertions, 1 deletions
diff --git a/src/hls/Schedule.ml b/src/hls/Schedule.ml
index 9ba2b51..829ded1 100644
--- a/src/hls/Schedule.ml
+++ b/src/hls/Schedule.ml
@@ -559,12 +559,17 @@ let assigned_vars vars = function
| RBsetpred (_, _, _, _) -> vars
| RBexit (_, _) -> vars
+(** To be able to properly eliminate dependencies on control-flow, one needs to be able to handle
+ comparisons of a register that has a value in one version, and no value in the other, which the
+ checker currently does not. *)
+
let get_pred = function
| RBnop -> None
| RBop (op, _, _, _) -> op
| RBload (op, _, _, _, _) -> op
| RBstore (op, _, _, _, _) -> op
- | RBexit (op, _) -> op
+ (* | RBexit (op, _) -> op *)
+ | RBexit (op, _) -> None
| RBsetpred (_, _, _, _) -> None
let independant_pred p p' =