From 4a90963748252e81ab50ed6136bd566d4a59cda6 Mon Sep 17 00:00:00 2001 From: Andreas Lindner Date: Fri, 16 Aug 2024 17:02:22 +0200 Subject: [PATCH] Fix CI tests --- .../symbexec/examples/test-birs_compose.sml | 19 +++++++++---------- .../symbexec/examples/test-birs_transfer.sml | 2 +- 2 files changed, 10 insertions(+), 11 deletions(-) diff --git a/src/tools/symbexec/examples/test-birs_compose.sml b/src/tools/symbexec/examples/test-birs_compose.sml index c721b7a74..88f9fdba6 100644 --- 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 index 447b495d3..fd7d97e97 100644 --- 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;