diff options
| -rw-r--r-- | cheri/cheri_prelude_128.sail | 8 | ||||
| -rw-r--r-- | cheri/cheri_prelude_256.sail | 7 |
2 files changed, 0 insertions, 15 deletions
diff --git a/cheri/cheri_prelude_128.sail b/cheri/cheri_prelude_128.sail index cb931962..ffd986a4 100644 --- a/cheri/cheri_prelude_128.sail +++ b/cheri/cheri_prelude_128.sail @@ -35,14 +35,6 @@ /* 128 bit cap + tag */ type CapReg = bits(129) -/* -val cast_bool_bit : cast extern bool -> bit effect pure -val cast_boolvec_bitvec : cast extern forall 'n, 'm. vector<'n,'m,dec,bool> -> vector<'n,'m,dec,bit> effect pure -val cast_range_bitvec : cast forall 'm. [|0:2**'m - 1|] -> vector<'m - 1,'m,dec,bit> effect pure -function vector<'m - 1,'m,dec,bit> cast_range_bitvec (v) = to_vec (v) -val not : extern bool -> bool effect pure -*/ - struct CapStruct = { tag : bool , uperms : bits(4) , diff --git a/cheri/cheri_prelude_256.sail b/cheri/cheri_prelude_256.sail index f09fe608..28c9599d 100644 --- a/cheri/cheri_prelude_256.sail +++ b/cheri/cheri_prelude_256.sail @@ -35,13 +35,6 @@ /* 256 bit cap + tag */ type CapReg = bits(257) -/* -val cast_bool_bit : bool -> bit effect pure -val cast_boolvec_bitvec : 'n, 'm. vector<'n,'m,dec,bool> -> vector<'n,'m,dec,bit> effect pure -val cast_range_bitvec : forall 'm. [|0:2**'m - 1|] -> vector<'m - 1,'m,dec,bit> effect pure -function vector<'m - 1,'m,dec,bit> cast_range_bitvec (v) = to_vec (v) -val not : extern bool -> bool effect pure */ - struct CapStruct = { tag : bool , padding : bits(8) , |