Skip to content

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

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

Activity

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

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