Svadev mailing list

[John Criswell <criswell AT illinois.edu>]

On 4/21/12 3:39 PM, Daniel Huang wrote: Hi,

Is there a place that documents all the instructions a SAFECode instrumentation pass can emit?

Are you asking for a list of all the run-time checks that SAFECode could emit and the situations under which it would do so, or are you asking which subset of the LLVM instruction set SAFECode instruments correctly?

 I'm thinking about building a verified type-checker for a subset of SVA and knowing what I need to model/how they work would be of great help. Right now, I've been writing test programs and trying to reverse engineer what the individual functions are doing w.r.t to the PLDI paper ...

Is your type-checker just checking that SVA enforces the points-to analysis and type-inference analysis correctly, or is it doing something more?

I can try to write up a description of the SAFECode run-time checks in the SAFECode Software Architecture manual.  Would that help?

-- John T.

Regards,

Dan

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