How to say `is_thread_run(run) == true` using mutex?

[Kiwamu Okabe]

Dear all,

I'm using mutex on VeriFast, but it can't say `is_thread_run(run) == true`.

https://github.com/metasepi/postmortem/blob/master/Security-Advisory/FreeBSD-kernel/FreeBSD-SA-20:20.ipv6/Resolution/VeriFast/error/main.c

Above code is written reference to following:

https://github.com/verifast/verifast/blob/master/tutorial_solutions/mutexes.c

Best regards,
--
Kiwamu Okabe at METASEPI DESIGN

[bart....@cs.kuleuven.be]

Dear Kiwamu,

You have to insert //@ : thread_run after the parameter list of function ip6_thread.

Best,

Bart

[Kiwamu Okabe]

Dear Bart,

On Fri, Aug 28, 2020 at 9:59 PM bart....@cs.kuleuven.be
<bart....@cs.kuleuven.be> wrote:
> You have to insert //@ : thread_run after the parameter list of function ip6_thread.

It's fixed with your advice.
Thanks, but I'm sorry to miss-understand the thread.