Closed
Description
For a comparator like "x > comparison_point", CBMC is generating 2 test cases to confirm MC/DC: one test case with a TRUE outcome and one test case with a FALSE outcome. Although MC/DC only requires two tests, minimum good requirements-based testing for a comparator would also require 3 additional tests: one input value slightly above, one input value slightly below, and one input value equal to the comparison point. This issue aims to integrate and test the option "--cover boundary-values", which was implemented by Youcheng. #298