对代码进行注解以申述 Polyspace 检查
此示例说明如何在生成的代码中打开注释,这些注释会抑制通过 Polyspace® 进行错误检测。
Polyspace 检查
使用 Polyspace Code Prover™ 软件,您可以将 Polyspace 验证应用于 Embedded Coder® 生成的代码。该软件检测生成代码中的运行时错误,并帮助您定位和修复模型故障。由于代码生成器实现某些合法运算的方式,Polyspace 可能会标记这些合法运算的溢出。Polyspace 不应标记这些合法的溢出。在代码中生成抑制此错误检测的注释。
代码生成
1.打开示例 Simulink® 模型 mSatAddSub。
model='mSatAddSub';
open_system(model);

2.在 Embedded Coder 上的配置参数对话框中,关闭运算符注解。
set_param('mSatAddSub','OperatorAnnotations','off');
3.要编译模型并生成代码,请按 Ctrl+B。
evalc('slbuild(''mSatAddSub'')');
%The generated code is: file = fullfile('mSatAddSub_ert_rtw','mSatAddSub.c'); coder.example.extractLines(file,'/* Model step function */',... 'End of Sum',1,1);
/* Model step function */
void mSatAddSub_step(void)
{
uint32_T qY;
/* Sum: '<Root>/SubUnsigned' incorporates:
* Inport: '<Root>/In1'
* Inport: '<Root>/In2'
*/
qY = U1 - U2;
if (qY > U1) {
qY = 0U;
}
/* Sum: '<Root>/SubUnsigned' */
USub = qY;
/* Outport: '<Root>/Out3' */
mSatAddSub_Y.Out3 = USub;
/* Matfile logging */
rt_UpdateTXYLogVars(mSatAddSub_M->rtwLogInfo, (&mSatAddSub_M->Timing.taskTime0));
/* signal main to stop simulation */
{ /* Sample time: [1.0s, 0.0s] */
if ((rtmGetTFinal(mSatAddSub_M)!=-1) &&
!((rtmGetTFinal(mSatAddSub_M)-mSatAddSub_M->Timing.taskTime0) >
mSatAddSub_M->Timing.taskTime0 * (DBL_EPSILON))) {
rtmSetErrorStatus(mSatAddSub_M, "Simulation finished");
}
}
/* Update absolute time for base rate */
/* The "clockTick0" counts the number of times the code of this task has
* been executed. The absolute time is the multiplication of "clockTick0"
* and "Timing.stepSize0". Size of "clockTick0" ensures timer will not
* overflow during the application lifespan selected.
*/
mSatAddSub_M->Timing.taskTime0 =
((time_T)(++mSatAddSub_M->Timing.clockTick0)) *
mSatAddSub_M->Timing.stepSize0;
}
/* Model initialize function */
void mSatAddSub_initialize(void)
{
/* Registration code */
/* initialize non-finites */
rt_InitInfAndNaN(sizeof(real_T));
/* initialize real-time model */
(void) memset((void *)mSatAddSub_M, 0,
sizeof(RT_MODEL_mSatAddSub));
rtmSetTFinal(mSatAddSub_M, 1.0);
mSatAddSub_M->Timing.stepSize0 = 1.0;
/* Setup for data logging */
{
static RTWLogInfo rt_DataLoggingInfo;
rt_DataLoggingInfo.loggingInterval = (NULL);
mSatAddSub_M->rtwLogInfo = &rt_DataLoggingInfo;
}
/* Setup for data logging */
{
rtliSetLogXSignalInfo(mSatAddSub_M->rtwLogInfo, (NULL));
rtliSetLogXSignalPtrs(mSatAddSub_M->rtwLogInfo, (NULL));
rtliSetLogT(mSatAddSub_M->rtwLogInfo, "tout");
rtliSetLogX(mSatAddSub_M->rtwLogInfo, "");
rtliSetLogXFinal(mSatAddSub_M->rtwLogInfo, "");
rtliSetLogVarNameModifier(mSatAddSub_M->rtwLogInfo, "rt_");
rtliSetLogFormat(mSatAddSub_M->rtwLogInfo, 1);
rtliSetLogMaxRows(mSatAddSub_M->rtwLogInfo, 1000);
rtliSetLogDecimation(mSatAddSub_M->rtwLogInfo, 1);
/*
* Set pointers to the data and signal info for each output
*/
{
static void * rt_LoggedOutputSignalPtrs[] = {
&mSatAddSub_Y.Out3
};
rtliSetLogYSignalPtrs(mSatAddSub_M->rtwLogInfo, ((LogSignalPtrsType)
rt_LoggedOutputSignalPtrs));
}
{
static int_T rt_LoggedOutputWidths[] = {
1
};
static int_T rt_LoggedOutputNumDimensions[] = {
1
};
static int_T rt_LoggedOutputDimensions[] = {
1
};
static boolean_T rt_LoggedOutputIsVarDims[] = {
0
};
static void* rt_LoggedCurrentSignalDimensions[] = {
(NULL)
};
static int_T rt_LoggedCurrentSignalDimensionsSize[] = {
4
};
static BuiltInDTypeId rt_LoggedOutputDataTypeIds[] = {
SS_UINT32
};
static int_T rt_LoggedOutputComplexSignals[] = {
0
};
static RTWPreprocessingFcnPtr rt_LoggingPreprocessingFcnPtrs[] = {
(NULL)
};
static const char_T *rt_LoggedOutputLabels[] = {
"USub" };
static const char_T *rt_LoggedOutputBlockNames[] = {
"mSatAddSub/Out3" };
static RTWLogDataTypeConvert rt_RTWLogDataTypeConvert[] = {
{ 0, SS_UINT32, SS_UINT32, 0, 0, 0, 1.0, 0, 0.0 }
};
static RTWLogSignalInfo rt_LoggedOutputSignalInfo[] = {
{
1,
rt_LoggedOutputWidths,
rt_LoggedOutputNumDimensions,
rt_LoggedOutputDimensions,
rt_LoggedOutputIsVarDims,
rt_LoggedCurrentSignalDimensions,
rt_LoggedCurrentSignalDimensionsSize,
rt_LoggedOutputDataTypeIds,
rt_LoggedOutputComplexSignals,
(NULL),
rt_LoggingPreprocessingFcnPtrs,
{ rt_LoggedOutputLabels },
(NULL),
(NULL),
(NULL),
{ rt_LoggedOutputBlockNames },
{ (NULL) },
(NULL),
rt_RTWLogDataTypeConvert
}
};
rtliSetLogYSignalInfo(mSatAddSub_M->rtwLogInfo, rt_LoggedOutputSignalInfo);
/* set currSigDims field */
rt_LoggedCurrentSignalDimensions[0] = &rt_LoggedOutputWidths[0];
}
rtliSetLogY(mSatAddSub_M->rtwLogInfo, "yout");
}
/* block I/O */
/* exported global signals */
USub = 0U;
/* external inputs */
U1 = 0U;
U2 = 0U;
/* external outputs */
mSatAddSub_Y.Out3 = 0U;
/* Matfile logging */
rt_StartDataLoggingWithStartTime(mSatAddSub_M->rtwLogInfo, 0.0, rtmGetTFinal
(mSatAddSub_M), mSatAddSub_M->Timing.stepSize0, (&rtmGetErrorStatus
(mSatAddSub_M)));
}
/* Model terminate function */
void mSatAddSub_terminate(void)
{
/* (no terminate code required) */
}
/*
* File trailer for generated code.
*
* [EOF]
*/
4.运行 Polyspace 检查。代码生成器识别出最大的内置数据类型是 32 位。无法使用 0U 和更大的单字整数数据类型对减法的所有结果进行饱和处理。在这种情况下,软件会检测结果溢出和溢出的方向,并对结果进行饱和处理。Polyspace 会标记此运算,因为它无法识别饱和处理。
5.在 Embedded Coder 上的配置参数对话框中,打开运算符注解。
set_param('mSatAddSub','OperatorAnnotations',"on"); evalc('slbuild(''mSatAddSub'')');
6.生成的代码如下:
file = fullfile('mSatAddSub_ert_rtw','mSatAddSub.c'); coder.example.extractLines(file,'/* Model step function */',... 'End of Sum',1,1);
/* Model step function */
void mSatAddSub_step(void)
{
uint32_T qY;
/* Sum: '<Root>/SubUnsigned' incorporates:
* Inport: '<Root>/In1'
* Inport: '<Root>/In2'
*/
qY = U1 -
/*MW:operator MISRA2012:D4.1 CERT-C:INT30-C 'Justifying MISRA C rule violation'*/
/*MW:OvSatOk*/ U2;
if (qY > U1) {
qY = 0U;
}
/* Sum: '<Root>/SubUnsigned' */
USub = qY;
/* Outport: '<Root>/Out3' */
mSatAddSub_Y.Out3 = USub;
/* Matfile logging */
rt_UpdateTXYLogVars(mSatAddSub_M->rtwLogInfo, (&mSatAddSub_M->Timing.taskTime0));
/* signal main to stop simulation */
{ /* Sample time: [1.0s, 0.0s] */
if ((rtmGetTFinal(mSatAddSub_M)!=-1) &&
!((rtmGetTFinal(mSatAddSub_M)-mSatAddSub_M->Timing.taskTime0) >
mSatAddSub_M->Timing.taskTime0 * (DBL_EPSILON))) {
rtmSetErrorStatus(mSatAddSub_M, "Simulation finished");
}
}
/* Update absolute time for base rate */
/* The "clockTick0" counts the number of times the code of this task has
* been executed. The absolute time is the multiplication of "clockTick0"
* and "Timing.stepSize0". Size of "clockTick0" ensures timer will not
* overflow during the application lifespan selected.
*/
mSatAddSub_M->Timing.taskTime0 =
((time_T)(++mSatAddSub_M->Timing.clockTick0)) *
mSatAddSub_M->Timing.stepSize0;
}
/* Model initialize function */
void mSatAddSub_initialize(void)
{
/* Registration code */
/* initialize non-finites */
rt_InitInfAndNaN(sizeof(real_T));
/* initialize real-time model */
(void) memset((void *)mSatAddSub_M, 0,
sizeof(RT_MODEL_mSatAddSub));
rtmSetTFinal(mSatAddSub_M, 1.0);
mSatAddSub_M->Timing.stepSize0 = 1.0;
/* Setup for data logging */
{
static RTWLogInfo rt_DataLoggingInfo;
rt_DataLoggingInfo.loggingInterval = (NULL);
mSatAddSub_M->rtwLogInfo = &rt_DataLoggingInfo;
}
/* Setup for data logging */
{
rtliSetLogXSignalInfo(mSatAddSub_M->rtwLogInfo, (NULL));
rtliSetLogXSignalPtrs(mSatAddSub_M->rtwLogInfo, (NULL));
rtliSetLogT(mSatAddSub_M->rtwLogInfo, "tout");
rtliSetLogX(mSatAddSub_M->rtwLogInfo, "");
rtliSetLogXFinal(mSatAddSub_M->rtwLogInfo, "");
rtliSetLogVarNameModifier(mSatAddSub_M->rtwLogInfo, "rt_");
rtliSetLogFormat(mSatAddSub_M->rtwLogInfo, 1);
rtliSetLogMaxRows(mSatAddSub_M->rtwLogInfo, 1000);
rtliSetLogDecimation(mSatAddSub_M->rtwLogInfo, 1);
/*
* Set pointers to the data and signal info for each output
*/
{
static void * rt_LoggedOutputSignalPtrs[] = {
&mSatAddSub_Y.Out3
};
rtliSetLogYSignalPtrs(mSatAddSub_M->rtwLogInfo, ((LogSignalPtrsType)
rt_LoggedOutputSignalPtrs));
}
{
static int_T rt_LoggedOutputWidths[] = {
1
};
static int_T rt_LoggedOutputNumDimensions[] = {
1
};
static int_T rt_LoggedOutputDimensions[] = {
1
};
static boolean_T rt_LoggedOutputIsVarDims[] = {
0
};
static void* rt_LoggedCurrentSignalDimensions[] = {
(NULL)
};
static int_T rt_LoggedCurrentSignalDimensionsSize[] = {
4
};
static BuiltInDTypeId rt_LoggedOutputDataTypeIds[] = {
SS_UINT32
};
static int_T rt_LoggedOutputComplexSignals[] = {
0
};
static RTWPreprocessingFcnPtr rt_LoggingPreprocessingFcnPtrs[] = {
(NULL)
};
static const char_T *rt_LoggedOutputLabels[] = {
"USub" };
static const char_T *rt_LoggedOutputBlockNames[] = {
"mSatAddSub/Out3" };
static RTWLogDataTypeConvert rt_RTWLogDataTypeConvert[] = {
{ 0, SS_UINT32, SS_UINT32, 0, 0, 0, 1.0, 0, 0.0 }
};
static RTWLogSignalInfo rt_LoggedOutputSignalInfo[] = {
{
1,
rt_LoggedOutputWidths,
rt_LoggedOutputNumDimensions,
rt_LoggedOutputDimensions,
rt_LoggedOutputIsVarDims,
rt_LoggedCurrentSignalDimensions,
rt_LoggedCurrentSignalDimensionsSize,
rt_LoggedOutputDataTypeIds,
rt_LoggedOutputComplexSignals,
(NULL),
rt_LoggingPreprocessingFcnPtrs,
{ rt_LoggedOutputLabels },
(NULL),
(NULL),
(NULL),
{ rt_LoggedOutputBlockNames },
{ (NULL) },
(NULL),
rt_RTWLogDataTypeConvert
}
};
rtliSetLogYSignalInfo(mSatAddSub_M->rtwLogInfo, rt_LoggedOutputSignalInfo);
/* set currSigDims field */
rt_LoggedCurrentSignalDimensions[0] = &rt_LoggedOutputWidths[0];
}
rtliSetLogY(mSatAddSub_M->rtwLogInfo, "yout");
}
/* block I/O */
/* exported global signals */
USub = 0U;
/* external inputs */
U1 = 0U;
U2 = 0U;
/* external outputs */
mSatAddSub_Y.Out3 = 0U;
/* Matfile logging */
rt_StartDataLoggingWithStartTime(mSatAddSub_M->rtwLogInfo, 0.0, rtmGetTFinal
(mSatAddSub_M), mSatAddSub_M->Timing.stepSize0, (&rtmGetErrorStatus
(mSatAddSub_M)));
}
/* Model terminate function */
void mSatAddSub_terminate(void)
{
/* (no terminate code required) */
}
/*
* File trailer for generated code.
*
* [EOF]
*/
代码生成器插入了 /*MW:OvSatOk*/ 注释,该注释会隐藏 Polyspace 检测到的错误。
7.关闭模型。
bdclose(model)
另请参阅
主题
- Model Configuration Parameters: Comments
- 对通过 Embedded Coder 生成的代码运行 Polyspace 分析 (Polyspace Bug Finder)