Merge pull request diffblue#6137 from tautschnig/offset-arithmetic

martin-cs · web-flow · commit 78a08ce28328 · 2021-05-24T17:59:22.000+01:00
bv_pointerst::offset_arithmetic: de-duplicate code
diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp
@@ -809,13 +809,8 @@ bvt bv_pointerst::offset_arithmetic(
 {
   const std::size_t offset_bits = bv_pointers_width.get_offset_width(type);
 
-  bvt bv1 = offset_literals(bv, type);
-
-  bvt bv2=bv_utils.build_constant(x, offset_bits);
-
-  bvt tmp=bv_utils.add(bv1, bv2);
-
-  return object_offset_encoding(object_literals(bv, type), tmp);
+  return offset_arithmetic(
+    type, bv, 1, bv_utils.build_constant(x, offset_bits));
 }
 
 bvt bv_pointerst::offset_arithmetic(

Original file line number	Diff line number	Diff line change
`@@ -809,13 +809,8 @@ bvt bv_pointerst::offset_arithmetic(`
`809`	`809`	`{`
`810`	`810`	`const std::size_t offset_bits = bv_pointers_width.get_offset_width(type);`
`811`	`811`
`812`		`- bvt bv1 = offset_literals(bv, type);`
`813`		`-`
`814`		`- bvt bv2=bv_utils.build_constant(x, offset_bits);`
`815`		`-`
`816`		`- bvt tmp=bv_utils.add(bv1, bv2);`
`817`		`-`
`818`		`- return object_offset_encoding(object_literals(bv, type), tmp);`
	`812`	`+ return offset_arithmetic(`
	`813`	`+ type, bv, 1, bv_utils.build_constant(x, offset_bits));`
`819`	`814`	`}`
`820`	`815`
`821`	`816`	`bvt bv_pointerst::offset_arithmetic(`