Skip to content

Commit 34e2c0f

Browse files
committed
fix memcpy calls
1 parent 14cabe0 commit 34e2c0f

File tree

1 file changed

+3
-3
lines changed

1 file changed

+3
-3
lines changed

src/Lean/Compiler/IR/EmitC.lean

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -904,7 +904,7 @@ def emitStructReshapeFn (origin target : IRType) (id1 id2 : Nat) : M Unit := do
904904
emit "(x.cs.c"; emit i; emitLn ");"
905905
| .struct _ tys us ss, .struct _ tys' _ _ =>
906906
if us ≠ 0 ∨ ss ≠ 0 then
907-
emit "memcpy(&y, &x, sizeof(size_t)*"; emit us; emit "+"; emit ss; emitLn ");"
907+
emit "memcpy(y.u, x.u, sizeof(size_t)*"; emit us; emit "+"; emit ss; emitLn ");"
908908
for h : i in *...tys.size do
909909
if tys'[i]! matches .erased | .void then
910910
continue
@@ -937,7 +937,7 @@ def emitStructBox (ty : IRType) (cidx : Nat) (x : String) : M Unit := do
937937
emit ", sizeof(size_t)*"; emit us; emit "+"; emit ss
938938
emitLn ");"
939939
if us ≠ 0 ∨ ss ≠ 0 then
940-
emit "memcpy(lean_ctor_scalar_cptr(y), &x, sizeof(size_t)*"
940+
emit "memcpy(lean_ctor_scalar_cptr(y), "; emit x; emit ".u, sizeof(size_t)*"
941941
emit us; emit "+"; emit ss; emitLn ");"
942942
for h : i in *...tys.size do
943943
emit "lean_ctor_set(y, "; emit i; emit ", "
@@ -977,7 +977,7 @@ def emitStructUnboxFn (ty : IRType) (id : Nat) : M Unit := do
977977
else
978978
let .struct _ tys us ss := ty | unreachable!
979979
if us ≠ 0 ∨ ss ≠ 0 then
980-
emit "memcpy(&y, lean_ctor_scalar_cptr(x), sizeof(size_t)*"
980+
emit "memcpy(y.u, lean_ctor_scalar_cptr(x), sizeof(size_t)*"
981981
emit us; emit "+"; emit ss; emitLn ");"
982982
for h : i in *...tys.size do
983983
if tys[i] matches .erased | .void then

0 commit comments

Comments
 (0)