diff options
| author | Jon French | 2019-05-13 16:25:43 +0100 |
|---|---|---|
| committer | Jon French | 2019-05-13 16:25:43 +0100 |
| commit | cc90f4b8c1254f119aabc4bbf913f257b4205d25 (patch) | |
| tree | 1f211699feb7f5fc3648a31351a4136c71f9b59d /aarch64_small | |
| parent | 99d3f4d6458704dad2bf6c31198def63a60fed94 (diff) | |
aarch64_small: correct a couple of incorrect effects
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 a9a78900..4b7323f6 100644 --- a/aarch64_small/armV8.sail +++ b/aarch64_small/armV8.sail @@ -2091,7 +2091,7 @@ function clause execute ( ConditionalSelect((d,n,m,datasize as int('R),condition wX(d) = result; } -val decodeData1Source : bits(32) -> option(ast) effect pure +val decodeData1Source : bits(32) -> option(ast) effect {escape} scattered function decodeData1Source /* RBIT */ @@ -2178,7 +2178,7 @@ function clause execute (CountLeading((d,n,datasize as int('R),opcode))) = { end decodeData1Source -val decodeData2Source : bits(32) -> option(ast) effect pure +val decodeData2Source : bits(32) -> option(ast) effect {escape} scattered function decodeData2Source /* SDIV o1=1 */ |