ENSURE

C++ Test Script Language

Syntax

ENSURE <native expression>

Location

WRAP, STUB, PROC

Description

The ENSURE statement describes a method post-condition. It can be used in a WRAP, STUB or PROC block.

Note The information below pertains to the use of ENSURE within a WRAP block. For more information about using the REQUIRE and ENSURE statement within a STUB or PROC block, please refer to the STUB and PROC.

<native expression>is a C++ Boolean expression (or an expression that can be converted into a Boolean), which can use:

  • Any of the public or protected class members.

  • The method parameters (with the names used in the signature or in the method definition).

  • Any of the global variables declared in the file where the method is defined.

  • The _ATO_result, _ATO_old and _ATO_in_exception variables (see below).

The following symbols cannot be used in the <native expression> parameter of the ENSURE statement:

  • Local variables

  • Macros

Variables

  • _ATO_result :This variable contains the method return value, if any. Its type is that of the method return type. Its value may be undefined if no value is returned (because an exception was thrown, or a return without a value is executed, or the function implicitly returns)._ATO_resultis not available when the option--postcondition_before_returnis activated (see Target Deployment Port options).

  • _ATO_old:This variablecontains a copy of the object as it was before the method call. The_ATO_oldobject is generated by the class copy constructor. If the class copy constructor is explicitly defined, you should remember that_ATO_oldis not araw copyof the current object, but a copy as defined by the copy constructor._ATO_oldis not available in constructors.

For performance purposes, the _ATO_old variable is generated only if it is used in the ENSURE expression.

  • _ATO_in_exception:This is a Boolean variable that isTRUEif the post-condition is executed because an exception has been thrown. This variable is available only if the Target Deployment Package is configured to support exceptions.

Evaluation

When --postcondition_before_return option is set in the Target Deployment Package .opp file, <native expression> is evaluated before the return expression. If the return expression evaluation causes side-effects, they are not taken into account at the time the post-condition is checked. This option is provided for compatibility with limited C++ compilers, and its use should be avoided as much as possible.

Otherwise, <native expression> is evaluated after any code of the method (local variables are already popped).

Warning: you can call methods in <native expression>, but you must make sure that these calls do not modify the object's state (that is, they do not write to any field). You can ensure this by calling const methods only. If you want the compiler to check this, use the ATO_AC_STRICT_CHECKING Target Deployment Port option.

Example

C++ source code example:

class Stack {

public:

int count;

Stack () : count(0) {}

void push (void *);

void *pop ();

};

C++ Contract Check Script code example:

CLASS Stack {

WRAP push

ENSURE (count == _ATO_old.count + 1)

}