-- This file is part of SmartEiffel The GNU Eiffel Compiler.
-- Copyright (C) 1994-2002 LORIA - INRIA - U.H.P. Nancy 1 - FRANCE
-- Dominique COLNET and Suzanne COLLIN - SmartEiffel@loria.fr
-- http://SmartEiffel.loria.fr
-- SmartEiffel 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. SmartEiffel 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 SmartEiffel; see the file COPYING. If not,
-- write to the Free Software Foundation, Inc., 59 Temple Place - Suite 330,
-- Boston, MA 02111-1307, USA.
--
class CLASS_INVARIANT
--
-- To store a `class invariant'.
--
inherit ASSERTION_LIST redefine pretty_print end
creation make, make_runnable
feature
is_require: BOOLEAN is false
name: STRING is
do
Result := fz_invariant
end
pretty_print is
local
indent_level, i: INTEGER
do
indent_level := pretty_printer.indent_level
pretty_printer.set_indent_level(0)
if not pretty_printer.zen_mode then
pretty_printer.skip(1)
end
pretty_printer.keyword(name)
if header_comment /= Void then
header_comment.pretty_print
end
if list /= Void then
from
i := 1
until
i > list.upper
loop
pretty_printer.set_indent_level(1)
pretty_printer.indent
if not pretty_printer.zen_mode then
pretty_printer.skip(1)
end
pretty_printer.set_semi_colon_flag(true)
list.item(i).pretty_print
i := i + 1
end
end
pretty_printer.set_indent_level(indent_level)
end
short(bc: BASE_CLASS) is
local
i: INTEGER
do
bc.header_comment_for(Current)
short_print.hook_or(once "hook811",once "invariant%N")
if header_comment = Void then
short_print.hook_or(once "hook812",once "")
else
short_print.hook_or(once "hook813",once "")
header_comment.short(once "hook814",once " --",once "hook815",once "%N")
short_print.hook_or(once "hook816",once "")
end
if list = Void then
short_print.hook_or(once "hook817",once "")
else
short_print.hook_or(once "hook818",once "")
from
i := 1
until
i = list.upper
loop
list.item(i).short(once "hook819",once " ", -- before each assertion
once "hook820",once "", -- no tag
once "hook821",once "", -- before tag
once "hook822",once ": ", -- after tag
once "hook823",once "", -- no expression
once "hook824",once "", -- before expression
once "hook825",once ";", -- after expression except last
once "hook826",once "%N", -- no comment
once "hook827",once "", -- before comment
once "hook828",once " --", -- comment begin line
once "hook829",once "%N", -- comment end of line
once "hook830",once "", -- after comment
once "hook831",once ""); -- end of each assertion
i := i + 1
end
list.item(i).short(once "hook819",once " ", -- before each assertion
once "hook820",once "", -- no tag
once "hook821",once "", -- before tag
once "hook822",once ": ", -- after tag
once "hook823",once "", -- no expression
once "hook824",once "", -- before expression
once "hook832",once ";", -- after last expression
once "hook826",once "%N", -- no comment
once "hook827",once "", -- before comment
once "hook828",once " --", -- comment begin line
once "hook829",once "%N", -- comment end of line
once "hook830",once "", -- after comment
once "hook831",once "")
short_print.hook_or(once "hook833",once "")
end
short_print.hook_or(once "hook834",once "")
end
feature {NONE}
check_assertion_mode: STRING is
do
Result := once "inv"
end
feature {RUN_CLASS}
c_define is
-- Define C function to check invariant.
require
current_type /= Void
run_class.at_run_time
smart_eiffel.is_ready
cpp.on_c
local
id: INTEGER
do
id := current_type.id
-- The invariant frame descriptor :
c_code.copy(once "se_frame_descriptor se_ifd")
id.append_in(c_code)
cpp.put_extern7(c_code)
c_code.copy(once "{%"invariant once ")
c_code.append(current_type.run_time_mark)
c_code.append(once "%",1,0,%"")
current_type.c_frame_descriptor_in(c_code)
c_code.append(once "%",1};%N")
cpp.put_string(c_code)
-- The function :
c_code.clear
c_code.extend('T')
id.append_in(c_code)
c_code.extend('*')
c_code.append(fz_se_i)
id.append_in(c_code)
c_code.append(once "(se_dump_stack*caller,T")
id.append_in(c_code)
c_code.append(once "*C)")
cpp.put_c_heading(c_code)
cpp.swap_on_c
c_code.copy(once "se_dump_stack ds;%N")
if smart_eiffel.scoop then
cpp.put_string(once "se_subsystem_t* self=se_current_subsystem_thread();%N")
end
c_code.append(once "ds.fd=&se_ifd")
id.append_in(c_code)
c_code.append(once ";%Nds.current=((void**)&C);%N")
cpp.put_string(c_code)
cpp.put_position_in_ds(start_position)
cpp.put_string(once "ds.caller=caller;%N")
if smart_eiffel.scoop then
cpp.put_string(once "(void)(self->vft.get_dst_and_lock(self));%N%
%self->vft.set_dst_and_unlock(self,&ds);/*link*/%N")
else
cpp.put_string(once "se_dst=&ds;/*link*/%N")
end
compile_to_c
if smart_eiffel.scoop then
cpp.put_string(once "(void)(self->vft.get_dst_and_lock(self));%N%
%self->vft.set_dst_and_unlock(self,caller);/*unlink*/%N")
else
cpp.put_string(once "se_dst=caller;/*unlink*/%N")
end
cpp.put_string(once "return C;%N}%N")
ensure
cpp.on_c
end
feature {NONE}
c_code: STRING is
once
!!Result.make(128)
end
end -- CLASS_INVARIANT