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

Is not yet specified does not work with overloads #666

Closed
lausdahl opened this issue Feb 19, 2018 · 9 comments
Closed

Is not yet specified does not work with overloads #666

lausdahl opened this issue Feb 19, 2018 · 9 comments
Labels
bug Incorrect behaviour of the tool Mergable A fix is available on a branch to merge for release
Milestone

Comments

@lausdahl
Copy link
Member

Description

When this model show below is generated and the getenv method is implemented then the interpreter still complains that it cannot find:

Cannot find native method: bridge.SystemEnv.getenv(org.overture.interpreter.values.Value, org.overture.interpreter.values.Value)

Main 206: Error evaluating code
Detailed Message: Cannot find native method: bridge.SystemEnv.getenv(org.overture.interpreter.values.Value, org.overture.interpreter.values.Value)

however it should never have searched for this method but the other one with only one argument.

class bridge_SystemEnv

types

public String = seq of char;
functions
  public static getenv: String -> [String]
  getenv(name)== is not yet specified;
  
  public static getenv: String * String -> String
  getenv(name,default)== let v = getenv(name) in if v=nil then default else v;
		
end bridge_SystemEnv

[Description of the issue]

Steps to Reproduce

make the model and try to run it

Expected behavior: no error

Actual behavior: reports that it cannot find a method which is fully implemented in VDM

Reproduces how often: always

Versions

Version: 2.5.6
Build date: 2017 Dec 11 09:50 CET
Git commit description: Release/2.5.6

@lausdahl lausdahl added the bug Incorrect behaviour of the tool label Feb 19, 2018
@nickbattle
Copy link
Contributor

I'll take a look at this. You mean this is an interpreter error, not an error with the code generator (you used the word "generated")?

@peterwvj
Copy link
Member

I take my previous comment back - I misread the model, sorry.

@peterwvj
Copy link
Member

peterwvj commented Feb 20, 2018

I'm not sure I understand this issue. When the getenv operation that takes two arguments is called, the interpreter raises an error because this operation invokes the other genenv operation (this line: let v = getenv(name)) which uses the is not yet specified construct.

λ java -jar Overture-2.5.6.jar -vdmpp A.vdmpp -i
Parsed 1 class in 0.045 secs. No syntax errors
Type checked 1 class in 0.053 secs. No type errors
Initialized 1 class in 0.044 secs. 
Interpreter started
> p bridge_SystemEnv`getenv("first", "second")
Error 4024: 'not yet specified' expression reached in 'bridge_SystemEnv' (A.vdmpp) at line 8:18
Stopped in 'bridge_SystemEnv' (A.vdmpp) at line 8:18
8:    getenv(name)== is not yet specified;
[MainThread-3]> 

@peterwvj peterwvj added this to the v2.6.2 milestone Feb 20, 2018
@nickbattle
Copy link
Contributor

I think it may be a problem with what happens when there is a delegate Java class (here called bridge.SystemEnv) on the classpath? It may be that when it is working out what method of that class to call, it somehow deduces it is the outer two-param overload rather than the one param one. I need to create a small test Java class to try that out though...

@nickbattle
Copy link
Contributor

OK, I can reproduce this. You can force the error by calling a one-param function when there is a two-param overload. I suspect it is in the binding process in the Delegate class. Will investigate. This doesn't happen in VDMJ though.

@nickbattle
Copy link
Contributor

OK, as I suspected it is to do with the way that definitions are looked up and then bound to the class. It just happens to work in VDMJ because of the ordering; Overture has a FIXME about ordering, and just happens not to work. It should be fixable... I'll have a look later.

@nickbattle
Copy link
Contributor

I've just pushed a fix to ncb/development. It seems to work. Can someone else give it a try?

@nickbattle nickbattle added the Mergable A fix is available on a branch to merge for release label Feb 21, 2018
@nickbattle
Copy link
Contributor

Incidentally, the fix for this can't quite distinguish overloads as well as the type checker can. If you have two overloads with different parameter types, but the same parameter names and number of parameters, then you may still get problems. A workaround in this case is to rename the parameters so that they can be distinguished by name alone. To fix it so that we do a full type-checked comparison would be much more difficult (that information is tricky to get from the execution context).

@peterwvj
Copy link
Member

peterwvj commented Feb 22, 2018

Fortunately, this situation is not that likely to occur anyway. Now that it's explained in the issue tracker, I think it's fine to consider this issue closed.

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 Mergable A fix is available on a branch to merge for release
Projects
None yet
Development

No branches or pull requests

3 participants