Using CPAChecker

[Aviral Kumar]

Hi, 

I am a beginner in the field of Program Verification and I am using CPAChecker for the first time. So, I apologize for any stupid questions which I ask. 

I am trying to verify xv6 (OS built by MIT) file system module. My code is attached below. The CPA checker evaluates to false, and gives a counter example, although it is not a true one. How should I proceed now, should I add new predicates and how?

Thanks,

Aviral

[Rodrigo Castaño]

Hi Aviral,

You might want to add which configuration you used (UsedConfiguration.properties within the output folder) and the counterexample you're getting. Also, if you figured out it's a spurious counterexample and pinpointed what exactly is wrong with it, that'd also help.

Best,

Rodrigo.

[Aviral Kumar]

Hi Rodrigo,

Thanks for replying.  I am using the predicate configuration file the default one, which comes with the downloaded tar of CPAchecker.  I can't figure out why it's a spurious counterexample. I will post the countered ample shortly.

Thanks
Aviral

--
You received this message because you are subscribed to a topic in the Google Groups "CPAchecker Users" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/cpachecker-users/_ECwQVnTIS4/unsubscribe.
To unsubscribe from this group and all its topics, send an email to cpachecker-users+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[Aviral Kumar]

Please find the counterexample file attached. Also, i don't understand how to interpret the counterexample.c file . Please explain that to me.

Thanks

Aviral

To unsubscribe from this group and all its topics, send an email to cpachecker-use...@googlegroups.com.

[Philipp Wendler]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

Hello Aviral,

Am 18.11.2016 um 17:57 schrieb Aviral Kumar:
> I am a beginner in the field of Program Verification and I am
> using CPAChecker for the first time. So, I apologize for any
> stupid questions which I ask.

Thank you for your interest in CPAchecker!
This is certainly not a stupid question.

> I am trying to verify xv6 (OS built by MIT) file system module. My
> code is attached below. The CPA checker evaluates to false, and
> gives a counter example, although it is not a true one. How should
> I proceed now, should I add new predicates and how?

No, new predicates won't help, because CPAchecker finds predicates
automatically if necessary.

It could be that the chosen configuration is too imprecise, although
we double-check all found counterexamples with a quite precise analysis.

The way to investigate this situation is to look at the various files
CPAchecker dumps for each counterexample.
For example, Counterexample.c contains C code that represents only
the one path through the original program which is the counterexample
(with additional assumptions about variables added).

An alternative is to look at our interactive HTML-based report
by running scripts/report-generator.py (this is probably the most
useful visualization of counterexamples).

If you are convinced that the counterexample is an invalid one, i.e.,
the given path is infeasible, there has to be a contradiction in this
path that you need to find.
Once such a contradiction is identified, we can investigate whether
CPAchecker did not detect it.

In the counterexample you got, for example, there is a contradiction:
- - iget_1 is called with devi == 23
- - __CPROVER_assume((ip->dev) == devi);
- - iget_1 returns the value of ip
- - main_0 assigns the return value to ipt
- - __CPROVER_assume((ipt->dev) != 23);

This is interesting, because CPAchecker's predicate analysis should
have no problems detecting this kind of contradiction, and thus
should not have returned this counterexample.

In fact, when I run

scripts/cpa.sh -predicateAnalysis tester.c \
-spec sv-comp-reachability -preprocess

for a few minutes at least I do not get your counterexample
(though I did not run it until completion).

So please provide more details:
What version of CPAchecker you are using?
What was the exact command line?

Please always provide this information.

Thank you,
Philipp

- --
Philipp Wendler
Software and Computational Systems Lab
LMU Munich, Germany
Oettingenstr. 67 Raum F 008 - Tel.: 089/2180-9181
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v2.0.22 (GNU/Linux)

iQIcBAEBAgAGBQJYMCYxAAoJEGLA94wxqd6MvEEQANTUlq0aIquol9s0i6ISgSA0
QdJiPTXnft1rLjQ+ZILlW2/mfBtOOyC/bXdQcaqxZSAiEDKtqMEEt5Ix4xthUzW0
f7aW6khOmes7HPphP6paYo5YQUc0ES2lQOJvmA1laC6619VqORVBiIeD9N137i31
Hi/yjuTJGSSs2qXpx+LA7vvKvVCufDewzaw8/KVEdKrTFTWlwDOm0nxo+Tw/7r9t
/q79o/tIXRfwzZSTRzeZLcYsn/l4ErVCgUL7RQhLVtaUfb9HBuqfnkPDeU/IJUQy
pcex8niD4+Hm9wILaUrrBPPidmAcHSSVmWd1694JKZUHa2SJTqGImaNOoM4b333u
Jcv/FQkxLQEUepjL2+yomFUehUZeVwWm3e0/R09tZX53fQEytVThnBTD2zt3CNLa
ok0C9XQTO+UMDECwg/AmdOnRvPMevo4oHoZ9wwedjjnY8ImOtxqSnY9tG6n3TxNY
5phbwMmprKCahEu9Tb25jp8RJ3qYFz27imFLfMXuMHF7TjlEarZD6Abhhy+YmUte
pLa/GKS0VVZKpDIx/EtVg1o+XhdrYFpCK3h5HdGH7lWth579Joj5C4IQY6HjbkgH
cNMDT6hQHo0b9GGKm2ccZbGHA4F6otNkdMtV0RmJoBlbnYxAGAFVH96bgOeLgYff
p9WjXjLI8eNtYmLQBDDj
=6JU3
-----END PGP SIGNATURE-----