Some problem when I use <spec file> in CPAchecker

[Liangchen]

Dear developers,

     I try to use CPAchecker to do static analyse, and then use it to perform formal verification, such as I hope to perform verification with properties file and get CFA and SDG at the same time.

    I use command "./cpa.sh -generateSlice -setprop dependencegraph.controldeps.considerInverseAssumption=false '/home/kali/Desktop/a.c' -spec /home/kali/Downloads/CPAchecker-2.2-unix/config/properties/unreach-call.prp", but it didn't give me a correct result, the output file is in the attachment.

   I wonder how to solve this problem?

                                                                                                                                        Yours,

                                                                                                                                        Liangchen

[Liangchen]

Sorry, attachment is wrong, here is the correct one.

[Philipp Wendler]

Dear Liangchen,

Am 19.08.23 um 04:52 schrieb Liangchen:

> I try to use CPAchecker to do static analyse, and then use it to
> perform formal verification, such as I hope to perform verification with
> properties file and get CFA and SDG at the same time.
> I use command "./cpa.sh -generateSlice -setprop
> dependencegraph.controldeps.considerInverseAssumption=false
> '/home/kali/Desktop/a.c' -spec
> /home/kali/Downloads/CPAchecker-2.2-unix/config/properties/unreach-call.prp",
> but it didn't give me a correct result, the output file is in the
> attachment.

If CPAchecker aborts with a stacktrace, it is a bug in CPAchecker.
For reproducing it, however, we would need the input file that you used.
You are invited to report this bug here:
https://gitlab.com/sosy-lab/software/cpachecker/-/issues/new

I suspect the bug is likely triggered by the fact that you used
undefined functions in your code.
In general, I would recommend to provide extern declarations for all
functions, because C rules on undefined functions are not useful.

Greetings
Philipp

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