Commit 62b35c3f authored by Colin Eles's avatar Colin Eles
Browse files

fixed checking of proven tables 

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

@PVS_checker/check_status.m

+3 −3
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)
@@ -24,7 +24,7 @@ for i=1:2:size(parsed,2)-1 
end



status = pass;

delete(script_name);

delete(script_name)



end

@PVS_checker/generate_pvs_status_script.m

+1 −1
Original line number Diff line number Diff line
@@ -11,7 +11,7 @@ 
function [script_name] = generate_pvs_status_script(object,filename)

script_name = [filename '_status' '.el'];

fileid = fopen(script_name,'w');

code = ['(status-proof-pvs-file "' filename '")'];

code = ['(typecheck-prove "' filename '") (status-proof-pvs-file "' filename '")'];



fprintf(fileid,code);

fclose(fileid);