@Settings/init.m → @TTSettings/init.m

@@ -11,6 +11,6 @@ function [] = init(object)
 object.pvs_includes = [];
 object.counter_trials = 1000;
 object.counter_range = 100;
-
+object.except = 0;
 end
 

@Settings/save.m → @TTSettings/save.m

@@ -25,6 +25,12 @@ else
 end
 object.pvs_includes = get(object.include_text,'String');
 
+if (get(object.except_check,'value') == get(object.except_check,'Max'))
+    object.except = true;
+else
+    object.except = false;
+end
+
 if err
     msgbox(msg);
 end

@Settings/setvalues.m → @TTSettings/setvalues.m

@@ -12,5 +12,9 @@ function [] = setvalues(object,settings)
 object.pvs_includes = settings.inputs;
 object.counter_trials = settings.count;
 object.counter_range = settings.range;
+if ~isfield(settings,'except')
+    settings.except = 0;
+end
+object.except = settings.except;
 end
 

@Settings/show.m → @TTSettings/show.m

@@ -8,7 +8,7 @@
 % Organization: McMaster Centre for Software Certification
 function [] = show(object)
 if (object.open)
-    figure(object.fig)
+    figure(object.fig);
 else
     
     object.fig = figure('units','pixels',...
@@ -57,7 +57,7 @@ uicontrol('style','text',...
     'Position',[0, object.fig_height-object.text_offset-object.title_height, object.fig_width, object.title_height],...
     'BackgroundColor',get(object.fig,'Color'));
 
-panel_height = object.text_offset*6+object.label_height*3;
+panel_height = object.text_offset*7+object.label_height*4;
 panel_width = object.fig_width-object.text_offset*2;
 panel = uipanel('Title','PVS',...
     'visible','on',...
@@ -130,7 +130,29 @@ object.range_text = uicontrol('style','edit',...
     'BackgroundColor',get(object.fig,'Color'),...
     'Position',[object.text_offset+object.label_width, panel_height-object.text_offset*4-object.label_height*3, panel_width - (object.text_offset*2+object.label_width), object.label_height]);
 
+% range label
+uicontrol('style','text',...
+    'string','Exception Output',...
+    'HorizontalAlign','left',...
+    'parent',panel,...
+    'Position',[object.text_offset, panel_height-object.text_offset*6-object.label_height*4, object.label_width, object.label_height],...
+    'BackgroundColor',get(object.fig,'Color'));
+
 
+% range text box
+object.except_check = uicontrol('style','checkbox',...
+    'units','pix',...
+    'Parent',panel,...
+    'HorizontalAlign','center',...
+    'BackgroundColor',get(object.fig,'Color'),...
+    'Position',[object.text_offset+object.label_width, panel_height-object.text_offset*5-object.label_height*4, panel_width - (object.text_offset*2+object.label_width), object.label_height]);
+
+if (object.except)
+    set(object.except_check,'value',get(object.except_check,'Max'));
+else
+    set(object.except_check,'value',get(object.except_check,'Min'));
+
+end
 object.open = 1;
 end
 

@ValidationReport/ValidationReport.m

@@ -35,6 +35,7 @@ classdef ValidationReport < handle
         offset = 10;
         page = 1;
         keyword = '1234a';
+        tc_mode = [];
     end
     
     methods

@ValidationReport/init.m

@@ -14,14 +14,21 @@ else
     
     object.fig_width = object.offset + object.TCC_width + object.offset + object.seq_width + object.offset + object.ce_width + object.offset;
     object.fig_height = object.offset + object.header_height + object.offset + object.seq_height + object.offset;
+    
+    
     object.fig = figure('units','pixels',...
         'position',[0, 0, object.fig_width, object.fig_height ],...
         'menubar','none',...
-        'name','PVS Report',...
         'numbertitle','off',...
         'resize','off',...
         'CloseRequestFcn',@(src,event)close_req_call(object,src,event));
     
+    if object.tc_mode == 0
+        set(object.fig,'name','PVS Report');
+    else
+        set(object.fig,'name','CVC3 Report');
+    end
+    
     stop = 0;
     i = 1;
     count = 0;
@@ -34,7 +41,6 @@ else
         'units','pix',...
         'min',0,'max',1,...  % This is the key to multiline edits.
         'Max',2.0,...
-        'Clipping','on',...
         'fontweight','bold',...
         'BackgroundColor',[1 1 1],...
         'horizontalalign','center',...
@@ -45,7 +51,6 @@ else
         'units','pix',...
         'min',0,'max',1,...  % This is the key to multiline edits.
         'Max',2.0,...
-        'Clipping','on',...
         'fontweight','bold',...
         'BackgroundColor',[1 1 1],...
         'horizontalalign','left',...
@@ -57,7 +62,6 @@ else
         'units','pix',...
         'min',0,'max',1,...  % This is the key to multiline edits.
         'Max',2.0,...
-        'Clipping','on',...
         'fontweight','bold',...
         'BackgroundColor',[1 1 1],...
         'horizontalalign','left',...
@@ -106,6 +110,7 @@ else
         'FontSize',15,...
         'BackgroundColor',get(object.fig,'Color'));
     
+    if object.tc_mode == 0
     object.pb_open = uicontrol('style','push',...
         'units','pix',...
         'string','Open PVS',...
@@ -113,6 +118,7 @@ else
         'Parent',object.fig,...
         'enable','on',...
         'callback',@(src,event)pb_open_call(object,src,event));
+    end
     
     object.position;
     object.populate;

@ValidationReport/position.m

@@ -15,7 +15,7 @@ set(object.label_tcc,'position',[object.offset, (object.fig_height - object.offs
 set(object.label_seq,'position',[object.offset + object.TCC_width + object.offset, (object.fig_height - object.offset - object.header_height) ,object.TCC_width,object.label_height]);
 set(object.label_ce,'position',[object.offset + object.TCC_width + object.offset + object.seq_width + object.offset, (object.fig_height - object.offset - object.header_height) ,object.TCC_width,object.label_height]);
 
-set(object.label_title,'position',[object.offset, (object.fig_height - object.offset - object.label_height*2) ,object.TCC_width,object.label_height*2])
+set(object.label_title,'position',[object.offset, (object.fig_height - object.offset - object.label_height*2) ,object.TCC_width,object.label_height*2]);
 set(object.label_page,'position',[object.fig_width-object.pb_nav_width*2-object.offset*2, object.fig_height-object.offset-object.header_height+object.label_height+object.pb_nav_height+object.offset/2,object.pb_nav_width*2+object.offset,object.pb_nav_height]);
 set(object.pb_next,'position',[object.fig_width - object.pb_nav_width - object.offset, object.fig_height - object.offset - object.header_height + object.label_height + object.offset/2, object.pb_nav_width, object.pb_nav_height]);
 set(object.pb_prev,'position',[object.fig_width - object.pb_nav_width - object.offset - object.offset - object.pb_nav_width, object.fig_height - object.offset - object.header_height + object.label_height+object.offset/2, object.pb_nav_width, object.pb_nav_height]);

@ValidationReport/set_mode.m

+function  set_mode( object, in_mode )
+%SET_MODE Summary of this function goes here
+%   Detailed explanation goes here
+
+% 1 = CVC
+% 0 = PVS
+object.tc_mode = in_mode;
+
+end
+

PVS_theories/double.pvs

+double: THEORY
+
+BEGIN
+IMPORTING float@enumerated_type_defs
+IMPORTING overload[2,53,192,1023,-1022,to_nearest]
+
+double: TYPE = {fp:fp_num|finite?(fp) OR infinite?(fp)}
+double_finite: TYPE = {fp:fp_num|finite?(fp)}
+
+END double