PR# 16353 Postcondition of non-fresh once routines is not checked

Problem Report Summary

Submitter: juliant

Category: Runtime

Priority: Low

Date: 2009/10/12

Class: Bug

Severity: Non-critical

Number: 16353

Release: 6.4

Confidential: No

Status: Open

Responsible:

Environment: Windows 7

Synopsis: Postcondition of non-fresh once routines is not checked

Description

The postcondition for non-fresh once routines is not checked, although it should according to ECMA General Call Semantics (8.23.26).

To Reproduce

foo (i: INTEGER): INTEGER
       require
               i > 0
       once
               Result := i * 2
       ensure
               Result = i * 2
       end

make
       local
               i: INTEGER
       do
               i := foo (2) -- 4
               i := foo (3) -- 4, but should be postcondition violation
               i := foo (-1) -- precondition violation
       end

Problem Report Interactions