summaryrefslogtreecommitdiff
path: root/aarch64_small/mono-splices/ASR_C.sail
blob: 0a47d8d7a9cfceabfa9dd65b7b3ec5c8c6c50c6e (plain)
1
2
3
4
5
6
7
8
val ASR_C : forall 'N 'S, 'N >= 1 & 'S >= 1.
  (bits('N), int('S)) -> (bits('N), bit) effect {escape}

function ASR_C (x, shift) = {
  result : bits('N) = sail_arith_shiftright(x, shift);
  carry_out : bit = if shift > 'N then x['N - 1] else x[shift - 1];
  return((result, carry_out))
}