diff mbox series

[5/5] scheck: fix type of operands in casts

Message ID 20210729212054.34327-6-lucvoo@kernel.org (mailing list archive)
State Mainlined, archived
Headers show
Series small fixes for the symbolic checker | expand

Commit Message

Luc Van Oostenryck July 29, 2021, 9:20 p.m. UTC 
From: Luc Van Oostenryck <luc.vanoostenryck@gmail.com>

Casts were using the target type for their operands.

Fix this by using the new helper mkivar() for them.

Signed-off-by: Luc Van Oostenryck <luc.vanoostenryck@gmail.com>
---
 scheck.c | 18 ++++++++----------
 1 file changed, 8 insertions(+), 10 deletions(-)
diff mbox series

Patch

diff --git a/scheck.c b/scheck.c
index 07b15a0600e3..bb052d97996d 100644
--- a/scheck.c
+++ b/scheck.c
@@ -165,18 +165,16 @@  static void icmp(Btor *btor, struct instruction *insn)
 
 static void unop(Btor *btor, struct instruction *insn)
 {
-	BoolectorSort s = get_sort(btor, insn->type, insn->pos);
-	BoolectorNode *t, *a;
+	pseudo_t src = insn->src;
+	BoolectorNode *t;
 
-	a = mkvar(btor, s, insn->src1);
-	if (!a)
-		return;
 	switch (insn->opcode) {
-	case OP_NEG:	t = boolector_neg(btor, a); break;
-	case OP_NOT:	t = boolector_not(btor, a); break;
-	case OP_SEXT:	t = sext(btor, insn, a); break;
-	case OP_ZEXT:	t = zext(btor, insn, a); break;
-	case OP_TRUNC:	t = slice(btor, insn, a); break;
+	case OP_SEXT:	t = sext(btor, insn, mkivar(btor, insn, src)); break;
+	case OP_ZEXT:	t = zext(btor, insn, mkivar(btor, insn, src)); break;
+	case OP_TRUNC:	t = slice(btor, insn, mkivar(btor, insn, src)); break;
+
+	case OP_NEG:	t = boolector_neg(btor, mktvar(btor, insn, src)); break;
+	case OP_NOT:	t = boolector_not(btor, mktvar(btor, insn, src)); break;
 	default:
 		fprintf(stderr, "unsupported insn: %s\n", show_instruction(insn));
 		return;