home *** CD-ROM | disk | FTP | other *** search
- -- 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://www.loria.fr/SmallEiffel
- -- 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.
- --
- class CLASS_INVARIANT
- --
- -- To store a `class invariant'.
- --
-
- inherit ASSERTION_LIST redefine pretty_print end;
-
- creation {ANY}
- make, from_runnable
-
- feature {ANY}
-
- name: STRING is
- do
- Result := fz_invariant;
- end;
-
- pretty_print is
- local
- i: INTEGER;
- do
- fmt.set_indent_level(0);
- if not fmt.zen_mode then
- fmt.skip(1);
- end;
- fmt.keyword(name);
- if header_comment /= Void then
- header_comment.pretty_print;
- end;
- if list /= Void then
- from
- i := 1;
- until
- i > list.upper
- loop
- fmt.set_indent_level(1);
- fmt.indent;
- if not fmt.zen_mode then
- fmt.skip(1);
- end;
- fmt.set_semi_colon_flag(true);
- list.item(i).pretty_print;
- i := i + 1;
- end;
- end;
- end;
-
- short(bc: BASE_CLASS) is
- local
- i: INTEGER;
- do
- bc.header_comment_for(Current);
- short_print.hook_or("hook811","invariant%N");
- if header_comment = Void then
- short_print.hook_or("hook812","");
- else
- short_print.hook_or("hook813","");
- header_comment.short("hook814"," -- ","hook815","%N");
- short_print.hook_or("hook816","");
- end;
- if list = Void then
- short_print.hook_or("hook817","");
- else
- short_print.hook_or("hook818","");
- from
- i := 1;
- until
- i = list.upper
- loop
- list.item(i).short("hook819"," ", -- before each assertion
- "hook820","", -- no tag
- "hook821","", -- before tag
- "hook822",": ", -- after tag
- "hook823","", -- no expression
- "hook824","", -- before expression
- "hook825",";", -- after expression except last
- "hook826","%N", -- no comment
- "hook827","", -- before comment
- "hook828"," -- ", -- comment begin line
- "hook829","%N", -- comment end of line
- "hook830","", -- after comment
- "hook831",""); -- end of each assertion
-
- i := i + 1;
- end;
- list.item(i).short("hook819"," ", -- before each assertion
- "hook820","", -- no tag
- "hook821","", -- before tag
- "hook822",": ", -- after tag
- "hook823","", -- no expression
- "hook824","", -- before expression
- "hook832",";", -- after last expression
- "hook826","%N", -- no comment
- "hook827","", -- before comment
- "hook828"," -- ", -- comment begin line
- "hook829","%N", -- comment end of line
- "hook830","", -- after comment
- "hook831","");
- short_print.hook_or("hook833","");
- end;
- short_print.hook_or("hook834","");
- ensure
- fmt.indent_level = old fmt.indent_level;
- end;
-
- feature {NONE}
-
- check_assertion_mode: STRING is
- do
- Result := "inv";
- end;
-
- feature {RUN_CLASS}
-
- c_define is
- -- Define C function to check invariant.
- require
- run_control.invariant_check;
- current_type /= Void;
- run_class.at_run_time;
- small_eiffel.is_ready;
- cpp.on_c
- local
- id: INTEGER;
- do
- id := current_type.id;
- cdm.clear;
- cdm.extend('T');
- id.append_in(cdm);
- cdm.extend('*');
- cdm.extend('i');
- id.append_in(cdm);
- cdm.extend('(');
- cdm.extend('T');
- id.append_in(cdm);
- cdm.extend('*');
- cdm.extend('C');
- cdm.extend(')');
- cpp.put_c_heading(cdm);
- cpp.swap_on_c;
- cdm.copy("*((int*)rs++)=INVid;*((char**)rs++)=p[");
- id.append_in(cdm);
- cdm.extend(']');
- cdm.append(fz_00);
- cpp.put_string(cdm);
- compile_to_c;
- cpp.put_string("rs-=2;return C;}%N");
- ensure
- cpp.on_c
- end;
-
- feature {NONE}
-
- cdm: STRING is
- once
- !!Result.make(128);
- end;
-
- end -- CLASS_INVARIANT
-
-