search

microsoft / Armada

Armada is a tool for writing, and proving correct, high-performance concurrent programs.
Other
137 stars 19 forks source link

Taking address of array causes crash #22

Closed jaylorch closed 3 years ago

jaylorch commented 3 years ago

The Armada program below crashes the state-machine translator while it's in HeadWithProxyArgs, since HeadWithProxyArgs doesn't support the sized-array case. Instead, Armada should report a bug due to the developer trying to take the address of an array (instead of an array element).

include "../../Armada/ArmadaCommonDefinitions.dfy"

structs SharedStructs {
  struct S {
    var x: uint32;
  }
}

level Test using SharedStructs {
  method main ()
  {
    var a: S[10];
    var p: ptr<S>;
    p := &a;
  }
}