From 145b8e8c03ff94c415303b56a9add6f51b100e93 Mon Sep 17 00:00:00 2001 From: Colin Eles Date: Tue, 26 Apr 2011 19:22:44 +0000 Subject: [PATCH] should work with PVS5 now git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@7277 57e6efec-57d4-0310-aeb1-a6c144bb1a8b --- @PVS_checker/parse_pvs_result.m | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/@PVS_checker/parse_pvs_result.m b/@PVS_checker/parse_pvs_result.m index 1794ead..3f552b4 100644 --- a/@PVS_checker/parse_pvs_result.m +++ b/@PVS_checker/parse_pvs_result.m @@ -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'); -- GitLab