diff options
| author | Christopher Pulte | 2019-03-04 14:35:40 +0000 |
|---|---|---|
| committer | Christopher Pulte | 2019-03-04 14:35:40 +0000 |
| commit | 191763ccfe4cc020236174ce9388c06d9c6d5b3c (patch) | |
| tree | 4010020ad358f8c035e0f9532c819f301af2a275 /aarch64_small | |
| parent | 4be604551897b00a09c4cc5535331181caf54621 (diff) | |
last bit of sail1 to sail2 porting
Diffstat (limited to 'aarch64_small')
| -rw-r--r-- | aarch64_small/armV8.sail | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/aarch64_small/armV8.sail b/aarch64_small/armV8.sail index b2f493ad..b43d9341 100644 --- a/aarch64_small/armV8.sail +++ b/aarch64_small/armV8.sail @@ -553,7 +553,7 @@ end decodeImplementationDefined val decodeTestBranchImmediate : bits(32) -> option(ast) effect {escape} function decodeTestBranchImmediate ([b5]@0b011011@[op]@(b40 : bits(5))@(imm14 : bits(14))@(Rt:bits(5))) = { t : reg_index = UInt_reg(Rt); - + let datasize : {| 32, 64 |} /* as atom('R) */ = if b5 == b1 then 64 else 32; let bit_pos : uinteger = UInt([b5]@b40); bit_val : bit = op; @@ -564,7 +564,7 @@ function decodeTestBranchImmediate ([b5]@0b011011@[op]@(b40 : bits(5))@(imm14 : Some(TestBitAndBranch((t,datasize,bit_pos,bit_val,offset))); } -function clause execute ( TestBitAndBranch((t:reg_index,datasize as atom('R),bit_pos,bit_val,offset)) ) = { +function clause execute ( TestBitAndBranch((t:reg_index,datasize as int('R),bit_pos,bit_val,offset)) ) = { /* assert ('R == 32 | 'R == 64); */ |