CIVL 1.16 Revision 4871

Downloads, Test and Coverage Reports, and Javadocs

Revision Information

Path: .
Working Copy Root Path: /usa/svn/work/civl/1.16/r4871
URL: svn://vsl.cis.udel.edu/civl/tags/1.16
Relative URL: ^/tags/1.16
Repository Root: svn://vsl.cis.udel.edu/civl
Repository UUID: fb995dde-84ed-4084-dfe6-e5aef3e2452c
Revision: 4871
Node Kind: directory
Schedule: normal
Last Changed Author: wuwenhao
Last Changed Rev: 4871
Last Changed Date: 2018-06-01 17:57:20 -0400 (Fri, 01 Jun 2018)

Build output

Stdout:

Buildfile: /usa/svn/work/civl/1.16/r4871/build.xml

checkCommandParserChanges:

CommandParser:
     [move] Moving 1 file to /usa/svn/work/civl/1.16/r4871/src/edu/udel/cis/vsl/civl/run/common
     [move] Moving 1 file to /usa/svn/work/civl/1.16/r4871/src/edu/udel/cis/vsl/civl/run/common
     [move] Moving 1 file to /usa/svn/work/civl/1.16/r4871/src/edu/udel/cis/vsl/civl/run/common
     [move] Moving 1 file to /usa/svn/work/civl/1.16/r4871/src/edu/udel/cis/vsl/civl/run/common

compile:
    [mkdir] Created dir: /usa/svn/work/civl/1.16/r4871/bin
    [javac] Compiling 533 source files to /usa/svn/work/civl/1.16/r4871/bin
    [javac] Creating empty /usa/svn/work/civl/1.16/r4871/bin/edu/udel/cis/vsl/civl/model/IF/expression/package-info.class
    [javac] Creating empty /usa/svn/work/civl/1.16/r4871/bin/edu/udel/cis/vsl/civl/state/IF/package-info.class
    [javac] Creating empty /usa/svn/work/civl/1.16/r4871/bin/edu/udel/cis/vsl/civl/gui/IF/package-info.class
    [javac] Creating empty /usa/svn/work/civl/1.16/r4871/bin/edu/udel/cis/vsl/civl/gui/common/package-info.class
    [javac] Creating empty /usa/svn/work/civl/1.16/r4871/bin/edu/udel/cis/vsl/civl/semantics/IF/package-info.class
    [javac] Creating empty /usa/svn/work/civl/1.16/r4871/bin/edu/udel/cis/vsl/civl/kripke/IF/package-info.class
    [javac] Creating empty /usa/svn/work/civl/1.16/r4871/bin/edu/udel/cis/vsl/civl/util/IF/package-info.class
    [javac] Creating empty /usa/svn/work/civl/1.16/r4871/bin/edu/udel/cis/vsl/civl/library/domain/package-info.class
    [javac] Creating empty /usa/svn/work/civl/1.16/r4871/bin/edu/udel/cis/vsl/civl/model/IF/type/package-info.class
    [javac] Creating empty /usa/svn/work/civl/1.16/r4871/bin/edu/udel/cis/vsl/civl/library/comm/package-info.class
    [javac] Creating empty /usa/svn/work/civl/1.16/r4871/bin/edu/udel/cis/vsl/civl/library/pointer/package-info.class
    [javac] Creating empty /usa/svn/work/civl/1.16/r4871/bin/edu/udel/cis/vsl/civl/model/IF/location/package-info.class
    [javac] Creating empty /usa/svn/work/civl/1.16/r4871/bin/edu/udel/cis/vsl/civl/library/time/package-info.class
    [javac] Creating empty /usa/svn/work/civl/1.16/r4871/bin/edu/udel/cis/vsl/civl/library/pthread/package-info.class
    [javac] Creating empty /usa/svn/work/civl/1.16/r4871/bin/edu/udel/cis/vsl/civl/config/IF/package-info.class
    [javac] Creating empty /usa/svn/work/civl/1.16/r4871/bin/edu/udel/cis/vsl/civl/dynamic/IF/package-info.class
    [javac] Creating empty /usa/svn/work/civl/1.16/r4871/bin/edu/udel/cis/vsl/civl/library/civlc/package-info.class
    [javac] Creating empty /usa/svn/work/civl/1.16/r4871/bin/edu/udel/cis/vsl/civl/log/IF/package-info.class
    [javac] Creating empty /usa/svn/work/civl/1.16/r4871/bin/edu/udel/cis/vsl/civl/library/common/package-info.class
    [javac] Creating empty /usa/svn/work/civl/1.16/r4871/bin/edu/udel/cis/vsl/civl/model/IF/package-info.class
    [javac] Creating empty /usa/svn/work/civl/1.16/r4871/bin/edu/udel/cis/vsl/civl/package-info.class
    [javac] Creating empty /usa/svn/work/civl/1.16/r4871/bin/edu/udel/cis/vsl/civl/model/IF/variable/package-info.class
    [javac] Creating empty /usa/svn/work/civl/1.16/r4871/bin/edu/udel/cis/vsl/civl/library/seq/package-info.class
    [javac] Creating empty /usa/svn/work/civl/1.16/r4871/bin/edu/udel/cis/vsl/civl/library/string/package-info.class
    [javac] Creating empty /usa/svn/work/civl/1.16/r4871/bin/edu/udel/cis/vsl/civl/analysis/IF/package-info.class
    [javac] Creating empty /usa/svn/work/civl/1.16/r4871/bin/edu/udel/cis/vsl/civl/library/scope/package-info.class
    [javac] Creating empty /usa/svn/work/civl/1.16/r4871/bin/edu/udel/cis/vsl/civl/model/IF/statement/package-info.class
    [javac] Creating empty /usa/svn/work/civl/1.16/r4871/bin/edu/udel/cis/vsl/civl/predicate/IF/package-info.class
    [javac] Creating empty /usa/svn/work/civl/1.16/r4871/bin/edu/udel/cis/vsl/civl/library/bundle/package-info.class
    [javac] Creating empty /usa/svn/work/civl/1.16/r4871/bin/edu/udel/cis/vsl/civl/slice/common/package-info.class
    [javac] Creating empty /usa/svn/work/civl/1.16/r4871/bin/edu/udel/cis/vsl/civl/slice/IF/package-info.class
    [javac] Creating empty /usa/svn/work/civl/1.16/r4871/bin/edu/udel/cis/vsl/civl/run/IF/package-info.class
    [javac] Creating empty /usa/svn/work/civl/1.16/r4871/bin/edu/udel/cis/vsl/civl/transform/IF/package-info.class
     [copy] Copying 32 files to /usa/svn/work/civl/1.16/r4871/bin/include

