Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Type checker defines RESULT symbol for post condition of void operations #727

Closed
nickbattle opened this issue Jun 7, 2020 · 1 comment
Closed
Labels
bug Incorrect behaviour of the tool language Issues in parser, TC, interpreter, POG or CG Mergable A fix is available on a branch to merge for release
Milestone

Comments

@nickbattle
Copy link
Contributor

The RESULT symbol is defined for functions and operations that return a value. But not all operations return a value - some are void. However, the type checker defines a "void" valued RESULT symbol in this case. There should be no such symbol. For example:

operations
	op: () ==> ()
	op() == skip
	post RESULT > 0;    -- Error: Left hand of > is not ordered. Actual: ()

This ought to say that there is no symbol RESULT in scope.

@nickbattle nickbattle added bug Incorrect behaviour of the tool language Issues in parser, TC, interpreter, POG or CG labels Jun 7, 2020
@nickbattle
Copy link
Contributor Author

Now fixed in ncb/development:

Error 3182: Name 'DEFAULT`RESULT' is not in scope in 'DEFAULT' (test.vdm) at line 4:10

@nickbattle nickbattle added the Mergable A fix is available on a branch to merge for release label Jun 7, 2020
@idhugoid idhugoid added this to the v3.0.0 milestone Aug 28, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Incorrect behaviour of the tool language Issues in parser, TC, interpreter, POG or CG Mergable A fix is available on a branch to merge for release
Projects
None yet
Development

No branches or pull requests

2 participants