Skip to content

Handle structure with positional trait whose first member is not required.  #727

@rishav-karanjit

Description

@rishav-karanjit

If I have a structure like this:

operation GetIntegerOutputPosition {
  input: GetIntegerOutputPositionInput
  output: GetIntegerOutputPositionOutput,
}

structure GetIntegerOutputPositionInput {
  value: Integer
}

@positional
structure GetIntegerOutputPositionOutput {
  value: Integer
}

From this model, the Dafny code will be polymorph'ed as

method GetIntegerOutputPosition ( input: GetIntegerOutputPositionInput )
      returns (output: Result<int32, Error>) 

Which is wrong because based on the model the return type should be Option.

To resolve this issue, there are two solutions:

  1. The polymorph should fail with a validation error.
  2. This should be generated as Option but not int32

Metadata

Metadata

Assignees

No one assigned

    Labels

    soundnessBugs that cause the generated code to compute the wrong value or crash

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions