Skip to content

Instantly share code, notes, and snippets.

@martinschaef

martinschaef/SatBranches_copyprop.cfg

Created January 1, 2017 01:34
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save martinschaef/510f55e08e64898db26cdeb8d8c88870 to your computer and use it in GitHub Desktop.
Save martinschaef/510f55e08e64898db26cdeb8d8c88870 to your computer and use it in GitHub Desktop.
Download ZIP
Copy Propagator issue
Raw
SatBranches_copyprop.cfg
$StaticFields_SatBranches $Global_SatBranches;
int $float37;
int $double40;
Method <A: void <init>()>($in_0)
Return types: java.lang.Throwable, int
Returns: java.lang.Throwable $ex_, int $co_1
locals:
r0: A
Block0:
(ln 3) push_1(A, $in_0, [$co_1])
return
Root ->Block1:
(ln -1) $this_ := $in_0
(ln -1) $ex_ := $null$
(ln 2) r0 := $in_0
(ln 3) $ex_ := call <java.lang.Object: void <init>()>($in_0)
(ln 2) $co_1 := 0
goto:
Block0
Method <A: void setI(int)>($in_0, $in_1)
Return types: java.lang.Throwable
Returns: java.lang.Throwable $ex_
locals:
r0: A
i0: int
r0_i_00: int
Block0:
(ln 7) push_2(A, $in_0, [$in_1])
return
Root ->Block1:
(ln -1) $this_ := $in_0
(ln -1) $ex_ := $null$
(ln 6) r0 := $in_0
(ln 7) r0_i_00 := pull(A, $in_0)[1]
(ln 6) i0 := $in_1
(ln 7) r0_i_00 := $in_1
goto:
Block0
Method <JayHornAssertions: void <clinit>()>()
Return types: java.lang.Throwable
Returns: java.lang.Throwable $ex_
Block0:
return
Root ->Block1:
(ln -1) $ex_ := $null$
(ln -1) $ex_ := $null$
goto:
Block0
Method <SatBranches: void <clinit>()>()
Return types: java.lang.Throwable
Returns: java.lang.Throwable $ex_
locals:
SatBranches_$assertionsDisabled0: boolean
Block0:
return
Root ->Block1:
(ln -1) $ex_ := $null$
(ln 14) SatBranches_$assertionsDisabled0 := false
(ln 14) push_4($StaticFields_SatBranches, $Global_SatBranches, [SatBranches_$assertionsDisabled0])
goto:
Block0
Method <SatBranches: void main(JayArray_java_lang_String)>($in_0)
Return types: java.lang.Throwable
Returns: java.lang.Throwable $ex_
locals:
r0: JayArray_java_lang_String
$r3: java.util.Random
$i1: int
$r4: A
$i0: int
$z0: boolean
$r3_seed_3540: java.util.concurrent.atomic.AtomicLong
$r3_nextNextGaussian_01: int
$r3_haveNextNextGaussian_02: boolean
$r4_i_03: int
Block0:
return
Root ->Block1:
(ln 17) assume (JayArray_java_lang_String $in_0#2 >= 0)
(ln -1) $ex_ := $null$
(ln 17) r0 := $in_0
(ln 17) push_107(JayArray_java_lang_String, $in_0, [JayArray_java_lang_String $in_0#2, undef_field0, undef_field1])
(ln 17) $ex_ := call <SatBranches: void <clinit>()>()
(ln 17) $ex_ := call <JayHornAssertions: void <clinit>()>()
(ln 18) $r3 := new java/util/Random
(ln 18) $ex_, $r3_seed_3540, $r3_nextNextGaussian_01, $r3_haveNextNextGaussian_02 := call <java.util.Random: void <init>()>($r3)
(ln 19) $r4 := new A
(ln 19) $ex_, $r4_i_03 := call <A: void <init>()>($r4)
(ln 20) $ex_, $z0 := call <java.util.Random: boolean nextBoolean()>($r3)
goto:
if ($z0 == false): Block2
if (!($z0 == false)): Block3
Block2:
(ln 23) $ex_ := call <A: void setI(int)>($r4, 42)
(ln 26) $r4_i_03 := pull(A, $r4)[2]
goto:
Block4
Block3:
(ln 21) $ex_ := call <A: void setI(int)>($r4, 41)
(ln 26) $r4_i_03 := pull(A, $r4)[2]
goto:
Block4
Block4:
(ln 26) $i0 := $r4_i_03
goto:
if ($r4_i_03 == 41): Block5
if (!($r4_i_03 == 41)): Block6
Block5:
goto:
Block0
Block6:
(ln 26) $r4_i_03 := pull(A, $r4)[2]
(ln 26) $i1 := $r4_i_03
goto:
if ($r4_i_03 == 42): Block5
if (!($r4_i_03 == 42)): Block7
Block7:
(ln 25) assert ((0 == 0)?false:true)
goto:
Block5
Method <java.lang.Object: void <init>()>($in_0)
Return types: java.lang.Throwable
Returns: java.lang.Throwable exc
Root ->Block0:
(ln 2) exc := $null$
(ln 2) push_106(java/lang/Object, $in_0, [])
return
Method <java.util.Random: boolean nextBoolean()>($in_0)
Return types: java.lang.Throwable, boolean
Returns: java.lang.Throwable exc, boolean $ret_
Root ->Block0:
(ln 17) exc := $null$
return
Method <java.util.Random: void <init>()>($in_0)
Return types: java.lang.Throwable, java.util.concurrent.atomic.AtomicLong, int, boolean
Returns: java.lang.Throwable exc, java.util.concurrent.atomic.AtomicLong $out1, int $out2, boolean $out3
Root ->Block0:
(ln 17) exc := $null$
(ln 17) $out1 := undef_field1
(ln 17) $out2 := undef_field2
(ln 17) $out3 := undef_field3
(ln 17) push_108(java/util/Random, $in_0, [undef_field1, undef_field2, undef_field3])
return
Raw
SatBranches_normal.cfg
$StaticFields_SatBranches $Global_SatBranches;
int $float37;
int $double40;
Method <A: void <init>()>($in_0)
Return types: java.lang.Throwable, int
Returns: java.lang.Throwable $ex_, int $co_1
locals:
r0: A
Block0:
(ln 3) push_1(A, r0, [$co_1])
return
Root ->Block1:
(ln -1) $this_ := $in_0
(ln -1) $ex_ := $null$
(ln 2) r0 := $this_
(ln 3) $ex_ := call <java.lang.Object: void <init>()>(r0)
(ln 2) $co_1 := 0
goto:
Block0
Method <A: void setI(int)>($in_0, $in_1)
Return types: java.lang.Throwable
Returns: java.lang.Throwable $ex_
locals:
r0: A
i0: int
r0_i_00: int
Block0:
(ln 7) push_2(A, r0, [r0_i_00])
return
Root ->Block1:
(ln -1) $this_ := $in_0
(ln -1) $ex_ := $null$
(ln 6) r0 := $this_
(ln 7) r0_i_00 := pull(A, r0)[1]
(ln 6) i0 := $in_1
(ln 7) r0_i_00 := i0
goto:
Block0
Method <JayHornAssertions: void <clinit>()>()
Return types: java.lang.Throwable
Returns: java.lang.Throwable $ex_
Block0:
return
Root ->Block1:
(ln -1) $ex_ := $null$
(ln -1) $ex_ := $null$
goto:
Block0
Method <SatBranches: void <clinit>()>()
Return types: java.lang.Throwable
Returns: java.lang.Throwable $ex_
locals:
SatBranches_$assertionsDisabled0: boolean
Block0:
return
Root ->Block1:
(ln -1) $ex_ := $null$
(ln 14) SatBranches_$assertionsDisabled0 := false
(ln 14) push_4($StaticFields_SatBranches, $Global_SatBranches, [SatBranches_$assertionsDisabled0])
goto:
Block0
Method <SatBranches: void main(JayArray_java_lang_String)>($in_0)
Return types: java.lang.Throwable
Returns: java.lang.Throwable $ex_
locals:
r0: JayArray_java_lang_String
$r3: java.util.Random
$i1: int
$r4: A
$i0: int
$z0: boolean
$r3_seed_3540: java.util.concurrent.atomic.AtomicLong
$r3_nextNextGaussian_01: int
$r3_haveNextNextGaussian_02: boolean
$r4_i_03: int
Block0:
return
Root ->Block1:
(ln 17) assume (JayArray_java_lang_String $in_0#2 >= 0)
(ln -1) $ex_ := $null$
(ln 17) r0 := $in_0
(ln 17) push_107(JayArray_java_lang_String, $in_0, [JayArray_java_lang_String $in_0#2, undef_field0, undef_field1])
(ln 17) $ex_ := call <SatBranches: void <clinit>()>()
(ln 17) $ex_ := call <JayHornAssertions: void <clinit>()>()
(ln 18) $r3 := new java/util/Random
(ln 18) $ex_, $r3_seed_3540, $r3_nextNextGaussian_01, $r3_haveNextNextGaussian_02 := call <java.util.Random: void <init>()>($r3)
(ln 19) $r4 := new A
(ln 19) $ex_, $r4_i_03 := call <A: void <init>()>($r4)
(ln 20) $ex_, $z0 := call <java.util.Random: boolean nextBoolean()>($r3)
goto:
if ($z0 == false): Block2
if (!($z0 == false)): Block3
Block2:
(ln 23) $ex_ := call <A: void setI(int)>($r4, 42)
(ln 26) $r4_i_03 := pull(A, $r4)[2]
goto:
Block4
Block3:
(ln 21) $ex_ := call <A: void setI(int)>($r4, 41)
(ln 26) $r4_i_03 := pull(A, $r4)[2]
goto:
Block4
Block4:
(ln 26) $i0 := $r4_i_03
goto:
if ($i0 == 41): Block5
if (!($i0 == 41)): Block6
Block5:
goto:
Block0
Block6:
(ln 26) $i1 := $r4_i_03
goto:
if ($i1 == 42): Block5
if (!($i1 == 42)): Block7
Block7:
(ln 25) assert ((0 == 0)?false:true)
goto:
Block5
Method <java.lang.Object: void <init>()>($in_0)
Return types: java.lang.Throwable
Returns: java.lang.Throwable exc
Root ->Block0:
(ln 2) exc := $null$
(ln 2) push_106(java/lang/Object, $in_0, [])
return
Method <java.util.Random: boolean nextBoolean()>($in_0)
Return types: java.lang.Throwable, boolean
Returns: java.lang.Throwable exc, boolean $ret_
Root ->Block0:
(ln 17) exc := $null$
return
Method <java.util.Random: void <init>()>($in_0)
Return types: java.lang.Throwable, java.util.concurrent.atomic.AtomicLong, int, boolean
Returns: java.lang.Throwable exc, java.util.concurrent.atomic.AtomicLong $out1, int $out2, boolean $out3
Root ->Block0:
(ln 17) exc := $null$
(ln 17) $out1 := undef_field1
(ln 17) $out2 := undef_field2
(ln 17) $out3 := undef_field3
(ln 17) push_108(java/util/Random, $in_0, [undef_field1, undef_field2, undef_field3])
return
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment