Path: . URL: svn://vsl.cis.udel.edu/civl/tags/0.1 Repository Root: svn://vsl.cis.udel.edu/civl Repository UUID: fb995dde-84ed-4084-dfe6-e5aef3e2452c Revision: 93 Node Kind: directory Schedule: normal Last Changed Author: siegel Last Changed Rev: 93 Last Changed Date: 2013-05-01 12:01:05 -0400 (Wed, 01 May 2013)
Stdout:
Buildfile: /Users/tester/work/civl/0.1/r93/build.xml
compile:
[mkdir] Created dir: /Users/tester/work/civl/0.1/r93/bin
[javac] Compiling 111 source files to /Users/tester/work/civl/0.1/r93/bin
jar:
[jar] Building jar: /Users/tester/work/civl/0.1/r93/civl.jar
test-init:
[mkdir] Created dir: /Users/tester/work/civl/0.1/r93/junit
[mkdir] Created dir: /Users/tester/work/civl/0.1/r93/junit/data
[mkdir] Created dir: /Users/tester/work/civl/0.1/r93/junit/reports
[mkdir] Created dir: /Users/tester/work/civl/0.1/r93/bin-test
test-compile:
[javac] Compiling 5 source files to /Users/tester/work/civl/0.1/r93/bin-test
test-run:
[jacoco:coverage] Enhancing junit with coverage
[junit] Testsuite: edu.udel.cis.vsl.civl.AdderTest
[junit] Tests run: 1, Failures: 0, Errors: 0, Time elapsed: 1.016 sec
[junit]
[junit] ------------- Standard Output ---------------
[junit] =================== Model ===================
[junit]
[junit] Model
[junit] | function _CIVL_system
[junit] | | formal parameters
[junit] | | scope 3 (parent: null)
[junit] | | | a : real[]
[junit] | | | scope 4 (parent: 3)
[junit] | | | | seq : real
[junit] | | | | par : real
[junit] | | locations (start=0)
[junit] | | | location 0 (scope: 4)
[junit] | | | | when (true) seq = adderSeq(n : int); goto location 1
[junit] | | | location 1 (scope: 4)
[junit] | | | | when (true) par = adderPar(m : int); goto location 2
[junit] | | | location 2 (scope: 4)
[junit] | | | | when (true) $assert seq==par; goto location 3
[junit] | | | location 3 (scope: 3)
[junit] | | | | when (true) return;
[junit] | function adderSeq
[junit] | | formal parameters
[junit] | | | n
[junit] | | scope 5 (parent: 3)
[junit] | | | n : int
[junit] | | | scope 6 (parent: 5)
[junit] | | | | s : real
[junit] | | | | scope 7 (parent: 6)
[junit] | | | | | i : int
[junit] | | | | | scope 8 (parent: 7)
[junit] | | locations (start=4)
[junit] | | | location 4 (scope: 6)
[junit] | | | | when (true) s = 0.0; goto location 5
[junit] | | | location 5 (scope: 7)
[junit] | | | | when (true) i = 0; goto location 6
[junit] | | | location 6 (scope: 8)
[junit] | | | | when (true&&i<n) s = s+a[i]; goto location 7
[junit] | | | | when (!(i<n)) ; goto location 8
[junit] | | | location 7 (scope: 7)
[junit] | | | | when (true) i = i+1; goto location 6
[junit] | | | location 8 (scope: 6)
[junit] | | | | when (true) return s;
[junit] | function adderPar
[junit] | | formal parameters
[junit] | | | m
[junit] | | scope 9 (parent: 3)
[junit] | | | m : int
[junit] | | | scope 10 (parent: 9)
[junit] | | | | s : real
[junit] | | | | mutex : int
[junit] | | | | workers : process[]
[junit] | | | | scope 13 (parent: 10)
[junit] | | | | | k : int
[junit] | | | | | scope 14 (parent: 13)
[junit] | | | | scope 11 (parent: 10)
[junit] | | | | | j : int
[junit] | | | | | scope 12 (parent: 11)
[junit] | | locations (start=9)
[junit] | | | location 9 (scope: 10)
[junit] | | | | when (true) s = 0.0; goto location 10
[junit] | | | location 10 (scope: 10)
[junit] | | | | when (true) mutex = 0; goto location 11
[junit] | | | location 11 (scope: 11)
[junit] | | | | when (true) j = 0; goto location 12
[junit] | | | location 12 (scope: 12)
[junit] | | | | when (!(j<m)) ; goto location 14
[junit] | | | | when (true&&j<m) workers[j] = spawn worker(j); goto location 13
[junit] | | | location 13 (scope: 11)
[junit] | | | | when (true) j = j+1; goto location 12
[junit] | | | location 14 (scope: 13)
[junit] | | | | when (true) k = 0; goto location 15
[junit] | | | location 15 (scope: 14)
[junit] | | | | when (!(k<m)) ; goto location 17
[junit] | | | | when (true&&k<m) wait workers[k]; goto location 16
[junit] | | | location 16 (scope: 13)
[junit] | | | | when (true) k = k+1; goto location 15
[junit] | | | location 17 (scope: 10)
[junit] | | | | when (true) return s;
[junit] | function worker
[junit] | | formal parameters
[junit] | | | i
[junit] | | scope 15 (parent: 10)
[junit] | | | i : int
[junit] | | | scope 16 (parent: 15)
[junit] | | | | t : real
[junit] | | locations (start=18)
[junit] | | | location 18 (scope: 16)
[junit] | | | | when (mutex==0) mutex = 1; goto location 19
[junit] | | | location 19 (scope: 16)
[junit] | | | | when (true) t = s; goto location 20
[junit] | | | location 20 (scope: 16)
[junit] | | | | when (true) t = t+a[i]; goto location 21
[junit] | | | location 21 (scope: 16)
[junit] | | | | when (true) s = t; goto location 22
[junit] | | | location 22 (scope: 16)
[junit] | | | | when (true) mutex = 0; goto location 23
[junit] | | | location 23 (scope: 15)
[junit] | | | | when (true) return;
[junit] =================== Stats ===================
[junit]
[junit] maxProcs : 4
[junit] statesSeen : 329
[junit] statesMatched : 115
[junit] transitionsExecuted : 443
[junit] proverValidCalls : 1951
[junit] CVC3ValidCalls : 2
[junit] memory (bytes) : 159121408
[junit] elapsedTime (s) : 0.347
[junit] The specified properties hold for all executions.
[junit] ------------- ---------------- ---------------
[junit] Testsuite: edu.udel.cis.vsl.civl.ArraysTest
[junit] Tests run: 2, Failures: 0, Errors: 0, Time elapsed: 0.035 sec
[junit]
[junit] ------------- Standard Output ---------------
[junit] =================== Model ===================
[junit]
[junit] Model
[junit] | function _CIVL_system
[junit] | | formal parameters
[junit] | | scope 3 (parent: null)
[junit] | | | scope 4 (parent: 3)
[junit] | | | | a : int[][]
[junit] | | | | b : int[]
[junit] | | locations (start=0)
[junit] | | | location 0 (scope: 4)
[junit] | | | | when (true) a[0][0] = 2; goto location 1
[junit] | | | location 1 (scope: 4)
[junit] | | | | when (true) b[1] = 5; goto location 2
[junit] | | | location 2 (scope: 4)
[junit] | | | | when (true) $assert a[0][0]==2; goto location 3
[junit] | | | location 3 (scope: 4)
[junit] | | | | when (true) $assert b[1]==5; goto location 4
[junit] | | | location 4 (scope: 3)
[junit] | | | | when (true) return;
[junit] =================== Stats ===================
[junit]
[junit] maxProcs : 1
[junit] statesSeen : 6
[junit] statesMatched : 0
[junit] transitionsExecuted : 5
[junit] proverValidCalls : 12
[junit] CVC3ValidCalls : 1
[junit] memory (bytes) : 159121408
[junit] elapsedTime (s) : 0.003
[junit] The specified properties hold for all executions.
[junit] array2d: new row is: a[0][0:=2]
[junit] ------------- ---------------- ---------------
[junit] Testsuite: edu.udel.cis.vsl.civl.ChooseTest
[junit] Tests run: 1, Failures: 0, Errors: 0, Time elapsed: 0.036 sec
[junit]
[junit] ------------- Standard Output ---------------
[junit] =================== Model ===================
[junit]
[junit] Model
[junit] | function _CIVL_system
[junit] | | formal parameters
[junit] | | scope 3 (parent: null)
[junit] | | | n : int
[junit] | | | x : real
[junit] | | | scope 4 (parent: 3)
[junit] | | | | scope 5 (parent: 4)
[junit] | | | | scope 6 (parent: 4)
[junit] | | | | scope 7 (parent: 4)
[junit] | | locations (start=0)
[junit] | | | location 0 (scope: 3)
[junit] | | | | when (true) n = 2; goto location 1
[junit] | | | location 1 (scope: 4)
[junit] | | | | when (!(2<n&&true||1<n&&true)&&true) x = 0.0; goto location 5
[junit] | | | | when (2<n&&true) x = 2.0; goto location 3
[junit] | | | | when (1<n&&true) x = 1.0; goto location 4
[junit] | | | location 3 (scope: 5)
[junit] | | | | when (true) ; goto location 6
[junit] | | | location 4 (scope: 6)
[junit] | | | | when (true) ; goto location 6
[junit] | | | location 5 (scope: 7)
[junit] | | | | when (true) ; goto location 6
[junit] | | | location 6 (scope: 4)
[junit] | | | | when (true) ; goto location 7
[junit] | | | location 7 (scope: 3)
[junit] | | | | when (true) return;
[junit] =================== Stats ===================
[junit]
[junit] maxProcs : 1
[junit] statesSeen : 6
[junit] statesMatched : 0
[junit] transitionsExecuted : 5
[junit] proverValidCalls : 16
[junit] CVC3ValidCalls : 2
[junit] memory (bytes) : 159121408
[junit] elapsedTime (s) : 0.004
[junit] The specified properties hold for all executions.
[junit] ------------- ---------------- ---------------
[junit] Testsuite: edu.udel.cis.vsl.civl.ExamplesTest
[junit] Tests run: 14, Failures: 0, Errors: 0, Time elapsed: 2.021 sec
[junit]
[junit] ------------- Standard Output ---------------
[junit] =================== Model ===================
[junit]
[junit] Model
[junit] | function _CIVL_system
[junit] | | formal parameters
[junit] | | scope 3 (parent: null)
[junit] | | | a : real[]
[junit] | | | scope 4 (parent: 3)
[junit] | | | | seq : real
[junit] | | | | par : real
[junit] | | locations (start=0)
[junit] | | | location 0 (scope: 4)
[junit] | | | | when (true) seq = adderSeq(n : int); goto location 1
[junit] | | | location 1 (scope: 4)
[junit] | | | | when (true) par = adderPar(m : int); goto location 2
[junit] | | | location 2 (scope: 4)
[junit] | | | | when (true) $assert seq==par; goto location 3
[junit] | | | location 3 (scope: 3)
[junit] | | | | when (true) return;
[junit] | function adderSeq
[junit] | | formal parameters
[junit] | | | n
[junit] | | scope 5 (parent: 3)
[junit] | | | n : int
[junit] | | | scope 6 (parent: 5)
[junit] | | | | s : real
[junit] | | | | scope 7 (parent: 6)
[junit] | | | | | i : int
[junit] | | | | | scope 8 (parent: 7)
[junit] | | locations (start=4)
[junit] | | | location 4 (scope: 6)
[junit] | | | | when (true) s = 0.0; goto location 5
[junit] | | | location 5 (scope: 7)
[junit] | | | | when (true) i = 0; goto location 6
[junit] | | | location 6 (scope: 8)
[junit] | | | | when (true&&i<n) s = s+a[i]; goto location 7
[junit] | | | | when (!(i<n)) ; goto location 8
[junit] | | | location 7 (scope: 7)
[junit] | | | | when (true) i = i+1; goto location 6
[junit] | | | location 8 (scope: 6)
[junit] | | | | when (true) return s;
[junit] | function adderPar
[junit] | | formal parameters
[junit] | | | m
[junit] | | scope 9 (parent: 3)
[junit] | | | m : int
[junit] | | | scope 10 (parent: 9)
[junit] | | | | s : real
[junit] | | | | mutex : int
[junit] | | | | workers : process[]
[junit] | | | | scope 11 (parent: 10)
[junit] | | | | | j : int
[junit] | | | | | scope 12 (parent: 11)
[junit] | | | | scope 13 (parent: 10)
[junit] | | | | | k : int
[junit] | | | | | scope 14 (parent: 13)
[junit] | | locations (start=9)
[junit] | | | location 9 (scope: 10)
[junit] | | | | when (true) s = 0.0; goto location 10
[junit] | | | location 10 (scope: 10)
[junit] | | | | when (true) mutex = 0; goto location 11
[junit] | | | location 11 (scope: 11)
[junit] | | | | when (true) j = 0; goto location 12
[junit] | | | location 12 (scope: 12)
[junit] | | | | when (true&&j<m) workers[j] = spawn worker(j); goto location 13
[junit] | | | | when (!(j<m)) ; goto location 14
[junit] | | | location 13 (scope: 11)
[junit] | | | | when (true) j = j+1; goto location 12
[junit] | | | location 14 (scope: 13)
[junit] | | | | when (true) k = 0; goto location 15
[junit] | | | location 15 (scope: 14)
[junit] | | | | when (true&&k<m) wait workers[k]; goto location 16
[junit] | | | | when (!(k<m)) ; goto location 17
[junit] | | | location 16 (scope: 13)
[junit] | | | | when (true) k = k+1; goto location 15
[junit] | | | location 17 (scope: 10)
[junit] | | | | when (true) return s;
[junit] | function worker
[junit] | | formal parameters
[junit] | | | i
[junit] | | scope 15 (parent: 10)
[junit] | | | i : int
[junit] | | | scope 16 (parent: 15)
[junit] | | | | t : real
[junit] | | locations (start=18)
[junit] | | | location 18 (scope: 16)
[junit] | | | | when (mutex==0) mutex = 1; goto location 19
[junit] | | | location 19 (scope: 16)
[junit] | | | | when (true) t = s; goto location 20
[junit] | | | location 20 (scope: 16)
[junit] | | | | when (true) t = t+a[i]; goto location 21
[junit] | | | location 21 (scope: 16)
[junit] | | | | when (true) s = t; goto location 22
[junit] | | | location 22 (scope: 16)
[junit] | | | | when (true) mutex = 0; goto location 23
[junit] | | | location 23 (scope: 15)
[junit] | | | | when (true) return;
[junit] =================== Stats ===================
[junit]
[junit] maxProcs : 4
[junit] statesSeen : 329
[junit] statesMatched : 115
[junit] transitionsExecuted : 443
[junit] proverValidCalls : 1955
[junit] CVC3ValidCalls : 2
[junit] memory (bytes) : 159121408
[junit] elapsedTime (s) : 0.207
[junit] The specified properties hold for all executions.
[junit] =================== Model ===================
[junit]
[junit] Model
[junit] | function _CIVL_system
[junit] | | formal parameters
[junit] | | scope 17 (parent: null)
[junit] | | | n : int
[junit] | | | x : real
[junit] | | | scope 18 (parent: 17)
[junit] | | | | scope 21 (parent: 18)
[junit] | | | | scope 20 (parent: 18)
[junit] | | | | scope 19 (parent: 18)
[junit] | | locations (start=24)
[junit] | | | location 24 (scope: 17)
[junit] | | | | when (true) n = 2; goto location 25
[junit] | | | location 25 (scope: 18)
[junit] | | | | when (!(2<n&&true||1<n&&true)&&true) x = 0.0; goto location 29
[junit] | | | | when (2<n&&true) x = 2.0; goto location 27
[junit] | | | | when (1<n&&true) x = 1.0; goto location 28
[junit] | | | location 27 (scope: 19)
[junit] | | | | when (true) ; goto location 30
[junit] | | | location 28 (scope: 20)
[junit] | | | | when (true) ; goto location 30
[junit] | | | location 29 (scope: 21)
[junit] | | | | when (true) ; goto location 30
[junit] | | | location 30 (scope: 18)
[junit] | | | | when (true) ; goto location 31
[junit] | | | location 31 (scope: 17)
[junit] | | | | when (true) return;
[junit] =================== Stats ===================
[junit]
[junit] maxProcs : 1
[junit] statesSeen : 6
[junit] statesMatched : 0
[junit] transitionsExecuted : 5
[junit] proverValidCalls : 1971
[junit] CVC3ValidCalls : 2
[junit] memory (bytes) : 159121408
[junit] elapsedTime (s) : 0.018
[junit] The specified properties hold for all executions.
[junit] =================== Model ===================
[junit]
[junit] Model
[junit] | function _CIVL_system
[junit] | | formal parameters
[junit] | | scope 22 (parent: null)
[junit] | | | nx : int
[junit] | | | u0 : real[]
[junit] | | | nsteps : int
[junit] | | | kappa : real
[junit] | | | data : real[][]
[junit] | | | u : real[]
[junit] | | | scope 23 (parent: 22)
[junit] | | | | scope 24 (parent: 23)
[junit] | | | | | iter : int
[junit] | | | | | scope 25 (parent: 24)
[junit] | | locations (start=32)
[junit] | | | location 32 (scope: 23)
[junit] | | | | when (true) init(); goto location 33
[junit] | | | location 33 (scope: 23)
[junit] | | | | when (true) write(time : int); goto location 34
[junit] | | | location 34 (scope: 24)
[junit] | | | | when (true) iter = 1; goto location 35
[junit] | | | location 35 (scope: 25)
[junit] | | | | when (true&&iter<=nsteps) update(); goto location 36
[junit] | | | | when (!(iter<=nsteps)) ; goto location 38
[junit] | | | location 36 (scope: 25)
[junit] | | | | when (true) write(time : int); goto location 37
[junit] | | | location 37 (scope: 24)
[junit] | | | | when (true) iter = iter+1; goto location 35
[junit] | | | location 38 (scope: 22)
[junit] | | | | when (true) return;
[junit] | function init
[junit] | | formal parameters
[junit] | | scope 26 (parent: 22)
[junit] | | | scope 27 (parent: 26)
[junit] | | | | scope 28 (parent: 27)
[junit] | | | | | i : int
[junit] | | | | | scope 29 (parent: 28)
[junit] | | locations (start=39)
[junit] | | | location 39 (scope: 27)
[junit] | | | | when (true) nx = 2; goto location 40
[junit] | | | location 40 (scope: 27)
[junit] | | | | when (true) nsteps = 2; goto location 41
[junit] | | | location 41 (scope: 27)
[junit] | | | | when (true) kappa = 0.1; goto location 42
[junit] | | | location 42 (scope: 28)
[junit] | | | | when (true) i = 0; goto location 43
[junit] | | | location 43 (scope: 29)
[junit] | | | | when (!(i<nx)) ; goto location 45
[junit] | | | | when (true&&i<nx) u[i] = u0[i]; goto location 44
[junit] | | | location 44 (scope: 28)
[junit] | | | | when (true) i = i+1; goto location 43
[junit] | | | location 45 (scope: 26)
[junit] | | | | when (true) return;
[junit] | function write
[junit] | | formal parameters
[junit] | | | time
[junit] | | scope 30 (parent: 22)
[junit] | | | time : int
[junit] | | | scope 31 (parent: 30)
[junit] | | | | scope 32 (parent: 31)
[junit] | | | | | i : int
[junit] | | | | | scope 33 (parent: 32)
[junit] | | locations (start=46)
[junit] | | | location 46 (scope: 32)
[junit] | | | | when (true) i = 0; goto location 47
[junit] | | | location 47 (scope: 33)
[junit] | | | | when (!(i<nx)) ; goto location 49
[junit] | | | | when (true&&i<nx) data[time][i] = u[i]; goto location 48
[junit] | | | location 48 (scope: 32)
[junit] | | | | when (true) i = i+1; goto location 47
[junit] | | | location 49 (scope: 30)
[junit] | | | | when (true) return;
[junit] | function update
[junit] | | formal parameters
[junit] | | scope 34 (parent: 22)
[junit] | | | scope 35 (parent: 34)
[junit] | | | | u_new : real[]
[junit] | | | | scope 36 (parent: 35)
[junit] | | | | | i : int
[junit] | | | | | scope 37 (parent: 36)
[junit] | | | | scope 38 (parent: 35)
[junit] | | | | | i : int
[junit] | | | | | scope 39 (parent: 38)
[junit] | | locations (start=50)
[junit] | | | location 50 (scope: 36)
[junit] | | | | when (true) i = 1; goto location 51
[junit] | | | location 51 (scope: 37)
[junit] | | | | when (true&&i<nx-1) u_new[i] = u[i]+kappa*u[i+1]+u[i-1]-2.0*u[i]; goto location 52
[junit] | | | | when (!(i<nx-1)) ; goto location 53
[junit] | | | location 52 (scope: 36)
[junit] | | | | when (true) i = i+1; goto location 51
[junit] | | | location 53 (scope: 38)
[junit] | | | | when (true) i = 1; goto location 54
[junit] | | | location 54 (scope: 39)
[junit] | | | | when (true&&i<nx-1) u[i] = u_new[i]; goto location 55
[junit] | | | | when (!(i<nx-1)) ; goto location 56
[junit] | | | location 55 (scope: 38)
[junit] | | | | when (true) i = i+1; goto location 54
[junit] | | | location 56 (scope: 34)
[junit] | | | | when (true) return;
[junit] =================== Stats ===================
[junit]
[junit] maxProcs : 1
[junit] statesSeen : 53
[junit] statesMatched : 0
[junit] transitionsExecuted : 52
[junit] proverValidCalls : 2135
[junit] CVC3ValidCalls : 2
[junit] memory (bytes) : 159121408
[junit] elapsedTime (s) : 0.053
[junit] The specified properties hold for all executions.
[junit] =================== Model ===================
[junit]
[junit] Model
[junit] | function _CIVL_system
[junit] | | formal parameters
[junit] | | scope 40 (parent: null)
[junit] | | | scope 41 (parent: 40)
[junit] | | | | scope 42 (parent: 41)
[junit] | | locations (start=57)
[junit] | | | location 57 (scope: 42)
[junit] | | | | when (true) ; goto location 58
[junit] | | | location 58 (scope: 40)
[junit] | | | | when (true) return;
[junit] =================== Stats ===================
[junit]
[junit] maxProcs : 1
[junit] statesSeen : 3
[junit] statesMatched : 0
[junit] transitionsExecuted : 2
[junit] proverValidCalls : 2139
[junit] CVC3ValidCalls : 2
[junit] memory (bytes) : 159121408
[junit] elapsedTime (s) : 0.002
[junit] The specified properties hold for all executions.
[junit] =================== Model ===================
[junit]
[junit] Model
[junit] | function _CIVL_system
[junit] | | formal parameters
[junit] | | scope 43 (parent: null)
[junit] | | | scope 44 (parent: 43)
[junit] | | | | i : int
[junit] | | | | j : real
[junit] | | locations (start=59)
[junit] | | | location 59 (scope: 44)
[junit] | | | | when (true) i = 0; goto location 60
[junit] | | | location 60 (scope: 44)
[junit] | | | | when (true) j = (real) i; goto location 61
[junit] | | | location 61 (scope: 44)
[junit] | | | | when (true) $assert j==0.0; goto location 62
[junit] | | | location 62 (scope: 43)
[junit] | | | | when (true) return;
[junit] =================== Stats ===================
[junit]
[junit] maxProcs : 1
[junit] statesSeen : 5
[junit] statesMatched : 0
[junit] transitionsExecuted : 4
[junit] proverValidCalls : 2148
[junit] CVC3ValidCalls : 2
[junit] memory (bytes) : 159121408
[junit] elapsedTime (s) : 0.014
[junit] The specified properties hold for all executions.
[junit] =================== Model ===================
[junit]
[junit] Model
[junit] | function _CIVL_system
[junit] | | formal parameters
[junit] | | scope 45 (parent: null)
[junit] | | | scope 46 (parent: 45)
[junit] | | | | a : int
[junit] | | | | b : int
[junit] | | | | c : int
[junit] | | | | scope 48 (parent: 46)
[junit] | | | | scope 47 (parent: 46)
[junit] | | | | scope 49 (parent: 46)
[junit] | | | | scope 50 (parent: 46)
[junit] | | locations (start=63)
[junit] | | | location 63 (scope: 47)
[junit] | | | | when (true) c = 0; goto location 64
[junit] | | | location 64 (scope: 47)
[junit] | | | | when (true) b = c; goto location 65
[junit] | | | location 65 (scope: 47)
[junit] | | | | when (true) a = b; goto location 66
[junit] | | | location 66 (scope: 46)
[junit] | | | | when (true) b = b+1; goto location 67
[junit] | | | location 67 (scope: 48)
[junit] | | | | when (true) b = b+1; goto location 68
[junit] | | | location 68 (scope: 48)
[junit] | | | | when (true) a = b; goto location 69
[junit] | | | location 69 (scope: 49)
[junit] | | | | when (true) c = a; goto location 70
[junit] | | | location 70 (scope: 49)
[junit] | | | | when (true) a = a-1; goto location 71
[junit] | | | location 71 (scope: 50)
[junit] | | | | when (true) b = c; goto location 72
[junit] | | | location 72 (scope: 50)
[junit] | | | | when (true) c = c+1; goto location 73
[junit] | | | location 73 (scope: 46)
[junit] | | | | when (true) $assert a==1; goto location 74
[junit] | | | location 74 (scope: 46)
[junit] | | | | when (true) $assert b==2; goto location 75
[junit] | | | location 75 (scope: 46)
[junit] | | | | when (true) $assert c==3; goto location 76
[junit] | | | location 76 (scope: 45)
[junit] | | | | when (true) return;
[junit] =================== Stats ===================
[junit]
[junit] maxProcs : 1
[junit] statesSeen : 15
[junit] statesMatched : 0
[junit] transitionsExecuted : 14
[junit] proverValidCalls : 2179
[junit] CVC3ValidCalls : 2
[junit] memory (bytes) : 159121408
[junit] elapsedTime (s) : 0.019
[junit] The specified properties hold for all executions.
[junit] =================== Model ===================
[junit]
[junit] Model
[junit] | function _CIVL_system
[junit] | | formal parameters
[junit] | | scope 51 (parent: null)
[junit] | | | scope 52 (parent: 51)
[junit] | | | | p : process
[junit] | | | | q : process
[junit] | | locations (start=77)
[junit] | | | location 77 (scope: 52)
[junit] | | | | when (true) p = spawn f(3); goto location 78
[junit] | | | location 78 (scope: 52)
[junit] | | | | when (true) q = spawn f(1000); goto location 79
[junit] | | | location 79 (scope: 52)
[junit] | | | | when (true) wait p; goto location 80
[junit] | | | location 80 (scope: 52)
[junit] | | | | when (true) wait q; goto location 81
[junit] | | | location 81 (scope: 51)
[junit] | | | | when (true) return;
[junit] | function f
[junit] | | formal parameters
[junit] | | | n
[junit] | | scope 53 (parent: 51)
[junit] | | | n : int
[junit] | | | scope 54 (parent: 53)
[junit] | | | | scope 55 (parent: 54)
[junit] | | | | | i : int
[junit] | | locations (start=82)
[junit] | | | location 82 (scope: 55)
[junit] | | | | when (true) i = 0; goto location 83
[junit] | | | location 83 (scope: 55)
[junit] | | | | when (!(i<n)) ; goto location 85
[junit] | | | | when (true&&i<n) ; goto location 84
[junit] | | | location 84 (scope: 55)
[junit] | | | | when (true) i = i+1; goto location 83
[junit] | | | location 85 (scope: 53)
[junit] | | | | when (true) return;
[junit] =================== Stats ===================
[junit]
[junit] maxProcs : 3
[junit] statesSeen : 2018
[junit] statesMatched : 0
[junit] transitionsExecuted : 2017
[junit] proverValidCalls : 13252
[junit] CVC3ValidCalls : 2
[junit] memory (bytes) : 159121408
[junit] elapsedTime (s) : 0.391
[junit] The specified properties hold for all executions.
[junit] =================== Model ===================
[junit]
[junit] Model
[junit] | function _CIVL_system
[junit] | | formal parameters
[junit] | | scope 56 (parent: null)
[junit] | | | scope 57 (parent: 56)
[junit] | | locations (start=86)
[junit] | | | location 86 (scope: 57)
[junit] | | | | when (true) ; goto location 87
[junit] | | | location 87 (scope: 56)
[junit] | | | | when (true) return;
[junit] =================== Stats ===================
[junit]
[junit] maxProcs : 1
[junit] statesSeen : 3
[junit] statesMatched : 0
[junit] transitionsExecuted : 2
[junit] proverValidCalls : 13256
[junit] CVC3ValidCalls : 2
[junit] memory (bytes) : 159121408
[junit] elapsedTime (s) : 0.001
[junit] The specified properties hold for all executions.
[junit] =================== Model ===================
[junit]
[junit] Model
[junit] | function _CIVL_system
[junit] | | formal parameters
[junit] | | scope 58 (parent: null)
[junit] | | | scope 59 (parent: 58)
[junit] | | | | a : int
[junit] | | | | b : int*
[junit] | | | | c : int[]
[junit] | | | | d : int*
[junit] | | | | g : int**
[junit] | | | | f : int*
[junit] | | locations (start=88)
[junit] | | | location 88 (scope: 59)
[junit] | | | | when (true) f = &(a); goto location 89
[junit] | | | location 89 (scope: 59)
[junit] | | | | when (true) a = 1; goto location 90
[junit] | | | location 90 (scope: 59)
[junit] | | | | when (true) b = &(a); goto location 91
[junit] | | | location 91 (scope: 59)
[junit] | | | | when (true) c[0] = 0; goto location 92
[junit] | | | location 92 (scope: 59)
[junit] | | | | when (true) c[1] = 1; goto location 93
[junit] | | | location 93 (scope: 59)
[junit] | | | | when (true) d = &(c[1]); goto location 94
[junit] | | | location 94 (scope: 59)
[junit] | | | | when (true) g = &(d); goto location 95
[junit] | | | location 95 (scope: 59)
[junit] | | | | when (true) $assert *(b)==1; goto location 96
[junit] | | | location 96 (scope: 59)
[junit] | | | | when (true) $assert *(d)==1; goto location 97
[junit] | | | location 97 (scope: 59)
[junit] | | | | when (true) $assert *(*(g))==1; goto location 98
[junit] | | | location 98 (scope: 59)
[junit] | | | | when (true) $assert g==&(d); goto location 99
[junit] | | | location 99 (scope: 59)
[junit] | | | | when (true) passByRef(array : int*); goto location 100
[junit] | | | location 100 (scope: 59)
[junit] | | | | when (true) $assert *(f)==42; goto location 101
[junit] | | | location 101 (scope: 58)
[junit] | | | | when (true) return;
[junit] | function passByRef
[junit] | | formal parameters
[junit] | | | array
[junit] | | scope 60 (parent: 58)
[junit] | | | array : int*
[junit] | | | scope 61 (parent: 60)
[junit] | | locations (start=102)
[junit] | | | location 102 (scope: 61)
[junit] | | | | when (true) *(array) = 42; goto location 103
[junit] | | | location 103 (scope: 60)
[junit] | | | | when (true) return;
[junit] =================== Stats ===================
[junit]
[junit] maxProcs : 1
[junit] statesSeen : 17
[junit] statesMatched : 0
[junit] transitionsExecuted : 16
[junit] proverValidCalls : 13293
[junit] CVC3ValidCalls : 2
[junit] memory (bytes) : 159121408
[junit] elapsedTime (s) : 0.029
[junit] The specified properties hold for all executions.
[junit] =================== Model ===================
[junit]
[junit] Model
[junit] | function _CIVL_system
[junit] | | formal parameters
[junit] | | scope 62 (parent: null)
[junit] | | | x : int
[junit] | | | y : int
[junit] | | | scope 63 (parent: 62)
[junit] | | | | p : process
[junit] | | | | q : process
[junit] | | locations (start=104)
[junit] | | | location 104 (scope: 63)
[junit] | | | | when (true) x = 0; goto location 105
[junit] | | | location 105 (scope: 63)
[junit] | | | | when (true) y = 0; goto location 106
[junit] | | | location 106 (scope: 63)
[junit] | | | | when (true) p = spawn f(10); goto location 107
[junit] | | | location 107 (scope: 63)
[junit] | | | | when (true) q = spawn g(10); goto location 108
[junit] | | | location 108 (scope: 63)
[junit] | | | | when (true) wait p; goto location 109
[junit] | | | location 109 (scope: 63)
[junit] | | | | when (true) wait q; goto location 110
[junit] | | | location 110 (scope: 62)
[junit] | | | | when (true) return;
[junit] | function f
[junit] | | formal parameters
[junit] | | | n
[junit] | | scope 64 (parent: 62)
[junit] | | | n : int
[junit] | | | scope 65 (parent: 64)
[junit] | | | | scope 66 (parent: 65)
[junit] | | | | | i : int
[junit] | | | | | scope 67 (parent: 66)
[junit] | | locations (start=111)
[junit] | | | location 111 (scope: 66)
[junit] | | | | when (true) i = 0; goto location 112
[junit] | | | location 112 (scope: 67)
[junit] | | | | when (!(i<n)) ; goto location 117
[junit] | | | | when (x==0&&i<n) x = 1; goto location 113
[junit] | | | location 113 (scope: 67)
[junit] | | | | when (y==0) y = 1; goto location 114
[junit] | | | location 114 (scope: 67)
[junit] | | | | when (true) y = 0; goto location 115
[junit] | | | location 115 (scope: 67)
[junit] | | | | when (true) x = 0; goto location 116
[junit] | | | location 116 (scope: 66)
[junit] | | | | when (true) i = i+1; goto location 112
[junit] | | | location 117 (scope: 64)
[junit] | | | | when (true) return;
[junit] | function g
[junit] | | formal parameters
[junit] | | | m
[junit] | | scope 68 (parent: 62)
[junit] | | | m : int
[junit] | | | scope 69 (parent: 68)
[junit] | | | | scope 70 (parent: 69)
[junit] | | | | | i : int
[junit] | | | | | scope 71 (parent: 70)
[junit] | | locations (start=118)
[junit] | | | location 118 (scope: 70)
[junit] | | | | when (true) i = 0; goto location 119
[junit] | | | location 119 (scope: 71)
[junit] | | | | when (!(i<m)) ; goto location 124
[junit] | | | | when (y==0&&i<m) y = 1; goto location 120
[junit] | | | location 120 (scope: 71)
[junit] | | | | when (x==0) x = 1; goto location 121
[junit] | | | location 121 (scope: 71)
[junit] | | | | when (true) x = 0; goto location 122
[junit] | | | location 122 (scope: 71)
[junit] | | | | when (true) y = 0; goto location 123
[junit] | | | location 123 (scope: 70)
[junit] | | | | when (true) i = i+1; goto location 119
[junit] | | | location 124 (scope: 68)
[junit] | | | | when (true) return;
[junit] A deadlock is possible:
[junit] *****************************************************************
[junit] Deadlock possible at State 250(nprocs=3, nscopes=10)!
[junit] Deadlock possible at State 250(nprocs=3, nscopes=10)!
[junit] *****************************************************************
[junit] Process 0: at location 108. Target process has not terminated:
[junit] p
[junit] Process 1: at location 113. Cannot prove enabling statement valid:
[junit] false
[junit] Process 2: at location 120. 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=63)
[junit] | | | reachers: 0
[junit] | | | p = PID_1
[junit] | | | q = PID_2
[junit] | | scope 1 (parent=-1, static=62)
[junit] | | | reachers: 0,1,2
[junit] | | | x = 1
[junit] | | | y = 1
[junit] | | scope 2 (parent=3, static=67)
[junit] | | | reachers: 1
[junit] | | scope 3 (parent=4, static=66)
[junit] | | | reachers: 1
[junit] | | | i = 9
[junit] | | scope 4 (parent=5, static=65)
[junit] | | | reachers: 1
[junit] | | scope 5 (parent=1, static=64)
[junit] | | | reachers: 1
[junit] | | | n = 10
[junit] | | scope 6 (parent=7, static=71)
[junit] | | | reachers: 2
[junit] | | scope 7 (parent=8, static=70)
[junit] | | | reachers: 2
[junit] | | | i = 0
[junit] | | scope 8 (parent=9, static=69)
[junit] | | | reachers: 2
[junit] | | scope 9 (parent=1, static=68)
[junit] | | | reachers: 2
[junit] | | | m = 10
[junit] | Process states
[junit] | | process 0 call stack
[junit] | | | Frame[function=_CIVL_system, location=108, scope=0]
[junit] | | process 1 call stack
[junit] | | | Frame[function=f, location=113, scope=2]
[junit] | | process 2 call stack
[junit] | | | Frame[function=g, location=120, scope=6]
[junit] =================== Stats ===================
[junit]
[junit] maxProcs : 3
[junit] statesSeen : 251
[junit] statesMatched : 42
[junit] transitionsExecuted : 292
[junit] proverValidCalls : 14716
[junit] CVC3ValidCalls : 2
[junit] memory (bytes) : 159121408
[junit] elapsedTime (s) : 0.059
[junit] The program MAY NOT be correct.
[junit] =================== Model ===================
[junit]
[junit] Model
[junit] | function _CIVL_system
[junit] | | formal parameters
[junit] | | scope 72 (parent: null)
[junit] | | | L : int
[junit] | | | M : int
[junit] | | | N : int
[junit] | | | TILE_SIZE : int
[junit] | | | A : real[][]
[junit] | | | B : real[][]
[junit] | | | C : real[][]
[junit] | | | D : real[][]
[junit] | | | scope 73 (parent: 72)
[junit] | | | | scope 74 (parent: 73)
[junit] | | | | | i : int
[junit] | | | | | scope 75 (parent: 74)
[junit] | | | | | | scope 76 (parent: 75)
[junit] | | | | | | | j : int
[junit] | | | | | | | scope 77 (parent: 76)
[junit] | | locations (start=125)
[junit] | | | location 125 (scope: 72)
[junit] | | | | when (true) L = 5; goto location 126
[junit] | | | location 126 (scope: 72)
[junit] | | | | when (true) M = 6; goto location 127
[junit] | | | location 127 (scope: 72)
[junit] | | | | when (true) N = 7; goto location 128
[junit] | | | location 128 (scope: 72)
[junit] | | | | when (true) TILE_SIZE = 3; goto location 129
[junit] | | | location 129 (scope: 73)
[junit] | | | | when (true) spec(); goto location 130
[junit] | | | location 130 (scope: 73)
[junit] | | | | when (true) rowdist(); goto location 131
[junit] | | | location 131 (scope: 74)
[junit] | | | | when (true) i = 0; goto location 132
[junit] | | | location 132 (scope: 76)
[junit] | | | | when (!(i<L)) ; goto location 136
[junit] | | | | when (true&&i<L) j = 0; goto location 133
[junit] | | | location 133 (scope: 77)
[junit] | | | | when (!(j<N)) ; goto location 135
[junit] | | | | when (true&&j<N) $assert C[i][j]==D[i][j]; goto location 134
[junit] | | | location 134 (scope: 76)
[junit] | | | | when (true) j = j+1; goto location 133
[junit] | | | location 135 (scope: 74)
[junit] | | | | when (true) i = i+1; goto location 132
[junit] | | | location 136 (scope: 72)
[junit] | | | | when (true) return;
[junit] | function spec
[junit] | | formal parameters
[junit] | | scope 78 (parent: 72)
[junit] | | | scope 79 (parent: 78)
[junit] | | | | scope 80 (parent: 79)
[junit] | | | | | i : int
[junit] | | | | | scope 81 (parent: 80)
[junit] | | | | | | j : int
[junit] | | | | | | scope 82 (parent: 81)
[junit] | | | | | | | scope 83 (parent: 82)
[junit] | | | | | | | | k : int
[junit] | | locations (start=137)
[junit] | | | location 137 (scope: 80)
[junit] | | | | when (true) i = 0; goto location 138
[junit] | | | location 138 (scope: 81)
[junit] | | | | when (!(i<L)) ; goto location 145
[junit] | | | | when (true&&i<L) j = 0; goto location 139
[junit] | | | location 139 (scope: 82)
[junit] | | | | when (true&&j<N) C[i][j] = 0.0; goto location 140
[junit] | | | | when (!(j<N)) ; goto location 144
[junit] | | | location 140 (scope: 83)
[junit] | | | | when (true) k = 0; goto location 141
[junit] | | | location 141 (scope: 83)
[junit] | | | | when (!(k<M)) ; goto location 143
[junit] | | | | when (true&&k<M) C[i][j] = C[i][j]+A[i][k]*B[k][j]; goto location 142
[junit] | | | location 142 (scope: 83)
[junit] | | | | when (true) k = k+1; goto location 141
[junit] | | | location 143 (scope: 81)
[junit] | | | | when (true) j = j+1; goto location 139
[junit] | | | location 144 (scope: 80)
[junit] | | | | when (true) i = i+1; goto location 138
[junit] | | | location 145 (scope: 78)
[junit] | | | | when (true) return;
[junit] | function rowdist
[junit] | | formal parameters
[junit] | | scope 84 (parent: 72)
[junit] | | | scope 85 (parent: 84)
[junit] | | | | hi1 : int
[junit] | | | | hi2 : int
[junit] | | | | hi3 : int
[junit] | | | | scope 86 (parent: 85)
[junit] | | | | | i : int
[junit] | | | | | scope 87 (parent: 86)
[junit] | | | | | | scope 88 (parent: 87)
[junit] | | | | | | | j : int
[junit] | | | | | | | scope 89 (parent: 88)
[junit] | | | | scope 90 (parent: 85)
[junit] | | | | | ii : int
[junit] | | | | | scope 91 (parent: 90)
[junit] | | | | | | scope 92 (parent: 91)
[junit] | | | | | | | jj : int
[junit] | | | | | | | scope 93 (parent: 92)
[junit] | | | | | | | | scope 94 (parent: 93)
[junit] | | | | | | | | | kk : int
[junit] | | | | | | | | | scope 95 (parent: 94)
[junit] | | | | | | | | | | scope 96 (parent: 95)
[junit] | | | | | | | | | | | i : int
[junit] | | | | | | | | | | | scope 97 (parent: 96)
[junit] | | | | | | | | | | | | scope 98 (parent: 97)
[junit] | | | | | | | | | | | | | j : int
[junit] | | | | | | | | | | | | | scope 99 (parent: 98)
[junit] | | | | | | | | | | | | | | scope 100 (parent: 99)
[junit] | | | | | | | | | | | | | | | k : int
[junit] | | locations (start=146)
[junit] | | | location 146 (scope: 86)
[junit] | | | | when (true) i = 0; goto location 147
[junit] | | | location 147 (scope: 88)
[junit] | | | | when (!(i<L)) ; goto location 151
[junit] | | | | when (true&&i<L) j = 0; goto location 148
[junit] | | | location 148 (scope: 89)
[junit] | | | | when (true&&j<N) D[i][j] = 0.0; goto location 149
[junit] | | | | when (!(j<N)) ; goto location 150
[junit] | | | location 149 (scope: 88)
[junit] | | | | when (true) j = j+1; goto location 148
[junit] | | | location 150 (scope: 86)
[junit] | | | | when (true) i = i+1; goto location 147
[junit] | | | location 151 (scope: 90)
[junit] | | | | when (true) ii = 0; goto location 152
[junit] | | | location 152 (scope: 92)
[junit] | | | | when (!(ii<L)) ; goto location 167
[junit] | | | | when (true&&ii<L) jj = 0; goto location 153
[junit] | | | location 153 (scope: 94)
[junit] | | | | when (true&&jj<N) kk = 0; goto location 154
[junit] | | | | when (!(jj<N)) ; goto location 166
[junit] | | | location 154 (scope: 95)
[junit] | | | | when (!(kk<M)) ; goto location 165
[junit] | | | | when (true&&kk<M) hi1 = (ii+TILE_SIZE<L ? ii+TILE_SIZE : L); goto location 155
[junit] | | | location 155 (scope: 96)
[junit] | | | | when (true) i = ii; goto location 156
[junit] | | | location 156 (scope: 97)
[junit] | | | | when (true&&i<hi1) hi2 = (jj+TILE_SIZE<N ? jj+TILE_SIZE : N); goto location 157
[junit] | | | | when (!(i<hi1)) ; goto location 164
[junit] | | | location 157 (scope: 98)
[junit] | | | | when (true) j = jj; goto location 158
[junit] | | | location 158 (scope: 99)
[junit] | | | | when (!(j<hi2)) ; goto location 163
[junit] | | | | when (true&&j<hi2) hi3 = (kk+TILE_SIZE<M ? kk+TILE_SIZE : M); goto location 159
[junit] | | | location 159 (scope: 100)
[junit] | | | | when (true) k = kk; goto location 160
[junit] | | | location 160 (scope: 100)
[junit] | | | | when (true&&k<hi3) D[i][j] = D[i][j]+A[i][k]*B[k][j]; goto location 161
[junit] | | | | when (!(k<hi3)) ; goto location 162
[junit] | | | location 161 (scope: 100)
[junit] | | | | when (true) k = k+1; goto location 160
[junit] | | | location 162 (scope: 98)
[junit] | | | | when (true) j = j+1; goto location 158
[junit] | | | location 163 (scope: 96)
[junit] | | | | when (true) i = i+1; goto location 156
[junit] | | | location 164 (scope: 94)
[junit] | | | | when (true) kk = kk+TILE_SIZE; goto location 154
[junit] | | | location 165 (scope: 92)
[junit] | | | | when (true) jj = jj+TILE_SIZE; goto location 153
[junit] | | | location 166 (scope: 90)
[junit] | | | | when (true) ii = ii+TILE_SIZE; goto location 152
[junit] | | | location 167 (scope: 84)
[junit] | | | | when (true) return;
[junit] =================== Stats ===================
[junit]
[junit] maxProcs : 1
[junit] statesSeen : 1655
[junit] statesMatched : 0
[junit] transitionsExecuted : 1654
[junit] proverValidCalls : 20339
[junit] CVC3ValidCalls : 2
[junit] memory (bytes) : 358481920
[junit] elapsedTime (s) : 1.162
[junit] The specified properties hold for all executions.
[junit] =================== Model ===================
[junit]
[junit] Model
[junit] | function _CIVL_system
[junit] | | formal parameters
[junit] | | scope 101 (parent: null)
[junit] | | | scope 102 (parent: 101)
[junit] | | | | i : int
[junit] | | | | j : int
[junit] | | | | scope 103 (parent: 102)
[junit] | | | | scope 104 (parent: 102)
[junit] | | locations (start=168)
[junit] | | | location 168 (scope: 102)
[junit] | | | | when (true) j = 0; goto location 169
[junit] | | | location 169 (scope: 103)
[junit] | | | | when (true) i = 0; goto location 170
[junit] | | | location 170 (scope: 103)
[junit] | | | | when (!(i<10)) ; goto location 172
[junit] | | | | when (true&&i<10) ; goto location 171
[junit] | | | location 171 (scope: 103)
[junit] | | | | when (true) i = i+1; goto location 170
[junit] | | | location 172 (scope: 104)
[junit] | | | | when (true&&j<10) ; goto location 173
[junit] | | | | when (!(j<10)) ; goto location 174
[junit] | | | location 173 (scope: 104)
[junit] | | | | when (true) j = j+1; goto location 172
[junit] | | | location 174 (scope: 101)
[junit] | | | | when (true) return;
[junit] =================== Stats ===================
[junit]
[junit] maxProcs : 1
[junit] statesSeen : 46
[junit] statesMatched : 0
[junit] transitionsExecuted : 45
[junit] proverValidCalls : 20486
[junit] CVC3ValidCalls : 2
[junit] memory (bytes) : 358481920
[junit] elapsedTime (s) : 0.01
[junit] The specified properties hold for all executions.
[junit] =================== Model ===================
[junit]
[junit] Model
[junit] | function _CIVL_system
[junit] | | formal parameters
[junit] | | scope 105 (parent: null)
[junit] | | | scope 106 (parent: 105)
[junit] | | locations (start=175)
[junit] | | | location 175 (scope: 106)
[junit] | | | | when (true) $assert 0.0<1.0; goto location 176
[junit] | | | location 176 (scope: 106)
[junit] | | | | when (true) $assert 0<1; goto location 177
[junit] | | | location 177 (scope: 106)
[junit] | | | | when (true) $assert 5.0<=5.1; goto location 178
[junit] | | | location 178 (scope: 106)
[junit] | | | | when (true) $assert 5<=5; goto location 179
[junit] | | | location 179 (scope: 105)
[junit] | | | | when (true) return;
[junit] =================== Stats ===================
[junit]
[junit] maxProcs : 1
[junit] statesSeen : 6
[junit] statesMatched : 0
[junit] transitionsExecuted : 5
[junit] proverValidCalls : 20500
[junit] CVC3ValidCalls : 2
[junit] memory (bytes) : 358481920
[junit] elapsedTime (s) : 0.012
[junit] The specified properties hold for all executions.
[junit] =================== Model ===================
[junit]
[junit] Model
[junit] | function _CIVL_system
[junit] | | formal parameters
[junit] | | scope 107 (parent: null)
[junit] | | | scope 108 (parent: 107)
[junit] | | | | a : int[][]
[junit] | | | | b : int[]
[junit] | | locations (start=180)
[junit] | | | location 180 (scope: 108)
[junit] | | | | when (true) a[0][0] = 2; goto location 181
[junit] | | | location 181 (scope: 108)
[junit] | | | | when (true) b[1] = 5; goto location 182
[junit] | | | location 182 (scope: 108)
[junit] | | | | when (true) $assert a[0][0]==2; goto location 183
[junit] | | | location 183 (scope: 108)
[junit] | | | | when (true) $assert b[1]==5; goto location 184
[junit] | | | location 184 (scope: 107)
[junit] | | | | when (true) return;
[junit] =================== Stats ===================
[junit]
[junit] maxProcs : 1
[junit] statesSeen : 6
[junit] statesMatched : 0
[junit] transitionsExecuted : 5
[junit] proverValidCalls : 20512
[junit] CVC3ValidCalls : 2
[junit] memory (bytes) : 358481920
[junit] elapsedTime (s) : 0.012
[junit] The specified properties hold for all executions.
[junit] ------------- ---------------- ---------------
[junit] Testsuite: edu.udel.cis.vsl.civl.PointersTest
[junit] Tests run: 1, Failures: 0, Errors: 0, Time elapsed: 0.026 sec
[junit]
[junit] ------------- Standard Output ---------------
[junit] =================== Model ===================
[junit]
[junit] Model
[junit] | function _CIVL_system
[junit] | | formal parameters
[junit] | | scope 3 (parent: null)
[junit] | | | scope 4 (parent: 3)
[junit] | | | | a : int
[junit] | | | | b : int*
[junit] | | | | c : int[]
[junit] | | | | d : int*
[junit] | | | | g : int**
[junit] | | | | f : int*
[junit] | | locations (start=0)
[junit] | | | location 0 (scope: 4)
[junit] | | | | when (true) f = &(a); goto location 1
[junit] | | | location 1 (scope: 4)
[junit] | | | | when (true) a = 1; goto location 2
[junit] | | | location 2 (scope: 4)
[junit] | | | | when (true) b = &(a); goto location 3
[junit] | | | location 3 (scope: 4)
[junit] | | | | when (true) c[0] = 0; goto location 4
[junit] | | | location 4 (scope: 4)
[junit] | | | | when (true) c[1] = 1; goto location 5
[junit] | | | location 5 (scope: 4)
[junit] | | | | when (true) d = &(c[1]); goto location 6
[junit] | | | location 6 (scope: 4)
[junit] | | | | when (true) g = &(d); goto location 7
[junit] | | | location 7 (scope: 4)
[junit] | | | | when (true) $assert *(b)==1; goto location 8
[junit] | | | location 8 (scope: 4)
[junit] | | | | when (true) $assert *(d)==1; goto location 9
[junit] | | | location 9 (scope: 4)
[junit] | | | | when (true) $assert *(*(g))==1; goto location 10
[junit] | | | location 10 (scope: 4)
[junit] | | | | when (true) $assert g==&(d); goto location 11
[junit] | | | location 11 (scope: 4)
[junit] | | | | when (true) passByRef(array : int*); goto location 12
[junit] | | | location 12 (scope: 4)
[junit] | | | | when (true) $assert *(f)==42; goto location 13
[junit] | | | location 13 (scope: 3)
[junit] | | | | when (true) return;
[junit] | function passByRef
[junit] | | formal parameters
[junit] | | | array
[junit] | | scope 5 (parent: 3)
[junit] | | | array : int*
[junit] | | | scope 6 (parent: 5)
[junit] | | locations (start=14)
[junit] | | | location 14 (scope: 6)
[junit] | | | | when (true) *(array) = 42; goto location 15
[junit] | | | location 15 (scope: 5)
[junit] | | | | when (true) return;
[junit] =================== Stats ===================
[junit]
[junit] maxProcs : 1
[junit] statesSeen : 17
[junit] statesMatched : 0
[junit] transitionsExecuted : 16
[junit] proverValidCalls : 37
[junit] CVC3ValidCalls : 1
[junit] memory (bytes) : 358481920
[junit] elapsedTime (s) : 0.004
[junit] The specified properties hold for all executions.
[junit] ------------- ---------------- ---------------
[junitreport] Processing /Users/tester/work/civl/0.1/r93/junit/data/TESTS-TestSuites.xml to /var/folders/tb/t0f_d_29043c_qts86hdnb1h0000gt/T/null521993748
[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: 385ms
[junitreport] Deleting: /var/folders/tb/t0f_d_29043c_qts86hdnb1h0000gt/T/null521993748
test:
[jacoco:report] Loading execution data file /Users/tester/work/civl/0.1/r93/jacoco.exec
[jacoco:report] Writing group "Test Coverage Report for CIVL 0.1 r93" with 78 classes
javadoc:
[mkdir] Created dir: /Users/tester/work/civl/0.1/r93/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.1/r93/src/edu/udel/cis/vsl/civl/model/IF/ModelFactory.java:251: warning - @param argument "expresssion" is not a parameter name.
[javadoc] /Users/tester/work/civl/0.1/r93/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.1/r93/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.1/r93/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.1/r93/src/edu/udel/cis/vsl/civl/model/common/CommonModelFactory.java:384: warning - @param argument "expresssion" is not a parameter name.
[javadoc] /Users/tester/work/civl/0.1/r93/src/edu/udel/cis/vsl/civl/model/common/CommonScope.java:133: warning - @param argument "A" is not a parameter name.
[javadoc] /Users/tester/work/civl/0.1/r93/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.1/r93/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.1/r93/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.1/r93/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.1/r93/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.1/r93/src/edu/udel/cis/vsl/civl/semantics/Evaluator.java:478: warning - @return tag has no arguments.
[javadoc] /Users/tester/work/civl/0.1/r93/src/edu/udel/cis/vsl/civl/semantics/Executor.java:634: warning - @return tag has no arguments.
[javadoc] /Users/tester/work/civl/0.1/r93/src/edu/udel/cis/vsl/civl/semantics/Executor.java:87: warning - @param argument "prover" is not a parameter name.
[javadoc] /Users/tester/work/civl/0.1/r93/src/edu/udel/cis/vsl/civl/semantics/Executor.java:115: warning - @param argument "prover" is not a parameter name.
[javadoc] /Users/tester/work/civl/0.1/r93/src/edu/udel/cis/vsl/civl/semantics/Executor.java:443: warning - @param argument "State" is not a parameter name.
[javadoc] /Users/tester/work/civl/0.1/r93/src/edu/udel/cis/vsl/civl/state/State.java:190: warning - @return tag has no arguments.
[javadoc] /Users/tester/work/civl/0.1/r93/src/edu/udel/cis/vsl/civl/state/State.java:199: warning - @return tag has no arguments.
[javadoc] /Users/tester/work/civl/0.1/r93/src/edu/udel/cis/vsl/civl/state/StateFactory.java:630: warning - @return tag has no arguments.
[javadoc] /Users/tester/work/civl/0.1/r93/src/edu/udel/cis/vsl/civl/state/StateFactory.java:540: warning - @return tag has no arguments.
[javadoc] /Users/tester/work/civl/0.1/r93/src/edu/udel/cis/vsl/civl/state/StateFactory.java:409: warning - @param argument "scopeID" is not a parameter name.
[javadoc] /Users/tester/work/civl/0.1/r93/src/edu/udel/cis/vsl/civl/state/StateFactory.java:794: warning - @param argument "process" is not a parameter name.
[javadoc] /Users/tester/work/civl/0.1/r93/src/edu/udel/cis/vsl/civl/state/StateFactory.java:794: warning - @param argument "location" is not a parameter name.
[javadoc] /Users/tester/work/civl/0.1/r93/src/edu/udel/cis/vsl/civl/state/StateFactory.java:794: warning - @param argument "lexicalScope" is not a parameter name.
[javadoc] /Users/tester/work/civl/0.1/r93/src/edu/udel/cis/vsl/civl/state/StateFactory.java:794: warning - @param argument "parentScope" is not a parameter name.
[javadoc] /Users/tester/work/civl/0.1/r93/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.1/r93/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.1/r93/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.1/r93/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.1/r93/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] Building index for all classes...
[javadoc] javadoc: error - Error while reading file /Users/tester/work/civl/0.1/r93/src/overview.html
[javadoc] Generating /Users/tester/work/civl/0.1/r93/doc/javadoc/help-doc.html...
[javadoc] 1 error
[javadoc] 30 warnings
all:
BUILD SUCCESSFUL
Total time: 16 seconds
Stderr: