Path: . Working Copy Root Path: /usa/svn/work/civl/1.21/r5476 URL: svn://vsl.cis.udel.edu/civl/trunk Relative URL: ^/trunk Repository Root: svn://vsl.cis.udel.edu/civl Repository UUID: fb995dde-84ed-4084-dfe6-e5aef3e2452c Revision: 5476 Node Kind: directory Schedule: normal Last Changed Author: wuwenhao Last Changed Rev: 5476 Last Changed Date: 2021-11-04 11:35:21 -0400 (Thu, 04 Nov 2021)
Stdout:
Buildfile: /usa/svn/work/civl/1.21/r5476/build.xml
checkCommandParserChanges:
CommandParser:
[move] Moving 1 file to /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/run/common
[move] Moving 1 file to /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/run/common
[move] Moving 1 file to /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/run/common
[move] Moving 1 file to /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/run/common
compile:
[mkdir] Created dir: /usa/svn/work/civl/1.21/r5476/bin
[javac] Compiling 515 source files to /usa/svn/work/civl/1.21/r5476/bin
[javac] Creating empty /usa/svn/work/civl/1.21/r5476/bin/edu/udel/cis/vsl/civl/model/IF/expression/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.21/r5476/bin/edu/udel/cis/vsl/civl/state/IF/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.21/r5476/bin/edu/udel/cis/vsl/civl/semantics/IF/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.21/r5476/bin/edu/udel/cis/vsl/civl/kripke/IF/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.21/r5476/bin/edu/udel/cis/vsl/civl/util/IF/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.21/r5476/bin/edu/udel/cis/vsl/civl/library/domain/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.21/r5476/bin/edu/udel/cis/vsl/civl/model/IF/type/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.21/r5476/bin/edu/udel/cis/vsl/civl/library/comm/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.21/r5476/bin/edu/udel/cis/vsl/civl/library/pointer/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.21/r5476/bin/edu/udel/cis/vsl/civl/model/IF/location/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.21/r5476/bin/edu/udel/cis/vsl/civl/library/time/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.21/r5476/bin/edu/udel/cis/vsl/civl/library/pthread/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.21/r5476/bin/edu/udel/cis/vsl/civl/config/IF/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.21/r5476/bin/edu/udel/cis/vsl/civl/dynamic/IF/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.21/r5476/bin/edu/udel/cis/vsl/civl/library/civlc/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.21/r5476/bin/edu/udel/cis/vsl/civl/log/IF/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.21/r5476/bin/edu/udel/cis/vsl/civl/library/common/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.21/r5476/bin/edu/udel/cis/vsl/civl/model/IF/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.21/r5476/bin/edu/udel/cis/vsl/civl/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.21/r5476/bin/edu/udel/cis/vsl/civl/model/IF/variable/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.21/r5476/bin/edu/udel/cis/vsl/civl/library/seq/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.21/r5476/bin/edu/udel/cis/vsl/civl/library/string/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.21/r5476/bin/edu/udel/cis/vsl/civl/analysis/IF/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.21/r5476/bin/edu/udel/cis/vsl/civl/library/scope/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.21/r5476/bin/edu/udel/cis/vsl/civl/model/IF/statement/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.21/r5476/bin/edu/udel/cis/vsl/civl/predicate/IF/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.21/r5476/bin/edu/udel/cis/vsl/civl/library/bundle/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.21/r5476/bin/edu/udel/cis/vsl/civl/slice/common/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.21/r5476/bin/edu/udel/cis/vsl/civl/slice/IF/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.21/r5476/bin/edu/udel/cis/vsl/civl/run/IF/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.21/r5476/bin/edu/udel/cis/vsl/civl/transform/IF/package-info.class
[copy] Copying 33 files to /usa/svn/work/civl/1.21/r5476/bin/include
jar:
[jar] Building jar: /usa/svn/work/civl/1.21/r5476/civl.jar
test-init:
[mkdir] Created dir: /usa/svn/work/civl/1.21/r5476/junit
[mkdir] Created dir: /usa/svn/work/civl/1.21/r5476/junit/data
[mkdir] Created dir: /usa/svn/work/civl/1.21/r5476/junit/reports
[mkdir] Created dir: /usa/svn/work/civl/1.21/r5476/bin-test/regress
test-compile:
[javac] Compiling 47 source files to /usa/svn/work/civl/1.21/r5476/bin-test/regress
test-run:
[jacoco:coverage] Enhancing junit with coverage
[junit] Testsuite: edu.udel.cis.vsl.civl.BackendTest
[junit] Testsuite: edu.udel.cis.vsl.civl.LanguageFeaturesTest
[junit] Testsuite: edu.udel.cis.vsl.civl.ArrayLambdaTest
[junit] Testsuite: edu.udel.cis.vsl.civl.AnalysisTest
[junit] Testsuite: edu.udel.cis.vsl.civl.AcfInterfaceTest
[junit] Testsuite: edu.udel.cis.vsl.civl.ConcurrencyTest
[junit] Testsuite: edu.udel.cis.vsl.civl.ArithmeticTest
[junit] Testsuite: edu.udel.cis.vsl.civl.CompareTest
[junit] Tests run: 4, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 11.04 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.LibraryTest
[junit] Tests run: 2, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 15.614 sec
[junit]
[junit] ------------- Standard Output ---------------
[junit] CIVL v1.21 of 2021-11-04 -- http://vsl.cis.udel.edu/civl
[junit] CIVL v1.21 of 2021-11-04 -- http://vsl.cis.udel.edu/civl
[junit] ------------- ---------------- ---------------
[junit] Tests run: 3, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 16.504 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.MemTest
[junit] Testsuite: edu.udel.cis.vsl.civl.ModelBuilderTest
[junit] Tests run: 19, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 18.579 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.PORTest
[junit] Tests run: 17, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 14.426 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.QuietOptionTest
[junit] Tests run: 17, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 17.291 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.ReadWriteSetTest
[junit] Tests run: 5, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 44.772 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.ReasoningTest
[junit] Tests run: 27, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 50.725 sec
[junit]
[junit] ------------- Standard Error -----------------
[junit] warning: [Warning] found a space character in strategy name 'Auto level 2': replaced by '_'warning: [Warning] found a space character in strategy name 'Auto level 1': replaced by '_'warning: [Warning] found a space character in strategy name 'Auto level 0': replaced by '_'Fatal error while loading driver file '/usr/share/why3/drivers/z3_440.drv': File "/usr/share/why3/drivers/smt-libv2.gen", line 34, characters 7-14:Library file not found: intUnexpected exception happens during running why3 proveredu.udel.cis.vsl.sarl.IF.SARLException: Theorem prover unexpected exception:
[junit] nullwarning: [Warning] found a space character in strategy name 'Auto level 2': replaced by '_'warning: [Warning] found a space character in strategy name 'Auto level 1': replaced by '_'warning: [Warning] found a space character in strategy name 'Auto level 0': replaced by '_'Fatal error while loading driver file '/usr/share/why3/drivers/cvc4_15.drv': File "/usr/share/why3/drivers/smt-libv2.gen", line 34, characters 7-14:Library file not found: intwarning: [Warning] found a space character in strategy name 'Auto level 2': replaced by '_'warning: [Warning] found a space character in strategy name 'Auto level 1': replaced by '_'warning: [Warning] found a space character in strategy name 'Auto level 0': replaced by '_'Fatal error while loading driver file '/usr/share/why3/drivers/alt_ergo.drv': File "/usr/share/why3/drivers/alt_ergo_common.drv", line 49, characters 7-14:Library file not found: intwarning: [Warning] found a space character in strategy name 'Auto level 2': replaced by '_'warning: [Warning] found a space character in strategy name 'Auto level 1': replaced by '_'warning: [Warning] found a space character in strategy name 'Auto level 0': replaced by '_'Fatal error while loading driver file '/usr/share/why3/drivers/z3_440.drv': File "/usr/share/why3/drivers/smt-libv2.gen", line 34, characters 7-14:Library file not found: intUnexpected exception happens during running why3 proveredu.udel.cis.vsl.sarl.IF.SARLException: Theorem prover unexpected exception:
[junit] nullwarning: [Warning] found a space character in strategy name 'Auto level 2': replaced by '_'warning: [Warning] found a space character in strategy name 'Auto level 1': replaced by '_'warning: [Warning] found a space character in strategy name 'Auto level 0': replaced by '_'Fatal error while loading driver file '/usr/share/why3/drivers/alt_ergo.drv': File "/usr/share/why3/drivers/alt_ergo_common.drv", line 49, characters 7-14:Library file not found: intwarning: [Warning] found a space character in strategy name 'Auto level 2': replaced by '_'warning: [Warning] found a space character in strategy name 'Auto level 1': replaced by '_'warning: [Warning] found a space character in strategy name 'Auto level 0': replaced by '_'Fatal error while loading driver file '/usr/share/why3/drivers/cvc4_15.drv': File "/usr/share/why3/drivers/smt-libv2.gen", line 34, characters 7-14:Library file not found: int------------- ---------------- ---------------
[junit] Tests run: 17, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 12.326 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.ReplayTest
[junit] Testsuite: edu.udel.cis.vsl.civl.RobustnessTest
[junit] Tests run: 2, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 5.187 sec
[junit]
[junit] Tests run: 1, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 5.454 sec
[junit]
[junit] Tests run: 5, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 23.56 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.SimpleMPITest
[junit] Testsuite: edu.udel.cis.vsl.civl.ShowStatesTest
[junit] Testsuite: edu.udel.cis.vsl.civl.SpecialStatementsTest
[junit] Tests run: 10, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 13.513 sec
[junit]
[junit] ------------- Standard Output ---------------
[junit] Warning: verified probabilistically with probability of error < 2.939 E-39
[junit] Warning: verified probabilistically with probability of error < 2.939 E-39
[junit] Warning: verified probabilistically with probability of error < 2.939 E-39
[junit] Warning: verified probabilistically with probability of error < 2.939 E-39
[junit] Warning: verified probabilistically with probability of error < 2.939 E-39
[junit] ------------- ---------------- ---------------
[junit] Testsuite: edu.udel.cis.vsl.civl.SvcompTest
[junit] Tests run: 47, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 45.457 sec
[junit]
[junit] Tests run: 2, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 4.677 sec
[junit]
[junit] Tests run: 7, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 5.691 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.VerifyThisTest
[junit] Testsuite: edu.udel.cis.vsl.civl.TicketsFixTest
[junit] Testsuite: edu.udel.cis.vsl.civl.fortran.FortranLanguageFeatureTest
[junit] Tests run: 37, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 65.683 sec
[junit]
[junit] ------------- Standard Output ---------------
[junit] CIVL v1.21 of 2021-11-04 -- http://vsl.cis.udel.edu/civl
[junit]
[junit] === Source files ===
[junit] ring2.cvl (examples/concurrency/ring2.cvl)
[junit] mp_root2.cvh (examples/concurrency/mp_root2.cvh)
[junit] mp_proc2.cvh (examples/concurrency/mp_proc2.cvh)
[junit]
[junit]
[junit] === Command ===
[junit] civl verify -deadlock=potential -inputNPROCS=3 examples/concurrency/ring2.cvl
[junit]
[junit] === Stats ===
[junit] time (s) : 2.15
[junit] memory (bytes) : 3732930560
[junit] max process count : 4
[junit] states : 2407
[junit] states saved : 1556
[junit] state matches : 35
[junit] transitions : 2441
[junit] trace steps : 1069
[junit] valid calls : 9929
[junit] provers : cvc4, z3, why3
[junit] prover calls : 0
[junit]
[junit] === Result ===
[junit] The standard properties hold for all executions.
[junit] ------------- ---------------- ---------------
[junit] Tests run: 2, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 5.975 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.fortran.ProvesaMXMTest
[junit] Tests run: 72, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 55.071 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.omp.DataRaceBenchFortranTest
[junit] Testsuite: edu.udel.cis.vsl.civl.omp.DataRaceBenchTest
[junit] Tests run: 1, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 17.252 sec
[junit]
[junit] ------------- Standard Output ---------------
[junit] CIVL v1.21 of 2021-11-04 -- http://vsl.cis.udel.edu/civl
[junit] a(N/2)= 7
[junit] Data-race detected: {Dyscope0_malloc_0[2], Dyscope0_malloc_0[4], Dyscope0_malloc_0[6], Dyscope0_malloc_0[8]} read by thread 1 intersects {Dyscope0_malloc_0[2], Dyscope0_malloc_0[4], Dyscope0_malloc_0[6], Dyscope0_malloc_0[8], Dyscope0_malloc_0[0]} written by thread 0
[junit]
[junit]
[junit] Violation 0 encountered at depth 218:
[junit] CIVL execution violation in p2 (kind: ASSERTION_VIOLATION, certainty: PROVEABLE)
[junit] at OpenMPTransformer "_omp_team" inserted by OpenMPTransformer.OpenMP2CIVLWorker2.procOmpParallelNode after DRB001-antidep1-orig-yes.f95:36.24 "1" before DRB001-antidep1-orig-yes.f95:41.4-8 "PRINT"
[junit] Assertion: $sef$28
[junit] -> false
[junit]
[junit] Input:
[junit] _omp_thread_max=2
[junit] Context:
[junit] forall _t : dynamicType . (0 <= CIVL_SIZEOF(_t) - 1)
[junit] 0<=(SIZEOF_INT-1)
[junit] 0<=(SIZEOF_REAL-1)
[junit] 0!=(SIZEOF_INT+(-1*SIZEOF_REAL))
[junit] Call stacks:
[junit] process 0:
[junit] main at OpenMPTransformer "$parfor (int _omp_ti" inserted by OpenMPTransformer.OpenMP2CIVLWorker2.procOmpParallelNode after DRB001-antidep1-orig-yes.f95:30.7 "I" before DRB001-antidep1-orig-yes.f95:35.11 "1"
[junit] process 1:
[junit] $barrier_exit at concurrency.cvl:58.2-6 "$when" called from
[junit] $barrier_call at concurrency.cvl:63.2-14 "$barrier_exit" called from
[junit] $omp_barrier at civl-omp.cvl:401.2-14 "$barrier_call" called from
[junit] _par_proc0 at OpenMPTransformer "_omp_team" inserted by OpenMPTransformer.OpenMP2CIVLWorker2.procOmpParallelNode after DRB001-antidep1-orig-yes.f95:36.24 "1" before DRB001-antidep1-orig-yes.f95:41.4-8 "PRINT"
[junit] process 2:
[junit] $omp_barrier at civl-omp.cvl:391.4-10 "$assert" called from
[junit] _par_proc0 at OpenMPTransformer "_omp_team" inserted by OpenMPTransformer.OpenMP2CIVLWorker2.procOmpParallelNode after DRB001-antidep1-orig-yes.f95:36.24 "1" before DRB001-antidep1-orig-yes.f95:41.4-8 "PRINT"
[junit]
[junit] Logging new entry 0, writing trace to CIVLREP/DRB001-antidep1-orig-yes_0.trace
[junit] Terminating search after finding 1 violation.
[junit]
[junit] === Source files ===
[junit] DRB001-antidep1-orig-yes.f95 (examples/omp/dataracebench-1.3.2/micro-benchmarks-fortran/DRB001-antidep1-orig-yes.f95)
[junit]
[junit]
[junit] === Command ===
[junit] civl verify -ompNoSimplify -input_omp_thread_max=2 examples/omp/dataracebench-1.3.2/micro-benchmarks-fortran/DRB001-antidep1-orig-yes.f95
[junit]
[junit] === Stats ===
[junit] time (s) : 16.68
[junit] memory (bytes) : 2587885568
[junit] max process count : 3
[junit] states : 1531
[junit] states saved : 385
[junit] state matches : 0
[junit] transitions : 1527
[junit] trace steps : 261
[junit] valid calls : 4264
[junit] provers : cvc4, z3, why3
[junit] prover calls : 2
[junit]
[junit] === Result ===
[junit] The program MAY NOT be correct. See CIVLREP/DRB001-antidep1-orig-yes_log.txt
[junit] ------------- ---------------- ---------------
[junit] Testsuite: edu.udel.cis.vsl.civl.transform.ACSLTransformTest
[junit] Tests run: 1, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 25.088 sec
[junit]
[junit] Tests run: 8, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 7.092 sec
[junit]
[junit] ------------- Standard Error -----------------
[junit] UnsatisfiablePathConditionException thrown during interpretation of logic function:eq
[junit] ------------- ---------------- ---------------
[junit] Testsuite: edu.udel.cis.vsl.civl.transform.CompareTest
[junit] Testsuite: edu.udel.cis.vsl.civl.transform.CudaTest
[junit] Tests run: 29, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 33.647 sec
[junit]
[junit] ------------- Standard Output ---------------
[junit] CIVL v1.21 of 2021-11-04 -- http://vsl.cis.udel.edu/civl
[junit] //====================== mod_spec.f90 ======================
[junit] $system[mod_spec] void $assert(_Bool expression, ...);
[junit] $system[mod_spec] _Bool $defined(void* obj);
[junit] //======================= pointer.cvh ======================
[junit] /*@ depends_on \access(x, y);
[junit] @ executes_when $true;
[junit] @*/
[junit] $system[pointer] void $assert_equals(void* x, void* y, ...);
[junit] //====================== mod_impl.f90 ======================
[junit] $input int INVAL;
[junit] //====================== mod_spec.f90 ======================
[junit] int OUTVAL_spec;
[junit] //====================== mod_impl.f90 ======================
[junit] int OUTVAL;
[junit] //====================== mod_spec.f90 ======================
[junit] int $system_spec() {
[junit] /*@ depends_on \nothing;
[junit] @ executes_when $true;
[junit] @*/
[junit] $system[civlc] void $assume(_Bool expr);
[junit] int $spec_main() {
[junit] int N;
[junit] $assume((0 <= INVAL) && (INVAL <= 10));
[junit] N = 2;
[junit] OUTVAL_spec = INVAL % N;
[junit] }
[junit] $spec_main();
[junit] }
[junit] //====================== mod_impl.f90 ======================
[junit] int $system_impl() {
[junit] /*@ depends_on \nothing;
[junit] @ executes_when $true;
[junit] @*/
[junit] $system[civlc] void $assume(_Bool expr);
[junit] int $impl_main() {
[junit] int I;
[junit] int N;
[junit] int M;
[junit] $assume((0 <= INVAL) && (INVAL <= 10));
[junit] M = INVAL;
[junit] N = INVAL / 2;
[junit] for (I = 1; I <= N; I = I + 1) {
[junit] M = M - 2;
[junit] }
[junit] OUTVAL = M;
[junit] }
[junit] $impl_main();
[junit] }
[junit] //====================== mod_spec.f90 ======================
[junit] void main() {
[junit] _Bool _isEqual;
[junit] $system_spec();
[junit] $system_impl();
[junit] $assert_equals(&(OUTVAL_spec), &(OUTVAL), "Specification and implementation have different values for the output OUTVAL!");
[junit] }
[junit]
[junit] === Source files ===
[junit] mod_spec.f90 (examples/fortran/civl/mod_spec.f90)
[junit] mod_impl.f90 (examples/fortran/civl/mod_impl.f90)
[junit]
[junit]
[junit] === Command ===
[junit] civl compare -showProgram -spec examples/fortran/civl/mod_spec.f90 -impl examples/fortran/civl/mod_impl.f90
[junit]
[junit] === Stats ===
[junit] time (s) : 1.68
[junit] memory (bytes) : 2587885568
[junit] max process count : 1
[junit] states : 68
[junit] states saved : 45
[junit] state matches : 0
[junit] transitions : 67
[junit] trace steps : 25
[junit] valid calls : 64
[junit] provers : cvc4, z3, why3
[junit] prover calls : 32
[junit]
[junit] === Result ===
[junit] The standard properties hold for all executions.
[junit] ------------- ---------------- ---------------
[junit] Testsuite: edu.udel.cis.vsl.civl.transform.GenTransformerTest
[junit] Tests run: 7, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 36.67 sec
[junit]
[junit] ------------- Standard Error -----------------
[junit] cvc4 query 0: time out
[junit] z3 query 1: time out
[junit] cvc4 query 2: time out
[junit] z3 query 3: time out
[junit] warning: [Warning] found a space character in strategy name 'Auto level 2': replaced by '_'warning: [Warning] found a space character in strategy name 'Auto level 1': replaced by '_'warning: [Warning] found a space character in strategy name 'Auto level 0': replaced by '_'Fatal error while loading driver file '/usr/share/why3/drivers/alt_ergo.drv': File "/usr/share/why3/drivers/alt_ergo_common.drv", line 49, characters 7-14:Library file not found: intUnexpected exception happens during running why3 proveredu.udel.cis.vsl.sarl.IF.SARLException: Theorem prover unexpected exception:
[junit] nullwarning: [Warning] found a space character in strategy name 'Auto level 2': replaced by '_'warning: [Warning] found a space character in strategy name 'Auto level 1': replaced by '_'warning: [Warning] found a space character in strategy name 'Auto level 0': replaced by '_'Fatal error while loading driver file '/usr/share/why3/drivers/z3_440.drv': File "/usr/share/why3/drivers/smt-libv2.gen", line 34, characters 7-14:Library file not found: intwarning: [Warning] found a space character in strategy name 'Auto level 2': replaced by '_'warning: [Warning] found a space character in strategy name 'Auto level 1': replaced by '_'warning: [Warning] found a space character in strategy name 'Auto level 0': replaced by '_'Fatal error while loading driver file '/usr/share/why3/drivers/cvc4_15.drv': File "/usr/share/why3/drivers/smt-libv2.gen", line 34, characters 7-14:Library file not found: intwarning: [Warning] found a space character in strategy name 'Auto level 2': replaced by '_'warning: [Warning] found a space character in strategy name 'Auto level 1': replaced by '_'warning: [Warning] found a space character in strategy name 'Auto level 0': replaced by '_'Fatal error while loading driver file '/usr/share/why3/drivers/z3_440.drv': File "/usr/share/why3/drivers/smt-libv2.gen", line 34, characters 7-14:Library file not found: intwarning: [Warning] found a space character in strategy name 'Auto level 2': replaced by '_'warning: [Warning] found a space character in strategy name 'Auto level 1': replaced by '_'warning: [Warning] found a space character in strategy name 'Auto level 0': replaced by '_'Fatal error while loading driver file '/usr/share/why3/drivers/alt_ergo.drv': File "/usr/share/why3/drivers/alt_ergo_common.drv", line 49, characters 7-14:Library file not found: intwarning: [Warning] found a space character in strategy name 'Auto level 2': replaced by '_'warning: [Warning] found a space character in strategy name 'Auto level 1': replaced by '_'warning: [Warning] found a space character in strategy name 'Auto level 0': replaced by '_'Fatal error while loading driver file '/usr/share/why3/drivers/cvc4_15.drv': File "/usr/share/why3/drivers/smt-libv2.gen", line 34, characters 7-14:Library file not found: intcvc4 query 12: time out
[junit] cvc4 query 14: time out
[junit] ------------- ---------------- ---------------
[junit] Testsuite: edu.udel.cis.vsl.civl.transform.IOTransformerTest
[junit] Tests run: 153, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 112.947 sec
[junit]
[junit] ------------- Standard Error -----------------
[junit] Warning: ignoring a division by zero
[junit] ------------- ---------------- ---------------
[junit] Testsuite: edu.udel.cis.vsl.civl.transform.LoopInvariantsNoAssignsTest
[junit] Tests run: 4, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 12.629 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.transform.LoopInvariantsWithAssignsPart1Test
[junit] Tests run: 3, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 16.86 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.transform.LoopInvariantsWithAssignsPart2Test
[junit] Tests run: 1, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 5.206 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.transform.MPICollectivePart1Test
[junit] Tests run: 2, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 7.652 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.transform.MPICollectivePart2Test
[junit] Tests run: 5, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 11.847 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.transform.MPIFeatureTest
[junit] Tests run: 4, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 45.666 sec
[junit]
[junit] ------------- Standard Output ---------------
[junit] CIVL v1.21 of 2021-11-04 -- http://vsl.cis.udel.edu/civl
[junit]
[junit] === Source files ===
[junit] kernel_after_main.cu (examples/cuda/kernel_after_main.cu)
[junit]
[junit]
[junit] === Command ===
[junit] civl verify examples/cuda/kernel_after_main.cu
[junit]
[junit] === Stats ===
[junit] time (s) : 11.36
[junit] memory (bytes) : 2155872256
[junit] max process count : 8
[junit] states : 1748
[junit] states saved : 1165
[junit] state matches : 61
[junit] transitions : 1787
[junit] trace steps : 727
[junit] valid calls : 4914
[junit] provers : cvc4, z3, why3
[junit] prover calls : 2
[junit]
[junit] === Result ===
[junit] The standard properties hold for all executions.
[junit] ------------- ---------------- ---------------
[junit] Testsuite: edu.udel.cis.vsl.civl.transform.MPITranslationTest
[junit] Tests run: 23, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 125.499 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.transform.MPI_OpenMPTest
[junit] Tests run: 15, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 124.08 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.transform.OpenMP2CIVLTransformerTest
[junit] Tests run: 5, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 64.073 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.transform.OpenMPSimplifierTest
[junit] Tests run: 3, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 24.622 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.transform.PthreadTest
[junit] Tests run: 20, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 93.47 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.transform.PthreadThreaderTest
[junit] Tests run: 27, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 24.364 sec
[junit]
[junit] ------------- Standard Error -----------------
[junit] warning: this is a sound and expected result but not precise enough. Improvement is expected in near future.
[junit] ------------- ---------------- ---------------
[junit] Testsuite: edu.udel.cis.vsl.civl.transform.SeqContractTest
[junit] Tests run: 27, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 35.687 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.transform.SideEffectsTest
[junit] Tests run: 1, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 5.691 sec
[junit]
[junit] Tests run: 75, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 159.529 sec
[junit]
[junit] ------------- Standard Output ---------------
[junit] CIVL v1.21 of 2021-11-04 -- http://vsl.cis.udel.edu/civl
[junit]
[junit] === Source files ===
[junit] DRB113-default-orig-no.c (examples/omp/dataracebench-1.3.2/micro-benchmarks/DRB113-default-orig-no.c)
[junit]
[junit]
[junit] === Command ===
[junit] civl verify -ompNoSimplify -input_omp_thread_max=2 -DN=10 examples/omp/dataracebench-1.3.2/micro-benchmarks/DRB113-default-orig-no.c
[junit]
[junit] === Stats ===
[junit] time (s) : 0.45
[junit] memory (bytes) : 3212836864
[junit] max process count : 3
[junit] states : 2216
[junit] states saved : 171
[junit] state matches : 2
[junit] transitions : 2207
[junit] trace steps : 111
[junit] valid calls : 6006
[junit] provers : cvc4, z3, why3
[junit] prover calls : 0
[junit]
[junit] === Result ===
[junit] The standard properties hold for all executions.
[junit] ------------- ---------------- ---------------
[junit] Tests run: 8, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 15.75 sec
[junit]
[junit] Tests run: 10, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 5.086 sec
[junit]
[junit] Tests run: 13, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 22.386 sec
[junit]
[junit] Tests run: 15, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 138.313 sec
[junit]
[junit] Tests run: 23, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 103.098 sec
[junit]
[junit] Tests run: 25, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 123.852 sec
[junit]
[junitreport] Processing /usa/svn/work/civl/1.21/r5476/junit/data/TESTS-TestSuites.xml to /tmp/null112572617
[junitreport] Loading stylesheet jar:file:/usr/share/ant/lib/ant-junit.jar!/org/apache/tools/ant/taskdefs/optional/junit/xsl/junit-frames.xsl
[junitreport] Transform time: 549ms
[junitreport] Deleting: /tmp/null112572617
test:
[jacoco:report] Loading execution data file /usa/svn/work/civl/1.21/r5476/jacoco.exec
[jacoco:report] Writing bundle 'Test Coverage Report for CIVL 1.21 r5476 Regression Suite' with 474 classes
javadoc:
[mkdir] Created dir: /usa/svn/work/civl/1.21/r5476/doc/javadoc
[javadoc] Generating Javadoc
[javadoc] Javadoc execution
[javadoc] Loading source files for package edu.udel.cis.vsl.civl...
[javadoc] Loading source files for package edu.udel.cis.vsl.civl.analysis.IF...
[javadoc] Loading source files for package edu.udel.cis.vsl.civl.config.IF...
[javadoc] Loading source files for package edu.udel.cis.vsl.civl.dynamic.IF...
[javadoc] Loading source files for package edu.udel.cis.vsl.civl.kripke.IF...
[javadoc] Loading source files for package edu.udel.cis.vsl.civl.log.IF...
[javadoc] Loading source files for package edu.udel.cis.vsl.civl.model.IF...
[javadoc] Loading source files for package edu.udel.cis.vsl.civl.model.IF.contract...
[javadoc] Loading source files for package edu.udel.cis.vsl.civl.model.IF.expression...
[javadoc] Loading source files for package edu.udel.cis.vsl.civl.model.IF.expression.reference...
[javadoc] Loading source files for package edu.udel.cis.vsl.civl.model.IF.location...
[javadoc] Loading source files for package edu.udel.cis.vsl.civl.model.IF.statement...
[javadoc] Loading source files for package edu.udel.cis.vsl.civl.model.IF.type...
[javadoc] Loading source files for package edu.udel.cis.vsl.civl.model.IF.variable...
[javadoc] Loading source files for package edu.udel.cis.vsl.civl.predicate.IF...
[javadoc] Loading source files for package edu.udel.cis.vsl.civl.run.IF...
[javadoc] Loading source files for package edu.udel.cis.vsl.civl.semantics.IF...
[javadoc] Loading source files for package edu.udel.cis.vsl.civl.slice.IF...
[javadoc] Loading source files for package edu.udel.cis.vsl.civl.state.IF...
[javadoc] Loading source files for package edu.udel.cis.vsl.civl.transform.IF...
[javadoc] Loading source files for package edu.udel.cis.vsl.civl.util.IF...
[javadoc] Constructing Javadoc information...
[javadoc] Standard Doclet version 11.0.11
[javadoc] Building tree for all the packages and classes...
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/config/IF/CIVLConstants.java:334: warning - Tag @link: reference not found: UpdaterRunnable
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/config/IF/CIVLConstants.java:334: warning - Tag @link: reference not found: UpdaterRunnable
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/dynamic/IF/DynamicMemoryLocationSet.java:36: warning - Tag @link: reference not found: ImmutableStateFactory#deallocate(edu.udel.cis.vsl.civl.state.IF.State, SymbolicExpression, int, int, int)
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:629: warning - invalid usage of tag >
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:328: warning - Tag @link: reference not found: #isPointerToHeap(heapPointer)
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:381: warning - invalid usage of tag &a
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:382: warning - invalid usage of tag &a
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:483: warning - Tag @author cannot be used in method documentation. It can only be used in the following types of documentation: overview, module, package, class/interface.
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:629: warning - invalid usage of tag >
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:639: warning - invalid usage of tag >
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:785: warning - invalid usage of tag &
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:785: warning - invalid usage of tag &
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:785: warning - invalid usage of tag <
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:785: warning - invalid usage of tag &
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:785: warning - invalid usage of tag &
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:785: warning - invalid usage of tag >
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:785: warning - invalid usage of tag <
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:786: warning - invalid usage of tag <
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:786: warning - invalid usage of tag >
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:786: warning - invalid usage of tag <
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:797: warning - @param argument "arguments" is not a parameter name.
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/kripke/IF/LibraryEnabler.java:54: warning - @param argument "reachablePtrWritableMap" is not a parameter name.
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/kripke/IF/LibraryEnabler.java:55: warning - @param argument "reachablePtrReadonlyMap" is not a parameter name.
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/kripke/IF/LibraryEnabler.java:56: warning - @param argument "reachableNonPtrWritableMap" is not a parameter name.
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/kripke/IF/LibraryEnabler.java:57: warning - @param argument "reachableNonPtrReadonlyMap" is not a parameter name.
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/kripke/IF/LibraryEnabler.java:58: warning - @param argument "reachableMemUnitsMap" is not a parameter name.
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/log/IF/CIVLErrorLogger.java:67: warning - @param argument "config" is not a parameter name.
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/log/IF/CIVLErrorLogger.java:104: warning - invalid usage of tag &
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/log/IF/CIVLErrorLogger.java:104: warning - invalid usage of tag &
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/log/IF/CIVLErrorLogger.java:105: warning - invalid usage of tag &
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/log/IF/CIVLErrorLogger.java:105: warning - invalid usage of tag &
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/log/IF/CIVLErrorLogger.java:106: warning - invalid usage of tag &
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/log/IF/CIVLErrorLogger.java:106: warning - invalid usage of tag &
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/log/IF/CIVLErrorLogger.java:107: warning - invalid usage of tag &
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/log/IF/CIVLErrorLogger.java:107: warning - invalid usage of tag &
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/log/IF/CIVLErrorLogger.java:121: warning - @param argument "process" is not a parameter name.
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/log/IF/CIVLExecutionException.java:47: warning - @param argument "stateString" is not a parameter name.
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/model/IF/CIVLFunction.java:185: warning - invalid usage of tag >
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/model/IF/CIVLFunction.java:186: warning - invalid usage of tag >
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/model/IF/CIVLFunction.java:186: warning - invalid usage of tag >
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/model/IF/CIVLFunction.java:187: warning - invalid usage of tag >
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/model/IF/CIVLFunction.java:188: warning - invalid usage of tag >
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/model/IF/CIVLFunction.java:188: warning - invalid usage of tag >
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/model/IF/CIVLFunction.java:314: warning - @param argument "validConsequences" is not a parameter name.
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/model/IF/CIVLTypeFactory.java:172: warning - invalid usage of tag >
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/model/IF/CIVLTypeFactory.java:172: warning - invalid usage of tag >
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/model/IF/CIVLTypeFactory.java:172: warning - invalid usage of tag >
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/model/IF/CIVLTypeFactory.java:172: warning - invalid usage of tag >
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/model/IF/CIVLTypeFactory.java:172: warning - invalid usage of tag >
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/model/IF/CIVLTypeFactory.java:172: warning - invalid usage of tag >
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/model/IF/CIVLTypeFactory.java:172: warning - invalid usage of tag >
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/model/IF/CIVLTypeFactory.java:455: warning - @param argument "universe" is not a parameter name.
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/model/IF/CIVLTypeFactory.java:457: warning - @param argument "the" is not a parameter name.
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/model/IF/CIVLTypeFactory.java:497: warning - @param argument "expr" is not a parameter name.
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/model/IF/LogicFunction.java:52: warning - Tag @author cannot be used in field documentation. It can only be used in the following types of documentation: overview, module, package, class/interface.
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:101: warning - Tag @link: reference not found: #function(CIVLSource, Identifier, List, CIVLType, Scope, Location)
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:130: warning - invalid usage of tag &e
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:533: warning - invalid usage of tag <
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:533: warning - invalid usage of tag <
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:130: warning - invalid usage of tag &e
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:158: warning - invalid usage of tag <
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:158: warning - invalid usage of tag <
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:158: warning - invalid usage of tag &
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:158: warning - invalid usage of tag &
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:474: warning - @param argument "boundVariableList" is not a parameter name.
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:514: warning - invalid usage of tag >
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:533: warning - invalid usage of tag <
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:533: warning - invalid usage of tag <
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:668: warning - invalid usage of tag &
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:668: warning - invalid usage of tag &
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:1057: warning - Tag @link: reference not found: #noopStatement(CIVLSource, Location)
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:1490: warning - @param argument "source" is not a parameter name.
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:1544: warning - @param argument "scope" is not a parameter name.
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/model/IF/Scope.java:87: warning - @param argument "A" is not a parameter name.
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/model/IF/Scope.java:213: warning - @param argument "des" is not a parameter name.
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/model/IF/contract/FunctionBehavior.java:109: warning - invalid usage of tag {@link #dependsNoact()==false
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/model/IF/contract/FunctionBehavior.java:101: warning - invalid usage of tag &
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/model/IF/contract/FunctionBehavior.java:101: warning - invalid usage of tag &
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/model/IF/contract/FunctionBehavior.java:87: warning - Tag @link: reference not found: #numReadsClauses()
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/model/IF/contract/FunctionBehavior.java:94: warning - Tag @link: reference not found: #numAssignsClauses()
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/model/IF/contract/FunctionBehavior.java:101: warning - invalid usage of tag &
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/model/IF/contract/FunctionBehavior.java:101: warning - invalid usage of tag &
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/model/IF/contract/FunctionBehavior.java:109: warning - invalid usage of tag {@link #dependsNoact()==false
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/model/IF/contract/FunctionBehavior.java:130: warning - @param argument "assigns" is not a parameter name.
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/model/IF/contract/FunctionBehavior.java:137: warning - @param argument "reads" is not a parameter name.
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/model/IF/contract/FunctionBehavior.java:145: warning - @param argument "depends" is not a parameter name.
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/model/IF/contract/FunctionBehavior.java:187: warning - @param argument "subPrefix" is not a parameter name.
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/model/IF/expression/AddressOfExpression.java:7: warning - invalid usage of tag &x
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/model/IF/expression/AddressOfExpression.java:7: warning - invalid usage of tag &
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/model/IF/expression/BinaryExpression.java:18: warning - invalid usage of tag &
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/model/IF/expression/BinaryExpression.java:18: warning - invalid usage of tag &
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/model/IF/expression/BinaryExpression.java:19: warning - invalid usage of tag <
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/model/IF/expression/BinaryExpression.java:20: warning - invalid usage of tag >
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/model/IF/expression/BinaryExpression.java:20: warning - invalid usage of tag >
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/model/IF/expression/BinaryExpression.java:21: warning - invalid usage of tag &
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/model/IF/expression/BinaryExpression.java:28: warning - invalid usage of tag <
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/model/IF/expression/BinaryExpression.java:29: warning - invalid usage of tag <
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/model/IF/expression/BinaryExpression.java:18: warning - invalid usage of tag &
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/model/IF/expression/BinaryExpression.java:18: warning - invalid usage of tag &
[javadoc] /usa/svn/work/civl/1.21/r5476/src/edu/udel/cis/vsl/civl/model/IF/expression/BinaryExpression.java:19: warning - invalid usage of tag <
[javadoc] Building index for all the packages and classes...
[javadoc] Building index for all classes...
[javadoc] Building index for all classes...
[javadoc] Generating /usa/svn/work/civl/1.21/r5476/doc/javadoc/help-doc.html...
[javadoc] 100 warnings
bench-compile:
[javac] Compiling 6 source files to /usa/svn/work/civl/1.21/r5476/bin
bench-scale-compile:
[javac] Compiling 5 source files to /usa/svn/work/civl/1.21/r5476/bin
all:
BUILD SUCCESSFUL
Total time: 4 minutes 30 seconds
Stderr: