Dear all,
I'd like to highlight two new features that have made it into CIL recently:
support for static local variables and GCC's "computed gotos" (or "labels as
values").
Both of them are disabled by default for backwards compatibility. However, the
former changes a bit how GVar constructors are used. You might need to update
your code if you are creating GVar global variables (see below).
Please, do not hesitate to send any feedback so that we can iron out the details
before the next release.
Static variables
----------------
The type varinfo has a new field, vinit of type initinfo, which contains the
initializer of the variable if there is one. It is only used for static and
global variables: initializers for automatic variables are still split into
Set instructions at the beginning of each function. (In particular, the const
qualifier is still discarded, except for static const variables.)
The current behaviour is that static local variables are translated into
global static variables. This translation is now controlled by the flag
--makeStaticGlobal, which is enabled by default to keep backwards compatibility.
If you use the flag --noMakeStaticGlobal instead, static variables are kept
local, accessible through the slocals list of fundec, and you can find the value
of the initializer in the vinit field of the varinfo.
Note that the vinit field of varinfo will be filled regardless of the mode you
chose. This changes how global variable definitions GVar are used. If you have
GVar(vi, init, l) then vi.vinit == init. Note the *physical* equality. You
should take care to preserve this equality when creating new GVar:
let makeGVar () =
let vi = ... in
vi.vinit.init <- ... ;
GVar(vi, vi.vinit, l)
The CIL visitor does the right thing, so it will only visit the initializer
once.
Computed goto
-------------
There is a new kind of expression, AddrOfGoto, to represent GCC's operator &&
which takes the address of a label. Similarly to Goto, it expects a reference
to the label the address of which is retained.
There is also a new statement kind, ComputedGoto, which expects an expression of
type void* holding the address of a label. It represents GCC's goto *(...).
Note that the derefence is implied in ComputedGoto, such that
ComputedGoto(AddrOfLabel sref, loc)
is equivalent to
Goto(sref, loc)
(there is no need to use Mem).
The current behaviour is that computed goto are translated into a state-machine
using switch. This translation is now controlled by the flag --useComputedGoto,
which is disabled by default to keep backwards compatibility.
Best regards,
--
Gabriel Kerneis
------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
CIL-users mailing list
CIL-users@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/cil-users
