Fix CI tests

kth-step · Aug 16, 2024 · 4a90963 · 4a90963
1 parent 3e61113
commit 4a90963
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 11 deletions.
diff --git a/src/tools/symbexec/examples/test-birs_compose.sml b/src/tools/symbexec/examples/test-birs_compose.sml
@@ -1,6 +1,7 @@
 
 open HolKernel Parse boolLib bossLib;
 
+open birs_execLib;
 open birs_stepLib;
 open birs_composeLib;
 
@@ -63,21 +64,19 @@ val bprog = (fst o dest_eq o concl) bprog_test_def;
 val birs_state_init_lbl = (snd o dest_eq o concl o EVAL) ``bir_block_pc (BL_Address (Imm32 2826w))``;
 val birs_state_init = ``<|
   bsst_pc       := ^birs_state_init_lbl;
-  bsst_environ  := ("R7"         =+ (SOME (BExp_Den (BVar "sy_R7" (BType_Imm Bit32)))))
-                   (("SP_process" =+ (SOME (BExp_Den (BVar "sy_SP_process" (BType_Imm Bit32)))))
-                      (("countw"     =+ (SOME (BExp_Den (BVar "sy_countw" (BType_Imm Bit64)))))
-                       (K NONE)
-                   ));
+  bsst_environ  := birs_gen_env
+                   [("R7", BExp_Den (BVar "sy_R7" (BType_Imm Bit32)));
+                    ("SP_process", BExp_Den (BVar "sy_SP_process" (BType_Imm Bit32)));
+                    ("countw", BExp_Den (BVar "sy_countw" (BType_Imm Bit64)))];
   bsst_status   := BST_Running;
   bsst_pcond    := BExp_Const (Imm1 1w)
 |>``;
 val birs_state_init_2 = ``<|
   bsst_pc       := ^birs_state_init_lbl;
-  bsst_environ  := ("R7"         =+ (SOME (BExp_Den (BVar "sy_R7" (BType_Imm Bit32)))))
-                   (("SP_process" =+ (SOME (BExp_Den (BVar "sy_SP_process" (BType_Imm Bit32)))))
-                      (("countw"     =+ (SOME (BExp_Den (BVar "sy_countw" (BType_Imm Bit64)))))
-                       (K NONE)
-                   ));
+  bsst_environ  := birs_gen_env
+                   [("R7", BExp_Den (BVar "sy_R7" (BType_Imm Bit32)));
+                    ("SP_process", BExp_Den (BVar "sy_SP_process" (BType_Imm Bit32)));
+                    ("countw", BExp_Den (BVar "sy_countw" (BType_Imm Bit64)))];
   bsst_status   := BST_Running;
   bsst_pcond    := BExp_BinPred BIExp_LessOrEqual
                      (BExp_Den (BVar "sy_countw" (BType_Imm Bit64)))

diff --git a/src/tools/symbexec/examples/test-birs_transfer.sml b/src/tools/symbexec/examples/test-birs_transfer.sml
@@ -3,7 +3,7 @@ open HolKernel Parse boolLib bossLib;
 
 open bir_symbTheory;
 
-open birs_stepLib;
+open birs_execLib;
 open birs_composeLib;
 
 open birs_auxTheory;