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

added some TA stuff, as well as a minor fix in TT where function name is not proper pvs syntax. 

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

@GUI/init.m

+2 −0
Original line number Diff line number Diff line
@@ -161,6 +161,8 @@ uimenu(checkmenu,'Label','Typecheck','Accelerator','t','Callback',@(src,event)ty 
prover_menu = uimenu(checkmenu,'Label','Default Prover');

object.prover_opt_cvc = uimenu(prover_menu,'Label','CVC3','Callback',@(src,event)prover_select_call(object,src,event));

object.prover_opt_pvs = uimenu(prover_menu,'Label','PVS','Callback',@(src,event)prover_select_call(object,src,event));

uimenu(checkmenu,'Label', 'Syntax Check','Callback',@(src,event)check_call(object,src,event));





uimenu(checkmenu,'Label','CVC Typecheck','Separator','on','Callback',@(src,event)cvc_ext_call(object,src,event));

uimenu(checkmenu,'Label','CVC Generate File');

@PVS_checker/generate_pvs_file.m

+12 −1
Original line number Diff line number Diff line
@@ -10,10 +10,11 @@ 
%   none

% Author: Colin Eles elesc@mcmaster.ca

% Organization: McMaster Centre for Software Certification

function [] = generate_pvs_file(object,filename)

function error = generate_pvs_file(object,filename)

% type_mode = 0 -> use pvs types

% type_mode = 1 -> use simulink typing information



error = 0;



if object.type_mode

    if size(object.output_type,2) == 2
@@ -22,6 +23,16 @@ if object.type_mode 
end

function_names = EMLGenerator.parse_inputs(object.data.function_name);

function_name = char(function_names{1}(1));



% make sure that function name is valid

valid = regexp(function_name,'[a-zA-Z][_a-zA-Z0-9]*','match');

if ~strcmp(function_name,valid)

    msgbox(['function name is not valid PVS syntax' char(10) 'proper syntax for PVS Id is [a-zA-Z][_a-zA-Z0-9]*']);

    error = 1;

    return;

end





% setup 1 output vs multiple outputs

if object.data.multi_mode == 0

@PVS_checker/pvs_check.m

+4 −1
Original line number Diff line number Diff line
@@ -16,7 +16,10 @@ output = []; 


function_names = EMLGenerator.parse_inputs(object.data.function_name);

function_name = char(function_names{1}(1));

object.generate_pvs_file(function_name);

error = object.generate_pvs_file(function_name);

if error == 1

    return;

end



object.pvs_version = PVS_checker.get_pvs_version;