sohah / ContractDR

Java Ranger is a path-merging extension of Symbolic PathFinder
https://github.com/SymbolicPathFinder/jpf-symbc
1 stars 0 forks source link

Support calling repair node with all variables that belong to the same category (input/output). #3

Closed sohah closed 4 years ago

sohah commented 4 years ago

We need to support calling the repair node with all variables that belong to the same category. For example

if the mutated spec is a and b and c and d where a, b are inputs, cand dare outputs. Then one possible repair option would be

repair(a, repairNode(a)) and b and c and d.

In the extension we want to add is to allow another configuration that would support the following, mainly the wrapping would depend on the category of a. In this example for instance, looking at a we realize that it is an input and so we'll repair allowing all inputs to appear at the point. So the call to the repairNode would instead be

repair(a, repairNode(a,b)) and b and c and d

This setup allows our tool to bring in new terms that do not exist in the mutated expression.

vaibhavbsharma commented 4 years ago

I've fixed this issue now. We're now respecting the repairScope which can be set using the "dimension" parameter in the JPF configuration file.