svadev AT lists.siebelschool.illinois.edu

Subject: Svadev mailing list

List archive

Re: [svadev] SAFEcode typechecker

From: John Criswell <criswell AT illinois.edu>
To: Daniel Huang <dehuang AT fas.harvard.edu>
Cc: "<svadev AT cs.illinois.edu>" <svadev AT cs.illinois.edu>
Subject: Re: [svadev] SAFEcode typechecker
Date: Tue, 5 Feb 2013 10:36:32 -0600
List-archive: <http://lists.cs.uiuc.edu/pipermail/svadev/>
List-id: <svadev.cs.uiuc.edu>
Organization: University of Illinois

On 2/4/13 11:33 PM, Daniel Huang wrote:

Hi Svadev,

Could someone point out where the code for the SAFEcode type-checker is located in the repository? I'm curious to see how the typing-rules work in the C-implementation.

This may not be as helpful as you'd like. My recommendation is not to spend any time on it.

The SAFECode type-checker was last used in the original SVA work which used LLVM 1.9. You can get the code by checking out https://llvm.org/svn/llvm-project/safecode/branches/see. I believe the relevant files are lib/ProofWrap/ProofWrap.cpp and include/ProofWrap/ProofWrap.h.

Be forewarned that Dinakar Dhurjati (the original SAFECode author) was the only one that wrote, used, and understood this code.

-- John T.

Thanks,

Dan

_______________________________________________
svadev mailing list
svadev AT cs.uiuc.edu
http://lists.cs.uiuc.edu/mailman/listinfo/svadev

[svadev] SAFEcode typechecker, Daniel Huang, 02/04/2013
- Re: [svadev] SAFEcode typechecker, John Criswell, 02/05/2013