MATLAB: Polyspace verification fails during compilation stage while verifying Ada code

Why does Ada code verification using Polyspace fail during the compilation phase with the below error message:

_Verifying _pst_main
Verifying gnat_oslib
gnat_oslib.adb, line 5 (column 19): Error:
"Normalize_Pathname" not declared(1) in "OS_Lib"
Warning: Failed compilation of gnat_oslib_

Best Answer

The above error occurs because Gnat_oslib specs, which is included in

%POLYSPACE_ADA%\Verifier\ada83include\g-os_lib.ads

($POLYSPACE_ADA/Verifier/ada83include/g-os_lib.ads for Unix), does not contain a declaration for the procedure _Normalize_Pathname_

To work around the issue:

Copy g-os_lib.ads, which includes a declaration of the procedure _Normalize_Pathname_, from adaincludes of your compiler.
Add g-os_lib.ads to your source folder.
Run the verification again.

Related Solutions

MATLAB: Can I perform with code verification for Ada if I have Polyspace Bug Finder and PolySpace Code Prover

Code verification for Ada requires the Polyspace Client for Ada, which is a separate product from PolySpace Bug Finder and PolySpace Code Prover.

To purchase the PolySpace Client for Ada, please reach out to your company's MathWorks sales representative, or contact the MathWorks sales department.

MATLAB: Verifying user input

If you're using a Command Window interface, then you could employ this function, which I wrote a while back. I use it to ensure the user gives a numerical input. It also insists on a scalar value. You can easily modify it to ensure that the number is real, and/or an integer, as well, by modifying the subfunction checknum.

function i = getnum(prompt, default)
% GETNUM Read a numerical value from the keyboard
%

%    I = GETNUM(PROMPT) prints the string PROMPT and waits for the user
%    to type a number followed by return. Checks that the input does
%    actually represent a scalar and prompts again if necessary.
%    Returns the number.
%
%    I = GETNUM(PROMPT, DEFAULT) does the same except that the number
%    DEFAULT is printed after the prompt, and is returned if the user
%    just presses return. Setting DEFAULT to [] is the same as omitting
%    it.
% David Young, March 2002
if nargin < 2
    default = [];
end
if isempty(default)
    str = prompt;
else
    if ~checknum(default)
        error('Expecting numerical default argument');
    end;
    str = [prompt, ' [', num2str(default), '] '];
end;
i = [];
while isempty(i)
    i = input(str, 's');
    if isempty(i) && ~isempty(default)
        i = default;
    else
        i = str2num(i); %#ok<ST2NM>
        if ~checknum(i)
            disp('A single number expected');
            i = [];
        end
    end
end
end
function i = checknum(x)
% Checks whether its argument is a single number
i = isnumeric(x) && isscalar(x);
end

Best Answer

Related Solutions

MATLAB: Can I perform with code verification for Ada if I have Polyspace Bug Finder and PolySpace Code Prover

MATLAB: Verifying user input

Related Question