search

microsoft / Armada

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

Return more than one value in concrete level #28

Closed MadeByMars closed 3 years ago

MadeByMars commented 3 years ago

As discussed in the meeting, Armada generates this error for concrete level:

cuckoo.arm_preproc.arm(615,7): Warning: Method cuckoohash_map_lock_three has more than one return value

Here is line 615 of cuckoo.arm_preproc.arm:

method cuckoohash_map_lock_three(this_ptr: ptr<cuckoohash_map>, ...) returns (ret1: TwoBuckets, ret2: LockManager)