Newer
Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
function [] = cvc_ext_call( object,src,event )
%CVC_EXT_CALL Summary of this function goes here
% Detailed explanation goes here
object.save_call([],[]);
object.save_data;
if (object.validation_report_handle ~= 0)
delete(object.validation_report_handle);
object.validation_report_handle = 0;
end
error = object.check_call([],2);
if (~error)
inputs = ca.mcmaster.cas.matlab2smt.VariableParser(object.Data.function_inputs);
vars = inputs.getVarList()
HGrid = ca.mcmaster.cas.tablularexpression.HierarchicalGrid
TableBlock.convert_hierarchical_grid_to_java(object.Data.Grid2.cells, HGrid.getSubHiearchy());
res = ca.mcmaster.cas.smtlibchecker.CheckerRunner.RunZ3(HGrid, inputs);
if object.Data.multi_mode == 0 && size(object.Data.Grid1.cells,2) > 1
HGrid = ca.mcmaster.cas.tablularexpression.HierarchicalGrid
TableBlock.convert_hierarchical_grid_to_java(object.Data.Grid1.cells, HGrid.getSubHiearchy());
res2 = ca.mcmaster.cas.smtlibchecker.CheckerRunner.RunZ3(HGrid, inputs);
res.addAll(res2);
end
if (res.isEmpty())
check = 1;
msgbox('table is valid');
else
check = 0;
result = [];
for i=0:res.size()-1
r = res.get(i)
var_out = {}
var_it = vars.iterator()
j = 0;
while var_it.hasNext()
var = var_it.next()
var = var.name()
var_out(j*2+1:j*2+2) = {char(var), r.SampleValues.get(var)};
j = j+1;
end
var_out
result = [result struct('id', '1234a', 'TCC', 'TCC', 'seq', r.Query, 'ce', {var_out})]
end
Valid_Report = ValidationReport(object);
Valid_Report.set_results(result);
Valid_Report.set_mode(1);
Valid_Report.init();
end
object.pvs_checked = check;
object.update_Statusbar;
if (object.mode == 1)
TableBlock.set_block_display(object.block_handle,object.pvs_checked);
end
end
end