Path: . Working Copy Root Path: /Users/tester/work/civl/0.2/r121 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: 121 Node Kind: directory Schedule: normal Last Changed Author: siegel Last Changed Rev: 121 Last Changed Date: 2013-06-23 10:43:23 -0400 (Sun, 23 Jun 2013)
Stdout:
Buildfile: /Users/tester/work/civl/0.2/r121/build.xml
compile:
[mkdir] Created dir: /Users/tester/work/civl/0.2/r121/bin
[javac] Compiling 115 source files to /Users/tester/work/civl/0.2/r121/bin
jar:
[jar] Building jar: /Users/tester/work/civl/0.2/r121/civl.jar
test-init:
[mkdir] Created dir: /Users/tester/work/civl/0.2/r121/junit
[mkdir] Created dir: /Users/tester/work/civl/0.2/r121/junit/data
[mkdir] Created dir: /Users/tester/work/civl/0.2/r121/junit/reports
[mkdir] Created dir: /Users/tester/work/civl/0.2/r121/bin-test
test-compile:
[javac] Compiling 1 source file to /Users/tester/work/civl/0.2/r121/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: 20.386 sec
[junit]
[junit] ------------- Standard Output ---------------
[junit] =================== Stats ===================
[junit]
[junit] maxProcs : 4
[junit] statesSeen : 329
[junit] statesMatched : 115
[junit] transitionsExecuted : 443
[junit] proverValidCalls : 1951
[junit] CVC3ValidCalls : 2
[junit] memory (bytes) : 127729664
[junit] elapsedTime (s) : 0.956
[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 : 1963
[junit] CVC3ValidCalls : 2
[junit] memory (bytes) : 127729664
[junit] elapsedTime (s) : 0.028
[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 : 1979
[junit] CVC3ValidCalls : 2
[junit] memory (bytes) : 127729664
[junit] elapsedTime (s) : 0.031
[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 : 2136
[junit] CVC3ValidCalls : 2
[junit] memory (bytes) : 127729664
[junit] elapsedTime (s) : 0.07
[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 66. Target process has not terminated:
[junit] p
[junit] Process 1: at location 71. Cannot prove enabling statement valid:
[junit] false
[junit] Process 2: at location 78. 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=43)
[junit] | | | reachers: 0
[junit] | | | p = PID_1
[junit] | | | q = PID_2
[junit] | | scope 1 (parent=-1, static=42)
[junit] | | | reachers: 0,1,2
[junit] | | | x = 1
[junit] | | | y = 1
[junit] | | scope 2 (parent=3, static=47)
[junit] | | | reachers: 1
[junit] | | scope 3 (parent=4, static=46)
[junit] | | | reachers: 1
[junit] | | | i = 9
[junit] | | scope 4 (parent=5, static=45)
[junit] | | | reachers: 1
[junit] | | scope 5 (parent=1, static=44)
[junit] | | | reachers: 1
[junit] | | | n = 10
[junit] | | scope 6 (parent=7, static=51)
[junit] | | | reachers: 2
[junit] | | scope 7 (parent=8, static=50)
[junit] | | | reachers: 2
[junit] | | | i = 0
[junit] | | scope 8 (parent=9, static=49)
[junit] | | | reachers: 2
[junit] | | scope 9 (parent=1, static=48)
[junit] | | | reachers: 2
[junit] | | | m = 10
[junit] | Process states
[junit] | | process 0 call stack
[junit] | | | Frame[function=_CIVL_system, location=66, scope=0]
[junit] | | process 1 call stack
[junit] | | | Frame[function=f, location=71, scope=2]
[junit] | | process 2 call stack
[junit] | | | Frame[function=g, location=78, scope=6]
[junit] =================== Stats ===================
[junit]
[junit] maxProcs : 3
[junit] statesSeen : 251
[junit] statesMatched : 42
[junit] transitionsExecuted : 292
[junit] proverValidCalls : 3559
[junit] CVC3ValidCalls : 2
[junit] memory (bytes) : 127729664
[junit] elapsedTime (s) : 0.118
[junit] The program MAY NOT be correct.
[junit] =================== Stats ===================
[junit]
[junit] maxProcs : 1
[junit] statesSeen : 1655
[junit] statesMatched : 0
[junit] transitionsExecuted : 1654
[junit] proverValidCalls : 9311
[junit] CVC3ValidCalls : 2
[junit] memory (bytes) : 149356544
[junit] elapsedTime (s) : 6.511
[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 : 9315
[junit] CVC3ValidCalls : 2
[junit] memory (bytes) : 149356544
[junit] elapsedTime (s) : 0.001
[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 : 9352
[junit] CVC3ValidCalls : 2
[junit] memory (bytes) : 149356544
[junit] elapsedTime (s) : 0.032
[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 : 9383
[junit] CVC3ValidCalls : 2
[junit] memory (bytes) : 149356544
[junit] elapsedTime (s) : 0.018
[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 : 19455
[junit] CVC3ValidCalls : 2
[junit] memory (bytes) : 142934016
[junit] elapsedTime (s) : 0.473
[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 : 19602
[junit] CVC3ValidCalls : 2
[junit] memory (bytes) : 142934016
[junit] elapsedTime (s) : 0.013
[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 : 19616
[junit] CVC3ValidCalls : 2
[junit] memory (bytes) : 142934016
[junit] elapsedTime (s) : 0.013
[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 : 19620
[junit] CVC3ValidCalls : 2
[junit] memory (bytes) : 142934016
[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 : 19629
[junit] CVC3ValidCalls : 2
[junit] memory (bytes) : 142934016
[junit] elapsedTime (s) : 0.015
[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 : 19641
[junit] CVC3ValidCalls : 2
[junit] memory (bytes) : 142934016
[junit] elapsedTime (s) : 0.016
[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 : 19659
[junit] CVC3ValidCalls : 2
[junit] memory (bytes) : 142934016
[junit] elapsedTime (s) : 0.017
[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 : 19684
[junit] CVC3ValidCalls : 2
[junit] memory (bytes) : 142934016
[junit] elapsedTime (s) : 0.026
[junit] The program MAY NOT be correct.
[junit] =================== Stats ===================
[junit]
[junit] maxProcs : 1
[junit] statesSeen : 6
[junit] statesMatched : 0
[junit] transitionsExecuted : 5
[junit] proverValidCalls : 19696
[junit] CVC3ValidCalls : 2
[junit] memory (bytes) : 142934016
[junit] elapsedTime (s) : 0.028
[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 : 2878317
[junit] CVC3ValidCalls : 2
[junit] memory (bytes) : 790102016
[junit] elapsedTime (s) : 11.1
[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 : 2907896
[junit] CVC3ValidCalls : 2
[junit] memory (bytes) : 787218432
[junit] elapsedTime (s) : 0.457
[junit] The specified properties hold for all executions.
[junit] ------------- ---------------- ---------------
[junitreport] Processing /Users/tester/work/civl/0.2/r121/junit/data/TESTS-TestSuites.xml to /var/folders/tb/t0f_d_29043c_qts86hdnb1h0000gt/T/null1840880452
[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: 322ms
[junitreport] Deleting: /var/folders/tb/t0f_d_29043c_qts86hdnb1h0000gt/T/null1840880452
test:
[jacoco:report] Loading execution data file /Users/tester/work/civl/0.2/r121/jacoco.exec
[jacoco:report] Writing group "Test Coverage Report for CIVL 0.2 r121" with 81 classes
javadoc:
[mkdir] Created dir: /Users/tester/work/civl/0.2/r121/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/r121/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/r121/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/r121/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/r121/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/r121/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/r121/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/r121/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/r121/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/r121/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/r121/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/r121/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/r121/src/edu/udel/cis/vsl/civl/semantics/Evaluator.java:594: warning - @return tag has no arguments.
[javadoc] /Users/tester/work/civl/0.2/r121/src/edu/udel/cis/vsl/civl/semantics/Executor.java:749: warning - @return tag has no arguments.
[javadoc] /Users/tester/work/civl/0.2/r121/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/r121/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/r121/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/r121/src/edu/udel/cis/vsl/civl/state/State.java:190: warning - @return tag has no arguments.
[javadoc] /Users/tester/work/civl/0.2/r121/src/edu/udel/cis/vsl/civl/state/State.java:199: warning - @return tag has no arguments.
[javadoc] /Users/tester/work/civl/0.2/r121/src/edu/udel/cis/vsl/civl/state/StateFactory.java:806: warning - @return tag has no arguments.
[javadoc] /Users/tester/work/civl/0.2/r121/src/edu/udel/cis/vsl/civl/state/StateFactory.java:681: warning - @return tag has no arguments.
[javadoc] /Users/tester/work/civl/0.2/r121/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/r121/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/r121/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/r121/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/r121/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/r121/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/r121/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/r121/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/r121/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/r121/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/r121/src/overview.html
[javadoc] Building index for all classes...
[javadoc] Generating /Users/tester/work/civl/0.2/r121/doc/javadoc/help-doc.html...
[javadoc] 1 error
[javadoc] 30 warnings
all:
BUILD SUCCESSFUL
Total time: 34 seconds
Stderr: