Path: . Working Copy Root Path: /usa/svn/work/civl/1.7.2/r3714 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: 3714 Node Kind: directory Schedule: normal Last Changed Author: ziqing Last Changed Rev: 3714 Last Changed Date: 2016-09-30 19:03:26 -0400 (Fri, 30 Sep 2016)
Stdout:
Buildfile: /usa/svn/work/civl/1.7.2/r3714/build.xml
checkCommandParserChanges:
CommandParser:
[move] Moving 1 file to /usa/svn/work/civl/1.7.2/r3714/src/edu/udel/cis/vsl/civl/run/common
[move] Moving 1 file to /usa/svn/work/civl/1.7.2/r3714/src/edu/udel/cis/vsl/civl/run/common
[move] Moving 1 file to /usa/svn/work/civl/1.7.2/r3714/src/edu/udel/cis/vsl/civl/run/common
[move] Moving 1 file to /usa/svn/work/civl/1.7.2/r3714/src/edu/udel/cis/vsl/civl/run/common
compile:
[mkdir] Created dir: /usa/svn/work/civl/1.7.2/r3714/bin
[javac] Compiling 493 source files to /usa/svn/work/civl/1.7.2/r3714/bin
[javac] Creating empty /usa/svn/work/civl/1.7.2/r3714/bin/edu/udel/cis/vsl/civl/model/IF/expression/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.7.2/r3714/bin/edu/udel/cis/vsl/civl/state/IF/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.7.2/r3714/bin/edu/udel/cis/vsl/civl/gui/IF/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.7.2/r3714/bin/edu/udel/cis/vsl/civl/gui/common/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.7.2/r3714/bin/edu/udel/cis/vsl/civl/semantics/IF/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.7.2/r3714/bin/edu/udel/cis/vsl/civl/kripke/IF/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.7.2/r3714/bin/edu/udel/cis/vsl/civl/util/IF/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.7.2/r3714/bin/edu/udel/cis/vsl/civl/library/domain/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.7.2/r3714/bin/edu/udel/cis/vsl/civl/model/IF/type/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.7.2/r3714/bin/edu/udel/cis/vsl/civl/library/comm/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.7.2/r3714/bin/edu/udel/cis/vsl/civl/library/pointer/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.7.2/r3714/bin/edu/udel/cis/vsl/civl/model/IF/location/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.7.2/r3714/bin/edu/udel/cis/vsl/civl/library/time/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.7.2/r3714/bin/edu/udel/cis/vsl/civl/library/pthread/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.7.2/r3714/bin/edu/udel/cis/vsl/civl/config/IF/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.7.2/r3714/bin/edu/udel/cis/vsl/civl/dynamic/IF/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.7.2/r3714/bin/edu/udel/cis/vsl/civl/library/civlc/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.7.2/r3714/bin/edu/udel/cis/vsl/civl/log/IF/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.7.2/r3714/bin/edu/udel/cis/vsl/civl/library/common/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.7.2/r3714/bin/edu/udel/cis/vsl/civl/model/IF/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.7.2/r3714/bin/edu/udel/cis/vsl/civl/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.7.2/r3714/bin/edu/udel/cis/vsl/civl/model/IF/variable/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.7.2/r3714/bin/edu/udel/cis/vsl/civl/library/seq/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.7.2/r3714/bin/edu/udel/cis/vsl/civl/library/string/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.7.2/r3714/bin/edu/udel/cis/vsl/civl/analysis/IF/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.7.2/r3714/bin/edu/udel/cis/vsl/civl/library/scope/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.7.2/r3714/bin/edu/udel/cis/vsl/civl/model/IF/statement/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.7.2/r3714/bin/edu/udel/cis/vsl/civl/predicate/IF/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.7.2/r3714/bin/edu/udel/cis/vsl/civl/library/bundle/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.7.2/r3714/bin/edu/udel/cis/vsl/civl/slice/common/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.7.2/r3714/bin/edu/udel/cis/vsl/civl/slice/IF/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.7.2/r3714/bin/edu/udel/cis/vsl/civl/run/IF/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.7.2/r3714/bin/edu/udel/cis/vsl/civl/transform/IF/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.7.2/r3714/bin/edu/udel/cis/vsl/civl/library/concurrency/package-info.class
[copy] Copying 28 files to /usa/svn/work/civl/1.7.2/r3714/bin/include
jar:
[jar] Building jar: /usa/svn/work/civl/1.7.2/r3714/civl.jar
test-init:
[mkdir] Created dir: /usa/svn/work/civl/1.7.2/r3714/junit
[mkdir] Created dir: /usa/svn/work/civl/1.7.2/r3714/junit/data
[mkdir] Created dir: /usa/svn/work/civl/1.7.2/r3714/junit/reports
[mkdir] Created dir: /usa/svn/work/civl/1.7.2/r3714/bin-test/regress
test-compile:
[javac] Compiling 31 source files to /usa/svn/work/civl/1.7.2/r3714/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: 6.716 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.ArithmeticTest
[junit] Tests run: 23, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 14.868 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: 17, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 2.115 sec
[junit]
[junit] ------------- Standard Output ---------------
[junit] CIVL v1.7.1+ of 2016-05-31 -- 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] CIVL v1.7.1+ of 2016-05-31 -- http://vsl.cis.udel.edu/civl
[junit] Executed by p0 from State 0:
[junit] 0->11: gcollator=$gcollator_create(d0, 1) at valueat.cvl:3.0-47 "$gcollator gcollator=$gcollator_create($here, ... )"
[junit] 11->12: gcollator=(struct _gcollator*)$malloc(d0, SIZEOF(193)) [gcollator:=&<d0>heap.malloc0[0][0]] at collate.cvl:72.2-77 "$gcollator gcollator = ($gcollator) ... )"
[junit] 12->13: (*(&<d0>heap.malloc0[0][0])).nprocs=1 at collate.cvl:74.2-27 "gcollator->nprocs = nprocs"
[junit] 13->14: (*(&<d0>heap.malloc0[0][0])).procs={[0]=$proc_null} at collate.cvl:75.2-60 "gcollator->procs = ($proc[ ... $proc_null"
[junit] 14->15: (*(&<d0>heap.malloc0[0][0])).queue_length=0 at collate.cvl:76.2-28 "gcollator->queue_length = 0"
[junit] 15->16: $seq_init(&<d0>heap.malloc0[0][0].queue, 0, ((void)*)0) at collate.cvl:77.2-40 "$seq_init(&(gcollator->queue), ... )"
[junit] 16->17: (*(&<d0>heap.malloc0[0][0])).entered={[0]=false} at collate.cvl:78.2-civlc.cvh:13.15 "gcollator->entered=(_Bool[nprocs] ... 0"
[junit] 17->RET: $gcollator_create(...) return &<d0>heap.malloc0[0][0] [gcollator:=&<d0>heap.malloc0[0][0]] at collate.cvl:79.2-18 "return gcollator;"
[junit] --> State 1
[junit] Executed by p0 from State 1:
[junit] 1->18: collator=$collator_create(&<d0>heap.malloc0[0][0], d0, 0) at valueat.cvl:4.0-55 "$collator collator=$collator_create(gcollator, ... )"
[junit] 18->19: collator=(struct _collator*)$malloc(d0, SIZEOF(198)) [collator:=&<d0>heap.malloc1[0][0]] at collate.cvl:94.2-73 "$collator collator = ($collator) ... )"
[junit] 19->20: (*(&<d0>heap.malloc1[0][0])).place=0 at collate.cvl:96.2-24 "collator->place = place"
[junit] 20->21: (*(&<d0>heap.malloc1[0][0])).gcollator=&<d0>heap.malloc0[0][0] at collate.cvl:97.2-32 "collator->gcollator = gcollator"
[junit] 21->22: (*(&<d0>heap.malloc0[0][0])).procs[0]=$self [(*(&<d0>heap.malloc0[0][0])).procs[0]:=p0] at collate.cvl:98.2-42 "collator->gcollator->procs[place] ... $self"
[junit] 22->RET: $collator_create(...) return &<d0>heap.malloc1[0][0] [collator:=&<d0>heap.malloc1[0][0]] at collate.cvl:99.2-17 "return collator;"
[junit] 2->3: i=0 at valueat.cvl:7.2-8 "int i=0"
[junit] --> State 2
[junit] Executed by p0 from State 2:
[junit] 3->23: pre=$collate_arrives(&<d0>heap.malloc1[0][0], d1) at valueat.cvl:8.2-53 "$collate_state pre=$collate_arrives(collator, ... )"
[junit] 23->24: place=0 at collate.cvl:118.2-21 "int place = c->place"
[junit] 24->25: first=true at collate.cvl:120.2-civlc.cvh:11.14 "_Bool first = 1"
[junit] 25->26: result=InitialValue(result) [result:=Y0] at collate.cvl:123.2-22 "$collate_state result"
[junit] 26->27: nprocs=1 at collate.cvl:125.2-30 "nprocs = c->gcollator->nprocs"
[junit] 27->28: queue=&<d0>heap.malloc0[0][0].queue[0] at collate.cvl:126.2-28 "queue = c->gcollator->queue"
[junit] 28->29: queue_size=0 at collate.cvl:127.2-40 "queue_size = c->gcollator->queue_length"
[junit] 29->30: i=0 at collate.cvl:131.7-15 "int i = 0"
[junit] --> State 3
[junit] Executed by p0 from State 3:
[junit] 30->36: LOOP_BODY_EXIT (guard: !(0<0)) at collate.cvl:131.18-31 "i < queue_size"
[junit] 36->37: TRUE_BRANCH_IF (guard: true) at collate.cvl:137.13 "{"
[junit] 37->38: root=$scopeof(*((*(c)).1)) [root:=d0] at collate.cvl:139.4-40 "$scope root = $scopeof(* ... )"
[junit] 38->39: gcollate_state=(struct _gcollate_state*)$malloc(d0, SIZEOF(202)) [gcollate_state:=&<d0>heap.malloc2[0][0]] at collate.cvl:141.4-82 "gcollate_state = ($gcollate_state)$malloc( ... )"
[junit] 39->40: (*(&<d0>heap.malloc2[0][0])).status={[0]=0} at collate.cvl:142.4-9.19 "gcollate_state->status = (int[ ... 0"
[junit] 40->41: (*(&<d0>heap.malloc2[0][0])).state=$state_null [(*(&<d0>heap.malloc2[0][0])).state:={-1}] at collate.cvl:143.4-38 "gcollate_state->state = $state_null"
[junit] 41->76: $seq_append(&<d0>heap.malloc0[0][0].queue, &<d3>gcollate_state, 1) at collate.cvl:144.4-56 "$seq_append(&c->gcollator->queue, ... )"
[junit] 76->77: length=$seq_length(&<d0>heap.malloc0[0][0].queue) [length:=0] at seq.cvl:6.2-32 "int length = $seq_length(array)"
[junit] 77->78: $seq_insert(&<d0>heap.malloc0[0][0].queue, 0, &<d3>gcollate_state, 1) at seq.cvl:8.2-42 "$seq_insert(array, length, values ... )"
[junit] 78->RET: $seq_append(...) return at seq.cvl:9.0 "}"
[junit] 42->43: (*(&<d0>heap.malloc0[0][0])).queue_length=0+1 [(*(&<d0>heap.malloc0[0][0])).queue_length:=1] at collate.cvl:145.4-29 "c->gcollator->queue_length"
[junit] 43->44: (result).place=0 at collate.cvl:147.2-21 "result.place = place"
[junit] 44->45: (result).gstate=&<d0>heap.malloc2[0][0] at collate.cvl:148.2-31 "result.gstate = gcollate_state"
[junit] 45->46: $collate_snapshot({.place=0, .gstate=&<d0>heap.malloc2[0][0]}, 1, d1) at collate.cvl:149.2-41 "$collate_snapshot(result, nprocs, scope)"
[junit] 46->47: (*(&<d0>heap.malloc2[0][0])).status[0]=1 at collate.cvl:150.2-10.19 "gcollate_state->status[place] = 1"
[junit] 47->RET: $collate_arrives(...) return {.place=0, .gstate=&<d0>heap.malloc2[0][0]} [pre:={.place=0, .gstate=&<d0>heap.malloc2[0][0]}] at collate.cvl:151.2-15 "return result;"
[junit] 4->5: i=0+1 [i:=1] at valueat.cvl:10.2 "i"
[junit] 5->75: $sef$0=$collate_get_state({.place=0, .gstate=&<d0>heap.malloc2[0][0]}) at valueat.cvl:11.20-42 "$collate_get_state(pre)"
[junit] 75->RET: $collate_get_state(...) return {4} [$sef$0:={4}] at collate.cvl:244.2-28 "return state.gstate->state;"
[junit] 6->7: $assert($value_at({4}, 0, 0)!=1) at valueat.cvl:11.2-55 "$assert($value_at($collate_get_state(pre), ... )"
[junit] --> State 5
[junit] Executed by p0 from State 5:
[junit] 7->48: $collate_departs(&<d0>heap.malloc1[0][0], {.place=0, .gstate=&<d0>heap.malloc2[0][0]}) at valueat.cvl:12.2-32 "$collate_departs(collator, pre)"
[junit] 48->49: gcollate_state=&<d0>heap.malloc2[0][0] at collate.cvl:157.2-43 "$gcollate_state gcollate_state = cs.gstate"
[junit] 49->50: place=0 at collate.cvl:159.2-17 "place = c->place"
[junit] 50->51: nprocs=1 at collate.cvl:160.2-30 "nprocs = c->gcollator->nprocs"
[junit] 51->52: queue_size=1 at collate.cvl:161.2-40 "queue_size = c->gcollator->queue_length"
[junit] 52->53: queue=&<d0>heap.malloc0[0][0].queue[0] at collate.cvl:162.2-28 "queue = c->gcollator->queue"
[junit] 53->54: $assert(((0<=1)&&(1<=2))&&((1==1)||(1==2)), "Only an arrived collate state can be freed ") at collate.cvl:163.2-165.47 "$assert(((gcollate_state)->status[ ... )"
[junit] 54->55: (*(&<d0>heap.malloc2[0][0])).status[0]=2 at collate.cvl:167.2-11.19 "gcollate_state->status[place] = 2"
[junit] 55->56: index=-1 at collate.cvl:171.2-11 "index = -1"
[junit] 56->57: i=0 at collate.cvl:172.7-15 "int i = 0"
[junit] --> State 6
[junit] Executed by p0 from State 6:
[junit] 57->58: LOOP_BODY_ENTER (guard: 0<1) at collate.cvl:172.18-31 "i < queue_size"
[junit] 58->59: isGarbage=true at collate.cvl:173.4-civlc.cvh:11.14 "_Bool isGarbage = 1"
[junit] 59->60: j=0 at collate.cvl:175.9-17 "int j = 0"
[junit] --> State 7
[junit] Executed by p0 from State 7:
[junit] 60->61: LOOP_BODY_ENTER (guard: 0<1) at collate.cvl:175.20-29 "j < nprocs"
[junit] 61->64: FALSE_BRANCH_IF (guard: !!(2==2)) at collate.cvl:179.6 "}"
[junit] 64->60: j=0+1 [j:=1] at collate.cvl:175.32 "j"
[junit] --> State 8
[junit] Executed by p0 from State 8:
[junit] 60->65: LOOP_BODY_EXIT (guard: !(1<1)) at collate.cvl:175.20-29 "j < nprocs"
[junit] --> State 9
[junit] Executed by p0 from State 9:
[junit] 65->66: TRUE_BRANCH_IF (guard: true) at collate.cvl:180.19 "{"
[junit] 66->67: index=0 at collate.cvl:181.6-14 "index = i"
[junit] 67->68: $free(&<d0>heap.malloc2[0][0]) at collate.cvl:182.6-26 "$free(gcollate_state)"
[junit] 68->70: NO_OP (guard: true) at collate.cvl:183.6-11 "break;"
[junit] 70->71: TRUE_BRANCH_IF (guard: 0<=0) at collate.cvl:186.18 "{"
[junit] 71->72: $seq_remove(&<d0>heap.malloc0[0][0].queue, 0, ((void)*)0, 1) at collate.cvl:187.4-52 "$seq_remove(&c->gcollator->queue, ... )"
[junit] 72->73: (*(&<d0>heap.malloc0[0][0])).queue_length=1-1 [(*(&<d0>heap.malloc0[0][0])).queue_length:=0] at collate.cvl:188.4-29 "c->gcollator->queue_length"
[junit] 73->74: (cs).gstate=((struct _gcollate_state)*)0 [(cs).gstate:=(void*)0] at collate.cvl:192.2-civlc.cvh:16.22 "cs.gstate = ((void ... )"
[junit] 74->RET: $collate_departs(...) return at collate.cvl:193.0 "}"
[junit] --> State 10
[junit] Executed by p0 from State 10:
[junit] 8->9: $free(&<d0>heap.malloc1[0][0]) at valueat.cvl:13.2-16 "$free(collator)"
[junit] --> State 11
[junit] Executed by p0 from State 11:
[junit] 9->10: $free(&<d0>heap.malloc0[0][0]) at valueat.cvl:14.2-17 "$free(gcollator)"
[junit] 10->RET: main(...) return at valueat.cvl:15.0 "}"
[junit] --> State 12
[junit]
[junit] === Command ===
[junit] civl verify -showTransitions examples/backend/valueat.cvl
[junit]
[junit] === Stats ===
[junit] time (s) : 0.16
[junit] memory (bytes) : 713555968
[junit] max process count : 1
[junit] states : 73
[junit] states saved : 13
[junit] state matches : 0
[junit] transitions : 72
[junit] trace steps : 11
[junit] valid calls : 117
[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.CompareTest
[junit] Tests run: 2, Failures: 2, Errors: 0, Skipped: 0, Time elapsed: 0.764 sec
[junit]
[junit] ------------- Standard Output ---------------
[junit] CIVL v1.7.1+ of 2016-05-31 -- http://vsl.cis.udel.edu/civl
[junit] CIVL v1.7.1+ of 2016-05-31 -- http://vsl.cis.udel.edu/civl
[junit] ------------- ---------------- ---------------
[junit] ------------- Standard Error -----------------
[junit] Error: Typedef name used before definition?
[junit] at spec.c:13.8-15 "PetscInt"
[junit] Syntax error: missing the definition of function PetscLogFlops
[junit] at petsc.h:61.0-36 "PetscErrorCode PetscLogFlops(double )" included from ex2Driver.c:9.
[junit] ------------- ---------------- ---------------
[junit] Testcase: typeAnalyzerException(edu.udel.cis.vsl.civl.CompareTest): FAILED
[junit] null
[junit] junit.framework.AssertionFailedError
[junit] at edu.udel.cis.vsl.civl.CompareTest.typeAnalyzerException(CompareTest.java:29)
[junit]
[junit]
[junit] Testcase: unableExtractInt(edu.udel.cis.vsl.civl.CompareTest): FAILED
[junit] null
[junit] junit.framework.AssertionFailedError
[junit] at edu.udel.cis.vsl.civl.CompareTest.unableExtractInt(CompareTest.java:34)
[junit]
[junit]
[junit] TEST edu.udel.cis.vsl.civl.CompareTest FAILED
[junit] Testsuite: edu.udel.cis.vsl.civl.ConcurrencyTest
[junit] Tests run: 32, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 11.028 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.ContractsTest
[junit] Tests run: 1, Failures: 0, Errors: 1, Skipped: 0, Time elapsed: 0.002 sec
[junit]
[junit] Testcase: initializationError(edu.udel.cis.vsl.civl.ContractsTest): Caused an ERROR
[junit] No runnable methods
[junit] java.lang.Exception: No runnable methods
[junit] at java.lang.reflect.Constructor.newInstance(Constructor.java:422)
[junit]
[junit]
[junit] TEST edu.udel.cis.vsl.civl.ContractsTest FAILED
[junit] Testsuite: edu.udel.cis.vsl.civl.LanguageFeaturesTest
[junit] Tests run: 127, Failures: 0, Errors: 0, Skipped: 1, Time elapsed: 10.58 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: missing the definition of function dummy
[junit] at civlValueUndefined.cvl:9.0-15 "int dummy(int x)".
[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] Testcase: bigO(edu.udel.cis.vsl.civl.LanguageFeaturesTest):SKIPPED
[junit] Testsuite: edu.udel.cis.vsl.civl.LibraryTest
[junit] Tests run: 51, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 4.743 sec
[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.22 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.PORTest
[junit] Tests run: 14, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.412 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.QuietOptionTest
[junit] Tests run: 5, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 2.045 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.ReasoningTest
[junit] Tests run: 5, Failures: 1, Errors: 0, Skipped: 0, Time elapsed: 0.244 sec
[junit]
[junit] Testcase: quantified(edu.udel.cis.vsl.civl.ReasoningTest): FAILED
[junit] null
[junit] junit.framework.AssertionFailedError
[junit] at edu.udel.cis.vsl.civl.ReasoningTest.quantified(ReasoningTest.java:54)
[junit]
[junit]
[junit] TEST edu.udel.cis.vsl.civl.ReasoningTest FAILED
[junit] Testsuite: edu.udel.cis.vsl.civl.ShowStatesTest
[junit] Tests run: 2, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.054 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.SimpleMPITest
[junit] Tests run: 24, Failures: 0, Errors: 0, Skipped: 1, Time elapsed: 35.077 sec
[junit]
[junit] Testcase: goodInitFinalize(edu.udel.cis.vsl.civl.SimpleMPITest):SKIPPED
[junit] Testsuite: edu.udel.cis.vsl.civl.SpecialStatementsTest
[junit] Tests run: 7, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.124 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: 1, Errors: 0, Skipped: 2, Time elapsed: 4.864 sec
[junit]
[junit] ------------- Standard Error -----------------
[junit] Error: Re-use of tag Operation for enumeration. Previous use was at op.h:6.8-20.9 "enum Operation{\n _NO_OP, ... _REPLACE" included from civlc.cvh:8
[junit] at op.h:6.8-20.9 "enum Operation{\n _NO_OP, ... _REPLACE" included from civlc.cvh:8
[junit] ------------- ---------------- ---------------
[junit] Testcase: stack_longest_true(edu.udel.cis.vsl.civl.SvcompTest): FAILED
[junit] null
[junit] junit.framework.AssertionFailedError
[junit] at edu.udel.cis.vsl.civl.SvcompTest.stack_longest_true(SvcompTest.java:62)
[junit]
[junit]
[junit] Testcase: fmaxsym_cas_true(edu.udel.cis.vsl.civl.SvcompTest):SKIPPED
[junit] Testcase: sync01_true(edu.udel.cis.vsl.civl.SvcompTest):SKIPPED
[junit] TEST edu.udel.cis.vsl.civl.SvcompTest FAILED
[junit] Testsuite: edu.udel.cis.vsl.civl.VerifyThisTest
[junit] Tests run: 9, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 38.212 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.transform.CompareTest
[junit] Tests run: 10, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 26.324 sec
[junit]
[junit] ------------- Standard Output ---------------
[junit] CIVL v1.7.1+ of 2016-05-31 -- 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.76
[junit] memory (bytes) : 698351616
[junit] max process count : 3
[junit] states : 2664
[junit] states saved : 989
[junit] state matches : 0
[junit] transitions : 2647
[junit] trace steps : 988
[junit] valid calls : 7592
[junit] provers : cvc4, z3, cvc3
[junit] prover calls : 64
[junit]
[junit] === Result ===
[junit] The standard properties hold for all executions.
[junit] ------------- ---------------- ---------------
[junit] Testsuite: edu.udel.cis.vsl.civl.transform.CudaTest
[junit] Tests run: 2, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 6.619 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.transform.GenTransformerTest
[junit] Tests run: 3, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 2.056 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.transform.IOTransformerTest
[junit] Tests run: 3, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.657 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: 28.95 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.transform.MPICollectivePart2Test
[junit] Tests run: 20, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 32.124 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.transform.MPITranslationTest
[junit] Tests run: 19, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 39.701 sec
[junit]
[junit] ------------- Standard Output ---------------
[junit] CIVL v1.7.1+ of 2016-05-31 -- 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) : 1.0
[junit] memory (bytes) : 899678208
[junit] max process count : 3
[junit] states : 418
[junit] states saved : 115
[junit] state matches : 0
[junit] transitions : 412
[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: 5.791 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.transform.OmpHelpersTest
[junit] Tests run: 9, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 2.169 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.transform.OpenMP2CIVLTransformerTest
[junit] Tests run: 7, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 7.728 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.transform.PthreadTest
[junit] Tests run: 17, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 7.052 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.transform.PthreadThreaderTest
[junit] Tests run: 8, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 1.967 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.transform.SideEffectsTest
[junit] Tests run: 4, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.073 sec
[junit]
[junitreport] Processing /usa/svn/work/civl/1.7.2/r3714/junit/data/TESTS-TestSuites.xml to /tmp/null1050127012
[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: 475ms
[junitreport] Deleting: /tmp/null1050127012
test:
[jacoco:report] Loading execution data file /usa/svn/work/civl/1.7.2/r3714/jacoco.exec
[jacoco:report] Writing bundle 'Test Coverage Report for CIVL 1.7.2 r3714 Regression Suite' with 460 classes
javadoc:
[mkdir] Created dir: /usa/svn/work/civl/1.7.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/src/edu/udel/cis/vsl/civl/config/IF/CIVLConfiguration.java:696: warning: no @return
[javadoc] public int getProcBound() {
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.7.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/src/edu/udel/cis/vsl/civl/model/IF/CIVLFunction.java:183: 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.2/r3714/src/edu/udel/cis/vsl/civl/model/IF/CIVLFunction.java:184: 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.2/r3714/src/edu/udel/cis/vsl/civl/model/IF/CIVLFunction.java:184: 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.2/r3714/src/edu/udel/cis/vsl/civl/model/IF/CIVLFunction.java:185: 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.2/r3714/src/edu/udel/cis/vsl/civl/model/IF/CIVLFunction.java:186: error: bad use of '>'
[javadoc] * be l1 (s1 -> l4, s2 -> l3), l3(), l4()
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.7.2/r3714/src/edu/udel/cis/vsl/civl/model/IF/CIVLFunction.java:186: error: bad use of '>'
[javadoc] * be l1 (s1 -> l4, s2 -> l3), l3(), l4()
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.7.2/r3714/src/edu/udel/cis/vsl/civl/model/IF/CIVLFunction.java:243: warning: no description for @return
[javadoc] * @return
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.7.2/r3714/src/edu/udel/cis/vsl/civl/model/IF/CIVLFunction.java:292: warning: no description for @return
[javadoc] * @return
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.7.2/r3714/src/edu/udel/cis/vsl/civl/model/IF/CIVLFunction.java:302: warning: no description for @param
[javadoc] * @param validConsequences
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.7.2/r3714/src/edu/udel/cis/vsl/civl/model/IF/CIVLFunction.java:312: error: @param name not found
[javadoc] * @param validConsequences
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.7.2/r3714/src/edu/udel/cis/vsl/civl/model/IF/CIVLFunction.java:312: warning: no description for @param
[javadoc] * @param validConsequences
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.7.2/r3714/src/edu/udel/cis/vsl/civl/model/IF/CIVLFunction.java:314: warning: no @return
[javadoc] List<Pair<Expression, Integer>> getPossibleValidConsequences();
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.7.2/r3714/src/edu/udel/cis/vsl/civl/model/IF/CIVLFunction.java:319: warning: no description for @return
[javadoc] * @return
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.7.2/r3714/src/edu/udel/cis/vsl/civl/model/IF/CIVLFunction.java:326: warning: no description for @return
[javadoc] * @return
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.7.2/r3714/src/edu/udel/cis/vsl/civl/model/IF/CIVLFunction.java:333: warning: no description for @param
[javadoc] * @param contract
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.7.2/r3714/src/edu/udel/cis/vsl/civl/model/IF/CIVLFunction.java:344: warning: no description for @return
[javadoc] * @return
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.7.2/r3714/src/edu/udel/cis/vsl/civl/model/IF/CIVLFunction.java:351: warning: no description for @param
[javadoc] * @param value
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.7.2/r3714/src/edu/udel/cis/vsl/civl/model/IF/CIVLFunction.java:358: warning: no description for @param
[javadoc] * @param value
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.7.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/src/edu/udel/cis/vsl/civl/model/IF/Model.java:29: warning: no description for @return
[javadoc] * @return
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.7.2/r3714/src/edu/udel/cis/vsl/civl/model/IF/Model.java:171: warning: no description for @param
[javadoc] * @param value
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.7.2/r3714/src/edu/udel/cis/vsl/civl/model/IF/Model.java:211: warning: no description for @return
[javadoc] * @return
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.7.2/r3714/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.2/r3714/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.2/r3714/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:131: error: semicolon missing
[javadoc] * Returns a new address-of expression <code>(&e)</code> with given operand.
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.7.2/r3714/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:159: error: malformed HTML
[javadoc] * A binary expression. One of {+,-,*,\,<,<=,==,!=,&&,||,%}
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.7.2/r3714/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:159: error: malformed HTML
[javadoc] * A binary expression. One of {+,-,*,\,<,<=,==,!=,&&,||,%}
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.7.2/r3714/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:159: error: bad HTML entity
[javadoc] * A binary expression. One of {+,-,*,\,<,<=,==,!=,&&,||,%}
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.7.2/r3714/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:159: error: bad HTML entity
[javadoc] * A binary expression. One of {+,-,*,\,<,<=,==,!=,&&,||,%}
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.7.2/r3714/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:195: warning: no description for @param
[javadoc] * @param expression
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.7.2/r3714/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:318: warning: no description for @param
[javadoc] * @param source
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.7.2/r3714/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:319: warning: no description for @param
[javadoc] * @param function
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.7.2/r3714/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:326: warning: no description for @param
[javadoc] * @param source
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.7.2/r3714/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:341: warning: no description for @param
[javadoc] * @param source
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.7.2/r3714/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:342: warning: no description for @param
[javadoc] * @param variable
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.7.2/r3714/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:461: warning: no description for @param
[javadoc] * @param source
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.7.2/r3714/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:462: warning: no description for @param
[javadoc] * @param type
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.7.2/r3714/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:463: warning: no description for @param
[javadoc] * @param quant
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.7.2/r3714/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:464: warning: no description for @param
[javadoc] * @param lo
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.7.2/r3714/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:465: warning: no description for @param
[javadoc] * @param hi
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.7.2/r3714/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:466: warning: no description for @param
[javadoc] * @param function
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.7.2/r3714/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:467: warning: no description for @return
[javadoc] * @return
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.7.2/r3714/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:488: error: bad use of '>'
[javadoc] * <code>(high-low)/step >= 0 </code>.
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.7.2/r3714/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:507: 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.2/r3714/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:507: 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.2/r3714/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:637: warning: no description for @param
[javadoc] * @param callStatement
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.7.2/r3714/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:656: error: bad HTML entity
[javadoc] * <code>sysCall.isCall == true && sysCall.isSystemCall() == true</code>.
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.7.2/r3714/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:656: error: bad HTML entity
[javadoc] * <code>sysCall.isCall == true && sysCall.isSystemCall() == true</code>.
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.7.2/r3714/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:859: warning: no description for @param
[javadoc] * @param domSize
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.7.2/r3714/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:906: warning: no description for @return
[javadoc] * @return
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.7.2/r3714/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:930: warning: no description for @return
[javadoc] * @return
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.7.2/r3714/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:1009: error: reference not found
[javadoc] * {@link #noopStatement(CIVLSource, Location)}.
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.7.2/r3714/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:1251: error: @param name not found
[javadoc] * @param expressionNode
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.7.2/r3714/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:1258: warning: no @param for startSource
[javadoc] Pair<Fragment, Expression> refineConditionalExpression(Scope scope,
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.7.2/r3714/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:1258: warning: no @param for endSource
[javadoc] Pair<Fragment, Expression> refineConditionalExpression(Scope scope,
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.7.2/r3714/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:1317: warning: no @param for parameterScope
[javadoc] AbstractFunction abstractFunction(CIVLSource source, Identifier name,
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.7.2/r3714/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:1317: warning: no @param for factory
[javadoc] AbstractFunction abstractFunction(CIVLSource source, Identifier name,
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.7.2/r3714/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:1343: warning: no @param for parameterScope
[javadoc] CIVLFunction function(CIVLSource source, boolean isAtomic, Identifier name,
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.7.2/r3714/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:1378: warning: no @param for program
[javadoc] Model model(CIVLSource source, CIVLFunction system, Program program);
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.7.2/r3714/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:1416: warning: no @param for parameterScope
[javadoc] SystemFunction systemFunction(CIVLSource source, Identifier name,
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.7.2/r3714/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:1543: error: @param name not found
[javadoc] * @param scopeValue
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.7.2/r3714/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:1548: warning: no @param for stateValue
[javadoc] int getStateRef(CIVLSource source, SymbolicExpression stateValue);
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.7.2/r3714/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:1589: error: malformed HTML
[javadoc] * <code>pid < 0</code>, returns undefinedProcessValue.
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.7.2/r3714/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:1600: warning: no description for @param
[javadoc] * @param type
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.7.2/r3714/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:1601: warning: no description for @return
[javadoc] * @return
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.7.2/r3714/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:1636: error: @param name not found
[javadoc] * @param scope
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.7.2/r3714/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:1668: warning: no description for @return
[javadoc] * @return
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.7.2/r3714/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:1694: warning: no description for @param
[javadoc] * @param source
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.7.2/r3714/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:1695: warning: no description for @param
[javadoc] * @param src
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.7.2/r3714/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:1696: warning: no description for @param
[javadoc] * @param dom
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.7.2/r3714/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:1697: warning: no description for @param
[javadoc] * @param variables
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.7.2/r3714/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:102: error: reference not found
[javadoc] * {@link #function(CIVLSource, Identifier, List, CIVLType, Scope, Location)}. A
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.7.2/r3714/src/edu/udel/cis/vsl/civl/model/IF/Scope.java:81: error: @param name not found
[javadoc] * @param A
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.7.2/r3714/src/edu/udel/cis/vsl/civl/model/IF/Scope.java:196: error: @param name not found
[javadoc] * @param des
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.7.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/src/edu/udel/cis/vsl/civl/model/IF/expression/Expression.java:140: error: semicolon missing
[javadoc] * an address-of expression. e.g., <code>(&a + &b)</code> returns
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.7.2/r3714/src/edu/udel/cis/vsl/civl/model/IF/expression/Expression.java:140: error: semicolon missing
[javadoc] * an address-of expression. e.g., <code>(&a + &b)</code> returns
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.7.2/r3714/src/edu/udel/cis/vsl/civl/model/IF/expression/Expression.java:152: error: semicolon missing
[javadoc] * e.g., <code>(&a + &b)</code> returns <code>{a, b}</code>.
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.7.2/r3714/src/edu/udel/cis/vsl/civl/model/IF/expression/Expression.java:152: error: semicolon missing
[javadoc] * e.g., <code>(&a + &b)</code> returns <code>{a, b}</code>.
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.7.2/r3714/src/edu/udel/cis/vsl/civl/model/IF/expression/Expression.java:186: error: malformed HTML
[javadoc] * e.g.: s<$here would return true.
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.7.2/r3714/src/edu/udel/cis/vsl/civl/model/IF/expression/Expression.java:196: 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.2/r3714/src/edu/udel/cis/vsl/civl/model/IF/expression/AddressOfExpression.java:5: 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.2/r3714/src/edu/udel/cis/vsl/civl/model/IF/expression/AddressOfExpression.java:5: 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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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.2/r3714/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] /usa/svn/work/civl/1.7.2/r3714/src/edu/udel/cis/vsl/civl/model/IF/expression/BinaryExpression.java:24: error: malformed HTML
[javadoc] * <code></code> (implication);</li> <li>LESS_THAN: <code><</code> (less
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.7.2/r3714/src/edu/udel/cis/vsl/civl/model/IF/expression/BinaryExpression.java:25: error: tag not allowed here: <li>
[javadoc] * than);</li> <li>LESS_THAN_EQUAL: <code><=</code> (less than or equal to);
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.7.2/r3714/src/edu/udel/cis/vsl/civl/model/IF/expression/BinaryExpression.java:25: error: malformed HTML
[javadoc] * than);</li> <li>LESS_THAN_EQUAL: <code><=</code> (less than or equal to);
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.7.2/r3714/src/edu/udel/cis/vsl/civl/model/IF/expression/BinaryExpression.java:26: error: tag not allowed here: <li>
[javadoc] * </li> <li>MINUS: <code>-</code> (subtraction);</li> <li>MODULO:
[javadoc] ^
[javadoc] Building index for all the packages and classes...
[javadoc] Building index for all classes...
[javadoc] Generating /usa/svn/work/civl/1.7.2/r3714/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.2/r3714/bin
bench-scale-compile:
[javac] Compiling 5 source files to /usa/svn/work/civl/1.7.2/r3714/bin
all:
BUILD SUCCESSFUL
Total time: 5 minutes 16 seconds
Stderr:
[junit] Tests FAILED