SymbolicPathFinder / jpf-symbc

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

Match statement with constraints #38

Closed dah-fari7009 closed 4 years ago

dah-fari7009 commented 4 years ago

Good morning,

I was wondering iif there is a way to know which specific statement in a program generated a given path constraint in the path summaries obtained with Symbolic PathFinder ? Here I mean, let's say I have this bit of code :

tesssttt

I obtain a summary like (val > 2) && val = 3 V (val<=2) && val =2 Is there a way for me to know during the symbolic execution that (val > 2) was obtained when parsing line 3 ?

Thanks !

corinus commented 4 years ago

The PCChoiceGenerator records that information (in method and offset)