hello,
I am currently looking at CIL for using it as part of my PhD project.
I would like to use CIL to instrument C implementations of cryptographic
protocols to output the protocol narration when they are run (much like
symbolic execution in CREST is working). I tried running CIL on OpenSSL
and it works, with one exception: during processing of sha512.c I get:
/c/docs/verification/tools/cil-1.3.7/obj/x86_WIN32/cilly.asm.exe --out
./sha512.cil.c --dologcalls --warnall ./sha512.i
sha512.c:77: Unimplemented: Cannot represent integer
0xcbbb9d5dc1059ed8ULL in 64 bits (signed)
(followed by several similar lines). The line in question is
c->h[0]=0xcbbb9d5dc1059ed8ULL;
where c is defined as
typedef struct SHA512state_st
{
unsigned long long h[8];
unsigned long long Nl,Nh;
union {
unsigned long long d[16];
unsigned char p[(16*8)];
} u;
unsigned int num,md_len;
} SHA512_CTX;
could you please provide some information about what is happening?
If I exclude sha512c from CIL processing, the rest of OpenSSL goes
through fine, so I am really impressed!
Best,
Misha
------------------------------------------------------------------------------
Let Crystal Reports handle the reporting - Free Crystal Reports 2008 30-Day
trial. Simplify your report design, integration and deployment - and focus on
what you do best, core application coding. Discover what's new with
Crystal Reports now. http://p.sf.net/sfu/bobj-july
_______________________________________________
CIL-users mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/cil-users
