Skip to content

Commit 3da969b

Browse files
authored
Expressions use keyword-only arguments for init (#2395)
A better way to enforce correct initialization of the objects
1 parent 29061a2 commit 3da969b

File tree

16 files changed

+424
-334
lines changed

16 files changed

+424
-334
lines changed

manticore/core/smtlib/constraints.py

Lines changed: 15 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -93,7 +93,7 @@ def add(self, constraint) -> None:
9393
:param constraint: The constraint to add to the set.
9494
"""
9595
if isinstance(constraint, bool):
96-
constraint = BoolConstant(constraint)
96+
constraint = BoolConstant(value=constraint)
9797
assert isinstance(constraint, Bool)
9898
constraint = simplify(constraint)
9999
# If self._child is not None this constraint set has been forked and a
@@ -380,8 +380,7 @@ def new_bool(self, name=None, taint=frozenset(), avoid_collisions=False):
380380
name = self._make_unique_name(name)
381381
if not avoid_collisions and name in self._declarations:
382382
raise ValueError(f"Name {name} already used")
383-
var = BoolVariable(name, taint=taint)
384-
return self._declare(var)
383+
return self._declare(BoolVariable(name=name, taint=taint))
385384

386385
def new_bitvec(self, size, name=None, taint=frozenset(), avoid_collisions=False):
387386
"""Declares a free symbolic bitvector in the constraint store
@@ -400,8 +399,7 @@ def new_bitvec(self, size, name=None, taint=frozenset(), avoid_collisions=False)
400399
name = self._make_unique_name(name)
401400
if not avoid_collisions and name in self._declarations:
402401
raise ValueError(f"Name {name} already used")
403-
var = BitVecVariable(size, name, taint=taint)
404-
return self._declare(var)
402+
return self._declare(BitVecVariable(size=size, name=name, taint=taint))
405403

406404
def new_array(
407405
self,
@@ -430,5 +428,15 @@ def new_array(
430428
name = self._make_unique_name(name)
431429
if not avoid_collisions and name in self._declarations:
432430
raise ValueError(f"Name {name} already used")
433-
var = self._declare(ArrayVariable(index_bits, index_max, value_bits, name, taint=taint))
434-
return ArrayProxy(var, default=default)
431+
return ArrayProxy(
432+
array=self._declare(
433+
ArrayVariable(
434+
index_bits=index_bits,
435+
index_max=index_max,
436+
value_bits=value_bits,
437+
name=name,
438+
taint=taint,
439+
)
440+
),
441+
default=default,
442+
)

0 commit comments

Comments
 (0)