Update to Overture 3.0.0 #127
Labels
Comments
|
@nickbattle do you have any idea of things that have changed since overture 2.6.4 that has to be reflected in vdm2c? |
|
@CThuleHansen Phew... well, I can start by looking through the bug list, though most of the fixes are really "bugs" in the way VDMJ/Overture works, rather than fundamental changes that would change code generation. If you can give me an example of a piece of C that has changed (before/after compare?), I might be able to guess the area more easily? |
|
@nickbattle so one example is the one in the original issue, where it tries to find a variable in a wrong class. |
|
@idhugoid i investigating currently |
|
@CThuleHansen Yes, I saw the one-liner in the issue above. But without more context, it's hard to know what created that. Is it possible to create a small example VDM++ spec that translates into two different C files? Perhaps based on the class in which this one-liner occurs? That would be easier to investigate. |
|
So this model does it: @idhugoid have you come any further? |
|
The tests works with overture 2.6.4 on ubuntu with gcc (not on mac with clang). This is also tested via github actions. All 4 vdm-rt examples (pretty much with the same error) and 1 vdmPP (with different error):
To test overture 3.0.0 on ubuntu I set up a github actions for the branch update_overture30 (Action running as we speak. To test it locally I created a docker container. Scripts are below: Dockerfile: Failure trace: |
|
@nickbattle I seem to have pinpointed it to here (note, the code snippet below is scrollable): In particular line 191: thisClassName = varExp.getAncestor(SClassDefinition.class).getName().getName(); which evaluates to Controller, but should be ValveActuator.
Related vdmrt position: (https://github.com/INTO-CPS-Association/example-single_watertank/blob/master/Models/SingleWT/ValveActuator.vdmrt#L14) If you run the test I am not familiar with how the codegeneration works or the overture AST, so it is quite time consuming to figure this out :D Using Does it help in any way? |
|
@CThuleHansen This is great detective work, but I'm not familiar with the code generator either. Are we still able to contact @peterwvj at all? It sounds as though something has happened to the ancestry structure in the codegen "IR" tree, but I can't imagine what change(s) in Overture might have caused that. |
|
@nickbattle I am unsure whether he can be contacted in this regard or not. The ancestry is as follows
|
|
@CThuleHansen OK, this is very strange. I started by assuming that the parent/child relationship was to do with the class hierarchy (eg. that ValveActuator was a subclass of Controller), but it is not; rather, ValveActuator is an instance variable within Controller. So it's lost track of which class it is generating, by the look of it. I assume the operation of this model in Overture is still correct? I mean, it does call the setValve method of the ValveActuator correctly? If you translate a simple two-class model with a Controller with an instance variable of a ValveActuator, does that translate correctly? |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
So the updating of VDM2C seems to have fallen behind - probably because @peterwvj just silently fixed everything beforehand 👍
Anyways, the challenge remains. I am tagging some people that I hope can help out with the task.
@nickbattle @idhugoid @peterwvj (as he might have some knowledge of the infrastructure) and @lausdahl .
I am experiencing the following:
Using overture 3.0.0 it still compiles, but the generated C does not.
I am pinpointed the issue to be related to classes somehow.
The water tank will serve as an example below.
With Overture 3.0.0 the
valveactuatorattempts to access fields of thecontroller:With Overture 3.6.4 it correctly uses
ValveActuatorclass.So the challenge is to update vdm2c from using Overture 2.6.4 to Overture 3.0.0.
I have not had time to dig further into this yet.
@idhugoid and I will have a meeting later today (Monday 21st September, 2020) to update the overture procedure such that vdm2c is updated on Overture updates.
The text was updated successfully, but these errors were encountered: