Path: . Working Copy Root Path: /Users/tester/work/civl/0.3/r234 URL: svn://vsl.cis.udel.edu/civl/tags/0.3 Relative URL: ^/tags/0.3 Repository Root: svn://vsl.cis.udel.edu/civl Repository UUID: fb995dde-84ed-4084-dfe6-e5aef3e2452c Revision: 234 Node Kind: directory Schedule: normal Last Changed Author: siegel Last Changed Rev: 234 Last Changed Date: 2013-11-20 15:15:46 -0500 (Wed, 20 Nov 2013)
Stdout:
Buildfile: /Users/tester/work/civl/0.3/r234/build.xml
compile:
[mkdir] Created dir: /Users/tester/work/civl/0.3/r234/bin
[javac] Compiling 143 source files to /Users/tester/work/civl/0.3/r234/bin
jar:
[jar] Building jar: /Users/tester/work/civl/0.3/r234/civl.jar
test-init:
[mkdir] Created dir: /Users/tester/work/civl/0.3/r234/junit
[mkdir] Created dir: /Users/tester/work/civl/0.3/r234/junit/data
[mkdir] Created dir: /Users/tester/work/civl/0.3/r234/junit/reports
[mkdir] Created dir: /Users/tester/work/civl/0.3/r234/bin-test
test-compile:
[javac] Compiling 3 source files to /Users/tester/work/civl/0.3/r234/bin-test
test-run:
[jacoco:coverage] Enhancing junit with coverage
[junit] Testsuite: edu.udel.cis.vsl.civl.ArithmeticTest
[junit] Tests run: 7, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 4.246 sec
[junit]
[junit] ------------- Standard Output ---------------
[junit] =================== Stats ===================
[junit]
[junit] maxProcs : 1
[junit] statesSeen : 74
[junit] statesMatched : 2
[junit] transitionsExecuted : 75
[junit] proverValidCalls : 256
[junit] CVC3ValidCalls : 16
[junit] memory (bytes) : 76218368
[junit] elapsedTime (s) : 1.232
[junit] The specified properties hold for all executions.
[junit] =================== Stats ===================
[junit]
[junit] maxProcs : 1
[junit] statesSeen : 16
[junit] statesMatched : 0
[junit] transitionsExecuted : 15
[junit] proverValidCalls : 34
[junit] CVC3ValidCalls : 0
[junit] memory (bytes) : 76218368
[junit] elapsedTime (s) : 0.199
[junit] The specified properties hold for all executions.
[junit] =================== Stats ===================
[junit]
[junit] maxProcs : 1
[junit] statesSeen : 21
[junit] statesMatched : 0
[junit] transitionsExecuted : 20
[junit] proverValidCalls : 58
[junit] CVC3ValidCalls : 0
[junit] memory (bytes) : 120520704
[junit] elapsedTime (s) : 0.165
[junit] The specified properties hold for all executions.
[junit] =================== Stats ===================
[junit]
[junit] maxProcs : 1
[junit] statesSeen : 192
[junit] statesMatched : 0
[junit] transitionsExecuted : 191
[junit] proverValidCalls : 641
[junit] CVC3ValidCalls : 3
[junit] memory (bytes) : 161611776
[junit] elapsedTime (s) : 1.227
[junit] The specified properties hold for all executions.
[junit] =================== Stats ===================
[junit]
[junit] maxProcs : 1
[junit] statesSeen : 9
[junit] statesMatched : 0
[junit] transitionsExecuted : 8
[junit] proverValidCalls : 24
[junit] CVC3ValidCalls : 4
[junit] memory (bytes) : 161611776
[junit] elapsedTime (s) : 0.032
[junit] The specified properties hold for all executions.
[junit] =================== Stats ===================
[junit]
[junit] maxProcs : 1
[junit] statesSeen : 825
[junit] statesMatched : 0
[junit] transitionsExecuted : 824
[junit] proverValidCalls : 3267
[junit] CVC3ValidCalls : 0
[junit] memory (bytes) : 150536192
[junit] elapsedTime (s) : 0.762
[junit] The specified properties hold for all executions.
[junit] =================== Model ===================
[junit]
[junit] Model
[junit] | function _CIVL_system
[junit] | | formal parameters
[junit] | | scope 0 (parent: null)
[junit] | | | nx : int
[junit] | | | $input u0 : $real[2]
[junit] | | | nsteps : int
[junit] | | | kappa : $real
[junit] | | | data : $real[2][3]
[junit] | | | u : $real[2]
[junit] | | | scope 4 (parent: 0)
[junit] | | | | scope 5 (parent: 4)
[junit] | | | | | iter : int
[junit] | | | | | scope 6 (parent: 5)
[junit] | | locations (start=0)
[junit] | | | location 0 (scope: 0)
[junit] | | | | when (true) u0 = InitialValue($input u0 : $real[2]); goto location 1
[junit] | | | location 1 (scope: 0)
[junit] | | | | when (true) data = InitialValue(data : $real[2][3]); goto location 2
[junit] | | | location 2 (scope: 0)
[junit] | | | | when (true) u = InitialValue(u : $real[2]); goto location 3
[junit] | | | location 3 (scope: 4)
[junit] | | | | when (true) init(); goto location 4
[junit] | | | location 4 (scope: 4)
[junit] | | | | when (true) write(0); goto location 5
[junit] | | | location 5 (scope: 5)
[junit] | | | | when (true) iter = 1; goto location 6
[junit] | | | location 6 (scope: 5)
[junit] | | | | when (!(iter<=nsteps)) no-op; goto location 10
[junit] | | | | when (iter<=nsteps) no-op; goto location 7
[junit] | | | location 7 (scope: 6)
[junit] | | | | when (true) update(); goto location 8
[junit] | | | location 8 (scope: 6)
[junit] | | | | when (true) write(iter); goto location 9
[junit] | | | location 9 (scope: 5)
[junit] | | | | when (true) iter = iter+1; goto location 6
[junit] | | | location 10 (scope: 0)
[junit] | | | | when (true) return;
[junit] | function init
[junit] | | formal parameters
[junit] | | scope 1 (parent: 0)
[junit] | | | scope 7 (parent: 1)
[junit] | | | | scope 8 (parent: 7)
[junit] | | | | | i : int
[junit] | | | | | scope 9 (parent: 8)
[junit] | | locations (start=11)
[junit] | | | location 11 (scope: 7)
[junit] | | | | when (true) nx = 2; goto location 12
[junit] | | | location 12 (scope: 7)
[junit] | | | | when (true) nsteps = 2; goto location 13
[junit] | | | location 13 (scope: 7)
[junit] | | | | when (true) kappa = 0.1; goto location 14
[junit] | | | location 14 (scope: 8)
[junit] | | | | when (true) i = 0; goto location 15
[junit] | | | location 15 (scope: 8)
[junit] | | | | when (!(i<nx)) no-op; goto location 18
[junit] | | | | when (i<nx) no-op; goto location 16
[junit] | | | location 16 (scope: 9)
[junit] | | | | when (true) u[i] = u0[i]; goto location 17
[junit] | | | location 17 (scope: 8)
[junit] | | | | when (true) i = i+1; goto location 15
[junit] | | | location 18 (scope: 1)
[junit] | | | | when (true) return;
[junit] | function write
[junit] | | formal parameters
[junit] | | | time
[junit] | | scope 2 (parent: 0)
[junit] | | | time : int
[junit] | | | scope 10 (parent: 2)
[junit] | | | | scope 11 (parent: 10)
[junit] | | | | | i : int
[junit] | | | | | scope 12 (parent: 11)
[junit] | | locations (start=19)
[junit] | | | location 19 (scope: 11)
[junit] | | | | when (true) i = 0; goto location 20
[junit] | | | location 20 (scope: 11)
[junit] | | | | when (!(i<nx)) no-op; goto location 23
[junit] | | | | when (i<nx) no-op; goto location 21
[junit] | | | location 21 (scope: 12)
[junit] | | | | when (true) data[time][i] = u[i]; goto location 22
[junit] | | | location 22 (scope: 11)
[junit] | | | | when (true) i = i+1; goto location 20
[junit] | | | location 23 (scope: 2)
[junit] | | | | when (true) return;
[junit] | function update
[junit] | | formal parameters
[junit] | | scope 3 (parent: 0)
[junit] | | | scope 13 (parent: 3)
[junit] | | | | u_new : $real[nx]
[junit] | | | | scope 16 (parent: 13)
[junit] | | | | | i : int
[junit] | | | | | scope 17 (parent: 16)
[junit] | | | | scope 14 (parent: 13)
[junit] | | | | | i : int
[junit] | | | | | scope 15 (parent: 14)
[junit] | | locations (start=24)
[junit] | | | location 24 (scope: 13)
[junit] | | | | when (true) u_new = InitialValue(u_new : $real[nx]); goto location 25
[junit] | | | location 25 (scope: 14)
[junit] | | | | when (true) i = 1; goto location 26
[junit] | | | location 26 (scope: 14)
[junit] | | | | when (i<nx-1) no-op; goto location 27
[junit] | | | | when (!(i<nx-1)) no-op; goto location 29
[junit] | | | location 27 (scope: 15)
[junit] | | | | when (true) u_new[i] = u[i]+kappa*u[i+1]+u[i-1]-($real) 2.0*u[i]; goto location 28
[junit] | | | location 28 (scope: 14)
[junit] | | | | when (true) i = i+1; goto location 26
[junit] | | | location 29 (scope: 16)
[junit] | | | | when (true) i = 1; goto location 30
[junit] | | | location 30 (scope: 16)
[junit] | | | | when (i<nx-1) no-op; goto location 31
[junit] | | | | when (!(i<nx-1)) no-op; goto location 33
[junit] | | | location 31 (scope: 17)
[junit] | | | | when (true) u[i] = u_new[i]; goto location 32
[junit] | | | location 32 (scope: 16)
[junit] | | | | when (true) i = i+1; goto location 30
[junit] | | | location 33 (scope: 3)
[junit] | | | | when (true) return;
[junit] =================== Stats ===================
[junit]
[junit] maxProcs : 1
[junit] statesSeen : 68
[junit] statesMatched : 0
[junit] transitionsExecuted : 67
[junit] proverValidCalls : 194
[junit] CVC3ValidCalls : 0
[junit] memory (bytes) : 150536192
[junit] elapsedTime (s) : 0.162
[junit] The specified properties hold for all executions.
[junit] ------------- ---------------- ---------------
[junit] Testsuite: edu.udel.cis.vsl.civl.ConcurrencyTest
[junit] Tests run: 6, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 3.255 sec
[junit]
[junit] ------------- Standard Output ---------------
[junit] =================== Model ===================
[junit]
[junit] Model
[junit] | function _CIVL_system
[junit] | | formal parameters
[junit] | | scope 0 (parent: null)
[junit] | | | $input a : $real[3]
[junit] | | | scope 3 (parent: 0)
[junit] | | | | seq : $real
[junit] | | | | par : $real
[junit] | | locations (start=0)
[junit] | | | location 0 (scope: 0)
[junit] | | | | when (true) a = InitialValue($input a : $real[3]); goto location 1
[junit] | | | location 1 (scope: 3)
[junit] | | | | when (true) seq = adderSeq(3); goto location 2
[junit] | | | location 2 (scope: 3)
[junit] | | | | when (true) par = adderPar(3); goto location 3
[junit] | | | location 3 (scope: 3)
[junit] | | | | when (true) $assert seq==par; goto location 4
[junit] | | | location 4 (scope: 0)
[junit] | | | | when (true) return;
[junit] | function adderSeq
[junit] | | formal parameters
[junit] | | | n
[junit] | | scope 1 (parent: 0)
[junit] | | | n : int
[junit] | | | scope 4 (parent: 1)
[junit] | | | | s : $real
[junit] | | | | scope 5 (parent: 4)
[junit] | | | | | i : int
[junit] | | | | | scope 6 (parent: 5)
[junit] | | locations (start=5)
[junit] | | | location 5 (scope: 4)
[junit] | | | | when (true) s = 0.0; goto location 6
[junit] | | | location 6 (scope: 5)
[junit] | | | | when (true) i = 0; goto location 7
[junit] | | | location 7 (scope: 5)
[junit] | | | | when (i<n) no-op; goto location 8
[junit] | | | | when (!(i<n)) no-op; goto location 10
[junit] | | | location 8 (scope: 6)
[junit] | | | | when (true) s = s+a[i]; goto location 9
[junit] | | | location 9 (scope: 5)
[junit] | | | | when (true) i = i+1; goto location 7
[junit] | | | location 10 (scope: 4)
[junit] | | | | when (true) return s;
[junit] | function adderPar
[junit] | | formal parameters
[junit] | | | m
[junit] | | scope 2 (parent: 0)
[junit] | | | m : int
[junit] | | | scope 7 (parent: 2)
[junit] | | | | s : $real
[junit] | | | | mutex : int
[junit] | | | | workers : $proc[m]
[junit] | | | | scope 9 (parent: 7)
[junit] | | | | | j : int
[junit] | | | | | scope 10 (parent: 9)
[junit] | | | | scope 11 (parent: 7)
[junit] | | | | | k : int
[junit] | | | | | scope 12 (parent: 11)
[junit] | | locations (start=11)
[junit] | | | location 11 (scope: 7)
[junit] | | | | when (true) s = 0.0; goto location 12
[junit] | | | location 12 (scope: 7)
[junit] | | | | when (true) mutex = 0; goto location 13
[junit] | | | location 13 (scope: 7)
[junit] | | | | when (true) workers = InitialValue(workers : $proc[m]); goto location 14
[junit] | | | location 14 (scope: 9)
[junit] | | | | when (true) j = 0; goto location 15
[junit] | | | location 15 (scope: 9)
[junit] | | | | when (!(j<m)) no-op; goto location 18
[junit] | | | | when (j<m) no-op; goto location 16
[junit] | | | location 16 (scope: 10)
[junit] | | | | when (true) workers[j] = $spawn worker(j); goto location 17
[junit] | | | location 17 (scope: 9)
[junit] | | | | when (true) j = j+1; goto location 15
[junit] | | | location 18 (scope: 11)
[junit] | | | | when (true) k = 0; goto location 19
[junit] | | | location 19 (scope: 11)
[junit] | | | | when (k<m) no-op; goto location 20
[junit] | | | | when (!(k<m)) no-op; goto location 22
[junit] | | | location 20 (scope: 12)
[junit] | | | | when (true) wait workers[k]; goto location 21
[junit] | | | location 21 (scope: 11)
[junit] | | | | when (true) k = k+1; goto location 19
[junit] | | | location 22 (scope: 7)
[junit] | | | | when (true) return s;
[junit] | function worker
[junit] | | formal parameters
[junit] | | | i
[junit] | | scope 8 (parent: 7)
[junit] | | | i : int
[junit] | | | scope 13 (parent: 8)
[junit] | | | | t : $real
[junit] | | locations (start=23)
[junit] | | | location 23 (scope: 13)
[junit] | | | | when (mutex==0) mutex = 1; goto location 24
[junit] | | | location 24 (scope: 13)
[junit] | | | | when (true) t = s; goto location 25
[junit] | | | location 25 (scope: 13)
[junit] | | | | when (true) t = t+a[i]; goto location 26
[junit] | | | location 26 (scope: 13)
[junit] | | | | when (true) s = t; goto location 27
[junit] | | | location 27 (scope: 13)
[junit] | | | | when (true) mutex = 0; goto location 28
[junit] | | | location 28 (scope: 8)
[junit] | | | | when (true) return;
[junit] =================== Stats ===================
[junit]
[junit] maxProcs : 4
[junit] statesSeen : 460
[junit] statesMatched : 200
[junit] transitionsExecuted : 659
[junit] proverValidCalls : 2527
[junit] CVC3ValidCalls : 0
[junit] memory (bytes) : 150536192
[junit] elapsedTime (s) : 0.272
[junit] The specified properties hold for all executions.
[junit] A deadlock is possible:
[junit] *****************************************************************
[junit] Deadlock possible at State 139(nprocs=3, nscopes=10)!
[junit] *****************************************************************
[junit] Process 0: at location 4. Target process has not terminated:
[junit] p
[junit] Process 1: at location 10. Cannot prove enabling statement valid:
[junit] false
[junit] Process 2: at location 18. Cannot prove enabling statement valid:
[junit] false
[junit]
[junit] State 139
[junit] | Path condition
[junit] | | true
[junit] | Dynamic scopes
[junit] | | scope 0 (parent=1, static=3)
[junit] | | | reachers: 0
[junit] | | | p = (process<int>)<1> : process<int>
[junit] | | | q = (process<int>)<2> : process<int>
[junit] | | scope 1 (parent=-1, static=0)
[junit] | | | reachers: 0,1,2
[junit] | | | x = 1 : int
[junit] | | | y = 1 : int
[junit] | | scope 2 (parent=3, static=6)
[junit] | | | reachers: 1
[junit] | | scope 3 (parent=4, static=5)
[junit] | | | reachers: 1
[junit] | | | i = 9 : int
[junit] | | scope 4 (parent=5, static=4)
[junit] | | | reachers: 1
[junit] | | scope 5 (parent=1, static=1)
[junit] | | | reachers: 1
[junit] | | | n = 10 : int
[junit] | | scope 6 (parent=7, static=9)
[junit] | | | reachers: 2
[junit] | | scope 7 (parent=8, static=8)
[junit] | | | reachers: 2
[junit] | | | i = 0 : int
[junit] | | scope 8 (parent=9, static=7)
[junit] | | | reachers: 2
[junit] | | scope 9 (parent=1, static=2)
[junit] | | | reachers: 2
[junit] | | | m = 10 : int
[junit] | Process states
[junit] | | process 0 call stack
[junit] | | | Frame[function=_CIVL_system, location=4, scope=0]
[junit] | | process 1 call stack
[junit] | | | Frame[function=f, location=10, scope=2]
[junit] | | process 2 call stack
[junit] | | | Frame[function=g, location=18, scope=6]
[junit] =================== Stats ===================
[junit]
[junit] maxProcs : 3
[junit] statesSeen : 140
[junit] statesMatched : 1
[junit] transitionsExecuted : 140
[junit] proverValidCalls : 526
[junit] CVC3ValidCalls : 0
[junit] memory (bytes) : 150536192
[junit] elapsedTime (s) : 0.146
[junit] The program MAY NOT be correct.
[junit] =================== Stats ===================
[junit]
[junit] maxProcs : 3
[junit] statesSeen : 3021
[junit] statesMatched : 0
[junit] transitionsExecuted : 3020
[junit] proverValidCalls : 11067
[junit] CVC3ValidCalls : 0
[junit] memory (bytes) : 150536192
[junit] elapsedTime (s) : 0.426
[junit] The specified properties hold for all executions.
[junit] =================== Stats ===================
[junit]
[junit] maxProcs : 5
[junit] statesSeen : 10435
[junit] statesMatched : 2341
[junit] transitionsExecuted : 12775
[junit] proverValidCalls : 91707
[junit] CVC3ValidCalls : 0
[junit] memory (bytes) : 188416000
[junit] elapsedTime (s) : 1.285
[junit] The specified properties hold for all executions.
[junit] =================== Model ===================
[junit]
[junit] Model
[junit] | function _CIVL_system
[junit] | | formal parameters
[junit] | | scope 0 (parent: null)
[junit] | | | N : int
[junit] | | | threads : $proc[N]
[junit] | | | lock : int
[junit] | | | in_barrier : int[N]
[junit] | | | num_in_barrier : int
[junit] | | | counter : int
[junit] | | | scope 4 (parent: 0)
[junit] | | | | scope 6 (parent: 4)
[junit] | | | | | i : int
[junit] | | | | scope 5 (parent: 4)
[junit] | | | | | i : int
[junit] | | locations (start=0)
[junit] | | | location 0 (scope: 0)
[junit] | | | | when (true) N = 3; goto location 1
[junit] | | | location 1 (scope: 0)
[junit] | | | | when (true) threads = InitialValue(threads : $proc[N]); goto location 2
[junit] | | | location 2 (scope: 0)
[junit] | | | | when (true) lock = 0; goto location 3
[junit] | | | location 3 (scope: 0)
[junit] | | | | when (true) in_barrier = InitialValue(in_barrier : int[N]); goto location 4
[junit] | | | location 4 (scope: 0)
[junit] | | | | when (true) num_in_barrier = 0; goto location 5
[junit] | | | location 5 (scope: 0)
[junit] | | | | when (true) counter = 0; goto location 6
[junit] | | | location 6 (scope: 4)
[junit] | | | | when (true) init(); goto location 7
[junit] | | | location 7 (scope: 5)
[junit] | | | | when (true) i = 0; goto location 8
[junit] | | | location 8 (scope: 5)
[junit] | | | | when (i<N) no-op; goto location 9
[junit] | | | | when (!(i<N)) no-op; goto location 11
[junit] | | | location 9 (scope: 5)
[junit] | | | | when (true) threads[i] = $spawn run(i); goto location 10
[junit] | | | location 10 (scope: 5)
[junit] | | | | when (true) i = i+1; goto location 8
[junit] | | | location 11 (scope: 6)
[junit] | | | | when (true) i = 0; goto location 12
[junit] | | | location 12 (scope: 6)
[junit] | | | | when (!(i<N)) no-op; goto location 15
[junit] | | | | when (i<N) no-op; goto location 13
[junit] | | | location 13 (scope: 6)
[junit] | | | | when (true) wait threads[i]; goto location 14
[junit] | | | location 14 (scope: 6)
[junit] | | | | when (true) i = i+1; goto location 12
[junit] | | | location 15 (scope: 0)
[junit] | | | | when (true) return;
[junit] | function init
[junit] | | formal parameters
[junit] | | scope 1 (parent: 0)
[junit] | | | scope 7 (parent: 1)
[junit] | | | | scope 8 (parent: 7)
[junit] | | | | | i : int
[junit] | | locations (start=16)
[junit] | | | location 16 (scope: 8)
[junit] | | | | when (true) i = 0; goto location 17
[junit] | | | location 17 (scope: 8)
[junit] | | | | when (!(i<N)) no-op; goto location 20
[junit] | | | | when (i<N) no-op; goto location 18
[junit] | | | location 18 (scope: 8)
[junit] | | | | when (true) in_barrier[i] = 0; goto location 19
[junit] | | | location 19 (scope: 8)
[junit] | | | | when (true) i = i+1; goto location 17
[junit] | | | location 20 (scope: 1)
[junit] | | | | when (true) return;
[junit] | function barrier
[junit] | | formal parameters
[junit] | | | tid
[junit] | | scope 2 (parent: 0)
[junit] | | | tid : int
[junit] | | | scope 9 (parent: 2)
[junit] | | | | scope 10 (parent: 9)
[junit] | | | | | scope 11 (parent: 10)
[junit] | | | | | | i : int
[junit] | | locations (start=21)
[junit] | | | location 21 (scope: 9)
[junit] | | | | when (lock==0) lock = 1; goto location 22
[junit] | | | location 22 (scope: 9)
[junit] | | | | when (true) in_barrier[tid] = 1; goto location 23
[junit] | | | location 23 (scope: 9)
[junit] | | | | when (true) num_in_barrier = num_in_barrier+1; goto location 24
[junit] | | | location 26 (scope: 11)
[junit] | | | | when (true) i = 0; goto location 27
[junit] | | | location 27 (scope: 11)
[junit] | | | | when (i<N) no-op; goto location 28
[junit] | | | | when (!(i<N)) no-op; goto location 30
[junit] | | | location 28 (scope: 11)
[junit] | | | | when (true) in_barrier[i] = 0; goto location 29
[junit] | | | location 29 (scope: 11)
[junit] | | | | when (true) i = i+1; goto location 27
[junit] | | | location 30 (scope: 10)
[junit] | | | | when (true) num_in_barrier = 0; goto location 25
[junit] | | | location 24 (scope: 9)
[junit] | | | | when (!(num_in_barrier==N)) no-op; goto location 25
[junit] | | | | when (num_in_barrier==N) no-op; goto location 26
[junit] | | | location 25 (scope: 9)
[junit] | | | | when (true) no-op; goto location 31
[junit] | | | location 31 (scope: 9)
[junit] | | | | when (true) lock = 0; goto location 32
[junit] | | | location 32 (scope: 9)
[junit] | | | | when (in_barrier[tid]==0) no-op; goto location 33
[junit] | | | location 33 (scope: 2)
[junit] | | | | when (true) return;
[junit] | function run
[junit] | | formal parameters
[junit] | | | tid
[junit] | | scope 3 (parent: 0)
[junit] | | | tid : int
[junit] | | | scope 12 (parent: 3)
[junit] | | | | scope 13 (parent: 12)
[junit] | | | | | scope 14 (parent: 13)
[junit] | | locations (start=34)
[junit] | | | location 34 (scope: 13)
[junit] | | | | when (!(true)) no-op; goto location 43
[junit] | | | | when (true) no-op; goto location 35
[junit] | | | location 35 (scope: 14)
[junit] | | | | when (true) $assert counter==0; goto location 36
[junit] | | | location 36 (scope: 14)
[junit] | | | | when (true) barrier(tid); goto location 37
[junit] | | | location 37 (scope: 14)
[junit] | | | | when (true) counter = counter+1; goto location 38
[junit] | | | location 38 (scope: 14)
[junit] | | | | when (true) barrier(tid); goto location 39
[junit] | | | location 39 (scope: 14)
[junit] | | | | when (true) $assert counter==N; goto location 40
[junit] | | | location 40 (scope: 14)
[junit] | | | | when (true) barrier(tid); goto location 41
[junit] | | | location 41 (scope: 14)
[junit] | | | | when (true) counter = counter-1; goto location 42
[junit] | | | location 42 (scope: 14)
[junit] | | | | when (true) barrier(tid); goto location 34
[junit] | | | location 43 (scope: 3)
[junit] | | | | when (true) return;
[junit] =================== Stats ===================
[junit]
[junit] maxProcs : 4
[junit] statesSeen : 13387
[junit] statesMatched : 8167
[junit] transitionsExecuted : 21553
[junit] proverValidCalls : 115575
[junit] CVC3ValidCalls : 0
[junit] memory (bytes) : 244449280
[junit] elapsedTime (s) : 0.761
[junit] The specified properties hold for all executions.
[junit] A deadlock is possible:
[junit] *****************************************************************
[junit] Deadlock possible at State 2675(nprocs=6, nscopes=31)!
[junit] *****************************************************************
[junit] Process 0: terminated
[junit] Process 1: at location 18. Cannot prove enabling statement valid:
[junit] false
[junit] Process 2: at location 18. Cannot prove enabling statement valid:
[junit] false
[junit] Process 3: at location 18. Cannot prove enabling statement valid:
[junit] false
[junit] Process 4: at location 18. Cannot prove enabling statement valid:
[junit] false
[junit] Process 5: at location 18. Cannot prove enabling statement valid:
[junit] false
[junit]
[junit] State 2675
[junit] | Path condition
[junit] | | true
[junit] | Dynamic scopes
[junit] | | scope 0 (parent=1, static=14)
[junit] | | | reachers: 1
[junit] | | scope 1 (parent=2, static=12)
[junit] | | | reachers: 1
[junit] | | scope 2 (parent=3, static=8)
[junit] | | | reachers: 1
[junit] | | scope 3 (parent=4, static=7)
[junit] | | | reachers: 1
[junit] | | scope 4 (parent=5, static=6)
[junit] | | | reachers: 1
[junit] | | | left = 0 : int
[junit] | | | right = 1 : int
[junit] | | scope 5 (parent=6, static=1)
[junit] | | | reachers: 1
[junit] | | | id = 0 : int
[junit] | | scope 6 (parent=-1, static=0)
[junit] | | | reachers: 1,2,3,4,5
[junit] | | | n = 5 : int
[junit] | | | chopsticks = X_s0v1[0:=1, 1:=1, 2:=1, 3:=1, 4:=1] : int[5]
[junit] | | scope 7 (parent=8, static=14)
[junit] | | | reachers: 2
[junit] | | scope 8 (parent=9, static=12)
[junit] | | | reachers: 2
[junit] | | scope 9 (parent=10, static=8)
[junit] | | | reachers: 2
[junit] | | scope 10 (parent=11, static=7)
[junit] | | | reachers: 2
[junit] | | scope 11 (parent=12, static=6)
[junit] | | | reachers: 2
[junit] | | | left = 1 : int
[junit] | | | right = 2 : int
[junit] | | scope 12 (parent=6, static=1)
[junit] | | | reachers: 2
[junit] | | | id = 1 : int
[junit] | | scope 13 (parent=14, static=14)
[junit] | | | reachers: 3
[junit] | | scope 14 (parent=15, static=12)
[junit] | | | reachers: 3
[junit] | | scope 15 (parent=16, static=8)
[junit] | | | reachers: 3
[junit] | | scope 16 (parent=17, static=7)
[junit] | | | reachers: 3
[junit] | | scope 17 (parent=18, static=6)
[junit] | | | reachers: 3
[junit] | | | left = 2 : int
[junit] | | | right = 3 : int
[junit] | | scope 18 (parent=6, static=1)
[junit] | | | reachers: 3
[junit] | | | id = 2 : int
[junit] | | scope 19 (parent=20, static=14)
[junit] | | | reachers: 4
[junit] | | scope 20 (parent=21, static=12)
[junit] | | | reachers: 4
[junit] | | scope 21 (parent=22, static=8)
[junit] | | | reachers: 4
[junit] | | scope 22 (parent=23, static=7)
[junit] | | | reachers: 4
[junit] | | scope 23 (parent=24, static=6)
[junit] | | | reachers: 4
[junit] | | | left = 3 : int
[junit] | | | right = 4 : int
[junit] | | scope 24 (parent=6, static=1)
[junit] | | | reachers: 4
[junit] | | | id = 3 : int
[junit] | | scope 25 (parent=26, static=14)
[junit] | | | reachers: 5
[junit] | | scope 26 (parent=27, static=12)
[junit] | | | reachers: 5
[junit] | | scope 27 (parent=28, static=8)
[junit] | | | reachers: 5
[junit] | | scope 28 (parent=29, static=7)
[junit] | | | reachers: 5
[junit] | | scope 29 (parent=30, static=6)
[junit] | | | reachers: 5
[junit] | | | left = 4 : int
[junit] | | | right = 0 : int
[junit] | | scope 30 (parent=6, static=1)
[junit] | | | reachers: 5
[junit] | | | id = 4 : int
[junit] | Process states
[junit] | | process 0 call stack
[junit] | | process 1 call stack
[junit] | | | Frame[function=dine, location=18, scope=0]
[junit] | | process 2 call stack
[junit] | | | Frame[function=dine, location=18, scope=7]
[junit] | | process 3 call stack
[junit] | | | Frame[function=dine, location=18, scope=13]
[junit] | | process 4 call stack
[junit] | | | Frame[function=dine, location=18, scope=19]
[junit] | | process 5 call stack
[junit] | | | Frame[function=dine, location=18, scope=25]
[junit] =================== Stats ===================
[junit]
[junit] maxProcs : 6
[junit] statesSeen : 2676
[junit] statesMatched : 1263
[junit] transitionsExecuted : 3938
[junit] proverValidCalls : 49547
[junit] CVC3ValidCalls : 0
[junit] memory (bytes) : 253886464
[junit] elapsedTime (s) : 0.353
[junit] The program MAY NOT be correct.
[junit] ------------- ---------------- ---------------
[junit] Testsuite: edu.udel.cis.vsl.civl.LanguageFeaturesTest
[junit] Tests run: 35, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 3.633 sec
[junit]
[junit] ------------- Standard Output ---------------
[junit] =================== Model ===================
[junit]
[junit] Model
[junit] | function _CIVL_system
[junit] | | formal parameters
[junit] | | scope 0 (parent: null)
[junit] | | | scope 3 (parent: 0)
[junit] | | | | c : int[6]
[junit] | | | | s : struct foo
[junit] | | | | bun : $bundle
[junit] | | | | scope 4 (parent: 3)
[junit] | | | | | i : int
[junit] | | | | | scope 5 (parent: 4)
[junit] | | locations (start=0)
[junit] | | | location 0 (scope: 3)
[junit] | | | | when (true) c = InitialValue(c : int[6]); goto location 1
[junit] | | | location 1 (scope: 3)
[junit] | | | | when (true) s = InitialValue(s : struct foo); goto location 2
[junit] | | | location 2 (scope: 4)
[junit] | | | | when (true) i = 0; goto location 3
[junit] | | | location 3 (scope: 4)
[junit] | | | | when (!(i<5)) no-op; goto location 6
[junit] | | | | when (i<5) no-op; goto location 4
[junit] | | | location 4 (scope: 5)
[junit] | | | | when (true) s.0[i] = i*i; goto location 5
[junit] | | | location 5 (scope: 4)
[junit] | | | | when (true) i = i+1; goto location 3
[junit] | | | location 6 (scope: 3)
[junit] | | | | when (true) s.1 = 25; goto location 7
[junit] | | | location 7 (scope: 3)
[junit] | | | | when (true) bun = $bundle_pack(&s.0, 6*sizeof(int)); goto location 8
[junit] | | | location 8 (scope: 3)
[junit] | | | | when (true) $bundle_unpack(bun, &c); goto location 9
[junit] | | | location 9 (scope: 3)
[junit] | | | | when (true) $assert c[5]==25; goto location 10
[junit] | | | location 10 (scope: 0)
[junit] | | | | when (true) return;
[junit] | function $bundle_pack
[junit] | | formal parameters
[junit] | | | ptr
[junit] | | | size
[junit] | | scope 1 (parent: 0)
[junit] | | | ptr : void*
[junit] | | | size : int
[junit] | function $bundle_unpack
[junit] | | formal parameters
[junit] | | | bundle
[junit] | | | ptr
[junit] | | scope 2 (parent: 0)
[junit] | | | bundle : $bundle
[junit] | | | ptr : void*
[junit]
[junit] ********** Error Detected **********
[junit] CIVL execution error (kind: OTHER, certainty: PROVEABLE)
[junit] sizeof element does not divide size argument
[junit] at bundleStructComponent.cvl:17.8-43 "$bundle_pack(&(s.a), ... )"
[junit] State
[junit] | Path condition
[junit] | | 0 < SIZEOF_INT
[junit] | Dynamic scopes
[junit] | | scope 0 (parent=1, static=3)
[junit] | | | reachers: 0
[junit] | | | c = X_s0v0 : int[6]
[junit] | | | s = (foo<int[5],int>)<(X_s0v1.0)[0:=0, 1:=1, 2:=4, 3:=9, 4:=16],25> : foo<int[5],int>
[junit] | | | bun = NULL : null
[junit] | | scope 1 (parent=-1, static=0)
[junit] | | | reachers: 0
[junit] | Process states
[junit] | | process 0 call stack
[junit] | | | Frame[function=_CIVL_system, location=7, scope=0]
[junit]
[junit] Path condition is unsatisfiable.
[junit] CIVL execution error (kind: POINTER, certainty: MAYBE)
[junit] unable to get concrete count of 0 or 1 from size
[junit] at bundleStructComponent.cvl:17.8-43 "$bundle_pack(&(s.a), ... )"
[junit] State
[junit] | Path condition
[junit] | | (0 < SIZEOF_INT) && (0 == SIZEOF_INT)
[junit] | Dynamic scopes
[junit] | | scope 0 (parent=1, static=3)
[junit] | | | reachers: 0
[junit] | | | c = X_s0v0 : int[6]
[junit] | | | s = (foo<int[5],int>)<(X_s0v1.0)[0:=0, 1:=1, 2:=4, 3:=9, 4:=16],25> : foo<int[5],int>
[junit] | | | bun = NULL : null
[junit] | | scope 1 (parent=-1, static=0)
[junit] | | | reachers: 0
[junit] | Process states
[junit] | | process 0 call stack
[junit] | | | Frame[function=_CIVL_system, location=7, scope=0]
[junit]
[junit] CIVL execution error (kind: POINTER, certainty: MAYBE)
[junit] unable to get concrete count of 0 or 1 from size
[junit] at bundleStructComponent.cvl:17.8-43 "$bundle_pack(&(s.a), ... )"
[junit] State
[junit] | Path condition
[junit] | | (0 < SIZEOF_INT) && (0 == SIZEOF_INT)
[junit] | Dynamic scopes
[junit] | | scope 0 (parent=1, static=3)
[junit] | | | reachers: 0
[junit] | | | c = X_s0v0 : int[6]
[junit] | | | s = (foo<int[5],int>)<(X_s0v1.0)[0:=0, 1:=1, 2:=4, 3:=9, 4:=16],25> : foo<int[5],int>
[junit] | | | bun = NULL : null
[junit] | | scope 1 (parent=-1, static=0)
[junit] | | | reachers: 0
[junit] | Process states
[junit] | | process 0 call stack
[junit] | | | Frame[function=_CIVL_system, location=7, scope=0]
[junit]
[junit] at edu.udel.cis.vsl.civl.library.civlc.Libcivlc.getArrayFromPointer(Libcivlc.java:966)
[junit] at edu.udel.cis.vsl.civl.library.civlc.Libcivlc.executeBundlePack(Libcivlc.java:357)
[junit] at edu.udel.cis.vsl.civl.library.civlc.Libcivlc.executeWork(Libcivlc.java:816)
[junit] at edu.udel.cis.vsl.civl.library.civlc.Libcivlc.execute(Libcivlc.java:866)
[junit] at edu.udel.cis.vsl.civl.semantics.Executor.executeCall(Executor.java:254)
[junit] at edu.udel.cis.vsl.civl.semantics.Executor.executeWork(Executor.java:508)
[junit] at edu.udel.cis.vsl.civl.semantics.Executor.execute(Executor.java:541)
[junit] at edu.udel.cis.vsl.civl.kripke.StateManager.nextStateWork(StateManager.java:73)
[junit] at edu.udel.cis.vsl.civl.kripke.StateManager.nextState(StateManager.java:45)
[junit] at edu.udel.cis.vsl.civl.kripke.StateManager.nextState(StateManager.java:23)
[junit] at edu.udel.cis.vsl.gmc.DfsSearcher.proceedToNewState(DfsSearcher.java:200)
[junit] at edu.udel.cis.vsl.gmc.DfsSearcher.search(DfsSearcher.java:152)
[junit] at edu.udel.cis.vsl.gmc.DfsSearcher.search(DfsSearcher.java:133)
[junit] at edu.udel.cis.vsl.civl.CIVL.verify(CIVL.java:270)
[junit] at edu.udel.cis.vsl.civl.CIVL.verify(CIVL.java:201)
[junit] at edu.udel.cis.vsl.civl.LanguageFeaturesTest.testBundleStructComponent(LanguageFeaturesTest.java:99)
[junit] at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
[junit] at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:57)
[junit] at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
[junit] at java.lang.reflect.Method.invoke(Method.java:601)
[junit] at org.junit.runners.model.FrameworkMethod$1.runReflectiveCall(FrameworkMethod.java:47)
[junit] at org.junit.internal.runners.model.ReflectiveCallable.run(ReflectiveCallable.java:12)
[junit] at org.junit.runners.model.FrameworkMethod.invokeExplosively(FrameworkMethod.java:44)
[junit] at org.junit.internal.runners.statements.InvokeMethod.evaluate(InvokeMethod.java:17)
[junit] at org.junit.runners.ParentRunner.runLeaf(ParentRunner.java:271)
[junit] at org.junit.runners.BlockJUnit4ClassRunner.runChild(BlockJUnit4ClassRunner.java:70)
[junit] at org.junit.runners.BlockJUnit4ClassRunner.runChild(BlockJUnit4ClassRunner.java:50)
[junit] at org.junit.runners.ParentRunner$3.run(ParentRunner.java:238)
[junit] at org.junit.runners.ParentRunner$1.schedule(ParentRunner.java:63)
[junit] at org.junit.runners.ParentRunner.runChildren(ParentRunner.java:236)
[junit] at org.junit.runners.ParentRunner.access$000(ParentRunner.java:53)
[junit] at org.junit.runners.ParentRunner$2.evaluate(ParentRunner.java:229)
[junit] at org.junit.runners.ParentRunner.run(ParentRunner.java:309)
[junit] at junit.framework.JUnit4TestAdapter.run(JUnit4TestAdapter.java:38)
[junit] at org.apache.tools.ant.taskdefs.optional.junit.JUnitTestRunner.run(JUnitTestRunner.java:523)
[junit] at org.apache.tools.ant.taskdefs.optional.junit.JUnitTestRunner.launch(JUnitTestRunner.java:1063)
[junit] at org.apache.tools.ant.taskdefs.optional.junit.JUnitTestRunner.main(JUnitTestRunner.java:887)
[junit]
[junit] =================== Stats ===================
[junit]
[junit] maxProcs : 1
[junit] statesSeen : 21
[junit] statesMatched : 0
[junit] transitionsExecuted : 20
[junit] proverValidCalls : 61
[junit] CVC3ValidCalls : 0
[junit] memory (bytes) : 253886464
[junit] elapsedTime (s) : 0.118
[junit] The program MAY NOT be correct.
[junit] =================== Stats ===================
[junit]
[junit] maxProcs : 4
[junit] statesSeen : 59
[junit] statesMatched : 0
[junit] transitionsExecuted : 58
[junit] proverValidCalls : 208
[junit] CVC3ValidCalls : 0
[junit] memory (bytes) : 253886464
[junit] elapsedTime (s) : 0.107
[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 : 4
[junit] CVC3ValidCalls : 0
[junit] memory (bytes) : 253886464
[junit] elapsedTime (s) : 0.002
[junit] The specified properties hold for all executions.
[junit] =================== Stats ===================
[junit]
[junit] maxProcs : 1
[junit] statesSeen : 66
[junit] statesMatched : 0
[junit] transitionsExecuted : 65
[junit] proverValidCalls : 185
[junit] CVC3ValidCalls : 0
[junit] memory (bytes) : 253886464
[junit] elapsedTime (s) : 0.004
[junit] The specified properties hold for all executions.
[junit] =================== Model ===================
[junit]
[junit] Model
[junit] | function _CIVL_system
[junit] | | formal parameters
[junit] | | scope 0 (parent: null)
[junit] | | | scope 3 (parent: 0)
[junit] | | | | h : $heap
[junit] | | | | p : $real*
[junit] | | locations (start=0)
[junit] | | | location 0 (scope: 3)
[junit] | | | | when (true) h = InitialValue(h : $heap); goto location 1
[junit] | | | location 1 (scope: 3)
[junit] | | | | when (true) p = ($real*)$malloc(&h, 5*sizeof($real)); goto location 2
[junit] | | | location 2 (scope: 3)
[junit] | | | | when (true) *(p+4) = 3.14; goto location 3
[junit] | | | location 3 (scope: 3)
[junit] | | | | when (true) $free(&h, p); goto location 4
[junit] | | | location 4 (scope: 3)
[junit] | | | | when (true) $assert *(p+4)==3.14; goto location 5
[junit] | | | location 5 (scope: 0)
[junit] | | | | when (true) return;
[junit] | function $malloc
[junit] | | formal parameters
[junit] | | | h
[junit] | | | size
[junit] | | scope 1 (parent: 0)
[junit] | | | h : $heap*
[junit] | | | size : int
[junit] | function $free
[junit] | | formal parameters
[junit] | | | h
[junit] | | | p
[junit] | | scope 2 (parent: 0)
[junit] | | | h : $heap*
[junit] | | | p : void*
[junit]
[junit] ********** Error Detected **********
[junit] CIVL execution error (kind: ASSERTION_VIOLATION, certainty: PROVEABLE)
[junit] Cannot prove assertion holds: $assert *(p+4)==3.14
[junit] Path condition: 0 <= SIZEOF_REAL+-1
[junit] Assertion: 0 == -1*UNDEFINED[4]+157/50
[junit]
[junit] at mallocBad.cvl:10.2-21 "$assert(p[4]==3.14)"
[junit] State
[junit] | Path condition
[junit] | | 0 <= SIZEOF_REAL+-1
[junit] | Dynamic scopes
[junit] | | scope 0 (parent=1, static=3)
[junit] | | | reachers: 0
[junit] | | | h = ($heap<real[][]>)<(real[1][])<UNDEFINED>> : $heap<real[][]>
[junit] | | | p = (pointer<scope<int>,int,Ref<int>>)<(scope<int>)<0>,0,ArrayElementRef(ArrayElementRef(TupleComponentRef((Ref<int>)<1>,0),0),0)> : pointer<scope<int>,int,Ref<int>>
[junit] | | scope 1 (parent=-1, static=0)
[junit] | | | reachers: 0
[junit] | Process states
[junit] | | process 0 call stack
[junit] | | | Frame[function=_CIVL_system, location=4, scope=0]
[junit]
[junit] =================== Stats ===================
[junit]
[junit] maxProcs : 1
[junit] statesSeen : 7
[junit] statesMatched : 0
[junit] transitionsExecuted : 6
[junit] proverValidCalls : 16
[junit] CVC3ValidCalls : 4
[junit] memory (bytes) : 253886464
[junit] elapsedTime (s) : 0.116
[junit] The program MAY NOT be correct.
[junit] =================== Stats ===================
[junit]
[junit] maxProcs : 1
[junit] statesSeen : 132
[junit] statesMatched : 0
[junit] transitionsExecuted : 131
[junit] proverValidCalls : 421
[junit] CVC3ValidCalls : 0
[junit] memory (bytes) : 253886464
[junit] elapsedTime (s) : 0.108
[junit] The specified properties hold for all executions.
[junit] =================== Stats ===================
[junit]
[junit] maxProcs : 1
[junit] statesSeen : 61
[junit] statesMatched : 0
[junit] transitionsExecuted : 60
[junit] proverValidCalls : 232
[junit] CVC3ValidCalls : 0
[junit] memory (bytes) : 253886464
[junit] elapsedTime (s) : 0.117
[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 : 9
[junit] CVC3ValidCalls : 0
[junit] memory (bytes) : 253886464
[junit] elapsedTime (s) : 0.099
[junit] The specified properties hold for all executions.
[junit] =================== Stats ===================
[junit]
[junit] maxProcs : 3
[junit] statesSeen : 103
[junit] statesMatched : 0
[junit] transitionsExecuted : 102
[junit] proverValidCalls : 328
[junit] CVC3ValidCalls : 2
[junit] memory (bytes) : 253886464
[junit] elapsedTime (s) : 0.126
[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 : 11
[junit] CVC3ValidCalls : 0
[junit] memory (bytes) : 253886464
[junit] elapsedTime (s) : 0.105
[junit] The specified properties hold for all executions.
[junit] =================== Model ===================
[junit]
[junit] Model
[junit] | function _CIVL_system
[junit] | | formal parameters
[junit] | | scope 0 (parent: null)
[junit] | | | $input N : int
[junit] | | | $input a : $real[N]
[junit] | | | scope 3 (parent: 0)
[junit] | | | | b : $real[N]
[junit] | | | | bun : $bundle
[junit] | | locations (start=0)
[junit] | | | location 0 (scope: 0)
[junit] | | | | when (true) N = InitialValue($input N : int); goto location 1
[junit] | | | location 1 (scope: 0)
[junit] | | | | when (true) $assume 2<=N; goto location 2
[junit] | | | location 2 (scope: 0)
[junit] | | | | when (true) a = InitialValue($input a : $real[N]); goto location 3
[junit] | | | location 3 (scope: 3)
[junit] | | | | when (true) b = InitialValue(b : $real[N]); goto location 4
[junit] | | | location 4 (scope: 3)
[junit] | | | | when (true) bun = $bundle_pack(&a[0], N*sizeof($real)); goto location 5
[junit] | | | location 5 (scope: 3)
[junit] | | | | when (true) $bundle_unpack(bun, &b[0]); goto location 6
[junit] | | | location 6 (scope: 3)
[junit] | | | | when (true) $assert a[0]==b[0]; goto location 7
[junit] | | | location 7 (scope: 3)
[junit] | | | | when (true) $assert a[1]==b[1]; goto location 8
[junit] | | | location 8 (scope: 0)
[junit] | | | | when (true) return;
[junit] | function $bundle_pack
[junit] | | formal parameters
[junit] | | | ptr
[junit] | | | size
[junit] | | scope 1 (parent: 0)
[junit] | | | ptr : void*
[junit] | | | size : int
[junit] | function $bundle_unpack
[junit] | | formal parameters
[junit] | | | bundle
[junit] | | | ptr
[junit] | | scope 2 (parent: 0)
[junit] | | | bundle : $bundle
[junit] | | | ptr : void*
[junit] =================== Stats ===================
[junit]
[junit] maxProcs : 1
[junit] statesSeen : 10
[junit] statesMatched : 0
[junit] transitionsExecuted : 9
[junit] proverValidCalls : 32
[junit] CVC3ValidCalls : 8
[junit] memory (bytes) : 253886464
[junit] elapsedTime (s) : 0.113
[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 : 31
[junit] CVC3ValidCalls : 0
[junit] memory (bytes) : 253886464
[junit] elapsedTime (s) : 0.098
[junit] The specified properties hold for all executions.
[junit] =================== Stats ===================
[junit]
[junit] maxProcs : 1
[junit] statesSeen : 7
[junit] statesMatched : 0
[junit] transitionsExecuted : 6
[junit] proverValidCalls : 15
[junit] CVC3ValidCalls : 0
[junit] memory (bytes) : 253886464
[junit] elapsedTime (s) : 0.129
[junit] The specified properties hold for all executions.
[junit] =================== Model ===================
[junit]
[junit] Model
[junit] | function _CIVL_system
[junit] | | formal parameters
[junit] | | scope 0 (parent: null)
[junit] | | | scope 2 (parent: 0)
[junit] | | | | h : $heap
[junit] | | | | p : $real*
[junit] | | locations (start=0)
[junit] | | | location 0 (scope: 2)
[junit] | | | | when (true) h = InitialValue(h : $heap); goto location 1
[junit] | | | location 1 (scope: 2)
[junit] | | | | when (true) *(p+4) = 3.14; goto location 2
[junit] | | | location 2 (scope: 2)
[junit] | | | | when (true) $assert *(p+4)==3.14; goto location 3
[junit] | | | location 3 (scope: 2)
[junit] | | | | when (true) $free(&h, p); goto location 4
[junit] | | | location 4 (scope: 0)
[junit] | | | | when (true) return;
[junit] | function $free
[junit] | | formal parameters
[junit] | | | h
[junit] | | | p
[junit] | | scope 1 (parent: 0)
[junit] | | | h : $heap*
[junit] | | | p : void*
[junit]
[junit] ********** Error Detected **********
[junit] CIVL execution error (kind: UNDEFINED_VALUE, certainty: PROVEABLE)
[junit] Attempt to read uninitialized variable
[junit] at mallocBad2.cvl:8.2-3 "p"
[junit] State
[junit] | Path condition
[junit] | | true
[junit] | Dynamic scopes
[junit] | | scope 0 (parent=1, static=2)
[junit] | | | reachers: 0
[junit] | | | h = ($heap<>)<> : $heap<>
[junit] | | | p = NULL : null
[junit] | | scope 1 (parent=-1, static=0)
[junit] | | | reachers: 0
[junit] | Process states
[junit] | | process 0 call stack
[junit] | | | Frame[function=_CIVL_system, location=1, scope=0]
[junit]
[junit] =================== Stats ===================
[junit]
[junit] maxProcs : 1
[junit] statesSeen : 2
[junit] statesMatched : 1
[junit] transitionsExecuted : 2
[junit] proverValidCalls : 3
[junit] CVC3ValidCalls : 0
[junit] memory (bytes) : 253886464
[junit] elapsedTime (s) : 0.107
[junit] The program MAY NOT be correct.
[junit] =================== Model ===================
[junit]
[junit] Model
[junit] | function _CIVL_system
[junit] | | formal parameters
[junit] | | scope 0 (parent: null)
[junit] | | | scope 3 (parent: 0)
[junit] | | | | h : $heap
[junit] | | | | h0 : $heap
[junit] | | | | p : $real*
[junit] | | locations (start=0)
[junit] | | | location 0 (scope: 3)
[junit] | | | | when (true) h = InitialValue(h : $heap); goto location 1
[junit] | | | location 1 (scope: 3)
[junit] | | | | when (true) h0 = InitialValue(h0 : $heap); goto location 2
[junit] | | | location 2 (scope: 3)
[junit] | | | | when (true) p = ($real*)$malloc(&h, 5*sizeof($real)); goto location 3
[junit] | | | location 3 (scope: 3)
[junit] | | | | when (true) *(p+4) = 3.14; goto location 4
[junit] | | | location 4 (scope: 3)
[junit] | | | | when (true) $assert *(p+4)==3.14; goto location 5
[junit] | | | location 5 (scope: 3)
[junit] | | | | when (true) $free(&h0, p); goto location 6
[junit] | | | location 6 (scope: 0)
[junit] | | | | when (true) return;
[junit] | function $malloc
[junit] | | formal parameters
[junit] | | | h
[junit] | | | size
[junit] | | scope 1 (parent: 0)
[junit] | | | h : $heap*
[junit] | | | size : int
[junit] | function $free
[junit] | | formal parameters
[junit] | | | h
[junit] | | | p
[junit] | | scope 2 (parent: 0)
[junit] | | | h : $heap*
[junit] | | | p : void*
[junit]
[junit] ********** Error Detected **********
[junit] CIVL execution error (kind: MALLOC, certainty: PROVEABLE)
[junit] Invalid pointer for heap
[junit] at mallocBad3.cvl:10.13-14 "p"
[junit] State
[junit] | Path condition
[junit] | | 0 <= SIZEOF_REAL+-1
[junit] | Dynamic scopes
[junit] | | scope 0 (parent=1, static=3)
[junit] | | | reachers: 0
[junit] | | | h = ($heap<real[][]>)<(real[1][])<H_p0s0v0i0l0[4:=157/50]>> : $heap<real[][]>
[junit] | | | h0 = ($heap<real[][]>)<(real[0][])<>> : $heap<real[][]>
[junit] | | | p = (pointer<scope<int>,int,Ref<int>>)<(scope<int>)<0>,0,ArrayElementRef(ArrayElementRef(TupleComponentRef((Ref<int>)<1>,0),0),0)> : pointer<scope<int>,int,Ref<int>>
[junit] | | scope 1 (parent=-1, static=0)
[junit] | | | reachers: 0
[junit] | Process states
[junit] | | process 0 call stack
[junit] | | | Frame[function=_CIVL_system, location=5, scope=0]
[junit]
[junit] Path condition is unsatisfiable.
[junit] =================== Stats ===================
[junit]
[junit] maxProcs : 1
[junit] statesSeen : 7
[junit] statesMatched : 0
[junit] transitionsExecuted : 6
[junit] proverValidCalls : 17
[junit] CVC3ValidCalls : 1
[junit] memory (bytes) : 253886464
[junit] elapsedTime (s) : 0.103
[junit] The program MAY NOT be correct.
[junit] =================== Model ===================
[junit]
[junit] Model
[junit] | function _CIVL_system
[junit] | | formal parameters
[junit] | | scope 0 (parent: null)
[junit] | | | scope 3 (parent: 0)
[junit] | | | | h : $heap
[junit] | | | | h0 : $heap
[junit] | | | | p : $real*
[junit] | | locations (start=0)
[junit] | | | location 0 (scope: 3)
[junit] | | | | when (true) h = InitialValue(h : $heap); goto location 1
[junit] | | | location 1 (scope: 3)
[junit] | | | | when (true) h0 = InitialValue(h0 : $heap); goto location 2
[junit] | | | location 2 (scope: 3)
[junit] | | | | when (true) p = ($real*)$malloc(&h, 5*sizeof($real)); goto location 3
[junit] | | | location 3 (scope: 3)
[junit] | | | | when (true) h = h0; goto location 4
[junit] | | | location 4 (scope: 3)
[junit] | | | | when (true) *(p+4) = 3.14; goto location 5
[junit] | | | location 5 (scope: 3)
[junit] | | | | when (true) $assert *(p+4)==3.14; goto location 6
[junit] | | | location 6 (scope: 3)
[junit] | | | | when (true) $free(&h, p); goto location 7
[junit] | | | location 7 (scope: 0)
[junit] | | | | when (true) return;
[junit] | function $malloc
[junit] | | formal parameters
[junit] | | | h
[junit] | | | size
[junit] | | scope 1 (parent: 0)
[junit] | | | h : $heap*
[junit] | | | size : int
[junit] | function $free
[junit] | | formal parameters
[junit] | | | h
[junit] | | | p
[junit] | | scope 2 (parent: 0)
[junit] | | | h : $heap*
[junit] | | | p : void*
[junit] A CIVL internal error has occurred.
[junit] Please send an error report to civl-dev@udel.edu.
[junit] SARL exception: edu.udel.cis.vsl.sarl.IF.SARLException: Array index out of bounds in method arrayRead.
[junit] array: (real[0][])<>
[junit] extent: 0
[junit] index: 0
[junit] at mallocBad4.cvl:9.2-6 "p[4]"
[junit] A CIVL internal error has occurred.
[junit] Please send an error report to civl-dev@udel.edu.
[junit] SARL exception: edu.udel.cis.vsl.sarl.IF.SARLException: Array index out of bounds in method arrayRead.
[junit] array: (real[0][])<>
[junit] extent: 0
[junit] index: 0
[junit] at mallocBad4.cvl:9.2-6 "p[4]"
[junit] at edu.udel.cis.vsl.civl.semantics.Executor.execute(Executor.java:545)
[junit] at edu.udel.cis.vsl.civl.kripke.StateManager.nextStateWork(StateManager.java:73)
[junit] at edu.udel.cis.vsl.civl.kripke.StateManager.nextState(StateManager.java:45)
[junit] at edu.udel.cis.vsl.civl.kripke.StateManager.nextState(StateManager.java:23)
[junit] at edu.udel.cis.vsl.gmc.DfsSearcher.proceedToNewState(DfsSearcher.java:200)
[junit] at edu.udel.cis.vsl.gmc.DfsSearcher.search(DfsSearcher.java:152)
[junit] at edu.udel.cis.vsl.gmc.DfsSearcher.search(DfsSearcher.java:133)
[junit] at edu.udel.cis.vsl.civl.CIVL.verify(CIVL.java:270)
[junit] at edu.udel.cis.vsl.civl.CIVL.verify(CIVL.java:201)
[junit] at edu.udel.cis.vsl.civl.LanguageFeaturesTest.testMallocBad4(LanguageFeaturesTest.java:53)
[junit] at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
[junit] at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:57)
[junit] at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
[junit] at java.lang.reflect.Method.invoke(Method.java:601)
[junit] at org.junit.runners.model.FrameworkMethod$1.runReflectiveCall(FrameworkMethod.java:47)
[junit] at org.junit.internal.runners.model.ReflectiveCallable.run(ReflectiveCallable.java:12)
[junit] at org.junit.runners.model.FrameworkMethod.invokeExplosively(FrameworkMethod.java:44)
[junit] at org.junit.internal.runners.statements.InvokeMethod.evaluate(InvokeMethod.java:17)
[junit] at org.junit.runners.ParentRunner.runLeaf(ParentRunner.java:271)
[junit] at org.junit.runners.BlockJUnit4ClassRunner.runChild(BlockJUnit4ClassRunner.java:70)
[junit] at org.junit.runners.BlockJUnit4ClassRunner.runChild(BlockJUnit4ClassRunner.java:50)
[junit] at org.junit.runners.ParentRunner$3.run(ParentRunner.java:238)
[junit] at org.junit.runners.ParentRunner$1.schedule(ParentRunner.java:63)
[junit] at org.junit.runners.ParentRunner.runChildren(ParentRunner.java:236)
[junit] at org.junit.runners.ParentRunner.access$000(ParentRunner.java:53)
[junit] at org.junit.runners.ParentRunner$2.evaluate(ParentRunner.java:229)
[junit] at org.junit.runners.ParentRunner.run(ParentRunner.java:309)
[junit] at junit.framework.JUnit4TestAdapter.run(JUnit4TestAdapter.java:38)
[junit] at org.apache.tools.ant.taskdefs.optional.junit.JUnitTestRunner.run(JUnitTestRunner.java:523)
[junit] at org.apache.tools.ant.taskdefs.optional.junit.JUnitTestRunner.launch(JUnitTestRunner.java:1063)
[junit] at org.apache.tools.ant.taskdefs.optional.junit.JUnitTestRunner.main(JUnitTestRunner.java:887)
[junit]
[junit] =================== Stats ===================
[junit]
[junit] maxProcs : 1
[junit] statesSeen : 5
[junit] statesMatched : 0
[junit] transitionsExecuted : 4
[junit] proverValidCalls : 10
[junit] CVC3ValidCalls : 1
[junit] memory (bytes) : 253886464
[junit] elapsedTime (s) : 0.103
[junit] The program MAY NOT be correct.
[junit] =================== Stats ===================
[junit]
[junit] maxProcs : 1
[junit] statesSeen : 981
[junit] statesMatched : 0
[junit] transitionsExecuted : 980
[junit] proverValidCalls : 3263
[junit] CVC3ValidCalls : 0
[junit] memory (bytes) : 253886464
[junit] elapsedTime (s) : 0.155
[junit] The specified properties hold for all executions.
[junit] =================== Model ===================
[junit]
[junit] Model
[junit] | function _CIVL_system
[junit] | | formal parameters
[junit] | | scope 0 (parent: null)
[junit] | | | N : int
[junit] | | | $input a : $real[N]
[junit] | | | scope 3 (parent: 0)
[junit] | | | | b : $real[N]
[junit] | | | | bun : $bundle
[junit] | | | | scope 5 (parent: 3)
[junit] | | | | | i : int
[junit] | | | | scope 4 (parent: 3)
[junit] | | | | | i : int
[junit] | | locations (start=0)
[junit] | | | location 0 (scope: 0)
[junit] | | | | when (true) N = 5; goto location 1
[junit] | | | location 1 (scope: 0)
[junit] | | | | when (true) a = InitialValue($input a : $real[N]); goto location 2
[junit] | | | location 2 (scope: 3)
[junit] | | | | when (true) b = InitialValue(b : $real[N]); goto location 3
[junit] | | | location 3 (scope: 4)
[junit] | | | | when (true) i = 0; goto location 4
[junit] | | | location 4 (scope: 4)
[junit] | | | | when (i<N) no-op; goto location 5
[junit] | | | | when (!(i<N)) no-op; goto location 7
[junit] | | | location 5 (scope: 4)
[junit] | | | | when (true) a[i] = ($real) i; goto location 6
[junit] | | | location 6 (scope: 4)
[junit] | | | | when (true) i = i+1; goto location 4
[junit] | | | location 7 (scope: 3)
[junit] | | | | when (true) bun = $bundle_pack(&a[0], 3*sizeof($real)); goto location 8
[junit] | | | location 8 (scope: 3)
[junit] | | | | when (true) $bundle_unpack(bun, &b[0]); goto location 9
[junit] | | | location 9 (scope: 5)
[junit] | | | | when (true) i = 0; goto location 10
[junit] | | | location 10 (scope: 5)
[junit] | | | | when (i<3) no-op; goto location 11
[junit] | | | | when (!(i<3)) no-op; goto location 13
[junit] | | | location 11 (scope: 5)
[junit] | | | | when (true) $assert b[i]==a[i]; goto location 12
[junit] | | | location 12 (scope: 5)
[junit] | | | | when (true) i = i+1; goto location 10
[junit] | | | location 13 (scope: 0)
[junit] | | | | when (true) return;
[junit] | function $bundle_pack
[junit] | | formal parameters
[junit] | | | ptr
[junit] | | | size
[junit] | | scope 1 (parent: 0)
[junit] | | | ptr : void*
[junit] | | | size : int
[junit] | function $bundle_unpack
[junit] | | formal parameters
[junit] | | | bundle
[junit] | | | ptr
[junit] | | scope 2 (parent: 0)
[junit] | | | bundle : $bundle
[junit] | | | ptr : void*
[junit] =================== Stats ===================
[junit]
[junit] maxProcs : 1
[junit] statesSeen : 35
[junit] statesMatched : 0
[junit] transitionsExecuted : 34
[junit] proverValidCalls : 111
[junit] CVC3ValidCalls : 1
[junit] memory (bytes) : 253886464
[junit] elapsedTime (s) : 0.11
[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 : 14
[junit] CVC3ValidCalls : 0
[junit] memory (bytes) : 253886464
[junit] elapsedTime (s) : 0.099
[junit] The specified properties hold for all executions.
[junit] =================== Stats ===================
[junit]
[junit] maxProcs : 1
[junit] statesSeen : 84
[junit] statesMatched : 4
[junit] transitionsExecuted : 87
[junit] proverValidCalls : 310
[junit] CVC3ValidCalls : 46
[junit] memory (bytes) : 253886464
[junit] elapsedTime (s) : 0.24
[junit] The specified properties hold for all executions.
[junit] =================== Model ===================
[junit]
[junit] Model
[junit] | function _CIVL_system
[junit] | | formal parameters
[junit] | | scope 0 (parent: null)
[junit] | | | N : int
[junit] | | | $input a : $real[N]
[junit] | | | scope 3 (parent: 0)
[junit] | | | | bun : $bundle
[junit] | | | | size : int
[junit] | | | | scope 4 (parent: 3)
[junit] | | | | | i : int
[junit] | | locations (start=0)
[junit] | | | location 0 (scope: 0)
[junit] | | | | when (true) N = 5; goto location 1
[junit] | | | location 1 (scope: 0)
[junit] | | | | when (true) a = InitialValue($input a : $real[N]); goto location 2
[junit] | | | location 2 (scope: 4)
[junit] | | | | when (true) i = 0; goto location 3
[junit] | | | location 3 (scope: 4)
[junit] | | | | when (i<N) no-op; goto location 4
[junit] | | | | when (!(i<N)) no-op; goto location 6
[junit] | | | location 4 (scope: 4)
[junit] | | | | when (true) a[i] = ($real) i; goto location 5
[junit] | | | location 5 (scope: 4)
[junit] | | | | when (true) i = i+1; goto location 3
[junit] | | | location 6 (scope: 3)
[junit] | | | | when (true) bun = $bundle_pack(&a[0], N*sizeof($real)); goto location 7
[junit] | | | location 7 (scope: 3)
[junit] | | | | when (true) size = $bundle_size(bun); goto location 8
[junit] | | | location 8 (scope: 3)
[junit] | | | | when (true) $assert size==N*sizeof($real); goto location 9
[junit] | | | location 9 (scope: 3)
[junit] | | | | when (true) $assert size/sizeof($real)==N; goto location 10
[junit] | | | location 10 (scope: 0)
[junit] | | | | when (true) return;
[junit] | function $bundle_size
[junit] | | formal parameters
[junit] | | | b
[junit] | | scope 1 (parent: 0)
[junit] | | | b : $bundle
[junit] | function $bundle_pack
[junit] | | formal parameters
[junit] | | | ptr
[junit] | | | size
[junit] | | scope 2 (parent: 0)
[junit] | | | ptr : void*
[junit] | | | size : int
[junit] =================== Stats ===================
[junit]
[junit] maxProcs : 1
[junit] statesSeen : 25
[junit] statesMatched : 0
[junit] transitionsExecuted : 24
[junit] proverValidCalls : 69
[junit] CVC3ValidCalls : 1
[junit] memory (bytes) : 253886464
[junit] elapsedTime (s) : 0.106
[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 : 4
[junit] CVC3ValidCalls : 0
[junit] memory (bytes) : 253886464
[junit] elapsedTime (s) : 0.001
[junit] The specified properties hold for all executions.
[junit] =================== Stats ===================
[junit]
[junit] maxProcs : 1
[junit] statesSeen : 19
[junit] statesMatched : 0
[junit] transitionsExecuted : 18
[junit] proverValidCalls : 51
[junit] CVC3ValidCalls : 0
[junit] memory (bytes) : 253886464
[junit] elapsedTime (s) : 0.101
[junit] The specified properties hold for all executions.
[junit] =================== Stats ===================
[junit]
[junit] maxProcs : 1
[junit] statesSeen : 18
[junit] statesMatched : 0
[junit] transitionsExecuted : 17
[junit] proverValidCalls : 39
[junit] CVC3ValidCalls : 0
[junit] memory (bytes) : 253886464
[junit] elapsedTime (s) : 0.099
[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 : 19
[junit] CVC3ValidCalls : 0
[junit] memory (bytes) : 253886464
[junit] elapsedTime (s) : 0.096
[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 : 9
[junit] CVC3ValidCalls : 1
[junit] memory (bytes) : 253886464
[junit] elapsedTime (s) : 0.099
[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 : 27
[junit] CVC3ValidCalls : 0
[junit] memory (bytes) : 253886464
[junit] elapsedTime (s) : 0.096
[junit] The specified properties hold for all executions.
[junit] =================== Stats ===================
[junit]
[junit] maxProcs : 1
[junit] statesSeen : 31
[junit] statesMatched : 0
[junit] transitionsExecuted : 30
[junit] proverValidCalls : 79
[junit] CVC3ValidCalls : 0
[junit] memory (bytes) : 253886464
[junit] elapsedTime (s) : 0.093
[junit] The specified properties hold for all executions.
[junit] =================== Model ===================
[junit]
[junit] Model
[junit] | function _CIVL_system
[junit] | | formal parameters
[junit] | | scope 0 (parent: null)
[junit] | | | scope 3 (parent: 0)
[junit] | | | | h : $heap
[junit] | | | | p : $real*
[junit] | | locations (start=0)
[junit] | | | location 0 (scope: 3)
[junit] | | | | when (true) h = InitialValue(h : $heap); goto location 1
[junit] | | | location 1 (scope: 3)
[junit] | | | | when (true) p = ($real*)$malloc(&h, 5*sizeof($real)); goto location 2
[junit] | | | location 2 (scope: 3)
[junit] | | | | when (true) *(p+4) = 3.14; goto location 3
[junit] | | | location 3 (scope: 3)
[junit] | | | | when (true) $assert *(p+4)==3.14; goto location 4
[junit] | | | location 4 (scope: 3)
[junit] | | | | when (true) $free(&h, p); goto location 5
[junit] | | | location 5 (scope: 0)
[junit] | | | | when (true) return;
[junit] | function $malloc
[junit] | | formal parameters
[junit] | | | h
[junit] | | | size
[junit] | | scope 1 (parent: 0)
[junit] | | | h : $heap*
[junit] | | | size : int
[junit] | function $free
[junit] | | formal parameters
[junit] | | | h
[junit] | | | p
[junit] | | scope 2 (parent: 0)
[junit] | | | h : $heap*
[junit] | | | p : void*
[junit] =================== Stats ===================
[junit]
[junit] maxProcs : 1
[junit] statesSeen : 7
[junit] statesMatched : 0
[junit] transitionsExecuted : 6
[junit] proverValidCalls : 17
[junit] CVC3ValidCalls : 1
[junit] memory (bytes) : 253886464
[junit] elapsedTime (s) : 0.1
[junit] The specified properties hold for all executions.
[junit] =================== Model ===================
[junit]
[junit] Model
[junit] | function _CIVL_system
[junit] | | formal parameters
[junit] | | scope 0 (parent: null)
[junit] | | | scope 3 (parent: 0)
[junit] | | | | interval0 : struct Interval
[junit] | | | | interval1 : struct Interval
[junit] | | | | bun : $bundle
[junit] | | locations (start=0)
[junit] | | | location 0 (scope: 3)
[junit] | | | | when (true) interval0 = InitialValue(interval0 : struct Interval); goto location 1
[junit] | | | location 1 (scope: 3)
[junit] | | | | when (true) interval1 = InitialValue(interval1 : struct Interval); goto location 2
[junit] | | | location 2 (scope: 3)
[junit] | | | | when (true) interval0.0 = 0; goto location 3
[junit] | | | location 3 (scope: 3)
[junit] | | | | when (true) interval0.1 = 1; goto location 4
[junit] | | | location 4 (scope: 3)
[junit] | | | | when (true) bun = $bundle_pack(&interval0, sizeof(struct Interval)); goto location 5
[junit] | | | location 5 (scope: 3)
[junit] | | | | when (true) $bundle_unpack(bun, &interval1); goto location 6
[junit] | | | location 6 (scope: 3)
[junit] | | | | when (true) $assert interval0.0==interval1.0; goto location 7
[junit] | | | location 7 (scope: 3)
[junit] | | | | when (true) $assert interval0.1==interval1.1; goto location 8
[junit] | | | location 8 (scope: 0)
[junit] | | | | when (true) return;
[junit] | function $bundle_pack
[junit] | | formal parameters
[junit] | | | ptr
[junit] | | | size
[junit] | | scope 1 (parent: 0)
[junit] | | | ptr : void*
[junit] | | | size : int
[junit] | function $bundle_unpack
[junit] | | formal parameters
[junit] | | | bundle
[junit] | | | ptr
[junit] | | scope 2 (parent: 0)
[junit] | | | bundle : $bundle
[junit] | | | ptr : void*
[junit] =================== Stats ===================
[junit]
[junit] maxProcs : 1
[junit] statesSeen : 10
[junit] statesMatched : 0
[junit] transitionsExecuted : 9
[junit] proverValidCalls : 24
[junit] CVC3ValidCalls : 1
[junit] memory (bytes) : 253886464
[junit] elapsedTime (s) : 0.099
[junit] The specified properties hold for all executions.
[junit] =================== Stats ===================
[junit]
[junit] maxProcs : 1
[junit] statesSeen : 9
[junit] statesMatched : 0
[junit] transitionsExecuted : 8
[junit] proverValidCalls : 21
[junit] CVC3ValidCalls : 1
[junit] memory (bytes) : 253886464
[junit] elapsedTime (s) : 0.105
[junit] The specified properties hold for all executions.
[junit] =================== Stats ===================
[junit]
[junit] maxProcs : 1
[junit] statesSeen : 7
[junit] statesMatched : 0
[junit] transitionsExecuted : 6
[junit] proverValidCalls : 14
[junit] CVC3ValidCalls : 0
[junit] memory (bytes) : 253886464
[junit] elapsedTime (s) : 0.09
[junit] The specified properties hold for all executions.
[junit] =================== Stats ===================
[junit]
[junit] maxProcs : 1
[junit] statesSeen : 16
[junit] statesMatched : 3
[junit] transitionsExecuted : 18
[junit] proverValidCalls : 68
[junit] CVC3ValidCalls : 18
[junit] memory (bytes) : 253886464
[junit] elapsedTime (s) : 0.146
[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 : 16
[junit] CVC3ValidCalls : 0
[junit] memory (bytes) : 253886464
[junit] elapsedTime (s) : 0.099
[junit] The specified properties hold for all executions.
[junit] =================== Stats ===================
[junit]
[junit] maxProcs : 1
[junit] statesSeen : 9
[junit] statesMatched : 0
[junit] transitionsExecuted : 8
[junit] proverValidCalls : 19
[junit] CVC3ValidCalls : 0
[junit] memory (bytes) : 253886464
[junit] elapsedTime (s) : 0.092
[junit] The specified properties hold for all executions.
[junit] ------------- ---------------- ---------------
[junit] ------------- Standard Error -----------------
[junit] edu.udel.cis.vsl.sarl.IF.SARLException: Array index out of bounds in method arrayRead.
[junit] array: (real[0][])<>
[junit] extent: 0
[junit] index: 0
[junit] at edu.udel.cis.vsl.sarl.preuniverse.common.CommonPreUniverse.err(CommonPreUniverse.java:213)
[junit] at edu.udel.cis.vsl.sarl.preuniverse.common.CommonPreUniverse.arrayRead(CommonPreUniverse.java:1724)
[junit] at edu.udel.cis.vsl.sarl.preuniverse.common.CommonPreUniverse.dereference(CommonPreUniverse.java:2239)
[junit] at edu.udel.cis.vsl.civl.semantics.Evaluator.dereference(Evaluator.java:1652)
[junit] at edu.udel.cis.vsl.civl.semantics.Evaluator.pointerAdd(Evaluator.java:566)
[junit] at edu.udel.cis.vsl.civl.semantics.Evaluator.evaluateBinary(Evaluator.java:1050)
[junit] at edu.udel.cis.vsl.civl.semantics.Evaluator.evaluate(Evaluator.java:1886)
[junit] at edu.udel.cis.vsl.civl.semantics.Evaluator.reference(Evaluator.java:1613)
[junit] at edu.udel.cis.vsl.civl.semantics.Executor.assign(Executor.java:200)
[junit] at edu.udel.cis.vsl.civl.semantics.Executor.executeAssign(Executor.java:225)
[junit] at edu.udel.cis.vsl.civl.semantics.Executor.executeWork(Executor.java:512)
[junit] at edu.udel.cis.vsl.civl.semantics.Executor.execute(Executor.java:541)
[junit] at edu.udel.cis.vsl.civl.kripke.StateManager.nextStateWork(StateManager.java:73)
[junit] at edu.udel.cis.vsl.civl.kripke.StateManager.nextState(StateManager.java:45)
[junit] at edu.udel.cis.vsl.civl.kripke.StateManager.nextState(StateManager.java:23)
[junit] at edu.udel.cis.vsl.gmc.DfsSearcher.proceedToNewState(DfsSearcher.java:200)
[junit] at edu.udel.cis.vsl.gmc.DfsSearcher.search(DfsSearcher.java:152)
[junit] at edu.udel.cis.vsl.gmc.DfsSearcher.search(DfsSearcher.java:133)
[junit] at edu.udel.cis.vsl.civl.CIVL.verify(CIVL.java:270)
[junit] at edu.udel.cis.vsl.civl.CIVL.verify(CIVL.java:201)
[junit] at edu.udel.cis.vsl.civl.LanguageFeaturesTest.testMallocBad4(LanguageFeaturesTest.java:53)
[junit] at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
[junit] at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:57)
[junit] at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
[junit] at java.lang.reflect.Method.invoke(Method.java:601)
[junit] at org.junit.runners.model.FrameworkMethod$1.runReflectiveCall(FrameworkMethod.java:47)
[junit] at org.junit.internal.runners.model.ReflectiveCallable.run(ReflectiveCallable.java:12)
[junit] at org.junit.runners.model.FrameworkMethod.invokeExplosively(FrameworkMethod.java:44)
[junit] at org.junit.internal.runners.statements.InvokeMethod.evaluate(InvokeMethod.java:17)
[junit] at org.junit.runners.ParentRunner.runLeaf(ParentRunner.java:271)
[junit] at org.junit.runners.BlockJUnit4ClassRunner.runChild(BlockJUnit4ClassRunner.java:70)
[junit] at org.junit.runners.BlockJUnit4ClassRunner.runChild(BlockJUnit4ClassRunner.java:50)
[junit] at org.junit.runners.ParentRunner$3.run(ParentRunner.java:238)
[junit] at org.junit.runners.ParentRunner$1.schedule(ParentRunner.java:63)
[junit] at org.junit.runners.ParentRunner.runChildren(ParentRunner.java:236)
[junit] at org.junit.runners.ParentRunner.access$000(ParentRunner.java:53)
[junit] at org.junit.runners.ParentRunner$2.evaluate(ParentRunner.java:229)
[junit] at org.junit.runners.ParentRunner.run(ParentRunner.java:309)
[junit] at junit.framework.JUnit4TestAdapter.run(JUnit4TestAdapter.java:38)
[junit] at org.apache.tools.ant.taskdefs.optional.junit.JUnitTestRunner.run(JUnitTestRunner.java:523)
[junit] at org.apache.tools.ant.taskdefs.optional.junit.JUnitTestRunner.launch(JUnitTestRunner.java:1063)
[junit] at org.apache.tools.ant.taskdefs.optional.junit.JUnitTestRunner.main(JUnitTestRunner.java:887)
[junit] ------------- ---------------- ---------------
[junitreport] Processing /Users/tester/work/civl/0.3/r234/junit/data/TESTS-TestSuites.xml to /var/folders/tb/t0f_d_29043c_qts86hdnb1h0000gt/T/null805444506
[junitreport] Loading stylesheet jar:file:/opt/local/share/java/apache-ant/lib/ant-junit.jar!/org/apache/tools/ant/taskdefs/optional/junit/xsl/junit-frames.xsl
[junitreport] Transform time: 411ms
[junitreport] Deleting: /var/folders/tb/t0f_d_29043c_qts86hdnb1h0000gt/T/null805444506
test:
[jacoco:report] Loading execution data file /Users/tester/work/civl/0.3/r234/jacoco.exec
[jacoco:report] Writing group "Test Coverage Report for CIVL 0.3 r234" with 103 classes
javadoc:
[mkdir] Created dir: /Users/tester/work/civl/0.3/r234/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.err...
[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.3/r234/src/edu/udel/cis/vsl/civl/model/IF/CIVLSource.java:41: warning - @return tag has no arguments.
[javadoc] /Users/tester/work/civl/0.3/r234/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:437: warning - @return tag has no arguments.
[javadoc] /Users/tester/work/civl/0.3/r234/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:386: warning - @param argument "expresssion" is not a parameter name.
[javadoc] /Users/tester/work/civl/0.3/r234/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:424: warning - Tag @link: reference not found: CIVLDynamicType
[javadoc] /Users/tester/work/civl/0.3/r234/src/edu/udel/cis/vsl/civl/model/IF/Scope.java:77: warning - @param argument "A" is not a parameter name.
[javadoc] /Users/tester/work/civl/0.3/r234/src/edu/udel/cis/vsl/civl/model/IF/expression/DynamicTypeOfExpression.java:23: warning - Tag @link: reference not found: CIVLDynamicType
[javadoc] /Users/tester/work/civl/0.3/r234/src/edu/udel/cis/vsl/civl/model/IF/statement/MallocStatement.java:76: warning - @return tag has no arguments.
[javadoc] /Users/tester/work/civl/0.3/r234/src/edu/udel/cis/vsl/civl/model/IF/type/CIVLType.java:52: warning - Tag @link: reference not found: PrimitiveTypeKind.VOID
[javadoc] /Users/tester/work/civl/0.3/r234/src/edu/udel/cis/vsl/civl/model/IF/type/CIVLType.java:52: warning - Tag @link: reference not found: PrimitiveTypeKind.VOID
[javadoc] /Users/tester/work/civl/0.3/r234/src/edu/udel/cis/vsl/civl/model/common/CommonIdentifier.java:26: warning - @param argument "name" is not a parameter name.
[javadoc] /Users/tester/work/civl/0.3/r234/src/edu/udel/cis/vsl/civl/model/common/CommonModelFactory.java:633: warning - @param argument "expresssion" is not a parameter name.
[javadoc] /Users/tester/work/civl/0.3/r234/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:424: warning - Tag @link: reference not found: CIVLDynamicType
[javadoc] /Users/tester/work/civl/0.3/r234/src/edu/udel/cis/vsl/civl/model/common/CommonModelFactory.java:714: warning - @param argument "field" is not a parameter name.
[javadoc] /Users/tester/work/civl/0.3/r234/src/edu/udel/cis/vsl/civl/model/common/CommonScope.java:143: warning - @param argument "A" is not a parameter name.
[javadoc] /Users/tester/work/civl/0.3/r234/src/edu/udel/cis/vsl/civl/model/common/ModelBuilderWorker.java:612: warning - @return tag has no arguments.
[javadoc] /Users/tester/work/civl/0.3/r234/src/edu/udel/cis/vsl/civl/model/common/ModelBuilderWorker.java:2065: warning - @return tag has no arguments.
[javadoc] /Users/tester/work/civl/0.3/r234/src/edu/udel/cis/vsl/civl/model/common/ModelBuilderWorker.java:2160: warning - @return tag has no arguments.
[javadoc] /Users/tester/work/civl/0.3/r234/src/edu/udel/cis/vsl/civl/model/common/ModelBuilderWorker.java:2740: warning - @param argument "unit" is not a parameter name.
[javadoc] /Users/tester/work/civl/0.3/r234/src/edu/udel/cis/vsl/civl/model/common/ModelBuilderWorker.java:2740: warning - @return tag cannot be used in method with void return type.
[javadoc] /Users/tester/work/civl/0.3/r234/src/edu/udel/cis/vsl/civl/model/common/expression/CommonBooleanLiteralExpression.java:26: warning - @param argument "The" is not a parameter name.
[javadoc] /Users/tester/work/civl/0.3/r234/src/edu/udel/cis/vsl/civl/model/common/expression/CommonBooleanLiteralExpression.java:42: warning - @param argument "The" is not a parameter name.
[javadoc] /Users/tester/work/civl/0.3/r234/src/edu/udel/cis/vsl/civl/model/common/expression/CommonDotExpression.java:28: warning - @param argument "field" is not a parameter name.
[javadoc] /Users/tester/work/civl/0.3/r234/src/edu/udel/cis/vsl/civl/model/IF/type/CIVLType.java:52: warning - Tag @link: reference not found: PrimitiveTypeKind.VOID
[javadoc] /Users/tester/work/civl/0.3/r234/src/edu/udel/cis/vsl/civl/model/IF/type/CIVLType.java:52: warning - Tag @link: reference not found: PrimitiveTypeKind.VOID
[javadoc] /Users/tester/work/civl/0.3/r234/src/edu/udel/cis/vsl/civl/model/IF/type/CIVLType.java:52: warning - Tag @link: reference not found: PrimitiveTypeKind.VOID
[javadoc] /Users/tester/work/civl/0.3/r234/src/edu/udel/cis/vsl/civl/model/IF/type/CIVLType.java:52: warning - Tag @link: reference not found: PrimitiveTypeKind.VOID
[javadoc] /Users/tester/work/civl/0.3/r234/src/edu/udel/cis/vsl/civl/model/common/type/CommonPrimitiveType.java:64: warning - @param argument "The" is not a parameter name.
[javadoc] /Users/tester/work/civl/0.3/r234/src/edu/udel/cis/vsl/civl/model/IF/type/CIVLType.java:52: warning - Tag @link: reference not found: PrimitiveTypeKind.VOID
[javadoc] /Users/tester/work/civl/0.3/r234/src/edu/udel/cis/vsl/civl/model/IF/type/CIVLType.java:52: warning - Tag @link: reference not found: PrimitiveTypeKind.VOID
[javadoc] /Users/tester/work/civl/0.3/r234/src/edu/udel/cis/vsl/civl/predicate/Deadlock.java:82: warning - @param argument "prover" is not a parameter name.
[javadoc] /Users/tester/work/civl/0.3/r234/src/edu/udel/cis/vsl/civl/state/Initializer.java:24: warning - @return tag has no arguments.
[javadoc] /Users/tester/work/civl/0.3/r234/src/edu/udel/cis/vsl/civl/semantics/Evaluator.java:360: warning - @return tag has no arguments.
[javadoc] /Users/tester/work/civl/0.3/r234/src/edu/udel/cis/vsl/civl/semantics/Evaluator.java:1738: warning - @return tag has no arguments.
[javadoc] /Users/tester/work/civl/0.3/r234/src/edu/udel/cis/vsl/civl/semantics/Evaluator.java:1331: warning - @return tag has no arguments.
[javadoc] /Users/tester/work/civl/0.3/r234/src/edu/udel/cis/vsl/civl/semantics/Evaluator.java:176: warning - @param argument "symbolicUniverse" is not a parameter name.
[javadoc] /Users/tester/work/civl/0.3/r234/src/edu/udel/cis/vsl/civl/semantics/Evaluator.java:360: warning - @param argument "assumption" is not a parameter name.
[javadoc] /Users/tester/work/civl/0.3/r234/src/edu/udel/cis/vsl/civl/semantics/Executor.java:482: warning - @return tag has no arguments.
[javadoc] /Users/tester/work/civl/0.3/r234/src/edu/udel/cis/vsl/civl/semantics/Executor.java:538: warning - @return tag has no arguments.
[javadoc] /Users/tester/work/civl/0.3/r234/src/edu/udel/cis/vsl/civl/semantics/Executor.java:98: warning - @param argument "model" is not a parameter name.
[javadoc] /Users/tester/work/civl/0.3/r234/src/edu/udel/cis/vsl/civl/semantics/Executor.java:98: warning - @param argument "symbolicUniverse" is not a parameter name.
[javadoc] /Users/tester/work/civl/0.3/r234/src/edu/udel/cis/vsl/civl/semantics/Executor.java:98: warning - @param argument "prover" is not a parameter name.
[javadoc] /Users/tester/work/civl/0.3/r234/src/edu/udel/cis/vsl/civl/semantics/Executor.java:122: warning - @param argument "model" is not a parameter name.
[javadoc] /Users/tester/work/civl/0.3/r234/src/edu/udel/cis/vsl/civl/semantics/Executor.java:122: warning - @param argument "symbolicUniverse" is not a parameter name.
[javadoc] /Users/tester/work/civl/0.3/r234/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.3/r234/src/edu/udel/cis/vsl/civl/state/State.java:191: warning - @return tag has no arguments.
[javadoc] /Users/tester/work/civl/0.3/r234/src/edu/udel/cis/vsl/civl/state/State.java:200: warning - @return tag has no arguments.
[javadoc] /Users/tester/work/civl/0.3/r234/src/edu/udel/cis/vsl/civl/state/StateFactory.java:611: warning - @return tag has no arguments.
[javadoc] /Users/tester/work/civl/0.3/r234/src/edu/udel/cis/vsl/civl/state/StateFactory.java:564: warning - @return tag has no arguments.
[javadoc] /Users/tester/work/civl/0.3/r234/src/edu/udel/cis/vsl/civl/state/StateFactory.java:339: warning - @param argument "variable" is not a parameter name.
[javadoc] /Users/tester/work/civl/0.3/r234/src/edu/udel/cis/vsl/civl/state/StateFactory.java:339: warning - @param argument "scopeID" is not a parameter name.
[javadoc] /Users/tester/work/civl/0.3/r234/src/edu/udel/cis/vsl/civl/state/StateFactory.java:775: warning - @param argument "process" is not a parameter name.
[javadoc] /Users/tester/work/civl/0.3/r234/src/edu/udel/cis/vsl/civl/state/StateFactory.java:775: warning - @param argument "location" is not a parameter name.
[javadoc] /Users/tester/work/civl/0.3/r234/src/edu/udel/cis/vsl/civl/state/StateFactory.java:775: warning - @param argument "lexicalScope" is not a parameter name.
[javadoc] /Users/tester/work/civl/0.3/r234/src/edu/udel/cis/vsl/civl/state/StateFactory.java:775: warning - @param argument "parentScope" is not a parameter name.
[javadoc] /Users/tester/work/civl/0.3/r234/src/edu/udel/cis/vsl/civl/state/StateFactoryIF.java:88: warning - @param argument "scopeID" is not a parameter name.
[javadoc] /Users/tester/work/civl/0.3/r234/src/edu/udel/cis/vsl/civl/state/StateFactoryIF.java:175: warning - @param argument "location" is not a parameter name.
[javadoc] /Users/tester/work/civl/0.3/r234/src/edu/udel/cis/vsl/civl/state/StateFactoryIF.java:175: warning - @param argument "parentScopeId" is not a parameter name.
[javadoc] /Users/tester/work/civl/0.3/r234/src/edu/udel/cis/vsl/civl/transition/Transition.java:61: warning - @param argument "The" is not a parameter name.
[javadoc] /Users/tester/work/civl/0.3/r234/src/edu/udel/cis/vsl/civl/transition/Transition.java:69: warning - @param argument "The" is not a parameter name.
[javadoc] Building index for all the packages and classes...
[javadoc] Building index for all classes...
[javadoc] Generating /Users/tester/work/civl/0.3/r234/doc/javadoc/help-doc.html...
[javadoc] 1 error
[javadoc] 59 warnings
[javadoc] javadoc: error - Error while reading file /Users/tester/work/civl/0.3/r234/src/overview.html
[javadoc] Patched 1 link injection vulnerable javadocs
all:
BUILD SUCCESSFUL
Total time: 20 seconds
Stderr: