%% 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 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 = ca.mcmaster.cas.matlab2smt.VariableParser(object.data.function_inputs); code = char(inputs.getCVC3Output()) % 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] = CVC_checker.generate_cvc_grid(object.data.Grid2,0); end 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]; code = [code new_code]; end fileid = fopen([function_name '.cvc'],'w'); fprintf(fileid,'%s',char(code)); fclose(fileid); filename = [function_name '.cvc']; end