search

diffblue / 2ls

Static Analyzer and Verifier
http://www.cprover.org/2LS
Other
43 stars 22 forks source link

Can 2ls work on a real world project? #174

Closed ConfZ closed 1 year ago

ConfZ commented 1 year ago

Hi, we are ready to make a testing on a real world project by some tools. Could you please give me some advise to make 2ls work on a project? Thanks!

peterschrammel commented 1 year ago

2LS uses the same infrastructure as CBMC. So, you can use goto-cc for compiling and linking the project into goto-binaries (CBMC's intermediate language).

2LS has similar restrictions wrt scalability as other model checkers. It's more likely to be successful for unit verification (cf. unit testing) rather than running it on the program's entry point. 2LS has lots of options for various types of analyses and degrees of precision.

What kind of properties do you want to check?

ConfZ commented 1 year ago

2LS uses the same infrastructure as CBMC. So, you can use goto-cc for compiling and linking the project into goto-binaries (CBMC's intermediate language).

2LS has similar restrictions wrt scalability as other model checkers. It's more likely to be successful for unit verification (cf. unit testing) rather than running it on the program's entry point. 2LS has lots of options for various types of analyses and degrees of precision.

What kind of properties do you want to check?

I'd like to check the non-termination of projects since they could have infinite loops or recursions. While these projects are consisted of 20 - 50 files rather than a single file, and I am not sure if 2LS can work. Your advise seems to be helpful. Two more questions, Which option should I use to deal with goto-binaries and wrt? If it can make unit test on non-termination property? Thanks!