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.