libTriton  version 0.6 build 1362
PathConstraint

Table of Contents

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

Description


This object is used to represent a path constraint.

>>> pcl = ctxt.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 = ctxt.getModel(b)
... for k, v in models.items():
... seed.append(v)
...
... # Branch 2, we assume that the path constraint contains a symbolic variable.
... models = ctxt.getModel(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()))
...

A possible output is :

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