[ldv-project] CIL-OCaml Linux Driver testing - usbkbd.c and usbmouse.c

[Iyer,Naveen R]

Hi all !


I am trying to use C Intermediate Language (CIL) to test usbkbd.c and usbmouse.c drivers.

For normal .c source codes, I do the following:


>From the /cil-1.7.3 location:

bin/cilly --dologcalls --save-temps -D HAPPY_MOOD -I myincludes hello.c -o hello.exe


And it works.

However, my primary aim is to test usbkbd.c and usbmouse.c.

I have compiled the linux kernel and have tried to modify the drivers by adding few comments and commenting few lines and then "insmod"'ing them.

However, now if I want to use "cilly" to "make" these driver files, I do the following:


>From the /linux-3.13.0 location:

make CC=/home/naveen/cil-1.7.3/bin/cilly SUBDIRS=drivers/hid/usbhid/ CONFIG_USB_MOUSE=m modules


And running the above command I get the following error:

root at naveen-VirtualBox:/home/naveen/linux-3.13.0# make CC=/home/naveen/cil-1.7.3/bin/cilly SUBDIRS=drivers/hid/usbhid/ CONFIG_USB_MOUSE=m modules
/home/naveen/linux-3.13.0/arch/x86/Makefile:98: stack protector enabled but no compiler support
/home/naveen/linux-3.13.0/arch/x86/Makefile:113: CONFIG_X86_X32 enabled but no binutils support
gcc -D_GNUCC -E -print-file-name=include
  CC [M]  drivers/hid/usbhid/hid-core.o
Warning: Unknown argument -Wframe-larger-than=1024
Warning: Unknown argument -Werror=implicit-int
Warning: Unknown argument -Werror=strict-prototypes
gcc -D_GNUCC -E -Wp,-MD,drivers/hid/usbhid/.hid-core.o.d -include /home/naveen/linux-3.13.0/include/linux/kconfig.h -nostdinc -isystem /usr/lib/gcc/x86_64-linux-gnu/4.8/include -I/home/naveen/linux-3.13.0/arch/x86/include -Iarch/x86/include/generated -Iinclude -I/home/naveen/linux-3.13.0/arch/x86/include/uapi -Iarch/x86/include/generated/uapi -I/home/naveen/linux-3.13.0/include/uapi -Iinclude/generated/uapi -Iubuntu/include -D__KERNEL__ -fno-strict-aliasing -fno-common -fno-delete-null-pointer-checks -O2 -m64 -mno-mmx -mno-sse -mpreferred-stack-boundary=3 -mtune=generic -mno-red-zone -mcmodel=kernel -funit-at-a-time -maccumulate-outgoing-args -DCONFIG_AS_CFI=1 -DCONFIG_AS_CFI_SIGNAL_FRAME=1 -DCONFIG_AS_CFI_SECTIONS=1 -DCONFIG_AS_FXSAVEQ=1 -DCONFIG_AS_AVX=1 -DCONFIG_AS_AVX2=1 -pipe -fno-asynchronous-unwind-tables -mno-sse -mno-mmx -mno-sse2 -mno-3dnow -mno-avx -fno-omit-frame-pointer -fno-optimize-sibling-calls -fno-var-tracking-assignments -g -mfentry -DCC_USING_FENTRY -fno-strict-overflow -fconserve-stack -DCC_HAVE_ASM_GOTO -I myincludes -DMODULE -DKBUILD_STR(s)=#s -DKBUILD_BASENAME=KBUILD_STR(hid_core) -DKBUILD_MODNAME=KBUILD_STR(usbhid) -DCIL=1 drivers/hid/usbhid/hid-core.c -o ./hid-core.i
/home/naveen/cil-1.7.3/bin/cilly.native --out ./hid-core.cil.c --warnall --envmachine --dologcalls ./hid-core.i
/home/naveen/linux-3.13.0/arch/x86/include/asm/cpufeature.h[396:7-7] : syntax error
Parsing errorFatal error: exception Frontc.ParseError("Parse error")
make[1]: *** [drivers/hid/usbhid/hid-core.o] Error 2
make: *** [_module_drivers/hid/usbhid] Error 2


Could anyone please guide me on this?


Thanks

Regards
Naveen R. Iyer
Graduate Student (Research Division: Computer Engineering)
Dept. of Electrical & Computer Engineering
University of Florida
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://linuxtesting.org/pipermail/ldv-project/attachments/20150701/79855e77/attachment.html>