Commit cdea6f18 authored by Matthew Dawson's avatar Matthew Dawson
Browse files

Fix PVS checking when dealing with multiline inputs. 

Multiline inputs are now being dealt with properly.


git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@8563 57e6efec-57d4-0310-aeb1-a6c144bb1a8b
parent 1d2ec29f

@PVS_checker/matlab_to_pvs_syntax_translation.m

+6 −0
Original line number Diff line number Diff line
@@ -12,6 +12,12 @@ 
% Author: Colin Eles elesc@mcmaster.ca

% Organization: McMaster Centre for Software Certification

function pvs_string = matlab_to_pvs_syntax_translation(object,matlab_string)

s = [matlab_string(1,:)];

for j = 2:size(matlab_string,1)

   s = [s ' ' matlab_string(j,:)];

end

matlab_string = s;



pvs_string = regexprep(matlab_string,'&&',' AND ');

pvs_string = regexprep(pvs_string,'~(?!=)',' NOT ');

pvs_string = regexprep(pvs_string,'~=',' /= ');

@PVS_checker/pvs_check_for_imports.m

+9 −1
Original line number Diff line number Diff line
@@ -60,7 +60,15 @@ end 


for k=1:size(hashtable,2)



    functions = regexp(char(object.data.function_inputs),hashtable{k}(1),'once');

    string_parts = char(object.data.function_inputs);

    

    s = [string_parts(1,:)];

    for j = 2:size(string_parts,1)

       s = [s ' ' string_parts(j,:)];

    end

    string_parts = s;

    

    functions = regexp(string_parts,hashtable{k}(1),'once')

            if ~isempty(functions{1})

                if (~any(ismember(found,hashtable{k}(1))))

                string = [string 'IMPORTING ' char(hashtable{k}(2)) sprintf('\n')];

@PVS_checker/pvs_check_for_imports_g.m

+6 −0
Original line number Diff line number Diff line
@@ -24,6 +24,12 @@ for i=1:size(grid.cells,2) 
    end

    text = char(grid.cells(i).cond_text);



    s = [text(1,:)];

    for j = 2:size(text,1)

       s = [s ' ' text(j,:)];

    end

    text = s;

    

    vars = regexp(text,'([a-zA-Z][a-zA-Z0-9_]*)','match');