|
|
||
|
Flow checks verify whether data objects and variables are accessed according to their declared modes - for example, operation parameters of mode in can be only read, whereas parameters of mode out can be only written to. Together with grammar checks and name checks, flow checks belong to the group of three verification activities that are invoked automatically after new operation is defined (or replaced). This automatic invocation is the default behaviour that can be changed with configuration options.
When the new operation has correct body, the successful completion of all three checks is reported with green message:
In the case of incorrect grammar or name conflicts, the flow check is not run and not reported automatically.
The flow check can be explicitly requested for all or selected operations in the model:
The flow is considered to be violated when data objects, parameters or variables are accessed not in line with their intended protocol - for example, when the in parameter is written to. Even though modification of input parameters is allowed in C, it is not allowed in Ada and is considered bad practice in general. The following operation demonstrates this error:
The red part of confirmation message indicates that the third check has failed.
The same result can be reported with explicitly invoked checks as well:
This model contains two operations and only one of them fails, which can be seen after pressing the “Show details” button above. The difference between these two buttons is that the first one, which was displayed after defining a new operation, shows results for that operation only; the button from the second command will display results for all operations that were included in the check, which in this case was invoked for the whole model. Thus, the combined report for the whole model looks like this:
Operations are grouped by package and those operations that have no flow errors are reported with green “OK”. If there are any errors found, they are reported in red, listing offending operations together with their numbers. The “show” button allows to locate the error on the highlighted control flow diagram:
Another, although more subtle way to trigger similar error is to attempt updating the input parameter not by means of explicit assignment, but by another call, where the input parameter is used as actual output of the called operation:
The detailed report, after pressing the “Show details” button, looks like:
and the control flow diagram showing the offending statement is:
Flow checks can be reported in the raw form as well, which can be useful for further processing:
The above structure is a nested Association object, keyed by package names, where for each package and operation included in the check the list of errors is reported. The list can be empty for correct or undefined operations (like updateValue, which was only declared, but not yet defined) and each element of the list is a pair composed of statement number and text description.
Flow checks reported this way include only those cases that can be found by analyzing individual statements. Such checks are cheap, but not profound - for example, they do not include verification that the inOut or out parameter was actually updated in the given operation; such checks are not decidable at the statement level and require the use of formal proofs. For example:
As far as basic flow checks are concerned, there are no obvious violations in any of the individual statements, so this operation is correct:
However, more in-depth analysis is performed by proof checks:
This kind of analysis, explained in a separate chapter, allows to use information gathered from different places of the model and arrive at conclusions that are not visible at the level of individual statements. In this case the error is in the fact that output parameter y is not updated, because its updating statement happens to be in the dead (unreachable) branch.
The difference between these two kinds of checks is that flow checks, even though not as thorough, are very lightweight and can be invoked automatically, providing some added value without unnecessary burden. This way basic mistakes can be detected and cleaned up before attempting the more in-depth, but at the same time more computationally expensive, proof checks.
Previous: Name checks, next: Control flow analysis
See also Table of Contents.