search

SymbolicPathFinder / jpf-symbc

Symbolic PathFinder
https://github.com/SymbolicPathFinder/jpf-symbc
124 stars 89 forks source link

How to get the constraints on symbolic output variables according to each path condition? #92

Closed cervoliu closed 3 months ago

cervoliu commented 4 months ago

By configuring the .jpf file one can specify the symbolic method and symbolic inputs. Some related (output) variables are then represented symbolically with symbolic inputs. How do I extract the constraints on symbolic outputs on each path condition? By the way, are there any resources (docs or manuals or etc.) that explain the source code of SPF? Thanks.

sohah commented 4 months ago

Hi @cervoliu,

To get the symbolic constraints on the output variables, you will have to extract them yourself from the PathCondition at the end of the execution path.

There are some resources in the wiki. But you can also look at this presentation. It has some details about specific SPF-related architecture.

sohah commented 3 months ago

@yannicnoller, I think we can close this issue now.