From 3d4806d52f65099192adc34a2c6b2c5979537fd3 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Mon, 30 Mar 2020 20:11:36 +0200
Subject: additional checks

---
 backend/Inject.v | 12 +++++++++++-
 1 file changed, 11 insertions(+), 1 deletion(-)

(limited to 'backend/Inject.v')

diff --git a/backend/Inject.v b/backend/Inject.v
index e65cb060..6da10019 100644
--- a/backend/Inject.v
+++ b/backend/Inject.v
@@ -84,7 +84,17 @@ Section INJECTOR.
   Definition transf_function (f : function) : res function :=
     let injections := PTree.elements (gen_injections f) in
     let max_pc := max_pc_function f in
-    if List.forallb (fun injection => (fst injection) <=? max_pc) injections
+    let max_reg := max_reg_function f in
+    if List.forallb
+         (fun injection =>
+            ((fst injection) <=? max_pc) &&
+            (List.forallb
+               (fun (i : inj_instr) =>
+                  (match i with
+                   | INJop _ _ res => res
+                   | INJload _ _ _ res => res
+                   end) <=? max_reg) (snd injection))
+         ) injections
     then
       OK {| fn_sig := f.(fn_sig);
             fn_params := f.(fn_params);
-- 
cgit