ERRORS in concurrency analysis with CPAchecker
65 views
Skip to first unread message
Bcg Vfh
Aug 13, 2023, 3:34:24 AM8/13/23
to CPAchecker Users
Recently, when I use cpachecker to detect dataRace in multi-threaded program, it return some Errors like:
1.Assuming external function pthread_create to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO)
2.Assuming external function pthread_join to be a pure function. (PredicateCPA:ExpressionToFormulaVisitor.visit, INFO)
The config I set is -preprocess -dataRaceAnalysis
The system i use is ubuntu on vmware
Please tell me whether this is a problem and if so what should I do to solve this problem. Thanks for your help！
Martin Spiessl
Aug 22, 2023, 4:00:24 AM8/22/23
to cpacheck...@googlegroups.com
Hi Bcg Vfh,
This is an excellent question! Notice that CPAchecker does not claim this is an error, however it prints these lines in bold to make sure you read them.
For data races, we have dedicated components that handle thread creation and termination, while we have a component called PredicateCPA which
is responsible for tracking the symbolic formula that encodes what the current (abstract) program state looks like.
For the creation of this formula, CPAchecker treats
pthread_create and pthread_join as pure functions, i.e., they do not have any side effects like magically changing some memory or the value of global variables.
This is exactly what one would want here, i.e., this is not really a problem.
The reason we highlight these functions where we assume this is to make sure that the user does not accidentally overlook cases in which external functions
are used in the program that do have side effects (e.g. a user-provided external function, CPAchecker could not possibly know how this function behaves,
so we will assume by default that it is a pure function, which might be unsound. Or put in other words, our analysis is only sound when these assumptions
that CPAchecker prints are indeed correct).
Best,
Martin
--
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 on the web visit https://groups.google.com/d/msgid/cpachecker-users/2a471258-29cf-4c3a-9a3a-17cb0a85d57an%40googlegroups.com.
-- Martin Spiessl Software and Computational Systems Lab LMU Munich, Germany Oettingenstr. 67 Room F012
Bcg Vfh
Sep 8, 2023, 5:11:08 AM9/8/23
to CPAchecker Users
Dear Developer,
Thanks for your answer, which really helps me a lot!
Here I have another question about the command line setting.
As far as I know, the sv-comp uses benchexec as the tool to test and get marks, and benchexec uses as input an XML file that defines the command(s) to execute.
So I look into the XML file used for cpachecker, here is one part of it:
<?xml version="1.0"?>
<!DOCTYPE benchmark PUBLIC "+//IDN sosy-lab.org//DTD BenchExec benchmark 1.9//EN" "https://www.sosy-lab.org/benchexec/benchmark-2.3.dtd">
<benchmark tool="cpachecker" timelimit="15 min" hardtimelimit="16 min" memlimit="15 GB" cpuCores="8">
<require cpuModel="Intel Xeon E3-1230 v5 @ 3.40 GHz"/>
<resultfiles>**/*.graphml</resultfiles>
<option name="-svcomp23"/>
<option name="-heap">10000M</option>
<option name="-benchmark"/>
<option name="-timelimit">900 s</option>
<rundefinition name="SV-COMP23_no-data-race">
<tasks name="NoDataRace-Main">
<includesfile>../sv-benchmarks/c/NoDataRace-Main.set</includesfile>
<propertyfile>../sv-benchmarks/c/properties/no-data-race.prp</propertyfile>
</tasks>
</rundefinition>
I wanna use this config setting in the form of command line in the shell of Ubuntu, but I don't know whether or not I get the right form, here is how I transform:
-svcomp23 -heap 10000M -benchmark - timelimit 900s <file> in ../sv-benchmarks/c/NoDataRace-Main.set
I don't know how to deal with the propertyfile, should I use -spec or something else?
Looking forward to your reply, I would really appreciate it!
Martin Spiessl
Sep 8, 2023, 5:15:10 AM9/8/23
to cpacheck...@googlegroups.com
Hi,
Looks alright, and -spec <path_to_prp_file> is the way to go.
If you are interested, inside benchexec, this is translated from the benchmark definition xml into the CPAchecker command line here:
https://github.com/sosy-lab/benchexec/blob/main/benchexec/tools/cpachecker.py#L93
Best,
Martin
To view this discussion on the web visit https://groups.google.com/d/msgid/cpachecker-users/9a8d2329-8493-4e49-aa10-6e253c814015n%40googlegroups.com.
Bcg Vfh
Sep 13, 2023, 1:22:32 AM9/13/23
to CPAchecker Users
Hi，
Thanks again for your reply，which I really appreciate.
This time I try using benchexec to get the results and hope to make it corresponding to the results realsed on sv-comp.
But after I installed it through PPA:
sudo add-apt-repository ppa:sosy-lab/benchmarking
sudo apt install benchexec
sudo apt install benchexec
and test with:
sudo benchexec /home/lin/Public/sosy-lab-benchexec-2bc3c11/doc/benchmark-example-rand.xml --read-only-dir /
It returned errors:
2023-09-13 13:11:15 - WARNING - Home directory in container should be /home/benchexec but this directory cannot be created due to directory mode of parent directory. It is recommended to use '--overlay-dir /home' or '--hidden-dir /home' and overwrite directory modes for subdirectories where necessary.
2023-09-13 13:11:15 - WARNING - No propertyfile specified. Score computation will ignore the results.
2023-09-13 13:11:15 - INFO - Unable to find pqos_wrapper, please install it for cache allocation and monitoring if your CPU supports Intel RDT (cf. https://gitlab.com/sosy-lab/software/pqos-wrapper).
executing run set (27 files)
2023-09-13 13:11:15 - WARNING - Cgroup subsystem cpuacct is not available. Please make sure it is supported by your kernel and mounted.
2023-09-13 13:11:15 - WARNING - Cannot measure CPU time without cpuacct cgroup.
2023-09-13 13:11:15 - WARNING - Cgroup subsystem freezer is not available. Please make sure it is supported by your kernel and mounted.
2023-09-13 13:11:15 - WARNING - Cgroup subsystem memory is not available. Please make sure it is supported by your kernel and mounted.
2023-09-13 13:11:15 - WARNING - Cannot measure memory consumption without memory cgroup.
2023-09-13 13:11:15 - WARNING - Cgroup subsystem cpuset is not available. Please make sure it is supported by your kernel and mounted.
13:11:15 /home/lin/Public/sosy-lab-benchexec-2bc3c11/doc/benchmark.dtd 2023-09-13 13:11:15 - WARNING - Home directory in container should be /home/benchexec but this directory cannot be created due to directory mode of parent directory. It is recommended to use '--overlay-dir /home' or '--hidden-dir /home' and overwrite directory modes for subdirectories where necessary.
true 0.00
13:11:15 /home/lin/Public/sosy-lab-benchexec-2bc3c11/doc/result.dtd 2023-09-13 13:11:15 - WARNING - Home directory in container should be /home/benchexec but this directory cannot be created due to directory mode of parent directory. It is recommended to use '--overlay-dir /home' or '--hidden-dir /home' and overwrite directory modes for subdirectories where necessary.
true 0.00
13:11:15 /home/lin/Public/sosy-lab-benchexec-2bc3c11/doc/table.dtd 2023-09-13 13:11:15 - WARNING - Home directory in container should be /home/benchexec but this directory cannot be created due to directory mode of parent directory. It is recommended to use '--overlay-dir /home' or '--hidden-dir /home' and overwrite directory modes for subdirectories where necessary.
true 0.00
13:11:15 /home/lin/Public/sosy-lab-benchexec-2bc3c11/doc/DEVELOPMENT.md 2023-09-13 13:11:15 - WARNING - Home directory in container should be /home/benchexec but this directory cannot be created due to directory mode of parent directory. It is recommended to use '--overlay-dir /home' or '--hidden-dir /home' and overwrite directory modes for subdirectories where necessary.
true 0.00
13:11:15 /home/lin/Public/sosy-lab-benchexec-2bc3c11/doc/INDEX.md 2023-09-13 13:11:15 - WARNING - Home directory in container should be /home/benchexec but this directory cannot be created due to directory mode of parent directory. It is recommended to use '--overlay-dir /home' or '--hidden-dir /home' and overwrite directory modes for subdirectories where necessary.
true 0.00
13:11:15 /home/lin/Public/sosy-lab-benchexec-2bc3c11/doc/INSTALL.md 2023-09-13 13:11:15 - WARNING - Home directory in container should be /home/benchexec but this directory cannot be created due to directory mode of parent directory. It is recommended to use '--overlay-dir /home' or '--hidden-dir /home' and overwrite directory modes for subdirectories where necessary.
false(unreach-call) 0.00
13:11:15 /home/lin/Public/sosy-lab-benchexec-2bc3c11/doc/benchexec.md 2023-09-13 13:11:15 - WARNING - Home directory in container should be /home/benchexec but this directory cannot be created due to directory mode of parent directory. It is recommended to use '--overlay-dir /home' or '--hidden-dir /home' and overwrite directory modes for subdirectories where necessary.
true 0.00
13:11:15 /home/lin/Public/sosy-lab-benchexec-2bc3c11/doc/benchmarking.md 2023-09-13 13:11:15 - WARNING - Home directory in container should be /home/benchexec but this directory cannot be created due to directory mode of parent directory. It is recommended to use '--overlay-dir /home' or '--hidden-dir /home' and overwrite directory modes for subdirectories where necessary.
false(unreach-call) 0.00
13:11:15 /home/lin/Public/sosy-lab-benchexec-2bc3c11/doc/container.md 2023-09-13 13:11:15 - WARNING - Home directory in container should be /home/benchexec but this directory cannot be created due to directory mode of parent directory. It is recommended to use '--overlay-dir /home' or '--hidden-dir /home' and overwrite directory modes for subdirectories where necessary.
false(unreach-call) 0.00
13:11:15 /home/lin/Public/sosy-lab-benchexec-2bc3c11/doc/properties.md 2023-09-13 13:11:15 - WARNING - Home directory in container should be /home/benchexec but this directory cannot be created due to directory mode of parent directory. It is recommended to use '--overlay-dir /home' or '--hidden-dir /home' and overwrite directory modes for subdirectories where necessary.
false(unreach-call) 0.00
13:11:15 /home/lin/Public/sosy-lab-benchexec-2bc3c11/doc/resources.md 2023-09-13 13:11:15 - WARNING - Home directory in container should be /home/benchexec but this directory cannot be created due to directory mode of parent directory. It is recommended to use '--overlay-dir /home' or '--hidden-dir /home' and overwrite directory modes for subdirectories where necessary.
false(unreach-call) 0.00
13:11:15 /home/lin/Public/sosy-lab-benchexec-2bc3c11/doc/run-results.md 2023-09-13 13:11:15 - WARNING - Home directory in container should be /home/benchexec but this directory cannot be created due to directory mode of parent directory. It is recommended to use '--overlay-dir /home' or '--hidden-dir /home' and overwrite directory modes for subdirectories where necessary.
true 0.00
13:11:15 /home/lin/Public/sosy-lab-benchexec-2bc3c11/doc/runexec.md 2023-09-13 13:11:15 - WARNING - Home directory in container should be /home/benchexec but this directory cannot be created due to directory mode of parent directory. It is recommended to use '--overlay-dir /home' or '--hidden-dir /home' and overwrite directory modes for subdirectories where necessary.
true 0.00
13:11:15 /home/lin/Public/sosy-lab-benchexec-2bc3c11/doc/table-generator.md 2023-09-13 13:11:15 - WARNING - Home directory in container should be /home/benchexec but this directory cannot be created due to directory mode of parent directory. It is recommended to use '--overlay-dir /home' or '--hidden-dir /home' and overwrite directory modes for subdirectories where necessary.
true 0.00
13:11:15 /home/lin/Public/sosy-lab-benchexec-2bc3c11/doc/tool-integration.md 2023-09-13 13:11:15 - WARNING - Home directory in container should be /home/benchexec but this directory cannot be created due to directory mode of parent directory. It is recommended to use '--overlay-dir /home' or '--hidden-dir /home' and overwrite directory modes for subdirectories where necessary.
true 0.00
13:11:15 /home/lin/Public/sosy-lab-benchexec-2bc3c11/doc/benchmark-example-calculatepi.xml 2023-09-13 13:11:15 - WARNING - Home directory in container should be /home/benchexec but this directory cannot be created due to directory mode of parent directory. It is recommended to use '--overlay-dir /home' or '--hidden-dir /home' and overwrite directory modes for subdirectories where necessary.
false(unreach-call) 0.00
13:11:15 /home/lin/Public/sosy-lab-benchexec-2bc3c11/doc/benchmark-example-cbmc.xml 2023-09-13 13:11:15 - WARNING - Home directory in container should be /home/benchexec but this directory cannot be created due to directory mode of parent directory. It is recommended to use '--overlay-dir /home' or '--hidden-dir /home' and overwrite directory modes for subdirectories where necessary.
true 0.00
13:11:15 /home/lin/Public/sosy-lab-benchexec-2bc3c11/doc/benchmark-example-rand.xml 2023-09-13 13:11:15 - WARNING - Home directory in container should be /home/benchexec but this directory cannot be created due to directory mode of parent directory. It is recommended to use '--overlay-dir /home' or '--hidden-dir /home' and overwrite directory modes for subdirectories where necessary.
false(unreach-call) 0.00
13:11:15 /home/lin/Public/sosy-lab-benchexec-2bc3c11/doc/benchmark-example-true.xml 2023-09-13 13:11:15 - WARNING - Home directory in container should be /home/benchexec but this directory cannot be created due to directory mode of parent directory. It is recommended to use '--overlay-dir /home' or '--hidden-dir /home' and overwrite directory modes for subdirectories where necessary.
false(unreach-call) 0.00
13:11:15 /home/lin/Public/sosy-lab-benchexec-2bc3c11/doc/benchmark.xml 2023-09-13 13:11:15 - WARNING - Home directory in container should be /home/benchexec but this directory cannot be created due to directory mode of parent directory. It is recommended to use '--overlay-dir /home' or '--hidden-dir /home' and overwrite directory modes for subdirectories where necessary.
false(unreach-call) 0.00
13:11:15 /home/lin/Public/sosy-lab-benchexec-2bc3c11/doc/table-generator-basic.xml 2023-09-13 13:11:15 - WARNING - Home directory in container should be /home/benchexec but this directory cannot be created due to directory mode of parent directory. It is recommended to use '--overlay-dir /home' or '--hidden-dir /home' and overwrite directory modes for subdirectories where necessary.
true 0.00
13:11:15 /home/lin/Public/sosy-lab-benchexec-2bc3c11/doc/table-generator-example.xml 2023-09-13 13:11:15 - WARNING - Home directory in container should be /home/benchexec but this directory cannot be created due to directory mode of parent directory. It is recommended to use '--overlay-dir /home' or '--hidden-dir /home' and overwrite directory modes for subdirectories where necessary.
true 0.00
13:11:15 /home/lin/Public/sosy-lab-benchexec-2bc3c11/doc/table-generator.xml 2023-09-13 13:11:15 - WARNING - Home directory in container should be /home/benchexec but this directory cannot be created due to directory mode of parent directory. It is recommended to use '--overlay-dir /home' or '--hidden-dir /home' and overwrite directory modes for subdirectories where necessary.
false(unreach-call) 0.00
13:11:15 /home/lin/Public/sosy-lab-benchexec-2bc3c11/doc/task-definition-example.yml 2023-09-13 13:11:15 - WARNING - Home directory in container should be /home/benchexec but this directory cannot be created due to directory mode of parent directory. It is recommended to use '--overlay-dir /home' or '--hidden-dir /home' and overwrite directory modes for subdirectories where necessary.
true 0.00
13:11:15 dummy task 1 2023-09-13 13:11:15 - WARNING - Home directory in container should be /home/benchexec but this directory cannot be created due to directory mode of parent directory. It is recommended to use '--overlay-dir /home' or '--hidden-dir /home' and overwrite directory modes for subdirectories where necessary.
false(unreach-call) 0.00
13:11:15 dummy task 2 2023-09-13 13:11:15 - WARNING - Home directory in container should be /home/benchexec but this directory cannot be created due to directory mode of parent directory. It is recommended to use '--overlay-dir /home' or '--hidden-dir /home' and overwrite directory modes for subdirectories where necessary.
true 0.00
13:11:15 dummy task 3 2023-09-13 13:11:15 - WARNING - Home directory in container should be /home/benchexec but this directory cannot be created due to directory mode of parent directory. It is recommended to use '--overlay-dir /home' or '--hidden-dir /home' and overwrite directory modes for subdirectories where necessary.
false(unreach-call) 0.00
Statistics: 27 Files
correct: 0
correct true: 0
correct false: 0
incorrect: 0
incorrect true: 0
incorrect false: 0
unknown: 0
In order to get HTML and CSV tables, run
table-generator results/benchmark-example-rand.2023-09-13_13-11-15.results.xml.bz2
2023-09-13 13:11:15 - WARNING - No propertyfile specified. Score computation will ignore the results.
2023-09-13 13:11:15 - INFO - Unable to find pqos_wrapper, please install it for cache allocation and monitoring if your CPU supports Intel RDT (cf. https://gitlab.com/sosy-lab/software/pqos-wrapper).
executing run set (27 files)
2023-09-13 13:11:15 - WARNING - Cgroup subsystem cpuacct is not available. Please make sure it is supported by your kernel and mounted.
2023-09-13 13:11:15 - WARNING - Cannot measure CPU time without cpuacct cgroup.
2023-09-13 13:11:15 - WARNING - Cgroup subsystem freezer is not available. Please make sure it is supported by your kernel and mounted.
2023-09-13 13:11:15 - WARNING - Cgroup subsystem memory is not available. Please make sure it is supported by your kernel and mounted.
2023-09-13 13:11:15 - WARNING - Cannot measure memory consumption without memory cgroup.
2023-09-13 13:11:15 - WARNING - Cgroup subsystem cpuset is not available. Please make sure it is supported by your kernel and mounted.
13:11:15 /home/lin/Public/sosy-lab-benchexec-2bc3c11/doc/benchmark.dtd 2023-09-13 13:11:15 - WARNING - Home directory in container should be /home/benchexec but this directory cannot be created due to directory mode of parent directory. It is recommended to use '--overlay-dir /home' or '--hidden-dir /home' and overwrite directory modes for subdirectories where necessary.
true 0.00
13:11:15 /home/lin/Public/sosy-lab-benchexec-2bc3c11/doc/result.dtd 2023-09-13 13:11:15 - WARNING - Home directory in container should be /home/benchexec but this directory cannot be created due to directory mode of parent directory. It is recommended to use '--overlay-dir /home' or '--hidden-dir /home' and overwrite directory modes for subdirectories where necessary.
true 0.00
13:11:15 /home/lin/Public/sosy-lab-benchexec-2bc3c11/doc/table.dtd 2023-09-13 13:11:15 - WARNING - Home directory in container should be /home/benchexec but this directory cannot be created due to directory mode of parent directory. It is recommended to use '--overlay-dir /home' or '--hidden-dir /home' and overwrite directory modes for subdirectories where necessary.
true 0.00
13:11:15 /home/lin/Public/sosy-lab-benchexec-2bc3c11/doc/DEVELOPMENT.md 2023-09-13 13:11:15 - WARNING - Home directory in container should be /home/benchexec but this directory cannot be created due to directory mode of parent directory. It is recommended to use '--overlay-dir /home' or '--hidden-dir /home' and overwrite directory modes for subdirectories where necessary.
true 0.00
13:11:15 /home/lin/Public/sosy-lab-benchexec-2bc3c11/doc/INDEX.md 2023-09-13 13:11:15 - WARNING - Home directory in container should be /home/benchexec but this directory cannot be created due to directory mode of parent directory. It is recommended to use '--overlay-dir /home' or '--hidden-dir /home' and overwrite directory modes for subdirectories where necessary.
true 0.00
13:11:15 /home/lin/Public/sosy-lab-benchexec-2bc3c11/doc/INSTALL.md 2023-09-13 13:11:15 - WARNING - Home directory in container should be /home/benchexec but this directory cannot be created due to directory mode of parent directory. It is recommended to use '--overlay-dir /home' or '--hidden-dir /home' and overwrite directory modes for subdirectories where necessary.
false(unreach-call) 0.00
13:11:15 /home/lin/Public/sosy-lab-benchexec-2bc3c11/doc/benchexec.md 2023-09-13 13:11:15 - WARNING - Home directory in container should be /home/benchexec but this directory cannot be created due to directory mode of parent directory. It is recommended to use '--overlay-dir /home' or '--hidden-dir /home' and overwrite directory modes for subdirectories where necessary.
true 0.00
13:11:15 /home/lin/Public/sosy-lab-benchexec-2bc3c11/doc/benchmarking.md 2023-09-13 13:11:15 - WARNING - Home directory in container should be /home/benchexec but this directory cannot be created due to directory mode of parent directory. It is recommended to use '--overlay-dir /home' or '--hidden-dir /home' and overwrite directory modes for subdirectories where necessary.
false(unreach-call) 0.00
13:11:15 /home/lin/Public/sosy-lab-benchexec-2bc3c11/doc/container.md 2023-09-13 13:11:15 - WARNING - Home directory in container should be /home/benchexec but this directory cannot be created due to directory mode of parent directory. It is recommended to use '--overlay-dir /home' or '--hidden-dir /home' and overwrite directory modes for subdirectories where necessary.
false(unreach-call) 0.00
13:11:15 /home/lin/Public/sosy-lab-benchexec-2bc3c11/doc/properties.md 2023-09-13 13:11:15 - WARNING - Home directory in container should be /home/benchexec but this directory cannot be created due to directory mode of parent directory. It is recommended to use '--overlay-dir /home' or '--hidden-dir /home' and overwrite directory modes for subdirectories where necessary.
false(unreach-call) 0.00
13:11:15 /home/lin/Public/sosy-lab-benchexec-2bc3c11/doc/resources.md 2023-09-13 13:11:15 - WARNING - Home directory in container should be /home/benchexec but this directory cannot be created due to directory mode of parent directory. It is recommended to use '--overlay-dir /home' or '--hidden-dir /home' and overwrite directory modes for subdirectories where necessary.
false(unreach-call) 0.00
13:11:15 /home/lin/Public/sosy-lab-benchexec-2bc3c11/doc/run-results.md 2023-09-13 13:11:15 - WARNING - Home directory in container should be /home/benchexec but this directory cannot be created due to directory mode of parent directory. It is recommended to use '--overlay-dir /home' or '--hidden-dir /home' and overwrite directory modes for subdirectories where necessary.
true 0.00
13:11:15 /home/lin/Public/sosy-lab-benchexec-2bc3c11/doc/runexec.md 2023-09-13 13:11:15 - WARNING - Home directory in container should be /home/benchexec but this directory cannot be created due to directory mode of parent directory. It is recommended to use '--overlay-dir /home' or '--hidden-dir /home' and overwrite directory modes for subdirectories where necessary.
true 0.00
13:11:15 /home/lin/Public/sosy-lab-benchexec-2bc3c11/doc/table-generator.md 2023-09-13 13:11:15 - WARNING - Home directory in container should be /home/benchexec but this directory cannot be created due to directory mode of parent directory. It is recommended to use '--overlay-dir /home' or '--hidden-dir /home' and overwrite directory modes for subdirectories where necessary.
true 0.00
13:11:15 /home/lin/Public/sosy-lab-benchexec-2bc3c11/doc/tool-integration.md 2023-09-13 13:11:15 - WARNING - Home directory in container should be /home/benchexec but this directory cannot be created due to directory mode of parent directory. It is recommended to use '--overlay-dir /home' or '--hidden-dir /home' and overwrite directory modes for subdirectories where necessary.
true 0.00
13:11:15 /home/lin/Public/sosy-lab-benchexec-2bc3c11/doc/benchmark-example-calculatepi.xml 2023-09-13 13:11:15 - WARNING - Home directory in container should be /home/benchexec but this directory cannot be created due to directory mode of parent directory. It is recommended to use '--overlay-dir /home' or '--hidden-dir /home' and overwrite directory modes for subdirectories where necessary.
false(unreach-call) 0.00
13:11:15 /home/lin/Public/sosy-lab-benchexec-2bc3c11/doc/benchmark-example-cbmc.xml 2023-09-13 13:11:15 - WARNING - Home directory in container should be /home/benchexec but this directory cannot be created due to directory mode of parent directory. It is recommended to use '--overlay-dir /home' or '--hidden-dir /home' and overwrite directory modes for subdirectories where necessary.
true 0.00
13:11:15 /home/lin/Public/sosy-lab-benchexec-2bc3c11/doc/benchmark-example-rand.xml 2023-09-13 13:11:15 - WARNING - Home directory in container should be /home/benchexec but this directory cannot be created due to directory mode of parent directory. It is recommended to use '--overlay-dir /home' or '--hidden-dir /home' and overwrite directory modes for subdirectories where necessary.
false(unreach-call) 0.00
13:11:15 /home/lin/Public/sosy-lab-benchexec-2bc3c11/doc/benchmark-example-true.xml 2023-09-13 13:11:15 - WARNING - Home directory in container should be /home/benchexec but this directory cannot be created due to directory mode of parent directory. It is recommended to use '--overlay-dir /home' or '--hidden-dir /home' and overwrite directory modes for subdirectories where necessary.
false(unreach-call) 0.00
13:11:15 /home/lin/Public/sosy-lab-benchexec-2bc3c11/doc/benchmark.xml 2023-09-13 13:11:15 - WARNING - Home directory in container should be /home/benchexec but this directory cannot be created due to directory mode of parent directory. It is recommended to use '--overlay-dir /home' or '--hidden-dir /home' and overwrite directory modes for subdirectories where necessary.
false(unreach-call) 0.00
13:11:15 /home/lin/Public/sosy-lab-benchexec-2bc3c11/doc/table-generator-basic.xml 2023-09-13 13:11:15 - WARNING - Home directory in container should be /home/benchexec but this directory cannot be created due to directory mode of parent directory. It is recommended to use '--overlay-dir /home' or '--hidden-dir /home' and overwrite directory modes for subdirectories where necessary.
true 0.00
13:11:15 /home/lin/Public/sosy-lab-benchexec-2bc3c11/doc/table-generator-example.xml 2023-09-13 13:11:15 - WARNING - Home directory in container should be /home/benchexec but this directory cannot be created due to directory mode of parent directory. It is recommended to use '--overlay-dir /home' or '--hidden-dir /home' and overwrite directory modes for subdirectories where necessary.
true 0.00
13:11:15 /home/lin/Public/sosy-lab-benchexec-2bc3c11/doc/table-generator.xml 2023-09-13 13:11:15 - WARNING - Home directory in container should be /home/benchexec but this directory cannot be created due to directory mode of parent directory. It is recommended to use '--overlay-dir /home' or '--hidden-dir /home' and overwrite directory modes for subdirectories where necessary.
false(unreach-call) 0.00
13:11:15 /home/lin/Public/sosy-lab-benchexec-2bc3c11/doc/task-definition-example.yml 2023-09-13 13:11:15 - WARNING - Home directory in container should be /home/benchexec but this directory cannot be created due to directory mode of parent directory. It is recommended to use '--overlay-dir /home' or '--hidden-dir /home' and overwrite directory modes for subdirectories where necessary.
true 0.00
13:11:15 dummy task 1 2023-09-13 13:11:15 - WARNING - Home directory in container should be /home/benchexec but this directory cannot be created due to directory mode of parent directory. It is recommended to use '--overlay-dir /home' or '--hidden-dir /home' and overwrite directory modes for subdirectories where necessary.
false(unreach-call) 0.00
13:11:15 dummy task 2 2023-09-13 13:11:15 - WARNING - Home directory in container should be /home/benchexec but this directory cannot be created due to directory mode of parent directory. It is recommended to use '--overlay-dir /home' or '--hidden-dir /home' and overwrite directory modes for subdirectories where necessary.
true 0.00
13:11:15 dummy task 3 2023-09-13 13:11:15 - WARNING - Home directory in container should be /home/benchexec but this directory cannot be created due to directory mode of parent directory. It is recommended to use '--overlay-dir /home' or '--hidden-dir /home' and overwrite directory modes for subdirectories where necessary.
false(unreach-call) 0.00
Statistics: 27 Files
correct: 0
correct true: 0
correct false: 0
incorrect: 0
incorrect true: 0
incorrect false: 0
unknown: 0
In order to get HTML and CSV tables, run
table-generator results/benchmark-example-rand.2023-09-13_13-11-15.results.xml.bz2
The system I use is :
Linux version 6.2.0-26-generic (buildd@bos03-amd64-042) (x86_64-linux-gnu-gcc-11 (Ubuntu 11.3.0-1ubuntu1~22.04.1) 11.3.0, GNU ld (GNU Binutils for Ubuntu) 2.38) #26~22.04.1-Ubuntu SMP PREEMPT_DYNAMIC Thu Jul 13 16:27:29 UTC 2 on VmWare
I will really appreciate it if you can solve my problem.
Philipp Wendler
Sep 13, 2023, 5:39:38 AM9/13/23
to cpacheck...@googlegroups.com
Hi,
Am 13.09.23 um 07:22 schrieb Bcg Vfh:
> *sudo add-apt-repository ppa:sosy-lab/benchmarkingsudo apt install
> benchexec*
>
> and test with:
>
> *sudo benchexec
> /home/lin/Public/sosy-lab-benchexec-2bc3c11/doc/benchmark-example-rand.xml
> --read-only-dir /*
>
> It returned errors:
> [...]
The log you attached did not show any errors, just warnings, and the
tool was executed. If you want to use cgroups, follow the installation
instructions for BenchExec:
https://github.com/sosy-lab/benchexec/blob/main/doc/INSTALL.md
For any general problems with BenchExec, please use the BenchExec issue
tracker, not the CPAchecker mailing list:
https://github.com/sosy-lab/benchexec/issues
Greetings
Philipp
--
Philipp Wendler
Am 13.09.23 um 07:22 schrieb Bcg Vfh:
> *sudo add-apt-repository ppa:sosy-lab/benchmarkingsudo apt install
> benchexec*
>
> and test with:
>
> *sudo benchexec
> /home/lin/Public/sosy-lab-benchexec-2bc3c11/doc/benchmark-example-rand.xml
> --read-only-dir /*
>
> It returned errors:
> [...]
The log you attached did not show any errors, just warnings, and the
tool was executed. If you want to use cgroups, follow the installation
instructions for BenchExec:
https://github.com/sosy-lab/benchexec/blob/main/doc/INSTALL.md
For any general problems with BenchExec, please use the BenchExec issue
tracker, not the CPAchecker mailing list:
https://github.com/sosy-lab/benchexec/issues
Greetings
Philipp
--
Philipp Wendler
Software and Computational Systems Lab
LMU Munich, Germany
Oettingenstr. 67 Raum F008 - Tel.: 089/2180-9181
LMU Munich, Germany
Reply all
Reply to author
Forward
0 new messages