From: Luc Van Oostenryck <luc.vanoostenryck@xxxxxxxxx>
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@xxxxxxxxx>
---
scheck.c | 12 ++++++++++++
1 file changed, 12 insertions(+)
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);
--
2.32.0