jar:
      [jar] Building jar: /usa/svn/work/civl/1.16/r4871/civl.jar

test-init:
    [mkdir] Created dir: /usa/svn/work/civl/1.16/r4871/junit
    [mkdir] Created dir: /usa/svn/work/civl/1.16/r4871/junit/data
    [mkdir] Created dir: /usa/svn/work/civl/1.16/r4871/junit/reports
    [mkdir] Created dir: /usa/svn/work/civl/1.16/r4871/bin-test/regress

test-compile:
    [javac] Compiling 38 source files to /usa/svn/work/civl/1.16/r4871/bin-test/regress

test-run:
[jacoco:coverage] Enhancing junit with coverage
    [junit] Testsuite: edu.udel.cis.vsl.civl.AnalysisTest
    [junit] Tests run: 3, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 4.693 sec
    [junit] 
    [junit] Testsuite: edu.udel.cis.vsl.civl.ArithmeticTest
    [junit] Tests run: 27, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 11.521 sec
    [junit] 
    [junit] Testsuite: edu.udel.cis.vsl.civl.BackendTest
    [junit] Tests run: 16, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 2.395 sec
    [junit] 
    [junit] Testsuite: edu.udel.cis.vsl.civl.CompareTest
    [junit] Tests run: 5, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 11.694 sec
    [junit] 
    [junit] Testsuite: edu.udel.cis.vsl.civl.ConcurrencyTest
    [junit] Tests run: 34, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 13.463 sec
    [junit] 
    [junit] Testsuite: edu.udel.cis.vsl.civl.LanguageFeaturesTest
    [junit] Tests run: 143, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 19.535 sec
    [junit] 
    [junit] ------------- Standard Output ---------------
    [junit] CIVL v1.16 of 2018-06-01 -- 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)      : 808976384
    [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, cvc3
    [junit]    prover calls        : 0
    [junit] 
    [junit] === Result ===
    [junit] The standard properties hold for all executions.
    [junit] CIVL v1.16 of 2018-06-01 -- 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)      : 820510720
    [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, cvc3
    [junit]    prover calls        : 0
    [junit] 
    [junit] === Result ===
    [junit] The standard properties hold for all executions.
    [junit] CIVL v1.16 of 2018-06-01 -- 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.29
    [junit]    memory (bytes)      : 829423616
    [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, cvc3
    [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) + (-1)))) THEN ((X_N) + (1)) ELSE ((X_N) + (-1)) ENDIF)))) AND (NOT(((0) = (IF (((X_N) + (-3))  <=  (0)) THEN ((X_N) + (3)) ELSE ((X_N) + (-3)) ENDIF)))) AND (NOT(((0) = (IF (((X_N) + (-2))  <=  (0)) THEN ((X_N) + (2)) ELSE ((X_N) + (-2)) 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: 11.83 sec
    [junit] 
    [junit] Testsuite: edu.udel.cis.vsl.civl.ModelBuilderTest
    [junit] Tests run: 15, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 1.011 sec
    [junit] 
    [junit] Testsuite: edu.udel.cis.vsl.civl.PORTest
    [junit] Tests run: 15, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.955 sec
    [junit] 
    [junit] Testsuite: edu.udel.cis.vsl.civl.QuietOptionTest
    [junit] Tests run: 5, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 2.973 sec
    [junit] 
    [junit] Testsuite: edu.udel.cis.vsl.civl.ReasoningTest
    [junit] Tests run: 9, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 1.667 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.113 sec
    [junit] 
    [junit] Testsuite: edu.udel.cis.vsl.civl.RobustnessTest
    [junit] Tests run: 1, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.057 sec
    [junit] 
    [junit] ------------- Standard Output ---------------
    [junit] CIVL v1.16 of 2018-06-01 -- 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)      : 807927808
    [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, cvc3
    [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.144 sec
    [junit] 
    [junit] Testsuite: edu.udel.cis.vsl.civl.SimpleMPITest
    [junit] Tests run: 23, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 46.141 sec
    [junit] 
    [junit] Testsuite: edu.udel.cis.vsl.civl.SpecialStatementsTest
    [junit] Tests run: 7, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.356 sec
    [junit] 
    [junit] Testsuite: edu.udel.cis.vsl.civl.SvcompTest
    [junit] Tests run: 10, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 9.703 sec
    [junit] 
    [junit] Testsuite: edu.udel.cis.vsl.civl.VerifyThisTest
    [junit] Tests run: 12, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 24.889 sec
    [junit] 
    [junit] ------------- Standard Output ---------------
    [junit] CIVL v1.16 of 2018-06-01 -- 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.83
    [junit]    memory (bytes)      : 898629632
    [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         : 15253
    [junit]    provers             : cvc4, z3, cvc3
    [junit]    prover calls        : 72
    [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.312 sec
    [junit] 
    [junit] Testsuite: edu.udel.cis.vsl.civl.transform.CompareTest
    [junit] Tests run: 10, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 49.659 sec
    [junit] 
    [junit] Testsuite: edu.udel.cis.vsl.civl.transform.ContractTest
    [junit] Tests run: 6, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 20.503 sec
    [junit] 
    [junit] Testsuite: edu.udel.cis.vsl.civl.transform.CudaTest
    [junit] Tests run: 3, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 8.115 sec
    [junit] 
    [junit] Testsuite: edu.udel.cis.vsl.civl.transform.GenTransformerTest
    [junit] Tests run: 3, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 2.84 sec
    [junit] 
    [junit] Testsuite: edu.udel.cis.vsl.civl.transform.IOTransformerTest
    [junit] Tests run: 4, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 1.342 sec
    [junit] 
    [junit] ------------- Standard Output ---------------
    [junit] CIVL v1.16 of 2018-06-01 -- 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.14
    [junit]    memory (bytes)      : 946864128
    [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, cvc3
    [junit]    prover calls        : 0
    [junit] 
    [junit] === Result ===
    [junit] The standard properties hold for all executions.
    [junit] CIVL v1.16 of 2018-06-01 -- 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.15
    [junit]    memory (bytes)      : 946864128
    [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, cvc3
    [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.863 sec
    [junit] 
    [junit] Testsuite: edu.udel.cis.vsl.civl.transform.MPICollectivePart1Test
    [junit] Tests run: 20, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 38.745 sec
    [junit] 
    [junit] Testsuite: edu.udel.cis.vsl.civl.transform.MPICollectivePart2Test
    [junit] Tests run: 25, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 54.157 sec
    [junit] 
    [junit] Testsuite: edu.udel.cis.vsl.civl.transform.MPITranslationTest
    [junit] Tests run: 23, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 57.687 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.711 sec
    [junit] 
    [junit] Testsuite: edu.udel.cis.vsl.civl.transform.OmpHelpersTest
    [junit] Tests run: 9, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 3.057 sec
    [junit] 
    [junit] Testsuite: edu.udel.cis.vsl.civl.transform.OpenMP2CIVLTransformerTest
    [junit] Tests run: 8, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 17.958 sec
    [junit] 
    [junit] Testsuite: edu.udel.cis.vsl.civl.transform.PthreadTest
    [junit] Tests run: 16, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 13.765 sec
    [junit] 
    [junit] Testsuite: edu.udel.cis.vsl.civl.transform.PthreadThreaderTest
    [junit] Tests run: 8, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 2.285 sec
    [junit] 
    [junit] Testsuite: edu.udel.cis.vsl.civl.transform.SideEffectsTest
    [junit] Tests run: 10, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.467 sec
    [junit] 
[junitreport] Processing /usa/svn/work/civl/1.16/r4871/junit/data/TESTS-TestSuites.xml to /tmp/null1366953686
[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: 529ms
[junitreport] Deleting: /tmp/null1366953686

test:
[jacoco:report] Loading execution data file /usa/svn/work/civl/1.16/r4871/jacoco.exec
[jacoco:report] Writing bundle 'Test Coverage Report for CIVL 1.16 r4871 Regression Suite' with 537 classes

javadoc:
    [mkdir] Created dir: /usa/svn/work/civl/1.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/src/edu/udel/cis/vsl/civl/config/IF/CIVLConfiguration.java:764: warning: no @return
  [javadoc] 	public int getProcBound() {
  [javadoc] 	           ^
  [javadoc] /usa/svn/work/civl/1.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:338: error: reference not found
  [javadoc] 	 *            {@link #isPointerToHeap(heapPointer)} must returns true.
  [javadoc] 	                     ^
  [javadoc] /usa/svn/work/civl/1.16/r4871/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:391: error: semicolon missing
  [javadoc] 	 * pointer. For example, given a pointer &a[5] and a reference [0], the
  [javadoc] 	                                         ^
  [javadoc] /usa/svn/work/civl/1.16/r4871/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:392: 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.16/r4871/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:661: error: tag not allowed here: <li>
  [javadoc] 	 * <li>length(array_extents) > 0</li>
  [javadoc] 	   ^
  [javadoc] /usa/svn/work/civl/1.16/r4871/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:661: error: bad use of '>'
  [javadoc] 	 * <li>length(array_extents) > 0</li>
  [javadoc] 	                             ^
  [javadoc] /usa/svn/work/civl/1.16/r4871/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:662: error: unexpected end tag: </p>
  [javadoc] 	 * </p>
  [javadoc] 	   ^
  [javadoc] /usa/svn/work/civl/1.16/r4871/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:671: 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.16/r4871/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:673: error: exception not thrown: edu.udel.cis.vsl.civl.state.IF.UnsatisfiablePathConditionException
  [javadoc] 	 * @throws UnsatisfiablePathConditionException
  [javadoc] 	           ^
  [javadoc] /usa/svn/work/civl/1.16/r4871/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:673: warning: no description for @throws
  [javadoc] 	 * @throws UnsatisfiablePathConditionException
  [javadoc] 	   ^
  [javadoc] /usa/svn/work/civl/1.16/r4871/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:761: warning: no description for @param
  [javadoc] 	 * @param domain
  [javadoc] 	   ^
  [javadoc] /usa/svn/work/civl/1.16/r4871/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:769: warning: no description for @param
  [javadoc] 	 * @param range
  [javadoc] 	   ^
  [javadoc] /usa/svn/work/civl/1.16/r4871/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:779: warning: no description for @param
  [javadoc] 	 * @param domain
  [javadoc] 	   ^
  [javadoc] /usa/svn/work/civl/1.16/r4871/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:780: warning: no description for @param
  [javadoc] 	 * @param index
  [javadoc] 	   ^
  [javadoc] /usa/svn/work/civl/1.16/r4871/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:791: warning: no description for @param
  [javadoc] 	 * @param range
  [javadoc] 	   ^
  [javadoc] /usa/svn/work/civl/1.16/r4871/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:801: warning: no description for @param
  [javadoc] 	 * @param range
  [javadoc] 	   ^
  [javadoc] /usa/svn/work/civl/1.16/r4871/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:812: warning: no description for @param
  [javadoc] 	 * @param range
  [javadoc] 	   ^
  [javadoc] /usa/svn/work/civl/1.16/r4871/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:820: warning: no description for @param
  [javadoc] 	 * @param domain
  [javadoc] 	   ^
  [javadoc] /usa/svn/work/civl/1.16/r4871/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:827: 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.16/r4871/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:827: 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.16/r4871/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:827: 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.16/r4871/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:827: 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.16/r4871/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:827: 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.16/r4871/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:827: 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.16/r4871/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:827: 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.16/r4871/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:828: 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.16/r4871/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:828: 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.16/r4871/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:828: 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.16/r4871/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:830: warning: no description for @param
  [javadoc] 	 * @param cnfClause
  [javadoc] 	   ^
  [javadoc] /usa/svn/work/civl/1.16/r4871/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:838: warning: no description for @param
  [javadoc] 	 * @param function
  [javadoc] 	   ^
  [javadoc] /usa/svn/work/civl/1.16/r4871/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:839: error: @param name not found
  [javadoc] 	 * @param arguments
  [javadoc] 	          ^
  [javadoc] /usa/svn/work/civl/1.16/r4871/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:839: warning: no description for @param
  [javadoc] 	 * @param arguments
  [javadoc] 	   ^
  [javadoc] /usa/svn/work/civl/1.16/r4871/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:840: warning: no description for @return
  [javadoc] 	 * @return
  [javadoc] 	   ^
  [javadoc] /usa/svn/work/civl/1.16/r4871/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:842: warning: no @param for library
  [javadoc] 	SymbolicExpression getAbstractGuardOfFunctionCall(String library,
  [javadoc] 	                   ^
  [javadoc] /usa/svn/work/civl/1.16/r4871/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:842: warning: no @param for argumentValues
  [javadoc] 	SymbolicExpression getAbstractGuardOfFunctionCall(String library,
  [javadoc] 	                   ^
  [javadoc] /usa/svn/work/civl/1.16/r4871/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:852: warning: no description for @param
  [javadoc] 	 * @param originalFunction
  [javadoc] 	   ^
  [javadoc] /usa/svn/work/civl/1.16/r4871/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:853: warning: no description for @param
  [javadoc] 	 * @param argument
  [javadoc] 	   ^
  [javadoc] /usa/svn/work/civl/1.16/r4871/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:854: warning: no description for @return
  [javadoc] 	 * @return
  [javadoc] 	   ^
  [javadoc] /usa/svn/work/civl/1.16/r4871/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:866: warning: no description for @param
  [javadoc] 	 * @param range
  [javadoc] 	   ^
  [javadoc] /usa/svn/work/civl/1.16/r4871/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:867: warning: no description for @return
  [javadoc] 	 * @return
  [javadoc] 	   ^
  [javadoc] /usa/svn/work/civl/1.16/r4871/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:869: warning: no @param for reasoner
  [javadoc] 	BitSet range2BitSet(SymbolicExpression range, Reasoner reasoner);
  [javadoc] 	       ^
  [javadoc] /usa/svn/work/civl/1.16/r4871/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:881: warning: no description for @param
  [javadoc] 	 * @param pointer
  [javadoc] 	   ^
  [javadoc] /usa/svn/work/civl/1.16/r4871/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:882: warning: no description for @return
  [javadoc] 	 * @return
  [javadoc] 	   ^
  [javadoc] /usa/svn/work/civl/1.16/r4871/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:341: warning - Tag @link: can't find isPointerToHeap(heapPointer) in edu.udel.cis.vsl.civl.dynamic.IF.SymbolicUtility
  [javadoc] /usa/svn/work/civl/1.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/src/edu/udel/cis/vsl/civl/model/IF/CIVLSource.java:34: warning: no @return
  [javadoc] 	String getLocation();
  [javadoc] 	       ^
  [javadoc] /usa/svn/work/civl/1.16/r4871/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.16/r4871/src/edu/udel/cis/vsl/civl/model/IF/CIVLTypeFactory.java:106: warning: no description for @param
  [javadoc] 	 * @param rangeType
  [javadoc] 	   ^
  [javadoc] /usa/svn/work/civl/1.16/r4871/src/edu/udel/cis/vsl/civl/model/IF/CIVLTypeFactory.java:164: error: bad use of '>'
  [javadoc] 	 * Create a new location. ======= Get the integer primitive type. >>>>>>>
  [javadoc] 	                                                                  ^
  [javadoc] /usa/svn/work/civl/1.16/r4871/src/edu/udel/cis/vsl/civl/model/IF/CIVLTypeFactory.java:164: error: bad use of '>'
  [javadoc] 	 * Create a new location. ======= Get the integer primitive type. >>>>>>>
  [javadoc] 	                                                                   ^
  [javadoc] /usa/svn/work/civl/1.16/r4871/src/edu/udel/cis/vsl/civl/model/IF/CIVLTypeFactory.java:164: error: bad use of '>'
  [javadoc] 	 * Create a new location. ======= Get the integer primitive type. >>>>>>>
  [javadoc] 	                                                                    ^
  [javadoc] /usa/svn/work/civl/1.16/r4871/src/edu/udel/cis/vsl/civl/model/IF/CIVLTypeFactory.java:164: error: bad use of '>'
  [javadoc] 	 * Create a new location. ======= Get the integer primitive type. >>>>>>>
  [javadoc] 	                                                                     ^
  [javadoc] /usa/svn/work/civl/1.16/r4871/src/edu/udel/cis/vsl/civl/model/IF/CIVLTypeFactory.java:164: error: bad use of '>'
  [javadoc] 	 * Create a new location. ======= Get the integer primitive type. >>>>>>>
  [javadoc] 	                                                                      ^
  [javadoc] /usa/svn/work/civl/1.16/r4871/src/edu/udel/cis/vsl/civl/model/IF/CIVLTypeFactory.java:164: error: bad use of '>'
  [javadoc] 	 * Create a new location. ======= Get the integer primitive type. >>>>>>>
  [javadoc] 	                                                                       ^
  [javadoc] /usa/svn/work/civl/1.16/r4871/src/edu/udel/cis/vsl/civl/model/IF/CIVLTypeFactory.java:164: error: bad use of '>'
  [javadoc] 	 * Create a new location. ======= Get the integer primitive type. >>>>>>>
  [javadoc] 	                                                                        ^
  [javadoc] /usa/svn/work/civl/1.16/r4871/src/edu/udel/cis/vsl/civl/model/IF/CIVLTypeFactory.java:339: warning: no description for @param
  [javadoc] 	 * @param type
  [javadoc] 	   ^
  [javadoc] /usa/svn/work/civl/1.16/r4871/src/edu/udel/cis/vsl/civl/model/IF/CIVLTypeFactory.java:340: warning: no description for @param
  [javadoc] 	 * @param id
  [javadoc] 	   ^
  [javadoc] /usa/svn/work/civl/1.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:871: warning: no description for @param
  [javadoc] 	 * @param domSize
  [javadoc] 	   ^
  [javadoc] /usa/svn/work/civl/1.16/r4871/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:918: warning: no description for @return
  [javadoc] 	 * @return
  [javadoc] 	   ^
  [javadoc] /usa/svn/work/civl/1.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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.16/r4871/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] /usa/svn/work/civl/1.16/r4871/src/edu/udel/cis/vsl/civl/model/IF/expression/BinaryExpression.java:20: error: bad use of '>'
  [javadoc] 	 * <li>RIGHT_SHIFT: <code>>></code> (bitwise right shift);</li>
  [javadoc] 	                          ^
  [javadoc] /usa/svn/work/civl/1.16/r4871/src/edu/udel/cis/vsl/civl/model/IF/expression/BinaryExpression.java:20: error: bad use of '>'
  [javadoc] 	 * <li>RIGHT_SHIFT: <code>>></code> (bitwise right shift);</li>
  [javadoc] 	                           ^
  [javadoc] /usa/svn/work/civl/1.16/r4871/src/edu/udel/cis/vsl/civl/model/IF/expression/BinaryExpression.java:21: error: tag not allowed here: <li>
  [javadoc] 	 * <li>BITAND: <code>&</code> (bitwise and);</li>
  [javadoc] 	   ^
  [javadoc] Building index for all the packages and classes...
  [javadoc] Building index for all classes...
  [javadoc] Generating /usa/svn/work/civl/1.16/r4871/doc/javadoc/help-doc.html...
  [javadoc] 100 errors
  [javadoc] 100 warnings

bench-compile:
    [javac] Compiling 6 source files to /usa/svn/work/civl/1.16/r4871/bin

bench-scale-compile:
    [javac] Compiling 5 source files to /usa/svn/work/civl/1.16/r4871/bin

all:

BUILD SUCCESSFUL
Total time: 7 minutes 39 seconds

Stderr: