Skip to content

[JAVA] Adding a 2nd property on the replace benchmark

Vaibhav Sharma requested to merge github/fork/vaibhavbsharma/replace5_eqchk-2 into master

This PR adds another equivalence-checking property on the replace benchmark. It also makes changes recommended under #860.

The replace program is part of the Siemens suite of programs. This benchmark performs pattern matching and substitution. One simple property that should fail on this benchmark is that the outputs of the benchmark from running it twice should not be equivalent if the starting states of the benchmark were not equivalent. This is done by not resetting the benchmark to its starting state. This benchmark was obtained from Wang et al. (https://labs.xjtudlc.com/labs/wlaq/hjwang/toolbench.html).

  • equivalence-check on the replace benchmark in a folder named replace5_eqchk
  • This benchmark wasn't distributed with a license. However, since this benchmark is being contributed by the developers of Java Ranger, we're adding under the same license used to maintain Java Ranger. Since Java Ranger is an extension of SPF, the same license as SPF and JPF also applies to this benchmark.
  • contributed by Java Ranger (https://github.com/vaibhavbsharma/java-ranger) but the benchmark was originally distributed by Wang et al. (https://labs.xjtudlc.com/labs/wlaq/hjwang/toolbench.html).
  • replace5_eqchk has been added under java-ranger-regressions which has been added to ReachSafety.set
  • assert.prp has been used as the property file
  • replace5_prop1.yml and replace5_prop2 are the task definition files. The implementation has been moved to a impl/ folder. The implementations for the two properties have been moved to prop1/ and prop2/ folders.

Merge request reports