C Instrumentation Framework

The output files produced by CIF are used as input source files to be verified by BLAST.
Now I want to compile it using GCC compiler in order to use some other tools to verify the code. But it always give me some error like

"../inst/current/envs/linux-2.6.36/linux-2.6.36/arch/x86/include/asm/thread_info.h:179: error: register name not specified for ‘current_stack_pointer’".

Thanks to Evgeny Novikov, I know where this error comes from:

I know that instrumented source code (like in cdrom.o.c) isn't perfect. It looks to be rather good for tools like CIL, BLAST, CPAchecker, UFO, CBMC and many others. But for a very strict compiler that tries to produce object/binary code on the basis of instrumented source code it isn't enough.
The error is presented from 171 to 179 lines of arch/x86/include/asm/thread_info.h file (http://lxr.free-electrons.com/source/arch/x86/include/asm/thread_info.h#L171). I can suggest that instead of:
register unsigned long current_stack_pointer asm("esp") __used;
something like:
register unsigned long current_stack_pointer;

But when I have simply replace the instruction:
register unsigned long current_stack_pointer;
with:
register unsigned long current_stack_pointer asm("esp") __used;

it still come with some other errors like

$gcc cdrom.o.c -o cdrom.o
....
....
/tmp/ccIgAU1q.o:(.rodata+0x16a8): undefined reference to `__crc_cdrom_get_media_event'
collect2: error: ld returned 1 exit status


I'm now using Predator(http://www.fit.vutbr.cz/research/groups/verifit/tools/predator/) to verify the driver codes. It's loaded as a plugin of gcc. And I want to use CIF to generate a closed source file for Predator to verify. So, I want to find out how can gcc compile the CIF output files.

The output file is generated by LDV using commmands like:
LDV_DEBUG=100 LDV_VIEW=y time ldv-manager envs=linux-2.6.36.tar.bz2 drivers=drivers/cdrom rule_models=32_7a kernel_driver=1
I have attached the .macro and cdrom.o.c files.

Thank you!