diff mbox series

[4/5] scheck: mkvar() with target or input type

Message ID 20210729212054.34327-5-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>

Most instructions have one associated type, the 'target type'.
Some, like compares, have another one too, the 'input type'.

So, when creating a bitvector from an instruction, we need to specify
the type in some way.

So, create an helper for both cases: mktvar() and mkivar().

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

Patch

diff --git a/scheck.c b/scheck.c
index 5e2b60abb163..07b15a0600e3 100644
--- a/scheck.c
+++ b/scheck.c
@@ -70,6 +70,18 @@  static BoolectorNode *mkvar(Btor *btor, BoolectorSort s, pseudo_t pseudo)
 	return pseudo->priv = n;
 }
 
+static BoolectorNode *mktvar(Btor *btor, struct instruction *insn, pseudo_t src)
+{
+	BoolectorSort s = get_sort(btor, insn->type, insn->pos);
+	return mkvar(btor, s, src);
+}
+
+static BoolectorNode *mkivar(Btor *btor, struct instruction *insn, pseudo_t src)
+{
+	BoolectorSort s = get_sort(btor, insn->itype, insn->pos);
+	return mkvar(btor, s, src);
+}
+
 static BoolectorNode *get_arg(Btor *btor, struct instruction *insn, int idx)
 {
 	pseudo_t arg = ptr_list_nth(insn->arguments, idx);