MATLAB: False Negative when using Polyspace Code Prover

code proverfalse negativepolyspacePolyspace Code Proverstatic analysis

Hello.

I am a beginner who is interested in Polyspace tool.

On page 63 of the Polyspace® Code Prover ™ Getting Started Guide, Code Prover says there are no false negatives.

However, as a result of static analysis of a part of NIST Juliet Test Suite for C / C ++ using Polyspace Code Prover, false negatives existed in the following CWE ID.

CWE 126 (Buffer Over-read)
CWE 561 (Dead Code)
CWE 674 (Uncontrolled Recursion)
CWE 835 (Loop with Unreachable Exit Condition ('Infinite Loop'))

I've analyzed the code, but I'm asking because I can't figure out why false negatives are occurring.

– Example of CWE 561 True Positive(Code Prover detects it.)

void CWE561_Dead_Code__return_before_code_01_bad ()

{

return;

/ * FLAW: code after the 'return' * /

printLine ("Hello");

}

– Example of CWE 561 False Negative(Code Prover cannot be detected)

static void helperBad ()

{

printLine ("helperBad ()");

}

There is no call to helperBad function anywhere.

Best Answer

Hi Hongjun,

For the two specific examples you give, you have to turn on the checks Function not called and Function not reachable. Often users are not interested in these two checks, for instance, because they are running Code Prover on units and some functions might be uncalled within an unit but eventually will get called from another unit. So these two checks are disabled by default. To enable them, use this option.

For all options related to tuning Code Prover checks, see the sections Check Behavior and Verification Assumptions.

Related Solutions

MATLAB: Can I create a C++ MEX-file S-function

We officially support C++ MEX-file S-functions as of Simulink 4.0 (R12).

To view an example of how to do this, please type:

sfundemos

at the MATLAB Command Prompt. This will open sfundemos.mdl. This demo that ships with SIMULINK provides examples of how to write different types of S-Functions and includes a C++ example.

You can also take a look at chapter 4 of the "Writing S-function" manual which has a good description on writing C++ MEX-file S-functions.

When writing the S-function, declare the MEX Function as extern "C". The rest of the code that you write can all be in C++. For example:

 extern "C" 
 {
 void mexFunction(
     int nlhs_,
     mxArray *plhs_[],
     int nrhs_,
     const mxArray *prhs_[])
 {
   /* Body can use all C++ language features and file can be compiled with a
      C++ compiler
    */
 }
 }

Below is the 'Timestwo' example written as a C++ file. You can compile the file using the MEX command. Note that if you are using the Watcom compiler, you need to add the -DNO_BUILT_IN_SUPPORT_FOR_BOOL flag to your COMPFLAGS option in your options file.

If you are using MSVC 5.0, you do not need to add this flag. The C compiler will automatically know to compile it as C++ code using the mex command.

 /*
* TIMESTWO An example C-file S-function for multiplying an input by 2
*      
*      y  = 2*x
*   
*   See sfuntmpl.c for a general S-function template.
*
*   See also VSFUNC, DSFUNC, SFUNTMPL.
* 
*   Copyright (c) 1990-96 by MathWorks, Inc.
*   All Rights Reserved
*   $Revision: 1.1 $
*/
 #ifdef __cplusplus
     extern "C" {
 #endif
 #define S_FUNCTION_NAME timestwo_level1_cpp
 /* The following three lines are necessary for the WATCOM compiler
* only. You need to remove these lines for the MSVC compiler.
*/
 #ifndef COMPILER_SUPPORTS_BOOL
 typedef int bool;
 #endif
 #include "simstruc.h"
 /*
* mdlInitializeSizes - initialize the sizes array
*/
 static void mdlInitializeSizes(SimStruct *S)
 {
     ssSetNumContStates(    S, 0);   /* number of continuous states */
     ssSetNumDiscStates(    S, 0);   /* number of discrete states */
     ssSetNumInputs(        S, DYNAMICALLY_SIZED);   /* number of inputs */
     ssSetNumOutputs(       S, DYNAMICALLY_SIZED);   /* number of outputs */
     ssSetDirectFeedThrough(S, 1);   /* direct feedthrough flag */
     ssSetNumSampleTimes(   S, 1);   /* number of sample times */
     ssSetNumSFcnParams(    S, 0);   /* number of input arguments */
     ssSetNumRWork(         S, 0);   /* number of real work vector elements */
     ssSetNumIWork(         S, 0);   /* number of integer work vector elements */
     ssSetNumPWork(         S, 0);   /* number of pointer work vector elements */
 }
 /*
* mdlInitializeSampleTimes - initialize the sample times array
*/
 static void mdlInitializeSampleTimes(SimStruct *S)
 {
     ssSetSampleTime(S, 0, CONTINUOUS_SAMPLE_TIME);
     ssSetOffsetTime(S, 0, 0.0);
 }
 /*
* mdlInitializeConditions - initialize the states
*/
 static void mdlInitializeConditions(double *x0, SimStruct *S)
 {
 }
 /*
* mdlOutputs - compute the outputs
*/
 static void mdlOutputs(double *y, double *x, double *u, SimStruct *S, int tid)
 {
     class mul2 {
         double            *u;
         double            *y;
         int                width;
     public:
         mul2(double *u_i, double *y_i, int width_i) 
         {
             u = u_i;
             y = y_i;
             width = width_i;
         }
         void output(void) 
         {
             for (int i=0;i<width;i++)
             { 
                 *y++=2.0*(*u++); 
             }
         }
     };
     class mul2 m(u,y,ssGetNumOutputs(S));
     m.output();
 }
 /*
* mdlUpdate - perform action at major integration time step
*/
 static void mdlUpdate(double *x, double *u, SimStruct *S, int tid)
 {
 }
 /*
* mdlDerivatives - compute the derivatives
*/
 static void mdlDerivatives(double *dx, double *x, 
                            double *u, SimStruct *S, int tid)
 {
 }
 /*
* mdlTerminate - called when the simulation is terminated.
*/
 static void mdlTerminate(SimStruct *S)
 {
 }
 #ifdefMATLAB_MEX_FILE    /* Is this file being compiled as a MEX-file? */
 #include "simulink.c"      /* MEX-file interface mechanism */
 #else
 #include "cg_sfun.h"       /* Code generation registration function */
 #endif
 #ifdef __cplusplus
     }
 #endif

MATLAB: CodeProver does not detect overflow/underflow with unsigned variables

Hello,

In standard C, there is no overflow on unsigned types. The C99 standard (§6.2.5/9) states:

"A computation involving unsigned operands can never overﬂow, because a result that cannot be represented by the resulting unsigned integer type is reduced modulo the number that is one greater than the largest value that can be represented by the resulting type."

Hence, by default, Code Prover will not report this kind of overflow.

Now, if you are interested by detecting them, you can change the default behavior thanks to the option "Detect overflows".

In the configuration pane, choose "Code Prover Verification" then "Check Behavior" and on the right page, for the option "Detect Overflows", select "signed and unsigned".

Please note that in your example, the overflow will appear on the assignment to the variable a, since the subtraction is performed on the int type (integral promotion).

Alex

Best Answer

Related Solutions

MATLAB: Can I create a C++ MEX-file S-function

MATLAB: CodeProver does not detect overflow/underflow with unsigned variables

Related Question