Difference Between Code Prover Analysis of Tests and Full Code Prover Analysis

In a typical test authoring workflow, you write a test that calls one or more functions, build the test, and finally run the test for a pass or fail status. If one of the functions under test causes run-time errors such as overflows or access out of bounds, your test results might be unreliable or you might see sporadic test failures. To avoid these issues, you can preemptively check the tested functions for run-time errors with respect to the test inputs. For more information, see Check for Bugs and Run-Time Errors in C/C++ Tests and Functions Under Test.

A Code Prover analysis of a test checks the functions under test for run-time errors with respect to the test inputs. This differs from a full Code Prover analysis, which can check functions for all inputs (subject to specified constraints). Since the analysis scope is reduced compared to a full Code Prover analysis, the analysis can run much faster and show more precise results.

Code Prover Analysis of Tests Skips xUnit API Implementation and Runs Faster

A Code Prover analysis of tests runs faster because Code Prover internally uses information about the xUnit-based test authoring API and does not analyze the API implementation.

When you author tests using the Polyspace® Test™ xUnit-based API or author tests in the user interface and generate the xUnit-based test code, you use C/C++ macros that define the test configurations and bodies. For instance, consider the following example:

  • Function under test:

    int times_two(int x) {
    return 2*x;
}

  • Test written using Polyspace Test xUnit API:

    #include <limits.h>
#include <pstunit.h>

int times_two(int); 

int param_comb1_val[] = {INT_MAX, 10, 1};
PST_PARAM_WITH_VALUES (param_comb1, int, pst_format_param_int, param_comb1_val,3);

PST_SUITE(arith_operations_suite);
PST_TEST_CONFIG(arith_operations_suite, test_times_two) {
    PST_ADD_PARAM(param_comb1);
}

PST_TEST_BODY(arith_operations_suite, test_times_two) {
    int p1 = *PST_PARAM_PTR(param_comb1);
    int p1_times_two = times_two(p1);
    PST_ASSERT(p1_times_two - p1 == p1);
}

PST_REGFCN(registerTest) {
    PST_ADD_TEST(arith_operations_suite, test_times_two);
}

#ifndef PSTEST_BUILD
int main(int argc, char* argv []) {
    PST_REGFCN_CALL(registerTest);
    return PST_MAIN(argc, argv);
}
#endif

This example uses the following test macros:

  • PST_PARAM_WITH_VALUES, which defines a test parameter.

  • PST_TEST_CONFIG, which defines a test configuration, and PST_TEST_BODY, which defines a test body.

These macros are defined in the file pstunit.c that is provided with the Polyspace Test installation. Since the macros represent standard C/C++ code, to check for run-time errors, you could have run a full Polyspace Code Prover™ analysis on a project that contains your source files with the functions under test, the test files and the file pstunit.c. However, the details of the macro definitions are not relevant for the Code Prover analysis and might lead to an unnecessary increase in analysis time (and reduction in analysis precision).

Instead, you can run a faster Code Prover analysis on the test that:

  • Does not require the test macro definitions in the file pstunit.c.

  • Replaces the actual test macro definitions with reduced stubs that allow determination of the test inputs.

  • Generates its own main function that invokes the functions under test with the test inputs.

Code Prover Analysis of Tests Checks Source Code for Test Inputs Only

A Code Prover analysis of tests checks source functions being tested only with respect to the test inputs. The objective of a Code Prover analysis of tests is to increase the reliability of your test results.

In a full Code Prover analysis, you can perform a more exhaustive run-time error checking of your application for all possible system inputs (subject to verification assumptions and any external constraints that you specify). Unlike the Code Prover analysis of tests, the objective of a full Code Prover analysis is to increase the overall reliability of your sources with respect to all inputs including ones that might not be covered in the tests.

Code Prover Analysis of Tests Ignores Specific Analysis Options

A Code Prover analysis of tests ignores certain analysis options that are only relevant for a complete Code Prover analysis. In particular, the analysis ignores these classes of options:

See Also

Topics