Commit e616118d authored by Matthew Dawson's avatar Matthew Dawson
Browse files

Fix up CVC3 generator to work against the latest jTET.

This moves CVC3's generator to use the new Table based system, making use of
the generic table conversion function.
parent 47cc67ca
Loading
Loading
Loading
Loading

@CVC_checker/generate_cvc_grid.m

deleted100644 → 0
+0 −33
Original line number Diff line number Diff line
%% genereate_cvc_grid
% generate the queries for cvc for the inputted grid.
%
% inputs:
%   grid:Grid - grid to generate conditions for.
%   level:int - count of the queries generated.
%   var_def:VariableParser - Parsed input of the variables, available in
%   the MATLAB2SMT java package.
%
% outputs;
%   code:string - string representing code to generate including comments
%   query:cell array - contains string representing both the disjoint and
%   complete without the comments, used for validation report.
% Author: Colin Eles elesc@mcmaster.ca
% Organization: McMaster Centre for Software Certification

function [ code , query] = generate_cvc_grid( object, grid , level, var_def)

% New Junk
% First build grid in java
HGrid = ca.mcscert.jtet.tablularexpression.HierarchicalGrid
TableBlock.convert_hierarchical_grid_to_java(grid.cells, HGrid.getSubHiearchy());
% generate the formulas for the main grid

gridGenerator = ca.mcscert.jtet.cvc3generator.HierarchicalGridCVC3Generator(var_def, level);
code = char(ca.mcscert.jtet.tablularexpression.HierarchcialGridCheckerWalkerGenerator.GenerateCheckerFromGrid(HGrid, gridGenerator));
query = gridGenerator.getFinalQueries();




end
+20 −0
Original line number Diff line number Diff line
%% genereate_cvc_tccs
% generate the type check conditions for cvc for the inputted table.
%
% inputs:
%   table:ca.mcscert.tabularexpression.Table - The table to generate for.
%
% outputs;
%   code:string - string representing code to generate including comments
%   query:cell array - contains string representing both the disjoint and
%   complete without the comments, used for validation report.
% Author: Colin Eles elesc@mcmaster.ca
% Organization: McMaster Centre for Software Certification

function [code, query] = generate_cvc_tccs(~, table)
    % generate the formulas for the grid
    gridGenerator = ca.mcscert.jtet.cvc3generator.HierarchicalGridCVC3Generator();
    code = char(table.walk(gridGenerator));
    query = gridGenerator.getFinalQueries();
end
+4 −17
Original line number Diff line number Diff line
@@ -16,29 +16,16 @@ function [ filename, queries ] = generate_file( object )
function_names = EMLGenerator.parse_inputs(object.data.function_name);
function_name = char(function_names{1}(1));

table = TableBlock.convert_table_to_java_table(object.data);

code = [];
% output the input variables
inputs = TET.getInstance.getVariableParser.parseVariables(object.data.function_inputs);
inputs = table.getVariables.getInputVariablesList();
code = char(object.generator.GenerateVariablesDeclaration(inputs));


% call the recursive function to generate the queries
new_code = '';
queries = [];
%generate grid 2
if size(object.data.Grid2.cells,2) > 1  
    [new_code,queries] = object.generate_cvc_grid(object.data.Grid2,1, inputs);
end
code = [code new_code];

if object.data.multi_mode == 0 && size(object.data.Grid1.cells,2) > 1
    [new_code,new_queries] = object.generate_cvc_grid(object.data.Grid1,queries.size(), inputs);
    queries.addAll(new_queries);
%generate type check conditions
[new_code,queries] = object.generate_cvc_tccs(table);
code = [code new_code];

end   


fileid = fopen([function_name '.cvc'],'w');
fprintf(fileid,'%s',char(code));