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

tagged v0.4 release with floating point features 

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/tags/TableTool/v0.4@7210 57e6efec-57d4-0310-aeb1-a6c144bb1a8b
parent 0c1c3173

@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

%tic

    % run the cvc command

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

toc

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

%toc

% check return status for errors

if (status ~= 0)

@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.3.1';

        version = '0.4';

        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(['pvs -batch -v 3 -l ' script_name]);

parsed = object.parse_status(result);

pass = 1;

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

@PVS_checker/pvs_check.m

+4 −4
Original line number Diff line number Diff line
@@ -52,7 +52,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(['pvs ' function_name '.pvs']);

    output = 'canceled';

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

    box = waitbar(0,'Generating Proof Script');
@@ -67,9 +67,9 @@ elseif (exists == 0 || strcmp(button,'Attempt to prove')) 
    %---------

    % 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

    %

    [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);

@PVS_checker/pvs_check_for_imports.m

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


for k=1:size(hashtable,2)

    

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

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

            if ~isempty(functions{1})

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

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