search

Baltoli / project-docs

Documents for my Part III project
0 stars 0 forks source link

Indirection is not parsed correctly #6

Closed Baltoli closed 7 years ago

Baltoli commented 7 years ago

The value of the indirection in the manifest is not the variable name, but instead is one of the structure fields. Initially noticed in the locks example, but only when trying to write an assertion like:

eventually(call(init(&lock)))

The issue does not appear when writing assertions of the form:

eventually(lifetime(&lock))

where lifetime is an explicit automaton.

Baltoli commented 7 years ago

Similar problem to the other one related to pass-by-value structs. The problem isn't there if the result of taking the address is itself a pointer - if it's a struct, we end up on the code path where the parser tries to split up all the arguments, which isn't what we want (I don't think).

If we use the same hack as before to specialise for value structs coming through, we run into a problem where it can't be printed.

Baltoli commented 7 years ago

Have verified that the indirection syntax does work, but only if the target of the indirection is a pointer (rather than a struct). Sent Jon a message asking about this, as the test case for parsing indirections uses &pointer_var rather than &struct_var, so this might be a known issue.

Baltoli commented 7 years ago

Jon said this probably is a bug, but it's not affecting me right now so will close.