Path: . Working Copy Root Path: /usa/svn/work/civl/1.13/r4606 URL: svn://vsl.cis.udel.edu/civl/trunk Relative URL: ^/trunk Repository Root: svn://vsl.cis.udel.edu/civl Repository UUID: fb995dde-84ed-4084-dfe6-e5aef3e2452c Revision: 4606 Node Kind: directory Schedule: normal Last Changed Author: ziqing Last Changed Rev: 4606 Last Changed Date: 2018-02-03 12:14:36 -0500 (Sat, 03 Feb 2018)
Stdout:
Buildfile: /usa/svn/work/civl/1.13/r4606/build.xml
checkCommandParserChanges:
CommandParser:
[move] Moving 1 file to /usa/svn/work/civl/1.13/r4606/src/edu/udel/cis/vsl/civl/run/common
[move] Moving 1 file to /usa/svn/work/civl/1.13/r4606/src/edu/udel/cis/vsl/civl/run/common
[move] Moving 1 file to /usa/svn/work/civl/1.13/r4606/src/edu/udel/cis/vsl/civl/run/common
[move] Moving 1 file to /usa/svn/work/civl/1.13/r4606/src/edu/udel/cis/vsl/civl/run/common
compile:
[mkdir] Created dir: /usa/svn/work/civl/1.13/r4606/bin
[javac] Compiling 507 source files to /usa/svn/work/civl/1.13/r4606/bin
[javac] Creating empty /usa/svn/work/civl/1.13/r4606/bin/edu/udel/cis/vsl/civl/model/IF/expression/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.13/r4606/bin/edu/udel/cis/vsl/civl/state/IF/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.13/r4606/bin/edu/udel/cis/vsl/civl/gui/IF/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.13/r4606/bin/edu/udel/cis/vsl/civl/gui/common/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.13/r4606/bin/edu/udel/cis/vsl/civl/semantics/IF/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.13/r4606/bin/edu/udel/cis/vsl/civl/kripke/IF/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.13/r4606/bin/edu/udel/cis/vsl/civl/util/IF/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.13/r4606/bin/edu/udel/cis/vsl/civl/library/domain/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.13/r4606/bin/edu/udel/cis/vsl/civl/model/IF/type/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.13/r4606/bin/edu/udel/cis/vsl/civl/library/comm/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.13/r4606/bin/edu/udel/cis/vsl/civl/library/pointer/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.13/r4606/bin/edu/udel/cis/vsl/civl/model/IF/location/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.13/r4606/bin/edu/udel/cis/vsl/civl/library/time/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.13/r4606/bin/edu/udel/cis/vsl/civl/library/pthread/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.13/r4606/bin/edu/udel/cis/vsl/civl/config/IF/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.13/r4606/bin/edu/udel/cis/vsl/civl/dynamic/IF/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.13/r4606/bin/edu/udel/cis/vsl/civl/library/civlc/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.13/r4606/bin/edu/udel/cis/vsl/civl/log/IF/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.13/r4606/bin/edu/udel/cis/vsl/civl/library/common/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.13/r4606/bin/edu/udel/cis/vsl/civl/model/IF/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.13/r4606/bin/edu/udel/cis/vsl/civl/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.13/r4606/bin/edu/udel/cis/vsl/civl/model/IF/variable/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.13/r4606/bin/edu/udel/cis/vsl/civl/library/seq/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.13/r4606/bin/edu/udel/cis/vsl/civl/library/string/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.13/r4606/bin/edu/udel/cis/vsl/civl/analysis/IF/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.13/r4606/bin/edu/udel/cis/vsl/civl/library/scope/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.13/r4606/bin/edu/udel/cis/vsl/civl/model/IF/statement/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.13/r4606/bin/edu/udel/cis/vsl/civl/predicate/IF/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.13/r4606/bin/edu/udel/cis/vsl/civl/library/bundle/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.13/r4606/bin/edu/udel/cis/vsl/civl/slice/common/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.13/r4606/bin/edu/udel/cis/vsl/civl/slice/IF/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.13/r4606/bin/edu/udel/cis/vsl/civl/run/IF/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.13/r4606/bin/edu/udel/cis/vsl/civl/transform/IF/package-info.class
[copy] Copying 30 files to /usa/svn/work/civl/1.13/r4606/bin/include
jar:
[jar] Building jar: /usa/svn/work/civl/1.13/r4606/civl.jar
test-init:
[mkdir] Created dir: /usa/svn/work/civl/1.13/r4606/junit
[mkdir] Created dir: /usa/svn/work/civl/1.13/r4606/junit/data
[mkdir] Created dir: /usa/svn/work/civl/1.13/r4606/junit/reports
[mkdir] Created dir: /usa/svn/work/civl/1.13/r4606/bin-test/regress
test-compile:
[javac] Compiling 34 source files to /usa/svn/work/civl/1.13/r4606/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.597 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.ArithmeticTest
[junit] Tests run: 24, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 7.776 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.BackendTest
[junit] Tests run: 16, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 2.156 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.CompareTest
[junit] Tests run: 4, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 4.007 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.ConcurrencyTest
[junit] Tests run: 34, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 11.047 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.LanguageFeaturesTest
[junit] Tests run: 132, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 12.367 sec
[junit]
[junit] ------------- Standard Output ---------------
[junit] CIVL v1.13 of 2018-02-03 -- http://vsl.cis.udel.edu/civl
[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) : 825753600
[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.13 of 2018-02-03 -- 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] int X = 1;
[junit] //======================= assert.cvl =======================
[junit] $atomic_f void assert(_Bool expr) {
[junit] $assert(expr);
[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) : 829947904
[junit] max process count : 0
[junit] states : 5
[junit] states saved : 2
[junit] state matches : 0
[junit] transitions : 5
[junit] trace steps : 1
[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] ------------- ---------------- ---------------
[junit] Testsuite: edu.udel.cis.vsl.civl.LibraryTest
[junit] Tests run: 70, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 8.714 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.ModelBuilderTest
[junit] Tests run: 8, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.455 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.PORTest
[junit] Tests run: 15, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.773 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.QuietOptionTest
[junit] Tests run: 5, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 2.245 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.ReasoningTest
[junit] Tests run: 8, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 1.48 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.088 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.ShowStatesTest
[junit] Tests run: 2, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.09 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.SimpleMPITest
[junit] Tests run: 23, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 39.699 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.SpecialStatementsTest
[junit] Tests run: 7, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.283 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.SvcompTest
[junit] Tests run: 10, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 6.874 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.VerifyThisTest
[junit] Tests run: 10, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 17.17 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.transform.CompareTest
[junit] Tests run: 10, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 38.25 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.transform.ContractTest
[junit] Tests run: 6, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 15.756 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.transform.CudaTest
[junit] Tests run: 3, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 8.594 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.transform.GenTransformerTest
[junit] Tests run: 3, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 2.449 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.transform.IOTransformerTest
[junit] Tests run: 4, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 1.129 sec
[junit]
[junit] ------------- Standard Output ---------------
[junit] CIVL v1.13 of 2018-02-03 -- http://vsl.cis.udel.edu/civl
[junit]
[junit] === Command ===
[junit] civl verify -enablePrintf=false examples/io/printf.cvl
[junit]
[junit] === Stats ===
[junit] time (s) : 0.11
[junit] memory (bytes) : 943194112
[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.13 of 2018-02-03 -- http://vsl.cis.udel.edu/civl
[junit]
[junit] === Command ===
[junit] civl verify examples/io/fscanf.cvl
[junit]
[junit] === Stats ===
[junit] time (s) : 0.12
[junit] memory (bytes) : 943194112
[junit] max process count : 1
[junit] states : 52
[junit] states saved : 44
[junit] state matches : 0
[junit] transitions : 51
[junit] trace steps : 28
[junit] valid calls : 167
[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.LoopInvariantsTest
[junit] Tests run: 18, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 7.68 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.transform.MPICollectivePart1Test
[junit] Tests run: 20, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 33.789 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.transform.MPICollectivePart2Test
[junit] Tests run: 25, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 46.529 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.transform.MPITranslationTest
[junit] Tests run: 19, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 38.585 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.transform.MPI_OpenMPTest
[junit] Tests run: 3, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 6.652 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.transform.OmpHelpersTest
[junit] Tests run: 9, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 2.556 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.transform.OpenMP2CIVLTransformerTest
[junit] Tests run: 7, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 14.857 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.transform.PthreadTest
[junit] Tests run: 16, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 11.982 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.transform.PthreadThreaderTest
[junit] Tests run: 8, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 1.824 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.transform.SideEffectsTest
[junit] Tests run: 10, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.381 sec
[junit]
[junitreport] Processing /usa/svn/work/civl/1.13/r4606/junit/data/TESTS-TestSuites.xml to /tmp/null441420190
[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: 410ms
[junitreport] Deleting: /tmp/null441420190
test:
[jacoco:report] Loading execution data file /usa/svn/work/civl/1.13/r4606/jacoco.exec
[jacoco:report] Writing bundle 'Test Coverage Report for CIVL 1.13 r4606 Regression Suite' with 489 classes
javadoc:
[mkdir] Created dir: /usa/svn/work/civl/1.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/src/edu/udel/cis/vsl/civl/config/IF/CIVLConfiguration.java:757: warning: no @return
[javadoc] public int getProcBound() {
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:340: error: reference not found
[javadoc] * {@link #isPointerToHeap(heapPointer)} must returns true.
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.13/r4606/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:393: error: semicolon missing
[javadoc] * pointer. For example, given a pointer &a[5] and a reference [0], the
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.13/r4606/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:394: 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.13/r4606/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:663: error: tag not allowed here: <li>
[javadoc] * <li>length(array_extents) > 0</li>
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.13/r4606/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:663: error: bad use of '>'
[javadoc] * <li>length(array_extents) > 0</li>
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.13/r4606/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:664: error: unexpected end tag: </p>
[javadoc] * </p>
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.13/r4606/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:673: 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.13/r4606/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:675: error: exception not thrown: edu.udel.cis.vsl.civl.state.IF.UnsatisfiablePathConditionException
[javadoc] * @throws UnsatisfiablePathConditionException
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.13/r4606/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:675: warning: no description for @throws
[javadoc] * @throws UnsatisfiablePathConditionException
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.13/r4606/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:763: warning: no description for @param
[javadoc] * @param domain
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.13/r4606/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:771: warning: no description for @param
[javadoc] * @param range
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.13/r4606/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:781: warning: no description for @param
[javadoc] * @param domain
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.13/r4606/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:782: warning: no description for @param
[javadoc] * @param index
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.13/r4606/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:793: warning: no description for @param
[javadoc] * @param range
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.13/r4606/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:803: warning: no description for @param
[javadoc] * @param range
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.13/r4606/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:814: warning: no description for @param
[javadoc] * @param range
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.13/r4606/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:822: warning: no description for @param
[javadoc] * @param domain
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.13/r4606/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:829: 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.13/r4606/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:829: 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.13/r4606/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:829: 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.13/r4606/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:829: 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.13/r4606/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:829: 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.13/r4606/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:829: 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.13/r4606/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:829: 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.13/r4606/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:830: 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.13/r4606/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:830: 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.13/r4606/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:830: 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.13/r4606/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:832: warning: no description for @param
[javadoc] * @param cnfClause
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.13/r4606/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:840: warning: no description for @param
[javadoc] * @param function
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.13/r4606/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:841: error: @param name not found
[javadoc] * @param arguments
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.13/r4606/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:841: warning: no description for @param
[javadoc] * @param arguments
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.13/r4606/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:842: warning: no description for @return
[javadoc] * @return
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.13/r4606/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:844: warning: no @param for library
[javadoc] SymbolicExpression getAbstractGuardOfFunctionCall(String library,
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.13/r4606/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:844: warning: no @param for argumentValues
[javadoc] SymbolicExpression getAbstractGuardOfFunctionCall(String library,
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.13/r4606/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:854: warning: no description for @param
[javadoc] * @param originalFunction
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.13/r4606/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:855: warning: no description for @param
[javadoc] * @param argument
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.13/r4606/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:856: warning: no description for @return
[javadoc] * @return
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.13/r4606/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:868: warning: no description for @param
[javadoc] * @param range
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.13/r4606/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:869: warning: no description for @return
[javadoc] * @return
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.13/r4606/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:871: warning: no @param for reasoner
[javadoc] BitSet range2BitSet(SymbolicExpression range, Reasoner reasoner);
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.13/r4606/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:883: warning: no description for @param
[javadoc] * @param pointer
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.13/r4606/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:884: warning: no description for @return
[javadoc] * @return
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.13/r4606/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:343: warning - Tag @link: can't find isPointerToHeap(heapPointer) in edu.udel.cis.vsl.civl.dynamic.IF.SymbolicUtility
[javadoc] /usa/svn/work/civl/1.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/src/edu/udel/cis/vsl/civl/model/IF/CIVLSource.java:34: warning: no @return
[javadoc] String getLocation();
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:445: error: @param name not found
[javadoc] * @param boundVariableList
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.13/r4606/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:452: warning: no @param for variable
[javadoc] LambdaExpression lambdaExpression(CIVLSource source,
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.13/r4606/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:458: warning: no description for @param
[javadoc] * @param source
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.13/r4606/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:459: warning: no description for @param
[javadoc] * @param type
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.13/r4606/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:460: warning: no description for @param
[javadoc] * @param quant
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.13/r4606/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:461: warning: no description for @param
[javadoc] * @param lo
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.13/r4606/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:462: warning: no description for @param
[javadoc] * @param hi
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.13/r4606/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:463: warning: no description for @param
[javadoc] * @param function
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.13/r4606/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:464: warning: no description for @return
[javadoc] * @return
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.13/r4606/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:485: error: bad use of '>'
[javadoc] * <code>(high-low)/step >= 0 </code>.
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.13/r4606/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:504: 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.13/r4606/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:504: 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.13/r4606/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:634: warning: no description for @param
[javadoc] * @param callStatement
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.13/r4606/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:653: error: bad HTML entity
[javadoc] * <code>sysCall.isCall == true && sysCall.isSystemCall() == true</code>.
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.13/r4606/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:653: error: bad HTML entity
[javadoc] * <code>sysCall.isCall == true && sysCall.isSystemCall() == true</code>.
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.13/r4606/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:729: warning: no description for @param
[javadoc] * @param source
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.13/r4606/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:730: warning: no description for @param
[javadoc] * @param function
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.13/r4606/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:731: warning: no description for @param
[javadoc] * @param degree
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.13/r4606/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:732: warning: no description for @param
[javadoc] * @param lowerBounds
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.13/r4606/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:733: warning: no description for @param
[javadoc] * @param upperBounds
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.13/r4606/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:734: warning: no description for @return
[javadoc] * @return
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.13/r4606/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:873: warning: no description for @param
[javadoc] * @param domSize
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.13/r4606/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:920: warning: no description for @return
[javadoc] * @return
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.13/r4606/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:944: warning: no description for @return
[javadoc] * @return
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.13/r4606/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:1023: error: reference not found
[javadoc] * {@link #noopStatement(CIVLSource, Location)}.
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.13/r4606/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:1265: error: @param name not found
[javadoc] * @param expressionNode
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.13/r4606/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:1547: error: @param name not found
[javadoc] * @param source
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.13/r4606/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:1549: error: @param name not found
[javadoc] * @param scopeValue
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.13/r4606/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:1576: error: @param name not found
[javadoc] * @param source
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.13/r4606/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:1630: error: @param name not found
[javadoc] * @param scope
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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.13/r4606/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] Building index for all the packages and classes...
[javadoc] Building index for all classes...
[javadoc] Generating /usa/svn/work/civl/1.13/r4606/doc/javadoc/help-doc.html...
[javadoc] 100 errors
[javadoc] 100 warnings
bench-compile:
[javac] Compiling 6 source files to /usa/svn/work/civl/1.13/r4606/bin
bench-scale-compile:
[javac] Compiling 5 source files to /usa/svn/work/civl/1.13/r4606/bin
all:
BUILD SUCCESSFUL
Total time: 6 minutes 5 seconds
Stderr: