Path: . Working Copy Root Path: /usa/svn/work/civl/1.17/r4979 URL: svn://vsl.cis.udel.edu/civl/branches/release-1.17 Relative URL: ^/branches/release-1.17 Repository Root: svn://vsl.cis.udel.edu/civl Repository UUID: fb995dde-84ed-4084-dfe6-e5aef3e2452c Revision: 4979 Node Kind: directory Schedule: normal Last Changed Author: yihaoyan Last Changed Rev: 4973 Last Changed Date: 2018-07-18 13:50:11 -0400 (Wed, 18 Jul 2018)
Stdout:
Buildfile: /usa/svn/work/civl/1.17/r4979/build.xml
checkCommandParserChanges:
CommandParser:
[move] Moving 1 file to /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/run/common
[move] Moving 1 file to /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/run/common
[move] Moving 1 file to /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/run/common
[move] Moving 1 file to /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/run/common
compile:
[mkdir] Created dir: /usa/svn/work/civl/1.17/r4979/bin
[javac] Compiling 537 source files to /usa/svn/work/civl/1.17/r4979/bin
[javac] Creating empty /usa/svn/work/civl/1.17/r4979/bin/edu/udel/cis/vsl/civl/model/IF/expression/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.17/r4979/bin/edu/udel/cis/vsl/civl/state/IF/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.17/r4979/bin/edu/udel/cis/vsl/civl/gui/IF/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.17/r4979/bin/edu/udel/cis/vsl/civl/gui/common/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.17/r4979/bin/edu/udel/cis/vsl/civl/semantics/IF/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.17/r4979/bin/edu/udel/cis/vsl/civl/kripke/IF/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.17/r4979/bin/edu/udel/cis/vsl/civl/util/IF/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.17/r4979/bin/edu/udel/cis/vsl/civl/library/domain/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.17/r4979/bin/edu/udel/cis/vsl/civl/model/IF/type/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.17/r4979/bin/edu/udel/cis/vsl/civl/library/comm/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.17/r4979/bin/edu/udel/cis/vsl/civl/library/pointer/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.17/r4979/bin/edu/udel/cis/vsl/civl/model/IF/location/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.17/r4979/bin/edu/udel/cis/vsl/civl/library/time/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.17/r4979/bin/edu/udel/cis/vsl/civl/library/pthread/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.17/r4979/bin/edu/udel/cis/vsl/civl/config/IF/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.17/r4979/bin/edu/udel/cis/vsl/civl/dynamic/IF/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.17/r4979/bin/edu/udel/cis/vsl/civl/library/civlc/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.17/r4979/bin/edu/udel/cis/vsl/civl/log/IF/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.17/r4979/bin/edu/udel/cis/vsl/civl/library/common/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.17/r4979/bin/edu/udel/cis/vsl/civl/model/IF/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.17/r4979/bin/edu/udel/cis/vsl/civl/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.17/r4979/bin/edu/udel/cis/vsl/civl/model/IF/variable/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.17/r4979/bin/edu/udel/cis/vsl/civl/library/seq/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.17/r4979/bin/edu/udel/cis/vsl/civl/library/string/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.17/r4979/bin/edu/udel/cis/vsl/civl/analysis/IF/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.17/r4979/bin/edu/udel/cis/vsl/civl/library/scope/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.17/r4979/bin/edu/udel/cis/vsl/civl/model/IF/statement/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.17/r4979/bin/edu/udel/cis/vsl/civl/predicate/IF/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.17/r4979/bin/edu/udel/cis/vsl/civl/library/bundle/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.17/r4979/bin/edu/udel/cis/vsl/civl/slice/common/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.17/r4979/bin/edu/udel/cis/vsl/civl/slice/IF/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.17/r4979/bin/edu/udel/cis/vsl/civl/run/IF/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.17/r4979/bin/edu/udel/cis/vsl/civl/transform/IF/package-info.class
[copy] Copying 32 files to /usa/svn/work/civl/1.17/r4979/bin/include
jar:
[jar] Building jar: /usa/svn/work/civl/1.17/r4979/civl.jar
test-init:
[mkdir] Created dir: /usa/svn/work/civl/1.17/r4979/junit
[mkdir] Created dir: /usa/svn/work/civl/1.17/r4979/junit/data
[mkdir] Created dir: /usa/svn/work/civl/1.17/r4979/junit/reports
[mkdir] Created dir: /usa/svn/work/civl/1.17/r4979/bin-test/regress
test-compile:
[javac] Compiling 39 source files to /usa/svn/work/civl/1.17/r4979/bin-test/regress
test-run:
[jacoco:coverage] Enhancing junit with coverage
[junit] Testsuite: edu.udel.cis.vsl.civl.AcfInterfaceTest
[junit] Tests run: 2, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 5.513 sec
[junit]
[junit] ------------- Standard Output ---------------
[junit] CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl
[junit] __VERIFIER_error() is called.
[junit]
[junit]
[junit] Violation 0 encountered at depth 25:
[junit] CIVL execution violation in p0 (kind: ASSERTION_VIOLATION, certainty: PROVEABLE)
[junit] at stress_test.c:56.10-25
[junit] __VERIFIER_error();
[junit] ^^^^^^^^^^^^^^^^
[junit]
[junit] Assertion: false
[junit] -> false
[junit]
[junit] Input:
[junit] _svcomp_unsigned_bound=4
[junit] Context:
[junit] (Y0-5)<=0
[junit] (Y0+1)<=0
[junit] (Y1-5)<=0
[junit] (Y2-5)<=0
[junit] (Y2+1)<=0
[junit] (Y3-5)<=0
[junit] (Y3+1)<=0
[junit] 0<=(Y0+5)
[junit] 0<=(Y1-1)
[junit] 0<=(Y1+5)
[junit] 0<=(Y2+5)
[junit] 0<=(Y3+5)
[junit] Call stacks:
[junit] process 0:
[junit] __VERIFIER_error at svcomp.cvl:97.2-8 "$assert" called from
[junit] main at stress_test.c:56.10-25 "__VERIFIER_error"
[junit]
[junit] Logging new entry 0, writing trace to CIVLREP/stress_test_0.trace
[junit] Terminating search after finding 1 violation.
[junit]
[junit] === Source files ===
[junit] stress_test.c (examples/slice/stress_test.c)
[junit]
[junit]
[junit] === Command ===
[junit] civl verify -svcomp16 examples/slice/stress_test.c
[junit]
[junit] === Stats ===
[junit] time (s) : 3.22
[junit] memory (bytes) : 332398592
[junit] max process count : 1
[junit] states : 39
[junit] states saved : 33
[junit] state matches : 0
[junit] transitions : 39
[junit] trace steps : 24
[junit] valid calls : 22
[junit] provers : cvc4, z3
[junit] prover calls : 9
[junit]
[junit] === Result ===
[junit] The program MAY NOT be correct. See CIVLREP/stress_test_log.txt
[junit] CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl
[junit] __VERIFIER_error() is called.
[junit]
[junit] Error 0:
[junit] CIVL execution violation in p0 (kind: ASSERTION_VIOLATION, certainty: PROVEABLE)
[junit] at stress_test.c:56.10-25
[junit] __VERIFIER_error();
[junit] ^^^^^^^^^^^^^^^^
[junit]
[junit] Assertion: false
[junit] -> false
[junit]
[junit] Input:
[junit] _svcomp_unsigned_bound=4
[junit] Context:
[junit] (Y0-5)<=0
[junit] (Y0+1)<=0
[junit] (Y1-5)<=0
[junit] (Y2-5)<=0
[junit] (Y2+1)<=0
[junit] (Y3-5)<=0
[junit] (Y3+1)<=0
[junit] 0<=(Y0+5)
[junit] 0<=(Y1-1)
[junit] 0<=(Y1+5)
[junit] 0<=(Y2+5)
[junit] 0<=(Y3+5)
[junit] Call stacks:
[junit] process 0:
[junit] __VERIFIER_error at svcomp.cvl:97.2-8 "$assert" called from
[junit] main at stress_test.c:56.10-25 "__VERIFIER_error"
[junit]
[junit] Trace ends after 25 trace steps.
[junit] Violation(s) found.
[junit]
[junit] === Source files ===
[junit] stress_test.c (examples/slice/stress_test.c)
[junit]
[junit]
[junit] === Command ===
[junit] civl replay -sliceAnalysis examples/slice/stress_test.c
[junit]
[junit] === Stats ===
[junit] time (s) : 0.73
[junit] memory (bytes) : 332398592
[junit] max process count : 1
[junit] states : 40
[junit] valid calls : 23
[junit] provers : cvc4, z3
[junit] prover calls : 9
[junit]
[junit] CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl
[junit] __VERIFIER_error() is called.
[junit]
[junit]
[junit] Violation 0 encountered at depth 34:
[junit] CIVL execution violation in p0 (kind: ASSERTION_VIOLATION, certainty: PROVEABLE)
[junit] at stress_test.c:56.10-25
[junit] __VERIFIER_error();
[junit] ^^^^^^^^^^^^^^^^
[junit]
[junit] Assertion: false
[junit] -> false
[junit]
[junit] Input:
[junit] _svcomp_unsigned_bound=4
[junit] Context:
[junit] (Y0-5)<=0
[junit] (Y0+1)<=0
[junit] (Y1-5)<=0
[junit] (Y2-5)<=0
[junit] (Y2+1)<=0
[junit] (Y3-5)<=0
[junit] (Y3+1)<=0
[junit] 0<=(Y0+5)
[junit] 0<=(Y1-1)
[junit] 0<=(Y1+5)
[junit] 0<=(Y2+5)
[junit] 0<=(Y3+5)
[junit] Call stacks:
[junit] process 0:
[junit] __VERIFIER_error at svcomp.cvl:97.2-8 "$assert" called from
[junit] main at stress_test.c:56.10-25 "__VERIFIER_error"
[junit]
[junit] Logging new entry 0, writing trace to CIVLREP/stress_test_0.trace
[junit] Terminating search after finding 1 violation.
[junit]
[junit] === Source files ===
[junit] stress_test.c (examples/slice/stress_test.c)
[junit]
[junit]
[junit] === Command ===
[junit] civl verify -svcomp16 -direct=examples/slice/stress_test.direct examples/slice/stress_test.c
[junit]
[junit] === Stats ===
[junit] time (s) : 0.68
[junit] memory (bytes) : 498597888
[junit] max process count : 1
[junit] states : 90
[junit] states saved : 54
[junit] state matches : 0
[junit] transitions : 90
[junit] trace steps : 33
[junit] valid calls : 22
[junit] provers : cvc4, z3
[junit] prover calls : 1
[junit]
[junit] === Result ===
[junit] The program MAY NOT be correct. See CIVLREP/stress_test_log.txt
[junit] CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl
[junit] __VERIFIER_error() is called.
[junit]
[junit] Error 0:
[junit] CIVL execution violation in p0 (kind: ASSERTION_VIOLATION, certainty: PROVEABLE)
[junit] at stress_test.c:56.10-25
[junit] __VERIFIER_error();
[junit] ^^^^^^^^^^^^^^^^
[junit]
[junit] Assertion: false
[junit] -> false
[junit]
[junit] Input:
[junit] _svcomp_unsigned_bound=4
[junit] Context:
[junit] (Y0-5)<=0
[junit] (Y0+1)<=0
[junit] (Y1-5)<=0
[junit] (Y2-5)<=0
[junit] (Y2+1)<=0
[junit] (Y3-5)<=0
[junit] (Y3+1)<=0
[junit] 0<=(Y0+5)
[junit] 0<=(Y1-1)
[junit] 0<=(Y1+5)
[junit] 0<=(Y2+5)
[junit] 0<=(Y3+5)
[junit] Call stacks:
[junit] process 0:
[junit] __VERIFIER_error at svcomp.cvl:97.2-8 "$assert" called from
[junit] main at stress_test.c:56.10-25 "__VERIFIER_error"
[junit]
[junit] Trace ends after 34 trace steps.
[junit] Violation(s) found.
[junit]
[junit] === Source files ===
[junit] stress_test.c (examples/slice/stress_test.c)
[junit]
[junit]
[junit] === Command ===
[junit] civl replay -sliceAnalysis examples/slice/stress_test.c
[junit]
[junit] === Stats ===
[junit] time (s) : 0.63
[junit] memory (bytes) : 498597888
[junit] max process count : 1
[junit] states : 91
[junit] valid calls : 23
[junit] provers : cvc4, z3
[junit] prover calls : 1
[junit]
[junit] ------------- ---------------- ---------------
[junit] Testsuite: edu.udel.cis.vsl.civl.AnalysisTest
[junit] Tests run: 3, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 1.995 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.ArithmeticTest
[junit] Tests run: 27, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 10.605 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.BackendTest
[junit] Tests run: 16, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 1.941 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.CompareTest
[junit] Tests run: 5, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 120.157 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.ConcurrencyTest
[junit] Tests run: 34, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 13.881 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.LanguageFeaturesTest
[junit] Tests run: 145, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 16.66 sec
[junit]
[junit] ------------- Standard Output ---------------
[junit] CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl
[junit]
[junit] Violation 0 encountered at depth 1:
[junit] CIVL execution violation in p0 (kind: ASSERTION_VIOLATION, certainty: PROVEABLE)
[junit] at sizeofTestBad.cvl:5.2-30
[junit] $assert(sizeof(struct T) > 1);
[junit] ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
[junit]
[junit] Assertion: (1<sizeof(struct T))
[junit] -> 1<CIVL_SIZEOF(115)
[junit] -> 0<=(CIVL_SIZEOF(115)-2)
[junit]
[junit] Context:
[junit] forall _t : dynamicType . (0 <= CIVL_SIZEOF(_t) - 1)
[junit] Call stacks:
[junit] process 0:
[junit] main at sizeofTestBad.cvl:5.2-8 "$assert"
[junit]
[junit] Logging new entry 0, writing trace to CIVLREP/sizeofTestBad_0.trace
[junit] Terminating search after finding 1 violation.
[junit]
[junit] === Source files ===
[junit] sizeofTestBad.cvl (examples/languageFeatures/sizeofTestBad.cvl)
[junit]
[junit]
[junit] === Command ===
[junit] civl verify examples/languageFeatures/sizeofTestBad.cvl
[junit]
[junit] === Stats ===
[junit] time (s) : 0.08
[junit] memory (bytes) : 824705024
[junit] max process count : 0
[junit] states : 1
[junit] states saved : 1
[junit] state matches : 0
[junit] transitions : 1
[junit] trace steps : 0
[junit] valid calls : 2
[junit] provers : cvc4, z3
[junit] prover calls : 4
[junit]
[junit] === Result ===
[junit] The program MAY NOT be correct. See CIVLREP/sizeofTestBad_log.txt
[junit] CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl
[junit]
[junit] === Source files ===
[junit] sizeofTest.cvl (examples/languageFeatures/sizeofTest.cvl)
[junit]
[junit]
[junit] === Command ===
[junit] civl verify examples/languageFeatures/sizeofTest.cvl
[junit]
[junit] === Stats ===
[junit] time (s) : 0.06
[junit] memory (bytes) : 823656448
[junit] max process count : 1
[junit] states : 3
[junit] states saved : 2
[junit] state matches : 0
[junit] transitions : 2
[junit] trace steps : 1
[junit] valid calls : 1
[junit] provers : cvc4, z3
[junit] prover calls : 1
[junit]
[junit] === Result ===
[junit] The standard properties hold for all executions.
[junit] CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl
[junit]
[junit] === Source files ===
[junit] typedefbugMain.c (examples/languageFeatures/typedefbugMain.c)
[junit] typedefbugHeader.h (examples/languageFeatures/typedefbugHeader.h)
[junit] typedefbugSource.c (examples/languageFeatures/typedefbugSource.c)
[junit]
[junit]
[junit] === Command ===
[junit] civl verify examples/languageFeatures/typedefbugMain.c examples/languageFeatures/typedefbugSource.c
[junit]
[junit] === Stats ===
[junit] time (s) : 0.01
[junit] memory (bytes) : 826277888
[junit] max process count : 1
[junit] states : 3
[junit] states saved : 3
[junit] state matches : 0
[junit] transitions : 2
[junit] trace steps : 1
[junit] valid calls : 0
[junit] provers : cvc4, z3
[junit] prover calls : 0
[junit]
[junit] === Result ===
[junit] The standard properties hold for all executions.
[junit] CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl
[junit] //======================== civlc.cvh =======================
[junit] /*@ depends_on \nothing;
[junit] @ executes_when $true;
[junit] @*/
[junit] $system[civlc] void $assert(_Bool expr, ...);
[junit] /*@ depends_on \nothing;
[junit] @ executes_when $true;
[junit] @*/
[junit] $system[civlc] void $assume(_Bool expr);
[junit] //======================== assert.h ========================
[junit] /*@ depends_on \nothing;
[junit] @*/
[junit] $atomic_f void assert(_Bool expr);
[junit] //==================== inputProblem1.cvl ===================
[junit] int X;
[junit] $assume(X > 0);
[junit] int main() {
[junit] assert(X == 1);
[junit] }
[junit] //==================== inputProblem2.cvl ===================
[junit] X = 1;
[junit] //======================= assert.cvl =======================
[junit] $atomic_f void assert(_Bool expr) {
[junit] $assert(expr);
[junit] }
[junit]
[junit] === Source files ===
[junit] inputProblem1.cvl (examples/languageFeatures/inputProblem1.cvl)
[junit] inputProblem2.cvl (examples/languageFeatures/inputProblem2.cvl)
[junit]
[junit]
[junit] === Command ===
[junit] civl verify -showProgram examples/languageFeatures/inputProblem1.cvl examples/languageFeatures/inputProblem2.cvl
[junit]
[junit] === Stats ===
[junit] time (s) : 0.07
[junit] memory (bytes) : 836239360
[junit] max process count : 1
[junit] states : 8
[junit] states saved : 3
[junit] state matches : 0
[junit] transitions : 7
[junit] trace steps : 1
[junit] valid calls : 1
[junit] provers : cvc4, z3
[junit] prover calls : 0
[junit]
[junit] === Result ===
[junit] The standard properties hold for all executions.
[junit] CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl
[junit] //=================== incompleteStruct.c ===================
[junit] typedef struct mytype mytype;
[junit] int main() {
[junit] mytype* a = (void*)0;
[junit] return (int)a;
[junit] }
[junit]
[junit] === Source files ===
[junit] incompleteStruct.c (examples/languageFeatures/incompleteStruct.c)
[junit]
[junit]
[junit] === Command ===
[junit] civl verify -showProgram examples/languageFeatures/incompleteStruct.c
[junit]
[junit] === Stats ===
[junit] time (s) : 0.3
[junit] memory (bytes) : 846725120
[junit] max process count : 1
[junit] states : 3
[junit] states saved : 4
[junit] state matches : 0
[junit] transitions : 2
[junit] trace steps : 2
[junit] valid calls : 1
[junit] provers : cvc4, z3
[junit] prover calls : 0
[junit]
[junit] === Result ===
[junit] The standard properties hold for all executions.
[junit]
[junit] cvc4 assumptions 0:
[junit] X_N : INT;
[junit] (0) <= ((X_N) + (-1))
[junit]
[junit] cvc4 predicate 0:
[junit] (NOT(((0) = (IF ((0) <= ((X_N) + (-4))) THEN ((X_N) + (-3)) ELSE ((X_N) + (3)) ENDIF)))) AND (NOT(((0) = (IF ((0) <= ((X_N) + (-3))) THEN ((X_N) + (-2)) ELSE ((X_N) + (2)) ENDIF)))) AND (NOT(((0) = (IF ((0) <= ((X_N) + (-2))) THEN ((X_N) + (-1)) ELSE ((X_N) + (1)) ENDIF))))
[junit]
[junit] cvc4 result 0: YES
[junit] ------------- ---------------- ---------------
[junit] ------------- Standard Error -----------------
[junit] Warning: ignoring a division by zero
[junit] ------------- ---------------- ---------------
[junit] Testsuite: edu.udel.cis.vsl.civl.LibraryTest
[junit] Tests run: 72, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 10.711 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.ModelBuilderTest
[junit] Tests run: 15, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 1.059 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.PORTest
[junit] Tests run: 15, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 1.015 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.QuietOptionTest
[junit] Tests run: 5, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 2.911 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.ReasoningTest
[junit] Tests run: 9, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 1.91 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.ReplayTest
[junit] Tests run: 1, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.126 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.RobustnessTest
[junit] Tests run: 1, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.055 sec
[junit]
[junit] ------------- Standard Output ---------------
[junit] CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl
[junit]
[junit] === Source files ===
[junit] missing_source_file.cvl (examples/robustness/missing_source_file.cvl)
[junit]
[junit]
[junit] === Command ===
[junit] civl verify examples/robustness/missing_source_file.cvl
[junit]
[junit] === Stats ===
[junit] time (s) : 0.06
[junit] memory (bytes) : 811597824
[junit] max process count : 1
[junit] states : 9
[junit] states saved : 5
[junit] state matches : 0
[junit] transitions : 8
[junit] trace steps : 2
[junit] valid calls : 3
[junit] provers : cvc4, z3
[junit] prover calls : 0
[junit]
[junit] === Result ===
[junit] The standard properties hold for all executions.
[junit] ------------- ---------------- ---------------
[junit] Testsuite: edu.udel.cis.vsl.civl.ShowStatesTest
[junit] Tests run: 2, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.106 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.SimpleMPITest
[junit] Tests run: 23, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 44.115 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.SpecialStatementsTest
[junit] Tests run: 7, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.336 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.SvcompTest
[junit] Tests run: 4, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 1.054 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.VerifyThisTest
[junit] Tests run: 12, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 22.141 sec
[junit]
[junit] ------------- Standard Output ---------------
[junit] CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl
[junit]
[junit] === Source files ===
[junit] driver.cvl (examples/verifyThis/treeBuffer/driver.cvl)
[junit] treebuffer.h (examples/verifyThis/treeBuffer/treebuffer.h)
[junit] treebuffer_naive.cvl (examples/verifyThis/treeBuffer/treebuffer_naive.cvl)
[junit] treebuffer.cvl (examples/verifyThis/treeBuffer/treebuffer.cvl)
[junit]
[junit]
[junit] === Command ===
[junit] civl compare -checkMemoryLeak=false -inputN=3 -spec examples/verifyThis/treeBuffer/driver.cvl examples/verifyThis/treeBuffer/treebuffer_naive.cvl -impl examples/verifyThis/treeBuffer/driver.cvl examples/verifyThis/treeBuffer/treebuffer.cvl
[junit]
[junit] === Stats ===
[junit] time (s) : 1.38
[junit] memory (bytes) : 885522432
[junit] max process count : 1
[junit] states : 8839
[junit] states saved : 3952
[junit] state matches : 0
[junit] transitions : 8838
[junit] trace steps : 2769
[junit] valid calls : 15326
[junit] provers : cvc4, z3
[junit] prover calls : 48
[junit]
[junit] === Result ===
[junit] The standard properties hold for all executions.
[junit] ------------- ---------------- ---------------
[junit] Testsuite: edu.udel.cis.vsl.civl.transform.ACSLTransformTest
[junit] Tests run: 6, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.242 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.transform.CompareTest
[junit] Tests run: 15, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 95.392 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.transform.ContractTest
[junit] Tests run: 6, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 17.103 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.transform.CudaTest
[junit] Tests run: 3, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 7.374 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.transform.GenTransformerTest
[junit] Tests run: 3, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 2.605 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.transform.IOTransformerTest
[junit] Tests run: 4, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 1.256 sec
[junit]
[junit] ------------- Standard Output ---------------
[junit] CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl
[junit]
[junit] === Source files ===
[junit] printf.cvl (examples/io/printf.cvl)
[junit]
[junit]
[junit] === Command ===
[junit] civl verify -enablePrintf=false examples/io/printf.cvl
[junit]
[junit] === Stats ===
[junit] time (s) : 0.13
[junit] memory (bytes) : 912785408
[junit] max process count : 1
[junit] states : 7
[junit] states saved : 5
[junit] state matches : 0
[junit] transitions : 6
[junit] trace steps : 3
[junit] valid calls : 2
[junit] provers : cvc4, z3
[junit] prover calls : 0
[junit]
[junit] === Result ===
[junit] The standard properties hold for all executions.
[junit] CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl
[junit]
[junit] === Source files ===
[junit] fscanf.cvl (examples/io/fscanf.cvl)
[junit]
[junit]
[junit] === Command ===
[junit] civl verify examples/io/fscanf.cvl
[junit]
[junit] === Stats ===
[junit] time (s) : 0.14
[junit] memory (bytes) : 912785408
[junit] max process count : 1
[junit] states : 49
[junit] states saved : 44
[junit] state matches : 0
[junit] transitions : 48
[junit] trace steps : 28
[junit] valid calls : 152
[junit] provers : cvc4, z3
[junit] prover calls : 0
[junit]
[junit] === Result ===
[junit] The standard properties hold for all executions.
[junit] //================= textFileLengthSpec.cvl =================
[junit] $system[textFileLengthSpec] void $assert(_Bool expression, ...);
[junit] $system[textFileLengthSpec] _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] //================= textFileLengthSpec.cvl =================
[junit] int $system_spec() {
[junit] typedef struct $scope $scope;
[junit] /*@ depends_on \nothing;
[junit] @ executes_when $true;
[junit] @*/
[junit] $system[civlc] void* $malloc($scope s, int size);
[junit] /*@ depends_on \access(p);
[junit] @ executes_when $true;
[junit] @*/
[junit] $system[civlc] void $free(void* p);
[junit] typedef enum _CIVL_File_mode{
[junit] CIVL_FILE_MODE_R,
[junit] CIVL_FILE_MODE_W,
[junit] CIVL_FILE_MODE_WX,
[junit] CIVL_FILE_MODE_A,
[junit] CIVL_FILE_MODE_RB,
[junit] CIVL_FILE_MODE_WB,
[junit] CIVL_FILE_MODE_WBX,
[junit] CIVL_FILE_MODE_AB,
[junit] CIVL_FILE_MODE_RP,
[junit] CIVL_FILE_MODE_WP,
[junit] CIVL_FILE_MODE_WPX,
[junit] CIVL_FILE_MODE_AP,
[junit] CIVL_FILE_MODE_RPB,
[junit] CIVL_FILE_MODE_WPB,
[junit] CIVL_FILE_MODE_WPBX,
[junit] CIVL_FILE_MODE_APB
[junit] } CIVL_File_mode;
[junit] typedef struct FILE FILE;
[junit] typedef struct $file $file;
[junit] typedef struct CIVL_filesystem* $filesystem;
[junit] /*@ depends_on \nothing;
[junit] @ executes_when $true;
[junit] @*/
[junit] $atomic_f $filesystem $filesystem_create($scope scope);
[junit] /*@ depends_on \access(fs);
[junit] @ executes_when $true;
[junit] @*/
[junit] $system[stdio] void $filesystem_destroy($filesystem fs);
[junit] /*@ depends_on \access(fs, filename);
[junit] @ executes_when $true;
[junit] @*/
[junit] $system[stdio] FILE* $fopen($filesystem fs, char* restrict filename, CIVL_File_mode mode);
[junit] struct CIVL_filesystem* _io_filesystem = $filesystem_create($here);
[junit] struct $file _io_output_filesystem[];
[junit] struct FILE* stdout = $fopen(_io_filesystem, "_stdout", CIVL_FILE_MODE_WX);
[junit] struct FILE* stdin = $fopen(_io_filesystem, "_stdin", CIVL_FILE_MODE_R);
[junit] struct FILE* stderr = $fopen(_io_filesystem, "_stderr", CIVL_FILE_MODE_WX);
[junit] /*@ depends_on \access(file);
[junit] @ executes_when $true;
[junit] @*/
[junit] $system[stdio] int $civl_text_file_length($filesystem fs, char* file);
[junit] /*@ depends_on \access(fs, output);
[junit] @ executes_when $true;
[junit] @*/
[junit] $system[stdio] void $filesystem_copy_output($filesystem fs, $file* output);
[junit] void $spec_main() {
[junit] FILE* file = $fopen(_io_filesystem, "fooaaa", CIVL_FILE_MODE_R);
[junit] int fooLength = $civl_text_file_length(_io_filesystem, "foo");
[junit] $free(file);
[junit] {
[junit] $filesystem_copy_output(_io_filesystem, _io_output_filesystem);
[junit] $filesystem_destroy(_io_filesystem);
[junit] if (stdout != (void*)0)
[junit] $free(stdout);
[junit] if (stdin != (void*)0)
[junit] $free(stdin);
[junit] if (stderr != (void*)0)
[junit] $free(stderr);
[junit] }
[junit] }
[junit] /*@ depends_on \access(array, value);
[junit] @ executes_when $true;
[junit] @*/
[junit] $system[seq] void $seq_init(void* array, int count, void* value);
[junit] struct $file{
[junit] char name[];
[junit] char contents[][];
[junit] int isOutput;
[junit] int isInput;
[junit] int isBinary;
[junit] int isWide;
[junit] int length;
[junit] };
[junit] struct CIVL_filesystem{
[junit] $scope scope;
[junit] $file files[];
[junit] };
[junit] struct FILE{
[junit] $file* file;
[junit] $filesystem fs;
[junit] int pos1;
[junit] int pos2;
[junit] CIVL_File_mode mode;
[junit] int isOpen;
[junit] };
[junit] /*@ depends_on \nothing;
[junit] @ assigns \nothing;
[junit] @ reads \nothing;
[junit] @ executes_when $true;
[junit] @*/
[junit] $filesystem $filesystem_create($scope scope) {
[junit] $filesystem fileSys = ($filesystem)($malloc(scope, sizeof(struct CIVL_filesystem)));
[junit] (fileSys)->scope = scope;
[junit] $seq_init(&((fileSys)->files), 0, (void*)0);
[junit] return fileSys;
[junit] }
[junit] $spec_main();
[junit] }
[junit] //================= textFileLengthImpl.cvl =================
[junit] int $system_impl() {
[junit] typedef struct $scope $scope;
[junit] /*@ depends_on \nothing;
[junit] @ executes_when $true;
[junit] @*/
[junit] $system[civlc] void* $malloc($scope s, int size);
[junit] /*@ depends_on \access(p);
[junit] @ executes_when $true;
[junit] @*/
[junit] $system[civlc] void $free(void* p);
[junit] typedef enum _CIVL_File_mode{
[junit] CIVL_FILE_MODE_R,
[junit] CIVL_FILE_MODE_W,
[junit] CIVL_FILE_MODE_WX,
[junit] CIVL_FILE_MODE_A,
[junit] CIVL_FILE_MODE_RB,
[junit] CIVL_FILE_MODE_WB,
[junit] CIVL_FILE_MODE_WBX,
[junit] CIVL_FILE_MODE_AB,
[junit] CIVL_FILE_MODE_RP,
[junit] CIVL_FILE_MODE_WP,
[junit] CIVL_FILE_MODE_WPX,
[junit] CIVL_FILE_MODE_AP,
[junit] CIVL_FILE_MODE_RPB,
[junit] CIVL_FILE_MODE_WPB,
[junit] CIVL_FILE_MODE_WPBX,
[junit] CIVL_FILE_MODE_APB
[junit] } CIVL_File_mode;
[junit] typedef struct FILE FILE;
[junit] typedef struct $file $file;
[junit] typedef struct CIVL_filesystem* $filesystem;
[junit] /*@ depends_on \nothing;
[junit] @ executes_when $true;
[junit] @*/
[junit] $atomic_f $filesystem $filesystem_create($scope scope);
[junit] /*@ depends_on \access(fs);
[junit] @ executes_when $true;
[junit] @*/
[junit] $system[stdio] void $filesystem_destroy($filesystem fs);
[junit] /*@ depends_on \access(fs, filename);
[junit] @ executes_when $true;
[junit] @*/
[junit] $system[stdio] FILE* $fopen($filesystem fs, char* restrict filename, CIVL_File_mode mode);
[junit] struct CIVL_filesystem* _io_filesystem = $filesystem_create($here);
[junit] struct $file _io_output_filesystem[];
[junit] struct FILE* stdout = $fopen(_io_filesystem, "_stdout", CIVL_FILE_MODE_WX);
[junit] struct FILE* stdin = $fopen(_io_filesystem, "_stdin", CIVL_FILE_MODE_R);
[junit] struct FILE* stderr = $fopen(_io_filesystem, "_stderr", CIVL_FILE_MODE_WX);
[junit] /*@ depends_on \access(fs, output);
[junit] @ executes_when $true;
[junit] @*/
[junit] $system[stdio] void $filesystem_copy_output($filesystem fs, $file* output);
[junit] void $impl_main() {
[junit] FILE* file = $fopen(_io_filesystem, "foo", CIVL_FILE_MODE_R);
[junit] $free(file);
[junit] {
[junit] $filesystem_copy_output(_io_filesystem, _io_output_filesystem);
[junit] $filesystem_destroy(_io_filesystem);
[junit] if (stdout != (void*)0)
[junit] $free(stdout);
[junit] if (stdin != (void*)0)
[junit] $free(stdin);
[junit] if (stderr != (void*)0)
[junit] $free(stderr);
[junit] }
[junit] }
[junit] /*@ depends_on \access(array, value);
[junit] @ executes_when $true;
[junit] @*/
[junit] $system[seq] void $seq_init(void* array, int count, void* value);
[junit] struct $file{
[junit] char name[];
[junit] char contents[][];
[junit] int isOutput;
[junit] int isInput;
[junit] int isBinary;
[junit] int isWide;
[junit] int length;
[junit] };
[junit] struct CIVL_filesystem{
[junit] $scope scope;
[junit] $file files[];
[junit] };
[junit] struct FILE{
[junit] $file* file;
[junit] $filesystem fs;
[junit] int pos1;
[junit] int pos2;
[junit] CIVL_File_mode mode;
[junit] int isOpen;
[junit] };
[junit] /*@ depends_on \nothing;
[junit] @ assigns \nothing;
[junit] @ reads \nothing;
[junit] @ executes_when $true;
[junit] @*/
[junit] $filesystem $filesystem_create($scope scope) {
[junit] $filesystem fileSys = ($filesystem)($malloc(scope, sizeof(struct CIVL_filesystem)));
[junit] (fileSys)->scope = scope;
[junit] $seq_init(&((fileSys)->files), 0, (void*)0);
[junit] return fileSys;
[junit] }
[junit] $impl_main();
[junit] }
[junit] //================= textFileLengthSpec.cvl =================
[junit] void main() {
[junit] _Bool _isEqual;
[junit] $system_spec();
[junit] $system_impl();
[junit] }
[junit] ------------- ---------------- ---------------
[junit] Testsuite: edu.udel.cis.vsl.civl.transform.LoopInvariantsNoAssignsTest
[junit] Tests run: 1, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.508 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.transform.MPICollectivePart1Test
[junit] Tests run: 20, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 36.48 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.transform.MPICollectivePart2Test
[junit] Tests run: 25, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 51.299 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.transform.MPITranslationTest
[junit] Tests run: 23, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 50.368 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.transform.MPI_OpenMPTest
[junit] Tests run: 3, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 7.1 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.transform.OmpHelpersTest
[junit] Tests run: 9, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 2.909 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.transform.OpenMP2CIVLTransformerTest
[junit] Tests run: 11, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 17.774 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.transform.PthreadTest
[junit] Tests run: 15, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 7.546 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.transform.PthreadThreaderTest
[junit] Tests run: 8, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 3.348 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.transform.SideEffectsTest
[junit] Tests run: 10, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.457 sec
[junit]
[junitreport] Processing /usa/svn/work/civl/1.17/r4979/junit/data/TESTS-TestSuites.xml to /tmp/null1251858831
[junitreport] Loading stylesheet jar:file:/usr/share/ant/lib/ant-junit.jar!/org/apache/tools/ant/taskdefs/optional/junit/xsl/junit-frames.xsl
[junitreport] Warning: org.apache.xerces.jaxp.SAXParserImpl$JAXPSAXParser: Property 'http://javax.xml.XMLConstants/property/accessExternalDTD' is not recognized.
[junitreport] Warning: org.apache.xerces.jaxp.SAXParserImpl$JAXPSAXParser: Property 'http://www.oracle.com/xml/jaxp/properties/entityExpansionLimit' is not recognized.
[junitreport] Transform time: 488ms
[junitreport] Deleting: /tmp/null1251858831
test:
[jacoco:report] Loading execution data file /usa/svn/work/civl/1.17/r4979/jacoco.exec
[jacoco:report] Writing bundle 'Test Coverage Report for CIVL 1.17 r4979 Regression Suite' with 543 classes
javadoc:
[mkdir] Created dir: /usa/svn/work/civl/1.17/r4979/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.gui.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 1.8.0_161
[javadoc] Building tree for all the packages and classes...
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/analysis/IF/CodeAnalyzer.java:21: warning: no description for @param
[javadoc] * @param state
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/analysis/IF/CodeAnalyzer.java:22: warning: no description for @param
[javadoc] * @param pid
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/analysis/IF/CodeAnalyzer.java:23: warning: no description for @param
[javadoc] * @param statement
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/analysis/IF/CodeAnalyzer.java:24: warning: no description for @param
[javadoc] * @param argumentValues
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/analysis/IF/CodeAnalyzer.java:33: warning: no description for @param
[javadoc] * @param statement
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/analysis/IF/CodeAnalyzer.java:40: warning: no description for @param
[javadoc] * @param out
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/config/IF/CIVLConfiguration.java:773: warning: no @return
[javadoc] public int getProcBound() {
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/dynamic/IF/Dynamics.java:26: warning: no @param for stateFactory
[javadoc] public static SymbolicUtility newSymbolicUtility(SymbolicUniverse universe,
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/dynamic/IF/DynamicWriteSet.java:70: warning: no description for @param
[javadoc] * @param operator
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/dynamic/IF/DynamicWriteSet.java:34: error: reference not found
[javadoc] * {@link ImmutableStateFactory#deallocate(edu.udel.cis.vsl.civl.state.IF.State, SymbolicExpression, int, int, int)}
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/dynamic/IF/DynamicWriteSet.java:36: error: tag not allowed here: <br>
[javadoc] * <li>executeMalloc and malloc in {@link CommonExecutor}</li> <br>
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/dynamic/IF/DynamicWriteSet.java:36: error: text not allowed in <ul> element
[javadoc] * <li>executeMalloc and malloc in {@link CommonExecutor}</li> <br>
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/dynamic/IF/DynamicWriteSet.java:45: error: unexpected end tag: </p>
[javadoc] * </p>
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/dynamic/IF/DynamicWriteSet.java:49: warning - Tag @link: can't find deallocate(edu.udel.cis.vsl.civl.state.IF.State, SymbolicExpression, int, int, int) in edu.udel.cis.vsl.civl.state.common.immutable.ImmutableStateFactory
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:308: error: reference not found
[javadoc] * {@link #isPointerToHeap(heapPointer)} must returns true.
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:361: error: semicolon missing
[javadoc] * pointer. For example, given a pointer &a[5] and a reference [0], the
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:362: error: semicolon missing
[javadoc] * result will be &a[0]. The given pointer can refer to a heap object, in
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:609: error: tag not allowed here: <li>
[javadoc] * <li>length(array_extents) > 0</li>
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:609: error: bad use of '>'
[javadoc] * <li>length(array_extents) > 0</li>
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:610: error: unexpected end tag: </p>
[javadoc] * </p>
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:619: error: bad use of '>'
[javadoc] * @return Sizes of all array slices. e.g. input:{2,3,4} ==> output:{12, 4,
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:621: error: exception not thrown: edu.udel.cis.vsl.civl.state.IF.UnsatisfiablePathConditionException
[javadoc] * @throws UnsatisfiablePathConditionException
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:621: warning: no description for @throws
[javadoc] * @throws UnsatisfiablePathConditionException
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:698: warning: no description for @param
[javadoc] * @param domain
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:706: warning: no description for @param
[javadoc] * @param range
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:716: warning: no description for @param
[javadoc] * @param domain
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:717: warning: no description for @param
[javadoc] * @param index
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:728: warning: no description for @param
[javadoc] * @param range
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:738: warning: no description for @param
[javadoc] * @param range
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:749: warning: no description for @param
[javadoc] * @param range
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:757: warning: no description for @param
[javadoc] * @param domain
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:764: error: bad HTML entity
[javadoc] * clause is <code> X==3 && Y<5 && (a[k]>2 || k<0) </code>, then the result
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:764: error: bad HTML entity
[javadoc] * clause is <code> X==3 && Y<5 && (a[k]>2 || k<0) </code>, then the result
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:764: error: malformed HTML
[javadoc] * clause is <code> X==3 && Y<5 && (a[k]>2 || k<0) </code>, then the result
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:764: error: bad HTML entity
[javadoc] * clause is <code> X==3 && Y<5 && (a[k]>2 || k<0) </code>, then the result
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:764: error: bad HTML entity
[javadoc] * clause is <code> X==3 && Y<5 && (a[k]>2 || k<0) </code>, then the result
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:764: error: bad use of '>'
[javadoc] * clause is <code> X==3 && Y<5 && (a[k]>2 || k<0) </code>, then the result
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:764: error: malformed HTML
[javadoc] * clause is <code> X==3 && Y<5 && (a[k]>2 || k<0) </code>, then the result
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:765: error: malformed HTML
[javadoc] * is an array of clauses:<code>{ X==3, Y<5, a[k]>2 || k<0}</code>
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:765: error: bad use of '>'
[javadoc] * is an array of clauses:<code>{ X==3, Y<5, a[k]>2 || k<0}</code>
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:765: error: malformed HTML
[javadoc] * is an array of clauses:<code>{ X==3, Y<5, a[k]>2 || k<0}</code>
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:767: warning: no description for @param
[javadoc] * @param cnfClause
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:775: warning: no description for @param
[javadoc] * @param function
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:776: error: @param name not found
[javadoc] * @param arguments
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:776: warning: no description for @param
[javadoc] * @param arguments
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:777: warning: no description for @return
[javadoc] * @return
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:779: warning: no @param for library
[javadoc] SymbolicExpression getAbstractGuardOfFunctionCall(String library,
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:779: warning: no @param for argumentValues
[javadoc] SymbolicExpression getAbstractGuardOfFunctionCall(String library,
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:789: warning: no description for @param
[javadoc] * @param originalFunction
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:790: warning: no description for @param
[javadoc] * @param argument
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:791: warning: no description for @return
[javadoc] * @return
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:803: warning: no description for @param
[javadoc] * @param range
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:804: warning: no description for @return
[javadoc] * @return
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:806: warning: no @param for reasoner
[javadoc] BitSet range2BitSet(SymbolicExpression range, Reasoner reasoner);
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:818: warning: no description for @param
[javadoc] * @param pointer
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:819: warning: no description for @return
[javadoc] * @return
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:311: warning - Tag @link: can't find isPointerToHeap(heapPointer) in edu.udel.cis.vsl.civl.dynamic.IF.SymbolicUtility
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/gui/IF/CIVL_GUI.java:101: error: @param name not found
[javadoc] * @param transitions
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/gui/IF/CIVL_GUI.java:104: warning: no @param for trace
[javadoc] public CIVL_GUI(Trace<Transition, State> trace,
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/gui/IF/CIVL_GUI.java:104: warning: no @param for symbolicAnalyzer
[javadoc] public CIVL_GUI(Trace<Transition, State> trace,
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/kripke/IF/Kripkes.java:43: warning: no @param for executor
[javadoc] public static Enabler newEnabler(StateFactory stateFactory,
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/kripke/IF/Kripkes.java:43: warning: no @param for gmcConfig
[javadoc] public static Enabler newEnabler(StateFactory stateFactory,
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/kripke/IF/LibraryEnabler.java:54: warning: no description for @param
[javadoc] * @param reachablePtrWritableMap
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/kripke/IF/LibraryEnabler.java:55: warning: no description for @param
[javadoc] * @param reachablePtrReadonlyMap
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/kripke/IF/LibraryEnabler.java:56: warning: no description for @param
[javadoc] * @param reachableNonPtrWritableMap
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/kripke/IF/LibraryEnabler.java:57: warning: no description for @param
[javadoc] * @param reachableNonPtrReadonlyMap
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/kripke/IF/LibraryEnabler.java:58: error: @param name not found
[javadoc] * @param reachableMemUnitsMap
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/kripke/IF/LibraryEnabler.java:61: warning: no description for @throws
[javadoc] * @throws UnsatisfiablePathConditionException
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/kripke/IF/LibraryEnabler.java:87: warning: no description for @throws
[javadoc] * @throws UnsatisfiablePathConditionException
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/kripke/IF/LibraryEnablerLoader.java:35: warning: no description for @throws
[javadoc] * @throws LibraryLoaderException
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/kripke/IF/TraceStep.java:58: error: unknown tag: returns
[javadoc] * @returns the final state of this trace step. If the final state has not
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/log/IF/CIVLErrorLogger.java:104: error: bad HTML entity
[javadoc] * <li>pcsat=YES && condsat=NO : certainty=PROVEABLE</li>
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/log/IF/CIVLErrorLogger.java:104: error: bad HTML entity
[javadoc] * <li>pcsat=YES && condsat=NO : certainty=PROVEABLE</li>
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/log/IF/CIVLErrorLogger.java:105: error: bad HTML entity
[javadoc] * <li>pcsat=YES && condsat=MAYBE : certainty=MAYBE</li>
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/log/IF/CIVLErrorLogger.java:105: error: bad HTML entity
[javadoc] * <li>pcsat=YES && condsat=MAYBE : certainty=MAYBE</li>
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/log/IF/CIVLErrorLogger.java:106: error: bad HTML entity
[javadoc] * <li>pcsat=MAYBE && condsat=NO : certainty=MAYBE</li>
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/log/IF/CIVLErrorLogger.java:106: error: bad HTML entity
[javadoc] * <li>pcsat=MAYBE && condsat=NO : certainty=MAYBE</li>
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/log/IF/CIVLErrorLogger.java:107: error: bad HTML entity
[javadoc] * <li>pcsat=MAYBE && condsat=MAYBE : certainty=MAYBE</li>
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/log/IF/CIVLErrorLogger.java:107: error: bad HTML entity
[javadoc] * <li>pcsat=MAYBE && condsat=MAYBE : certainty=MAYBE</li>
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/log/IF/CIVLErrorLogger.java:110: error: unexpected end tag: </p>
[javadoc] * </p>
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/log/IF/CIVLErrorLogger.java:121: error: @param name not found
[javadoc] * @param process
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/log/IF/CIVLErrorLogger.java:150: warning: no @param for pid
[javadoc] public State logError(CIVLSource source, State state, int pid,
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/log/IF/CIVLErrorLogger.java:64: warning: no description for @param
[javadoc] * @param directory
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/log/IF/CIVLErrorLogger.java:65: warning: no description for @param
[javadoc] * @param sessionName
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/log/IF/CIVLErrorLogger.java:66: warning: no description for @param
[javadoc] * @param out
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/log/IF/CIVLErrorLogger.java:67: error: @param name not found
[javadoc] * @param config
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/log/IF/CIVLErrorLogger.java:67: warning: no description for @param
[javadoc] * @param config
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/log/IF/CIVLErrorLogger.java:68: warning: no description for @param
[javadoc] * @param universe
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/log/IF/CIVLErrorLogger.java:69: warning: no description for @param
[javadoc] * @param solve
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/log/IF/CIVLErrorLogger.java:71: warning: no @param for civlConfig
[javadoc] public CIVLErrorLogger(File directory, String sessionName, PrintStream out,
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/log/IF/CIVLErrorLogger.java:71: warning: no @param for gmcConfig
[javadoc] public CIVLErrorLogger(File directory, String sessionName, PrintStream out,
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/log/IF/CIVLErrorLogger.java:71: warning: no @param for stateFactory
[javadoc] public CIVLErrorLogger(File directory, String sessionName, PrintStream out,
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/log/IF/CIVLExecutionException.java:47: error: @param name not found
[javadoc] * @param stateString
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/log/IF/CIVLExecutionException.java:53: warning: no @param for state
[javadoc] public CIVLExecutionException(ErrorKind kind, Certainty certainty,
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/CIVLFunction.java:185: error: bad use of '>'
[javadoc] * location to the target of the no-op location. For example, let l(s->l',
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/CIVLFunction.java:186: error: bad use of '>'
[javadoc] * ...) be a location l with statement s going to l' ... l1 (s1 -> l2, s2 ->
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/CIVLFunction.java:186: error: bad use of '>'
[javadoc] * ...) be a location l with statement s going to l' ... l1 (s1 -> l2, s2 ->
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/CIVLFunction.java:187: error: bad use of '>'
[javadoc] * l3), l2 ([true]no-op -> l4), l3(), l(4) After applying simplify(), should
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/CIVLFunction.java:188: error: bad use of '>'
[javadoc] * be l1 (s1 -> l4, s2 -> l3), l3(), l4()
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/CIVLFunction.java:188: error: bad use of '>'
[javadoc] * be l1 (s1 -> l4, s2 -> l3), l3(), l4()
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/CIVLFunction.java:245: warning: no description for @return
[javadoc] * @return
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/CIVLFunction.java:294: warning: no description for @return
[javadoc] * @return
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/CIVLFunction.java:304: warning: no description for @param
[javadoc] * @param validConsequences
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/CIVLFunction.java:314: error: @param name not found
[javadoc] * @param validConsequences
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/CIVLFunction.java:314: warning: no description for @param
[javadoc] * @param validConsequences
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/CIVLFunction.java:316: warning: no @return
[javadoc] List<Pair<Expression, Integer>> getPossibleValidConsequences();
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/CIVLFunction.java:321: warning: no description for @return
[javadoc] * @return
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/CIVLFunction.java:328: warning: no description for @return
[javadoc] * @return
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/CIVLFunction.java:335: warning: no description for @param
[javadoc] * @param contract
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/CIVLFunction.java:346: warning: no description for @return
[javadoc] * @return
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/CIVLFunction.java:353: warning: no description for @param
[javadoc] * @param value
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/CIVLFunction.java:360: warning: no description for @param
[javadoc] * @param value
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/CIVLSource.java:34: warning: no @return
[javadoc] String getLocation();
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/CIVLSource.java:42: warning: no description for @return
[javadoc] * @return
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/CIVLTypeFactory.java:110: warning: no description for @param
[javadoc] * @param rangeType
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/CIVLTypeFactory.java:168: error: bad use of '>'
[javadoc] * Create a new location. ======= Get the integer primitive type. >>>>>>>
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/CIVLTypeFactory.java:168: error: bad use of '>'
[javadoc] * Create a new location. ======= Get the integer primitive type. >>>>>>>
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/CIVLTypeFactory.java:168: error: bad use of '>'
[javadoc] * Create a new location. ======= Get the integer primitive type. >>>>>>>
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/CIVLTypeFactory.java:168: error: bad use of '>'
[javadoc] * Create a new location. ======= Get the integer primitive type. >>>>>>>
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/CIVLTypeFactory.java:168: error: bad use of '>'
[javadoc] * Create a new location. ======= Get the integer primitive type. >>>>>>>
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/CIVLTypeFactory.java:168: error: bad use of '>'
[javadoc] * Create a new location. ======= Get the integer primitive type. >>>>>>>
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/CIVLTypeFactory.java:168: error: bad use of '>'
[javadoc] * Create a new location. ======= Get the integer primitive type. >>>>>>>
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/CIVLTypeFactory.java:343: warning: no description for @param
[javadoc] * @param type
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/CIVLTypeFactory.java:344: warning: no description for @param
[javadoc] * @param id
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/CIVLTypeFactory.java:423: error: @param name not found
[javadoc] * @param universe
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/CIVLTypeFactory.java:425: error: @param name not found
[javadoc] * @param the
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/CIVLTypeFactory.java:429: warning: no @param for dynamicType
[javadoc] NumericExpression sizeofDynamicType(SymbolicType dynamicType);
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/CIVLTypeFactory.java:465: error: @param name not found
[javadoc] * @param expr
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/CIVLTypeFactory.java:471: warning: no @param for typeId
[javadoc] CIVLType getStaticTypeOfDynamicType(SymbolicExpression typeId);
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/Fragment.java:97: error: tag not allowed here: <dt>
[javadoc] * the second fragment to be combined with <dt>
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/Fragment.java:99: error: tag not allowed here: <dd>
[javadoc] * <dd>
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/Model.java:27: warning: no description for @return
[javadoc] * @return
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/Model.java:169: warning: no description for @param
[javadoc] * @param value
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/Model.java:209: warning: no description for @return
[javadoc] * @return
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/ModelBuilder.java:34: warning: no description for @param
[javadoc] * @param debugging
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/ModelBuilder.java:35: warning: no description for @param
[javadoc] * @param debugOut
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:130: error: semicolon missing
[javadoc] * Returns a new address-of expression <code>(&e)</code> with given operand.
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:158: error: malformed HTML
[javadoc] * A binary expression. One of {+,-,*,\,<,<=,==,!=,&&,||,%}
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:158: error: malformed HTML
[javadoc] * A binary expression. One of {+,-,*,\,<,<=,==,!=,&&,||,%}
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:158: error: bad HTML entity
[javadoc] * A binary expression. One of {+,-,*,\,<,<=,==,!=,&&,||,%}
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:158: error: bad HTML entity
[javadoc] * A binary expression. One of {+,-,*,\,<,<=,==,!=,&&,||,%}
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:194: warning: no description for @param
[javadoc] * @param expression
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:317: warning: no description for @param
[javadoc] * @param source
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:318: warning: no description for @param
[javadoc] * @param function
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:325: warning: no description for @param
[javadoc] * @param source
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:340: warning: no description for @param
[javadoc] * @param source
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:341: warning: no description for @param
[javadoc] * @param variable
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:443: error: @param name not found
[javadoc] * @param boundVariableList
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:450: warning: no @param for variable
[javadoc] LambdaExpression lambdaExpression(CIVLSource source,
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:456: warning: no description for @param
[javadoc] * @param source
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:457: warning: no description for @param
[javadoc] * @param type
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:458: warning: no description for @param
[javadoc] * @param quant
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:459: warning: no description for @param
[javadoc] * @param lo
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:460: warning: no description for @param
[javadoc] * @param hi
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:461: warning: no description for @param
[javadoc] * @param function
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:462: warning: no description for @return
[javadoc] * @return
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:483: error: bad use of '>'
[javadoc] * <code>(high-low)/step >= 0 </code>.
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:502: error: malformed HTML
[javadoc] * the domain, and <code>ri (where 1 <= i <= m)</code> is a range expression
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:502: error: malformed HTML
[javadoc] * the domain, and <code>ri (where 1 <= i <= m)</code> is a range expression
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:632: warning: no description for @param
[javadoc] * @param callStatement
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:651: error: bad HTML entity
[javadoc] * <code>sysCall.isCall == true && sysCall.isSystemCall() == true</code>.
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:651: error: bad HTML entity
[javadoc] * <code>sysCall.isCall == true && sysCall.isSystemCall() == true</code>.
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:727: warning: no description for @param
[javadoc] * @param source
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:728: warning: no description for @param
[javadoc] * @param function
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:729: warning: no description for @param
[javadoc] * @param degree
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:730: warning: no description for @param
[javadoc] * @param lowerBounds
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:731: warning: no description for @param
[javadoc] * @param upperBounds
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:732: warning: no description for @return
[javadoc] * @return
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:1021: error: reference not found
[javadoc] * {@link #noopStatement(CIVLSource, Location)}.
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:1454: error: @param name not found
[javadoc] * @param source
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:1456: error: @param name not found
[javadoc] * @param scopeValue
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:1483: error: @param name not found
[javadoc] * @param source
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:1537: error: @param name not found
[javadoc] * @param scope
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:101: error: reference not found
[javadoc] * {@link #function(CIVLSource, Identifier, List, CIVLType, Scope, Location)}. A
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/Scope.java:87: error: @param name not found
[javadoc] * @param A
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/Scope.java:213: error: @param name not found
[javadoc] * @param des
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/contract/FunctionBehavior.java:87: error: reference not found
[javadoc] * Precondition: {@link #numReadsClauses()}==0;
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/contract/FunctionBehavior.java:94: error: reference not found
[javadoc] * Precondition: {@link #numAssignsClauses()}==0;
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/contract/FunctionBehavior.java:101: error: bad HTML entity
[javadoc] * Precondition: {@link #numDependsEvents()}==0 && {@link #dependsAnyact()
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/contract/FunctionBehavior.java:101: error: bad HTML entity
[javadoc] * Precondition: {@link #numDependsEvents()}==0 && {@link #dependsAnyact()
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/contract/FunctionBehavior.java:109: error: ')' missing in reference
[javadoc] * Precondition: {@link #dependsNoact()==false};
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/contract/FunctionBehavior.java:130: error: @param name not found
[javadoc] * @param assigns
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/contract/FunctionBehavior.java:137: error: @param name not found
[javadoc] * @param reads
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/contract/FunctionBehavior.java:145: error: @param name not found
[javadoc] * @param depends
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/contract/FunctionBehavior.java:187: error: @param name not found
[javadoc] * @param subPrefix
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/expression/Expression.java:147: error: semicolon missing
[javadoc] * an address-of expression. e.g., <code>(&a + &b)</code> returns
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/expression/Expression.java:147: error: semicolon missing
[javadoc] * an address-of expression. e.g., <code>(&a + &b)</code> returns
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/expression/Expression.java:159: error: semicolon missing
[javadoc] * e.g., <code>(&a + &b)</code> returns <code>{a, b}</code>.
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/expression/Expression.java:159: error: semicolon missing
[javadoc] * e.g., <code>(&a + &b)</code> returns <code>{a, b}</code>.
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/expression/Expression.java:193: error: malformed HTML
[javadoc] * e.g.: s<$here would return true.
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/expression/Expression.java:203: error: semicolon missing
[javadoc] * any error checking. e.g., &anon[0] which is used to translate array
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/expression/AddressOfExpression.java:7: error: semicolon missing
[javadoc] * the format: <code>&x</code>, where <code>&</code> is the address-of operator
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/expression/AddressOfExpression.java:7: error: bad HTML entity
[javadoc] * the format: <code>&x</code>, where <code>&</code> is the address-of operator
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/expression/BinaryExpression.java:17: error: unknown tag: ui
[javadoc] * <ui>
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/expression/BinaryExpression.java:18: error: tag not allowed here: <li>
[javadoc] * <li>AND: <code>&&</code> (logical and);</li>
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/expression/BinaryExpression.java:18: error: bad HTML entity
[javadoc] * <li>AND: <code>&&</code> (logical and);</li>
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/expression/BinaryExpression.java:18: error: bad HTML entity
[javadoc] * <li>AND: <code>&&</code> (logical and);</li>
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/expression/BinaryExpression.java:19: error: tag not allowed here: <li>
[javadoc] * <li>LEFT_SHIFT: <code><</code> (bitwise left shift);</li>
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/expression/BinaryExpression.java:19: error: malformed HTML
[javadoc] * <li>LEFT_SHIFT: <code><</code> (bitwise left shift);</li>
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.17/r4979/src/edu/udel/cis/vsl/civl/model/IF/expression/BinaryExpression.java:20: error: tag not allowed here: <li>
[javadoc] * <li>RIGHT_SHIFT: <code>>></code> (bitwise right shift);</li>
[javadoc] ^
[javadoc] Building index for all the packages and classes...
[javadoc] Building index for all classes...
[javadoc] Generating /usa/svn/work/civl/1.17/r4979/doc/javadoc/help-doc.html...
[javadoc] 100 errors
[javadoc] 100 warnings
bench-compile:
[javac] Compiling 6 source files to /usa/svn/work/civl/1.17/r4979/bin
bench-scale-compile:
[javac] Compiling 5 source files to /usa/svn/work/civl/1.17/r4979/bin
all:
BUILD SUCCESSFUL
Total time: 9 minutes 34 seconds
Stderr: