creating sys/ forwarding header /tmp/rig/forwarder_x86_64/include/poll.h
creating sys/ forwarding header /tmp/rig/forwarder_x86_64/include/syslog.h
creating sys/ forwarding header /tmp/rig/forwarder_x86_64/include/ucontext.h
cc  -O2 -pipe   -D_KERNEL -Wall -Wredundant-decls -Wnested-externs -Wstrict-prototypes  -Wmissing-prototypes -Wpointer-arith -Wcast-qual  -Wold-style-definition -Wmissing-include-dirs  -Wno-pointer-sign -Winit-self -Wundef -Wno-unused-but-set-variable -std=gnu11  -DKLD_MODULE -nostdinc  -I. -Idragonfly -I/tmp/rig/forwarder_x86_64/include -Idragonfly/../include -I/usr/include  -Wold-style-declaration -fno-common -ffreestanding -fno-stack-protector -fno-strict-aliasing -fno-strict-overflow -fno-asynchronous-unwind-tables -fno-omit-frame-pointer -mcmodel=kernel -mno-red-zone -mno-mmx -mno-sse -msoft-float -mno-fp-ret-in-387 -mindirect-branch=thunk-inline   -c seqputs_rig.c
cc -Wl,--build-id=sha1 -nostdlib -Wl,--hash-style=sysv   -r -Wl,-d -o seqputs_rig.ko seqputs_rig.o
Warning: Object directory not changed from original /tmp/rig
cc  -O2 -pipe   -D_KERNEL -Wall -Wredundant-decls -Wnested-externs -Wstrict-prototypes  -Wmissing-prototypes -Wpointer-arith -Wcast-qual  -Wold-style-definition -Wmissing-include-dirs  -Wno-pointer-sign -Winit-self -Wundef -Wno-unused-but-set-variable -std=gnu11  -DKLD_MODULE -nostdinc  -I. -Idragonfly -I/tmp/rig/forwarder_x86_64/include -Idragonfly/../include  -Wold-style-declaration -fno-common -ffreestanding -fno-stack-protector -fno-strict-aliasing -fno-strict-overflow -fno-asynchronous-unwind-tables -fno-omit-frame-pointer -mcmodel=kernel -mno-red-zone -mno-mmx -mno-sse -msoft-float -mno-fp-ret-in-387 -mindirect-branch=thunk-inline   -c seqputs_rigc.c
cc -Wl,--build-id=sha1 -nostdlib -Wl,--hash-style=sysv   -r -Wl,-d -o seqputs_rigc.ko seqputs_rigc.o
-rw-r--r--  1 root  wheel  936 Oct 11 21:28 seqputs_rig.ko
-rw-r--r--  1 root  wheel  936 Oct 11 21:28 seqputs_rigc.ko
                 U __start_set_modmetadata_set
                 U __start_set_sysinit_set
                 U __stop_set_modmetadata_set
                 U __stop_set_sysinit_set
                 U kprintf
                 U ksnprintf
                 U module_register_init
-rw-r--r--  1 root  wheel  3768 Oct 11 21:29 seqputs_rig.ko
-rw-r--r--  1 root  wheel  3304 Oct 11 21:29 seqputs_rigc.ko
DF5778: ==== all proofs complete ====
seqputs_rig: loaded
seqputs_rig A: %n wrote 2 (2 == LIVE write conv)
seqputs_rig B: seq_puts(m,data) produced: 'conn=DP-1 link=0 ok=100%
'
seqputs_rig B: Linux contract would print the literal data string verbatim (no interpretation)