Newer
Older
%% genereate_file
% generate the cvc file to be inputted into cvc, calls the generate grid
% function. generates all the variable declarations.
%
% inputs:
% object:CVC_checker - current object.
%
% outputs;
% filename:string - the filename of the generated file
% queries:cell arrray - a list of queries generated by the grids.
% Author: Colin Eles elesc@mcmaster.ca
% Organization: McMaster Centre for Software Certification
Colin Eles
committed
function [ filename, queries ] = generate_file( object )
function_names = EMLGenerator.parse_inputs(object.data.function_name);
function_name = char(function_names{1}(1));
code = [];
% output the input variables
inputs = EMLGenerator.parse_inputs(object.data.function_inputs);
for i = 1:size(inputs,2)
if size(inputs{i},2) > 1
cvc_type = CVC_checker.pvs_to_cvc_subtypes(inputs{i}(2));
else
cvc_type = 'REAL';
end
code = [code char(inputs{i}(1)) ':' char(cvc_type) ';' char(10)];
Colin Eles
committed
end
% call the recursive function to generate the queries
new_code = '';
%generate grid 2
if size(object.data.Grid2.cells,2) > 1
[new_code,queries] = CVC_checker.generate_cvc_grid(object.data.Grid2,0);
end
Colin Eles
committed
code = [code new_code];
if object.data.multi_mode == 0 && size(object.data.Grid1.cells,2) > 1
[new_code,new_queries] = CVC_checker.generate_cvc_grid(object.data.Grid1,size(queries,2));
queries = [queries new_queries];