Path: . Working Copy Root Path: /usa/svn/work/civl/1.19/r5139 URL: svn://vsl.cis.udel.edu/civl/tags/1.19 Relative URL: ^/tags/1.19 Repository Root: svn://vsl.cis.udel.edu/civl Repository UUID: fb995dde-84ed-4084-dfe6-e5aef3e2452c Revision: 5139 Node Kind: directory Schedule: normal Last Changed Author: ziqing Last Changed Rev: 5139 Last Changed Date: 2019-02-08 12:18:37 -0500 (Fri, 08 Feb 2019)
Stdout:
Buildfile: /usa/svn/work/civl/1.19/r5139/build.xml
checkCommandParserChanges:
CommandParser:
[move] Moving 1 file to /usa/svn/work/civl/1.19/r5139/src/edu/udel/cis/vsl/civl/run/common
[move] Moving 1 file to /usa/svn/work/civl/1.19/r5139/src/edu/udel/cis/vsl/civl/run/common
[move] Moving 1 file to /usa/svn/work/civl/1.19/r5139/src/edu/udel/cis/vsl/civl/run/common
[move] Moving 1 file to /usa/svn/work/civl/1.19/r5139/src/edu/udel/cis/vsl/civl/run/common
compile:
[mkdir] Created dir: /usa/svn/work/civl/1.19/r5139/bin
[javac] Compiling 540 source files to /usa/svn/work/civl/1.19/r5139/bin
[javac] Creating empty /usa/svn/work/civl/1.19/r5139/bin/edu/udel/cis/vsl/civl/model/IF/expression/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.19/r5139/bin/edu/udel/cis/vsl/civl/state/IF/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.19/r5139/bin/edu/udel/cis/vsl/civl/gui/IF/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.19/r5139/bin/edu/udel/cis/vsl/civl/gui/common/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.19/r5139/bin/edu/udel/cis/vsl/civl/semantics/IF/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.19/r5139/bin/edu/udel/cis/vsl/civl/kripke/IF/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.19/r5139/bin/edu/udel/cis/vsl/civl/util/IF/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.19/r5139/bin/edu/udel/cis/vsl/civl/library/domain/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.19/r5139/bin/edu/udel/cis/vsl/civl/model/IF/type/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.19/r5139/bin/edu/udel/cis/vsl/civl/library/comm/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.19/r5139/bin/edu/udel/cis/vsl/civl/library/pointer/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.19/r5139/bin/edu/udel/cis/vsl/civl/model/IF/location/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.19/r5139/bin/edu/udel/cis/vsl/civl/library/time/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.19/r5139/bin/edu/udel/cis/vsl/civl/library/pthread/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.19/r5139/bin/edu/udel/cis/vsl/civl/config/IF/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.19/r5139/bin/edu/udel/cis/vsl/civl/dynamic/IF/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.19/r5139/bin/edu/udel/cis/vsl/civl/library/civlc/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.19/r5139/bin/edu/udel/cis/vsl/civl/log/IF/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.19/r5139/bin/edu/udel/cis/vsl/civl/library/common/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.19/r5139/bin/edu/udel/cis/vsl/civl/model/IF/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.19/r5139/bin/edu/udel/cis/vsl/civl/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.19/r5139/bin/edu/udel/cis/vsl/civl/model/IF/variable/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.19/r5139/bin/edu/udel/cis/vsl/civl/library/seq/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.19/r5139/bin/edu/udel/cis/vsl/civl/library/string/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.19/r5139/bin/edu/udel/cis/vsl/civl/analysis/IF/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.19/r5139/bin/edu/udel/cis/vsl/civl/library/scope/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.19/r5139/bin/edu/udel/cis/vsl/civl/model/IF/statement/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.19/r5139/bin/edu/udel/cis/vsl/civl/predicate/IF/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.19/r5139/bin/edu/udel/cis/vsl/civl/library/bundle/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.19/r5139/bin/edu/udel/cis/vsl/civl/slice/common/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.19/r5139/bin/edu/udel/cis/vsl/civl/slice/IF/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.19/r5139/bin/edu/udel/cis/vsl/civl/run/IF/package-info.class
[javac] Creating empty /usa/svn/work/civl/1.19/r5139/bin/edu/udel/cis/vsl/civl/transform/IF/package-info.class
[copy] Copying 32 files to /usa/svn/work/civl/1.19/r5139/bin/include
jar:
[jar] Building jar: /usa/svn/work/civl/1.19/r5139/civl.jar
test-init:
[mkdir] Created dir: /usa/svn/work/civl/1.19/r5139/junit
[mkdir] Created dir: /usa/svn/work/civl/1.19/r5139/junit/data
[mkdir] Created dir: /usa/svn/work/civl/1.19/r5139/junit/reports
[mkdir] Created dir: /usa/svn/work/civl/1.19/r5139/bin-test/regress
test-compile:
[javac] Compiling 41 source files to /usa/svn/work/civl/1.19/r5139/bin-test/regress
test-run:
[jacoco:coverage] Enhancing junit with coverage
[junit] Testsuite: edu.udel.cis.vsl.civl.AcfInterfaceTest
[junit] Tests run: 2, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 6.064 sec
[junit]
[junit] ------------- Standard Output ---------------
[junit] CIVL v1.19 of 2019-02-08 -- http://vsl.cis.udel.edu/civl
[junit] CIVL v1.19 of 2019-02-08 -- http://vsl.cis.udel.edu/civl
[junit] ------------- ---------------- ---------------
[junit] Testsuite: edu.udel.cis.vsl.civl.AnalysisTest
[junit] Tests run: 3, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 2.486 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.ArithmeticTest
[junit] Tests run: 27, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 13.707 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.ArrayLambdaTest
[junit] Tests run: 4, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 1.425 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.BackendTest
[junit] Tests run: 19, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 2.848 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.CompareTest
[junit] Tests run: 5, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 103.277 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.ConcurrencyTest
[junit] Tests run: 34, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 17.099 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.LanguageFeaturesTest
[junit] Tests run: 148, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 20.861 sec
[junit]
[junit] ------------- Standard Error -----------------
[junit] Warning: ignoring a division by zero
[junit] ------------- ---------------- ---------------
[junit] Testsuite: edu.udel.cis.vsl.civl.LibraryTest
[junit] Tests run: 72, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 12.905 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.ModelBuilderTest
[junit] Tests run: 17, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 1.197 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.PORTest
[junit] Tests run: 15, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.976 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.QuietOptionTest
[junit] Tests run: 5, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 3.463 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.ReasoningTest
[junit] Tests run: 9, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 2.231 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.114 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.RobustnessTest
[junit] Tests run: 1, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.058 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.ShowStatesTest
[junit] Tests run: 2, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.115 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.SimpleMPITest
[junit] Tests run: 23, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 55.615 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.SpecialStatementsTest
[junit] Tests run: 7, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.368 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.SvcompTest
[junit] Tests run: 4, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 1.397 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.TicketsFixTest
[junit] Tests run: 4, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 62.756 sec
[junit]
[junit] ------------- Standard Output ---------------
[junit] CIVL v1.19 of 2019-02-08 -- http://vsl.cis.udel.edu/civl
[junit]
[junit] Violation 0 encountered at depth 4:
[junit] CIVL execution violation in p0 (kind: ASSERTION_VIOLATION, certainty: PROVEABLE)
[junit] at ticket_919_char_to_int_cast1.cvl:11.2-20
[junit] $assert(x.c == y.c);
[junit] ^^^^^^^^^^^^^^^^^^^
[junit]
[junit] Assertion: ((int) (x).0==(int) (y).0)
[junit] -> (int)Y2.0==(int)Y3.0
[junit] -> (int)(Y2.0)==(int)(Y3.0)
[junit] -> 0==((int)(Y2.0) - 1*(int)(Y3.0))
[junit]
[junit] Context:
[junit] true
[junit] Call stacks:
[junit] process 0:
[junit] main at ticket_919_char_to_int_cast1.cvl:11.2-8 "$assert"
[junit]
[junit] Logging new entry 0, writing trace to CIVLREP/ticket_919_char_to_int_cast1_0.trace
[junit] Terminating search after finding 1 violation.
[junit]
[junit] === Source files ===
[junit] ticket_919_char_to_int_cast1.cvl (examples/tickets/ticket_919_char_to_int_cast1.cvl)
[junit]
[junit]
[junit] === Command ===
[junit] civl verify examples/tickets/ticket_919_char_to_int_cast1.cvl
[junit]
[junit] === Stats ===
[junit] time (s) : 0.07
[junit] memory (bytes) : 851443712
[junit] max process count : 1
[junit] states : 5
[junit] states saved : 4
[junit] state matches : 0
[junit] transitions : 5
[junit] trace steps : 3
[junit] valid calls : 2
[junit] provers : cvc4, z3
[junit] prover calls : 1
[junit]
[junit] === Result ===
[junit] The program MAY NOT be correct. See CIVLREP/ticket_919_char_to_int_cast1_log.txt
[junit] CIVL v1.19 of 2019-02-08 -- http://vsl.cis.udel.edu/civl
[junit] a[0] = ' ' a[1] = ' ' a[2] = ' ' a[3] = Y0[3] a[4] = Y0[4]
[junit] === Source files ===
[junit] ticket_919_char_to_int_cast2.cvl (examples/tickets/ticket_919_char_to_int_cast2.cvl)
[junit]
[junit]
[junit] === Command ===
[junit] civl verify examples/tickets/ticket_919_char_to_int_cast2.cvl
[junit]
[junit] === Stats ===
[junit] time (s) : 0.19
[junit] memory (bytes) : 894435328
[junit] max process count : 1
[junit] states : 22
[junit] states saved : 16
[junit] state matches : 0
[junit] transitions : 21
[junit] trace steps : 13
[junit] valid calls : 30
[junit] provers : cvc4, z3
[junit] prover calls : 0
[junit]
[junit] === Result ===
[junit] The standard properties hold for all executions.
[junit] ------------- ---------------- ---------------
[junit] Testsuite: edu.udel.cis.vsl.civl.VerifyThisTest
[junit] Tests run: 15, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 42.17 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.transform.ACSLTransformTest
[junit] Tests run: 8, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.656 sec
[junit]
[junit] ------------- Standard Error -----------------
[junit] UnsatisfiablePathConditionException thrown during interpretation of logic function:eq
[junit] ------------- ---------------- ---------------
[junit] Testsuite: edu.udel.cis.vsl.civl.transform.CompareTest
[junit] Tests run: 15, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 114.047 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.transform.ContractTest
[junit] Tests run: 6, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 22.845 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.transform.CudaTest
[junit] Tests run: 3, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 8.618 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.transform.GenTransformerTest
[junit] Tests run: 3, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 3.076 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.transform.IOTransformerTest
[junit] Tests run: 4, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 1.833 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.transform.LoopInvariantsNoAssignsTest
[junit] Tests run: 1, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.649 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.transform.MPICollectivePart1Test
[junit] Tests run: 20, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 39.058 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.transform.MPICollectivePart2Test
[junit] Tests run: 25, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 53.857 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.transform.MPITranslationTest
[junit] Tests run: 23, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 53.113 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.transform.MPI_OpenMPTest
[junit] Tests run: 3, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 7.845 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.transform.OmpHelpersTest
[junit] Tests run: 9, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 3.042 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.transform.OpenMP2CIVLTransformerTest
[junit] Tests run: 17, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 22.744 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.transform.PthreadTest
[junit] Tests run: 15, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 7.914 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.transform.PthreadThreaderTest
[junit] Tests run: 8, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 3.602 sec
[junit]
[junit] Testsuite: edu.udel.cis.vsl.civl.transform.SideEffectsTest
[junit] Tests run: 10, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.494 sec
[junit]
[junitreport] Processing /usa/svn/work/civl/1.19/r5139/junit/data/TESTS-TestSuites.xml to /tmp/null304747354
[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: 549ms
[junitreport] Deleting: /tmp/null304747354
test:
[jacoco:report] Loading execution data file /usa/svn/work/civl/1.19/r5139/jacoco.exec
[jacoco:report] Writing bundle 'Test Coverage Report for CIVL 1.19 r5139 Regression Suite' with 546 classes
javadoc:
[mkdir] Created dir: /usa/svn/work/civl/1.19/r5139/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_181
[javadoc] Building tree for all the packages and classes...
[javadoc] /usa/svn/work/civl/1.19/r5139/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.19/r5139/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.19/r5139/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.19/r5139/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.19/r5139/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.19/r5139/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.19/r5139/src/edu/udel/cis/vsl/civl/config/IF/CIVLConfiguration.java:778: warning: no @return
[javadoc] public int getProcBound() {
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.19/r5139/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.19/r5139/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.19/r5139/src/edu/udel/cis/vsl/civl/dynamic/IF/DynamicWriteSet.java:34: error: reference not found
[javadoc] * {@link ImmutableStateFactory#deallocate(edu.udel.cis.vsl.civl.state.IF.State, SymbolicExpression, int, int, int)}
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.19/r5139/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.19/r5139/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.19/r5139/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.19/r5139/src/edu/udel/cis/vsl/civl/dynamic/IF/DynamicWriteSet.java:49: warning - Tag @link: can't find deallocate(edu.udel.cis.vsl.civl.state.IF.State, SymbolicExpression, int, int, int) in edu.udel.cis.vsl.civl.state.common.immutable.ImmutableStateFactory
[javadoc] /usa/svn/work/civl/1.19/r5139/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:328: error: reference not found
[javadoc] * {@link #isPointerToHeap(heapPointer)} must returns true.
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.19/r5139/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:381: error: semicolon missing
[javadoc] * pointer. For example, given a pointer &a[5] and a reference [0], the
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.19/r5139/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:382: 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.19/r5139/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:629: error: tag not allowed here: <li>
[javadoc] * <li>length(array_extents) > 0</li>
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.19/r5139/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:629: error: bad use of '>'
[javadoc] * <li>length(array_extents) > 0</li>
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.19/r5139/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:630: error: unexpected end tag: </p>
[javadoc] * </p>
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.19/r5139/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:639: 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.19/r5139/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:641: error: exception not thrown: edu.udel.cis.vsl.civl.state.IF.UnsatisfiablePathConditionException
[javadoc] * @throws UnsatisfiablePathConditionException
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.19/r5139/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:641: warning: no description for @throws
[javadoc] * @throws UnsatisfiablePathConditionException
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.19/r5139/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:718: warning: no description for @param
[javadoc] * @param domain
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.19/r5139/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:726: warning: no description for @param
[javadoc] * @param range
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.19/r5139/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:736: warning: no description for @param
[javadoc] * @param domain
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.19/r5139/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:737: warning: no description for @param
[javadoc] * @param index
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.19/r5139/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:748: warning: no description for @param
[javadoc] * @param range
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.19/r5139/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:758: warning: no description for @param
[javadoc] * @param range
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.19/r5139/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:769: warning: no description for @param
[javadoc] * @param range
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.19/r5139/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:777: warning: no description for @param
[javadoc] * @param domain
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.19/r5139/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:784: 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.19/r5139/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:784: 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.19/r5139/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:784: 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.19/r5139/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:784: 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.19/r5139/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:784: 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.19/r5139/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:784: 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.19/r5139/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:784: 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.19/r5139/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:785: 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.19/r5139/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:785: 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.19/r5139/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:785: 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.19/r5139/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:787: warning: no description for @param
[javadoc] * @param cnfClause
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.19/r5139/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:795: warning: no description for @param
[javadoc] * @param function
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.19/r5139/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:796: error: @param name not found
[javadoc] * @param arguments
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.19/r5139/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:796: warning: no description for @param
[javadoc] * @param arguments
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.19/r5139/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:797: warning: no description for @return
[javadoc] * @return
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.19/r5139/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:799: warning: no @param for library
[javadoc] SymbolicExpression getAbstractGuardOfFunctionCall(String library,
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.19/r5139/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:799: warning: no @param for argumentValues
[javadoc] SymbolicExpression getAbstractGuardOfFunctionCall(String library,
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.19/r5139/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:809: warning: no description for @param
[javadoc] * @param originalFunction
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.19/r5139/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:810: warning: no description for @param
[javadoc] * @param argument
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.19/r5139/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:811: warning: no description for @return
[javadoc] * @return
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.19/r5139/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:823: warning: no description for @param
[javadoc] * @param range
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.19/r5139/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:824: warning: no description for @return
[javadoc] * @return
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.19/r5139/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:826: warning: no @param for reasoner
[javadoc] BitSet range2BitSet(SymbolicExpression range, Reasoner reasoner);
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.19/r5139/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:838: warning: no description for @param
[javadoc] * @param pointer
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.19/r5139/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:839: warning: no description for @return
[javadoc] * @return
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.19/r5139/src/edu/udel/cis/vsl/civl/dynamic/IF/SymbolicUtility.java:331: warning - Tag @link: can't find isPointerToHeap(heapPointer) in edu.udel.cis.vsl.civl.dynamic.IF.SymbolicUtility
[javadoc] /usa/svn/work/civl/1.19/r5139/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.19/r5139/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.19/r5139/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.19/r5139/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.19/r5139/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.19/r5139/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.19/r5139/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.19/r5139/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.19/r5139/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.19/r5139/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.19/r5139/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.19/r5139/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.19/r5139/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.19/r5139/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.19/r5139/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.19/r5139/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.19/r5139/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.19/r5139/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.19/r5139/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.19/r5139/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.19/r5139/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.19/r5139/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.19/r5139/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.19/r5139/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.19/r5139/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.19/r5139/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.19/r5139/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.19/r5139/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.19/r5139/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.19/r5139/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.19/r5139/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.19/r5139/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.19/r5139/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.19/r5139/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.19/r5139/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.19/r5139/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.19/r5139/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.19/r5139/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.19/r5139/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.19/r5139/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.19/r5139/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.19/r5139/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.19/r5139/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.19/r5139/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.19/r5139/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.19/r5139/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.19/r5139/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.19/r5139/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.19/r5139/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.19/r5139/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.19/r5139/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.19/r5139/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.19/r5139/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.19/r5139/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.19/r5139/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.19/r5139/src/edu/udel/cis/vsl/civl/model/IF/CIVLSource.java:34: warning: no @return
[javadoc] String getLocation();
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.19/r5139/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.19/r5139/src/edu/udel/cis/vsl/civl/model/IF/CIVLTypeFactory.java:111: warning: no description for @param
[javadoc] * @param rangeType
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.19/r5139/src/edu/udel/cis/vsl/civl/model/IF/CIVLTypeFactory.java:169: error: bad use of '>'
[javadoc] * Create a new location. ======= Get the integer primitive type. >>>>>>>
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.19/r5139/src/edu/udel/cis/vsl/civl/model/IF/CIVLTypeFactory.java:169: error: bad use of '>'
[javadoc] * Create a new location. ======= Get the integer primitive type. >>>>>>>
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.19/r5139/src/edu/udel/cis/vsl/civl/model/IF/CIVLTypeFactory.java:169: error: bad use of '>'
[javadoc] * Create a new location. ======= Get the integer primitive type. >>>>>>>
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.19/r5139/src/edu/udel/cis/vsl/civl/model/IF/CIVLTypeFactory.java:169: error: bad use of '>'
[javadoc] * Create a new location. ======= Get the integer primitive type. >>>>>>>
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.19/r5139/src/edu/udel/cis/vsl/civl/model/IF/CIVLTypeFactory.java:169: error: bad use of '>'
[javadoc] * Create a new location. ======= Get the integer primitive type. >>>>>>>
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.19/r5139/src/edu/udel/cis/vsl/civl/model/IF/CIVLTypeFactory.java:169: error: bad use of '>'
[javadoc] * Create a new location. ======= Get the integer primitive type. >>>>>>>
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.19/r5139/src/edu/udel/cis/vsl/civl/model/IF/CIVLTypeFactory.java:169: error: bad use of '>'
[javadoc] * Create a new location. ======= Get the integer primitive type. >>>>>>>
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.19/r5139/src/edu/udel/cis/vsl/civl/model/IF/CIVLTypeFactory.java:353: warning: no description for @param
[javadoc] * @param type
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.19/r5139/src/edu/udel/cis/vsl/civl/model/IF/CIVLTypeFactory.java:354: warning: no description for @param
[javadoc] * @param id
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.19/r5139/src/edu/udel/cis/vsl/civl/model/IF/CIVLTypeFactory.java:433: error: @param name not found
[javadoc] * @param universe
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.19/r5139/src/edu/udel/cis/vsl/civl/model/IF/CIVLTypeFactory.java:435: error: @param name not found
[javadoc] * @param the
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.19/r5139/src/edu/udel/cis/vsl/civl/model/IF/CIVLTypeFactory.java:439: warning: no @param for dynamicType
[javadoc] NumericExpression sizeofDynamicType(SymbolicType dynamicType);
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.19/r5139/src/edu/udel/cis/vsl/civl/model/IF/CIVLTypeFactory.java:475: error: @param name not found
[javadoc] * @param expr
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.19/r5139/src/edu/udel/cis/vsl/civl/model/IF/CIVLTypeFactory.java:481: warning: no @param for typeId
[javadoc] CIVLType getStaticTypeOfDynamicType(SymbolicExpression typeId);
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.19/r5139/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.19/r5139/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.19/r5139/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.19/r5139/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.19/r5139/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.19/r5139/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.19/r5139/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.19/r5139/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.19/r5139/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.19/r5139/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.19/r5139/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.19/r5139/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.19/r5139/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.19/r5139/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.19/r5139/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.19/r5139/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.19/r5139/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.19/r5139/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.19/r5139/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:444: error: @param name not found
[javadoc] * @param boundVariableList
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.19/r5139/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:451: warning: no @param for variable
[javadoc] LambdaExpression lambdaExpression(CIVLSource source,
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.19/r5139/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:457: warning: no description for @param
[javadoc] * @param source
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.19/r5139/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:458: warning: no description for @param
[javadoc] * @param type
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.19/r5139/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:459: warning: no description for @param
[javadoc] * @param quant
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.19/r5139/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:460: warning: no description for @param
[javadoc] * @param lo
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.19/r5139/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:461: warning: no description for @param
[javadoc] * @param hi
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.19/r5139/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:462: warning: no description for @param
[javadoc] * @param function
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.19/r5139/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:463: warning: no description for @return
[javadoc] * @return
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.19/r5139/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:484: error: bad use of '>'
[javadoc] * <code>(high-low)/step >= 0 </code>.
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.19/r5139/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:503: 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.19/r5139/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:503: 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.19/r5139/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:619: warning: no description for @param
[javadoc] * @param callStatement
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.19/r5139/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:638: error: bad HTML entity
[javadoc] * <code>sysCall.isCall == true && sysCall.isSystemCall() == true</code>.
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.19/r5139/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:638: error: bad HTML entity
[javadoc] * <code>sysCall.isCall == true && sysCall.isSystemCall() == true</code>.
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.19/r5139/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:714: warning: no description for @param
[javadoc] * @param source
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.19/r5139/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:715: warning: no description for @param
[javadoc] * @param function
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.19/r5139/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:716: warning: no description for @param
[javadoc] * @param degree
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.19/r5139/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:717: warning: no description for @param
[javadoc] * @param lowerBounds
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.19/r5139/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:718: warning: no description for @param
[javadoc] * @param upperBounds
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.19/r5139/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:719: warning: no description for @return
[javadoc] * @return
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.19/r5139/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:1013: error: reference not found
[javadoc] * {@link #noopStatement(CIVLSource, Location)}.
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.19/r5139/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:1446: error: @param name not found
[javadoc] * @param source
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.19/r5139/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:1448: error: @param name not found
[javadoc] * @param scopeValue
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.19/r5139/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:1475: error: @param name not found
[javadoc] * @param source
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.19/r5139/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:1529: error: @param name not found
[javadoc] * @param scope
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.19/r5139/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.19/r5139/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.19/r5139/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.19/r5139/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.19/r5139/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.19/r5139/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.19/r5139/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.19/r5139/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.19/r5139/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.19/r5139/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.19/r5139/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.19/r5139/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.19/r5139/src/edu/udel/cis/vsl/civl/model/IF/expression/Expression.java:147: error: semicolon missing
[javadoc] * an address-of expression. e.g., <code>(&a + &b)</code> returns
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.19/r5139/src/edu/udel/cis/vsl/civl/model/IF/expression/Expression.java:147: error: semicolon missing
[javadoc] * an address-of expression. e.g., <code>(&a + &b)</code> returns
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.19/r5139/src/edu/udel/cis/vsl/civl/model/IF/expression/Expression.java:159: error: semicolon missing
[javadoc] * e.g., <code>(&a + &b)</code> returns <code>{a, b}</code>.
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.19/r5139/src/edu/udel/cis/vsl/civl/model/IF/expression/Expression.java:159: error: semicolon missing
[javadoc] * e.g., <code>(&a + &b)</code> returns <code>{a, b}</code>.
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.19/r5139/src/edu/udel/cis/vsl/civl/model/IF/expression/Expression.java:193: error: malformed HTML
[javadoc] * e.g.: s<$here would return true.
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.19/r5139/src/edu/udel/cis/vsl/civl/model/IF/expression/Expression.java:203: error: semicolon missing
[javadoc] * any error checking. e.g., &anon[0] which is used to translate array
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.19/r5139/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.19/r5139/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.19/r5139/src/edu/udel/cis/vsl/civl/model/IF/expression/BinaryExpression.java:17: error: unknown tag: ui
[javadoc] * <ui>
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.19/r5139/src/edu/udel/cis/vsl/civl/model/IF/expression/BinaryExpression.java:18: error: tag not allowed here: <li>
[javadoc] * <li>AND: <code>&&</code> (logical and);</li>
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.19/r5139/src/edu/udel/cis/vsl/civl/model/IF/expression/BinaryExpression.java:18: error: bad HTML entity
[javadoc] * <li>AND: <code>&&</code> (logical and);</li>
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.19/r5139/src/edu/udel/cis/vsl/civl/model/IF/expression/BinaryExpression.java:18: error: bad HTML entity
[javadoc] * <li>AND: <code>&&</code> (logical and);</li>
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.19/r5139/src/edu/udel/cis/vsl/civl/model/IF/expression/BinaryExpression.java:19: error: tag not allowed here: <li>
[javadoc] * <li>LEFT_SHIFT: <code><</code> (bitwise left shift);</li>
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.19/r5139/src/edu/udel/cis/vsl/civl/model/IF/expression/BinaryExpression.java:19: error: malformed HTML
[javadoc] * <li>LEFT_SHIFT: <code><</code> (bitwise left shift);</li>
[javadoc] ^
[javadoc] /usa/svn/work/civl/1.19/r5139/src/edu/udel/cis/vsl/civl/model/IF/expression/BinaryExpression.java:20: error: tag not allowed here: <li>
[javadoc] * <li>RIGHT_SHIFT: <code>>></code> (bitwise right shift);</li>
[javadoc] ^
[javadoc] Building index for all the packages and classes...
[javadoc] Building index for all classes...
[javadoc] Generating /usa/svn/work/civl/1.19/r5139/doc/javadoc/help-doc.html...
[javadoc] 100 errors
[javadoc] 100 warnings
bench-compile:
[javac] Compiling 6 source files to /usa/svn/work/civl/1.19/r5139/bin
bench-scale-compile:
[javac] Compiling 5 source files to /usa/svn/work/civl/1.19/r5139/bin
all:
BUILD SUCCESSFUL
Total time: 11 minutes 54 seconds
Stderr: