Skip to content

Commit b8839dd

Browse files
committed
Add krml extraction for memcpy_l.
1 parent 6186d0d commit b8839dd

1 file changed

Lines changed: 5 additions & 0 deletions

File tree

src/extraction/ExtractPulse.fst

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -173,6 +173,11 @@ let pulse_translate_expr : translate_expr_t = fun env e ->
173173
when string_of_mlpath p = "Pulse.Lib.Array.Core.sub" ->
174174
EBufSub (translate_expr env a, translate_expr env i)
175175

176+
| MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ l; src; dst; _; _; _ ])
177+
when string_of_mlpath p = "Pulse.Lib.Array.memcpy_l" ->
178+
let zero = EConstant (SizeT, "0") in
179+
EBufBlit (translate_expr env src, zero, translate_expr env dst, zero, translate_expr env l)
180+
176181
| MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ r; _p; _w ])
177182
when string_of_mlpath p = "Pulse.Lib.Reference.to_array_mask" ->
178183
translate_expr env r

0 commit comments

Comments
 (0)