Hi Gabriel, On Thu, Sep 19, 2013 at 2:11 AM, Gabriel Kerneis <gabr...@kerneis.info> wrote: > On Wed, Sep 18, 2013 at 03:58:46PM -0400, Edward Schwartz wrote: >> Are the CIL semantics formally defined anywhere? I am aware of >> http://www.cs.berkeley.edu/~necula/Papers/cil_cc02.pdf but it seems >> incomplete. Alternatively, is there a concrete evaluator for CIL? I >> am particularly interested in the semantics of casts, and how >> expressions can be created that use the Ptr type. > > I'm not aware of it. You have the LLVM backend in CIL source, but I wouldn't > call that a (reference) "concrete evaluator". Basically, CIL is a subset of > the C language so its semantics are the C semantics on that subset... but > that doesn't help a lot since the C semantics is quite tricky! Could you give > an example of what exactly you would like to evaluate?
Thanks, I did not consider the LLVM backend, but it does seem helpful for understanding the possible casts. Explicitly naming types of casts like llvm does seems a lot cleaner to me than simply expressing "coerce expression to <type>". Anyway, I was looking for the CIL semantics to understand all possible derivations of expressions that can be used as pointers to stack and global objects. Is it reasonable to assume that AddrOf or StartOf must be used in any expression that points to a stack or global object (without referencing an existing lvalue that points to the object)? > > There is some work in the K c-semantics repository on that matter too: > http://code.google.com/p/c-semantics/source/browse/ (svn/trunk/cil-semantics) > > If you want a C-like subset with a formally defined semantics, you might > be interested in CompCert and Cminor in particular. CompCert used to use > CIL as a front-end, but they switched to their own parser and AST a long time > ago. I'm just trying to understand CIL's semantics a little better, whether formally or informally. > >> Also, is the CCured source code available anywhere? There are a few >> references to it in the CIL source code, but that is all. > > When I took over CIL maintenance, I decided not to care about CCured because > I knew nothing about it and had not interest in what it did. I believe that > the source code unfortunately disappeared when CIL svn at Berkeley was shut > down, but some people on the list might still have a copy. > > http://stackoverflow.com/questions/15230380/where-to-download-ccured Thanks, Ed ------------------------------------------------------------------------------ LIMITED TIME SALE - Full Year of Microsoft Training For Just $49.99! 1,500+ hours of tutorials including VisualStudio 2012, Windows 8, SharePoint 2013, SQL 2012, MVC 4, more. BEST VALUE: New Multi-Library Power Pack includes Mobile, Cloud, Java, and UX Design. Lowest price ever! Ends 9/20/13. http://pubads.g.doubleclick.net/gampad/clk?id=58041151&iu=/4140/ostg.clktrk _______________________________________________ CIL-users mailing list CIL-users@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/cil-users
