Using Pragma Assert to Set Data Ranges

You can use the construct 'pragma assert' within your code to inform Polyspace® of constraints imposed by the environment in which the software will run. A "pragma assert" function is:

pragma assert(<integer expression>);

If <integer expression> evaluates to zero, then the program is assumed to be terminated, therefore there is a "real" run-time error. This condition is why Polyspace produces checks for the assertions. The behavior matches the one exhibited during execution, because execution paths for unsatisfied conditions are truncated (red and then gray). Thus it can be assumed that a verification performed downstream of the assert uses value ranges which satisfy the assert conditions.

You can use the construct 'pragma assert' in a procedure to inform Polyspace of constraints in the environment in which the software will be embedded. You can use user assertions to describe the physical properties of the environment, such as:

  • The maximum and minimum speed limit (a car does not go faster than 200 miles per hour or slower than 0 miles per hour),

  • The maximum duration of software exploitation (five years for a satellite and one hour for its launcher)


procedure main is   
        counter: integer;   
        -- counter is not initialized  
        random: integer;   
        pragma volatile (random); 
        counter:= random;  
        -- counter~ [-2^31, 2^31-1]   
        pragma assert (counter < 1000);   
        pragma assert (counter > 100); 

end main;

Both assertions are orange because the conditions may or may not be fulfilled. From then on, counter ~ [101, 999] because execution paths that do not meet the conditions are halted.

Was this topic helpful?