Path: . Working Copy Root Path: /Users/tester/work/civl/0.2/r123 URL: svn://vsl.cis.udel.edu/civl/tags/0.2 Repository Root: svn://vsl.cis.udel.edu/civl Repository UUID: fb995dde-84ed-4084-dfe6-e5aef3e2452c Revision: 123 Node Kind: directory Schedule: normal Last Changed Author: siegel Last Changed Rev: 123 Last Changed Date: 2013-06-23 10:56:37 -0400 (Sun, 23 Jun 2013)
Stdout:
Buildfile: /Users/tester/work/civl/0.2/r123/build.xml
compile:
[mkdir] Created dir: /Users/tester/work/civl/0.2/r123/bin
[javac] Compiling 115 source files to /Users/tester/work/civl/0.2/r123/bin
jar:
[jar] Building jar: /Users/tester/work/civl/0.2/r123/civl.jar
test-init:
[mkdir] Created dir: /Users/tester/work/civl/0.2/r123/junit
[mkdir] Created dir: /Users/tester/work/civl/0.2/r123/junit/data
[mkdir] Created dir: /Users/tester/work/civl/0.2/r123/junit/reports
[mkdir] Created dir: /Users/tester/work/civl/0.2/r123/bin-test
test-compile:
[javac] Compiling 1 source file to /Users/tester/work/civl/0.2/r123/bin-test
test-run:
[jacoco:coverage] Enhancing junit with coverage
[junit] Testsuite: edu.udel.cis.vsl.civl.ExamplesTest
[junit] Tests run: 20, Failures: 0, Errors: 0, Time elapsed: 19.397 sec
[junit]
[junit] ------------- Standard Output ---------------
[junit] =================== Stats ===================
[junit]
[junit] maxProcs : 1
[junit] statesSeen : 6
[junit] statesMatched : 0
[junit] transitionsExecuted : 5
[junit] proverValidCalls : 16
[junit] CVC3ValidCalls : 2
[junit] memory (bytes) : 127729664
[junit] elapsedTime (s) : 0.66
[junit] The specified properties hold for all executions.
[junit] =================== Stats ===================
[junit]
[junit] maxProcs : 1
[junit] statesSeen : 53
[junit] statesMatched : 0
[junit] transitionsExecuted : 52
[junit] proverValidCalls : 176
[junit] CVC3ValidCalls : 2
[junit] memory (bytes) : 127729664
[junit] elapsedTime (s) : 0.124
[junit] The specified properties hold for all executions.
[junit] A deadlock is possible:
[junit] *****************************************************************
[junit] Deadlock possible at State 250(nprocs=3, nscopes=10)!
[junit] *****************************************************************
[junit] Process 0: at location 37. Target process has not terminated:
[junit] p
[junit] Process 1: at location 42. Cannot prove enabling statement valid:
[junit] false
[junit] Process 2: at location 49. Cannot prove enabling statement valid:
[junit] false
[junit]
[junit] State 250
[junit] | Path condition
[junit] | | true
[junit] | Dynamic scopes
[junit] | | scope 0 (parent=1, static=27)
[junit] | | | reachers: 0
[junit] | | | p = PID_1
[junit] | | | q = PID_2
[junit] | | scope 1 (parent=-1, static=26)
[junit] | | | reachers: 0,1,2
[junit] | | | x = 1
[junit] | | | y = 1
[junit] | | scope 2 (parent=3, static=31)
[junit] | | | reachers: 1
[junit] | | scope 3 (parent=4, static=30)
[junit] | | | reachers: 1
[junit] | | | i = 9
[junit] | | scope 4 (parent=5, static=29)
[junit] | | | reachers: 1
[junit] | | scope 5 (parent=1, static=28)
[junit] | | | reachers: 1
[junit] | | | n = 10
[junit] | | scope 6 (parent=7, static=35)
[junit] | | | reachers: 2
[junit] | | scope 7 (parent=8, static=34)
[junit] | | | reachers: 2
[junit] | | | i = 0
[junit] | | scope 8 (parent=9, static=33)
[junit] | | | reachers: 2
[junit] | | scope 9 (parent=1, static=32)
[junit] | | | reachers: 2
[junit] | | | m = 10
[junit] | Process states
[junit] | | process 0 call stack
[junit] | | | Frame[function=_CIVL_system, location=37, scope=0]
[junit] | | process 1 call stack
[junit] | | | Frame[function=f, location=42, scope=2]
[junit] | | process 2 call stack
[junit] | | | Frame[function=g, location=49, scope=6]
[junit] =================== Stats ===================
[junit]
[junit] maxProcs : 3
[junit] statesSeen : 251
[junit] statesMatched : 42
[junit] transitionsExecuted : 292
[junit] proverValidCalls : 1590
[junit] CVC3ValidCalls : 2
[junit] memory (bytes) : 127729664
[junit] elapsedTime (s) : 0.182
[junit] The program MAY NOT be correct.
[junit] =================== Stats ===================
[junit]
[junit] maxProcs : 1
[junit] statesSeen : 1655
[junit] statesMatched : 0
[junit] transitionsExecuted : 1654
[junit] proverValidCalls : 7297
[junit] CVC3ValidCalls : 2
[junit] memory (bytes) : 131792896
[junit] elapsedTime (s) : 6.104
[junit] The specified properties hold for all executions.
[junit] =================== Stats ===================
[junit]
[junit] maxProcs : 1
[junit] statesSeen : 3
[junit] statesMatched : 0
[junit] transitionsExecuted : 2
[junit] proverValidCalls : 7301
[junit] CVC3ValidCalls : 2
[junit] memory (bytes) : 131792896
[junit] elapsedTime (s) : 0.002
[junit] The specified properties hold for all executions.
[junit] =================== Stats ===================
[junit]
[junit] maxProcs : 1
[junit] statesSeen : 17
[junit] statesMatched : 0
[junit] transitionsExecuted : 16
[junit] proverValidCalls : 7338
[junit] CVC3ValidCalls : 2
[junit] memory (bytes) : 131792896
[junit] elapsedTime (s) : 0.033
[junit] The specified properties hold for all executions.
[junit] =================== Stats ===================
[junit]
[junit] maxProcs : 1
[junit] statesSeen : 15
[junit] statesMatched : 0
[junit] transitionsExecuted : 14
[junit] proverValidCalls : 7369
[junit] CVC3ValidCalls : 2
[junit] memory (bytes) : 131792896
[junit] elapsedTime (s) : 0.02
[junit] The specified properties hold for all executions.
[junit] =================== Stats ===================
[junit]
[junit] maxProcs : 3
[junit] statesSeen : 2018
[junit] statesMatched : 0
[junit] transitionsExecuted : 2017
[junit] proverValidCalls : 17441
[junit] CVC3ValidCalls : 2
[junit] memory (bytes) : 137232384
[junit] elapsedTime (s) : 0.407
[junit] The specified properties hold for all executions.
[junit] =================== Stats ===================
[junit]
[junit] maxProcs : 1
[junit] statesSeen : 46
[junit] statesMatched : 0
[junit] transitionsExecuted : 45
[junit] proverValidCalls : 17579
[junit] CVC3ValidCalls : 2
[junit] memory (bytes) : 137232384
[junit] elapsedTime (s) : 0.01
[junit] The specified properties hold for all executions.
[junit] =================== Stats ===================
[junit]
[junit] maxProcs : 1
[junit] statesSeen : 6
[junit] statesMatched : 0
[junit] transitionsExecuted : 5
[junit] proverValidCalls : 17593
[junit] CVC3ValidCalls : 2
[junit] memory (bytes) : 137232384
[junit] elapsedTime (s) : 0.015
[junit] The specified properties hold for all executions.
[junit] =================== Stats ===================
[junit]
[junit] maxProcs : 1
[junit] statesSeen : 3
[junit] statesMatched : 0
[junit] transitionsExecuted : 2
[junit] proverValidCalls : 17597
[junit] CVC3ValidCalls : 2
[junit] memory (bytes) : 137232384
[junit] elapsedTime (s) : 0.002
[junit] The specified properties hold for all executions.
[junit] =================== Stats ===================
[junit]
[junit] maxProcs : 1
[junit] statesSeen : 5
[junit] statesMatched : 0
[junit] transitionsExecuted : 4
[junit] proverValidCalls : 17606
[junit] CVC3ValidCalls : 2
[junit] memory (bytes) : 137232384
[junit] elapsedTime (s) : 0.017
[junit] The specified properties hold for all executions.
[junit] =================== Stats ===================
[junit]
[junit] maxProcs : 2
[junit] statesSeen : 6
[junit] statesMatched : 0
[junit] transitionsExecuted : 5
[junit] proverValidCalls : 17618
[junit] CVC3ValidCalls : 2
[junit] memory (bytes) : 137232384
[junit] elapsedTime (s) : 0.014
[junit] The specified properties hold for all executions.
[junit] =================== Stats ===================
[junit]
[junit] maxProcs : 4
[junit] statesSeen : 329
[junit] statesMatched : 115
[junit] transitionsExecuted : 443
[junit] proverValidCalls : 19571
[junit] CVC3ValidCalls : 2
[junit] memory (bytes) : 137232384
[junit] elapsedTime (s) : 0.091
[junit] The specified properties hold for all executions.
[junit] =================== Stats ===================
[junit]
[junit] maxProcs : 1
[junit] statesSeen : 6
[junit] statesMatched : 0
[junit] transitionsExecuted : 5
[junit] proverValidCalls : 19583
[junit] CVC3ValidCalls : 2
[junit] memory (bytes) : 130088960
[junit] elapsedTime (s) : 0.02
[junit] The specified properties hold for all executions.
[junit] =================== Stats ===================
[junit]
[junit] maxProcs : 1
[junit] statesSeen : 8
[junit] statesMatched : 0
[junit] transitionsExecuted : 7
[junit] proverValidCalls : 19601
[junit] CVC3ValidCalls : 2
[junit] memory (bytes) : 130088960
[junit] elapsedTime (s) : 0.016
[junit] The specified properties hold for all executions.
[junit]
[junit] ********** Error Detected **********
[junit] CIVL execution error (kind: ASSERTION_VIOLATION, certainty: PROVEABLE)
[junit] Cannot prove assertion holds: $assert 0==1
[junit] Path condition: true
[junit] Assertion: false
[junit]
[junit] State 4
[junit] | Path condition
[junit] | | true
[junit] | Dynamic scopes
[junit] | | scope 0 (parent=1, static=119)
[junit] | | | reachers: 0
[junit] | | | i = 1
[junit] | | scope 1 (parent=2, static=118)
[junit] | | | reachers: 0
[junit] | | scope 2 (parent=-1, static=117)
[junit] | | | reachers: 0,1
[junit] | | | N = 5
[junit] | | | threads = A_s0v1[0:=PID_1]
[junit] | | scope 3 (parent=4, static=122)
[junit] | | | reachers: 1
[junit] | | scope 4 (parent=2, static=121)
[junit] | | | reachers: 1
[junit] | | | tid = 0
[junit] | Process states
[junit] | | process 0 call stack
[junit] | | | Frame[function=_CIVL_system, location=200, scope=0]
[junit] | | process 1 call stack
[junit] | | | Frame[function=run, location=206, scope=3]
[junit]
[junit] =================== Stats ===================
[junit]
[junit] maxProcs : 2
[junit] statesSeen : 6
[junit] statesMatched : 0
[junit] transitionsExecuted : 5
[junit] proverValidCalls : 19628
[junit] CVC3ValidCalls : 2
[junit] memory (bytes) : 130088960
[junit] elapsedTime (s) : 0.024
[junit] The program MAY NOT be correct.
[junit] =================== Stats ===================
[junit]
[junit] maxProcs : 1
[junit] statesSeen : 6
[junit] statesMatched : 0
[junit] transitionsExecuted : 5
[junit] proverValidCalls : 19640
[junit] CVC3ValidCalls : 2
[junit] memory (bytes) : 130088960
[junit] elapsedTime (s) : 0.024
[junit] The specified properties hold for all executions.
[junit] =================== Stats ===================
[junit]
[junit] maxProcs : 6
[junit] statesSeen : 243601
[junit] statesMatched : 167429
[junit] transitionsExecuted : 411029
[junit] proverValidCalls : 2988769
[junit] CVC3ValidCalls : 2
[junit] memory (bytes) : 790953984
[junit] elapsedTime (s) : 10.494
[junit] The specified properties hold for all executions.
[junit] =================== Stats ===================
[junit]
[junit] maxProcs : 5
[junit] statesSeen : 2620
[junit] statesMatched : 214
[junit] transitionsExecuted : 2833
[junit] proverValidCalls : 3017283
[junit] CVC3ValidCalls : 2
[junit] memory (bytes) : 790953984
[junit] elapsedTime (s) : 0.412
[junit] The specified properties hold for all executions.
[junit] ------------- ---------------- ---------------
[junitreport] Processing /Users/tester/work/civl/0.2/r123/junit/data/TESTS-TestSuites.xml to /var/folders/tb/t0f_d_29043c_qts86hdnb1h0000gt/T/null176754710
[junitreport] Loading stylesheet jar:file:/usr/share/ant/lib/ant-junit.jar!/org/apache/tools/ant/taskdefs/optional/junit/xsl/junit-frames.xsl
[junitreport] Transform time: 327ms
[junitreport] Deleting: /var/folders/tb/t0f_d_29043c_qts86hdnb1h0000gt/T/null176754710
test:
[jacoco:report] Loading execution data file /Users/tester/work/civl/0.2/r123/jacoco.exec
[jacoco:report] Writing group "Test Coverage Report for CIVL 0.2 r123" with 81 classes
javadoc:
[mkdir] Created dir: /Users/tester/work/civl/0.2/r123/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.kripke...
[javadoc] Loading source files for package edu.udel.cis.vsl.civl.library...
[javadoc] Loading source files for package edu.udel.cis.vsl.civl.library.civlc...
[javadoc] Loading source files for package edu.udel.cis.vsl.civl.library.stdlib...
[javadoc] Loading source files for package edu.udel.cis.vsl.civl.log...
[javadoc] Loading source files for package edu.udel.cis.vsl.civl.model...
[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.expression...
[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.model.common...
[javadoc] Loading source files for package edu.udel.cis.vsl.civl.model.common.expression...
[javadoc] Loading source files for package edu.udel.cis.vsl.civl.model.common.location...
[javadoc] Loading source files for package edu.udel.cis.vsl.civl.model.common.statement...
[javadoc] Loading source files for package edu.udel.cis.vsl.civl.model.common.type...
[javadoc] Loading source files for package edu.udel.cis.vsl.civl.model.common.variable...
[javadoc] Loading source files for package edu.udel.cis.vsl.civl.predicate...
[javadoc] Loading source files for package edu.udel.cis.vsl.civl.semantics...
[javadoc] Loading source files for package edu.udel.cis.vsl.civl.semantics.IF...
[javadoc] Loading source files for package edu.udel.cis.vsl.civl.state...
[javadoc] Loading source files for package edu.udel.cis.vsl.civl.transition...
[javadoc] Loading source files for package edu.udel.cis.vsl.civl.util...
[javadoc] Constructing Javadoc information...
[javadoc] Standard Doclet version 1.7.0_15
[javadoc] Building tree for all the packages and classes...
[javadoc] /Users/tester/work/civl/0.2/r123/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:255: warning - @param argument "expresssion" is not a parameter name.
[javadoc] /Users/tester/work/civl/0.2/r123/src/edu/udel/cis/vsl/civl/model/IF/Scope.java:72: warning - @param argument "A" is not a parameter name.
[javadoc] /Users/tester/work/civl/0.2/r123/src/edu/udel/cis/vsl/civl/model/IF/expression/BooleanLiteralExpression.java:23: warning - @param argument "The" is not a parameter name.
[javadoc] /Users/tester/work/civl/0.2/r123/src/edu/udel/cis/vsl/civl/model/IF/type/PrimitiveType.java:24: warning - @param argument "The" is not a parameter name.
[javadoc] /Users/tester/work/civl/0.2/r123/src/edu/udel/cis/vsl/civl/model/common/CommonModelFactory.java:451: warning - @param argument "expresssion" is not a parameter name.
[javadoc] /Users/tester/work/civl/0.2/r123/src/edu/udel/cis/vsl/civl/model/common/CommonScope.java:139: warning - @param argument "A" is not a parameter name.
[javadoc] /Users/tester/work/civl/0.2/r123/src/edu/udel/cis/vsl/civl/model/common/expression/CommonBooleanLiteralExpression.java:25: warning - @param argument "The" is not a parameter name.
[javadoc] /Users/tester/work/civl/0.2/r123/src/edu/udel/cis/vsl/civl/model/common/expression/CommonBooleanLiteralExpression.java:40: warning - @param argument "The" is not a parameter name.
[javadoc] /Users/tester/work/civl/0.2/r123/src/edu/udel/cis/vsl/civl/model/common/type/CommonPrimitiveType.java:21: warning - @param argument "The" is not a parameter name.
[javadoc] /Users/tester/work/civl/0.2/r123/src/edu/udel/cis/vsl/civl/model/common/type/CommonPrimitiveType.java:36: warning - @param argument "The" is not a parameter name.
[javadoc] /Users/tester/work/civl/0.2/r123/src/edu/udel/cis/vsl/civl/predicate/Deadlock.java:79: warning - @param argument "prover" is not a parameter name.
[javadoc] /Users/tester/work/civl/0.2/r123/src/edu/udel/cis/vsl/civl/semantics/Evaluator.java:594: warning - @return tag has no arguments.
[javadoc] /Users/tester/work/civl/0.2/r123/src/edu/udel/cis/vsl/civl/semantics/Executor.java:749: warning - @return tag has no arguments.
[javadoc] /Users/tester/work/civl/0.2/r123/src/edu/udel/cis/vsl/civl/semantics/Executor.java:94: warning - @param argument "prover" is not a parameter name.
[javadoc] /Users/tester/work/civl/0.2/r123/src/edu/udel/cis/vsl/civl/semantics/Executor.java:122: warning - @param argument "prover" is not a parameter name.
[javadoc] /Users/tester/work/civl/0.2/r123/src/edu/udel/cis/vsl/civl/semantics/Executor.java:450: warning - @param argument "State" is not a parameter name.
[javadoc] /Users/tester/work/civl/0.2/r123/src/edu/udel/cis/vsl/civl/state/State.java:190: warning - @return tag has no arguments.
[javadoc] /Users/tester/work/civl/0.2/r123/src/edu/udel/cis/vsl/civl/state/State.java:199: warning - @return tag has no arguments.
[javadoc] /Users/tester/work/civl/0.2/r123/src/edu/udel/cis/vsl/civl/state/StateFactory.java:806: warning - @return tag has no arguments.
[javadoc] /Users/tester/work/civl/0.2/r123/src/edu/udel/cis/vsl/civl/state/StateFactory.java:681: warning - @return tag has no arguments.
[javadoc] /Users/tester/work/civl/0.2/r123/src/edu/udel/cis/vsl/civl/state/StateFactory.java:489: warning - @param argument "scopeID" is not a parameter name.
[javadoc] /Users/tester/work/civl/0.2/r123/src/edu/udel/cis/vsl/civl/state/StateFactory.java:970: warning - @param argument "process" is not a parameter name.
[javadoc] /Users/tester/work/civl/0.2/r123/src/edu/udel/cis/vsl/civl/state/StateFactory.java:970: warning - @param argument "location" is not a parameter name.
[javadoc] /Users/tester/work/civl/0.2/r123/src/edu/udel/cis/vsl/civl/state/StateFactory.java:970: warning - @param argument "lexicalScope" is not a parameter name.
[javadoc] /Users/tester/work/civl/0.2/r123/src/edu/udel/cis/vsl/civl/state/StateFactory.java:970: warning - @param argument "parentScope" is not a parameter name.
[javadoc] /Users/tester/work/civl/0.2/r123/src/edu/udel/cis/vsl/civl/state/StateFactoryIF.java:80: warning - @param argument "scopeID" is not a parameter name.
[javadoc] /Users/tester/work/civl/0.2/r123/src/edu/udel/cis/vsl/civl/state/StateFactoryIF.java:164: warning - @param argument "location" is not a parameter name.
[javadoc] /Users/tester/work/civl/0.2/r123/src/edu/udel/cis/vsl/civl/state/StateFactoryIF.java:164: warning - @param argument "parentScopeId" is not a parameter name.
[javadoc] /Users/tester/work/civl/0.2/r123/src/edu/udel/cis/vsl/civl/transition/Transition.java:52: warning - @param argument "The" is not a parameter name.
[javadoc] /Users/tester/work/civl/0.2/r123/src/edu/udel/cis/vsl/civl/transition/Transition.java:59: warning - @param argument "The" is not a parameter name.
[javadoc] Building index for all the packages and classes...
[javadoc] javadoc: error - Error while reading file /Users/tester/work/civl/0.2/r123/src/overview.html
[javadoc] Building index for all classes...
[javadoc] Generating /Users/tester/work/civl/0.2/r123/doc/javadoc/help-doc.html...
[javadoc] 1 error
[javadoc] 30 warnings
all:
BUILD SUCCESSFUL
Total time: 32 seconds
Stderr: