Flexelint: WRK_BgThread starts threads

d90da286 · Nils Goroll · 600b092c · d90da286
Unverified Commit d90da286 authored Nov 26, 2023 by Nils Goroll
Hide whitespace changes
Inline Side-by-side

Showing with 4 additions and 0 deletions

flint.lnt src/flint.lnt +4 -0

No files found.
--- a/src/flint.lnt
+++ b/src/flint.lnt
 -header(flint.h)

+// semantics
 -sem(VAS_Fail, r_no)
+-function(pthread_create(3), WRK_BgThread(3) )
+
 -e801			// goto
 -e716			// while(1)
 -e717			// do ... while(1) ...
@@ -79,6 +82,7 @@
 -esym(528, init_*, assert_fcos*)
 -esym(755, BWIT_*)
 -esym(755, fc_inj_*, FC_INJ_SZLIM_SET)	// not referenced
+-esym(457, assert_fcos_transition)	// wrongbuf

 // fellow_io_uring.c
 -emacro(835, BLKDISCARD)