From 551b2ddea4daddc740181d15b7bd781dfcb54340 Mon Sep 17 00:00:00 2001 From: Colin Eles Date: Thu, 16 Dec 2010 17:42:10 +0000 Subject: [PATCH] tagged v0.3 of table tool git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/tags/TableTool/v0.3@6667 57e6efec-57d4-0310-aeb1-a6c144bb1a8b --- @CVC_checker/CVC_checker.m | 10 ++++++-- @CVC_checker/cvc_check.m | 34 ++++++++++++++-------------- @CVC_checker/find_parents.m | 14 +++++++++++- @CVC_checker/generate_cvc_grid.m | 29 ++++++++++++------------ @CVC_checker/generate_file.m | 21 ++++++++++------- @CVC_checker/pvs_to_cvc_subtypes.m | 12 ++++++++++ @GUI/GUI.m | 2 +- utilities/unsuppressed_output_file.m | 5 ++++ 8 files changed, 83 insertions(+), 44 deletions(-) diff --git a/@CVC_checker/CVC_checker.m b/@CVC_checker/CVC_checker.m index 3b9932c..1ae1b8e 100644 --- a/@CVC_checker/CVC_checker.m +++ b/@CVC_checker/CVC_checker.m @@ -1,6 +1,6 @@ +% Author: Colin Eles elesc@mcmaster.ca +% Organization: McMaster Centre for Software Certification classdef CVC_checker - %CVC_CHECKER Summary of this class goes here - % Detailed explanation goes here properties @@ -21,6 +21,12 @@ classdef CVC_checker methods + %% CVC_checker + % constructor + % inputs: + % data:Data - data to generate from + % outputs: + % object:CVC_checker - generated object. function object = CVC_checker(data) object.data = data; end diff --git a/@CVC_checker/cvc_check.m b/@CVC_checker/cvc_check.m index 181d83c..c13462e 100644 --- a/@CVC_checker/cvc_check.m +++ b/@CVC_checker/cvc_check.m @@ -1,3 +1,16 @@ +%% cvc_check +% checks a table using cvc, parses results and returns them +% +% inputs: +% object:cvc_checker - cvc_checker object +% +% outputs; +% check:boolean - 0 if check fails, 1 if succeds +% seqs:structure - if typecheck succeds then output contains +% parsed output from cvc +% Author: Colin Eles elesc@mcmaster.ca +% Organization: McMaster Centre for Software Certification + function [ check, seqs ] = cvc_check( object ) %CVC_CHECK Summary of this function goes here % Detailed explanation goes here @@ -7,8 +20,10 @@ function [ check, seqs ] = cvc_check( object ) waitbar(.10,box,'Running Proof'); + % run the cvc command [status, result] = system(['cvc3 ' filename ' +model']); +% check return status for errors if (status ~= 0) if (status == 127) @@ -26,19 +41,7 @@ end seqs = []; -% look for incompleteness, happens with non-linear artihmetic, ie. -% % multiplication -% incomplete = regexp(result,'CVC3 was incomplete in this example due to','match'); -% if ~isempty(incomplete) -% incomplete_reason = regexp(result,'(?<=CVC3 was incomplete in this example due to:\n)[^\n]*','match','once') -% msgbox(['CVC could not typecheck this table for the following reasons:' char(10) incomplete_reason]); -% -% check = 0; -% seqs = 'canceled'; -% delete(box); -% return; -% -% end + % look for parse errors fatal_exception = regexp(result,'*** Fatal exception'); @@ -66,10 +69,7 @@ for i = 1:size(queries,2) % formula was found to be invalid % look for a counter example asserts = regexp(char(query_result),'(?<=ASSERT[ ]*\()[^\n]*(?==)|(?<==)[^\n]*(?=\);)','match'); -% for j = 1:size(asserts,2) -% splits = {splits regexp(asserts(j),'=','split')}; -% -% end + if mod(i,2) == 1 name = [filename '_' num2str(i) '_DIS']; diff --git a/@CVC_checker/find_parents.m b/@CVC_checker/find_parents.m index 69061a1..f3c0124 100644 --- a/@CVC_checker/find_parents.m +++ b/@CVC_checker/find_parents.m @@ -1,6 +1,18 @@ +%% find_parents +% function will find all the parents of a cell, used to determine what +% preconditions must be true. +% +% inputs: +% cell:Cell - cell to find the parents of +% +% outputs; +% code:string - string of conjunction of all parent cells. +% Author: Colin Eles elesc@mcmaster.ca +% Organization: McMaster Centre for Software Certification + function [ code ] = find_parents( cell ) % assumption, initial input will be grid we want to find parents for not -% parent cell itself +% cell itself code = ''; if isempty(cell) diff --git a/@CVC_checker/generate_cvc_grid.m b/@CVC_checker/generate_cvc_grid.m index 492fce6..b44d879 100644 --- a/@CVC_checker/generate_cvc_grid.m +++ b/@CVC_checker/generate_cvc_grid.m @@ -1,6 +1,18 @@ +%% 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. +% +% 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( grid , level) -%GENERATE_CVC_GRID Summary of this function goes here -% Detailed explanation goes here % generate the formulas for the main grid @@ -15,19 +27,6 @@ end for i=1:size(grid.cells,2) -% 1 -% 2 -% 3 -% -% 1 2 -% 1 3 -% 2 3 -% -% 1 2 3 4 -% 1 2 -% 1 3 -% 1 4 -% for j = i+1:size(grid.cells,2) % compare i to j diff --git a/@CVC_checker/generate_file.m b/@CVC_checker/generate_file.m index a3cc613..953a581 100644 --- a/@CVC_checker/generate_file.m +++ b/@CVC_checker/generate_file.m @@ -1,6 +1,17 @@ +%% 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 ) -%GENERATE_FILE Summary of this function goes here -% Detailed explanation goes here function_names = EMLGenerator.parse_inputs(object.data.function_name); function_name = char(function_names{1}(1)); @@ -36,12 +47,6 @@ if size(object.data.Grid1.cells,2) > 1 end -% generate grid 2 - - - -char(code); - fileid = fopen([function_name '.cvc'],'w'); fprintf(fileid,'%s',char(code)); fclose(fileid); diff --git a/@CVC_checker/pvs_to_cvc_subtypes.m b/@CVC_checker/pvs_to_cvc_subtypes.m index c0346d0..126265e 100644 --- a/@CVC_checker/pvs_to_cvc_subtypes.m +++ b/@CVC_checker/pvs_to_cvc_subtypes.m @@ -1,3 +1,15 @@ +%% pvs_to_cvc_subtypes +% converts types of the pvs syntax to cvc3 syntax. the syntax for doing +% typing in the two languages is slightly different so we need to write +% this function to translate between them. +% +% inputs: +% pvs_type:string - a string of a pvs type +% outputs; +% cvc_type:string - a string of the cvc type. +% Author: Colin Eles elesc@mcmaster.ca +% Organization: McMaster Centre for Software Certification + function [ cvc_type ] = pvs_to_cvc_subtypes( pvs_type ) %PVS_TO_CVC_SUBTYPES Summary of this function goes here % Detailed explanation goes here diff --git a/@GUI/GUI.m b/@GUI/GUI.m index 4782bb3..7b2e129 100644 --- a/@GUI/GUI.m +++ b/@GUI/GUI.m @@ -64,7 +64,7 @@ classdef GUI < handle multi_opt_out = []; prover_opt_pvs = []; prover_opt_cvc = []; - version = '0.2'; + version = '0.3'; undo_man = []; undo_opt = []; redo_opt = []; diff --git a/utilities/unsuppressed_output_file.m b/utilities/unsuppressed_output_file.m index 3586424..924a259 100644 --- a/utilities/unsuppressed_output_file.m +++ b/utilities/unsuppressed_output_file.m @@ -1,4 +1,9 @@ function [] = unsuppressed_output_file(file) +% [] = unsuppressed_output_file(file) +% +% Outputs to the command window a list of the lines in file which likely do +% not have suppressed output. Lines with keywords which will not produce outputs ie +% (if, else, continue, function, etc.) are ignored. % look through a file for lines which are unsuppressed -- GitLab