www.gusucode.com > polyspace_code_prover 案例源码程序 matlab代码 > polyspace_code_prover/GenerateAndVerifyCodeExample.m

    %% Verify Generated Code
% Verify code generated from models by using
% Polyspace Code Prover. Polyspace Code Prover proves code correctness,
% finds run-time errors, and checks for MISRA-C compliance in generated and
% handwritten code.
%% Open Model
% Open the example model.
%%
modelName = 'psdemo_model_link_sl';
open_system(modelName)
%% Generate Code
% Generate code for the |controller| subsystem in the model.
%
% # Right-click the |controller| subsystem and select *C/C++ Code* > *Build
% This SubSystem*.
% # In the dialog box, select *Build*.
%
%% Verify Code
% Verify the code generated for the |controller| subsystem.
% 
% # Right-click the |controller| subsystem again and select *Polyspace* >
% *Verify Code Generated for* > *Selected Subsystem*.
% # Follow the progress of verification in the MATLAB Command Window.
% 
%% Review Verification Results
% After verification, the results are displayed in the Polyspace user
% interface. The results consist of checks that are color-coded as follows:
%
% * *Green (proven code)* : The check does not fail for the data
% constraints provided. For instance, a division operation does not cause a
% *Division by Zero* error.
% * *Red (verified error)*: The check always fails for the set of data
% constraints provided. For instance, a division operation always causes a
% *Division by Zero* error.
% * *Orange (possible error)*: The check indicates unproven code and can
% fail for certain values of the data constraints provided. For instance, a
% division operation sometimes causes a *Division by Zero* error.
% * *Gray (unreachable code)*: The check indicates a code operation that
% cannot be reached for the data constraints provided.
%
% Review each verification result in detail. For instance:
%
% # On the *Results List* pane, select the red *Out of bounds array
% index* check.
% # On the *Source* pane, place your cursor on the red check to view
% additional information. For instance, the tooltip on the red |[| operator
% states the array size and possible values of the array index. The *Result
% Details* pane also provides this information.
%
% The error occurs in a handwritten C file |Command_strategy_file.c|. The C
% file is inside an S-Function block |Command_Strategy| in the
% |controller| subsystem.
%% Trace Errors Back to Model and Fix Them
% For code generated from the model, you can trace an error back to your
% model.
%
% *Error 1: Out of bounds array index*
%
% # On the *Results List* pane, select the orange *Out of bounds array
% index* error that occurs in the file |controller.c|.
% # On the *Source* pane, click the link *S5:76* in comments above the
% orange error. 
% 
% <<../orange_obai.png>>
%
% You see that the error occurs due to a transition in the Stateflow chart
% |synch_and_asynch_monitoring|. You can trace the error to the input
% variable |index| of the Stateflow chart. 
% 
% <<../stateflow_chart_error_source.png>>
%
% You can avoid the *Out of bounds array index* in several ways. One way is
% to constrain the input variable |index| using a Saturation block before
% the Stateflow chart.
%
% *Error 2: Overflow*
% 
% # On the *Results List* pane, select the orange *Overflow* 
% error shown below. The error appears in the file |controller.c|.
% # On the *Source* pane, review the error. To trace the error back to the
% model, click the link *S2/Gain* in comments above the orange error.
% 
% <<../orange_ovfl.png>>
%
% You see that the error occurs in the |Fault Management| subsystem inside
% a Gain block following a Sum block. 
% 
% <<../back_to_model_orange_ovfl.png>>
%
% You can avoid the *Overflow* in several ways. One way is to constrain the
% value of the signal |in_battery_info| that is fed to the Sum block. To
% constrain the signal:
%
% # Double-click the Inport block *Battery info* that provides the input
% signal |in_battery_info| to the |controller| subsystem.
% # On the *Signal Attributes* tab, change the *Maximum* value of the
% signal.
%
% The errors in this model occur due to one or more of the following:
%
% * Faulty scaling, unknown calibrations and untested data ranges coming
% out of a subsystem into an arithmetic block.
% * Array manipulation in Stateflow event-based modelling and handwritten
% lookup table functions.
% * Saturations leading to unexpected data flow inside the generated code.
% * Faulty Stateflow programming.
% 
% Once you identify the root cause of the error, you can modify the model
% appropriately to fix the issue.
%% Check for Coding Rule Violations
%
% To check for coding rule violations, before starting code verification:
%
% # Right-click the |controller| subsystem and select *Polyspace* >
% *Options*.
% # In the Configuration Parameters dialog box, select an appropriate
% option in the *Settings from* list. For instance, select |Project
% configuration and MISRA C 2012 AGC Checking|.
% # Click *Apply* or *OK* and rerun the verification.

%% Annotate Blocks to Justify Results
% 
% You can justify your results by adding annotations to your blocks. During
% code verification, Polyspace Code Prover reads your annotations and
% populates the result with your justification. Once you justify a result,
% you do not have to review it again.
%
% # On the *Results List* pane, from the drop-down list in the upper
% left corner, select *File*.
% # In the file |controller.c|, in the function |controller_step()|, select
% the violation of MISRA C:2012 rule 10.4. The *Source* pane shows that an
% addition operation violates the rule.
% # On the *Source* pane, click the link *S2/Sum1* in comments above the
% addition operation. 
%
% <<../rule_violation.png>>
%
% You see that the rule violation occurs in a Sum block. 
%
% <<../annotate_block.png>>
%
% To annotate this block and justify the rule violation:
% 
% # Right-click the block and select *Polyspace* > *Annotate Selected
% Block* > *Edit*.
% # Select |MISRA-C-2012| for *Annotation type* and enter information about
% the rule violation. Set the *Status* to *No action planned* and the
% *Severity* to *Not a defect*.
% # Click *Apply* or *OK*. The words *Polyspace annotation* appear below
% the block, indicating that the block contains a code annotation.
% # Regenerate code and rerun the verification. The *Severity* and *Status*
% columns on the *Results Summary* pane are prepopulated with your
% annotations.