search

ultimate-pa / ultimate

The Ultimate program analysis framework.
https://ultimate-pa.org/
200 stars 41 forks source link

Can this tool used in a real world project? #612

Closed ConfZ closed 1 year ago

ConfZ commented 1 year ago

Hi, I'd like to checking the non-termination of my real world project. Could please give me some advise to make it work on the hole project?

danieldietsch commented 1 year ago

Can you be more specific? What kind of project are you working on? You added ReqAnalyzer as label, but ReqAnalyzer is a tool that analyses requirements. I am not sure what non-termination is in this context.

ConfZ commented 1 year ago

Can you be more specific? What kind of project are you working on? You added ReqAnalyzer as label, but ReqAnalyzer is a tool that analyses requirements. I am not sure what non-termination is in this context.

Im sorry for the wrong label... I am working on a C/C++ project, and as I know UAutomizer can work very well on SV-comp benchmark. However, I'd like to check the non-termination of a C++ project with about 50 C/C++ files rather than the code snippets, and I'm not sure if it can work. Shall I slice the code or input the single file to UAutomizer? Thanks!

Heizmann commented 1 year ago

We do support only C but not C++. If you preprocess your project and put everything into one file (e.g., by gcc) Ultimate Automizer should work on this file. I can't remember the status of our support for taking a project as input. Maybe @danieldietsch can comment on that.

danieldietsch commented 1 year ago

Unfortunately, even a C project cannot be used as input at the moment.

ConfZ commented 1 year ago

Unfortunately, even a C project cannot be used as input at the moment.

What a pity, and still thanks for your reply. I have no other questions.