Type checker: missing exit checks

[joey-coleman]

The following bug was originally reported on Sourceforge by nick_battle, 2009-09-28 11:31:09:

The type checking of statements which handle exceptions (eg. trap) looks for whether the body of the specification covered can in fact throw exceptions, raising an error if not. This search process is limited in VDMJ. In particular, it cannot cross an operation call, assuming that all operations can raise exceptions. This leads to false negatives - not reporting a TC error, when it should.

[joey-coleman]

Comment by nick_battle, 2013-05-31 21:00:24.329000:

• Release: --> v2.0.0beta2

[joey-coleman]

Comment by nick_battle, 2013-05-31 21:00:24.573000:

Still present in 2.0.0b2

[joey-coleman]

Comment by nick_battle, 2013-08-09 07:32:45.420000:

• Release: v2.0.0beta2 --> v2.0.0beta4

[joey-coleman]

Comment by nick_battle, 2013-08-27 15:48:50.271000:

• Release: v2.0.0beta4 --> v2.0.0beta5

[joey-coleman]

Comment by nick_battle, 2013-09-02 11:07:24.655000:

• Release: v2.0.0beta5 --> v2.0.0beta6

[joey-coleman]

Comment by nick_battle, 2013-10-16 07:06:17.198000:

• Release: v2.0.0beta6 --> v2.0.0

[joey-coleman]

Comment by nick_battle, 2013-10-16 07:06:17.629000:

Still in 2.0

[lausdahl]

Please add test case!

[nickbattle]

Here you go...

operations
    op1: () ==> ()
    op1() ==
        trap e with skip in skip;       -- error as expected

    op2: () ==> ()
    op2() ==
        trap e with skip in noop();     -- should also be error, but isn't

    noop: () ==> ()
    noop() == skip;     -- NB. no exceptions!

[nickbattle]

This is now much improved in VDMJ and the example above is certainly reporting problems correctly:

Parsed 1 module in 0.124 secs. No syntax errors
Error 3241: Body of trap statement does not throw exceptions in 'DEFAULT' (test.vdm) at line 4:9
Error 3241: Body of trap statement does not throw exceptions in 'DEFAULT' (test.vdm) at line 8:9
Type checked 1 module in 0.254 secs. Found 2 type errors

Applying the changes to the Overture visitor framework next...

[nickbattle]

Now fixed in Overture on ncb/development.

[nickbattle]

Added some extra changes that allow expressions to be searched for exit clauses (via their apply calls, which may be operations that raise exceptions).