Fix CI and allow record field access#158
Fix CI and allow record field access#158phiwuu merged 3 commits intobmw-software-engineering:mainfrom
Conversation
… (step 1/2) * Update PyVCG and CVC5 * Permit record field references * Add new LRM rule that the prefix of a dereference may not be null * Add unsupported note in VCG (this will be done in step 2)
… (step 2/2) * Add basic support for record references in VCG. Some bits (like references in quantifiers) do not work yet.
It is dead.
|
|
||
| type T { | ||
| arr Integer [2 .. *] | ||
| ref T |
There was a problem hiding this comment.
Should a recursive type not be optional?
There was a problem hiding this comment.
So its possible but unlikely for such a type to exist. I made it non-optional in the test to avoid having to write the null guard :)
A future lint check would probably be a good idea, to spot any self or mutual recursion with all links being non-optional.
|
|
||
| type T { | ||
| value Integer | ||
| arr T [0 .. *] |
| cb_link.item >= 50000, warning "cb item value is oddly low" | ||
| // you can obtain a tuple's values | ||
|
|
||
| bar.asil == asil, warning "mismatch in ASIL levels" |
There was a problem hiding this comment.
We should have a positive testcase for this. I only see negative testcases
There was a problem hiding this comment.
That's not a test, that is an example fragment of the LRM.
Or do you mean having a test that shows such a construct passing?
There was a problem hiding this comment.
Sorry for the late reply, havent seen your comments. I meant: I went through the test_cases and did not find any positive test case for this, there were only negative ones.
| link = R1 | ||
| } | ||
|
|
||
| T R3 { |
|
Thanks for implementing it, Florian! |
|
A much bigger change is coming that properly fixes VCG for this. |
|
Thanks, Looking Forward the the PR! Do you need any assistance for this? |
3 participants
This obsoletes PR #153.
This fixes #157 (OSX13 is dead).
This implements the first step in #156.