diff mbox series

[3/5] scheck: constants are untyped

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

in sparse, constants (PSEUDO_VALs) are not typed, so the same pseudo
can be used to represent 1-bit 0, 8-bit 0, 16-bit 0, ...

That's incompatible with the bit vectors used here, so we can't associate
a PSEUDO_VAL with its own bitvector like it's done for PSEUDO_REGs.
A fresh one is needed for each occurrence (we could use a small table
but won't bother).

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

Patch

diff --git a/scheck.c b/scheck.c
index d3ebddd6c2f5..5e2b60abb163 100644
--- a/scheck.c
+++ b/scheck.c
@@ -53,15 +53,14 @@  static BoolectorNode *mkvar(Btor *btor, BoolectorSort s, pseudo_t pseudo)
 	static char buff[33];
 	BoolectorNode *n;
 
-	if (pseudo->priv)
-		return pseudo->priv;
-
 	switch (pseudo->type) {
 	case PSEUDO_VAL:
 		sprintf(buff, "%llx", pseudo->value);
 		return boolector_consth(btor, s, buff);
 	case PSEUDO_ARG:
 	case PSEUDO_REG:
+		if (pseudo->priv)
+			return pseudo->priv;
 		n = boolector_var(btor, s, show_pseudo(pseudo));
 		break;
 	default: