Permalink
Browse files

The scope of object-test locals can cover the following assertions in…

… the same postcondition or invariant clause because it's as if they were separated by "and then" operators. It was already implemented that way in preconditions.
  • Loading branch information...
1 parent 73cc9ff commit 2610c8fcacdbc89ec921dfddd263beb7f00da28a @ebezault committed Jun 5, 2011
Showing with 18 additions and 0 deletions.
  1. +4 −0 History.txt
  2. +14 −0 library/tools/eiffel/compilation/et_feature_checker.e
View
@@ -127,6 +127,10 @@ Version 3.10 - ?
* Improved the way the type of a manifest array is determined in the
case where the types of all items conform to one of them. In that
case the manifest array will be an array of that type.
+ * The scope of object-test locals can cover the following assertions
+ in the same postcondition or invariant clause because it's as if
+ they were separated by "and then" operators. It was already
+ implemented that way in preconditions.
Gobo Eiffel XML Library:
@@ -435,6 +435,7 @@ feature -- Validity checking
l_feature_impl: ET_FEATURE
l_class_impl: ET_CLASS
l_current_class: ET_CLASS
+ l_old_scope: INTEGER
do
has_fatal_error := False
l_feature_impl := a_current_feature_impl.implementation_feature
@@ -479,6 +480,7 @@ feature -- Validity checking
else
boolean_type := current_universe_impl.boolean_type
l_assertion_context := new_context (current_type)
+ l_old_scope := current_object_test_scope.count
nb := a_postconditions.count
from i := 1 until i > nb loop
l_expression := a_postconditions.assertion (i).expression
@@ -493,9 +495,14 @@ feature -- Validity checking
error_handler.report_vwbe0a_error (current_class, current_class_impl, l_expression, l_named_type)
end
l_assertion_context.wipe_out
+ -- The scope of object-test locals can cover the following assertions
+ -- in the same postcondition clause because it's as if they were separated
+ -- by "and then" operators.
+ object_test_scope_builder.build_scope (l_expression, current_object_test_scope)
end
i := i + 1
end
+ current_object_test_scope.keep_object_tests (l_old_scope)
free_context (l_assertion_context)
has_fatal_error := has_fatal_error or had_error
end
@@ -539,6 +546,7 @@ feature -- Validity checking
had_error: BOOLEAN
l_class_impl: ET_CLASS
l_current_class: ET_CLASS
+ l_old_scope: INTEGER
do
has_fatal_error := False
l_class_impl := an_invariants.implementation_class
@@ -582,6 +590,7 @@ feature -- Validity checking
else
boolean_type := current_universe_impl.boolean_type
l_assertion_context := new_context (current_type)
+ l_old_scope := current_object_test_scope.count
nb := an_invariants.count
from i := 1 until i > nb loop
l_expression := an_invariants.assertion (i).expression
@@ -596,9 +605,14 @@ feature -- Validity checking
error_handler.report_vwbe0a_error (current_class, current_class_impl, l_expression, l_named_type)
end
l_assertion_context.wipe_out
+ -- The scope of object-test locals can cover the following assertions
+ -- in the same invariant clause because it's as if they were separated
+ -- by "and then" operators.
+ object_test_scope_builder.build_scope (l_expression, current_object_test_scope)
end
i := i + 1
end
+ current_object_test_scope.keep_object_tests (l_old_scope)
free_context (l_assertion_context)
has_fatal_error := has_fatal_error or had_error
if current_class = current_class_impl then

0 comments on commit 2610c8f

Please sign in to comment.