Question Regarding Reporting Multiple Bugs in CPAchecker

[Edgar Khachatryan]

Dear CPAchecker team,

My name is Edgar Khachatryan, and I am a student currently working on a project that involves static analysis using CPAchecker.

While analyzing simple test cases, I noticed that CPAchecker stops the analysis after detecting the first bug and reports only that issue. I would like to ask if there is a way to configure CPAchecker to continue the analysis and report multiple bugs in a single run?

If this is possible, could you please provide guidance or point me to relevant documentation on how to enable this behavior?

Thank you very much for your time and assistance! I look forward to your response.

Best regards,

Edgar Khachatryan,

Russian-Armenian University

[Philipp Wendler]

Dear Edgar,

thanks for your interest in CPAchecker!

Am 11.03.25 um 16:29 schrieb Edgar Khachatryan:

>
> While analyzing simple test cases, I noticed that CPAchecker stops the
> analysis after detecting the first bug and reports only that issue. I would
> like to ask if there is a way to configure CPAchecker to continue the
> analysis and report multiple bugs in a single run?

Yes, most configuration should do this if the option
analysis.stopAfterError=false
is set.

However, note that this may result in many counterexamples that are
highly similar, for example differ only in the number of loop
unrollings, or some small part of their paths, or even just in variable
values.
We have some heuristics that can be chosen for filtering out redundant
counterexamples with the option counterexample.export.filters.
But I have to note that I am not sure if anyone has used this in the
last years.

Greetings
Philipp
--
Philipp Wendler
Software and Computational Systems Lab
LMU Munich, Germany
Oettingenstr. 67 Raum F008 - Tel.: 089/2180-9181

[Edgar Khachatryan]

Dear Philipp,

Thank you very much for your quick response and for clarifying the use of the option to enable reporting multiple bugs.

I tried running CPAchecker with this option, but unfortunately, it keeps crashing during analysis and does not produce any report.

To help you better understand the issue, I have have attached to this email:

• The full command-line call I used to run CPAchecker with the output showing the crash,
• The C source file I used as input for the analysis,
• The output directory (compressed).

Could you please take a look and let me know if I might be missing something in the configuration or if this could be a known issue?

Thank you again for your time and support!

Best regards,
Edgar Khachatryan,

Russian-Armenian University

--
You received this message because you are subscribed to the Google Groups "CPAchecker Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to cpachecker-use...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/cpachecker-users/508b29b7-9ee7-41ee-8039-cb2a000ac902%40philippwendler.de.

[Philipp Wendler]

Dear Edgar,

Am 12.03.25 um 12:05 schrieb Edgar Khachatryan:

> I tried running CPAchecker with this option, but unfortunately, it keeps
> crashing during analysis and does not produce any report.

Thanks for reporting.

In this case, the reason is that the default configuration of CPAchecker
is a meta analysis that uses techniques like strategy selection and
parallel portfolio to start one or more actual analyses depending on the
program and the property.
I was not aware that this does not work with stopAfterError=false, and
we do not have a quick fix for this.

The best way out of this is to select and use a single analysis. For
memory safety we recommend the one based on symbolic memory graphs
(SMGs). You can select it with "--smg --spec memorysafety".

However, I noticed it triggers an assertion failure in CPAchecker that
is currently under investigation:
https://gitlab.com/sosy-lab/software/cpachecker/-/issues/598

You can temporarily disable internal assertions as a workaround, but you
would have to use the latest development version of CPAchecker for this
(from the git repository).
Then the following command line is what I recommend:

bin/cpachecker --preprocess manybugs.c \
--smg --spec memorysafety --disable-java-assertions \
--option analysis.stopAfterError=false

I just want to let you know that if you have any questions that are
specific to the SMG analysis, my colleague Daniel knows more about this,
but he is currently on vacation so an answer might take more time.

[Edgar Khachatryan]

Dear Philipp,

Thank you so much for your helpful guidance on using the --smg --spec memorysafety option and the workaround for disabling assertions. I really appreciate your support!

I had initially wanted CPAchecker to continue the analysis after the first CWE was found because I was interested in seeing if it could identify specific CWE types, such as memory leaks, in a file that contains multiple CWEs (e.g., double free or use after free). However, when I modified the memsafety.prp file to include only one property specification (e.g., CHECK( init(main()), LTL(G valid-memtrack) )), I still see that other property specifications (e.g., CHECK( init(main()), LTL(G valid-deref) ) and CHECK( init(main()), LTL(G valid-free) )) are being reported as well.

Is there a way to disable other property specifications and enable only one specific property specification for the analysis?

Thank you again for your kind help!

Best regards,
Edgar Khachatryan,
Russian-Armenian University

--
You received this message because you are subscribed to the Google Groups "CPAchecker Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to cpachecker-use...@googlegroups.com.

To view this discussion visit https://groups.google.com/d/msgid/cpachecker-users/d663e6a6-a682-499e-8112-13a33a7799cf%40philippwendler.de.

[Daniel Baier]

Hi Edgar,

the problem with the SMG analysis is that it is tuned for the MemorySafety category that contains all 3.

My guess is that the check for the sub-property is accidentally reporting for all 3 if one is specified.

Could you maybe file a issue with steps to reproduce your problem?

Then i can investigate it fully and fix it.

Best,

Daniel

[Edgar Khachatryan]

Dear Daniel,

Thank you for the clarification.

I have now created an issue with detailed steps to reproduce the problem, along with the manybugs.c file attached. 

You can find the issue here: https://gitlab.com/sosy-lab/software/cpachecker/-/issues/1336

Please let me know if any further information is needed.

Best regards,
Edgar Khachatryan,
Russian-Armenian University

--

You received this message because you are subscribed to the Google Groups "CPAchecker Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to cpachecker-use...@googlegroups.com.

To view this discussion visit https://groups.google.com/d/msgid/cpachecker-users/CALbnJVqH-EzduoKcCPmD8FhwnxQKHaaGYqQVPCoq77HCoR5kAA%40mail.gmail.com.