Go beyond your test suite
On the previous page, we proved the absence of undefined behaviors on the test.
As you have successfully verified your first program, you may stop the configuration effort here if you are happy with the coverage of this analysis. After each new commit pushed to GitHub, TrustInSoft CI will keep running the analysis to check for non-regression.
1. Go back to the latest build without undefined behavior of our demo-caesar:
2. Click on
Inspectof the (first) analysis.
3. Once TrustInSoft CI Analyzer has loaded the new analysis, take a look at the Overview panel, which provides a few statistics about our test. In particular, the statement coverage is 94%, meaning that some statements are not reached by the analysis so not tested:
4. Click on the Statements tab (bottom) and set the Reachability filter to unreachable to see all the dead statements. 6 statements were not reached:
5. Click on the last statement in file caesar.c line 60 in the list. The Interactive code panel highlights this statement in blue:
From the code, it looks like a test that takes as input, a string with a character "greater" than "Z", should be added to reach that statement.
6. You can do the same exercise with the other dead statements highlighted in red.
Recall that demo-caesar is intended to be used with any input strings or shift values. Can you guess what you would get with the shift_value
Another undefined behavior as shown here:
abs_xis a signed integer so can only hold values between
xcontains the shift value
INT_MIN = -2147483648, calculating the opposite of
xcauses a signed overflow.
Analyzing with input values approaching or crossing the boundaries is an effective way of finding new undefined behaviors.
Finally, you may also use fuzzing to automatically generate lots of relevant inputs.
In formally verifying your tests, TrustInSoft CI goes far beyond "classic" testing, since it can detect the most subtle undefined behaviors, even when applied to well-tested code that has never revealed any problem.
But what if you would like to both achieve full statement and value coverage and stick to a decent amount of analyses?
The solution is called analysis generalization. It consists in "relaxing" the inputs of your existing analyses by specifying, as program inputs, ranges or sets of values instead of single values.
To be fully confident that the user of this library will be able to choose any integer as shift value, let's say that we'd like to test and verify with all possible integer values.
Instead of creating
tests, we can re-use the current test and specify as shift value, with the special function
tis_interval, an integer range between
INT_MAXinstead of a single integer value:
printf("\nTest 3: All shift values\n");
int shift = tis_interval(INT_MIN, INT_MAX);
gen_test(orig_str, str_len, shift);
After running the analysis again, the Values widget shows, with the notation
--, that the shift value has been initialized to the interval
The Properties widget shows that 3 undefined behaviors have been detected:
But what about the two other undefined behaviors? They both reveal a signed overflow, but on another part of the code as shown here:
The absolute value
abs_shiftof the input shift can take any value between
2147483647and the input string is made of
80. Adding the two together triggers a signed overflow.
Let's assume that you've implemented a fix. The statement coverage increases to 96%. As you've tested with all input shifts, you are on the right path, but not fully there yet!
Same as above. Instead of verifying on a limited number of additional input strings, you can specify, with the special function
tis_make_unknown, an abstract input string representing all possible char arrays of a given size:
printf("\nTest 4: All shift values and all string inputs\n");
gen_test(orig_str, str_len, shift);
Let's run the analysis again and observe the results. There's no undefined behaviors.
Assuming the library is meant to be used with any shift value between
INT_MAXand any input string of length
39, you have formally proved it is free of undefined behaviors!
As bonus, we get a statement coverage of 100%: