CIVL 1.7.4 Revision 4061

Downloads, Test and Coverage Reports, and Javadocs

Revision Information

Path: .
Working Copy Root Path: /usa/svn/work/civl/1.7.4/r4061
URL: svn://vsl.cis.udel.edu/civl/tags/1.7.4
Relative URL: ^/tags/1.7.4
Repository Root: svn://vsl.cis.udel.edu/civl
Repository UUID: fb995dde-84ed-4084-dfe6-e5aef3e2452c
Revision: 4061
Node Kind: directory
Schedule: normal
Last Changed Author: ziqing
Last Changed Rev: 4061
Last Changed Date: 2017-03-10 13:27:59 -0500 (Fri, 10 Mar 2017)

Build output

Stdout:

Buildfile: /usa/svn/work/civl/1.7.4/r4061/build.xml

checkCommandParserChanges:

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

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

jar:
      [jar] Building jar: /usa/svn/work/civl/1.7.4/r4061/civl.jar

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

test-compile:
    [javac] Compiling 30 source files to /usa/svn/work/civl/1.7.4/r4061/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: 3.009 sec
    [junit] 
    [junit] Testsuite: edu.udel.cis.vsl.civl.ArithmeticTest
    [junit] Tests run: 23, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 9.75 sec
    [junit] 
    [junit] ------------- Standard Error -----------------
    [junit] Syntax error: denominator can not be zero.
    [junit] ------------- ---------------- ---------------
    [junit] Testsuite: edu.udel.cis.vsl.civl.BackendTest
    [junit] Tests run: 16, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 2.104 sec
    [junit] 
    [junit] ------------- Standard Output ---------------
    [junit] CIVL v1.7.4 of 2017-03-10 -- http://vsl.cis.udel.edu/civl
    [junit] input variables:
    [junit] $input int _civl_argc
    [junit] $input char  _civl_argv[_civl_argc][]
    [junit] $input long NB = 20
    [junit] $input long N
    [junit] $input int _mpi_nprocs
    [junit] $input int _mpi_nprocs_lo = 1
    [junit] $input int _mpi_nprocs_hi = 8
    [junit] ------------- ---------------- ---------------
    [junit] ------------- Standard Error -----------------
    [junit] Error: Unknown expression kind
    [junit] at original.cvl:7.29-40 "$original(i)"
    [junit] ------------- ---------------- ---------------
    [junit] Testsuite: edu.udel.cis.vsl.civl.CompareTest
    [junit] Tests run: 1, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 6.022 sec
    [junit] 
    [junit] ------------- Standard Output ---------------
    [junit] CIVL v1.7.4 of 2017-03-10 -- http://vsl.cis.udel.edu/civl
    [junit] 
    [junit] Error: This feature is not yet implemented: 
    [junit] Ability to deterine whether a non-concrete pointer is defined.
    [junit] pointer value: [<<0>,0,ArrayElementRef(ArrayElementRef(TupleComponentRef(<1>,1),0),0)>,<<0>,0,ArrayElementRef(ArrayElementRef(TupleComponentRef(<1>,1),1),0)>,<<0>,0,ArrayElementRef(ArrayElementRef(TupleComponentRef(<1>,1),2),0)>][X_ys]
    [junit] at ex2a.c:62.36-42 "x[j][i]".
    [junit] ------------- ---------------- ---------------
    [junit] Testsuite: edu.udel.cis.vsl.civl.ConcurrencyTest
    [junit] Tests run: 32, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 11.792 sec
    [junit] 
    [junit] ------------- Standard Output ---------------
    [junit] CIVL v1.7.4 of 2017-03-10 -- http://vsl.cis.udel.edu/civl
    [junit] 
    [junit] === Command ===
    [junit] civl verify -inputB=4 examples/concurrency/barrier2.cvl 
    [junit] 
    [junit] === Stats ===
    [junit]    time (s)            : 1.17
    [junit]    memory (bytes)      : 738721792
    [junit]    max process count   : 5
    [junit]    states              : 20702
    [junit]    states saved        : 3741
    [junit]    state matches       : 6340
    [junit]    transitions         : 27033
    [junit]    trace steps         : 10080
    [junit]    valid calls         : 139481
    [junit]    provers             : cvc4, z3, cvc3
    [junit]    prover calls        : 6
    [junit] 
    [junit] === Result ===
    [junit] The standard properties hold for all executions.
    [junit] ------------- ---------------- ---------------
    [junit] Testsuite: edu.udel.cis.vsl.civl.LanguageFeaturesTest
    [junit] Tests run: 127, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 10.316 sec
    [junit] 
    [junit] ------------- Standard Output ---------------
    [junit] 
    [junit] Error: This feature is not yet implemented: Pointer addition for anything other than array elements or variables
    [junit] at pointerAddBad5.c:6.15-26 "&point.x + 1".
    [junit] 
    [junit] Error: This feature is not yet implemented: Converting integer whose value is larger than UCHAR_MAX or is less than UCHAR_MIN to char type
    [junit] 
    [junit] 
    [junit] Error: This feature is not yet implemented: sub-references of union type
    [junit] at pointersBad.cvl:42.31-38 "&number0".
    [junit] ------------- ---------------- ---------------
    [junit] ------------- Standard Error -----------------
    [junit] Syntax error: Function dummy doesn't have a definition.
    [junit] at civlValueUndefined.cvl:9.4-8 "dummy".
    [junit] Syntax error: Invalid precision for the format "%c"...
    [junit] at splitFormatBad.cvl:9.9-32 ""The value of c is %.2c"".
    [junit] Syntax error: The format %%q is not allowed in fprintf
    [junit] at splitFormatBad2.cvl:8.9-30 ""The value of c is %q"".
    [junit] Syntax error: The format %%l is not allowed in fprintf
    [junit] at splitFormatBad3.cvl:8.9-30 ""The value of a is %l"".
    [junit] Syntax error: $abstract functions must have at least one input.
    [junit] An abstract function with 0 inputs is a constant.
    [junit] It can be declared as an unconstrained input variable instead, e.g.
    [junit] $input int N;
    [junit] at abstractFunNoArg.cvl:4.0-25 "$abstract int random(void)".
    [junit] Error: Type of the left argument of assignment has input-qualifier
    [junit] at assignInput.cvl:9.2 "N"
    [junit] Error: the guard of a $when statement is not allowed to have side effects.
    [junit] at badGuard.cvl:14.10-17 "x/y > 10"
    [junit] ------------- ---------------- ---------------
    [junit] Testsuite: edu.udel.cis.vsl.civl.LibraryTest
    [junit] Tests run: 56, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 4.929 sec
    [junit] 
    [junit] ------------- Standard Output ---------------
    [junit] CIVL v1.7.4 of 2017-03-10 -- http://vsl.cis.udel.edu/civl
    [junit] 
    [junit] Violation 0 encountered at depth 2:
    [junit] CIVL execution violation in p0 (kind: UNDEFINED_VALUE, certainty: PROVEABLE)
    [junit] at undefinedVar.cvl:5.17-20 "temp":
    [junit] Attempt to dereference a pointer that refers to an object with undefined value
    [junit] 
    [junit] Context:
    [junit]   true
    [junit] Call stacks:
    [junit] process 0:
    [junit]   main at undefinedVar.cvl:5.1-24 "double temp2 = *temp  ... 1"
    [junit] 
    [junit] Logging new entry 0, writing trace to CIVLREP/undefinedVar_0.trace
    [junit] Terminating search after finding 1 violation.
    [junit] 
    [junit] === Command ===
    [junit] civl verify examples/library/pointer/undefinedVar.cvl 
    [junit] 
    [junit] === Stats ===
    [junit]    time (s)            : 0.03
    [junit]    memory (bytes)      : 778567680
    [junit]    max process count   : 1
    [junit]    states              : 2
    [junit]    states saved        : 2
    [junit]    state matches       : 0
    [junit]    transitions         : 2
    [junit]    trace steps         : 1
    [junit]    valid calls         : 1
    [junit]    provers             : cvc4, z3, cvc3
    [junit]    prover calls        : 0
    [junit] 
    [junit] === Result ===
    [junit] The program MAY NOT be correct.  See CIVLREP/undefinedVar_log.txt
    [junit] CIVL v1.7.4 of 2017-03-10 -- http://vsl.cis.udel.edu/civl
    [junit] 
    [junit] === Command ===
    [junit] civl verify examples/library/pointer/simpleCopyTest.cvl 
    [junit] 
    [junit] === Stats ===
    [junit]    time (s)            : 0.03
    [junit]    memory (bytes)      : 781189120
    [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         : 0
    [junit]    provers             : cvc4, z3, cvc3
    [junit]    prover calls        : 0
    [junit] 
    [junit] === Result ===
    [junit] The standard properties hold for all executions.
    [junit] ------------- ---------------- ---------------
    [junit] ------------- Standard Error -----------------
    [junit] Syntax error: The format %%l is not allowed in fprintf
    [junit] at printfBad.cvl:7.9-14 ""x=%l"".
    [junit] ------------- ---------------- ---------------
    [junit] Testsuite: edu.udel.cis.vsl.civl.ModelBuilderTest
    [junit] Tests run: 6, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.247 sec
    [junit] 
    [junit] Testsuite: edu.udel.cis.vsl.civl.PORTest
    [junit] Tests run: 14, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.485 sec
    [junit] 
    [junit] Testsuite: edu.udel.cis.vsl.civl.QuietOptionTest
    [junit] Tests run: 5, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 2.315 sec
    [junit] 
    [junit] Testsuite: edu.udel.cis.vsl.civl.ReasoningTest
    [junit] Tests run: 5, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 1.253 sec
    [junit] 
    [junit] Testsuite: edu.udel.cis.vsl.civl.ShowStatesTest
    [junit] Tests run: 2, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.059 sec
    [junit] 
    [junit] Testsuite: edu.udel.cis.vsl.civl.SimpleMPITest
    [junit] Tests run: 23, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 40.579 sec
    [junit] 
    [junit] Testsuite: edu.udel.cis.vsl.civl.SpecialStatementsTest
    [junit] Tests run: 7, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.145 sec
    [junit] 
    [junit] ------------- Standard Error -----------------
    [junit] Syntax error: the first (recursively) primitive statement of a clause of $choose should not use $here
    [junit] at choose_bad1.cvl:7.4-6 "ptr".
    [junit] Syntax error: the first (recursively) primitive statement of a clause of $choose should not use $here
    [junit] at choose_bad2.cvl:8.4-8 "$when".
    [junit] Syntax error: the first (recursively) primitive statement of a clause of $choose should not use $here
    [junit] at choose_bad3.cvl:8.4-8 "$when".
    [junit] ------------- ---------------- ---------------
    [junit] Testsuite: edu.udel.cis.vsl.civl.SvcompTest
    [junit] Tests run: 10, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 7.955 sec
    [junit] 
    [junit] ------------- Standard Output ---------------
    [junit] CIVL v1.7.4 of 2017-03-10 -- http://vsl.cis.udel.edu/civl
    [junit] ------------- ---------------- ---------------
    [junit] ------------- Standard Error -----------------
    [junit] Preprocessor error: Could not find file examples/pthread/svcomp/pthread-numerical-integration_true-unreach-call.i
    [junit] ------------- ---------------- ---------------
    [junit] Testsuite: edu.udel.cis.vsl.civl.VerifyThisTest
    [junit] Tests run: 10, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 59.855 sec
    [junit] 
    [junit] Testsuite: edu.udel.cis.vsl.civl.transform.CompareTest
    [junit] Tests run: 10, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 52.363 sec
    [junit] 
    [junit] ------------- Standard Output ---------------
    [junit] CIVL v1.7.4 of 2017-03-10 -- http://vsl.cis.udel.edu/civl
    [junit] 
    [junit] === Command ===
    [junit] civl compare -enablePrintf=false -showProgram=false -input_mpi_nprocs_hi=2 -inputNB=4 -impl examples/compare/adder/adder_par.c -spec examples/compare/adder/adder_spec.c 
    [junit] 
    [junit] === Stats ===
    [junit]    time (s)            : 1.97
    [junit]    memory (bytes)      : 795869184
    [junit]    max process count   : 3
    [junit]    states              : 2728
    [junit]    states saved        : 1033
    [junit]    state matches       : 0
    [junit]    transitions         : 2711
    [junit]    trace steps         : 1032
    [junit]    valid calls         : 7800
    [junit]    provers             : cvc4, z3, cvc3
    [junit]    prover calls        : 50
    [junit] 
    [junit] === Result ===
    [junit] The standard properties hold for all executions.
    [junit] ------------- ---------------- ---------------
    [junit] ------------- Standard Error -----------------
    [junit] This feature is not yet implemented: compatible structure or union conversion
    [junit] at comm.cvl:56.4-41 "result.data = $bundle_pack(data ... )".
    [junit] ------------- ---------------- ---------------
    [junit] Testsuite: edu.udel.cis.vsl.civl.transform.CudaTest
    [junit] Tests run: 2, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 10.616 sec
    [junit] 
    [junit] Testsuite: edu.udel.cis.vsl.civl.transform.GenTransformerTest
    [junit] Tests run: 3, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 2.243 sec
    [junit] 
    [junit] Testsuite: edu.udel.cis.vsl.civl.transform.IOTransformerTest
    [junit] Tests run: 3, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.676 sec
    [junit] 
    [junit] ------------- Standard Output ---------------
    [junit] 
    [junit] Error: This feature is not yet implemented: pointer into string of unknown length
    [junit] at fileOpen.cvl:33.22-36 "&icaFilename[2]".
    [junit] 
    [junit] Error: This feature is not yet implemented: pointer to char is not into an array of char
    [junit] at fileOpen.cvl:31.22-23 "&c".
    [junit] ------------- ---------------- ---------------
    [junit] Testsuite: edu.udel.cis.vsl.civl.transform.MPICollectivePart1Test
    [junit] Tests run: 20, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 34.492 sec
    [junit] 
    [junit] Testsuite: edu.udel.cis.vsl.civl.transform.MPICollectivePart2Test
    [junit] Tests run: 20, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 41.672 sec
    [junit] 
    [junit] Testsuite: edu.udel.cis.vsl.civl.transform.MPITranslationTest
    [junit] Tests run: 19, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 46.231 sec
    [junit] 
    [junit] ------------- Standard Output ---------------
    [junit] CIVL v1.7.4 of 2017-03-10 -- http://vsl.cis.udel.edu/civl
    [junit] 
    [junit] === Command ===
    [junit] civl verify -input_mpi_nprocs=2 examples/mpi/ring1.c 
    [junit] 
    [junit] === Stats ===
    [junit]    time (s)            : 0.92
    [junit]    memory (bytes)      : 901775360
    [junit]    max process count   : 3
    [junit]    states              : 423
    [junit]    states saved        : 115
    [junit]    state matches       : 0
    [junit]    transitions         : 417
    [junit]    trace steps         : 114
    [junit]    valid calls         : 908
    [junit]    provers             : cvc4, z3, cvc3
    [junit]    prover calls        : 1
    [junit] 
    [junit] === Result ===
    [junit] The standard properties hold for all executions.
    [junit] ------------- ---------------- ---------------
    [junit] Testsuite: edu.udel.cis.vsl.civl.transform.MPI_OpenMPTest
    [junit] Tests run: 3, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 6.719 sec
    [junit] 
    [junit] Testsuite: edu.udel.cis.vsl.civl.transform.OmpHelpersTest
    [junit] Tests run: 9, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 3.297 sec
    [junit] 
    [junit] Testsuite: edu.udel.cis.vsl.civl.transform.OpenMP2CIVLTransformerTest
    [junit] Tests run: 7, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 14.956 sec
    [junit] 
    [junit] ------------- Standard Output ---------------
    [junit] CIVL v1.7.4 of 2017-03-10 -- http://vsl.cis.udel.edu/civl
    [junit] 
    [junit] === Command ===
    [junit] civl verify -enablePrintf=false -input_omp_thread_max=2 examples/omp/parallelfor.c 
    [junit] 
    [junit] === Stats ===
    [junit]    time (s)            : 0.73
    [junit]    memory (bytes)      : 925368320
    [junit]    max process count   : 3
    [junit]    states              : 5107
    [junit]    states saved        : 1376
    [junit]    state matches       : 23
    [junit]    transitions         : 5126
    [junit]    trace steps         : 1398
    [junit]    valid calls         : 9876
    [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.transform.PthreadTest
    [junit] Tests run: 16, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 11.108 sec
    [junit] 
    [junit] Testsuite: edu.udel.cis.vsl.civl.transform.PthreadThreaderTest
    [junit] Tests run: 8, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 1.714 sec
    [junit] 
    [junit] Testsuite: edu.udel.cis.vsl.civl.transform.SideEffectsTest
    [junit] Tests run: 5, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.107 sec
    [junit] 
    [junit] ------------- Standard Output ---------------
    [junit] CIVL v1.7.4 of 2017-03-10 -- http://vsl.cis.udel.edu/civl
    [junit] 
    [junit] === Command ===
    [junit] civl verify examples/sideEffects/structWithDiv.cvl 
    [junit] 
    [junit] === Stats ===
    [junit]    time (s)            : 0.02
    [junit]    memory (bytes)      : 942145536
    [junit]    max process count   : 1
    [junit]    states              : 13
    [junit]    states saved        : 6
    [junit]    state matches       : 0
    [junit]    transitions         : 12
    [junit]    trace steps         : 5
    [junit]    valid calls         : 6
    [junit]    provers             : cvc4, z3, cvc3
    [junit]    prover calls        : 0
    [junit] 
    [junit] === Result ===
    [junit] The standard properties hold for all executions.
    [junit] ------------- ---------------- ---------------
[junitreport] Processing /usa/svn/work/civl/1.7.4/r4061/junit/data/TESTS-TestSuites.xml to /tmp/null2133933163
[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: 472ms
[junitreport] Deleting: /tmp/null2133933163

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

javadoc:
    [mkdir] Created dir: /usa/svn/work/civl/1.7.4/r4061/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_66
  [javadoc] Building tree for all the packages and classes...
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/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.7.4/r4061/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.7.4/r4061/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.7.4/r4061/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.7.4/r4061/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.7.4/r4061/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.7.4/r4061/src/edu/udel/cis/vsl/civl/config/IF/CIVLConfiguration.java:734: warning: no @return
  [javadoc] 	public int getProcBound() {
  [javadoc] 	           ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:341: error: semicolon missing
  [javadoc] 	 * pointer. For example, given a pointer &a[5] and a reference [0], the
  [javadoc] 	                                         ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:342: 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.7.4/r4061/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:614: error: tag not allowed here: <li>
  [javadoc] 	 * <li>length(array_extents) > 0</li>
  [javadoc] 	   ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:614: error: bad use of '>'
  [javadoc] 	 * <li>length(array_extents) > 0</li>
  [javadoc] 	                             ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:615: error: unexpected end tag: </p>
  [javadoc] 	 * </p>
  [javadoc] 	   ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:622: 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.7.4/r4061/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:624: error: exception not thrown: edu.udel.cis.vsl.civl.state.IF.UnsatisfiablePathConditionException
  [javadoc] 	 * @throws UnsatisfiablePathConditionException
  [javadoc] 	           ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:624: warning: no description for @throws
  [javadoc] 	 * @throws UnsatisfiablePathConditionException
  [javadoc] 	   ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:713: warning: no description for @param
  [javadoc] 	 * @param domain
  [javadoc] 	   ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:721: warning: no description for @param
  [javadoc] 	 * @param range
  [javadoc] 	   ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:731: warning: no description for @param
  [javadoc] 	 * @param domain
  [javadoc] 	   ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:732: warning: no description for @param
  [javadoc] 	 * @param index
  [javadoc] 	   ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:743: warning: no description for @param
  [javadoc] 	 * @param range
  [javadoc] 	   ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:753: warning: no description for @param
  [javadoc] 	 * @param range
  [javadoc] 	   ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:764: warning: no description for @param
  [javadoc] 	 * @param range
  [javadoc] 	   ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:772: warning: no description for @param
  [javadoc] 	 * @param domain
  [javadoc] 	   ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:779: 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.7.4/r4061/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:779: 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.7.4/r4061/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:779: 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.7.4/r4061/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:779: 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.7.4/r4061/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:779: 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.7.4/r4061/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:779: 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.7.4/r4061/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:779: 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.7.4/r4061/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:780: 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.7.4/r4061/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:780: 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.7.4/r4061/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:780: 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.7.4/r4061/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:782: warning: no description for @param
  [javadoc] 	 * @param cnfClause
  [javadoc] 	   ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:790: warning: no description for @param
  [javadoc] 	 * @param function
  [javadoc] 	   ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:791: error: @param name not found
  [javadoc] 	 * @param arguments
  [javadoc] 	          ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:791: warning: no description for @param
  [javadoc] 	 * @param arguments
  [javadoc] 	   ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:792: warning: no description for @return
  [javadoc] 	 * @return
  [javadoc] 	   ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:794: warning: no @param for library
  [javadoc] 	SymbolicExpression getAbstractGuardOfFunctionCall(String library,
  [javadoc] 	                   ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:794: warning: no @param for argumentValues
  [javadoc] 	SymbolicExpression getAbstractGuardOfFunctionCall(String library,
  [javadoc] 	                   ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:804: warning: no description for @param
  [javadoc] 	 * @param originalFunction
  [javadoc] 	   ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:805: warning: no description for @param
  [javadoc] 	 * @param argument
  [javadoc] 	   ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:806: warning: no description for @return
  [javadoc] 	 * @return
  [javadoc] 	   ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:818: warning: no description for @param
  [javadoc] 	 * @param range
  [javadoc] 	   ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/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.7.4/r4061/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:821: warning: no @param for reasoner
  [javadoc] 	BitSet range2BitSet(SymbolicExpression range, Reasoner reasoner);
  [javadoc] 	       ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:833: warning: no description for @param
  [javadoc] 	 * @param pointer
  [javadoc] 	   ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:834: warning: no description for @return
  [javadoc] 	 * @return
  [javadoc] 	   ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/gui/IF/CIVL_GUI.java:100: error: @param name not found
  [javadoc] 	 * @param transitions
  [javadoc] 	          ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/gui/IF/CIVL_GUI.java:103: warning: no @param for trace
  [javadoc] 	public CIVL_GUI(Trace<Transition, State> trace,
  [javadoc] 	       ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/gui/IF/CIVL_GUI.java:103: warning: no @param for symbolicAnalyzer
  [javadoc] 	public CIVL_GUI(Trace<Transition, State> trace,
  [javadoc] 	       ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/kripke/IF/Kripkes.java:42: warning: no @param for executor
  [javadoc] 	public static Enabler newEnabler(StateFactory stateFactory,
  [javadoc] 	                      ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/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.7.4/r4061/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.7.4/r4061/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.7.4/r4061/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.7.4/r4061/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.7.4/r4061/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.7.4/r4061/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.7.4/r4061/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.7.4/r4061/src/edu/udel/cis/vsl/civl/log/IF/CIVLErrorLogger.java:96: error: bad HTML entity
  [javadoc] 	 * <li>pcsat=YES && condsat=NO : certainty=PROVEABLE</li>
  [javadoc] 	                 ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/log/IF/CIVLErrorLogger.java:96: error: bad HTML entity
  [javadoc] 	 * <li>pcsat=YES && condsat=NO : certainty=PROVEABLE</li>
  [javadoc] 	                  ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/log/IF/CIVLErrorLogger.java:97: error: bad HTML entity
  [javadoc] 	 * <li>pcsat=YES && condsat=MAYBE : certainty=MAYBE</li>
  [javadoc] 	                 ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/log/IF/CIVLErrorLogger.java:97: error: bad HTML entity
  [javadoc] 	 * <li>pcsat=YES && condsat=MAYBE : certainty=MAYBE</li>
  [javadoc] 	                  ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/log/IF/CIVLErrorLogger.java:98: error: bad HTML entity
  [javadoc] 	 * <li>pcsat=MAYBE && condsat=NO : certainty=MAYBE</li>
  [javadoc] 	                   ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/log/IF/CIVLErrorLogger.java:98: error: bad HTML entity
  [javadoc] 	 * <li>pcsat=MAYBE && condsat=NO : certainty=MAYBE</li>
  [javadoc] 	                    ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/log/IF/CIVLErrorLogger.java:99: error: bad HTML entity
  [javadoc] 	 * <li>pcsat=MAYBE && condsat=MAYBE : certainty=MAYBE</li>
  [javadoc] 	                   ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/log/IF/CIVLErrorLogger.java:99: error: bad HTML entity
  [javadoc] 	 * <li>pcsat=MAYBE && condsat=MAYBE : certainty=MAYBE</li>
  [javadoc] 	                    ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/log/IF/CIVLErrorLogger.java:102: error: unexpected end tag: </p>
  [javadoc] 	 * </p>
  [javadoc] 	   ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/log/IF/CIVLErrorLogger.java:58: warning: no description for @param
  [javadoc] 	 * @param directory
  [javadoc] 	   ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/log/IF/CIVLErrorLogger.java:59: warning: no description for @param
  [javadoc] 	 * @param sessionName
  [javadoc] 	   ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/log/IF/CIVLErrorLogger.java:60: warning: no description for @param
  [javadoc] 	 * @param out
  [javadoc] 	   ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/log/IF/CIVLErrorLogger.java:61: error: @param name not found
  [javadoc] 	 * @param config
  [javadoc] 	          ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/log/IF/CIVLErrorLogger.java:61: warning: no description for @param
  [javadoc] 	 * @param config
  [javadoc] 	   ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/log/IF/CIVLErrorLogger.java:62: warning: no description for @param
  [javadoc] 	 * @param universe
  [javadoc] 	   ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/log/IF/CIVLErrorLogger.java:63: warning: no description for @param
  [javadoc] 	 * @param solve
  [javadoc] 	   ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/log/IF/CIVLErrorLogger.java:65: warning: no @param for civlConfig
  [javadoc] 	public CIVLErrorLogger(File directory, String sessionName, PrintStream out,
  [javadoc] 	       ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/log/IF/CIVLErrorLogger.java:65: warning: no @param for gmcConfig
  [javadoc] 	public CIVLErrorLogger(File directory, String sessionName, PrintStream out,
  [javadoc] 	       ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/log/IF/CIVLExecutionException.java:42: error: @param name not found
  [javadoc] 	 * @param stateString
  [javadoc] 	          ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/log/IF/CIVLExecutionException.java:48: warning: no @param for state
  [javadoc] 	public CIVLExecutionException(ErrorKind kind, Certainty certainty,
  [javadoc] 	       ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/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.7.4/r4061/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.7.4/r4061/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.7.4/r4061/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.7.4/r4061/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.7.4/r4061/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.7.4/r4061/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.7.4/r4061/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.7.4/r4061/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.7.4/r4061/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.7.4/r4061/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.7.4/r4061/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.7.4/r4061/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.7.4/r4061/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.7.4/r4061/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.7.4/r4061/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.7.4/r4061/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.7.4/r4061/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.7.4/r4061/src/edu/udel/cis/vsl/civl/model/IF/CIVLSource.java:34: warning: no @return
  [javadoc] 	String getLocation();
  [javadoc] 	       ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/model/IF/CIVLSource.java:39: warning: no description for @return
  [javadoc] 	 * @return
  [javadoc] 	   ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/model/IF/CIVLTypeFactory.java:104: warning: no description for @param
  [javadoc] 	 * @param rangeType
  [javadoc] 	   ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/model/IF/CIVLTypeFactory.java:162: error: bad use of '>'
  [javadoc] 	 * Create a new location. ======= Get the integer primitive type. >>>>>>>
  [javadoc] 	                                                                  ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/model/IF/CIVLTypeFactory.java:162: error: bad use of '>'
  [javadoc] 	 * Create a new location. ======= Get the integer primitive type. >>>>>>>
  [javadoc] 	                                                                   ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/model/IF/CIVLTypeFactory.java:162: error: bad use of '>'
  [javadoc] 	 * Create a new location. ======= Get the integer primitive type. >>>>>>>
  [javadoc] 	                                                                    ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/model/IF/CIVLTypeFactory.java:162: error: bad use of '>'
  [javadoc] 	 * Create a new location. ======= Get the integer primitive type. >>>>>>>
  [javadoc] 	                                                                     ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/model/IF/CIVLTypeFactory.java:162: error: bad use of '>'
  [javadoc] 	 * Create a new location. ======= Get the integer primitive type. >>>>>>>
  [javadoc] 	                                                                      ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/model/IF/CIVLTypeFactory.java:162: error: bad use of '>'
  [javadoc] 	 * Create a new location. ======= Get the integer primitive type. >>>>>>>
  [javadoc] 	                                                                       ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/model/IF/CIVLTypeFactory.java:162: error: bad use of '>'
  [javadoc] 	 * Create a new location. ======= Get the integer primitive type. >>>>>>>
  [javadoc] 	                                                                        ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/model/IF/CIVLTypeFactory.java:337: warning: no description for @param
  [javadoc] 	 * @param type
  [javadoc] 	   ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/model/IF/CIVLTypeFactory.java:338: warning: no description for @param
  [javadoc] 	 * @param id
  [javadoc] 	   ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/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.7.4/r4061/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.7.4/r4061/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.7.4/r4061/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.7.4/r4061/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.7.4/r4061/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.7.4/r4061/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.7.4/r4061/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:132: error: semicolon missing
  [javadoc] 	 * Returns a new address-of expression <code>(&e)</code> with given operand.
  [javadoc] 	                                              ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:160: error: malformed HTML
  [javadoc] 	 * A binary expression. One of {+,-,*,\,<,<=,==,!=,&&,||,%}
  [javadoc] 	                                        ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:160: error: malformed HTML
  [javadoc] 	 * A binary expression. One of {+,-,*,\,<,<=,==,!=,&&,||,%}
  [javadoc] 	                                          ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:160: error: bad HTML entity
  [javadoc] 	 * A binary expression. One of {+,-,*,\,<,<=,==,!=,&&,||,%}
  [javadoc] 	                                                   ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:160: error: bad HTML entity
  [javadoc] 	 * A binary expression. One of {+,-,*,\,<,<=,==,!=,&&,||,%}
  [javadoc] 	                                                    ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:196: warning: no description for @param
  [javadoc] 	 * @param expression
  [javadoc] 	   ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:319: warning: no description for @param
  [javadoc] 	 * @param source
  [javadoc] 	   ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:320: warning: no description for @param
  [javadoc] 	 * @param function
  [javadoc] 	   ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:327: warning: no description for @param
  [javadoc] 	 * @param source
  [javadoc] 	   ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:342: warning: no description for @param
  [javadoc] 	 * @param source
  [javadoc] 	   ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:343: warning: no description for @param
  [javadoc] 	 * @param variable
  [javadoc] 	   ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:462: warning: no description for @param
  [javadoc] 	 * @param source
  [javadoc] 	   ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:463: warning: no description for @param
  [javadoc] 	 * @param type
  [javadoc] 	   ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:464: warning: no description for @param
  [javadoc] 	 * @param quant
  [javadoc] 	   ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:465: warning: no description for @param
  [javadoc] 	 * @param lo
  [javadoc] 	   ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:466: warning: no description for @param
  [javadoc] 	 * @param hi
  [javadoc] 	   ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:467: warning: no description for @param
  [javadoc] 	 * @param function
  [javadoc] 	   ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:468: warning: no description for @return
  [javadoc] 	 * @return
  [javadoc] 	   ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:489: error: bad use of '>'
  [javadoc] 	 * <code>(high-low)/step >= 0 </code>.
  [javadoc] 	                         ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:508: 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.7.4/r4061/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:508: 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.7.4/r4061/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:638: warning: no description for @param
  [javadoc] 	 * @param callStatement
  [javadoc] 	   ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:657: error: bad HTML entity
  [javadoc] 	 * <code>sysCall.isCall == true && sysCall.isSystemCall() == true</code>.
  [javadoc] 	                                ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:657: error: bad HTML entity
  [javadoc] 	 * <code>sysCall.isCall == true && sysCall.isSystemCall() == true</code>.
  [javadoc] 	                                 ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:733: warning: no description for @param
  [javadoc] 	 * @param source
  [javadoc] 	   ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:734: warning: no description for @param
  [javadoc] 	 * @param function
  [javadoc] 	   ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:735: warning: no description for @param
  [javadoc] 	 * @param degree
  [javadoc] 	   ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:736: warning: no description for @param
  [javadoc] 	 * @param lowerBounds
  [javadoc] 	   ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:737: warning: no description for @param
  [javadoc] 	 * @param upperBounds
  [javadoc] 	   ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:738: warning: no description for @return
  [javadoc] 	 * @return
  [javadoc] 	   ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:877: warning: no description for @param
  [javadoc] 	 * @param domSize
  [javadoc] 	   ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:924: warning: no description for @return
  [javadoc] 	 * @return
  [javadoc] 	   ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:948: warning: no description for @return
  [javadoc] 	 * @return
  [javadoc] 	   ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:1027: error: reference not found
  [javadoc] 	 *            {@link #noopStatement(CIVLSource, Location)}.
  [javadoc] 	                     ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:1269: error: @param name not found
  [javadoc] 	 * @param expressionNode
  [javadoc] 	          ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:1276: warning: no @param for startSource
  [javadoc] 	Pair<Fragment, Expression> refineConditionalExpression(Scope scope,
  [javadoc] 	                           ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:1276: warning: no @param for endSource
  [javadoc] 	Pair<Fragment, Expression> refineConditionalExpression(Scope scope,
  [javadoc] 	                           ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:1335: warning: no @param for parameterScope
  [javadoc] 	AbstractFunction abstractFunction(CIVLSource source, Identifier name,
  [javadoc] 	                 ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:1335: warning: no @param for factory
  [javadoc] 	AbstractFunction abstractFunction(CIVLSource source, Identifier name,
  [javadoc] 	                 ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:1361: warning: no @param for parameterScope
  [javadoc] 	CIVLFunction function(CIVLSource source, boolean isAtomic, Identifier name,
  [javadoc] 	             ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:1399: warning: no @param for program
  [javadoc] 	Model model(CIVLSource source, CIVLFunction system, Program program);
  [javadoc] 	      ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:1437: warning: no @param for parameterScope
  [javadoc] 	SystemFunction systemFunction(CIVLSource source, Identifier name,
  [javadoc] 	               ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:1564: error: @param name not found
  [javadoc] 	 * @param scopeValue
  [javadoc] 	          ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:1610: error: malformed HTML
  [javadoc] 	 * <code>pid < 0</code>, returns undefinedProcessValue.
  [javadoc] 	             ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:1657: error: @param name not found
  [javadoc] 	 * @param scope
  [javadoc] 	          ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:103: error: reference not found
  [javadoc]  * {@link #function(CIVLSource, Identifier, List, CIVLType, Scope, Location)}. A
  [javadoc]           ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/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.7.4/r4061/src/edu/udel/cis/vsl/civl/model/IF/Scope.java:202: error: @param name not found
  [javadoc] 	 * @param des
  [javadoc] 	          ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/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.7.4/r4061/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.7.4/r4061/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.7.4/r4061/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.7.4/r4061/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.7.4/r4061/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.7.4/r4061/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.7.4/r4061/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.7.4/r4061/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.7.4/r4061/src/edu/udel/cis/vsl/civl/model/IF/expression/Expression.java:134: error: semicolon missing
  [javadoc] 	 * an address-of expression. e.g., <code>(&a + &b)</code> returns
  [javadoc] 	                                          ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/model/IF/expression/Expression.java:134: error: semicolon missing
  [javadoc] 	 * an address-of expression. e.g., <code>(&a + &b)</code> returns
  [javadoc] 	                                               ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/model/IF/expression/Expression.java:146: error: semicolon missing
  [javadoc] 	 * e.g., <code>(&a + &b)</code> returns <code>{a, b}</code>.
  [javadoc] 	                ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/model/IF/expression/Expression.java:146: error: semicolon missing
  [javadoc] 	 * e.g., <code>(&a + &b)</code> returns <code>{a, b}</code>.
  [javadoc] 	                     ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/model/IF/expression/Expression.java:180: error: malformed HTML
  [javadoc] 	 * e.g.: s<$here would return true.
  [javadoc] 	          ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/model/IF/expression/Expression.java:190: error: semicolon missing
  [javadoc] 	 * any error checking. e.g., &anon[0] which is used to translate array
  [javadoc] 	                             ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/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.7.4/r4061/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.7.4/r4061/src/edu/udel/cis/vsl/civl/model/IF/expression/BinaryExpression.java:17: error: unknown tag: ui
  [javadoc] 	 * <ui> <li>AND: <code>&&</code> (logical and);</li> <li>LEFT_SHIFT:
  [javadoc] 	   ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/model/IF/expression/BinaryExpression.java:17: error: tag not allowed here: <li>
  [javadoc] 	 * <ui> <li>AND: <code>&&</code> (logical and);</li> <li>LEFT_SHIFT:
  [javadoc] 	        ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/model/IF/expression/BinaryExpression.java:17: error: bad HTML entity
  [javadoc] 	 * <ui> <li>AND: <code>&&</code> (logical and);</li> <li>LEFT_SHIFT:
  [javadoc] 	                       ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/model/IF/expression/BinaryExpression.java:17: error: bad HTML entity
  [javadoc] 	 * <ui> <li>AND: <code>&&</code> (logical and);</li> <li>LEFT_SHIFT:
  [javadoc] 	                        ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/model/IF/expression/BinaryExpression.java:17: error: tag not allowed here: <li>
  [javadoc] 	 * <ui> <li>AND: <code>&&</code> (logical and);</li> <li>LEFT_SHIFT:
  [javadoc] 	                                                     ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/model/IF/expression/BinaryExpression.java:18: error: malformed HTML
  [javadoc] 	 * <code><</code> (bitwise left shift);</li> <li>RIGHT_SHIFT:
  [javadoc] 	         ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/model/IF/expression/BinaryExpression.java:18: error: tag not allowed here: <li>
  [javadoc] 	 * <code><</code> (bitwise left shift);</li> <li>RIGHT_SHIFT:
  [javadoc] 	                                             ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/model/IF/expression/BinaryExpression.java:19: error: bad use of '>'
  [javadoc] 	 * <code>>></code> (bitwise right shift);</li> <li>BITAND: <code>&</code>
  [javadoc] 	         ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/model/IF/expression/BinaryExpression.java:19: error: bad use of '>'
  [javadoc] 	 * <code>>></code> (bitwise right shift);</li> <li>BITAND: <code>&</code>
  [javadoc] 	          ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/model/IF/expression/BinaryExpression.java:19: error: tag not allowed here: <li>
  [javadoc] 	 * <code>>></code> (bitwise right shift);</li> <li>BITAND: <code>&</code>
  [javadoc] 	                                               ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/model/IF/expression/BinaryExpression.java:19: error: bad HTML entity
  [javadoc] 	 * <code>>></code> (bitwise right shift);</li> <li>BITAND: <code>&</code>
  [javadoc] 	                                                                 ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/model/IF/expression/BinaryExpression.java:20: error: tag not allowed here: <li>
  [javadoc] 	 * (bitwise and);</li> <li>BITCOMPLEMENT: <code>~</code> (bitwise
  [javadoc] 	                       ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/model/IF/expression/BinaryExpression.java:21: error: tag not allowed here: <li>
  [javadoc] 	 * complement);</li> <li>BITOR: <code>|</code> (bitwise or);</li> <li>
  [javadoc] 	                     ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/model/IF/expression/BinaryExpression.java:21: error: tag not allowed here: <li>
  [javadoc] 	 * complement);</li> <li>BITOR: <code>|</code> (bitwise or);</li> <li>
  [javadoc] 	                                                                  ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/model/IF/expression/BinaryExpression.java:22: error: tag not allowed here: <li>
  [javadoc] 	 * BITXOR: <code>^</code> (bitwise xor);</li> <li>DIVIDE: <code>/</code>
  [javadoc] 	                                              ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/model/IF/expression/BinaryExpression.java:23: error: tag not allowed here: <li>
  [javadoc] 	 * (division);</li> <li>EQUAL: <code>==</code> (equal to);</li> <li>IMPLIES:
  [javadoc] 	                    ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/model/IF/expression/BinaryExpression.java:23: error: tag not allowed here: <li>
  [javadoc] 	 * (division);</li> <li>EQUAL: <code>==</code> (equal to);</li> <li>IMPLIES:
  [javadoc] 	                                                                ^
  [javadoc] /usa/svn/work/civl/1.7.4/r4061/src/edu/udel/cis/vsl/civl/model/IF/expression/BinaryExpression.java:24: error: tag not allowed here: <li>
  [javadoc] 	 * <code></code> (implication);</li> <li>LESS_THAN: <code><</code> (less
  [javadoc] 	                                     ^
  [javadoc] Building index for all the packages and classes...
  [javadoc] Building index for all classes...
  [javadoc] Generating /usa/svn/work/civl/1.7.4/r4061/doc/javadoc/help-doc.html...
  [javadoc] 100 errors
  [javadoc] 100 warnings

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

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

all:

BUILD SUCCESSFUL
Total time: 6 minutes 42 seconds

Stderr: