home
***
CD-ROM
|
disk
|
FTP
|
other
***
search
/
AmigActive 3
/
AACD03.BIN
/
AACD
/
Programming
/
sofa
/
archive
/
SmallEiffel.lha
/
SmallEiffel
/
lib_se
/
assertion_list.e
< prev
next >
Wrap
Text File
|
1999-06-05
|
9KB
|
361 lines
-- This file is part of SmallEiffel The GNU Eiffel Compiler.
-- Copyright (C) 1994-98 LORIA - UHP - CRIN - INRIA - FRANCE
-- Dominique COLNET and Suzanne COLLIN - colnet@loria.fr
-- http://SmallEiffel.loria.fr
-- SmallEiffel is free software; you can redistribute it and/or modify it
-- under the terms of the GNU General Public License as published by the Free
-- Software Foundation; either version 2, or (at your option) any later
-- version. SmallEiffel is distributed in the hope that it will be useful,but
-- WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
-- or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License
-- for more details. You should have received a copy of the GNU General
-- Public License along with SmallEiffel; see the file COPYING. If not,
-- write to the Free Software Foundation, Inc., 59 Temple Place - Suite 330,
-- Boston, MA 02111-1307, USA.
--
deferred class ASSERTION_LIST
--
-- To store a list of assertions (see ASSERTION).
--
-- See also : CLASS_INVARIANT, E_REQUIRE, E_ENSURE,
-- LOOP_INVARIANT and CHECK_INVARIANT.
--
inherit GLOBALS;
feature
name: STRING is
-- "require", "ensure" or "invariant".
deferred
end;
start_position: POSITION;
-- If any, the position of the first letter of `name'.
header_comment: COMMENT;
feature {ASSERTION_LIST,E_CHECK,E_FEATURE}
list: ARRAY[ASSERTION];
feature
current_type: TYPE;
-- Not Void when checked in.
feature {NONE}
run_feature: RUN_FEATURE;
-- Corresponding one (if any) when runnable.
-- Note: class invariant are not inside a RUN_FEATURE.
feature
set_current_type(ct: like current_type) is
do
current_type := ct;
end;
afd_check is
local
i: INTEGER;
do
if list /= Void then
from
i := list.upper;
until
i = 0
loop
list.item(i).afd_check;
i := i - 1;
end;
end;
end;
feature {NONE}
is_always_true: BOOLEAN is
local
i: INTEGER;
assertion: ASSERTION;
do
from
i := list.upper;
Result := true;
until
not Result or else i = 0
loop
assertion := list.item(i);
Result := assertion.is_always_true;
i := i - 1;
end;
end;
feature
compile_to_c is
require
run_control.require_check
local
i: INTEGER;
need_se_tmp: BOOLEAN;
assertion: ASSERTION;
do
if is_always_true then
cpp.increment_static_expression_count(list.count);
else
if run_feature = Void then
cpp.put_string("if(ds.fd->assertion_flag){%N%
%ds.fd->assertion_flag=0;%N");
else
cpp.put_string("if(");
run_feature.c_assertion_flag;
cpp.put_string("){%N");
run_feature.c_assertion_flag;
cpp.put_string("=0;%N");
end;
from
i := 1;
until
i > list.upper
loop
assertion := list.item(i);
if assertion.is_always_true then
else
assertion.collect_c_tmp;
need_se_tmp := cpp.se_tmp_open_declaration;
cpp.set_check_assertion_mode(check_assertion_mode);
assertion.compile_to_c;
if need_se_tmp then
cpp.se_tmp_close_declaration;
end;
end;
i := i + 1;
end;
if run_feature = Void then
cpp.put_string("ds.fd->assertion_flag=1;%N}%N");
else
run_feature.c_assertion_flag;
cpp.put_string("=1;%N}%N");
end;
end;
end;
frozen compile_to_jvm(last_chance: BOOLEAN) is
-- If `last_chance' is true, an error message is printed at
-- run-time.
-- The final result is always left a top of stack.
local
point_true, i: INTEGER;
ca: like code_attribute;
do
ca := code_attribute;
ca.check_opening;
from
failure.clear;
i := 1;
until
i > list.upper
loop
list.item(i).compile_to_jvm(last_chance);
failure.add_last(ca.opcode_ifeq);
i := i + 1;
end;
ca.opcode_iconst_1;
point_true := ca.opcode_goto;
ca.resolve_with(failure);
ca.opcode_iconst_0;
ca.resolve_u2_branch(point_true);
ca.check_closing;
end;
is_pre_computable: BOOLEAN is
local
i: INTEGER;
do
if list = Void then
Result := true;
else
from
i := list.upper;
Result := true;
until
not Result or else i = 0
loop
Result := list.item(i).is_pre_computable;
i := i - 1;
end;
end;
end;
use_current: BOOLEAN is
local
i: INTEGER;
do
if list /= Void then
from
i := list.upper;
until
Result or else i = 0
loop
Result := list.item(i).use_current;
i := i - 1;
end;
end;
end;
feature {NONE}
make(sp: like start_position; hc: like header_comment; l: like list) is
require
l /= Void implies not l.empty;
hc /= Void or else l /= Void;
do
start_position := sp;
header_comment := hc;
list := l;
ensure
start_position = sp;
header_comment = hc;
list = l;
end;
feature {NONE}
make_runnable(sp: like start_position; l: like list;
ct: like current_type; rf: like run_feature) is
require
not l.empty;
ct /= Void
do
start_position := sp;
list := l;
current_type := ct;
run_feature := rf;
ensure
start_position = sp;
list = l;
current_type = ct;
run_feature = rf
end;
feature
empty: BOOLEAN is
do
Result := list = Void;
end;
run_class: RUN_CLASS is
do
Result := current_type.run_class;
end;
frozen to_runnable(ct: TYPE): like Current is
require
ct.run_type = ct;
do
if current_type = Void then
current_type := ct;
run_feature := small_eiffel.top_rf;
if list /= Void then
list := assertion_collector.runnable(list,ct,run_feature,'_');
end;
if nb_errors = 0 then
Result := Current;
end;
else
Result := twin;
Result.set_current_type(Void);
Result := Result.to_runnable(ct);
end;
ensure
nb_errors = 0 implies Result /= Void
end;
pretty_print is
local
i: INTEGER;
do
fmt.indent;
fmt.keyword(name);
fmt.level_incr;
if header_comment /= Void then
header_comment.pretty_print;
else
fmt.indent;
end;
if list /= Void then
from
i := 1;
until
i > list.upper
loop
if fmt.zen_mode and i = list.upper then
fmt.set_semi_colon_flag(false);
else
fmt.set_semi_colon_flag(true);
end;
fmt.indent;
list.item(i).pretty_print;
i := i + 1;
end;
end;
fmt.level_decr;
fmt.indent;
ensure
fmt.indent_level = old fmt.indent_level;
end;
set_header_comment(hc: like header_comment) is
do
header_comment := hc;
end;
feature {E_FEATURE,RUN_CLASS,ASSERTION_COLLECTOR}
add_into(collector: ARRAY[ASSERTION]) is
local
i: INTEGER;
a: ASSERTION;
do
if list /= Void then
from
i := 1;
until
i > list.upper
loop
a := list.item(i);
if not collector.fast_has(a) then
collector.add_last(a);
end;
i := i + 1;
end;
end;
end;
feature {NONE}
failure: FIXED_ARRAY[INTEGER] is
once
!!Result.with_capacity(12);
end;
check_assertion_mode: STRING is
deferred
end;
feature {RUN_FEATURE_6, RUN_REQUIRE}
clear_run_feature is
do
run_feature := Void;
end;
invariant
list /= Void implies (list.lower = 1 and not list.empty);
end -- ASSERTION_LIST