aboutsummaryrefslogtreecommitdiffstats
path: root/src/hls/Gible.v
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2022-06-05 22:42:28 +0100
committerYann Herklotz <git@yannherklotz.com>2022-06-05 22:42:28 +0100
commit48d907ee56b39e7a8819700ae8a88af05c1b031e (patch)
tree0d9cddc5622e5b9953b871908195aa606b3dd748 /src/hls/Gible.v
parent2e731050c69c98142d29d87fb863f199d50dfe19 (diff)
downloadvericert-48d907ee56b39e7a8819700ae8a88af05c1b031e.tar.gz
vericert-48d907ee56b39e7a8819700ae8a88af05c1b031e.zip
Fix many more lemmas
Diffstat (limited to 'src/hls/Gible.v')
-rw-r--r--src/hls/Gible.v10
1 files changed, 10 insertions, 0 deletions
diff --git a/src/hls/Gible.v b/src/hls/Gible.v
index e50fdc0..c51b250 100644
--- a/src/hls/Gible.v
+++ b/src/hls/Gible.v
@@ -613,4 +613,14 @@ type ~genv~ which was declared earlier.
end
) b nil.
+ Definition pred_uses i :=
+ match i with
+ | RBop (Some p) _ _ _
+ | RBload (Some p) _ _ _ _
+ | RBstore (Some p) _ _ _ _
+ | RBexit (Some p) _ => predicate_use p
+ | RBsetpred (Some p) _ _ p' => p' :: predicate_use p
+ | _ => nil
+ end.
+
End Gible.