hi all,
what is the statement regarding CIL and compiler warnings that are not
triggered in the original code, but that appear after the translation? I
am seeing some of these when trying to compile OpenSSL (it is triggering
-Wshadow for instance). Should I report those or is the warning
behavio
hi,
when I try to compile the attached file with CIL and
-Wmissing-prototypes, I get
cilly -Wmissing-prototypeshello.c -o hello
C:/programs/cygwin/bin/gcc -D_GNUCC -E -DCIL=1 hello.c -o
/tmp/cil-bojpekco.i
/c/docs/verification/tools/cil-1.3.7/obj/x86_WIN32/cilly.asm.exe --out
/tmp/cil-OW
Benjamin Ylvisaker wrote:
> On Oct 26, 2009, at 11:34 AM, Misha Aizatulin wrote:
>
>> It would be really nice if I could tell CIL not to remove some of the
>> definitions, for instance by using an attribute. Any comments on that?
>
> Do you mean something other than the
> Here is how we solve the very same problem for CPC:
>
> # Makefile
> .cpc.cpi:
> gcc -E -x c $(CFLAGS) -include cpc/cpc_runtime.h \
> -o $@ $<
>
> And then, process the .cpi files with CIL.
I realised that this is not quite the right thing for me, because I
run CIL on a big and
Gabriel Kerneis wrote:
> On Thu, Oct 22, 2009 at 08:21:59AM +0100, Misha Aizatulin wrote:
>> Does anyone have a suggestion for dealing with this? Is there a way to
>> add something to the file before the first preprocessing pass?
>
> Here is how we solve the very
hi,
I'm facing the following problem: I'm inserting some function calls
into the code using CIL. The new functions are defined in a separate
header, say funs.h. The naive idea would be to add
GText "#include \"funs.h\""
to the list of globals, however this doesn't work: if funs.h itself
#inclu
Hi Kristis,
> For whatever it's worth, I've run against a problem similar to this
> using CIL 1.3.7, but NOT CIL 1.3.6. So I'm now using CIL 1.3.6 as a
> quite stable version.
>
> Also note that this problem does not appear using the latest CIL from
> the repository.
great to know, thanks!
M
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
an
