Commit 00bf82f8 authored by Mark Lawford's avatar Mark Lawford
Browse files

Changes to make PVS run under Windows Services for Linux (WSL)

parent df68c56b

@GUI/GUI.m

+1 −1
Original line number Diff line number Diff line
@@ -64,7 +64,7 @@ classdef GUI < handle 
        multi_opt_out = [];

        prover_opt_pvs = [];

        prover_opt_cvc = [];

        version = '0.7.4';

        version = '0.7.5';

        undo_man = [];

        undo_opt = [];

        redo_opt = [];

@PVS_checker/check_status.m

+1 −1
Original line number Diff line number Diff line
@@ -11,7 +11,7 @@ 
% Organization: McMaster Centre for Software Certification

function status = check_status(object)

script_name = object.generate_pvs_status_script(object.data.function_name );

[status, result] = system(['pvs -batch -v 3 -l ' script_name]);

[status, result] = system(['bash -c "pvs -batch -v 3 -l ' script_name '"']);

parsed = object.parse_status(result);

pass = 1;

if (size(parsed,2) == 0)

@PVS_checker/get_pvs_version.m

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

% Organization: McMaster Centre for Software Certification

function version = get_pvs_version

[status, result] = system('pvs --version');

[status, result] = system('bash -c "pvs --version"');

version = result;

end
 
 No newline at end of file

@PVS_checker/pvs_check.m

+2 −2
Original line number Diff line number Diff line
@@ -54,7 +54,7 @@ if (exists == 1 && (isempty(button) || strcmp(button,'Cancel'))) 
    output = 'canceled';

    return;

elseif (exists == 1 && (strcmp(button,'Open PVS')));

    [status, result] = system(['pvs ' function_name '.pvs']);

    [status, result] = system(['bash -c "pvs ' function_name '.pvs"']);

    output = 'canceled';

elseif (exists == 0 || strcmp(button,'Attempt to prove'))

    box = waitbar(0,'Generating Proof Script');
@@ -70,7 +70,7 @@ elseif (exists == 0 || strcmp(button,'Attempt to prove')) 
    % call pvs in batch mode with script

    % ADD check that pvs actually exists in system

    %

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

    [status, result] = safe_execute_external_command(['bash -c "pvs -batch -v 3 -l ' function_name '.el"']);

    %toc

    %objectect.msgbox_scroll(result);

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

@ValidationReport/pb_open_call.m

+1 −1
Original line number Diff line number Diff line
@@ -10,7 +10,7 @@ 
% Author: Colin Eles elesc@mcmaster.ca

% Organization: McMaster Centre for Software Certification

function [] = pb_open_call(object,src,event)

[status, result] = system(['pvs ' get(object.gui.function_name_control,'String') '.pvs']);

[status, result] = system(['bash -c "pvs ' get(object.gui.function_name_control,'String') '.pvs"']);



end