[seL4] Re: camkes-vm-linux kernel example

Hi Kent, no, I didn't changed the implementation of the poke module, just modified the string to be printed. Hugo, El jue., 1 jul. 2021 9:26, Kent Mcleod escribió:

On Thu, Jun 24, 2021 at 8:03 PM Hugo V.C. wrote:

...

Hi,

just a simple question: why this tutorial:

https://docs.sel4.systems/Tutorials/camkes-vm-linux.html

shows this output:

Welcome to Buildroot buildroot login: root Password: # grep poke /proc/devices # figure out the major number of our

driver

...

244 poke # mknod /dev/poke c 244 0 # create the special file # echo > /dev/poke # write to the file [ 57.389643] hi -sh: write error: Bad address # the shell complains, but our module is being invoked!

I'm not getting the shell complain error, just this:

# grep poke /proc/devices 247 poke # mknod /dev/poke c 247 0 # echo > /dev/poke [ 138.946905] TOC TOC NEO... #

FYI: my kernel is a custom compiled one but same version as the pre-compiled you provide:

# uname -a Linux buildroot 4.9.189 #4 SMP Thu Jun 24 00:16:49 CEST 2021 aarch64 GNU/Linux

Any hint?

Have you changed the implementation of poke_write? By the end of the tutorial there isn't a write error in the example shell output. I think if the kernel module returns a different length result than what was requested the shell interprets this as a write error. If you return the correct length that was requested then there would be no error. (This is a guess though)

Kent.

...

Cheers, _______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems