libTriton  version 0.4 build 1356
PathConstraint

Table of Contents

[python api] All information about the PathConstraint python object.

Description


This object is used to represent a path constraint.

>>> pcl = getPathConstraints()
>>> for pc in pcl:
... if pc.isMultipleBranches():
... b1 = pc.getBranchConstraints()[0]['constraint']
... b2 = pc.getBranchConstraints()[1]['constraint']
...
... print 'Constraint branch 1:', b1
... print 'Constraint branch 2:', b2
...
... seed = list()
...
... # Branch 1, we assume that the path constraint contains a symbolic variable
... models = getModel(assert_(b1))
... for k, v in models.items():
... seed.append(v)
...
... # Branch 2, we assume that the path constraint contains a symbolic variable.
... models = getModel(assert_(b2))
... for k, v in models.items():
... seed.append(v)
...
... if seed:
... print 'B1: %s (%c) | B2: %s (%c)' %(seed[0], chr(seed[0].getValue()), seed[1], chr(seed[1].getValue())
...
Constraint branch 1: (not (= (ite (= ((_ extract 0 0) ref!179) (_ bv1 1)) (_ bv4195769 64) (_ bv4195762 64)) (_ bv4195762 64)))
Constraint branch 2: (= (ite (= ((_ extract 0 0) ref!179) (_ bv1 1)) (_ bv4195769 64) (_ bv4195762 64)) (_ bv4195762 64))
B1: SymVar_0 = 65 (e) | B2: SymVar_0 = 0 ()
[...]
>>>

Python API - Methods of the PathConstraint class