----- Brad Hards <[email protected]> wrote: > Overall, I think it might be easier if there was a script to check for CVC3 > and a GCC with plugin support, and to set things up. Ideally I would be able > to use the CVC3 packages from my distro, and gcc header (when gcc 4.5 > actually > gets released). > > A patch to implement this is attached. > > The only problem is that CVC3 doesn't actually use pkgconfig yet, and while I > have a patch to fix that, I'm not sure if it will get applied. The backup > plan > is to do a search for the includes / libs, but pkgconfig would be nicer. > > Thoughts, comments?
Wow, thanks! A few comments: 1. It looks like there is a config.h.in missing from the patch. 2. Can this be made to work even if CVC3 does not use pkgconfig? 3. I'm not sure pkgconfig is really needed for CVC3; I'd thought of configuration for this project as being: ./configure [--with-cvc3=/path/to/cvc3] [--with-yices=/path/to/yices] And auto-detect the GCC headers as your patch does. (I have zero experience building configure scripts though) > BTW: Now I have it built, can I have a hint on how to run this stuff? Yep, the tool runs in two phases; the frontend to build databases with CFGs and other source information, and the backend to do the actual analysis and assertion checking. If you want to use annotations, adapt the nsDebug.h patch for the program you're testing and you'll have the appropriate macros. For the frontend, there are two different methods: 1. Building a toy/test program: gcc -fplugin=/path/to/xgill.so test.c gcc -E test.c | xsource 2. Building a real project: Copy the bin/wrap_gcc directory somewhere, then modify basecc and build_xgill for the project you are building. build_xgill from the appropriate project directory. Both of these should make a directory with various .xdb databases, e.g. src_body.xdb for all function bodies. For the backend, run these from the .xdb directory: xmemlocal # build memory model for each function xinfer # get assertions to check, infer some loop invariants xcheck -check-kind=kind # check assertions of the specified kind make_index kind # make a directory 'kind' with HTML reports for the specified kind The 'kind' used by xcheck can be 'write_overflow', 'read_overflow', 'annotation', or a few others. This method of running doesn't use any timeouts or failure recovery and is best suited for analyzing small programs. For bigger programs, you can run with recovery and multiple cores: xmonitor /path/to/poll_file 1 xmonitor /path/to/poll_file 2 ... repeat for the number of processes you want to run. these can be on multiple machines, they just need to be able to read the same poll_file via NFS xcomplete /path/to/poll_file /path/to/xdb_dir Brian _______________________________________________ dev-static-analysis mailing list [email protected] https://lists.mozilla.org/listinfo/dev-static-analysis
