No Unassigned Mode-Out Procedure Parameters (RPP04)

Level \(\rightarrow\) Required

Category

Safety:

\(\checkmark\)

Cyber:

\(\checkmark\)

Goal

Maintainability:

\(\checkmark\)

Reliability:

\(\checkmark\)

Portability:

\(\checkmark\)

Performance:

Security:

Remediation \(\rightarrow\) High

Verification Method \(\rightarrow\) GNATcheck rule: Unassigned_OUT_Parameters

Reference

MISRA C Rule 9.1 "The value of an object with automatic storage duration shall not be read before it has been set"

Description

For any procedure, all formal parameters of mode out must be assigned a value if the procedure exits normally. This rule ensures that, upon a normal return, the corresponding actual parameter has a defined value. Ensuring a defined value is especially important for scalar parameters because they are passed by value, such that some value is copied out to the actual. These undefined values can be especially difficult to locate because evaluation of the actual parameter's value might not occur immediately after the call returns.

Applicable Vulnerability within ISO TR 24772-2

• 6.32 Passing parameters and return values [CSJ]

Noncompliant Code Example

for Value_T use
  (Alpha   => 2#1#,
   Baker   => 2#10#,
   Charlie => 2#100#,
   Dog     => 2#1000#,
   Invalid => 2#1111#);

procedure Noncompliant (Register  :     Character;
                        Registera : out Value_T;
                        Registerb : out Value_T) is
begin
   if Register = 'A' then
      Registera := Alpha;
   end if;
end Noncompliant;

In the above example, some value is copied back for an output parameter as specified by Register. The other parameter is not assigned, and on return the value copied to the actual parameter may not be a valid representation for a value of the type. (We give the enumeration values a non-standard representation for the sake of illustration, i.e., to make it more likely that the undefined value is not valid.)

Compliant Code Example

procedure Compliant (Register  :     Character;
                     Registera : out Value_T;
                     Registerb : out Value_T) is
begin
   Registera := Invalid;
   Registerb := Invalid;
   if Register = 'A' then
      Registera := Alpha;
   end if;
end Compliant;

Notes

The GNATcheck rule specified above only detects a trivial case of an unassigned variable and doesn't provide a guarantee that there is no uninitialized access. It is not a replacement for a rigorous check for uninitialized access provided by advanced static analysis tools such as SPARK and CodePeer.

Note that the GNATcheck rule does not check function parameters (as of Ada 2012 functions can have out parameters). As a result, the better choice is either SPARK or CodePeer.