Commit ae3c731a authored by Colin Eles's avatar Colin Eles
Browse files

found bug in parsing pvs result, updated proof script 

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@7019 57e6efec-57d4-0310-aeb1-a6c144bb1a8b
parent 5343fad5

@CVC_checker/cvc_check.m

+3 −3
Original line number Diff line number Diff line
@@ -19,10 +19,10 @@ function [ check, seqs ] = cvc_check( object ) 
[filename, queries] = object.generate_file;



    waitbar(.10,box,'Running Proof');



tic

    % run the cvc command

[status, result] = system(['cvc3 ' filename ' +model'])



[status, result] = system(['cvc3 ' filename ' +model']);

toc

% check return status for errors

if (status ~= 0)

@PVS_checker/generate_pvs_file.m

+1 −17
Original line number Diff line number Diff line
@@ -130,23 +130,7 @@ end 
    end

    code = [code sprintf('%s(%s):%s = \n',function_name,inputs_new,function_name_type)];

    

%else

    %inputs_new = [];

    %for i=1:size(object.input_type,1)



        

    %    inputs_new = [inputs_new char(object.input_type(i,1)) ':' PVS_checker.matlab_type_to_pvs_type(char(object.input_type(i,2)))];

        

    %    if(i~=(size(object.input_type,1)))

    %            inputs_new = [inputs_new ','];

    %    end

    %end

    %code = [code sprintf('%s(%s):%s = \n',function_name,inputs_new,function_name_type)];

    

    %code = [code sprintf('%s(%s):real = \n',object.data.function_name,inputs_new)];

    

    

%end

code = [code object.generate_pvs(object.data.Grid1,object.data.Grid2,0)];

code = [code sprintf('\nEND %s',function_name)];

fprintf(fileid,code);

@PVS_checker/generate_pvs_script.m

+6 −3
Original line number Diff line number Diff line
@@ -9,10 +9,13 @@ 
%    none

% Author: Colin Eles elesc@mcmaster.ca

% Organization: McMaster Centre for Software Certification

function [] = generate_pvs_script(object,filename)

function [] = generate_pvs_script(object,filename,sim_types)

fileid = fopen([filename '.el'],'w');

code = ['(prove-tccs-pvs-file "' filename '" "(try (try (tcc) (try (assert) (skip) (fail) ) (fail))(skip) (random-test :count ' sprintf('%ld',object.data.settings.count) ' :size ' sprintf('%d',object.data.settings.range) '))"  )' sprintf('\n')];



%if sim_types == 0 

code = ['(prove-tccs-pvs-file "' filename '" "(try (try (subtype-tcc) (try (assert) (skip) (fail) ) (fail))(skip) (random-test :count ' sprintf('%ld',object.data.settings.count) ' :size ' sprintf('%d',object.data.settings.range) '))"  )' sprintf('\n')];

%else

%    code = ['(prove-tccs-pvs-file "' filename '" "(try (try (subtype-tcc) (try (assert) (skip) (fail) ) (fail))(skip) (random-test :count ' sprintf('%ld',object.data.settings.count) ' :size ' sprintf('%d',object.data.settings.range) '))"  )' sprintf('\n')];

%end

fprintf(fileid,code);

fclose(fileid);

end

@PVS_checker/parse_pvs_result.m

+2 −2
Original line number Diff line number Diff line
@@ -28,7 +28,7 @@ else 
                % find the TCC that was unprovable

                search_str = sprintf('(?<=Proving formula %s[\\n]*)%s.*?(?=[ \\n]*Rerunning step)',char(found(i)),char(found(i)));

            elseif strncmp(object.pvs_version,'PVS Version 4.2',15)

                search_str =  sprintf('(?<=Installing rewrite rule singleton_rew\\s\\s)%s.*?(?=[ \\n]*Rerunning step)',char(found(i)));

                search_str =  sprintf('(?<=Installing rewrite rule \\w+\\s\\s)%s.*?(?=[ \\n]*Rerunning step)',char(found(i)));

            end

            found2 = regexp(result,char(search_str),'match','once');

@PVS_checker/pvs_check.m

+4 −2
Original line number Diff line number Diff line
@@ -52,12 +52,14 @@ elseif (exists == 0 || strcmp(button,'Attempt to prove')) 
    

    

    % generate the proof script

    object.generate_pvs_script(function_name);

    object.generate_pvs_script(function_name,1);

    waitbar(.10,box,'Running Proof');

    %---------

    % call pvs in batch mode with script

    % ADD check that pvs actually exists in system

    tic

    [status, result] = system(['pvs -batch -v 3 -l ' function_name '.el'])

    toc

    %objectect.msgbox_scroll(result);

    waitbar(.70,box,'Parsing Results');

    [parsed error] = object.parse_pvs_result(result);
@@ -76,7 +78,7 @@ elseif (exists == 0 || strcmp(button,'Attempt to prove')) 
    end

    waitbar(.100,box,'Deleting Proof Script');

    

    delete([function_name '.el']);

    %delete([function_name '.el']);

    

    delete(box);

end