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? 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. > 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 Best regards, -- Gabriel ------------------------------------------------------------------------------ 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