Skip to content
Snippets Groups Projects
Commit 145b8e8c authored by Colin Eles's avatar Colin Eles
Browse files

should work with PVS5 now

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@7277 57e6efec-57d4-0310-aeb1-a6c144bb1a8b
parent 782ec023
No related branches found
No related tags found
No related merge requests found
......@@ -5,8 +5,8 @@
% object:PVS_checker - PVS_checker object
% result:string - string containing text that comes back from pvs
% outputs:
% output:structure - results paresed into structure for easier
% manipulatings
% output:structure - results parsed into structure for easier
% manipulating
% error:boolean - 0 if no error, 1 if error found during parsing.
% Author: Colin Eles elesc@mcmaster.ca
% Organization: McMaster Centre for Software Certification
......@@ -27,8 +27,10 @@ else
if strncmp(object.pvs_version,'PVS Version 4.0',15)
% 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) || strncmp(object.pvs_version,'PVS Version 5.0',15)
elseif strncmp(object.pvs_version,'PVS Version 4.2',15)
search_str = sprintf('(?<=Installing rewrite rule \\w+\\s\\s)%s.*?(?=[ \\n]*Rerunning step)',char(found(i)));
elseif strncmp(object.pvs_version,'PVS Version 5.0',15)
search_str = sprintf('(?<=Installing rewrite rule.*\\s\\s)%s.*?(?=[ \\n]*Rerunning step)',char(found(i)));
end
found2 = regexp(result,char(search_str),'match','once');
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment