home *** CD-ROM | disk | FTP | other *** search
/ AmigActive 3 / AACD03.BIN / AACD / Programming / sofa / archive / SmallEiffel.lha / SmallEiffel / lib_se / class_invariant.e < prev    next >
Text File  |  1999-06-05  |  6KB  |  188 lines
  1. --          This file is part of SmallEiffel The GNU Eiffel Compiler.
  2. --          Copyright (C) 1994-98 LORIA - UHP - CRIN - INRIA - FRANCE
  3. --            Dominique COLNET and Suzanne COLLIN - colnet@loria.fr
  4. --                       http://SmallEiffel.loria.fr
  5. -- SmallEiffel is  free  software;  you can  redistribute it and/or modify it
  6. -- under the terms of the GNU General Public License as published by the Free
  7. -- Software  Foundation;  either  version  2, or (at your option)  any  later
  8. -- version. SmallEiffel is distributed in the hope that it will be useful,but
  9. -- WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
  10. -- or  FITNESS FOR A PARTICULAR PURPOSE.   See the GNU General Public License
  11. -- for  more  details.  You  should  have  received a copy of the GNU General
  12. -- Public  License  along  with  SmallEiffel;  see the file COPYING.  If not,
  13. -- write to the  Free Software Foundation, Inc., 59 Temple Place - Suite 330,
  14. -- Boston, MA 02111-1307, USA.
  15. --
  16. class CLASS_INVARIANT
  17.    --
  18.    -- To store a `class invariant'.
  19.    --
  20.  
  21. inherit ASSERTION_LIST redefine pretty_print end;
  22.  
  23. creation make, make_runnable
  24.  
  25. feature
  26.  
  27.    name: STRING is
  28.       do
  29.          Result := fz_invariant;
  30.       end;
  31.  
  32.    pretty_print is
  33.       local
  34.          i: INTEGER;
  35.       do
  36.          fmt.set_indent_level(0);
  37.          if not fmt.zen_mode then
  38.             fmt.skip(1);
  39.          end;
  40.          fmt.keyword(name);
  41.          if header_comment /= Void then
  42.             header_comment.pretty_print;
  43.          end;
  44.          if list /= Void then
  45.             from
  46.                i := 1;
  47.             until
  48.                i > list.upper
  49.             loop
  50.                fmt.set_indent_level(1);
  51.                fmt.indent;
  52.                if not fmt.zen_mode then
  53.                   fmt.skip(1);
  54.                end;
  55.                fmt.set_semi_colon_flag(true);
  56.                list.item(i).pretty_print;
  57.                i := i + 1;
  58.             end;
  59.          end;
  60.       end;
  61.  
  62.    short(bc: BASE_CLASS) is
  63.       local
  64.          i: INTEGER;
  65.       do
  66.          bc.header_comment_for(Current);
  67.          short_print.hook_or("hook811","invariant%N");
  68.          if header_comment = Void then
  69.             short_print.hook_or("hook812","");
  70.          else
  71.             short_print.hook_or("hook813","");
  72.             header_comment.short("hook814","   -- ","hook815","%N");
  73.             short_print.hook_or("hook816","");
  74.          end;
  75.          if list = Void then
  76.             short_print.hook_or("hook817","");
  77.          else
  78.             short_print.hook_or("hook818","");
  79.             from
  80.                i := 1;
  81.             until
  82.                i = list.upper
  83.             loop
  84.                list.item(i).short("hook819","   ", -- before each assertion
  85.                                   "hook820","", -- no tag
  86.                                   "hook821","", -- before tag
  87.                                   "hook822",": ", -- after tag
  88.                                   "hook823","", -- no expression
  89.                                   "hook824","", -- before expression
  90.                                   "hook825",";", -- after expression except last
  91.                                   "hook826","%N", -- no comment
  92.                                   "hook827","", -- before comment
  93.                                   "hook828"," -- ", -- comment begin line
  94.                                   "hook829","%N", -- comment end of line
  95.                                   "hook830","", -- after comment
  96.                                   "hook831",""); -- end of each assertion
  97.  
  98.                i := i + 1;
  99.             end;
  100.             list.item(i).short("hook819","   ", -- before each assertion
  101.                                "hook820","", -- no tag
  102.                                "hook821","", -- before tag
  103.                                "hook822",": ", -- after tag
  104.                                "hook823","", -- no expression
  105.                                "hook824","", -- before expression
  106.                                "hook832",";", -- after last expression
  107.                                "hook826","%N", -- no comment
  108.                                "hook827","", -- before comment
  109.                                "hook828"," -- ", -- comment begin line
  110.                                "hook829","%N", -- comment end of line
  111.                                "hook830","", -- after comment
  112.                                "hook831","");
  113.             short_print.hook_or("hook833","");
  114.          end;
  115.          short_print.hook_or("hook834","");
  116.       ensure
  117.          fmt.indent_level = old fmt.indent_level;
  118.       end;
  119.  
  120. feature {NONE}
  121.  
  122.    check_assertion_mode: STRING is
  123.       do
  124.          Result := "inv";
  125.       end;
  126.  
  127. feature {RUN_CLASS}
  128.  
  129.    c_define is
  130.          -- Define C function to check invariant.
  131.       require
  132.          run_control.invariant_check;
  133.          current_type /= Void;
  134.          run_class.at_run_time;
  135.          small_eiffel.is_ready;
  136.          cpp.on_c
  137.       local
  138.          id: INTEGER;
  139.       do
  140.          id := current_type.id;
  141.          -- The invariant frame descriptor :
  142.          c_code.copy("se_frame_descriptor se_ifd");
  143.          id.append_in(c_code);
  144.          cpp.put_extern7(c_code);
  145.          c_code.copy("{%"Class invariant of ");
  146.          c_code.append(current_type.run_time_mark);
  147.          c_code.append("%",1,0,%"");
  148.          c_frame_descriptor_format.clear;
  149.          current_type.c_frame_descriptor;
  150.          c_code.append(c_frame_descriptor_format);
  151.          c_code.append("%",1};%N");
  152.          cpp.put_string(c_code);
  153.          -- The function :
  154.          c_code.clear;
  155.          c_code.extend('T');
  156.          id.append_in(c_code);
  157.          c_code.extend('*');
  158.          c_code.append(fz_se_i);
  159.          id.append_in(c_code);
  160.          c_code.append("(se_dump_stack*caller,T");
  161.          id.append_in(c_code);
  162.          c_code.append("*C)");
  163.          cpp.put_c_heading(c_code);
  164.          cpp.swap_on_c;
  165.          c_code.copy("se_dump_stack ds;%Nds.fd=&se_ifd");
  166.          id.append_in(c_code);
  167.          c_code.append(";%Nds.current=((void**)&C);%N");
  168.          cpp.put_string(c_code);
  169.          cpp.put_position_in_ds(start_position);
  170.          cpp.put_string(
  171.             "ds.caller=caller;%N%
  172.             %se_dst=&ds;%N");
  173.          compile_to_c;
  174.          cpp.put_string("se_dst=caller;%Nreturn C;%N}%N");
  175.       ensure
  176.          cpp.on_c
  177.       end;
  178.  
  179. feature {NONE}
  180.  
  181.    c_code: STRING is
  182.       once
  183.          !!Result.make(128);
  184.       end;
  185.  
  186. end -- CLASS_INVARIANT
  187.  
  188.