From 0f1db1bd8b531582a7e4b1bb3ccdadfce20f4fdf Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Wed, 4 Mar 2020 06:21:26 -0800 Subject: [PATCH] [sledge] Fix potential name clash when executing memmov Reviewed By: jvillard Differential Revision: D20214527 fbshipit-source-id: 9e1bbb435 --- sledge/src/symbheap/exec.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/sledge/src/symbheap/exec.ml b/sledge/src/symbheap/exec.ml index 0f549b264..0e0bafd1c 100644 --- a/sledge/src/symbheap/exec.ml +++ b/sledge/src/symbheap/exec.ml @@ -165,7 +165,7 @@ let memmov_foot us dst src len = let mem_src = (src_dst, arr_src) in let mem_dst_mid_src = [|mem_dst; mem_mid; mem_src|] in let siz_dst_mid_src, us, xs = fresh_var "m" us xs in - let arr_dst_mid_src, _, xs = fresh_var "a" us xs in + let arr_dst_mid_src, us, xs = fresh_var "a" us xs in let eq_mem_dst_mid_src = Term.eq_concat (siz_dst_mid_src, arr_dst_mid_src) mem_dst_mid_src in @@ -178,14 +178,14 @@ let memmov_foot us dst src len = (Sh.and_ (Term.lt dst src) (Sh.and_ (Term.lt src (Term.add dst len)) seg)) in - (xs, bas, siz, mem_dst, mem_mid, mem_src, foot) + (us, xs, bas, siz, mem_dst, mem_mid, mem_src, foot) (* { d⟨s-d,α⟩^⟨l-(s-d),β⟩^⟨s-d,γ⟩ } * memmov l d s * { d-[b;m)->⟨l-(s-d),β⟩^⟨s-d,γ⟩^⟨s-d,γ⟩ } *) let memmov_dn_spec us dst src len = - let xs, bas, siz, _, mem_mid, mem_src, foot = + let us, xs, bas, siz, _, mem_mid, mem_src, foot = memmov_foot us dst src len in let mem_mid_src_src = [|mem_mid; mem_src; mem_src|] in @@ -210,7 +210,7 @@ let memmov_dn_spec us dst src len = * { s-[b;m)->⟨d-s,α⟩^⟨d-s,α⟩^⟨l-(d-s),β⟩ } *) let memmov_up_spec us dst src len = - let xs, bas, siz, mem_src, mem_mid, _, foot = + let us, xs, bas, siz, mem_src, mem_mid, _, foot = memmov_foot us src dst len in let mem_src_src_mid = [|mem_src; mem_src; mem_mid|] in