[PATCH 3/5] scheck: constants are untyped

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]


From: Luc Van Oostenryck <luc.vanoostenryck@xxxxxxxxx>

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@xxxxxxxxx>
 scheck.c | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

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));

[Index of Archives]     [Newbies FAQ]     [LKML]     [IETF Annouce]     [DCCP]     [Netdev]     [Networking]     [Security]     [Bugtraq]     [Yosemite]     [MIPS Linux]     [ARM Linux]     [Linux Security]     [Linux RAID]     [Linux SCSI]     [Trinity Fuzzer Tool]

  Powered by Linux