microsoft / Armada

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

Concrete-level checker unnecessarily rejects return of multiple values #18

Open jaylorch opened 3 years ago

jaylorch commented 3 years ago

The concrete-level checker rejects a concrete level that contains a method with more than one returned value. However, it doesn't need to do this, since the Clight compiler properly handles returning multiple values.