From 962f8d5252b3f5ec4d19e0cd2a430934bd55cc6d Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sun, 28 Jun 2015 01:44:30 +0100 Subject: Normalise line endings using a .gitattributes file. Unfortunately this required that this commit globally modify most files. If you want to use git blame to see the real author of a line use the ``-w`` flag so that whitespace changes are ignored. --- Test/prover/EQ_v2.Eval__v4.Eval_out.bpl | 4514 +++++++++++++++---------------- Test/prover/z3mutl.bpl | 46 +- 2 files changed, 2280 insertions(+), 2280 deletions(-) (limited to 'Test/prover') diff --git a/Test/prover/EQ_v2.Eval__v4.Eval_out.bpl b/Test/prover/EQ_v2.Eval__v4.Eval_out.bpl index 80b50686..bd823c3f 100644 --- a/Test/prover/EQ_v2.Eval__v4.Eval_out.bpl +++ b/Test/prover/EQ_v2.Eval__v4.Eval_out.bpl @@ -1,2257 +1,2257 @@ -// RUN: %boogie -typeEncoding:m -z3multipleErrors "%s" > "%t" -// RUN: %diff "%s.expect" "%t" -var v4.Mem: [name][int]int; - -var v4.alloc: int; - -var v4.Mem_T.INT4: [int]int; - -var v4.Mem_T.op1__EXPR: [int]int; - -var v4.Mem_T.op2__EXPR: [int]int; - -var v4.Mem_T.oper__EXPR: [int]int; - -var v4.Mem_T.result__EXPR: [int]int; - -var v4.detChoiceCnt: int; - -var v4.Res_KERNEL_SOURCE: [int]int; - -var v4.Res_PROBED: [int]int; - -var v4.isUnsigned: int; - -const unique v4.T.oper__EXPR: name; - -const unique v4.T.op1__EXPR: name; - -const unique v4.T.op2__EXPR: name; - -const unique v4.T.result__EXPR: name; - -const unique v4.T.INT4: name; - -const unique v4.T.PINT4: name; - -const unique v4.T.PPINT4: name; - -const unique v4.T.PP_EXPR: name; - -const unique v4.T.P_EXPR: name; - -const unique v4.T._EXPR: name; - -const {:model_const "e->op2"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 23} unique v4.__ctobpl_const_9: int; - -const {:model_const "res"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 24} unique v4.__ctobpl_const_10: int; - -const {:model_const "op"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 26} unique v4.__ctobpl_const_11: int; - -const {:model_const "e"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 41} unique v4.__ctobpl_const_12: int; - -const {:model_const "e->op1"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 22} unique v4.__ctobpl_const_6: int; - -const {:model_const "a2"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 23} unique v4.__ctobpl_const_7: int; - -const {:model_const "e"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 23} unique v4.__ctobpl_const_8: int; - -const {:model_const "e->oper"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 21} unique v4.__ctobpl_const_3: int; - -const {:model_const "op"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 21} unique v4.__ctobpl_const_1: int; - -const {:model_const "e"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 21} unique v4.__ctobpl_const_2: int; - -const {:model_const "e->result"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 41} unique v4.__ctobpl_const_13: int; - -const {:model_const "res"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 41} unique v4.__ctobpl_const_14: int; - -const {:model_const "isUnsigned"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 29} unique v4.__ctobpl_const_15: int; - -const {:model_const "isUnsigned"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 35} unique v4.__ctobpl_const_16: int; - -const {:model_const "res"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 38} unique v4.__ctobpl_const_17: int; - -const {:model_const "a1"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 38} unique v4.__ctobpl_const_18: int; - -const {:model_const "a2"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 38} unique v4.__ctobpl_const_19: int; - -const {:model_const "a1"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 36} unique v4.__ctobpl_const_20: int; - -const {:model_const "a2"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 36} unique v4.__ctobpl_const_21: int; - -const {:model_const "a1"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 36} unique v4.__ctobpl_const_22: int; - -const {:model_const "a2"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 36} unique v4.__ctobpl_const_23: int; - -const {:model_const "res"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 36} unique v4.__ctobpl_const_24: int; - -const {:model_const "result.UnsignedSub"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 36} unique v4.__ctobpl_const_25: int; - -const {:model_const "res"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 32} unique v4.__ctobpl_const_26: int; - -const {:model_const "a1"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 32} unique v4.__ctobpl_const_27: int; - -const {:model_const "a2"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 32} unique v4.__ctobpl_const_28: int; - -const {:model_const "a1"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 30} unique v4.__ctobpl_const_29: int; - -const {:model_const "a2"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 30} unique v4.__ctobpl_const_30: int; - -const {:model_const "a1"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 30} unique v4.__ctobpl_const_31: int; - -const {:model_const "a2"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 30} unique v4.__ctobpl_const_32: int; - -const {:model_const "res"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 30} unique v4.__ctobpl_const_33: int; - -const {:model_const "result.UnsignedAdd"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 30} unique v4.__ctobpl_const_34: int; - -const {:model_const "isUnsigned"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 47} unique v4.__ctobpl_const_35: int; - -const {:model_const "a1"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 22} unique v4.__ctobpl_const_4: int; - -const {:model_const "e"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 22} unique v4.__ctobpl_const_5: int; - -const {:model_const "e"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 48} unique v4.__ctobpl_const_36: int; - -const {:model_const "e"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 48} unique v4.__ctobpl_const_37: int; - -const {:model_const "outval"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 49} unique v4.__ctobpl_const_38: int; - -const {:model_const "*outval"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 49} unique v4.__ctobpl_const_39: int; - -const {:model_const "e"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 49} unique v4.__ctobpl_const_40: int; - -const {:model_const "e->result"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 49} unique v4.__ctobpl_const_41: int; - -const {:model_const "isUnsigned"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 54} unique v4.__ctobpl_const_42: int; - -const {:model_const "e"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 55} unique v4.__ctobpl_const_43: int; - -const {:model_const "e"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 55} unique v4.__ctobpl_const_44: int; - -function v4.OneByteToInt(arg_0: byte) : int; - -function v4.TwoBytesToInt(arg_0: byte, arg_1: byte) : int; - -function v4.FourBytesToInt(arg_0: byte, arg_1: byte, arg_2: byte, arg_3: byte) : int; - -function v4.Field(arg_0: int) : name; - -function v4.Base(arg_0: int) : int; - -function v4.Match(a: int, t: name) : bool; - -function v4.MatchBase(b: int, a: int, t: name) : bool; - -function v4.HasType(v: int, t: name) : bool; - -function v4.T.Ptr(t: name) : name; - -function v4.op1__EXPR(arg_0: int) : int; - -function v4.op1__EXPRInv(arg_0: int) : int; - -function v4._S_op1__EXPR(arg_0: [int]bool) : [int]bool; - -function v4._S_op1__EXPRInv(arg_0: [int]bool) : [int]bool; - -function v4.op2__EXPR(arg_0: int) : int; - -function v4.op2__EXPRInv(arg_0: int) : int; - -function v4._S_op2__EXPR(arg_0: [int]bool) : [int]bool; - -function v4._S_op2__EXPRInv(arg_0: [int]bool) : [int]bool; - -function v4.oper__EXPR(arg_0: int) : int; - -function v4.oper__EXPRInv(arg_0: int) : int; - -function v4._S_oper__EXPR(arg_0: [int]bool) : [int]bool; - -function v4._S_oper__EXPRInv(arg_0: [int]bool) : [int]bool; - -function v4.result__EXPR(arg_0: int) : int; - -function v4.result__EXPRInv(arg_0: int) : int; - -function v4._S_result__EXPR(arg_0: [int]bool) : [int]bool; - -function v4._S_result__EXPRInv(arg_0: [int]bool) : [int]bool; - -function v4.INT_EQ(x: int, y: int) : bool; - -function v4.INT_NEQ(x: int, y: int) : bool; - -function v4.INT_ADD(x: int, y: int) : int; - -function v4.INT_SUB(x: int, y: int) : int; - -function v4.INT_MULT(x: int, y: int) : int; - -function v4.INT_DIV(x: int, y: int) : int; - -function v4.INT_LT(x: int, y: int) : bool; - -function v4.INT_ULT(x: int, y: int) : bool; - -function v4.INT_LEQ(x: int, y: int) : bool; - -function v4.INT_ULEQ(x: int, y: int) : bool; - -function v4.INT_GT(x: int, y: int) : bool; - -function v4.INT_UGT(x: int, y: int) : bool; - -function v4.INT_GEQ(x: int, y: int) : bool; - -function v4.INT_UGEQ(x: int, y: int) : bool; - -function v4.BV32_EQ(x: bv32, y: bv32) : bool; - -function v4.BV32_NEQ(x: bv32, y: bv32) : bool; - -function {:bvbuiltin "bvadd"} v4.BV32_ADD(x: bv32, y: bv32) : bv32; - -function {:bvbuiltin "bvsub"} v4.BV32_SUB(x: bv32, y: bv32) : bv32; - -function {:bvbuiltin "bvmul"} v4.BV32_MULT(x: bv32, y: bv32) : bv32; - -function {:bvbuiltin "bvudiv"} v4.BV32_DIV(x: bv32, y: bv32) : bv32; - -function {:bvbuiltin "bvult"} v4.BV32_ULT(x: bv32, y: bv32) : bool; - -function {:bvbuiltin "bvslt"} v4.BV32_LT(x: bv32, y: bv32) : bool; - -function {:bvbuiltin "bvule"} v4.BV32_ULEQ(x: bv32, y: bv32) : bool; - -function {:bvbuiltin "bvsle"} v4.BV32_LEQ(x: bv32, y: bv32) : bool; - -function {:bvbuiltin "bvugt"} v4.BV32_UGT(x: bv32, y: bv32) : bool; - -function {:bvbuiltin "bvsgt"} v4.BV32_GT(x: bv32, y: bv32) : bool; - -function {:bvbuiltin "bvuge"} v4.BV32_UGEQ(x: bv32, y: bv32) : bool; - -function {:bvbuiltin "bvsge"} v4.BV32_GEQ(x: bv32, y: bv32) : bool; - -function v4.MINUS_BOTH_PTR_OR_BOTH_INT(a: int, b: int, size: int) : int; - -function v4.MINUS_LEFT_PTR(a: int, a_size: int, b: int) : int; - -function v4.PLUS(a: int, a_size: int, b: int) : int; - -function v4.MULT(a: int, b: int) : int; - -function v4.DIV(a: int, b: int) : int; - -function v4.BINARY_BOTH_INT(a: int, b: int) : int; - -function v4.POW2(a: int) : bool; - -function v4.BIT_BAND(a: int, b: int) : int; - -function v4.BIT_BOR(a: int, b: int) : int; - -function v4.BIT_BXOR(a: int, b: int) : int; - -function v4.BIT_BNOT(a: int) : int; - -function v4.choose(a: bool, b: int, c: int) : int; - -function v4.LIFT(a: bool) : int; - -function v4.PTR_NOT(a: int) : int; - -function v4.NULL_CHECK(a: int) : int; - -function v4.NewAlloc(x: int, y: int) : int; - -function v4.DetChoiceFunc(a: int) : int; - -function v4.Equal(arg_0: [int]bool, arg_1: [int]bool) : bool; - -function v4.Subset(arg_0: [int]bool, arg_1: [int]bool) : bool; - -function v4.Disjoint(arg_0: [int]bool, arg_1: [int]bool) : bool; - -function v4.Empty() : [int]bool; - -function v4.SetTrue() : [int]bool; - -function v4.Singleton(arg_0: int) : [int]bool; - -function v4.Reachable(arg_0: [int,int]bool, arg_1: int) : [int]bool; - -function v4.Union(arg_0: [int]bool, arg_1: [int]bool) : [int]bool; - -function v4.Intersection(arg_0: [int]bool, arg_1: [int]bool) : [int]bool; - -function v4.Difference(arg_0: [int]bool, arg_1: [int]bool) : [int]bool; - -function v4.Dereference(arg_0: [int]bool, arg_1: [int]int) : [int]bool; - -function v4.Inverse(f: [int]int, x: int) : [int]bool; - -function v4.AtLeast(arg_0: int, arg_1: int) : [int]bool; - -function v4.Rep(arg_0: int, arg_1: int) : int; - -function v4.Array(arg_0: int, arg_1: int, arg_2: int) : [int]bool; - -function v4.Unified(arg_0: [name][int]int) : [int]int; - -function v4.value_is(c: int, e: int) : bool; - -axiom (forall b0: byte, c0: byte :: { v4.OneByteToInt(b0), v4.OneByteToInt(c0) } v4.OneByteToInt(b0) == v4.OneByteToInt(c0) ==> b0 == c0); - -axiom (forall b0: byte, b1: byte, c0: byte, c1: byte :: { v4.TwoBytesToInt(b0, b1), v4.TwoBytesToInt(c0, c1) } v4.TwoBytesToInt(b0, b1) == v4.TwoBytesToInt(c0, c1) ==> b0 == c0 && b1 == c1); - -axiom (forall b0: byte, b1: byte, b2: byte, b3: byte, c0: byte, c1: byte, c2: byte, c3: byte :: { v4.FourBytesToInt(b0, b1, b2, b3), v4.FourBytesToInt(c0, c1, c2, c3) } v4.FourBytesToInt(b0, b1, b2, b3) == v4.FourBytesToInt(c0, c1, c2, c3) ==> b0 == c0 && b1 == c1 && b2 == c2 && b3 == c3); - -axiom (forall x: int :: { v4.Base(x) } v4.INT_LEQ(v4.Base(x), x)); - -axiom (forall a: int, t: name :: { v4.Match(a, v4.T.Ptr(t)) } v4.Match(a, v4.T.Ptr(t)) <==> v4.Field(a) == v4.T.Ptr(t)); - -axiom (forall b: int, a: int, t: name :: { v4.MatchBase(b, a, v4.T.Ptr(t)) } v4.MatchBase(b, a, v4.T.Ptr(t)) <==> v4.Base(a) == b); - -axiom (forall v: int, t: name :: { v4.HasType(v, v4.T.Ptr(t)) } v4.HasType(v, v4.T.Ptr(t)) <==> v == 0 || (v4.INT_GT(v, 0) && v4.Match(v, t) && v4.MatchBase(v4.Base(v), v, t))); - -axiom (forall x: int, S: [int]bool :: { v4._S_op1__EXPR(S)[x] } v4._S_op1__EXPR(S)[x] <==> S[v4.op1__EXPRInv(x)]); - -axiom (forall x: int, S: [int]bool :: { v4._S_op1__EXPRInv(S)[x] } v4._S_op1__EXPRInv(S)[x] <==> S[v4.op1__EXPR(x)]); - -axiom (forall x: int, S: [int]bool :: { S[x], v4._S_op1__EXPR(S) } S[x] ==> v4._S_op1__EXPR(S)[v4.op1__EXPR(x)]); - -axiom (forall x: int, S: [int]bool :: { S[x], v4._S_op1__EXPRInv(S) } S[x] ==> v4._S_op1__EXPRInv(S)[v4.op1__EXPRInv(x)]); - -axiom (forall x: int :: { v4.op1__EXPR(x) } v4.op1__EXPR(x) == v4.INT_ADD(x, 4)); - -axiom (forall x: int :: { v4.op1__EXPRInv(x) } v4.op1__EXPRInv(x) == v4.INT_SUB(x, 4)); - -axiom (forall x: int :: { v4.op1__EXPR(x) } v4.op1__EXPR(x) == v4.PLUS(x, 1, 4)); - -axiom (forall x: int, S: [int]bool :: { v4._S_op2__EXPR(S)[x] } v4._S_op2__EXPR(S)[x] <==> S[v4.op2__EXPRInv(x)]); - -axiom (forall x: int, S: [int]bool :: { v4._S_op2__EXPRInv(S)[x] } v4._S_op2__EXPRInv(S)[x] <==> S[v4.op2__EXPR(x)]); - -axiom (forall x: int, S: [int]bool :: { S[x], v4._S_op2__EXPR(S) } S[x] ==> v4._S_op2__EXPR(S)[v4.op2__EXPR(x)]); - -axiom (forall x: int, S: [int]bool :: { S[x], v4._S_op2__EXPRInv(S) } S[x] ==> v4._S_op2__EXPRInv(S)[v4.op2__EXPRInv(x)]); - -axiom (forall x: int :: { v4.op2__EXPR(x) } v4.op2__EXPR(x) == v4.INT_ADD(x, 8)); - -axiom (forall x: int :: { v4.op2__EXPRInv(x) } v4.op2__EXPRInv(x) == v4.INT_SUB(x, 8)); - -axiom (forall x: int :: { v4.op2__EXPR(x) } v4.op2__EXPR(x) == v4.PLUS(x, 1, 8)); - -axiom (forall x: int, S: [int]bool :: { v4._S_oper__EXPR(S)[x] } v4._S_oper__EXPR(S)[x] <==> S[v4.oper__EXPRInv(x)]); - -axiom (forall x: int, S: [int]bool :: { v4._S_oper__EXPRInv(S)[x] } v4._S_oper__EXPRInv(S)[x] <==> S[v4.oper__EXPR(x)]); - -axiom (forall x: int, S: [int]bool :: { S[x], v4._S_oper__EXPR(S) } S[x] ==> v4._S_oper__EXPR(S)[v4.oper__EXPR(x)]); - -axiom (forall x: int, S: [int]bool :: { S[x], v4._S_oper__EXPRInv(S) } S[x] ==> v4._S_oper__EXPRInv(S)[v4.oper__EXPRInv(x)]); - -axiom (forall x: int :: { v4.oper__EXPR(x) } v4.oper__EXPR(x) == v4.INT_ADD(x, 0)); - -axiom (forall x: int :: { v4.oper__EXPRInv(x) } v4.oper__EXPRInv(x) == v4.INT_SUB(x, 0)); - -axiom (forall x: int :: { v4.oper__EXPR(x) } v4.oper__EXPR(x) == v4.PLUS(x, 1, 0)); - -axiom (forall x: int, S: [int]bool :: { v4._S_result__EXPR(S)[x] } v4._S_result__EXPR(S)[x] <==> S[v4.result__EXPRInv(x)]); - -axiom (forall x: int, S: [int]bool :: { v4._S_result__EXPRInv(S)[x] } v4._S_result__EXPRInv(S)[x] <==> S[v4.result__EXPR(x)]); - -axiom (forall x: int, S: [int]bool :: { S[x], v4._S_result__EXPR(S) } S[x] ==> v4._S_result__EXPR(S)[v4.result__EXPR(x)]); - -axiom (forall x: int, S: [int]bool :: { S[x], v4._S_result__EXPRInv(S) } S[x] ==> v4._S_result__EXPRInv(S)[v4.result__EXPRInv(x)]); - -axiom (forall x: int :: { v4.result__EXPR(x) } v4.result__EXPR(x) == v4.INT_ADD(x, 12)); - -axiom (forall x: int :: { v4.result__EXPRInv(x) } v4.result__EXPRInv(x) == v4.INT_SUB(x, 12)); - -axiom (forall x: int :: { v4.result__EXPR(x) } v4.result__EXPR(x) == v4.PLUS(x, 1, 12)); - -axiom (forall x: int, y: int :: { v4.INT_EQ(x, y): bool } v4.INT_EQ(x, y): bool <==> x == y); - -axiom (forall x: int, y: int :: { v4.INT_NEQ(x, y): bool } v4.INT_NEQ(x, y): bool <==> x != y); - -axiom (forall x: int, y: int :: { v4.INT_ADD(x, y): int } v4.INT_ADD(x, y): int == x + y); - -axiom (forall x: int, y: int :: { v4.INT_SUB(x, y): int } v4.INT_SUB(x, y): int == x - y); - -axiom (forall x: int, y: int :: { v4.INT_MULT(x, y): int } v4.INT_MULT(x, y): int == x * y); - -axiom (forall x: int, y: int :: { v4.INT_DIV(x, y): int } v4.INT_DIV(x, y): int == x div y); - -axiom (forall x: int, y: int :: { v4.INT_LT(x, y): bool } v4.INT_LT(x, y): bool <==> x < y); - -axiom (forall x: int, y: int :: { v4.INT_ULT(x, y): bool } v4.INT_ULT(x, y): bool <==> x < y); - -axiom (forall x: int, y: int :: { v4.INT_LEQ(x, y): bool } v4.INT_LEQ(x, y): bool <==> x <= y); - -axiom (forall x: int, y: int :: { v4.INT_ULEQ(x, y): bool } v4.INT_ULEQ(x, y): bool <==> x <= y); - -axiom (forall x: int, y: int :: { v4.INT_GT(x, y): bool } v4.INT_GT(x, y): bool <==> x > y); - -axiom (forall x: int, y: int :: { v4.INT_UGT(x, y): bool } v4.INT_UGT(x, y): bool <==> x > y); - -axiom (forall x: int, y: int :: { v4.INT_GEQ(x, y): bool } v4.INT_GEQ(x, y): bool <==> x >= y); - -axiom (forall x: int, y: int :: { v4.INT_UGEQ(x, y): bool } v4.INT_UGEQ(x, y): bool <==> x >= y); - -axiom (forall x: bv32, y: bv32 :: { v4.BV32_EQ(x, y): bool } v4.BV32_EQ(x, y): bool <==> x == y); - -axiom (forall x: bv32, y: bv32 :: { v4.BV32_NEQ(x, y): bool } v4.BV32_NEQ(x, y): bool <==> x != y); - -axiom (forall a: int, b: int, size: int :: { v4.MINUS_BOTH_PTR_OR_BOTH_INT(a, b, size) } v4.INT_LEQ(v4.INT_MULT(size, v4.MINUS_BOTH_PTR_OR_BOTH_INT(a, b, size)), v4.INT_SUB(a, b)) && v4.INT_LT(v4.INT_SUB(a, b), v4.INT_MULT(size, v4.INT_ADD(v4.MINUS_BOTH_PTR_OR_BOTH_INT(a, b, size), 1)))); - -axiom (forall a: int, b: int, size: int :: { v4.MINUS_BOTH_PTR_OR_BOTH_INT(a, b, size) } v4.MINUS_BOTH_PTR_OR_BOTH_INT(a, b, 1) == v4.INT_SUB(a, b)); - -axiom (forall a: int, a_size: int, b: int :: { v4.MINUS_LEFT_PTR(a, a_size, b) } v4.MINUS_LEFT_PTR(a, a_size, b) == v4.INT_SUB(a, v4.INT_MULT(a_size, b))); - -axiom (forall a: int, a_size: int, b: int :: { v4.PLUS(a, a_size, b) } v4.PLUS(a, a_size, b) == v4.INT_ADD(a, v4.INT_MULT(a_size, b))); - -axiom (forall a: int, b: int :: { v4.MULT(a, b) } v4.MULT(a, b) == v4.INT_MULT(a, b)); - -axiom (forall a: int, b: int :: { v4.DIV(a, b) } a >= 0 && b > 0 ==> b * v4.DIV(a, b) <= a && a < b * (v4.DIV(a, b) + 1)); - -axiom (forall a: int, b: int :: { v4.DIV(a, b) } a >= 0 && b < 0 ==> b * v4.DIV(a, b) <= a && a < b * (v4.DIV(a, b) - 1)); - -axiom (forall a: int, b: int :: { v4.DIV(a, b) } a < 0 && b > 0 ==> b * v4.DIV(a, b) >= a && a > b * (v4.DIV(a, b) - 1)); - -axiom (forall a: int, b: int :: { v4.DIV(a, b) } a < 0 && b < 0 ==> b * v4.DIV(a, b) >= a && a > b * (v4.DIV(a, b) + 1)); - -axiom v4.POW2(1); - -axiom v4.POW2(2); - -axiom v4.POW2(4); - -axiom v4.POW2(8); - -axiom v4.POW2(16); - -axiom v4.POW2(32); - -axiom v4.POW2(64); - -axiom v4.POW2(128); - -axiom v4.POW2(256); - -axiom v4.POW2(512); - -axiom v4.POW2(1024); - -axiom v4.POW2(2048); - -axiom v4.POW2(4096); - -axiom v4.POW2(8192); - -axiom v4.POW2(16384); - -axiom v4.POW2(32768); - -axiom v4.POW2(65536); - -axiom v4.POW2(131072); - -axiom v4.POW2(262144); - -axiom v4.POW2(524288); - -axiom v4.POW2(1048576); - -axiom v4.POW2(2097152); - -axiom v4.POW2(4194304); - -axiom v4.POW2(8388608); - -axiom v4.POW2(16777216); - -axiom v4.POW2(33554432); - -axiom (forall a: int, b: int :: { v4.BIT_BAND(a, b) } a == b ==> v4.BIT_BAND(a, b) == a); - -axiom (forall a: int, b: int :: { v4.BIT_BAND(a, b) } v4.POW2(a) && v4.POW2(b) && a != b ==> v4.BIT_BAND(a, b) == 0); - -axiom (forall a: int, b: int :: { v4.BIT_BAND(a, b) } a == 0 || b == 0 ==> v4.BIT_BAND(a, b) == 0); - -axiom (forall a: bool, b: int, c: int :: { v4.choose(a, b, c) } a ==> v4.choose(a, b, c) == b); - -axiom (forall a: bool, b: int, c: int :: { v4.choose(a, b, c) } !a ==> v4.choose(a, b, c) == c); - -axiom (forall a: bool :: { v4.LIFT(a) } a <==> v4.LIFT(a) != 0); - -axiom (forall a: int :: { v4.PTR_NOT(a) } a == 0 ==> v4.PTR_NOT(a) != 0); - -axiom (forall a: int :: { v4.PTR_NOT(a) } a != 0 ==> v4.PTR_NOT(a) == 0); - -axiom (forall a: int :: { v4.NULL_CHECK(a) } a == 0 ==> v4.NULL_CHECK(a) != 0); - -axiom (forall a: int :: { v4.NULL_CHECK(a) } a != 0 ==> v4.NULL_CHECK(a) == 0); - -axiom (forall n: int, x: int, y: int :: { v4.AtLeast(n, x)[y] } v4.AtLeast(n, x)[y] ==> v4.INT_LEQ(x, y) && v4.Rep(n, x) == v4.Rep(n, y)); - -axiom (forall n: int, x: int, y: int :: { v4.AtLeast(n, x), v4.Rep(n, x), v4.Rep(n, y) } v4.INT_LEQ(x, y) && v4.Rep(n, x) == v4.Rep(n, y) ==> v4.AtLeast(n, x)[y]); - -axiom (forall n: int, x: int :: { v4.AtLeast(n, x) } v4.AtLeast(n, x)[x]); - -axiom (forall n: int, x: int, z: int :: { v4.PLUS(x, n, z) } v4.Rep(n, x) == v4.Rep(n, v4.PLUS(x, n, z))); - -axiom (forall n: int, x: int :: { v4.Rep(n, x) } (exists k: int :: v4.INT_SUB(v4.Rep(n, x), x) == v4.INT_MULT(n, k))); - -axiom (forall x: int, n: int, z: int :: { v4.Array(x, n, z) } v4.INT_LEQ(z, 0) ==> v4.Equal(v4.Array(x, n, z), v4.Empty())); - -axiom (forall x: int, n: int, z: int :: { v4.Array(x, n, z) } v4.INT_GT(z, 0) ==> v4.Equal(v4.Array(x, n, z), v4.Difference(v4.AtLeast(n, x), v4.AtLeast(n, v4.PLUS(x, n, z))))); - -axiom (forall x: int :: !v4.Empty()[x]); - -axiom (forall x: int :: v4.SetTrue()[x]); - -axiom (forall x: int, y: int :: { v4.Singleton(y)[x] } v4.Singleton(y)[x] <==> x == y); - -axiom (forall y: int :: { v4.Singleton(y) } v4.Singleton(y)[y]); - -axiom (forall x: int, S: [int]bool, T: [int]bool :: { v4.Union(S, T)[x] } { v4.Union(S, T), S[x] } { v4.Union(S, T), T[x] } v4.Union(S, T)[x] <==> S[x] || T[x]); - -axiom (forall x: int, S: [int]bool, T: [int]bool :: { v4.Intersection(S, T)[x] } { v4.Intersection(S, T), S[x] } { v4.Intersection(S, T), T[x] } v4.Intersection(S, T)[x] <==> S[x] && T[x]); - -axiom (forall x: int, S: [int]bool, T: [int]bool :: { v4.Difference(S, T)[x] } { v4.Difference(S, T), S[x] } { v4.Difference(S, T), T[x] } v4.Difference(S, T)[x] <==> S[x] && !T[x]); - -axiom (forall S: [int]bool, T: [int]bool :: { v4.Equal(S, T) } v4.Equal(S, T) <==> v4.Subset(S, T) && v4.Subset(T, S)); - -axiom (forall x: int, S: [int]bool, T: [int]bool :: { S[x], v4.Subset(S, T) } { T[x], v4.Subset(S, T) } S[x] && v4.Subset(S, T) ==> T[x]); - -axiom (forall S: [int]bool, T: [int]bool :: { v4.Subset(S, T) } v4.Subset(S, T) || (exists x: int :: S[x] && !T[x])); - -axiom (forall x: int, S: [int]bool, T: [int]bool :: { S[x], v4.Disjoint(S, T) } { T[x], v4.Disjoint(S, T) } !(S[x] && v4.Disjoint(S, T) && T[x])); - -axiom (forall S: [int]bool, T: [int]bool :: { v4.Disjoint(S, T) } v4.Disjoint(S, T) || (exists x: int :: S[x] && T[x])); - -axiom (forall f: [int]int, x: int :: { v4.Inverse(f, f[x]) } v4.Inverse(f, f[x])[x]); - -axiom (forall f: [int]int, x: int, y: int :: { v4.Inverse(f, y), f[x] } v4.Inverse(f, y)[x] ==> f[x] == y); - -axiom (forall f: [int]int, x: int, y: int :: { v4.Inverse(f[x := y], y) } v4.Equal(v4.Inverse(f[x := y], y), v4.Union(v4.Inverse(f, y), v4.Singleton(x)))); - -axiom (forall f: [int]int, x: int, y: int, z: int :: { v4.Inverse(f[x := y], z) } y == z || v4.Equal(v4.Inverse(f[x := y], z), v4.Difference(v4.Inverse(f, z), v4.Singleton(x)))); - -axiom (forall x: int, S: [int]bool, M: [int]int :: { v4.Dereference(S, M)[x] } v4.Dereference(S, M)[x] ==> (exists y: int :: x == M[y] && S[y])); - -axiom (forall x: int, S: [int]bool, M: [int]int :: { M[x], S[x], v4.Dereference(S, M) } S[x] ==> v4.Dereference(S, M)[M[x]]); - -axiom (forall x: int, y: int, S: [int]bool, M: [int]int :: { v4.Dereference(S, M[x := y]) } !S[x] ==> v4.Equal(v4.Dereference(S, M[x := y]), v4.Dereference(S, M))); - -axiom (forall x: int, y: int, S: [int]bool, M: [int]int :: { v4.Dereference(S, M[x := y]) } S[x] && v4.Equal(v4.Intersection(v4.Inverse(M, M[x]), S), v4.Singleton(x)) ==> v4.Equal(v4.Dereference(S, M[x := y]), v4.Union(v4.Difference(v4.Dereference(S, M), v4.Singleton(M[x])), v4.Singleton(y)))); - -axiom (forall x: int, y: int, S: [int]bool, M: [int]int :: { v4.Dereference(S, M[x := y]) } S[x] && !v4.Equal(v4.Intersection(v4.Inverse(M, M[x]), S), v4.Singleton(x)) ==> v4.Equal(v4.Dereference(S, M[x := y]), v4.Union(v4.Dereference(S, M), v4.Singleton(y)))); - -axiom (forall M: [name][int]int, x: int :: { v4.Unified(M)[x] } v4.Unified(M)[x] == M[v4.Field(x)][x]); - -axiom (forall M: [name][int]int, x: int, y: int :: { v4.Unified(M[v4.Field(x) := M[v4.Field(x)][x := y]]) } v4.Unified(M[v4.Field(x) := M[v4.Field(x)][x := y]]) == v4.Unified(M)[x := y]); - -procedure v4.havoc_assert(i: int); - - - -procedure v4.havoc_assume(i: int); - - - -procedure v4.__HAVOC_free(a: int); - - - -procedure v4.__HAVOC_malloc(obj_size: int) returns (new: int); - free ensures new == _uf_v4.__HAVOC_malloc_new(obj_size); - - - -procedure v4.__HAVOC_det_malloc(obj_size: int) returns (new: int); - free ensures new == _uf_v4.__HAVOC_det_malloc_new(obj_size); - - - -procedure v4.__HAVOC_memset_split_1(A: [int]int, p: int, c: int, n: int) returns (ret: [int]int); - free ensures ret == _uf_v4.__HAVOC_memset_split_1_ret(A, p, c, n); - - - -procedure v4.__HAVOC_memset_split_2(A: [int]int, p: int, c: int, n: int) returns (ret: [int]int); - free ensures ret == _uf_v4.__HAVOC_memset_split_2_ret(A, p, c, n); - - - -procedure v4.__HAVOC_memset_split_4(A: [int]int, p: int, c: int, n: int) returns (ret: [int]int); - free ensures ret == _uf_v4.__HAVOC_memset_split_4_ret(A, p, c, n); - - - -procedure v4.nondet_choice() returns (x: int); - free ensures x == _uf_v4.nondet_choice_x(); - - - -procedure v4.det_choice() returns (x: int); - free ensures x == _uf_v4.det_choice_x(); - - - -procedure v4._strdup(str: int) returns (new: int); - free ensures new == _uf_v4._strdup_new(str); - - - -procedure v4._xstrcasecmp(a0: int, a1: int) returns (ret: int); - free ensures ret == _uf_v4._xstrcasecmp_ret(a0, a1); - - - -procedure v4._xstrcmp(a0: int, a1: int) returns (ret: int); - free ensures ret == _uf_v4._xstrcmp_ret(a0, a1); - - - -procedure v4.UnsignedAdd(a0: int, a1: int) returns (ret: int); - - - -procedure v4.UnsignedSub(a0: int, a1: int) returns (ret: int); - - - -procedure {:inline 1} v4.Eval(e_.1: int); - modifies v4.Mem_T.result__EXPR; - free ensures v4.Mem_T.result__EXPR == _uf_v4.Eval_v4.Mem_T.result__EXPR(e_.1, old(v4.alloc), old(v4.Mem_T.oper__EXPR), old(v4.Mem_T.op1__EXPR), old(v4.Mem_T.op2__EXPR), old(v4.Mem_T.result__EXPR), old(v4.isUnsigned)); - - - -procedure v4.EvalEntry1(e_.1: int, outval_.1: int); - modifies v4.isUnsigned, v4.Mem_T.result__EXPR, v4.Mem_T.INT4; - free ensures v4.isUnsigned == _uf_v4.EvalEntry1_v4.isUnsigned(e_.1, outval_.1, old(v4.alloc), old(v4.Mem_T.oper__EXPR), old(v4.Mem_T.op1__EXPR), old(v4.Mem_T.op2__EXPR), old(v4.Mem_T.result__EXPR), old(v4.Mem_T.INT4), old(v4.isUnsigned)); - free ensures v4.Mem_T.result__EXPR == _uf_v4.EvalEntry1_v4.Mem_T.result__EXPR(e_.1, outval_.1, old(v4.alloc), old(v4.Mem_T.oper__EXPR), old(v4.Mem_T.op1__EXPR), old(v4.Mem_T.op2__EXPR), old(v4.Mem_T.result__EXPR), old(v4.Mem_T.INT4), old(v4.isUnsigned)); - free ensures v4.Mem_T.INT4 == _uf_v4.EvalEntry1_v4.Mem_T.INT4(e_.1, outval_.1, old(v4.alloc), old(v4.Mem_T.oper__EXPR), old(v4.Mem_T.op1__EXPR), old(v4.Mem_T.op2__EXPR), old(v4.Mem_T.result__EXPR), old(v4.Mem_T.INT4), old(v4.isUnsigned)); - - - -procedure v4.EvalEntry2(e_.1: int); - modifies v4.isUnsigned, v4.Mem_T.result__EXPR; - free ensures v4.isUnsigned == _uf_v4.EvalEntry2_v4.isUnsigned(e_.1, old(v4.alloc), old(v4.Mem_T.oper__EXPR), old(v4.Mem_T.op1__EXPR), old(v4.Mem_T.op2__EXPR), old(v4.Mem_T.result__EXPR), old(v4.isUnsigned)); - free ensures v4.Mem_T.result__EXPR == _uf_v4.EvalEntry2_v4.Mem_T.result__EXPR(e_.1, old(v4.alloc), old(v4.Mem_T.oper__EXPR), old(v4.Mem_T.op1__EXPR), old(v4.Mem_T.op2__EXPR), old(v4.Mem_T.result__EXPR), old(v4.isUnsigned)); - - - -procedure v4.__havoc_heapglobal_init(); - - - -implementation {:inline 1} v4.Eval(e_.1: int) -{ - var havoc_stringTemp: int; - var condVal: int; - var a1: int; - var a2: int; - var e: int; - var op: int; - var res: int; - var result.UnsignedAdd$1: int; - var result.UnsignedSub$2: int; - var tempBoogie0: int; - var tempBoogie1: int; - var tempBoogie2: int; - var tempBoogie3: int; - var tempBoogie4: int; - var tempBoogie5: int; - var tempBoogie6: int; - var tempBoogie7: int; - var tempBoogie8: int; - var tempBoogie9: int; - var tempBoogie10: int; - var tempBoogie11: int; - var tempBoogie12: int; - var tempBoogie13: int; - var tempBoogie14: int; - var tempBoogie15: int; - var tempBoogie16: int; - var tempBoogie17: int; - var tempBoogie18: int; - var tempBoogie19: int; - var __havoc_dummy_return: int; - - anon0#2: - havoc_stringTemp := 0; - goto start#2; - - start#2: - assume v4.INT_LT(e_.1, v4.alloc); - a1 := 0; - a2 := 0; - e := 0; - op := 0; - res := 0; - result.UnsignedAdd$1 := 0; - result.UnsignedSub$2 := 0; - e := e_.1; - goto label_3#2; - - label_3#2: - assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 19} true; - goto label_4#2; - - label_4#2: - assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 19} true; - goto label_5#2; - - label_5#2: - assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 19} true; - goto label_6#2; - - label_6#2: - assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 19} true; - goto label_7#2; - - label_7#2: - assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 21} true; - assert true; - op := v4.Mem_T.oper__EXPR[v4.oper__EXPR(e)]; - assume v4.value_is(v4.__ctobpl_const_1, op); - assume v4.value_is(v4.__ctobpl_const_2, e); - assume v4.value_is(v4.__ctobpl_const_3, v4.Mem_T.oper__EXPR[v4.oper__EXPR(e)]); - goto label_8#2; - - label_8#2: - assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 22} true; - assert true; - a1 := v4.Mem_T.op1__EXPR[v4.op1__EXPR(e)]; - assume v4.value_is(v4.__ctobpl_const_4, a1); - assume v4.value_is(v4.__ctobpl_const_5, e); - assume v4.value_is(v4.__ctobpl_const_6, v4.Mem_T.op1__EXPR[v4.op1__EXPR(e)]); - goto label_9#2; - - label_9#2: - assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 23} true; - assert true; - a2 := v4.Mem_T.op2__EXPR[v4.op2__EXPR(e)]; - assume v4.value_is(v4.__ctobpl_const_7, a2); - assume v4.value_is(v4.__ctobpl_const_8, e); - assume v4.value_is(v4.__ctobpl_const_9, v4.Mem_T.op2__EXPR[v4.op2__EXPR(e)]); - goto label_10#2; - - label_10#2: - assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 24} true; - res := 0 - 1; - assume v4.value_is(v4.__ctobpl_const_10, res); - goto label_11#2; - - label_11#2: - assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 26} true; - goto label_11_case_0#2, label_11_case_1#2, label_11_case_2#2; - - label_11_case_2#2: - assume v4.INT_EQ(op, 2); - assume v4.value_is(v4.__ctobpl_const_11, op); - goto label_14#2; - - label_14#2: - assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 35} true; - goto label_14_true#2, label_14_false#2; - - label_14_false#2: - assume v4.isUnsigned == 0; - assume v4.value_is(v4.__ctobpl_const_16, v4.isUnsigned); - goto label_15#2; - - label_15#2: - assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 38} true; - res := v4.MINUS_BOTH_PTR_OR_BOTH_INT(a1, a2, 1); - assume v4.value_is(v4.__ctobpl_const_17, res); - assume v4.value_is(v4.__ctobpl_const_18, a1); - assume v4.value_is(v4.__ctobpl_const_19, a2); - goto label_12#2; - - label_14_true#2: - assume v4.isUnsigned != 0; - assume v4.value_is(v4.__ctobpl_const_16, v4.isUnsigned); - goto label_16#2; - - label_16#2: - assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 36} true; - call result.UnsignedSub$2 := v4.UnsignedSub(a1, a2); - assume v4.value_is(v4.__ctobpl_const_20, a1); - assume v4.value_is(v4.__ctobpl_const_21, a2); - assume v4.value_is(v4.__ctobpl_const_22, a1); - assume v4.value_is(v4.__ctobpl_const_23, a2); - goto label_19#2; - - label_19#2: - assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 36} true; - res := result.UnsignedSub$2; - assume v4.value_is(v4.__ctobpl_const_24, res); - assume v4.value_is(v4.__ctobpl_const_25, result.UnsignedSub$2); - goto label_12#2; - - label_11_case_1#2: - assume v4.INT_EQ(op, 1); - assume v4.value_is(v4.__ctobpl_const_11, op); - goto label_13#2; - - label_13#2: - assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 29} true; - goto label_13_true#2, label_13_false#2; - - label_13_false#2: - assume v4.isUnsigned == 0; - assume v4.value_is(v4.__ctobpl_const_15, v4.isUnsigned); - goto label_20#2; - - label_20#2: - assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 32} true; - res := v4.PLUS(a1, 1, a2); - assume v4.value_is(v4.__ctobpl_const_26, res); - assume v4.value_is(v4.__ctobpl_const_27, a1); - assume v4.value_is(v4.__ctobpl_const_28, a2); - goto label_12#2; - - label_13_true#2: - assume v4.isUnsigned != 0; - assume v4.value_is(v4.__ctobpl_const_15, v4.isUnsigned); - goto label_21#2; - - label_21#2: - assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 30} true; - call result.UnsignedAdd$1 := v4.UnsignedAdd(a1, a2); - assume v4.value_is(v4.__ctobpl_const_29, a1); - assume v4.value_is(v4.__ctobpl_const_30, a2); - assume v4.value_is(v4.__ctobpl_const_31, a1); - assume v4.value_is(v4.__ctobpl_const_32, a2); - goto label_24#2; - - label_24#2: - assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 30} true; - res := result.UnsignedAdd$1; - assume v4.value_is(v4.__ctobpl_const_33, res); - assume v4.value_is(v4.__ctobpl_const_34, result.UnsignedAdd$1); - goto label_12#2; - - label_11_case_0#2: - assume v4.INT_NEQ(op, 1); - assume v4.INT_NEQ(op, 2); - assume v4.value_is(v4.__ctobpl_const_11, op); - goto label_12#2; - - label_12#2: - assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 41} true; - assert true; - v4.Mem_T.result__EXPR := v4.Mem_T.result__EXPR[v4.result__EXPR(e) := res]; - assume v4.value_is(v4.__ctobpl_const_12, e); - assume v4.value_is(v4.__ctobpl_const_13, v4.Mem_T.result__EXPR[v4.result__EXPR(e)]); - assume v4.value_is(v4.__ctobpl_const_14, res); - goto label_1#2; - - label_1#2: - assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 42} true; - return; -} - - - -implementation v4.EvalEntry1(e_.1: int, outval_.1: int) -{ - var havoc_stringTemp: int; - var condVal: int; - var e: int; - var outval: int; - var tempBoogie0: int; - var tempBoogie1: int; - var tempBoogie2: int; - var tempBoogie3: int; - var tempBoogie4: int; - var tempBoogie5: int; - var tempBoogie6: int; - var tempBoogie7: int; - var tempBoogie8: int; - var tempBoogie9: int; - var tempBoogie10: int; - var tempBoogie11: int; - var tempBoogie12: int; - var tempBoogie13: int; - var tempBoogie14: int; - var tempBoogie15: int; - var tempBoogie16: int; - var tempBoogie17: int; - var tempBoogie18: int; - var tempBoogie19: int; - var __havoc_dummy_return: int; - - anon0#2: - havoc_stringTemp := 0; - goto start#2; - - start#2: - assume v4.INT_LT(e_.1, v4.alloc); - assume v4.INT_LT(outval_.1, v4.alloc); - e := 0; - outval := 0; - e := e_.1; - outval := outval_.1; - goto label_3#2; - - label_3#2: - assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 47} true; - v4.isUnsigned := 1; - assume v4.value_is(v4.__ctobpl_const_35, v4.isUnsigned); - goto label_4#2; - - label_4#2: - assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 48} true; - call v4.Eval(e); - assume v4.value_is(v4.__ctobpl_const_36, e); - assume v4.value_is(v4.__ctobpl_const_37, e); - goto label_7#2; - - label_7#2: - assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 49} true; - assert true; - assert true; - v4.Mem_T.INT4 := v4.Mem_T.INT4[outval := v4.Mem_T.result__EXPR[v4.result__EXPR(e)]]; - assume v4.value_is(v4.__ctobpl_const_38, outval); - assume v4.value_is(v4.__ctobpl_const_39, v4.Mem_T.INT4[outval]); - assume v4.value_is(v4.__ctobpl_const_40, e); - assume v4.value_is(v4.__ctobpl_const_41, v4.Mem_T.result__EXPR[v4.result__EXPR(e)]); - goto label_1#2; - - label_1#2: - assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 50} true; - return; -} - - - -implementation v4.EvalEntry2(e_.1: int) -{ - var havoc_stringTemp: int; - var condVal: int; - var e: int; - var tempBoogie0: int; - var tempBoogie1: int; - var tempBoogie2: int; - var tempBoogie3: int; - var tempBoogie4: int; - var tempBoogie5: int; - var tempBoogie6: int; - var tempBoogie7: int; - var tempBoogie8: int; - var tempBoogie9: int; - var tempBoogie10: int; - var tempBoogie11: int; - var tempBoogie12: int; - var tempBoogie13: int; - var tempBoogie14: int; - var tempBoogie15: int; - var tempBoogie16: int; - var tempBoogie17: int; - var tempBoogie18: int; - var tempBoogie19: int; - var __havoc_dummy_return: int; - - anon0#2: - havoc_stringTemp := 0; - goto start#2; - - start#2: - assume v4.INT_LT(e_.1, v4.alloc); - e := 0; - e := e_.1; - goto label_3#2; - - label_3#2: - assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 54} true; - v4.isUnsigned := 0; - assume v4.value_is(v4.__ctobpl_const_42, v4.isUnsigned); - goto label_4#2; - - label_4#2: - assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 55} true; - call v4.Eval(e); - assume v4.value_is(v4.__ctobpl_const_43, e); - assume v4.value_is(v4.__ctobpl_const_44, e); - goto label_1#2; - - label_1#2: - assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 56} true; - return; -} - - - -implementation v4.__havoc_heapglobal_init() -{ - - anon0#2: - return; -} - - - -var v2.Mem: [name][int]int; - -var v2.alloc: int; - -var v2.Mem_T.INT4: [int]int; - -var v2.Mem_T.op1__EXPR: [int]int; - -var v2.Mem_T.op2__EXPR: [int]int; - -var v2.Mem_T.oper__EXPR: [int]int; - -var v2.Mem_T.result__EXPR: [int]int; - -var v2.detChoiceCnt: int; - -var v2.Res_KERNEL_SOURCE: [int]int; - -var v2.Res_PROBED: [int]int; - -const unique v2.T.oper__EXPR: name; - -const unique v2.T.op1__EXPR: name; - -const unique v2.T.op2__EXPR: name; - -const unique v2.T.result__EXPR: name; - -const unique v2.T.INT4: name; - -const unique v2.T.PINT4: name; - -const unique v2.T.PPINT4: name; - -const unique v2.T.PP_EXPR: name; - -const unique v2.T.P_EXPR: name; - -const unique v2.T._EXPR: name; - -const {:model_const "a2"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceLine 21} unique v2.__ctobpl_const_7: int; - -const {:model_const "e"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceLine 21} unique v2.__ctobpl_const_8: int; - -const {:model_const "e->oper"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceLine 19} unique v2.__ctobpl_const_3: int; - -const {:model_const "a1"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceLine 20} unique v2.__ctobpl_const_4: int; - -const {:model_const "e"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceLine 20} unique v2.__ctobpl_const_5: int; - -const {:model_const "e->op1"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceLine 20} unique v2.__ctobpl_const_6: int; - -const {:model_const "e->op2"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceLine 21} unique v2.__ctobpl_const_9: int; - -const {:model_const "res"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceLine 22} unique v2.__ctobpl_const_10: int; - -const {:model_const "op"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceLine 24} unique v2.__ctobpl_const_11: int; - -const {:model_const "e"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceLine 35} unique v2.__ctobpl_const_12: int; - -const {:model_const "e->result"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceLine 35} unique v2.__ctobpl_const_13: int; - -const {:model_const "res"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceLine 35} unique v2.__ctobpl_const_14: int; - -const {:model_const "res"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceLine 27} unique v2.__ctobpl_const_15: int; - -const {:model_const "a1"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceLine 27} unique v2.__ctobpl_const_16: int; - -const {:model_const "a2"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceLine 27} unique v2.__ctobpl_const_17: int; - -const {:model_const "res"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceLine 29} unique v2.__ctobpl_const_18: int; - -const {:model_const "a1"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceLine 29} unique v2.__ctobpl_const_19: int; - -const {:model_const "a2"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceLine 29} unique v2.__ctobpl_const_20: int; - -const {:model_const "e"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceLine 40} unique v2.__ctobpl_const_21: int; - -const {:model_const "e"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceLine 40} unique v2.__ctobpl_const_22: int; - -const {:model_const "outval"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceLine 41} unique v2.__ctobpl_const_23: int; - -const {:model_const "*outval"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceLine 41} unique v2.__ctobpl_const_24: int; - -const {:model_const "e"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceLine 41} unique v2.__ctobpl_const_25: int; - -const {:model_const "e->result"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceLine 41} unique v2.__ctobpl_const_26: int; - -const {:model_const "e"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceLine 46} unique v2.__ctobpl_const_27: int; - -const {:model_const "e"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceLine 46} unique v2.__ctobpl_const_28: int; - -const {:model_const "op"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceLine 19} unique v2.__ctobpl_const_1: int; - -const {:model_const "e"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceLine 19} unique v2.__ctobpl_const_2: int; - -axiom (forall b0: byte, c0: byte :: { v4.OneByteToInt(b0), v4.OneByteToInt(c0) } v4.OneByteToInt(b0) == v4.OneByteToInt(c0) ==> b0 == c0); - -axiom (forall b0: byte, b1: byte, c0: byte, c1: byte :: { v4.TwoBytesToInt(b0, b1), v4.TwoBytesToInt(c0, c1) } v4.TwoBytesToInt(b0, b1) == v4.TwoBytesToInt(c0, c1) ==> b0 == c0 && b1 == c1); - -axiom (forall b0: byte, b1: byte, b2: byte, b3: byte, c0: byte, c1: byte, c2: byte, c3: byte :: { v4.FourBytesToInt(b0, b1, b2, b3), v4.FourBytesToInt(c0, c1, c2, c3) } v4.FourBytesToInt(b0, b1, b2, b3) == v4.FourBytesToInt(c0, c1, c2, c3) ==> b0 == c0 && b1 == c1 && b2 == c2 && b3 == c3); - -axiom (forall x: int :: { v4.Base(x) } v4.INT_LEQ(v4.Base(x), x)); - -axiom (forall a: int, t: name :: { v4.Match(a, v4.T.Ptr(t)) } v4.Match(a, v4.T.Ptr(t)) <==> v4.Field(a) == v4.T.Ptr(t)); - -axiom (forall b: int, a: int, t: name :: { v4.MatchBase(b, a, v4.T.Ptr(t)) } v4.MatchBase(b, a, v4.T.Ptr(t)) <==> v4.Base(a) == b); - -axiom (forall v: int, t: name :: { v4.HasType(v, v4.T.Ptr(t)) } v4.HasType(v, v4.T.Ptr(t)) <==> v == 0 || (v4.INT_GT(v, 0) && v4.Match(v, t) && v4.MatchBase(v4.Base(v), v, t))); - -axiom (forall x: int, S: [int]bool :: { v4._S_op1__EXPR(S)[x] } v4._S_op1__EXPR(S)[x] <==> S[v4.op1__EXPRInv(x)]); - -axiom (forall x: int, S: [int]bool :: { v4._S_op1__EXPRInv(S)[x] } v4._S_op1__EXPRInv(S)[x] <==> S[v4.op1__EXPR(x)]); - -axiom (forall x: int, S: [int]bool :: { S[x], v4._S_op1__EXPR(S) } S[x] ==> v4._S_op1__EXPR(S)[v4.op1__EXPR(x)]); - -axiom (forall x: int, S: [int]bool :: { S[x], v4._S_op1__EXPRInv(S) } S[x] ==> v4._S_op1__EXPRInv(S)[v4.op1__EXPRInv(x)]); - -axiom (forall x: int :: { v4.op1__EXPR(x) } v4.op1__EXPR(x) == v4.INT_ADD(x, 4)); - -axiom (forall x: int :: { v4.op1__EXPRInv(x) } v4.op1__EXPRInv(x) == v4.INT_SUB(x, 4)); - -axiom (forall x: int :: { v4.op1__EXPR(x) } v4.op1__EXPR(x) == v4.PLUS(x, 1, 4)); - -axiom (forall x: int, S: [int]bool :: { v4._S_op2__EXPR(S)[x] } v4._S_op2__EXPR(S)[x] <==> S[v4.op2__EXPRInv(x)]); - -axiom (forall x: int, S: [int]bool :: { v4._S_op2__EXPRInv(S)[x] } v4._S_op2__EXPRInv(S)[x] <==> S[v4.op2__EXPR(x)]); - -axiom (forall x: int, S: [int]bool :: { S[x], v4._S_op2__EXPR(S) } S[x] ==> v4._S_op2__EXPR(S)[v4.op2__EXPR(x)]); - -axiom (forall x: int, S: [int]bool :: { S[x], v4._S_op2__EXPRInv(S) } S[x] ==> v4._S_op2__EXPRInv(S)[v4.op2__EXPRInv(x)]); - -axiom (forall x: int :: { v4.op2__EXPR(x) } v4.op2__EXPR(x) == v4.INT_ADD(x, 8)); - -axiom (forall x: int :: { v4.op2__EXPRInv(x) } v4.op2__EXPRInv(x) == v4.INT_SUB(x, 8)); - -axiom (forall x: int :: { v4.op2__EXPR(x) } v4.op2__EXPR(x) == v4.PLUS(x, 1, 8)); - -axiom (forall x: int, S: [int]bool :: { v4._S_oper__EXPR(S)[x] } v4._S_oper__EXPR(S)[x] <==> S[v4.oper__EXPRInv(x)]); - -axiom (forall x: int, S: [int]bool :: { v4._S_oper__EXPRInv(S)[x] } v4._S_oper__EXPRInv(S)[x] <==> S[v4.oper__EXPR(x)]); - -axiom (forall x: int, S: [int]bool :: { S[x], v4._S_oper__EXPR(S) } S[x] ==> v4._S_oper__EXPR(S)[v4.oper__EXPR(x)]); - -axiom (forall x: int, S: [int]bool :: { S[x], v4._S_oper__EXPRInv(S) } S[x] ==> v4._S_oper__EXPRInv(S)[v4.oper__EXPRInv(x)]); - -axiom (forall x: int :: { v4.oper__EXPR(x) } v4.oper__EXPR(x) == v4.INT_ADD(x, 0)); - -axiom (forall x: int :: { v4.oper__EXPRInv(x) } v4.oper__EXPRInv(x) == v4.INT_SUB(x, 0)); - -axiom (forall x: int :: { v4.oper__EXPR(x) } v4.oper__EXPR(x) == v4.PLUS(x, 1, 0)); - -axiom (forall x: int, S: [int]bool :: { v4._S_result__EXPR(S)[x] } v4._S_result__EXPR(S)[x] <==> S[v4.result__EXPRInv(x)]); - -axiom (forall x: int, S: [int]bool :: { v4._S_result__EXPRInv(S)[x] } v4._S_result__EXPRInv(S)[x] <==> S[v4.result__EXPR(x)]); - -axiom (forall x: int, S: [int]bool :: { S[x], v4._S_result__EXPR(S) } S[x] ==> v4._S_result__EXPR(S)[v4.result__EXPR(x)]); - -axiom (forall x: int, S: [int]bool :: { S[x], v4._S_result__EXPRInv(S) } S[x] ==> v4._S_result__EXPRInv(S)[v4.result__EXPRInv(x)]); - -axiom (forall x: int :: { v4.result__EXPR(x) } v4.result__EXPR(x) == v4.INT_ADD(x, 12)); - -axiom (forall x: int :: { v4.result__EXPRInv(x) } v4.result__EXPRInv(x) == v4.INT_SUB(x, 12)); - -axiom (forall x: int :: { v4.result__EXPR(x) } v4.result__EXPR(x) == v4.PLUS(x, 1, 12)); - -axiom (forall x: int, y: int :: { v4.INT_EQ(x, y): bool } v4.INT_EQ(x, y): bool <==> x == y); - -axiom (forall x: int, y: int :: { v4.INT_NEQ(x, y): bool } v4.INT_NEQ(x, y): bool <==> x != y); - -axiom (forall x: int, y: int :: { v4.INT_ADD(x, y): int } v4.INT_ADD(x, y): int == x + y); - -axiom (forall x: int, y: int :: { v4.INT_SUB(x, y): int } v4.INT_SUB(x, y): int == x - y); - -axiom (forall x: int, y: int :: { v4.INT_MULT(x, y): int } v4.INT_MULT(x, y): int == x * y); - -axiom (forall x: int, y: int :: { v4.INT_DIV(x, y): int } v4.INT_DIV(x, y): int == x div y); - -axiom (forall x: int, y: int :: { v4.INT_LT(x, y): bool } v4.INT_LT(x, y): bool <==> x < y); - -axiom (forall x: int, y: int :: { v4.INT_ULT(x, y): bool } v4.INT_ULT(x, y): bool <==> x < y); - -axiom (forall x: int, y: int :: { v4.INT_LEQ(x, y): bool } v4.INT_LEQ(x, y): bool <==> x <= y); - -axiom (forall x: int, y: int :: { v4.INT_ULEQ(x, y): bool } v4.INT_ULEQ(x, y): bool <==> x <= y); - -axiom (forall x: int, y: int :: { v4.INT_GT(x, y): bool } v4.INT_GT(x, y): bool <==> x > y); - -axiom (forall x: int, y: int :: { v4.INT_UGT(x, y): bool } v4.INT_UGT(x, y): bool <==> x > y); - -axiom (forall x: int, y: int :: { v4.INT_GEQ(x, y): bool } v4.INT_GEQ(x, y): bool <==> x >= y); - -axiom (forall x: int, y: int :: { v4.INT_UGEQ(x, y): bool } v4.INT_UGEQ(x, y): bool <==> x >= y); - -axiom (forall x: bv32, y: bv32 :: { v4.BV32_EQ(x, y): bool } v4.BV32_EQ(x, y): bool <==> x == y); - -axiom (forall x: bv32, y: bv32 :: { v4.BV32_NEQ(x, y): bool } v4.BV32_NEQ(x, y): bool <==> x != y); - -axiom (forall a: int, b: int, size: int :: { v4.MINUS_BOTH_PTR_OR_BOTH_INT(a, b, size) } v4.INT_LEQ(v4.INT_MULT(size, v4.MINUS_BOTH_PTR_OR_BOTH_INT(a, b, size)), v4.INT_SUB(a, b)) && v4.INT_LT(v4.INT_SUB(a, b), v4.INT_MULT(size, v4.INT_ADD(v4.MINUS_BOTH_PTR_OR_BOTH_INT(a, b, size), 1)))); - -axiom (forall a: int, b: int, size: int :: { v4.MINUS_BOTH_PTR_OR_BOTH_INT(a, b, size) } v4.MINUS_BOTH_PTR_OR_BOTH_INT(a, b, 1) == v4.INT_SUB(a, b)); - -axiom (forall a: int, a_size: int, b: int :: { v4.MINUS_LEFT_PTR(a, a_size, b) } v4.MINUS_LEFT_PTR(a, a_size, b) == v4.INT_SUB(a, v4.INT_MULT(a_size, b))); - -axiom (forall a: int, a_size: int, b: int :: { v4.PLUS(a, a_size, b) } v4.PLUS(a, a_size, b) == v4.INT_ADD(a, v4.INT_MULT(a_size, b))); - -axiom (forall a: int, b: int :: { v4.MULT(a, b) } v4.MULT(a, b) == v4.INT_MULT(a, b)); - -axiom (forall a: int, b: int :: { v4.DIV(a, b) } a >= 0 && b > 0 ==> b * v4.DIV(a, b) <= a && a < b * (v4.DIV(a, b) + 1)); - -axiom (forall a: int, b: int :: { v4.DIV(a, b) } a >= 0 && b < 0 ==> b * v4.DIV(a, b) <= a && a < b * (v4.DIV(a, b) - 1)); - -axiom (forall a: int, b: int :: { v4.DIV(a, b) } a < 0 && b > 0 ==> b * v4.DIV(a, b) >= a && a > b * (v4.DIV(a, b) - 1)); - -axiom (forall a: int, b: int :: { v4.DIV(a, b) } a < 0 && b < 0 ==> b * v4.DIV(a, b) >= a && a > b * (v4.DIV(a, b) + 1)); - -axiom v4.POW2(1); - -axiom v4.POW2(2); - -axiom v4.POW2(4); - -axiom v4.POW2(8); - -axiom v4.POW2(16); - -axiom v4.POW2(32); - -axiom v4.POW2(64); - -axiom v4.POW2(128); - -axiom v4.POW2(256); - -axiom v4.POW2(512); - -axiom v4.POW2(1024); - -axiom v4.POW2(2048); - -axiom v4.POW2(4096); - -axiom v4.POW2(8192); - -axiom v4.POW2(16384); - -axiom v4.POW2(32768); - -axiom v4.POW2(65536); - -axiom v4.POW2(131072); - -axiom v4.POW2(262144); - -axiom v4.POW2(524288); - -axiom v4.POW2(1048576); - -axiom v4.POW2(2097152); - -axiom v4.POW2(4194304); - -axiom v4.POW2(8388608); - -axiom v4.POW2(16777216); - -axiom v4.POW2(33554432); - -axiom (forall a: int, b: int :: { v4.BIT_BAND(a, b) } a == b ==> v4.BIT_BAND(a, b) == a); - -axiom (forall a: int, b: int :: { v4.BIT_BAND(a, b) } v4.POW2(a) && v4.POW2(b) && a != b ==> v4.BIT_BAND(a, b) == 0); - -axiom (forall a: int, b: int :: { v4.BIT_BAND(a, b) } a == 0 || b == 0 ==> v4.BIT_BAND(a, b) == 0); - -axiom (forall a: bool, b: int, c: int :: { v4.choose(a, b, c) } a ==> v4.choose(a, b, c) == b); - -axiom (forall a: bool, b: int, c: int :: { v4.choose(a, b, c) } !a ==> v4.choose(a, b, c) == c); - -axiom (forall a: bool :: { v4.LIFT(a) } a <==> v4.LIFT(a) != 0); - -axiom (forall a: int :: { v4.PTR_NOT(a) } a == 0 ==> v4.PTR_NOT(a) != 0); - -axiom (forall a: int :: { v4.PTR_NOT(a) } a != 0 ==> v4.PTR_NOT(a) == 0); - -axiom (forall a: int :: { v4.NULL_CHECK(a) } a == 0 ==> v4.NULL_CHECK(a) != 0); - -axiom (forall a: int :: { v4.NULL_CHECK(a) } a != 0 ==> v4.NULL_CHECK(a) == 0); - -axiom (forall n: int, x: int, y: int :: { v4.AtLeast(n, x)[y] } v4.AtLeast(n, x)[y] ==> v4.INT_LEQ(x, y) && v4.Rep(n, x) == v4.Rep(n, y)); - -axiom (forall n: int, x: int, y: int :: { v4.AtLeast(n, x), v4.Rep(n, x), v4.Rep(n, y) } v4.INT_LEQ(x, y) && v4.Rep(n, x) == v4.Rep(n, y) ==> v4.AtLeast(n, x)[y]); - -axiom (forall n: int, x: int :: { v4.AtLeast(n, x) } v4.AtLeast(n, x)[x]); - -axiom (forall n: int, x: int, z: int :: { v4.PLUS(x, n, z) } v4.Rep(n, x) == v4.Rep(n, v4.PLUS(x, n, z))); - -axiom (forall n: int, x: int :: { v4.Rep(n, x) } (exists k: int :: v4.INT_SUB(v4.Rep(n, x), x) == v4.INT_MULT(n, k))); - -axiom (forall x: int, n: int, z: int :: { v4.Array(x, n, z) } v4.INT_LEQ(z, 0) ==> v4.Equal(v4.Array(x, n, z), v4.Empty())); - -axiom (forall x: int, n: int, z: int :: { v4.Array(x, n, z) } v4.INT_GT(z, 0) ==> v4.Equal(v4.Array(x, n, z), v4.Difference(v4.AtLeast(n, x), v4.AtLeast(n, v4.PLUS(x, n, z))))); - -axiom (forall x: int :: !v4.Empty()[x]); - -axiom (forall x: int :: v4.SetTrue()[x]); - -axiom (forall x: int, y: int :: { v4.Singleton(y)[x] } v4.Singleton(y)[x] <==> x == y); - -axiom (forall y: int :: { v4.Singleton(y) } v4.Singleton(y)[y]); - -axiom (forall x: int, S: [int]bool, T: [int]bool :: { v4.Union(S, T)[x] } { v4.Union(S, T), S[x] } { v4.Union(S, T), T[x] } v4.Union(S, T)[x] <==> S[x] || T[x]); - -axiom (forall x: int, S: [int]bool, T: [int]bool :: { v4.Intersection(S, T)[x] } { v4.Intersection(S, T), S[x] } { v4.Intersection(S, T), T[x] } v4.Intersection(S, T)[x] <==> S[x] && T[x]); - -axiom (forall x: int, S: [int]bool, T: [int]bool :: { v4.Difference(S, T)[x] } { v4.Difference(S, T), S[x] } { v4.Difference(S, T), T[x] } v4.Difference(S, T)[x] <==> S[x] && !T[x]); - -axiom (forall S: [int]bool, T: [int]bool :: { v4.Equal(S, T) } v4.Equal(S, T) <==> v4.Subset(S, T) && v4.Subset(T, S)); - -axiom (forall x: int, S: [int]bool, T: [int]bool :: { S[x], v4.Subset(S, T) } { T[x], v4.Subset(S, T) } S[x] && v4.Subset(S, T) ==> T[x]); - -axiom (forall S: [int]bool, T: [int]bool :: { v4.Subset(S, T) } v4.Subset(S, T) || (exists x: int :: S[x] && !T[x])); - -axiom (forall x: int, S: [int]bool, T: [int]bool :: { S[x], v4.Disjoint(S, T) } { T[x], v4.Disjoint(S, T) } !(S[x] && v4.Disjoint(S, T) && T[x])); - -axiom (forall S: [int]bool, T: [int]bool :: { v4.Disjoint(S, T) } v4.Disjoint(S, T) || (exists x: int :: S[x] && T[x])); - -axiom (forall f: [int]int, x: int :: { v4.Inverse(f, f[x]) } v4.Inverse(f, f[x])[x]); - -axiom (forall f: [int]int, x: int, y: int :: { v4.Inverse(f, y), f[x] } v4.Inverse(f, y)[x] ==> f[x] == y); - -axiom (forall f: [int]int, x: int, y: int :: { v4.Inverse(f[x := y], y) } v4.Equal(v4.Inverse(f[x := y], y), v4.Union(v4.Inverse(f, y), v4.Singleton(x)))); - -axiom (forall f: [int]int, x: int, y: int, z: int :: { v4.Inverse(f[x := y], z) } y == z || v4.Equal(v4.Inverse(f[x := y], z), v4.Difference(v4.Inverse(f, z), v4.Singleton(x)))); - -axiom (forall x: int, S: [int]bool, M: [int]int :: { v4.Dereference(S, M)[x] } v4.Dereference(S, M)[x] ==> (exists y: int :: x == M[y] && S[y])); - -axiom (forall x: int, S: [int]bool, M: [int]int :: { M[x], S[x], v4.Dereference(S, M) } S[x] ==> v4.Dereference(S, M)[M[x]]); - -axiom (forall x: int, y: int, S: [int]bool, M: [int]int :: { v4.Dereference(S, M[x := y]) } !S[x] ==> v4.Equal(v4.Dereference(S, M[x := y]), v4.Dereference(S, M))); - -axiom (forall x: int, y: int, S: [int]bool, M: [int]int :: { v4.Dereference(S, M[x := y]) } S[x] && v4.Equal(v4.Intersection(v4.Inverse(M, M[x]), S), v4.Singleton(x)) ==> v4.Equal(v4.Dereference(S, M[x := y]), v4.Union(v4.Difference(v4.Dereference(S, M), v4.Singleton(M[x])), v4.Singleton(y)))); - -axiom (forall x: int, y: int, S: [int]bool, M: [int]int :: { v4.Dereference(S, M[x := y]) } S[x] && !v4.Equal(v4.Intersection(v4.Inverse(M, M[x]), S), v4.Singleton(x)) ==> v4.Equal(v4.Dereference(S, M[x := y]), v4.Union(v4.Dereference(S, M), v4.Singleton(y)))); - -axiom (forall M: [name][int]int, x: int :: { v4.Unified(M)[x] } v4.Unified(M)[x] == M[v4.Field(x)][x]); - -axiom (forall M: [name][int]int, x: int, y: int :: { v4.Unified(M[v4.Field(x) := M[v4.Field(x)][x := y]]) } v4.Unified(M[v4.Field(x) := M[v4.Field(x)][x := y]]) == v4.Unified(M)[x := y]); - -procedure v2.havoc_assert(i: int); - - - -procedure v2.havoc_assume(i: int); - - - -procedure v2.__HAVOC_free(a: int); - - - -procedure v2.__HAVOC_malloc(obj_size: int) returns (new: int); - free ensures new == _uf_v4.__HAVOC_malloc_new(obj_size); - - - -procedure v2.__HAVOC_det_malloc(obj_size: int) returns (new: int); - free ensures new == _uf_v4.__HAVOC_det_malloc_new(obj_size); - - - -procedure v2.__HAVOC_memset_split_1(A: [int]int, p: int, c: int, n: int) returns (ret: [int]int); - free ensures ret == _uf_v4.__HAVOC_memset_split_1_ret(A, p, c, n); - - - -procedure v2.__HAVOC_memset_split_2(A: [int]int, p: int, c: int, n: int) returns (ret: [int]int); - free ensures ret == _uf_v4.__HAVOC_memset_split_2_ret(A, p, c, n); - - - -procedure v2.__HAVOC_memset_split_4(A: [int]int, p: int, c: int, n: int) returns (ret: [int]int); - free ensures ret == _uf_v4.__HAVOC_memset_split_4_ret(A, p, c, n); - - - -procedure v2.nondet_choice() returns (x: int); - free ensures x == _uf_v4.nondet_choice_x(); - - - -procedure v2.det_choice() returns (x: int); - free ensures x == _uf_v4.det_choice_x(); - - - -procedure v2._strdup(str: int) returns (new: int); - free ensures new == _uf_v4._strdup_new(str); - - - -procedure v2._xstrcasecmp(a0: int, a1: int) returns (ret: int); - free ensures ret == _uf_v4._xstrcasecmp_ret(a0, a1); - - - -procedure v2._xstrcmp(a0: int, a1: int) returns (ret: int); - free ensures ret == _uf_v4._xstrcmp_ret(a0, a1); - - - -procedure {:inline 1} v2.Eval(e_.1: int); - modifies v4.Mem_T.result__EXPR; - free ensures v4.Mem_T.result__EXPR == _uf_v4.Eval_v4.Mem_T.result__EXPR(e_.1, old(v4.alloc), old(v4.Mem_T.oper__EXPR), old(v4.Mem_T.op1__EXPR), old(v4.Mem_T.op2__EXPR), old(v4.Mem_T.result__EXPR), old(v4.isUnsigned)); - - - -procedure v2.EvalEntry1(e_.1: int, outval_.1: int); - modifies v4.Mem_T.result__EXPR, v4.Mem_T.INT4; - free ensures v4.Mem_T.result__EXPR == _uf_v4.EvalEntry1_v4.Mem_T.result__EXPR(e_.1, outval_.1, old(v4.alloc), old(v4.Mem_T.oper__EXPR), old(v4.Mem_T.op1__EXPR), old(v4.Mem_T.op2__EXPR), old(v4.Mem_T.result__EXPR), old(v4.Mem_T.INT4), old(v4.isUnsigned)); - free ensures v4.Mem_T.INT4 == _uf_v4.EvalEntry1_v4.Mem_T.INT4(e_.1, outval_.1, old(v4.alloc), old(v4.Mem_T.oper__EXPR), old(v4.Mem_T.op1__EXPR), old(v4.Mem_T.op2__EXPR), old(v4.Mem_T.result__EXPR), old(v4.Mem_T.INT4), old(v4.isUnsigned)); - - - -procedure v2.EvalEntry2(e_.1: int); - modifies v4.Mem_T.result__EXPR; - free ensures v4.Mem_T.result__EXPR == _uf_v4.EvalEntry2_v4.Mem_T.result__EXPR(e_.1, old(v4.alloc), old(v4.Mem_T.oper__EXPR), old(v4.Mem_T.op1__EXPR), old(v4.Mem_T.op2__EXPR), old(v4.Mem_T.result__EXPR), old(v4.isUnsigned)); - - - -procedure v2.__havoc_heapglobal_init(); - - - -implementation {:inline 1} v2.Eval(e_.1: int) -{ - var havoc_stringTemp: int; - var condVal: int; - var a1: int; - var a2: int; - var e: int; - var op: int; - var res: int; - var tempBoogie0: int; - var tempBoogie1: int; - var tempBoogie2: int; - var tempBoogie3: int; - var tempBoogie4: int; - var tempBoogie5: int; - var tempBoogie6: int; - var tempBoogie7: int; - var tempBoogie8: int; - var tempBoogie9: int; - var tempBoogie10: int; - var tempBoogie11: int; - var tempBoogie12: int; - var tempBoogie13: int; - var tempBoogie14: int; - var tempBoogie15: int; - var tempBoogie16: int; - var tempBoogie17: int; - var tempBoogie18: int; - var tempBoogie19: int; - var __havoc_dummy_return: int; - - anon0#2: - havoc_stringTemp := 0; - goto start#2; - - start#2: - assume v4.INT_LT(e_.1, v4.alloc); - a1 := 0; - a2 := 0; - e := 0; - op := 0; - res := 0; - e := e_.1; - goto label_3#2; - - label_3#2: - assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 17} true; - goto label_4#2; - - label_4#2: - assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 17} true; - goto label_5#2; - - label_5#2: - assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 17} true; - goto label_6#2; - - label_6#2: - assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 17} true; - goto label_7#2; - - label_7#2: - assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 19} true; - assert true; - op := v4.Mem_T.oper__EXPR[v4.oper__EXPR(e)]; - assume v4.value_is(v2.__ctobpl_const_1, op); - assume v4.value_is(v2.__ctobpl_const_2, e); - assume v4.value_is(v2.__ctobpl_const_3, v4.Mem_T.oper__EXPR[v4.oper__EXPR(e)]); - goto label_8#2; - - label_8#2: - assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 20} true; - assert true; - a1 := v4.Mem_T.op1__EXPR[v4.op1__EXPR(e)]; - assume v4.value_is(v2.__ctobpl_const_4, a1); - assume v4.value_is(v2.__ctobpl_const_5, e); - assume v4.value_is(v2.__ctobpl_const_6, v4.Mem_T.op1__EXPR[v4.op1__EXPR(e)]); - goto label_9#2; - - label_9#2: - assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 21} true; - assert true; - a2 := v4.Mem_T.op2__EXPR[v4.op2__EXPR(e)]; - assume v4.value_is(v2.__ctobpl_const_7, a2); - assume v4.value_is(v2.__ctobpl_const_8, e); - assume v4.value_is(v2.__ctobpl_const_9, v4.Mem_T.op2__EXPR[v4.op2__EXPR(e)]); - goto label_10#2; - - label_10#2: - assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 22} true; - res := 0 - 1; - assume v4.value_is(v2.__ctobpl_const_10, res); - goto label_11#2; - - label_11#2: - assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 24} true; - goto label_11_case_0#2, label_11_case_1#2, label_11_case_2#2; - - label_11_case_2#2: - assume v4.INT_EQ(op, 2); - assume v4.value_is(v2.__ctobpl_const_11, op); - goto label_14#2; - - label_14#2: - assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 29} true; - res := v4.MINUS_BOTH_PTR_OR_BOTH_INT(a1, a2, 1); - assume v4.value_is(v2.__ctobpl_const_18, res); - assume v4.value_is(v2.__ctobpl_const_19, a1); - assume v4.value_is(v2.__ctobpl_const_20, a2); - goto label_12#2; - - label_11_case_1#2: - assume v4.INT_EQ(op, 1); - assume v4.value_is(v2.__ctobpl_const_11, op); - goto label_13#2; - - label_13#2: - assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 27} true; - res := v4.PLUS(a1, 1, a2); - assume v4.value_is(v2.__ctobpl_const_15, res); - assume v4.value_is(v2.__ctobpl_const_16, a1); - assume v4.value_is(v2.__ctobpl_const_17, a2); - goto label_12#2; - - label_11_case_0#2: - assume v4.INT_NEQ(op, 1); - assume v4.INT_NEQ(op, 2); - assume v4.value_is(v2.__ctobpl_const_11, op); - goto label_12#2; - - label_12#2: - assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 35} true; - assert true; - v4.Mem_T.result__EXPR := v4.Mem_T.result__EXPR[v4.result__EXPR(e) := res]; - assume v4.value_is(v2.__ctobpl_const_12, e); - assume v4.value_is(v2.__ctobpl_const_13, v4.Mem_T.result__EXPR[v4.result__EXPR(e)]); - assume v4.value_is(v2.__ctobpl_const_14, res); - goto label_1#2; - - label_1#2: - assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 36} true; - return; -} - - - -implementation v2.EvalEntry1(e_.1: int, outval_.1: int) -{ - var havoc_stringTemp: int; - var condVal: int; - var e: int; - var outval: int; - var tempBoogie0: int; - var tempBoogie1: int; - var tempBoogie2: int; - var tempBoogie3: int; - var tempBoogie4: int; - var tempBoogie5: int; - var tempBoogie6: int; - var tempBoogie7: int; - var tempBoogie8: int; - var tempBoogie9: int; - var tempBoogie10: int; - var tempBoogie11: int; - var tempBoogie12: int; - var tempBoogie13: int; - var tempBoogie14: int; - var tempBoogie15: int; - var tempBoogie16: int; - var tempBoogie17: int; - var tempBoogie18: int; - var tempBoogie19: int; - var __havoc_dummy_return: int; - - anon0#2: - havoc_stringTemp := 0; - goto start#2; - - start#2: - assume v4.INT_LT(e_.1, v4.alloc); - assume v4.INT_LT(outval_.1, v4.alloc); - e := 0; - outval := 0; - e := e_.1; - outval := outval_.1; - goto label_3#2; - - label_3#2: - assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 40} true; - call v2.Eval(e); - assume v4.value_is(v2.__ctobpl_const_21, e); - assume v4.value_is(v2.__ctobpl_const_22, e); - goto label_6#2; - - label_6#2: - assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 41} true; - assert true; - assert true; - v4.Mem_T.INT4 := v4.Mem_T.INT4[outval := v4.Mem_T.result__EXPR[v4.result__EXPR(e)]]; - assume v4.value_is(v2.__ctobpl_const_23, outval); - assume v4.value_is(v2.__ctobpl_const_24, v4.Mem_T.INT4[outval]); - assume v4.value_is(v2.__ctobpl_const_25, e); - assume v4.value_is(v2.__ctobpl_const_26, v4.Mem_T.result__EXPR[v4.result__EXPR(e)]); - goto label_1#2; - - label_1#2: - assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 42} true; - return; -} - - - -implementation v2.EvalEntry2(e_.1: int) -{ - var havoc_stringTemp: int; - var condVal: int; - var e: int; - var tempBoogie0: int; - var tempBoogie1: int; - var tempBoogie2: int; - var tempBoogie3: int; - var tempBoogie4: int; - var tempBoogie5: int; - var tempBoogie6: int; - var tempBoogie7: int; - var tempBoogie8: int; - var tempBoogie9: int; - var tempBoogie10: int; - var tempBoogie11: int; - var tempBoogie12: int; - var tempBoogie13: int; - var tempBoogie14: int; - var tempBoogie15: int; - var tempBoogie16: int; - var tempBoogie17: int; - var tempBoogie18: int; - var tempBoogie19: int; - var __havoc_dummy_return: int; - - anon0#2: - havoc_stringTemp := 0; - goto start#2; - - start#2: - assume v4.INT_LT(e_.1, v4.alloc); - e := 0; - e := e_.1; - goto label_3#2; - - label_3#2: - assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 46} true; - call v2.Eval(e); - assume v4.value_is(v2.__ctobpl_const_27, e); - assume v4.value_is(v2.__ctobpl_const_28, e); - goto label_1#2; - - label_1#2: - assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 47} true; - return; -} - - - -implementation v2.__havoc_heapglobal_init() -{ - - anon0#2: - return; -} - - - -type name; - -type byte; - -var Output_of_v2.Eval_v4.Mem_T.result__EXPR: [int]int; - -var Output_of_v4.Eval_v4.Mem_T.result__EXPR: [int]int; - -procedure EQ_v2.Eval__v4.Eval(e_.1: int) returns (AA_TEMP30: bool); - modifies v4.Mem_T.result__EXPR, Output_of_v2.Eval_v4.Mem_T.result__EXPR, Output_of_v4.Eval_v4.Mem_T.result__EXPR; - ensures AA_TEMP30; - - - -implementation EQ_v2.Eval__v4.Eval(e_.1: int) returns (AA_TEMP30: bool) -{ - var AA_TEMP10: [int]int; - var AA_TEMP00: [int]int; - var inline$v2.Eval$0$havoc_stringTemp: int; - var inline$v2.Eval$0$condVal: int; - var inline$v2.Eval$0$a1: int; - var inline$v2.Eval$0$a2: int; - var inline$v2.Eval$0$e: int; - var inline$v2.Eval$0$op: int; - var inline$v2.Eval$0$res: int; - var inline$v2.Eval$0$tempBoogie0: int; - var inline$v2.Eval$0$tempBoogie1: int; - var inline$v2.Eval$0$tempBoogie2: int; - var inline$v2.Eval$0$tempBoogie3: int; - var inline$v2.Eval$0$tempBoogie4: int; - var inline$v2.Eval$0$tempBoogie5: int; - var inline$v2.Eval$0$tempBoogie6: int; - var inline$v2.Eval$0$tempBoogie7: int; - var inline$v2.Eval$0$tempBoogie8: int; - var inline$v2.Eval$0$tempBoogie9: int; - var inline$v2.Eval$0$tempBoogie10: int; - var inline$v2.Eval$0$tempBoogie11: int; - var inline$v2.Eval$0$tempBoogie12: int; - var inline$v2.Eval$0$tempBoogie13: int; - var inline$v2.Eval$0$tempBoogie14: int; - var inline$v2.Eval$0$tempBoogie15: int; - var inline$v2.Eval$0$tempBoogie16: int; - var inline$v2.Eval$0$tempBoogie17: int; - var inline$v2.Eval$0$tempBoogie18: int; - var inline$v2.Eval$0$tempBoogie19: int; - var inline$v2.Eval$0$__havoc_dummy_return: int; - var inline$v2.Eval$0$e_.1: int; - var inline$v2.Eval$0$v4.Mem_T.result__EXPR: [int]int; - var inline$v4.Eval$0$havoc_stringTemp: int; - var inline$v4.Eval$0$condVal: int; - var inline$v4.Eval$0$a1: int; - var inline$v4.Eval$0$a2: int; - var inline$v4.Eval$0$e: int; - var inline$v4.Eval$0$op: int; - var inline$v4.Eval$0$res: int; - var inline$v4.Eval$0$result.UnsignedAdd$1: int; - var inline$v4.Eval$0$result.UnsignedSub$2: int; - var inline$v4.Eval$0$tempBoogie0: int; - var inline$v4.Eval$0$tempBoogie1: int; - var inline$v4.Eval$0$tempBoogie2: int; - var inline$v4.Eval$0$tempBoogie3: int; - var inline$v4.Eval$0$tempBoogie4: int; - var inline$v4.Eval$0$tempBoogie5: int; - var inline$v4.Eval$0$tempBoogie6: int; - var inline$v4.Eval$0$tempBoogie7: int; - var inline$v4.Eval$0$tempBoogie8: int; - var inline$v4.Eval$0$tempBoogie9: int; - var inline$v4.Eval$0$tempBoogie10: int; - var inline$v4.Eval$0$tempBoogie11: int; - var inline$v4.Eval$0$tempBoogie12: int; - var inline$v4.Eval$0$tempBoogie13: int; - var inline$v4.Eval$0$tempBoogie14: int; - var inline$v4.Eval$0$tempBoogie15: int; - var inline$v4.Eval$0$tempBoogie16: int; - var inline$v4.Eval$0$tempBoogie17: int; - var inline$v4.Eval$0$tempBoogie18: int; - var inline$v4.Eval$0$tempBoogie19: int; - var inline$v4.Eval$0$__havoc_dummy_return: int; - var inline$v4.Eval$0$e_.1: int; - var inline$v4.Eval$0$v4.Mem_T.result__EXPR: [int]int; - - AA_INSTR_EQ_BODY: - AA_TEMP00 := v4.Mem_T.result__EXPR; - goto inline$v2.Eval$0$Entry; - - inline$v2.Eval$0$Entry: - inline$v2.Eval$0$e_.1 := e_.1; - inline$v2.Eval$0$v4.Mem_T.result__EXPR := v4.Mem_T.result__EXPR; - goto inline$v2.Eval$0$anon0#2; - - inline$v2.Eval$0$anon0#2: - inline$v2.Eval$0$havoc_stringTemp := 0; - goto inline$v2.Eval$0$start#2; - - inline$v2.Eval$0$start#2: - assume v4.INT_LT(inline$v2.Eval$0$e_.1, v4.alloc); - inline$v2.Eval$0$a1 := 0; - inline$v2.Eval$0$a2 := 0; - inline$v2.Eval$0$e := 0; - inline$v2.Eval$0$op := 0; - inline$v2.Eval$0$res := 0; - inline$v2.Eval$0$e := inline$v2.Eval$0$e_.1; - goto inline$v2.Eval$0$label_3#2; - - inline$v2.Eval$0$label_3#2: - assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 17} true; - goto inline$v2.Eval$0$label_4#2; - - inline$v2.Eval$0$label_4#2: - assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 17} true; - goto inline$v2.Eval$0$label_5#2; - - inline$v2.Eval$0$label_5#2: - assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 17} true; - goto inline$v2.Eval$0$label_6#2; - - inline$v2.Eval$0$label_6#2: - assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 17} true; - goto inline$v2.Eval$0$label_7#2; - - inline$v2.Eval$0$label_7#2: - assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 19} true; - assert true; - inline$v2.Eval$0$op := v4.Mem_T.oper__EXPR[v4.oper__EXPR(inline$v2.Eval$0$e)]; - assume v4.value_is(v2.__ctobpl_const_1, inline$v2.Eval$0$op); - assume v4.value_is(v2.__ctobpl_const_2, inline$v2.Eval$0$e); - assume v4.value_is(v2.__ctobpl_const_3, v4.Mem_T.oper__EXPR[v4.oper__EXPR(inline$v2.Eval$0$e)]); - goto inline$v2.Eval$0$label_8#2; - - inline$v2.Eval$0$label_8#2: - assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 20} true; - assert true; - inline$v2.Eval$0$a1 := v4.Mem_T.op1__EXPR[v4.op1__EXPR(inline$v2.Eval$0$e)]; - assume v4.value_is(v2.__ctobpl_const_4, inline$v2.Eval$0$a1); - assume v4.value_is(v2.__ctobpl_const_5, inline$v2.Eval$0$e); - assume v4.value_is(v2.__ctobpl_const_6, v4.Mem_T.op1__EXPR[v4.op1__EXPR(inline$v2.Eval$0$e)]); - goto inline$v2.Eval$0$label_9#2; - - inline$v2.Eval$0$label_9#2: - assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 21} true; - assert true; - inline$v2.Eval$0$a2 := v4.Mem_T.op2__EXPR[v4.op2__EXPR(inline$v2.Eval$0$e)]; - assume v4.value_is(v2.__ctobpl_const_7, inline$v2.Eval$0$a2); - assume v4.value_is(v2.__ctobpl_const_8, inline$v2.Eval$0$e); - assume v4.value_is(v2.__ctobpl_const_9, v4.Mem_T.op2__EXPR[v4.op2__EXPR(inline$v2.Eval$0$e)]); - goto inline$v2.Eval$0$label_10#2; - - inline$v2.Eval$0$label_10#2: - assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 22} true; - inline$v2.Eval$0$res := 0 - 1; - assume v4.value_is(v2.__ctobpl_const_10, inline$v2.Eval$0$res); - goto inline$v2.Eval$0$label_11#2; - - inline$v2.Eval$0$label_11#2: - assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 24} true; - goto inline$v2.Eval$0$label_11_case_0#2, inline$v2.Eval$0$label_11_case_1#2, inline$v2.Eval$0$label_11_case_2#2; - - inline$v2.Eval$0$label_11_case_2#2: - assume v4.INT_EQ(inline$v2.Eval$0$op, 2); - assume v4.value_is(v2.__ctobpl_const_11, inline$v2.Eval$0$op); - goto inline$v2.Eval$0$label_14#2; - - inline$v2.Eval$0$label_14#2: - assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 29} true; - inline$v2.Eval$0$res := v4.MINUS_BOTH_PTR_OR_BOTH_INT(inline$v2.Eval$0$a1, inline$v2.Eval$0$a2, 1); - assume v4.value_is(v2.__ctobpl_const_18, inline$v2.Eval$0$res); - assume v4.value_is(v2.__ctobpl_const_19, inline$v2.Eval$0$a1); - assume v4.value_is(v2.__ctobpl_const_20, inline$v2.Eval$0$a2); - goto inline$v2.Eval$0$label_12#2; - - inline$v2.Eval$0$label_11_case_1#2: - assume v4.INT_EQ(inline$v2.Eval$0$op, 1); - assume v4.value_is(v2.__ctobpl_const_11, inline$v2.Eval$0$op); - goto inline$v2.Eval$0$label_13#2; - - inline$v2.Eval$0$label_13#2: - assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 27} true; - inline$v2.Eval$0$res := v4.PLUS(inline$v2.Eval$0$a1, 1, inline$v2.Eval$0$a2); - assume v4.value_is(v2.__ctobpl_const_15, inline$v2.Eval$0$res); - assume v4.value_is(v2.__ctobpl_const_16, inline$v2.Eval$0$a1); - assume v4.value_is(v2.__ctobpl_const_17, inline$v2.Eval$0$a2); - goto inline$v2.Eval$0$label_12#2; - - inline$v2.Eval$0$label_11_case_0#2: - assume v4.INT_NEQ(inline$v2.Eval$0$op, 1); - assume v4.INT_NEQ(inline$v2.Eval$0$op, 2); - assume v4.value_is(v2.__ctobpl_const_11, inline$v2.Eval$0$op); - goto inline$v2.Eval$0$label_12#2; - - inline$v2.Eval$0$label_12#2: - assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 35} true; - assert true; - v4.Mem_T.result__EXPR := v4.Mem_T.result__EXPR[v4.result__EXPR(inline$v2.Eval$0$e) := inline$v2.Eval$0$res]; - assume v4.value_is(v2.__ctobpl_const_12, inline$v2.Eval$0$e); - assume v4.value_is(v2.__ctobpl_const_13, v4.Mem_T.result__EXPR[v4.result__EXPR(inline$v2.Eval$0$e)]); - assume v4.value_is(v2.__ctobpl_const_14, inline$v2.Eval$0$res); - goto inline$v2.Eval$0$label_1#2; - - inline$v2.Eval$0$label_1#2: - assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 36} true; - goto inline$v2.Eval$0$Return; - - inline$v2.Eval$0$Return: - goto AA_INSTR_EQ_BODY$1; - - AA_INSTR_EQ_BODY$1: - AA_TEMP10 := v4.Mem_T.result__EXPR; - v4.Mem_T.result__EXPR := AA_TEMP00; - goto inline$v4.Eval$0$Entry; - - inline$v4.Eval$0$Entry: - inline$v4.Eval$0$e_.1 := e_.1; - inline$v4.Eval$0$v4.Mem_T.result__EXPR := v4.Mem_T.result__EXPR; - goto inline$v4.Eval$0$anon0#2; - - inline$v4.Eval$0$anon0#2: - inline$v4.Eval$0$havoc_stringTemp := 0; - goto inline$v4.Eval$0$start#2; - - inline$v4.Eval$0$start#2: - assume v4.INT_LT(inline$v4.Eval$0$e_.1, v4.alloc); - inline$v4.Eval$0$a1 := 0; - inline$v4.Eval$0$a2 := 0; - inline$v4.Eval$0$e := 0; - inline$v4.Eval$0$op := 0; - inline$v4.Eval$0$res := 0; - inline$v4.Eval$0$result.UnsignedAdd$1 := 0; - inline$v4.Eval$0$result.UnsignedSub$2 := 0; - inline$v4.Eval$0$e := inline$v4.Eval$0$e_.1; - goto inline$v4.Eval$0$label_3#2; - - inline$v4.Eval$0$label_3#2: - assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 19} true; - goto inline$v4.Eval$0$label_4#2; - - inline$v4.Eval$0$label_4#2: - assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 19} true; - goto inline$v4.Eval$0$label_5#2; - - inline$v4.Eval$0$label_5#2: - assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 19} true; - goto inline$v4.Eval$0$label_6#2; - - inline$v4.Eval$0$label_6#2: - assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 19} true; - goto inline$v4.Eval$0$label_7#2; - - inline$v4.Eval$0$label_7#2: - assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 21} true; - assert true; - inline$v4.Eval$0$op := v4.Mem_T.oper__EXPR[v4.oper__EXPR(inline$v4.Eval$0$e)]; - assume v4.value_is(v4.__ctobpl_const_1, inline$v4.Eval$0$op); - assume v4.value_is(v4.__ctobpl_const_2, inline$v4.Eval$0$e); - assume v4.value_is(v4.__ctobpl_const_3, v4.Mem_T.oper__EXPR[v4.oper__EXPR(inline$v4.Eval$0$e)]); - goto inline$v4.Eval$0$label_8#2; - - inline$v4.Eval$0$label_8#2: - assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 22} true; - assert true; - inline$v4.Eval$0$a1 := v4.Mem_T.op1__EXPR[v4.op1__EXPR(inline$v4.Eval$0$e)]; - assume v4.value_is(v4.__ctobpl_const_4, inline$v4.Eval$0$a1); - assume v4.value_is(v4.__ctobpl_const_5, inline$v4.Eval$0$e); - assume v4.value_is(v4.__ctobpl_const_6, v4.Mem_T.op1__EXPR[v4.op1__EXPR(inline$v4.Eval$0$e)]); - goto inline$v4.Eval$0$label_9#2; - - inline$v4.Eval$0$label_9#2: - assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 23} true; - assert true; - inline$v4.Eval$0$a2 := v4.Mem_T.op2__EXPR[v4.op2__EXPR(inline$v4.Eval$0$e)]; - assume v4.value_is(v4.__ctobpl_const_7, inline$v4.Eval$0$a2); - assume v4.value_is(v4.__ctobpl_const_8, inline$v4.Eval$0$e); - assume v4.value_is(v4.__ctobpl_const_9, v4.Mem_T.op2__EXPR[v4.op2__EXPR(inline$v4.Eval$0$e)]); - goto inline$v4.Eval$0$label_10#2; - - inline$v4.Eval$0$label_10#2: - assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 24} true; - inline$v4.Eval$0$res := 0 - 1; - assume v4.value_is(v4.__ctobpl_const_10, inline$v4.Eval$0$res); - goto inline$v4.Eval$0$label_11#2; - - inline$v4.Eval$0$label_11#2: - assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 26} true; - goto inline$v4.Eval$0$label_11_case_0#2, inline$v4.Eval$0$label_11_case_1#2, inline$v4.Eval$0$label_11_case_2#2; - - inline$v4.Eval$0$label_11_case_2#2: - assume v4.INT_EQ(inline$v4.Eval$0$op, 2); - assume v4.value_is(v4.__ctobpl_const_11, inline$v4.Eval$0$op); - goto inline$v4.Eval$0$label_14#2; - - inline$v4.Eval$0$label_14#2: - assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 35} true; - goto inline$v4.Eval$0$label_14_true#2, inline$v4.Eval$0$label_14_false#2; - - inline$v4.Eval$0$label_14_false#2: - assume v4.isUnsigned == 0; - assume v4.value_is(v4.__ctobpl_const_16, v4.isUnsigned); - goto inline$v4.Eval$0$label_15#2; - - inline$v4.Eval$0$label_15#2: - assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 38} true; - inline$v4.Eval$0$res := v4.MINUS_BOTH_PTR_OR_BOTH_INT(inline$v4.Eval$0$a1, inline$v4.Eval$0$a2, 1); - assume v4.value_is(v4.__ctobpl_const_17, inline$v4.Eval$0$res); - assume v4.value_is(v4.__ctobpl_const_18, inline$v4.Eval$0$a1); - assume v4.value_is(v4.__ctobpl_const_19, inline$v4.Eval$0$a2); - goto inline$v4.Eval$0$label_12#2; - - inline$v4.Eval$0$label_14_true#2: - assume v4.isUnsigned != 0; - assume v4.value_is(v4.__ctobpl_const_16, v4.isUnsigned); - goto inline$v4.Eval$0$label_16#2; - - inline$v4.Eval$0$label_16#2: - assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 36} true; - call inline$v4.Eval$0$result.UnsignedSub$2 := v4.UnsignedSub(inline$v4.Eval$0$a1, inline$v4.Eval$0$a2); - assume v4.value_is(v4.__ctobpl_const_20, inline$v4.Eval$0$a1); - assume v4.value_is(v4.__ctobpl_const_21, inline$v4.Eval$0$a2); - assume v4.value_is(v4.__ctobpl_const_22, inline$v4.Eval$0$a1); - assume v4.value_is(v4.__ctobpl_const_23, inline$v4.Eval$0$a2); - goto inline$v4.Eval$0$label_19#2; - - inline$v4.Eval$0$label_19#2: - assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 36} true; - inline$v4.Eval$0$res := inline$v4.Eval$0$result.UnsignedSub$2; - assume v4.value_is(v4.__ctobpl_const_24, inline$v4.Eval$0$res); - assume v4.value_is(v4.__ctobpl_const_25, inline$v4.Eval$0$result.UnsignedSub$2); - goto inline$v4.Eval$0$label_12#2; - - inline$v4.Eval$0$label_11_case_1#2: - assume v4.INT_EQ(inline$v4.Eval$0$op, 1); - assume v4.value_is(v4.__ctobpl_const_11, inline$v4.Eval$0$op); - goto inline$v4.Eval$0$label_13#2; - - inline$v4.Eval$0$label_13#2: - assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 29} true; - goto inline$v4.Eval$0$label_13_true#2, inline$v4.Eval$0$label_13_false#2; - - inline$v4.Eval$0$label_13_false#2: - assume v4.isUnsigned == 0; - assume v4.value_is(v4.__ctobpl_const_15, v4.isUnsigned); - goto inline$v4.Eval$0$label_20#2; - - inline$v4.Eval$0$label_20#2: - assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 32} true; - inline$v4.Eval$0$res := v4.PLUS(inline$v4.Eval$0$a1, 1, inline$v4.Eval$0$a2); - assume v4.value_is(v4.__ctobpl_const_26, inline$v4.Eval$0$res); - assume v4.value_is(v4.__ctobpl_const_27, inline$v4.Eval$0$a1); - assume v4.value_is(v4.__ctobpl_const_28, inline$v4.Eval$0$a2); - goto inline$v4.Eval$0$label_12#2; - - inline$v4.Eval$0$label_13_true#2: - assume v4.isUnsigned != 0; - assume v4.value_is(v4.__ctobpl_const_15, v4.isUnsigned); - goto inline$v4.Eval$0$label_21#2; - - inline$v4.Eval$0$label_21#2: - assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 30} true; - call inline$v4.Eval$0$result.UnsignedAdd$1 := v4.UnsignedAdd(inline$v4.Eval$0$a1, inline$v4.Eval$0$a2); - assume v4.value_is(v4.__ctobpl_const_29, inline$v4.Eval$0$a1); - assume v4.value_is(v4.__ctobpl_const_30, inline$v4.Eval$0$a2); - assume v4.value_is(v4.__ctobpl_const_31, inline$v4.Eval$0$a1); - assume v4.value_is(v4.__ctobpl_const_32, inline$v4.Eval$0$a2); - goto inline$v4.Eval$0$label_24#2; - - inline$v4.Eval$0$label_24#2: - assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 30} true; - inline$v4.Eval$0$res := inline$v4.Eval$0$result.UnsignedAdd$1; - assume v4.value_is(v4.__ctobpl_const_33, inline$v4.Eval$0$res); - assume v4.value_is(v4.__ctobpl_const_34, inline$v4.Eval$0$result.UnsignedAdd$1); - goto inline$v4.Eval$0$label_12#2; - - inline$v4.Eval$0$label_11_case_0#2: - assume v4.INT_NEQ(inline$v4.Eval$0$op, 1); - assume v4.INT_NEQ(inline$v4.Eval$0$op, 2); - assume v4.value_is(v4.__ctobpl_const_11, inline$v4.Eval$0$op); - goto inline$v4.Eval$0$label_12#2; - - inline$v4.Eval$0$label_12#2: - assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 41} true; - assert true; - v4.Mem_T.result__EXPR := v4.Mem_T.result__EXPR[v4.result__EXPR(inline$v4.Eval$0$e) := inline$v4.Eval$0$res]; - assume v4.value_is(v4.__ctobpl_const_12, inline$v4.Eval$0$e); - assume v4.value_is(v4.__ctobpl_const_13, v4.Mem_T.result__EXPR[v4.result__EXPR(inline$v4.Eval$0$e)]); - assume v4.value_is(v4.__ctobpl_const_14, inline$v4.Eval$0$res); - goto inline$v4.Eval$0$label_1#2; - - inline$v4.Eval$0$label_1#2: - assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 42} true; - goto inline$v4.Eval$0$Return; - - inline$v4.Eval$0$Return: - goto AA_INSTR_EQ_BODY$2; - - AA_INSTR_EQ_BODY$2: - Output_of_v2.Eval_v4.Mem_T.result__EXPR := AA_TEMP10; - Output_of_v4.Eval_v4.Mem_T.result__EXPR := v4.Mem_T.result__EXPR; - AA_TEMP30 := AA_TEMP10 == v4.Mem_T.result__EXPR || (forall _x0: int :: AA_TEMP10[_x0] == v4.Mem_T.result__EXPR[_x0]); - return; -} - - - -var Output_of_v2.EvalEntry1_v4.Mem_T.result__EXPR: [int]int; - -var Output_of_v4.EvalEntry1_v4.Mem_T.result__EXPR: [int]int; - -var Output_of_v2.EvalEntry1_v4.Mem_T.INT4: [int]int; - -var Output_of_v4.EvalEntry1_v4.Mem_T.INT4: [int]int; - -var Output_of_v2.EvalEntry1_v4.isUnsigned: int; - -var Output_of_v4.EvalEntry1_v4.isUnsigned: int; - -procedure EQ_v2.EvalEntry1__v4.EvalEntry1(e_.1: int, outval_.1: int) returns (AA_TEMP80: bool, AA_TEMP81: bool, AA_TEMP82: bool); - modifies v4.Mem_T.result__EXPR, v4.Mem_T.INT4, v4.isUnsigned, Output_of_v2.EvalEntry1_v4.Mem_T.result__EXPR, Output_of_v4.EvalEntry1_v4.Mem_T.result__EXPR, Output_of_v2.EvalEntry1_v4.Mem_T.INT4, Output_of_v4.EvalEntry1_v4.Mem_T.INT4, Output_of_v2.EvalEntry1_v4.isUnsigned, Output_of_v4.EvalEntry1_v4.isUnsigned; - ensures AA_TEMP82 && AA_TEMP81 && AA_TEMP80; - - - -implementation EQ_v2.EvalEntry1__v4.EvalEntry1(e_.1: int, outval_.1: int) returns (AA_TEMP80: bool, AA_TEMP81: bool, AA_TEMP82: bool) -{ - var AA_TEMP60: [int]int; - var AA_TEMP61: [int]int; - var AA_TEMP62: int; - var AA_TEMP50: [int]int; - var AA_TEMP51: [int]int; - var AA_TEMP52: int; - - AA_INSTR_EQ_BODY: - AA_TEMP50 := v4.Mem_T.result__EXPR; - AA_TEMP51 := v4.Mem_T.INT4; - AA_TEMP52 := v4.isUnsigned; - call v2.EvalEntry1(e_.1, outval_.1); - AA_TEMP60 := v4.Mem_T.result__EXPR; - AA_TEMP61 := v4.Mem_T.INT4; - AA_TEMP62 := v4.isUnsigned; - v4.Mem_T.result__EXPR := AA_TEMP50; - v4.Mem_T.INT4 := AA_TEMP51; - v4.isUnsigned := AA_TEMP52; - call v4.EvalEntry1(e_.1, outval_.1); - Output_of_v2.EvalEntry1_v4.Mem_T.result__EXPR := AA_TEMP60; - Output_of_v4.EvalEntry1_v4.Mem_T.result__EXPR := v4.Mem_T.result__EXPR; - Output_of_v2.EvalEntry1_v4.Mem_T.INT4 := AA_TEMP61; - Output_of_v4.EvalEntry1_v4.Mem_T.INT4 := v4.Mem_T.INT4; - Output_of_v2.EvalEntry1_v4.isUnsigned := AA_TEMP62; - Output_of_v4.EvalEntry1_v4.isUnsigned := v4.isUnsigned; - AA_TEMP80, AA_TEMP81, AA_TEMP82 := AA_TEMP60 == v4.Mem_T.result__EXPR || (forall _x0: int :: AA_TEMP60[_x0] == v4.Mem_T.result__EXPR[_x0]), AA_TEMP61 == v4.Mem_T.INT4 || (forall _x0: int :: AA_TEMP61[_x0] == v4.Mem_T.INT4[_x0]), AA_TEMP62 == v4.isUnsigned; - return; -} - - - -var Output_of_v2.EvalEntry2_v4.Mem_T.result__EXPR: [int]int; - -var Output_of_v4.EvalEntry2_v4.Mem_T.result__EXPR: [int]int; - -var Output_of_v2.EvalEntry2_v4.isUnsigned: int; - -var Output_of_v4.EvalEntry2_v4.isUnsigned: int; - -procedure EQ_v2.EvalEntry2__v4.EvalEntry2(e_.1: int) returns (AA_TEMP130: bool, AA_TEMP131: bool); - modifies v4.Mem_T.result__EXPR, v4.isUnsigned, Output_of_v2.EvalEntry2_v4.Mem_T.result__EXPR, Output_of_v4.EvalEntry2_v4.Mem_T.result__EXPR, Output_of_v2.EvalEntry2_v4.isUnsigned, Output_of_v4.EvalEntry2_v4.isUnsigned; - ensures AA_TEMP131 && AA_TEMP130; - - - -implementation EQ_v2.EvalEntry2__v4.EvalEntry2(e_.1: int) returns (AA_TEMP130: bool, AA_TEMP131: bool) -{ - var AA_TEMP110: [int]int; - var AA_TEMP111: int; - var AA_TEMP100: [int]int; - var AA_TEMP101: int; - - AA_INSTR_EQ_BODY: - AA_TEMP100 := v4.Mem_T.result__EXPR; - AA_TEMP101 := v4.isUnsigned; - call v2.EvalEntry2(e_.1); - AA_TEMP110 := v4.Mem_T.result__EXPR; - AA_TEMP111 := v4.isUnsigned; - v4.Mem_T.result__EXPR := AA_TEMP100; - v4.isUnsigned := AA_TEMP101; - call v4.EvalEntry2(e_.1); - Output_of_v2.EvalEntry2_v4.Mem_T.result__EXPR := AA_TEMP110; - Output_of_v4.EvalEntry2_v4.Mem_T.result__EXPR := v4.Mem_T.result__EXPR; - Output_of_v2.EvalEntry2_v4.isUnsigned := AA_TEMP111; - Output_of_v4.EvalEntry2_v4.isUnsigned := v4.isUnsigned; - AA_TEMP130, AA_TEMP131 := AA_TEMP110 == v4.Mem_T.result__EXPR || (forall _x0: int :: AA_TEMP110[_x0] == v4.Mem_T.result__EXPR[_x0]), AA_TEMP111 == v4.isUnsigned; - return; -} - - - -function _uf_v4.__HAVOC_malloc_new(arg_0: int) : int; - -function _uf_v2.__HAVOC_malloc_new(arg_0: int) : int; - -function _uf_v4.__HAVOC_det_malloc_new(arg_0: int) : int; - -function _uf_v2.__HAVOC_det_malloc_new(arg_0: int) : int; - -function _uf_v4.__HAVOC_memset_split_1_ret(arg_0: [int]int, arg_1: int, arg_2: int, arg_3: int) : [int]int; - -function _uf_v2.__HAVOC_memset_split_1_ret(arg_0: [int]int, arg_1: int, arg_2: int, arg_3: int) : [int]int; - -function _uf_v4.__HAVOC_memset_split_2_ret(arg_0: [int]int, arg_1: int, arg_2: int, arg_3: int) : [int]int; - -function _uf_v2.__HAVOC_memset_split_2_ret(arg_0: [int]int, arg_1: int, arg_2: int, arg_3: int) : [int]int; - -function _uf_v4.__HAVOC_memset_split_4_ret(arg_0: [int]int, arg_1: int, arg_2: int, arg_3: int) : [int]int; - -function _uf_v2.__HAVOC_memset_split_4_ret(arg_0: [int]int, arg_1: int, arg_2: int, arg_3: int) : [int]int; - -function _uf_v4.nondet_choice_x() : int; - -function _uf_v2.nondet_choice_x() : int; - -function _uf_v4.det_choice_x() : int; - -function _uf_v2.det_choice_x() : int; - -function _uf_v4._strdup_new(arg_0: int) : int; - -function _uf_v2._strdup_new(arg_0: int) : int; - -function _uf_v4._xstrcasecmp_ret(arg_0: int, arg_1: int) : int; - -function _uf_v2._xstrcasecmp_ret(arg_0: int, arg_1: int) : int; - -function _uf_v4._xstrcmp_ret(arg_0: int, arg_1: int) : int; - -function _uf_v2._xstrcmp_ret(arg_0: int, arg_1: int) : int; - -function _uf_v4.Eval_v4.Mem_T.result__EXPR(arg_0: int, arg_1: int, arg_2: [int]int, arg_3: [int]int, arg_4: [int]int, arg_5: [int]int, arg_6: int) : [int]int; - -function _uf_v2.Eval_v4.Mem_T.result__EXPR(arg_0: int, arg_1: int, arg_2: [int]int, arg_3: [int]int, arg_4: [int]int, arg_5: [int]int, arg_6: int) : [int]int; - -function _uf_v4.EvalEntry1_v4.Mem_T.result__EXPR(arg_0: int, arg_1: int, arg_2: int, arg_3: [int]int, arg_4: [int]int, arg_5: [int]int, arg_6: [int]int, arg_7: [int]int, arg_8: int) : [int]int; - -function _uf_v4.EvalEntry1_v4.Mem_T.INT4(arg_0: int, arg_1: int, arg_2: int, arg_3: [int]int, arg_4: [int]int, arg_5: [int]int, arg_6: [int]int, arg_7: [int]int, arg_8: int) : [int]int; - -function _uf_v4.EvalEntry1_v4.isUnsigned(arg_0: int, arg_1: int, arg_2: int, arg_3: [int]int, arg_4: [int]int, arg_5: [int]int, arg_6: [int]int, arg_7: [int]int, arg_8: int) : int; - -function _uf_v2.EvalEntry1_v4.Mem_T.result__EXPR(arg_0: int, arg_1: int, arg_2: int, arg_3: [int]int, arg_4: [int]int, arg_5: [int]int, arg_6: [int]int, arg_7: [int]int, arg_8: int) : [int]int; - -function _uf_v2.EvalEntry1_v4.Mem_T.INT4(arg_0: int, arg_1: int, arg_2: int, arg_3: [int]int, arg_4: [int]int, arg_5: [int]int, arg_6: [int]int, arg_7: [int]int, arg_8: int) : [int]int; - -function _uf_v4.EvalEntry2_v4.Mem_T.result__EXPR(arg_0: int, arg_1: int, arg_2: [int]int, arg_3: [int]int, arg_4: [int]int, arg_5: [int]int, arg_6: int) : [int]int; - -function _uf_v4.EvalEntry2_v4.isUnsigned(arg_0: int, arg_1: int, arg_2: [int]int, arg_3: [int]int, arg_4: [int]int, arg_5: [int]int, arg_6: int) : int; - -function _uf_v2.EvalEntry2_v4.Mem_T.result__EXPR(arg_0: int, arg_1: int, arg_2: [int]int, arg_3: [int]int, arg_4: [int]int, arg_5: [int]int, arg_6: int) : [int]int; +// RUN: %boogie -typeEncoding:m -z3multipleErrors "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +var v4.Mem: [name][int]int; + +var v4.alloc: int; + +var v4.Mem_T.INT4: [int]int; + +var v4.Mem_T.op1__EXPR: [int]int; + +var v4.Mem_T.op2__EXPR: [int]int; + +var v4.Mem_T.oper__EXPR: [int]int; + +var v4.Mem_T.result__EXPR: [int]int; + +var v4.detChoiceCnt: int; + +var v4.Res_KERNEL_SOURCE: [int]int; + +var v4.Res_PROBED: [int]int; + +var v4.isUnsigned: int; + +const unique v4.T.oper__EXPR: name; + +const unique v4.T.op1__EXPR: name; + +const unique v4.T.op2__EXPR: name; + +const unique v4.T.result__EXPR: name; + +const unique v4.T.INT4: name; + +const unique v4.T.PINT4: name; + +const unique v4.T.PPINT4: name; + +const unique v4.T.PP_EXPR: name; + +const unique v4.T.P_EXPR: name; + +const unique v4.T._EXPR: name; + +const {:model_const "e->op2"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 23} unique v4.__ctobpl_const_9: int; + +const {:model_const "res"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 24} unique v4.__ctobpl_const_10: int; + +const {:model_const "op"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 26} unique v4.__ctobpl_const_11: int; + +const {:model_const "e"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 41} unique v4.__ctobpl_const_12: int; + +const {:model_const "e->op1"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 22} unique v4.__ctobpl_const_6: int; + +const {:model_const "a2"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 23} unique v4.__ctobpl_const_7: int; + +const {:model_const "e"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 23} unique v4.__ctobpl_const_8: int; + +const {:model_const "e->oper"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 21} unique v4.__ctobpl_const_3: int; + +const {:model_const "op"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 21} unique v4.__ctobpl_const_1: int; + +const {:model_const "e"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 21} unique v4.__ctobpl_const_2: int; + +const {:model_const "e->result"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 41} unique v4.__ctobpl_const_13: int; + +const {:model_const "res"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 41} unique v4.__ctobpl_const_14: int; + +const {:model_const "isUnsigned"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 29} unique v4.__ctobpl_const_15: int; + +const {:model_const "isUnsigned"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 35} unique v4.__ctobpl_const_16: int; + +const {:model_const "res"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 38} unique v4.__ctobpl_const_17: int; + +const {:model_const "a1"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 38} unique v4.__ctobpl_const_18: int; + +const {:model_const "a2"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 38} unique v4.__ctobpl_const_19: int; + +const {:model_const "a1"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 36} unique v4.__ctobpl_const_20: int; + +const {:model_const "a2"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 36} unique v4.__ctobpl_const_21: int; + +const {:model_const "a1"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 36} unique v4.__ctobpl_const_22: int; + +const {:model_const "a2"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 36} unique v4.__ctobpl_const_23: int; + +const {:model_const "res"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 36} unique v4.__ctobpl_const_24: int; + +const {:model_const "result.UnsignedSub"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 36} unique v4.__ctobpl_const_25: int; + +const {:model_const "res"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 32} unique v4.__ctobpl_const_26: int; + +const {:model_const "a1"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 32} unique v4.__ctobpl_const_27: int; + +const {:model_const "a2"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 32} unique v4.__ctobpl_const_28: int; + +const {:model_const "a1"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 30} unique v4.__ctobpl_const_29: int; + +const {:model_const "a2"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 30} unique v4.__ctobpl_const_30: int; + +const {:model_const "a1"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 30} unique v4.__ctobpl_const_31: int; + +const {:model_const "a2"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 30} unique v4.__ctobpl_const_32: int; + +const {:model_const "res"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 30} unique v4.__ctobpl_const_33: int; + +const {:model_const "result.UnsignedAdd"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 30} unique v4.__ctobpl_const_34: int; + +const {:model_const "isUnsigned"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 47} unique v4.__ctobpl_const_35: int; + +const {:model_const "a1"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 22} unique v4.__ctobpl_const_4: int; + +const {:model_const "e"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 22} unique v4.__ctobpl_const_5: int; + +const {:model_const "e"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 48} unique v4.__ctobpl_const_36: int; + +const {:model_const "e"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 48} unique v4.__ctobpl_const_37: int; + +const {:model_const "outval"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 49} unique v4.__ctobpl_const_38: int; + +const {:model_const "*outval"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 49} unique v4.__ctobpl_const_39: int; + +const {:model_const "e"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 49} unique v4.__ctobpl_const_40: int; + +const {:model_const "e->result"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 49} unique v4.__ctobpl_const_41: int; + +const {:model_const "isUnsigned"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 54} unique v4.__ctobpl_const_42: int; + +const {:model_const "e"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 55} unique v4.__ctobpl_const_43: int; + +const {:model_const "e"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 55} unique v4.__ctobpl_const_44: int; + +function v4.OneByteToInt(arg_0: byte) : int; + +function v4.TwoBytesToInt(arg_0: byte, arg_1: byte) : int; + +function v4.FourBytesToInt(arg_0: byte, arg_1: byte, arg_2: byte, arg_3: byte) : int; + +function v4.Field(arg_0: int) : name; + +function v4.Base(arg_0: int) : int; + +function v4.Match(a: int, t: name) : bool; + +function v4.MatchBase(b: int, a: int, t: name) : bool; + +function v4.HasType(v: int, t: name) : bool; + +function v4.T.Ptr(t: name) : name; + +function v4.op1__EXPR(arg_0: int) : int; + +function v4.op1__EXPRInv(arg_0: int) : int; + +function v4._S_op1__EXPR(arg_0: [int]bool) : [int]bool; + +function v4._S_op1__EXPRInv(arg_0: [int]bool) : [int]bool; + +function v4.op2__EXPR(arg_0: int) : int; + +function v4.op2__EXPRInv(arg_0: int) : int; + +function v4._S_op2__EXPR(arg_0: [int]bool) : [int]bool; + +function v4._S_op2__EXPRInv(arg_0: [int]bool) : [int]bool; + +function v4.oper__EXPR(arg_0: int) : int; + +function v4.oper__EXPRInv(arg_0: int) : int; + +function v4._S_oper__EXPR(arg_0: [int]bool) : [int]bool; + +function v4._S_oper__EXPRInv(arg_0: [int]bool) : [int]bool; + +function v4.result__EXPR(arg_0: int) : int; + +function v4.result__EXPRInv(arg_0: int) : int; + +function v4._S_result__EXPR(arg_0: [int]bool) : [int]bool; + +function v4._S_result__EXPRInv(arg_0: [int]bool) : [int]bool; + +function v4.INT_EQ(x: int, y: int) : bool; + +function v4.INT_NEQ(x: int, y: int) : bool; + +function v4.INT_ADD(x: int, y: int) : int; + +function v4.INT_SUB(x: int, y: int) : int; + +function v4.INT_MULT(x: int, y: int) : int; + +function v4.INT_DIV(x: int, y: int) : int; + +function v4.INT_LT(x: int, y: int) : bool; + +function v4.INT_ULT(x: int, y: int) : bool; + +function v4.INT_LEQ(x: int, y: int) : bool; + +function v4.INT_ULEQ(x: int, y: int) : bool; + +function v4.INT_GT(x: int, y: int) : bool; + +function v4.INT_UGT(x: int, y: int) : bool; + +function v4.INT_GEQ(x: int, y: int) : bool; + +function v4.INT_UGEQ(x: int, y: int) : bool; + +function v4.BV32_EQ(x: bv32, y: bv32) : bool; + +function v4.BV32_NEQ(x: bv32, y: bv32) : bool; + +function {:bvbuiltin "bvadd"} v4.BV32_ADD(x: bv32, y: bv32) : bv32; + +function {:bvbuiltin "bvsub"} v4.BV32_SUB(x: bv32, y: bv32) : bv32; + +function {:bvbuiltin "bvmul"} v4.BV32_MULT(x: bv32, y: bv32) : bv32; + +function {:bvbuiltin "bvudiv"} v4.BV32_DIV(x: bv32, y: bv32) : bv32; + +function {:bvbuiltin "bvult"} v4.BV32_ULT(x: bv32, y: bv32) : bool; + +function {:bvbuiltin "bvslt"} v4.BV32_LT(x: bv32, y: bv32) : bool; + +function {:bvbuiltin "bvule"} v4.BV32_ULEQ(x: bv32, y: bv32) : bool; + +function {:bvbuiltin "bvsle"} v4.BV32_LEQ(x: bv32, y: bv32) : bool; + +function {:bvbuiltin "bvugt"} v4.BV32_UGT(x: bv32, y: bv32) : bool; + +function {:bvbuiltin "bvsgt"} v4.BV32_GT(x: bv32, y: bv32) : bool; + +function {:bvbuiltin "bvuge"} v4.BV32_UGEQ(x: bv32, y: bv32) : bool; + +function {:bvbuiltin "bvsge"} v4.BV32_GEQ(x: bv32, y: bv32) : bool; + +function v4.MINUS_BOTH_PTR_OR_BOTH_INT(a: int, b: int, size: int) : int; + +function v4.MINUS_LEFT_PTR(a: int, a_size: int, b: int) : int; + +function v4.PLUS(a: int, a_size: int, b: int) : int; + +function v4.MULT(a: int, b: int) : int; + +function v4.DIV(a: int, b: int) : int; + +function v4.BINARY_BOTH_INT(a: int, b: int) : int; + +function v4.POW2(a: int) : bool; + +function v4.BIT_BAND(a: int, b: int) : int; + +function v4.BIT_BOR(a: int, b: int) : int; + +function v4.BIT_BXOR(a: int, b: int) : int; + +function v4.BIT_BNOT(a: int) : int; + +function v4.choose(a: bool, b: int, c: int) : int; + +function v4.LIFT(a: bool) : int; + +function v4.PTR_NOT(a: int) : int; + +function v4.NULL_CHECK(a: int) : int; + +function v4.NewAlloc(x: int, y: int) : int; + +function v4.DetChoiceFunc(a: int) : int; + +function v4.Equal(arg_0: [int]bool, arg_1: [int]bool) : bool; + +function v4.Subset(arg_0: [int]bool, arg_1: [int]bool) : bool; + +function v4.Disjoint(arg_0: [int]bool, arg_1: [int]bool) : bool; + +function v4.Empty() : [int]bool; + +function v4.SetTrue() : [int]bool; + +function v4.Singleton(arg_0: int) : [int]bool; + +function v4.Reachable(arg_0: [int,int]bool, arg_1: int) : [int]bool; + +function v4.Union(arg_0: [int]bool, arg_1: [int]bool) : [int]bool; + +function v4.Intersection(arg_0: [int]bool, arg_1: [int]bool) : [int]bool; + +function v4.Difference(arg_0: [int]bool, arg_1: [int]bool) : [int]bool; + +function v4.Dereference(arg_0: [int]bool, arg_1: [int]int) : [int]bool; + +function v4.Inverse(f: [int]int, x: int) : [int]bool; + +function v4.AtLeast(arg_0: int, arg_1: int) : [int]bool; + +function v4.Rep(arg_0: int, arg_1: int) : int; + +function v4.Array(arg_0: int, arg_1: int, arg_2: int) : [int]bool; + +function v4.Unified(arg_0: [name][int]int) : [int]int; + +function v4.value_is(c: int, e: int) : bool; + +axiom (forall b0: byte, c0: byte :: { v4.OneByteToInt(b0), v4.OneByteToInt(c0) } v4.OneByteToInt(b0) == v4.OneByteToInt(c0) ==> b0 == c0); + +axiom (forall b0: byte, b1: byte, c0: byte, c1: byte :: { v4.TwoBytesToInt(b0, b1), v4.TwoBytesToInt(c0, c1) } v4.TwoBytesToInt(b0, b1) == v4.TwoBytesToInt(c0, c1) ==> b0 == c0 && b1 == c1); + +axiom (forall b0: byte, b1: byte, b2: byte, b3: byte, c0: byte, c1: byte, c2: byte, c3: byte :: { v4.FourBytesToInt(b0, b1, b2, b3), v4.FourBytesToInt(c0, c1, c2, c3) } v4.FourBytesToInt(b0, b1, b2, b3) == v4.FourBytesToInt(c0, c1, c2, c3) ==> b0 == c0 && b1 == c1 && b2 == c2 && b3 == c3); + +axiom (forall x: int :: { v4.Base(x) } v4.INT_LEQ(v4.Base(x), x)); + +axiom (forall a: int, t: name :: { v4.Match(a, v4.T.Ptr(t)) } v4.Match(a, v4.T.Ptr(t)) <==> v4.Field(a) == v4.T.Ptr(t)); + +axiom (forall b: int, a: int, t: name :: { v4.MatchBase(b, a, v4.T.Ptr(t)) } v4.MatchBase(b, a, v4.T.Ptr(t)) <==> v4.Base(a) == b); + +axiom (forall v: int, t: name :: { v4.HasType(v, v4.T.Ptr(t)) } v4.HasType(v, v4.T.Ptr(t)) <==> v == 0 || (v4.INT_GT(v, 0) && v4.Match(v, t) && v4.MatchBase(v4.Base(v), v, t))); + +axiom (forall x: int, S: [int]bool :: { v4._S_op1__EXPR(S)[x] } v4._S_op1__EXPR(S)[x] <==> S[v4.op1__EXPRInv(x)]); + +axiom (forall x: int, S: [int]bool :: { v4._S_op1__EXPRInv(S)[x] } v4._S_op1__EXPRInv(S)[x] <==> S[v4.op1__EXPR(x)]); + +axiom (forall x: int, S: [int]bool :: { S[x], v4._S_op1__EXPR(S) } S[x] ==> v4._S_op1__EXPR(S)[v4.op1__EXPR(x)]); + +axiom (forall x: int, S: [int]bool :: { S[x], v4._S_op1__EXPRInv(S) } S[x] ==> v4._S_op1__EXPRInv(S)[v4.op1__EXPRInv(x)]); + +axiom (forall x: int :: { v4.op1__EXPR(x) } v4.op1__EXPR(x) == v4.INT_ADD(x, 4)); + +axiom (forall x: int :: { v4.op1__EXPRInv(x) } v4.op1__EXPRInv(x) == v4.INT_SUB(x, 4)); + +axiom (forall x: int :: { v4.op1__EXPR(x) } v4.op1__EXPR(x) == v4.PLUS(x, 1, 4)); + +axiom (forall x: int, S: [int]bool :: { v4._S_op2__EXPR(S)[x] } v4._S_op2__EXPR(S)[x] <==> S[v4.op2__EXPRInv(x)]); + +axiom (forall x: int, S: [int]bool :: { v4._S_op2__EXPRInv(S)[x] } v4._S_op2__EXPRInv(S)[x] <==> S[v4.op2__EXPR(x)]); + +axiom (forall x: int, S: [int]bool :: { S[x], v4._S_op2__EXPR(S) } S[x] ==> v4._S_op2__EXPR(S)[v4.op2__EXPR(x)]); + +axiom (forall x: int, S: [int]bool :: { S[x], v4._S_op2__EXPRInv(S) } S[x] ==> v4._S_op2__EXPRInv(S)[v4.op2__EXPRInv(x)]); + +axiom (forall x: int :: { v4.op2__EXPR(x) } v4.op2__EXPR(x) == v4.INT_ADD(x, 8)); + +axiom (forall x: int :: { v4.op2__EXPRInv(x) } v4.op2__EXPRInv(x) == v4.INT_SUB(x, 8)); + +axiom (forall x: int :: { v4.op2__EXPR(x) } v4.op2__EXPR(x) == v4.PLUS(x, 1, 8)); + +axiom (forall x: int, S: [int]bool :: { v4._S_oper__EXPR(S)[x] } v4._S_oper__EXPR(S)[x] <==> S[v4.oper__EXPRInv(x)]); + +axiom (forall x: int, S: [int]bool :: { v4._S_oper__EXPRInv(S)[x] } v4._S_oper__EXPRInv(S)[x] <==> S[v4.oper__EXPR(x)]); + +axiom (forall x: int, S: [int]bool :: { S[x], v4._S_oper__EXPR(S) } S[x] ==> v4._S_oper__EXPR(S)[v4.oper__EXPR(x)]); + +axiom (forall x: int, S: [int]bool :: { S[x], v4._S_oper__EXPRInv(S) } S[x] ==> v4._S_oper__EXPRInv(S)[v4.oper__EXPRInv(x)]); + +axiom (forall x: int :: { v4.oper__EXPR(x) } v4.oper__EXPR(x) == v4.INT_ADD(x, 0)); + +axiom (forall x: int :: { v4.oper__EXPRInv(x) } v4.oper__EXPRInv(x) == v4.INT_SUB(x, 0)); + +axiom (forall x: int :: { v4.oper__EXPR(x) } v4.oper__EXPR(x) == v4.PLUS(x, 1, 0)); + +axiom (forall x: int, S: [int]bool :: { v4._S_result__EXPR(S)[x] } v4._S_result__EXPR(S)[x] <==> S[v4.result__EXPRInv(x)]); + +axiom (forall x: int, S: [int]bool :: { v4._S_result__EXPRInv(S)[x] } v4._S_result__EXPRInv(S)[x] <==> S[v4.result__EXPR(x)]); + +axiom (forall x: int, S: [int]bool :: { S[x], v4._S_result__EXPR(S) } S[x] ==> v4._S_result__EXPR(S)[v4.result__EXPR(x)]); + +axiom (forall x: int, S: [int]bool :: { S[x], v4._S_result__EXPRInv(S) } S[x] ==> v4._S_result__EXPRInv(S)[v4.result__EXPRInv(x)]); + +axiom (forall x: int :: { v4.result__EXPR(x) } v4.result__EXPR(x) == v4.INT_ADD(x, 12)); + +axiom (forall x: int :: { v4.result__EXPRInv(x) } v4.result__EXPRInv(x) == v4.INT_SUB(x, 12)); + +axiom (forall x: int :: { v4.result__EXPR(x) } v4.result__EXPR(x) == v4.PLUS(x, 1, 12)); + +axiom (forall x: int, y: int :: { v4.INT_EQ(x, y): bool } v4.INT_EQ(x, y): bool <==> x == y); + +axiom (forall x: int, y: int :: { v4.INT_NEQ(x, y): bool } v4.INT_NEQ(x, y): bool <==> x != y); + +axiom (forall x: int, y: int :: { v4.INT_ADD(x, y): int } v4.INT_ADD(x, y): int == x + y); + +axiom (forall x: int, y: int :: { v4.INT_SUB(x, y): int } v4.INT_SUB(x, y): int == x - y); + +axiom (forall x: int, y: int :: { v4.INT_MULT(x, y): int } v4.INT_MULT(x, y): int == x * y); + +axiom (forall x: int, y: int :: { v4.INT_DIV(x, y): int } v4.INT_DIV(x, y): int == x div y); + +axiom (forall x: int, y: int :: { v4.INT_LT(x, y): bool } v4.INT_LT(x, y): bool <==> x < y); + +axiom (forall x: int, y: int :: { v4.INT_ULT(x, y): bool } v4.INT_ULT(x, y): bool <==> x < y); + +axiom (forall x: int, y: int :: { v4.INT_LEQ(x, y): bool } v4.INT_LEQ(x, y): bool <==> x <= y); + +axiom (forall x: int, y: int :: { v4.INT_ULEQ(x, y): bool } v4.INT_ULEQ(x, y): bool <==> x <= y); + +axiom (forall x: int, y: int :: { v4.INT_GT(x, y): bool } v4.INT_GT(x, y): bool <==> x > y); + +axiom (forall x: int, y: int :: { v4.INT_UGT(x, y): bool } v4.INT_UGT(x, y): bool <==> x > y); + +axiom (forall x: int, y: int :: { v4.INT_GEQ(x, y): bool } v4.INT_GEQ(x, y): bool <==> x >= y); + +axiom (forall x: int, y: int :: { v4.INT_UGEQ(x, y): bool } v4.INT_UGEQ(x, y): bool <==> x >= y); + +axiom (forall x: bv32, y: bv32 :: { v4.BV32_EQ(x, y): bool } v4.BV32_EQ(x, y): bool <==> x == y); + +axiom (forall x: bv32, y: bv32 :: { v4.BV32_NEQ(x, y): bool } v4.BV32_NEQ(x, y): bool <==> x != y); + +axiom (forall a: int, b: int, size: int :: { v4.MINUS_BOTH_PTR_OR_BOTH_INT(a, b, size) } v4.INT_LEQ(v4.INT_MULT(size, v4.MINUS_BOTH_PTR_OR_BOTH_INT(a, b, size)), v4.INT_SUB(a, b)) && v4.INT_LT(v4.INT_SUB(a, b), v4.INT_MULT(size, v4.INT_ADD(v4.MINUS_BOTH_PTR_OR_BOTH_INT(a, b, size), 1)))); + +axiom (forall a: int, b: int, size: int :: { v4.MINUS_BOTH_PTR_OR_BOTH_INT(a, b, size) } v4.MINUS_BOTH_PTR_OR_BOTH_INT(a, b, 1) == v4.INT_SUB(a, b)); + +axiom (forall a: int, a_size: int, b: int :: { v4.MINUS_LEFT_PTR(a, a_size, b) } v4.MINUS_LEFT_PTR(a, a_size, b) == v4.INT_SUB(a, v4.INT_MULT(a_size, b))); + +axiom (forall a: int, a_size: int, b: int :: { v4.PLUS(a, a_size, b) } v4.PLUS(a, a_size, b) == v4.INT_ADD(a, v4.INT_MULT(a_size, b))); + +axiom (forall a: int, b: int :: { v4.MULT(a, b) } v4.MULT(a, b) == v4.INT_MULT(a, b)); + +axiom (forall a: int, b: int :: { v4.DIV(a, b) } a >= 0 && b > 0 ==> b * v4.DIV(a, b) <= a && a < b * (v4.DIV(a, b) + 1)); + +axiom (forall a: int, b: int :: { v4.DIV(a, b) } a >= 0 && b < 0 ==> b * v4.DIV(a, b) <= a && a < b * (v4.DIV(a, b) - 1)); + +axiom (forall a: int, b: int :: { v4.DIV(a, b) } a < 0 && b > 0 ==> b * v4.DIV(a, b) >= a && a > b * (v4.DIV(a, b) - 1)); + +axiom (forall a: int, b: int :: { v4.DIV(a, b) } a < 0 && b < 0 ==> b * v4.DIV(a, b) >= a && a > b * (v4.DIV(a, b) + 1)); + +axiom v4.POW2(1); + +axiom v4.POW2(2); + +axiom v4.POW2(4); + +axiom v4.POW2(8); + +axiom v4.POW2(16); + +axiom v4.POW2(32); + +axiom v4.POW2(64); + +axiom v4.POW2(128); + +axiom v4.POW2(256); + +axiom v4.POW2(512); + +axiom v4.POW2(1024); + +axiom v4.POW2(2048); + +axiom v4.POW2(4096); + +axiom v4.POW2(8192); + +axiom v4.POW2(16384); + +axiom v4.POW2(32768); + +axiom v4.POW2(65536); + +axiom v4.POW2(131072); + +axiom v4.POW2(262144); + +axiom v4.POW2(524288); + +axiom v4.POW2(1048576); + +axiom v4.POW2(2097152); + +axiom v4.POW2(4194304); + +axiom v4.POW2(8388608); + +axiom v4.POW2(16777216); + +axiom v4.POW2(33554432); + +axiom (forall a: int, b: int :: { v4.BIT_BAND(a, b) } a == b ==> v4.BIT_BAND(a, b) == a); + +axiom (forall a: int, b: int :: { v4.BIT_BAND(a, b) } v4.POW2(a) && v4.POW2(b) && a != b ==> v4.BIT_BAND(a, b) == 0); + +axiom (forall a: int, b: int :: { v4.BIT_BAND(a, b) } a == 0 || b == 0 ==> v4.BIT_BAND(a, b) == 0); + +axiom (forall a: bool, b: int, c: int :: { v4.choose(a, b, c) } a ==> v4.choose(a, b, c) == b); + +axiom (forall a: bool, b: int, c: int :: { v4.choose(a, b, c) } !a ==> v4.choose(a, b, c) == c); + +axiom (forall a: bool :: { v4.LIFT(a) } a <==> v4.LIFT(a) != 0); + +axiom (forall a: int :: { v4.PTR_NOT(a) } a == 0 ==> v4.PTR_NOT(a) != 0); + +axiom (forall a: int :: { v4.PTR_NOT(a) } a != 0 ==> v4.PTR_NOT(a) == 0); + +axiom (forall a: int :: { v4.NULL_CHECK(a) } a == 0 ==> v4.NULL_CHECK(a) != 0); + +axiom (forall a: int :: { v4.NULL_CHECK(a) } a != 0 ==> v4.NULL_CHECK(a) == 0); + +axiom (forall n: int, x: int, y: int :: { v4.AtLeast(n, x)[y] } v4.AtLeast(n, x)[y] ==> v4.INT_LEQ(x, y) && v4.Rep(n, x) == v4.Rep(n, y)); + +axiom (forall n: int, x: int, y: int :: { v4.AtLeast(n, x), v4.Rep(n, x), v4.Rep(n, y) } v4.INT_LEQ(x, y) && v4.Rep(n, x) == v4.Rep(n, y) ==> v4.AtLeast(n, x)[y]); + +axiom (forall n: int, x: int :: { v4.AtLeast(n, x) } v4.AtLeast(n, x)[x]); + +axiom (forall n: int, x: int, z: int :: { v4.PLUS(x, n, z) } v4.Rep(n, x) == v4.Rep(n, v4.PLUS(x, n, z))); + +axiom (forall n: int, x: int :: { v4.Rep(n, x) } (exists k: int :: v4.INT_SUB(v4.Rep(n, x), x) == v4.INT_MULT(n, k))); + +axiom (forall x: int, n: int, z: int :: { v4.Array(x, n, z) } v4.INT_LEQ(z, 0) ==> v4.Equal(v4.Array(x, n, z), v4.Empty())); + +axiom (forall x: int, n: int, z: int :: { v4.Array(x, n, z) } v4.INT_GT(z, 0) ==> v4.Equal(v4.Array(x, n, z), v4.Difference(v4.AtLeast(n, x), v4.AtLeast(n, v4.PLUS(x, n, z))))); + +axiom (forall x: int :: !v4.Empty()[x]); + +axiom (forall x: int :: v4.SetTrue()[x]); + +axiom (forall x: int, y: int :: { v4.Singleton(y)[x] } v4.Singleton(y)[x] <==> x == y); + +axiom (forall y: int :: { v4.Singleton(y) } v4.Singleton(y)[y]); + +axiom (forall x: int, S: [int]bool, T: [int]bool :: { v4.Union(S, T)[x] } { v4.Union(S, T), S[x] } { v4.Union(S, T), T[x] } v4.Union(S, T)[x] <==> S[x] || T[x]); + +axiom (forall x: int, S: [int]bool, T: [int]bool :: { v4.Intersection(S, T)[x] } { v4.Intersection(S, T), S[x] } { v4.Intersection(S, T), T[x] } v4.Intersection(S, T)[x] <==> S[x] && T[x]); + +axiom (forall x: int, S: [int]bool, T: [int]bool :: { v4.Difference(S, T)[x] } { v4.Difference(S, T), S[x] } { v4.Difference(S, T), T[x] } v4.Difference(S, T)[x] <==> S[x] && !T[x]); + +axiom (forall S: [int]bool, T: [int]bool :: { v4.Equal(S, T) } v4.Equal(S, T) <==> v4.Subset(S, T) && v4.Subset(T, S)); + +axiom (forall x: int, S: [int]bool, T: [int]bool :: { S[x], v4.Subset(S, T) } { T[x], v4.Subset(S, T) } S[x] && v4.Subset(S, T) ==> T[x]); + +axiom (forall S: [int]bool, T: [int]bool :: { v4.Subset(S, T) } v4.Subset(S, T) || (exists x: int :: S[x] && !T[x])); + +axiom (forall x: int, S: [int]bool, T: [int]bool :: { S[x], v4.Disjoint(S, T) } { T[x], v4.Disjoint(S, T) } !(S[x] && v4.Disjoint(S, T) && T[x])); + +axiom (forall S: [int]bool, T: [int]bool :: { v4.Disjoint(S, T) } v4.Disjoint(S, T) || (exists x: int :: S[x] && T[x])); + +axiom (forall f: [int]int, x: int :: { v4.Inverse(f, f[x]) } v4.Inverse(f, f[x])[x]); + +axiom (forall f: [int]int, x: int, y: int :: { v4.Inverse(f, y), f[x] } v4.Inverse(f, y)[x] ==> f[x] == y); + +axiom (forall f: [int]int, x: int, y: int :: { v4.Inverse(f[x := y], y) } v4.Equal(v4.Inverse(f[x := y], y), v4.Union(v4.Inverse(f, y), v4.Singleton(x)))); + +axiom (forall f: [int]int, x: int, y: int, z: int :: { v4.Inverse(f[x := y], z) } y == z || v4.Equal(v4.Inverse(f[x := y], z), v4.Difference(v4.Inverse(f, z), v4.Singleton(x)))); + +axiom (forall x: int, S: [int]bool, M: [int]int :: { v4.Dereference(S, M)[x] } v4.Dereference(S, M)[x] ==> (exists y: int :: x == M[y] && S[y])); + +axiom (forall x: int, S: [int]bool, M: [int]int :: { M[x], S[x], v4.Dereference(S, M) } S[x] ==> v4.Dereference(S, M)[M[x]]); + +axiom (forall x: int, y: int, S: [int]bool, M: [int]int :: { v4.Dereference(S, M[x := y]) } !S[x] ==> v4.Equal(v4.Dereference(S, M[x := y]), v4.Dereference(S, M))); + +axiom (forall x: int, y: int, S: [int]bool, M: [int]int :: { v4.Dereference(S, M[x := y]) } S[x] && v4.Equal(v4.Intersection(v4.Inverse(M, M[x]), S), v4.Singleton(x)) ==> v4.Equal(v4.Dereference(S, M[x := y]), v4.Union(v4.Difference(v4.Dereference(S, M), v4.Singleton(M[x])), v4.Singleton(y)))); + +axiom (forall x: int, y: int, S: [int]bool, M: [int]int :: { v4.Dereference(S, M[x := y]) } S[x] && !v4.Equal(v4.Intersection(v4.Inverse(M, M[x]), S), v4.Singleton(x)) ==> v4.Equal(v4.Dereference(S, M[x := y]), v4.Union(v4.Dereference(S, M), v4.Singleton(y)))); + +axiom (forall M: [name][int]int, x: int :: { v4.Unified(M)[x] } v4.Unified(M)[x] == M[v4.Field(x)][x]); + +axiom (forall M: [name][int]int, x: int, y: int :: { v4.Unified(M[v4.Field(x) := M[v4.Field(x)][x := y]]) } v4.Unified(M[v4.Field(x) := M[v4.Field(x)][x := y]]) == v4.Unified(M)[x := y]); + +procedure v4.havoc_assert(i: int); + + + +procedure v4.havoc_assume(i: int); + + + +procedure v4.__HAVOC_free(a: int); + + + +procedure v4.__HAVOC_malloc(obj_size: int) returns (new: int); + free ensures new == _uf_v4.__HAVOC_malloc_new(obj_size); + + + +procedure v4.__HAVOC_det_malloc(obj_size: int) returns (new: int); + free ensures new == _uf_v4.__HAVOC_det_malloc_new(obj_size); + + + +procedure v4.__HAVOC_memset_split_1(A: [int]int, p: int, c: int, n: int) returns (ret: [int]int); + free ensures ret == _uf_v4.__HAVOC_memset_split_1_ret(A, p, c, n); + + + +procedure v4.__HAVOC_memset_split_2(A: [int]int, p: int, c: int, n: int) returns (ret: [int]int); + free ensures ret == _uf_v4.__HAVOC_memset_split_2_ret(A, p, c, n); + + + +procedure v4.__HAVOC_memset_split_4(A: [int]int, p: int, c: int, n: int) returns (ret: [int]int); + free ensures ret == _uf_v4.__HAVOC_memset_split_4_ret(A, p, c, n); + + + +procedure v4.nondet_choice() returns (x: int); + free ensures x == _uf_v4.nondet_choice_x(); + + + +procedure v4.det_choice() returns (x: int); + free ensures x == _uf_v4.det_choice_x(); + + + +procedure v4._strdup(str: int) returns (new: int); + free ensures new == _uf_v4._strdup_new(str); + + + +procedure v4._xstrcasecmp(a0: int, a1: int) returns (ret: int); + free ensures ret == _uf_v4._xstrcasecmp_ret(a0, a1); + + + +procedure v4._xstrcmp(a0: int, a1: int) returns (ret: int); + free ensures ret == _uf_v4._xstrcmp_ret(a0, a1); + + + +procedure v4.UnsignedAdd(a0: int, a1: int) returns (ret: int); + + + +procedure v4.UnsignedSub(a0: int, a1: int) returns (ret: int); + + + +procedure {:inline 1} v4.Eval(e_.1: int); + modifies v4.Mem_T.result__EXPR; + free ensures v4.Mem_T.result__EXPR == _uf_v4.Eval_v4.Mem_T.result__EXPR(e_.1, old(v4.alloc), old(v4.Mem_T.oper__EXPR), old(v4.Mem_T.op1__EXPR), old(v4.Mem_T.op2__EXPR), old(v4.Mem_T.result__EXPR), old(v4.isUnsigned)); + + + +procedure v4.EvalEntry1(e_.1: int, outval_.1: int); + modifies v4.isUnsigned, v4.Mem_T.result__EXPR, v4.Mem_T.INT4; + free ensures v4.isUnsigned == _uf_v4.EvalEntry1_v4.isUnsigned(e_.1, outval_.1, old(v4.alloc), old(v4.Mem_T.oper__EXPR), old(v4.Mem_T.op1__EXPR), old(v4.Mem_T.op2__EXPR), old(v4.Mem_T.result__EXPR), old(v4.Mem_T.INT4), old(v4.isUnsigned)); + free ensures v4.Mem_T.result__EXPR == _uf_v4.EvalEntry1_v4.Mem_T.result__EXPR(e_.1, outval_.1, old(v4.alloc), old(v4.Mem_T.oper__EXPR), old(v4.Mem_T.op1__EXPR), old(v4.Mem_T.op2__EXPR), old(v4.Mem_T.result__EXPR), old(v4.Mem_T.INT4), old(v4.isUnsigned)); + free ensures v4.Mem_T.INT4 == _uf_v4.EvalEntry1_v4.Mem_T.INT4(e_.1, outval_.1, old(v4.alloc), old(v4.Mem_T.oper__EXPR), old(v4.Mem_T.op1__EXPR), old(v4.Mem_T.op2__EXPR), old(v4.Mem_T.result__EXPR), old(v4.Mem_T.INT4), old(v4.isUnsigned)); + + + +procedure v4.EvalEntry2(e_.1: int); + modifies v4.isUnsigned, v4.Mem_T.result__EXPR; + free ensures v4.isUnsigned == _uf_v4.EvalEntry2_v4.isUnsigned(e_.1, old(v4.alloc), old(v4.Mem_T.oper__EXPR), old(v4.Mem_T.op1__EXPR), old(v4.Mem_T.op2__EXPR), old(v4.Mem_T.result__EXPR), old(v4.isUnsigned)); + free ensures v4.Mem_T.result__EXPR == _uf_v4.EvalEntry2_v4.Mem_T.result__EXPR(e_.1, old(v4.alloc), old(v4.Mem_T.oper__EXPR), old(v4.Mem_T.op1__EXPR), old(v4.Mem_T.op2__EXPR), old(v4.Mem_T.result__EXPR), old(v4.isUnsigned)); + + + +procedure v4.__havoc_heapglobal_init(); + + + +implementation {:inline 1} v4.Eval(e_.1: int) +{ + var havoc_stringTemp: int; + var condVal: int; + var a1: int; + var a2: int; + var e: int; + var op: int; + var res: int; + var result.UnsignedAdd$1: int; + var result.UnsignedSub$2: int; + var tempBoogie0: int; + var tempBoogie1: int; + var tempBoogie2: int; + var tempBoogie3: int; + var tempBoogie4: int; + var tempBoogie5: int; + var tempBoogie6: int; + var tempBoogie7: int; + var tempBoogie8: int; + var tempBoogie9: int; + var tempBoogie10: int; + var tempBoogie11: int; + var tempBoogie12: int; + var tempBoogie13: int; + var tempBoogie14: int; + var tempBoogie15: int; + var tempBoogie16: int; + var tempBoogie17: int; + var tempBoogie18: int; + var tempBoogie19: int; + var __havoc_dummy_return: int; + + anon0#2: + havoc_stringTemp := 0; + goto start#2; + + start#2: + assume v4.INT_LT(e_.1, v4.alloc); + a1 := 0; + a2 := 0; + e := 0; + op := 0; + res := 0; + result.UnsignedAdd$1 := 0; + result.UnsignedSub$2 := 0; + e := e_.1; + goto label_3#2; + + label_3#2: + assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 19} true; + goto label_4#2; + + label_4#2: + assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 19} true; + goto label_5#2; + + label_5#2: + assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 19} true; + goto label_6#2; + + label_6#2: + assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 19} true; + goto label_7#2; + + label_7#2: + assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 21} true; + assert true; + op := v4.Mem_T.oper__EXPR[v4.oper__EXPR(e)]; + assume v4.value_is(v4.__ctobpl_const_1, op); + assume v4.value_is(v4.__ctobpl_const_2, e); + assume v4.value_is(v4.__ctobpl_const_3, v4.Mem_T.oper__EXPR[v4.oper__EXPR(e)]); + goto label_8#2; + + label_8#2: + assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 22} true; + assert true; + a1 := v4.Mem_T.op1__EXPR[v4.op1__EXPR(e)]; + assume v4.value_is(v4.__ctobpl_const_4, a1); + assume v4.value_is(v4.__ctobpl_const_5, e); + assume v4.value_is(v4.__ctobpl_const_6, v4.Mem_T.op1__EXPR[v4.op1__EXPR(e)]); + goto label_9#2; + + label_9#2: + assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 23} true; + assert true; + a2 := v4.Mem_T.op2__EXPR[v4.op2__EXPR(e)]; + assume v4.value_is(v4.__ctobpl_const_7, a2); + assume v4.value_is(v4.__ctobpl_const_8, e); + assume v4.value_is(v4.__ctobpl_const_9, v4.Mem_T.op2__EXPR[v4.op2__EXPR(e)]); + goto label_10#2; + + label_10#2: + assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 24} true; + res := 0 - 1; + assume v4.value_is(v4.__ctobpl_const_10, res); + goto label_11#2; + + label_11#2: + assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 26} true; + goto label_11_case_0#2, label_11_case_1#2, label_11_case_2#2; + + label_11_case_2#2: + assume v4.INT_EQ(op, 2); + assume v4.value_is(v4.__ctobpl_const_11, op); + goto label_14#2; + + label_14#2: + assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 35} true; + goto label_14_true#2, label_14_false#2; + + label_14_false#2: + assume v4.isUnsigned == 0; + assume v4.value_is(v4.__ctobpl_const_16, v4.isUnsigned); + goto label_15#2; + + label_15#2: + assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 38} true; + res := v4.MINUS_BOTH_PTR_OR_BOTH_INT(a1, a2, 1); + assume v4.value_is(v4.__ctobpl_const_17, res); + assume v4.value_is(v4.__ctobpl_const_18, a1); + assume v4.value_is(v4.__ctobpl_const_19, a2); + goto label_12#2; + + label_14_true#2: + assume v4.isUnsigned != 0; + assume v4.value_is(v4.__ctobpl_const_16, v4.isUnsigned); + goto label_16#2; + + label_16#2: + assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 36} true; + call result.UnsignedSub$2 := v4.UnsignedSub(a1, a2); + assume v4.value_is(v4.__ctobpl_const_20, a1); + assume v4.value_is(v4.__ctobpl_const_21, a2); + assume v4.value_is(v4.__ctobpl_const_22, a1); + assume v4.value_is(v4.__ctobpl_const_23, a2); + goto label_19#2; + + label_19#2: + assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 36} true; + res := result.UnsignedSub$2; + assume v4.value_is(v4.__ctobpl_const_24, res); + assume v4.value_is(v4.__ctobpl_const_25, result.UnsignedSub$2); + goto label_12#2; + + label_11_case_1#2: + assume v4.INT_EQ(op, 1); + assume v4.value_is(v4.__ctobpl_const_11, op); + goto label_13#2; + + label_13#2: + assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 29} true; + goto label_13_true#2, label_13_false#2; + + label_13_false#2: + assume v4.isUnsigned == 0; + assume v4.value_is(v4.__ctobpl_const_15, v4.isUnsigned); + goto label_20#2; + + label_20#2: + assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 32} true; + res := v4.PLUS(a1, 1, a2); + assume v4.value_is(v4.__ctobpl_const_26, res); + assume v4.value_is(v4.__ctobpl_const_27, a1); + assume v4.value_is(v4.__ctobpl_const_28, a2); + goto label_12#2; + + label_13_true#2: + assume v4.isUnsigned != 0; + assume v4.value_is(v4.__ctobpl_const_15, v4.isUnsigned); + goto label_21#2; + + label_21#2: + assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 30} true; + call result.UnsignedAdd$1 := v4.UnsignedAdd(a1, a2); + assume v4.value_is(v4.__ctobpl_const_29, a1); + assume v4.value_is(v4.__ctobpl_const_30, a2); + assume v4.value_is(v4.__ctobpl_const_31, a1); + assume v4.value_is(v4.__ctobpl_const_32, a2); + goto label_24#2; + + label_24#2: + assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 30} true; + res := result.UnsignedAdd$1; + assume v4.value_is(v4.__ctobpl_const_33, res); + assume v4.value_is(v4.__ctobpl_const_34, result.UnsignedAdd$1); + goto label_12#2; + + label_11_case_0#2: + assume v4.INT_NEQ(op, 1); + assume v4.INT_NEQ(op, 2); + assume v4.value_is(v4.__ctobpl_const_11, op); + goto label_12#2; + + label_12#2: + assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 41} true; + assert true; + v4.Mem_T.result__EXPR := v4.Mem_T.result__EXPR[v4.result__EXPR(e) := res]; + assume v4.value_is(v4.__ctobpl_const_12, e); + assume v4.value_is(v4.__ctobpl_const_13, v4.Mem_T.result__EXPR[v4.result__EXPR(e)]); + assume v4.value_is(v4.__ctobpl_const_14, res); + goto label_1#2; + + label_1#2: + assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 42} true; + return; +} + + + +implementation v4.EvalEntry1(e_.1: int, outval_.1: int) +{ + var havoc_stringTemp: int; + var condVal: int; + var e: int; + var outval: int; + var tempBoogie0: int; + var tempBoogie1: int; + var tempBoogie2: int; + var tempBoogie3: int; + var tempBoogie4: int; + var tempBoogie5: int; + var tempBoogie6: int; + var tempBoogie7: int; + var tempBoogie8: int; + var tempBoogie9: int; + var tempBoogie10: int; + var tempBoogie11: int; + var tempBoogie12: int; + var tempBoogie13: int; + var tempBoogie14: int; + var tempBoogie15: int; + var tempBoogie16: int; + var tempBoogie17: int; + var tempBoogie18: int; + var tempBoogie19: int; + var __havoc_dummy_return: int; + + anon0#2: + havoc_stringTemp := 0; + goto start#2; + + start#2: + assume v4.INT_LT(e_.1, v4.alloc); + assume v4.INT_LT(outval_.1, v4.alloc); + e := 0; + outval := 0; + e := e_.1; + outval := outval_.1; + goto label_3#2; + + label_3#2: + assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 47} true; + v4.isUnsigned := 1; + assume v4.value_is(v4.__ctobpl_const_35, v4.isUnsigned); + goto label_4#2; + + label_4#2: + assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 48} true; + call v4.Eval(e); + assume v4.value_is(v4.__ctobpl_const_36, e); + assume v4.value_is(v4.__ctobpl_const_37, e); + goto label_7#2; + + label_7#2: + assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 49} true; + assert true; + assert true; + v4.Mem_T.INT4 := v4.Mem_T.INT4[outval := v4.Mem_T.result__EXPR[v4.result__EXPR(e)]]; + assume v4.value_is(v4.__ctobpl_const_38, outval); + assume v4.value_is(v4.__ctobpl_const_39, v4.Mem_T.INT4[outval]); + assume v4.value_is(v4.__ctobpl_const_40, e); + assume v4.value_is(v4.__ctobpl_const_41, v4.Mem_T.result__EXPR[v4.result__EXPR(e)]); + goto label_1#2; + + label_1#2: + assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 50} true; + return; +} + + + +implementation v4.EvalEntry2(e_.1: int) +{ + var havoc_stringTemp: int; + var condVal: int; + var e: int; + var tempBoogie0: int; + var tempBoogie1: int; + var tempBoogie2: int; + var tempBoogie3: int; + var tempBoogie4: int; + var tempBoogie5: int; + var tempBoogie6: int; + var tempBoogie7: int; + var tempBoogie8: int; + var tempBoogie9: int; + var tempBoogie10: int; + var tempBoogie11: int; + var tempBoogie12: int; + var tempBoogie13: int; + var tempBoogie14: int; + var tempBoogie15: int; + var tempBoogie16: int; + var tempBoogie17: int; + var tempBoogie18: int; + var tempBoogie19: int; + var __havoc_dummy_return: int; + + anon0#2: + havoc_stringTemp := 0; + goto start#2; + + start#2: + assume v4.INT_LT(e_.1, v4.alloc); + e := 0; + e := e_.1; + goto label_3#2; + + label_3#2: + assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 54} true; + v4.isUnsigned := 0; + assume v4.value_is(v4.__ctobpl_const_42, v4.isUnsigned); + goto label_4#2; + + label_4#2: + assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 55} true; + call v4.Eval(e); + assume v4.value_is(v4.__ctobpl_const_43, e); + assume v4.value_is(v4.__ctobpl_const_44, e); + goto label_1#2; + + label_1#2: + assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 56} true; + return; +} + + + +implementation v4.__havoc_heapglobal_init() +{ + + anon0#2: + return; +} + + + +var v2.Mem: [name][int]int; + +var v2.alloc: int; + +var v2.Mem_T.INT4: [int]int; + +var v2.Mem_T.op1__EXPR: [int]int; + +var v2.Mem_T.op2__EXPR: [int]int; + +var v2.Mem_T.oper__EXPR: [int]int; + +var v2.Mem_T.result__EXPR: [int]int; + +var v2.detChoiceCnt: int; + +var v2.Res_KERNEL_SOURCE: [int]int; + +var v2.Res_PROBED: [int]int; + +const unique v2.T.oper__EXPR: name; + +const unique v2.T.op1__EXPR: name; + +const unique v2.T.op2__EXPR: name; + +const unique v2.T.result__EXPR: name; + +const unique v2.T.INT4: name; + +const unique v2.T.PINT4: name; + +const unique v2.T.PPINT4: name; + +const unique v2.T.PP_EXPR: name; + +const unique v2.T.P_EXPR: name; + +const unique v2.T._EXPR: name; + +const {:model_const "a2"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceLine 21} unique v2.__ctobpl_const_7: int; + +const {:model_const "e"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceLine 21} unique v2.__ctobpl_const_8: int; + +const {:model_const "e->oper"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceLine 19} unique v2.__ctobpl_const_3: int; + +const {:model_const "a1"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceLine 20} unique v2.__ctobpl_const_4: int; + +const {:model_const "e"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceLine 20} unique v2.__ctobpl_const_5: int; + +const {:model_const "e->op1"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceLine 20} unique v2.__ctobpl_const_6: int; + +const {:model_const "e->op2"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceLine 21} unique v2.__ctobpl_const_9: int; + +const {:model_const "res"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceLine 22} unique v2.__ctobpl_const_10: int; + +const {:model_const "op"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceLine 24} unique v2.__ctobpl_const_11: int; + +const {:model_const "e"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceLine 35} unique v2.__ctobpl_const_12: int; + +const {:model_const "e->result"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceLine 35} unique v2.__ctobpl_const_13: int; + +const {:model_const "res"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceLine 35} unique v2.__ctobpl_const_14: int; + +const {:model_const "res"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceLine 27} unique v2.__ctobpl_const_15: int; + +const {:model_const "a1"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceLine 27} unique v2.__ctobpl_const_16: int; + +const {:model_const "a2"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceLine 27} unique v2.__ctobpl_const_17: int; + +const {:model_const "res"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceLine 29} unique v2.__ctobpl_const_18: int; + +const {:model_const "a1"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceLine 29} unique v2.__ctobpl_const_19: int; + +const {:model_const "a2"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceLine 29} unique v2.__ctobpl_const_20: int; + +const {:model_const "e"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceLine 40} unique v2.__ctobpl_const_21: int; + +const {:model_const "e"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceLine 40} unique v2.__ctobpl_const_22: int; + +const {:model_const "outval"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceLine 41} unique v2.__ctobpl_const_23: int; + +const {:model_const "*outval"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceLine 41} unique v2.__ctobpl_const_24: int; + +const {:model_const "e"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceLine 41} unique v2.__ctobpl_const_25: int; + +const {:model_const "e->result"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceLine 41} unique v2.__ctobpl_const_26: int; + +const {:model_const "e"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceLine 46} unique v2.__ctobpl_const_27: int; + +const {:model_const "e"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceLine 46} unique v2.__ctobpl_const_28: int; + +const {:model_const "op"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceLine 19} unique v2.__ctobpl_const_1: int; + +const {:model_const "e"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceLine 19} unique v2.__ctobpl_const_2: int; + +axiom (forall b0: byte, c0: byte :: { v4.OneByteToInt(b0), v4.OneByteToInt(c0) } v4.OneByteToInt(b0) == v4.OneByteToInt(c0) ==> b0 == c0); + +axiom (forall b0: byte, b1: byte, c0: byte, c1: byte :: { v4.TwoBytesToInt(b0, b1), v4.TwoBytesToInt(c0, c1) } v4.TwoBytesToInt(b0, b1) == v4.TwoBytesToInt(c0, c1) ==> b0 == c0 && b1 == c1); + +axiom (forall b0: byte, b1: byte, b2: byte, b3: byte, c0: byte, c1: byte, c2: byte, c3: byte :: { v4.FourBytesToInt(b0, b1, b2, b3), v4.FourBytesToInt(c0, c1, c2, c3) } v4.FourBytesToInt(b0, b1, b2, b3) == v4.FourBytesToInt(c0, c1, c2, c3) ==> b0 == c0 && b1 == c1 && b2 == c2 && b3 == c3); + +axiom (forall x: int :: { v4.Base(x) } v4.INT_LEQ(v4.Base(x), x)); + +axiom (forall a: int, t: name :: { v4.Match(a, v4.T.Ptr(t)) } v4.Match(a, v4.T.Ptr(t)) <==> v4.Field(a) == v4.T.Ptr(t)); + +axiom (forall b: int, a: int, t: name :: { v4.MatchBase(b, a, v4.T.Ptr(t)) } v4.MatchBase(b, a, v4.T.Ptr(t)) <==> v4.Base(a) == b); + +axiom (forall v: int, t: name :: { v4.HasType(v, v4.T.Ptr(t)) } v4.HasType(v, v4.T.Ptr(t)) <==> v == 0 || (v4.INT_GT(v, 0) && v4.Match(v, t) && v4.MatchBase(v4.Base(v), v, t))); + +axiom (forall x: int, S: [int]bool :: { v4._S_op1__EXPR(S)[x] } v4._S_op1__EXPR(S)[x] <==> S[v4.op1__EXPRInv(x)]); + +axiom (forall x: int, S: [int]bool :: { v4._S_op1__EXPRInv(S)[x] } v4._S_op1__EXPRInv(S)[x] <==> S[v4.op1__EXPR(x)]); + +axiom (forall x: int, S: [int]bool :: { S[x], v4._S_op1__EXPR(S) } S[x] ==> v4._S_op1__EXPR(S)[v4.op1__EXPR(x)]); + +axiom (forall x: int, S: [int]bool :: { S[x], v4._S_op1__EXPRInv(S) } S[x] ==> v4._S_op1__EXPRInv(S)[v4.op1__EXPRInv(x)]); + +axiom (forall x: int :: { v4.op1__EXPR(x) } v4.op1__EXPR(x) == v4.INT_ADD(x, 4)); + +axiom (forall x: int :: { v4.op1__EXPRInv(x) } v4.op1__EXPRInv(x) == v4.INT_SUB(x, 4)); + +axiom (forall x: int :: { v4.op1__EXPR(x) } v4.op1__EXPR(x) == v4.PLUS(x, 1, 4)); + +axiom (forall x: int, S: [int]bool :: { v4._S_op2__EXPR(S)[x] } v4._S_op2__EXPR(S)[x] <==> S[v4.op2__EXPRInv(x)]); + +axiom (forall x: int, S: [int]bool :: { v4._S_op2__EXPRInv(S)[x] } v4._S_op2__EXPRInv(S)[x] <==> S[v4.op2__EXPR(x)]); + +axiom (forall x: int, S: [int]bool :: { S[x], v4._S_op2__EXPR(S) } S[x] ==> v4._S_op2__EXPR(S)[v4.op2__EXPR(x)]); + +axiom (forall x: int, S: [int]bool :: { S[x], v4._S_op2__EXPRInv(S) } S[x] ==> v4._S_op2__EXPRInv(S)[v4.op2__EXPRInv(x)]); + +axiom (forall x: int :: { v4.op2__EXPR(x) } v4.op2__EXPR(x) == v4.INT_ADD(x, 8)); + +axiom (forall x: int :: { v4.op2__EXPRInv(x) } v4.op2__EXPRInv(x) == v4.INT_SUB(x, 8)); + +axiom (forall x: int :: { v4.op2__EXPR(x) } v4.op2__EXPR(x) == v4.PLUS(x, 1, 8)); + +axiom (forall x: int, S: [int]bool :: { v4._S_oper__EXPR(S)[x] } v4._S_oper__EXPR(S)[x] <==> S[v4.oper__EXPRInv(x)]); + +axiom (forall x: int, S: [int]bool :: { v4._S_oper__EXPRInv(S)[x] } v4._S_oper__EXPRInv(S)[x] <==> S[v4.oper__EXPR(x)]); + +axiom (forall x: int, S: [int]bool :: { S[x], v4._S_oper__EXPR(S) } S[x] ==> v4._S_oper__EXPR(S)[v4.oper__EXPR(x)]); + +axiom (forall x: int, S: [int]bool :: { S[x], v4._S_oper__EXPRInv(S) } S[x] ==> v4._S_oper__EXPRInv(S)[v4.oper__EXPRInv(x)]); + +axiom (forall x: int :: { v4.oper__EXPR(x) } v4.oper__EXPR(x) == v4.INT_ADD(x, 0)); + +axiom (forall x: int :: { v4.oper__EXPRInv(x) } v4.oper__EXPRInv(x) == v4.INT_SUB(x, 0)); + +axiom (forall x: int :: { v4.oper__EXPR(x) } v4.oper__EXPR(x) == v4.PLUS(x, 1, 0)); + +axiom (forall x: int, S: [int]bool :: { v4._S_result__EXPR(S)[x] } v4._S_result__EXPR(S)[x] <==> S[v4.result__EXPRInv(x)]); + +axiom (forall x: int, S: [int]bool :: { v4._S_result__EXPRInv(S)[x] } v4._S_result__EXPRInv(S)[x] <==> S[v4.result__EXPR(x)]); + +axiom (forall x: int, S: [int]bool :: { S[x], v4._S_result__EXPR(S) } S[x] ==> v4._S_result__EXPR(S)[v4.result__EXPR(x)]); + +axiom (forall x: int, S: [int]bool :: { S[x], v4._S_result__EXPRInv(S) } S[x] ==> v4._S_result__EXPRInv(S)[v4.result__EXPRInv(x)]); + +axiom (forall x: int :: { v4.result__EXPR(x) } v4.result__EXPR(x) == v4.INT_ADD(x, 12)); + +axiom (forall x: int :: { v4.result__EXPRInv(x) } v4.result__EXPRInv(x) == v4.INT_SUB(x, 12)); + +axiom (forall x: int :: { v4.result__EXPR(x) } v4.result__EXPR(x) == v4.PLUS(x, 1, 12)); + +axiom (forall x: int, y: int :: { v4.INT_EQ(x, y): bool } v4.INT_EQ(x, y): bool <==> x == y); + +axiom (forall x: int, y: int :: { v4.INT_NEQ(x, y): bool } v4.INT_NEQ(x, y): bool <==> x != y); + +axiom (forall x: int, y: int :: { v4.INT_ADD(x, y): int } v4.INT_ADD(x, y): int == x + y); + +axiom (forall x: int, y: int :: { v4.INT_SUB(x, y): int } v4.INT_SUB(x, y): int == x - y); + +axiom (forall x: int, y: int :: { v4.INT_MULT(x, y): int } v4.INT_MULT(x, y): int == x * y); + +axiom (forall x: int, y: int :: { v4.INT_DIV(x, y): int } v4.INT_DIV(x, y): int == x div y); + +axiom (forall x: int, y: int :: { v4.INT_LT(x, y): bool } v4.INT_LT(x, y): bool <==> x < y); + +axiom (forall x: int, y: int :: { v4.INT_ULT(x, y): bool } v4.INT_ULT(x, y): bool <==> x < y); + +axiom (forall x: int, y: int :: { v4.INT_LEQ(x, y): bool } v4.INT_LEQ(x, y): bool <==> x <= y); + +axiom (forall x: int, y: int :: { v4.INT_ULEQ(x, y): bool } v4.INT_ULEQ(x, y): bool <==> x <= y); + +axiom (forall x: int, y: int :: { v4.INT_GT(x, y): bool } v4.INT_GT(x, y): bool <==> x > y); + +axiom (forall x: int, y: int :: { v4.INT_UGT(x, y): bool } v4.INT_UGT(x, y): bool <==> x > y); + +axiom (forall x: int, y: int :: { v4.INT_GEQ(x, y): bool } v4.INT_GEQ(x, y): bool <==> x >= y); + +axiom (forall x: int, y: int :: { v4.INT_UGEQ(x, y): bool } v4.INT_UGEQ(x, y): bool <==> x >= y); + +axiom (forall x: bv32, y: bv32 :: { v4.BV32_EQ(x, y): bool } v4.BV32_EQ(x, y): bool <==> x == y); + +axiom (forall x: bv32, y: bv32 :: { v4.BV32_NEQ(x, y): bool } v4.BV32_NEQ(x, y): bool <==> x != y); + +axiom (forall a: int, b: int, size: int :: { v4.MINUS_BOTH_PTR_OR_BOTH_INT(a, b, size) } v4.INT_LEQ(v4.INT_MULT(size, v4.MINUS_BOTH_PTR_OR_BOTH_INT(a, b, size)), v4.INT_SUB(a, b)) && v4.INT_LT(v4.INT_SUB(a, b), v4.INT_MULT(size, v4.INT_ADD(v4.MINUS_BOTH_PTR_OR_BOTH_INT(a, b, size), 1)))); + +axiom (forall a: int, b: int, size: int :: { v4.MINUS_BOTH_PTR_OR_BOTH_INT(a, b, size) } v4.MINUS_BOTH_PTR_OR_BOTH_INT(a, b, 1) == v4.INT_SUB(a, b)); + +axiom (forall a: int, a_size: int, b: int :: { v4.MINUS_LEFT_PTR(a, a_size, b) } v4.MINUS_LEFT_PTR(a, a_size, b) == v4.INT_SUB(a, v4.INT_MULT(a_size, b))); + +axiom (forall a: int, a_size: int, b: int :: { v4.PLUS(a, a_size, b) } v4.PLUS(a, a_size, b) == v4.INT_ADD(a, v4.INT_MULT(a_size, b))); + +axiom (forall a: int, b: int :: { v4.MULT(a, b) } v4.MULT(a, b) == v4.INT_MULT(a, b)); + +axiom (forall a: int, b: int :: { v4.DIV(a, b) } a >= 0 && b > 0 ==> b * v4.DIV(a, b) <= a && a < b * (v4.DIV(a, b) + 1)); + +axiom (forall a: int, b: int :: { v4.DIV(a, b) } a >= 0 && b < 0 ==> b * v4.DIV(a, b) <= a && a < b * (v4.DIV(a, b) - 1)); + +axiom (forall a: int, b: int :: { v4.DIV(a, b) } a < 0 && b > 0 ==> b * v4.DIV(a, b) >= a && a > b * (v4.DIV(a, b) - 1)); + +axiom (forall a: int, b: int :: { v4.DIV(a, b) } a < 0 && b < 0 ==> b * v4.DIV(a, b) >= a && a > b * (v4.DIV(a, b) + 1)); + +axiom v4.POW2(1); + +axiom v4.POW2(2); + +axiom v4.POW2(4); + +axiom v4.POW2(8); + +axiom v4.POW2(16); + +axiom v4.POW2(32); + +axiom v4.POW2(64); + +axiom v4.POW2(128); + +axiom v4.POW2(256); + +axiom v4.POW2(512); + +axiom v4.POW2(1024); + +axiom v4.POW2(2048); + +axiom v4.POW2(4096); + +axiom v4.POW2(8192); + +axiom v4.POW2(16384); + +axiom v4.POW2(32768); + +axiom v4.POW2(65536); + +axiom v4.POW2(131072); + +axiom v4.POW2(262144); + +axiom v4.POW2(524288); + +axiom v4.POW2(1048576); + +axiom v4.POW2(2097152); + +axiom v4.POW2(4194304); + +axiom v4.POW2(8388608); + +axiom v4.POW2(16777216); + +axiom v4.POW2(33554432); + +axiom (forall a: int, b: int :: { v4.BIT_BAND(a, b) } a == b ==> v4.BIT_BAND(a, b) == a); + +axiom (forall a: int, b: int :: { v4.BIT_BAND(a, b) } v4.POW2(a) && v4.POW2(b) && a != b ==> v4.BIT_BAND(a, b) == 0); + +axiom (forall a: int, b: int :: { v4.BIT_BAND(a, b) } a == 0 || b == 0 ==> v4.BIT_BAND(a, b) == 0); + +axiom (forall a: bool, b: int, c: int :: { v4.choose(a, b, c) } a ==> v4.choose(a, b, c) == b); + +axiom (forall a: bool, b: int, c: int :: { v4.choose(a, b, c) } !a ==> v4.choose(a, b, c) == c); + +axiom (forall a: bool :: { v4.LIFT(a) } a <==> v4.LIFT(a) != 0); + +axiom (forall a: int :: { v4.PTR_NOT(a) } a == 0 ==> v4.PTR_NOT(a) != 0); + +axiom (forall a: int :: { v4.PTR_NOT(a) } a != 0 ==> v4.PTR_NOT(a) == 0); + +axiom (forall a: int :: { v4.NULL_CHECK(a) } a == 0 ==> v4.NULL_CHECK(a) != 0); + +axiom (forall a: int :: { v4.NULL_CHECK(a) } a != 0 ==> v4.NULL_CHECK(a) == 0); + +axiom (forall n: int, x: int, y: int :: { v4.AtLeast(n, x)[y] } v4.AtLeast(n, x)[y] ==> v4.INT_LEQ(x, y) && v4.Rep(n, x) == v4.Rep(n, y)); + +axiom (forall n: int, x: int, y: int :: { v4.AtLeast(n, x), v4.Rep(n, x), v4.Rep(n, y) } v4.INT_LEQ(x, y) && v4.Rep(n, x) == v4.Rep(n, y) ==> v4.AtLeast(n, x)[y]); + +axiom (forall n: int, x: int :: { v4.AtLeast(n, x) } v4.AtLeast(n, x)[x]); + +axiom (forall n: int, x: int, z: int :: { v4.PLUS(x, n, z) } v4.Rep(n, x) == v4.Rep(n, v4.PLUS(x, n, z))); + +axiom (forall n: int, x: int :: { v4.Rep(n, x) } (exists k: int :: v4.INT_SUB(v4.Rep(n, x), x) == v4.INT_MULT(n, k))); + +axiom (forall x: int, n: int, z: int :: { v4.Array(x, n, z) } v4.INT_LEQ(z, 0) ==> v4.Equal(v4.Array(x, n, z), v4.Empty())); + +axiom (forall x: int, n: int, z: int :: { v4.Array(x, n, z) } v4.INT_GT(z, 0) ==> v4.Equal(v4.Array(x, n, z), v4.Difference(v4.AtLeast(n, x), v4.AtLeast(n, v4.PLUS(x, n, z))))); + +axiom (forall x: int :: !v4.Empty()[x]); + +axiom (forall x: int :: v4.SetTrue()[x]); + +axiom (forall x: int, y: int :: { v4.Singleton(y)[x] } v4.Singleton(y)[x] <==> x == y); + +axiom (forall y: int :: { v4.Singleton(y) } v4.Singleton(y)[y]); + +axiom (forall x: int, S: [int]bool, T: [int]bool :: { v4.Union(S, T)[x] } { v4.Union(S, T), S[x] } { v4.Union(S, T), T[x] } v4.Union(S, T)[x] <==> S[x] || T[x]); + +axiom (forall x: int, S: [int]bool, T: [int]bool :: { v4.Intersection(S, T)[x] } { v4.Intersection(S, T), S[x] } { v4.Intersection(S, T), T[x] } v4.Intersection(S, T)[x] <==> S[x] && T[x]); + +axiom (forall x: int, S: [int]bool, T: [int]bool :: { v4.Difference(S, T)[x] } { v4.Difference(S, T), S[x] } { v4.Difference(S, T), T[x] } v4.Difference(S, T)[x] <==> S[x] && !T[x]); + +axiom (forall S: [int]bool, T: [int]bool :: { v4.Equal(S, T) } v4.Equal(S, T) <==> v4.Subset(S, T) && v4.Subset(T, S)); + +axiom (forall x: int, S: [int]bool, T: [int]bool :: { S[x], v4.Subset(S, T) } { T[x], v4.Subset(S, T) } S[x] && v4.Subset(S, T) ==> T[x]); + +axiom (forall S: [int]bool, T: [int]bool :: { v4.Subset(S, T) } v4.Subset(S, T) || (exists x: int :: S[x] && !T[x])); + +axiom (forall x: int, S: [int]bool, T: [int]bool :: { S[x], v4.Disjoint(S, T) } { T[x], v4.Disjoint(S, T) } !(S[x] && v4.Disjoint(S, T) && T[x])); + +axiom (forall S: [int]bool, T: [int]bool :: { v4.Disjoint(S, T) } v4.Disjoint(S, T) || (exists x: int :: S[x] && T[x])); + +axiom (forall f: [int]int, x: int :: { v4.Inverse(f, f[x]) } v4.Inverse(f, f[x])[x]); + +axiom (forall f: [int]int, x: int, y: int :: { v4.Inverse(f, y), f[x] } v4.Inverse(f, y)[x] ==> f[x] == y); + +axiom (forall f: [int]int, x: int, y: int :: { v4.Inverse(f[x := y], y) } v4.Equal(v4.Inverse(f[x := y], y), v4.Union(v4.Inverse(f, y), v4.Singleton(x)))); + +axiom (forall f: [int]int, x: int, y: int, z: int :: { v4.Inverse(f[x := y], z) } y == z || v4.Equal(v4.Inverse(f[x := y], z), v4.Difference(v4.Inverse(f, z), v4.Singleton(x)))); + +axiom (forall x: int, S: [int]bool, M: [int]int :: { v4.Dereference(S, M)[x] } v4.Dereference(S, M)[x] ==> (exists y: int :: x == M[y] && S[y])); + +axiom (forall x: int, S: [int]bool, M: [int]int :: { M[x], S[x], v4.Dereference(S, M) } S[x] ==> v4.Dereference(S, M)[M[x]]); + +axiom (forall x: int, y: int, S: [int]bool, M: [int]int :: { v4.Dereference(S, M[x := y]) } !S[x] ==> v4.Equal(v4.Dereference(S, M[x := y]), v4.Dereference(S, M))); + +axiom (forall x: int, y: int, S: [int]bool, M: [int]int :: { v4.Dereference(S, M[x := y]) } S[x] && v4.Equal(v4.Intersection(v4.Inverse(M, M[x]), S), v4.Singleton(x)) ==> v4.Equal(v4.Dereference(S, M[x := y]), v4.Union(v4.Difference(v4.Dereference(S, M), v4.Singleton(M[x])), v4.Singleton(y)))); + +axiom (forall x: int, y: int, S: [int]bool, M: [int]int :: { v4.Dereference(S, M[x := y]) } S[x] && !v4.Equal(v4.Intersection(v4.Inverse(M, M[x]), S), v4.Singleton(x)) ==> v4.Equal(v4.Dereference(S, M[x := y]), v4.Union(v4.Dereference(S, M), v4.Singleton(y)))); + +axiom (forall M: [name][int]int, x: int :: { v4.Unified(M)[x] } v4.Unified(M)[x] == M[v4.Field(x)][x]); + +axiom (forall M: [name][int]int, x: int, y: int :: { v4.Unified(M[v4.Field(x) := M[v4.Field(x)][x := y]]) } v4.Unified(M[v4.Field(x) := M[v4.Field(x)][x := y]]) == v4.Unified(M)[x := y]); + +procedure v2.havoc_assert(i: int); + + + +procedure v2.havoc_assume(i: int); + + + +procedure v2.__HAVOC_free(a: int); + + + +procedure v2.__HAVOC_malloc(obj_size: int) returns (new: int); + free ensures new == _uf_v4.__HAVOC_malloc_new(obj_size); + + + +procedure v2.__HAVOC_det_malloc(obj_size: int) returns (new: int); + free ensures new == _uf_v4.__HAVOC_det_malloc_new(obj_size); + + + +procedure v2.__HAVOC_memset_split_1(A: [int]int, p: int, c: int, n: int) returns (ret: [int]int); + free ensures ret == _uf_v4.__HAVOC_memset_split_1_ret(A, p, c, n); + + + +procedure v2.__HAVOC_memset_split_2(A: [int]int, p: int, c: int, n: int) returns (ret: [int]int); + free ensures ret == _uf_v4.__HAVOC_memset_split_2_ret(A, p, c, n); + + + +procedure v2.__HAVOC_memset_split_4(A: [int]int, p: int, c: int, n: int) returns (ret: [int]int); + free ensures ret == _uf_v4.__HAVOC_memset_split_4_ret(A, p, c, n); + + + +procedure v2.nondet_choice() returns (x: int); + free ensures x == _uf_v4.nondet_choice_x(); + + + +procedure v2.det_choice() returns (x: int); + free ensures x == _uf_v4.det_choice_x(); + + + +procedure v2._strdup(str: int) returns (new: int); + free ensures new == _uf_v4._strdup_new(str); + + + +procedure v2._xstrcasecmp(a0: int, a1: int) returns (ret: int); + free ensures ret == _uf_v4._xstrcasecmp_ret(a0, a1); + + + +procedure v2._xstrcmp(a0: int, a1: int) returns (ret: int); + free ensures ret == _uf_v4._xstrcmp_ret(a0, a1); + + + +procedure {:inline 1} v2.Eval(e_.1: int); + modifies v4.Mem_T.result__EXPR; + free ensures v4.Mem_T.result__EXPR == _uf_v4.Eval_v4.Mem_T.result__EXPR(e_.1, old(v4.alloc), old(v4.Mem_T.oper__EXPR), old(v4.Mem_T.op1__EXPR), old(v4.Mem_T.op2__EXPR), old(v4.Mem_T.result__EXPR), old(v4.isUnsigned)); + + + +procedure v2.EvalEntry1(e_.1: int, outval_.1: int); + modifies v4.Mem_T.result__EXPR, v4.Mem_T.INT4; + free ensures v4.Mem_T.result__EXPR == _uf_v4.EvalEntry1_v4.Mem_T.result__EXPR(e_.1, outval_.1, old(v4.alloc), old(v4.Mem_T.oper__EXPR), old(v4.Mem_T.op1__EXPR), old(v4.Mem_T.op2__EXPR), old(v4.Mem_T.result__EXPR), old(v4.Mem_T.INT4), old(v4.isUnsigned)); + free ensures v4.Mem_T.INT4 == _uf_v4.EvalEntry1_v4.Mem_T.INT4(e_.1, outval_.1, old(v4.alloc), old(v4.Mem_T.oper__EXPR), old(v4.Mem_T.op1__EXPR), old(v4.Mem_T.op2__EXPR), old(v4.Mem_T.result__EXPR), old(v4.Mem_T.INT4), old(v4.isUnsigned)); + + + +procedure v2.EvalEntry2(e_.1: int); + modifies v4.Mem_T.result__EXPR; + free ensures v4.Mem_T.result__EXPR == _uf_v4.EvalEntry2_v4.Mem_T.result__EXPR(e_.1, old(v4.alloc), old(v4.Mem_T.oper__EXPR), old(v4.Mem_T.op1__EXPR), old(v4.Mem_T.op2__EXPR), old(v4.Mem_T.result__EXPR), old(v4.isUnsigned)); + + + +procedure v2.__havoc_heapglobal_init(); + + + +implementation {:inline 1} v2.Eval(e_.1: int) +{ + var havoc_stringTemp: int; + var condVal: int; + var a1: int; + var a2: int; + var e: int; + var op: int; + var res: int; + var tempBoogie0: int; + var tempBoogie1: int; + var tempBoogie2: int; + var tempBoogie3: int; + var tempBoogie4: int; + var tempBoogie5: int; + var tempBoogie6: int; + var tempBoogie7: int; + var tempBoogie8: int; + var tempBoogie9: int; + var tempBoogie10: int; + var tempBoogie11: int; + var tempBoogie12: int; + var tempBoogie13: int; + var tempBoogie14: int; + var tempBoogie15: int; + var tempBoogie16: int; + var tempBoogie17: int; + var tempBoogie18: int; + var tempBoogie19: int; + var __havoc_dummy_return: int; + + anon0#2: + havoc_stringTemp := 0; + goto start#2; + + start#2: + assume v4.INT_LT(e_.1, v4.alloc); + a1 := 0; + a2 := 0; + e := 0; + op := 0; + res := 0; + e := e_.1; + goto label_3#2; + + label_3#2: + assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 17} true; + goto label_4#2; + + label_4#2: + assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 17} true; + goto label_5#2; + + label_5#2: + assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 17} true; + goto label_6#2; + + label_6#2: + assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 17} true; + goto label_7#2; + + label_7#2: + assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 19} true; + assert true; + op := v4.Mem_T.oper__EXPR[v4.oper__EXPR(e)]; + assume v4.value_is(v2.__ctobpl_const_1, op); + assume v4.value_is(v2.__ctobpl_const_2, e); + assume v4.value_is(v2.__ctobpl_const_3, v4.Mem_T.oper__EXPR[v4.oper__EXPR(e)]); + goto label_8#2; + + label_8#2: + assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 20} true; + assert true; + a1 := v4.Mem_T.op1__EXPR[v4.op1__EXPR(e)]; + assume v4.value_is(v2.__ctobpl_const_4, a1); + assume v4.value_is(v2.__ctobpl_const_5, e); + assume v4.value_is(v2.__ctobpl_const_6, v4.Mem_T.op1__EXPR[v4.op1__EXPR(e)]); + goto label_9#2; + + label_9#2: + assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 21} true; + assert true; + a2 := v4.Mem_T.op2__EXPR[v4.op2__EXPR(e)]; + assume v4.value_is(v2.__ctobpl_const_7, a2); + assume v4.value_is(v2.__ctobpl_const_8, e); + assume v4.value_is(v2.__ctobpl_const_9, v4.Mem_T.op2__EXPR[v4.op2__EXPR(e)]); + goto label_10#2; + + label_10#2: + assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 22} true; + res := 0 - 1; + assume v4.value_is(v2.__ctobpl_const_10, res); + goto label_11#2; + + label_11#2: + assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 24} true; + goto label_11_case_0#2, label_11_case_1#2, label_11_case_2#2; + + label_11_case_2#2: + assume v4.INT_EQ(op, 2); + assume v4.value_is(v2.__ctobpl_const_11, op); + goto label_14#2; + + label_14#2: + assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 29} true; + res := v4.MINUS_BOTH_PTR_OR_BOTH_INT(a1, a2, 1); + assume v4.value_is(v2.__ctobpl_const_18, res); + assume v4.value_is(v2.__ctobpl_const_19, a1); + assume v4.value_is(v2.__ctobpl_const_20, a2); + goto label_12#2; + + label_11_case_1#2: + assume v4.INT_EQ(op, 1); + assume v4.value_is(v2.__ctobpl_const_11, op); + goto label_13#2; + + label_13#2: + assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 27} true; + res := v4.PLUS(a1, 1, a2); + assume v4.value_is(v2.__ctobpl_const_15, res); + assume v4.value_is(v2.__ctobpl_const_16, a1); + assume v4.value_is(v2.__ctobpl_const_17, a2); + goto label_12#2; + + label_11_case_0#2: + assume v4.INT_NEQ(op, 1); + assume v4.INT_NEQ(op, 2); + assume v4.value_is(v2.__ctobpl_const_11, op); + goto label_12#2; + + label_12#2: + assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 35} true; + assert true; + v4.Mem_T.result__EXPR := v4.Mem_T.result__EXPR[v4.result__EXPR(e) := res]; + assume v4.value_is(v2.__ctobpl_const_12, e); + assume v4.value_is(v2.__ctobpl_const_13, v4.Mem_T.result__EXPR[v4.result__EXPR(e)]); + assume v4.value_is(v2.__ctobpl_const_14, res); + goto label_1#2; + + label_1#2: + assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 36} true; + return; +} + + + +implementation v2.EvalEntry1(e_.1: int, outval_.1: int) +{ + var havoc_stringTemp: int; + var condVal: int; + var e: int; + var outval: int; + var tempBoogie0: int; + var tempBoogie1: int; + var tempBoogie2: int; + var tempBoogie3: int; + var tempBoogie4: int; + var tempBoogie5: int; + var tempBoogie6: int; + var tempBoogie7: int; + var tempBoogie8: int; + var tempBoogie9: int; + var tempBoogie10: int; + var tempBoogie11: int; + var tempBoogie12: int; + var tempBoogie13: int; + var tempBoogie14: int; + var tempBoogie15: int; + var tempBoogie16: int; + var tempBoogie17: int; + var tempBoogie18: int; + var tempBoogie19: int; + var __havoc_dummy_return: int; + + anon0#2: + havoc_stringTemp := 0; + goto start#2; + + start#2: + assume v4.INT_LT(e_.1, v4.alloc); + assume v4.INT_LT(outval_.1, v4.alloc); + e := 0; + outval := 0; + e := e_.1; + outval := outval_.1; + goto label_3#2; + + label_3#2: + assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 40} true; + call v2.Eval(e); + assume v4.value_is(v2.__ctobpl_const_21, e); + assume v4.value_is(v2.__ctobpl_const_22, e); + goto label_6#2; + + label_6#2: + assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 41} true; + assert true; + assert true; + v4.Mem_T.INT4 := v4.Mem_T.INT4[outval := v4.Mem_T.result__EXPR[v4.result__EXPR(e)]]; + assume v4.value_is(v2.__ctobpl_const_23, outval); + assume v4.value_is(v2.__ctobpl_const_24, v4.Mem_T.INT4[outval]); + assume v4.value_is(v2.__ctobpl_const_25, e); + assume v4.value_is(v2.__ctobpl_const_26, v4.Mem_T.result__EXPR[v4.result__EXPR(e)]); + goto label_1#2; + + label_1#2: + assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 42} true; + return; +} + + + +implementation v2.EvalEntry2(e_.1: int) +{ + var havoc_stringTemp: int; + var condVal: int; + var e: int; + var tempBoogie0: int; + var tempBoogie1: int; + var tempBoogie2: int; + var tempBoogie3: int; + var tempBoogie4: int; + var tempBoogie5: int; + var tempBoogie6: int; + var tempBoogie7: int; + var tempBoogie8: int; + var tempBoogie9: int; + var tempBoogie10: int; + var tempBoogie11: int; + var tempBoogie12: int; + var tempBoogie13: int; + var tempBoogie14: int; + var tempBoogie15: int; + var tempBoogie16: int; + var tempBoogie17: int; + var tempBoogie18: int; + var tempBoogie19: int; + var __havoc_dummy_return: int; + + anon0#2: + havoc_stringTemp := 0; + goto start#2; + + start#2: + assume v4.INT_LT(e_.1, v4.alloc); + e := 0; + e := e_.1; + goto label_3#2; + + label_3#2: + assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 46} true; + call v2.Eval(e); + assume v4.value_is(v2.__ctobpl_const_27, e); + assume v4.value_is(v2.__ctobpl_const_28, e); + goto label_1#2; + + label_1#2: + assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 47} true; + return; +} + + + +implementation v2.__havoc_heapglobal_init() +{ + + anon0#2: + return; +} + + + +type name; + +type byte; + +var Output_of_v2.Eval_v4.Mem_T.result__EXPR: [int]int; + +var Output_of_v4.Eval_v4.Mem_T.result__EXPR: [int]int; + +procedure EQ_v2.Eval__v4.Eval(e_.1: int) returns (AA_TEMP30: bool); + modifies v4.Mem_T.result__EXPR, Output_of_v2.Eval_v4.Mem_T.result__EXPR, Output_of_v4.Eval_v4.Mem_T.result__EXPR; + ensures AA_TEMP30; + + + +implementation EQ_v2.Eval__v4.Eval(e_.1: int) returns (AA_TEMP30: bool) +{ + var AA_TEMP10: [int]int; + var AA_TEMP00: [int]int; + var inline$v2.Eval$0$havoc_stringTemp: int; + var inline$v2.Eval$0$condVal: int; + var inline$v2.Eval$0$a1: int; + var inline$v2.Eval$0$a2: int; + var inline$v2.Eval$0$e: int; + var inline$v2.Eval$0$op: int; + var inline$v2.Eval$0$res: int; + var inline$v2.Eval$0$tempBoogie0: int; + var inline$v2.Eval$0$tempBoogie1: int; + var inline$v2.Eval$0$tempBoogie2: int; + var inline$v2.Eval$0$tempBoogie3: int; + var inline$v2.Eval$0$tempBoogie4: int; + var inline$v2.Eval$0$tempBoogie5: int; + var inline$v2.Eval$0$tempBoogie6: int; + var inline$v2.Eval$0$tempBoogie7: int; + var inline$v2.Eval$0$tempBoogie8: int; + var inline$v2.Eval$0$tempBoogie9: int; + var inline$v2.Eval$0$tempBoogie10: int; + var inline$v2.Eval$0$tempBoogie11: int; + var inline$v2.Eval$0$tempBoogie12: int; + var inline$v2.Eval$0$tempBoogie13: int; + var inline$v2.Eval$0$tempBoogie14: int; + var inline$v2.Eval$0$tempBoogie15: int; + var inline$v2.Eval$0$tempBoogie16: int; + var inline$v2.Eval$0$tempBoogie17: int; + var inline$v2.Eval$0$tempBoogie18: int; + var inline$v2.Eval$0$tempBoogie19: int; + var inline$v2.Eval$0$__havoc_dummy_return: int; + var inline$v2.Eval$0$e_.1: int; + var inline$v2.Eval$0$v4.Mem_T.result__EXPR: [int]int; + var inline$v4.Eval$0$havoc_stringTemp: int; + var inline$v4.Eval$0$condVal: int; + var inline$v4.Eval$0$a1: int; + var inline$v4.Eval$0$a2: int; + var inline$v4.Eval$0$e: int; + var inline$v4.Eval$0$op: int; + var inline$v4.Eval$0$res: int; + var inline$v4.Eval$0$result.UnsignedAdd$1: int; + var inline$v4.Eval$0$result.UnsignedSub$2: int; + var inline$v4.Eval$0$tempBoogie0: int; + var inline$v4.Eval$0$tempBoogie1: int; + var inline$v4.Eval$0$tempBoogie2: int; + var inline$v4.Eval$0$tempBoogie3: int; + var inline$v4.Eval$0$tempBoogie4: int; + var inline$v4.Eval$0$tempBoogie5: int; + var inline$v4.Eval$0$tempBoogie6: int; + var inline$v4.Eval$0$tempBoogie7: int; + var inline$v4.Eval$0$tempBoogie8: int; + var inline$v4.Eval$0$tempBoogie9: int; + var inline$v4.Eval$0$tempBoogie10: int; + var inline$v4.Eval$0$tempBoogie11: int; + var inline$v4.Eval$0$tempBoogie12: int; + var inline$v4.Eval$0$tempBoogie13: int; + var inline$v4.Eval$0$tempBoogie14: int; + var inline$v4.Eval$0$tempBoogie15: int; + var inline$v4.Eval$0$tempBoogie16: int; + var inline$v4.Eval$0$tempBoogie17: int; + var inline$v4.Eval$0$tempBoogie18: int; + var inline$v4.Eval$0$tempBoogie19: int; + var inline$v4.Eval$0$__havoc_dummy_return: int; + var inline$v4.Eval$0$e_.1: int; + var inline$v4.Eval$0$v4.Mem_T.result__EXPR: [int]int; + + AA_INSTR_EQ_BODY: + AA_TEMP00 := v4.Mem_T.result__EXPR; + goto inline$v2.Eval$0$Entry; + + inline$v2.Eval$0$Entry: + inline$v2.Eval$0$e_.1 := e_.1; + inline$v2.Eval$0$v4.Mem_T.result__EXPR := v4.Mem_T.result__EXPR; + goto inline$v2.Eval$0$anon0#2; + + inline$v2.Eval$0$anon0#2: + inline$v2.Eval$0$havoc_stringTemp := 0; + goto inline$v2.Eval$0$start#2; + + inline$v2.Eval$0$start#2: + assume v4.INT_LT(inline$v2.Eval$0$e_.1, v4.alloc); + inline$v2.Eval$0$a1 := 0; + inline$v2.Eval$0$a2 := 0; + inline$v2.Eval$0$e := 0; + inline$v2.Eval$0$op := 0; + inline$v2.Eval$0$res := 0; + inline$v2.Eval$0$e := inline$v2.Eval$0$e_.1; + goto inline$v2.Eval$0$label_3#2; + + inline$v2.Eval$0$label_3#2: + assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 17} true; + goto inline$v2.Eval$0$label_4#2; + + inline$v2.Eval$0$label_4#2: + assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 17} true; + goto inline$v2.Eval$0$label_5#2; + + inline$v2.Eval$0$label_5#2: + assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 17} true; + goto inline$v2.Eval$0$label_6#2; + + inline$v2.Eval$0$label_6#2: + assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 17} true; + goto inline$v2.Eval$0$label_7#2; + + inline$v2.Eval$0$label_7#2: + assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 19} true; + assert true; + inline$v2.Eval$0$op := v4.Mem_T.oper__EXPR[v4.oper__EXPR(inline$v2.Eval$0$e)]; + assume v4.value_is(v2.__ctobpl_const_1, inline$v2.Eval$0$op); + assume v4.value_is(v2.__ctobpl_const_2, inline$v2.Eval$0$e); + assume v4.value_is(v2.__ctobpl_const_3, v4.Mem_T.oper__EXPR[v4.oper__EXPR(inline$v2.Eval$0$e)]); + goto inline$v2.Eval$0$label_8#2; + + inline$v2.Eval$0$label_8#2: + assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 20} true; + assert true; + inline$v2.Eval$0$a1 := v4.Mem_T.op1__EXPR[v4.op1__EXPR(inline$v2.Eval$0$e)]; + assume v4.value_is(v2.__ctobpl_const_4, inline$v2.Eval$0$a1); + assume v4.value_is(v2.__ctobpl_const_5, inline$v2.Eval$0$e); + assume v4.value_is(v2.__ctobpl_const_6, v4.Mem_T.op1__EXPR[v4.op1__EXPR(inline$v2.Eval$0$e)]); + goto inline$v2.Eval$0$label_9#2; + + inline$v2.Eval$0$label_9#2: + assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 21} true; + assert true; + inline$v2.Eval$0$a2 := v4.Mem_T.op2__EXPR[v4.op2__EXPR(inline$v2.Eval$0$e)]; + assume v4.value_is(v2.__ctobpl_const_7, inline$v2.Eval$0$a2); + assume v4.value_is(v2.__ctobpl_const_8, inline$v2.Eval$0$e); + assume v4.value_is(v2.__ctobpl_const_9, v4.Mem_T.op2__EXPR[v4.op2__EXPR(inline$v2.Eval$0$e)]); + goto inline$v2.Eval$0$label_10#2; + + inline$v2.Eval$0$label_10#2: + assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 22} true; + inline$v2.Eval$0$res := 0 - 1; + assume v4.value_is(v2.__ctobpl_const_10, inline$v2.Eval$0$res); + goto inline$v2.Eval$0$label_11#2; + + inline$v2.Eval$0$label_11#2: + assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 24} true; + goto inline$v2.Eval$0$label_11_case_0#2, inline$v2.Eval$0$label_11_case_1#2, inline$v2.Eval$0$label_11_case_2#2; + + inline$v2.Eval$0$label_11_case_2#2: + assume v4.INT_EQ(inline$v2.Eval$0$op, 2); + assume v4.value_is(v2.__ctobpl_const_11, inline$v2.Eval$0$op); + goto inline$v2.Eval$0$label_14#2; + + inline$v2.Eval$0$label_14#2: + assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 29} true; + inline$v2.Eval$0$res := v4.MINUS_BOTH_PTR_OR_BOTH_INT(inline$v2.Eval$0$a1, inline$v2.Eval$0$a2, 1); + assume v4.value_is(v2.__ctobpl_const_18, inline$v2.Eval$0$res); + assume v4.value_is(v2.__ctobpl_const_19, inline$v2.Eval$0$a1); + assume v4.value_is(v2.__ctobpl_const_20, inline$v2.Eval$0$a2); + goto inline$v2.Eval$0$label_12#2; + + inline$v2.Eval$0$label_11_case_1#2: + assume v4.INT_EQ(inline$v2.Eval$0$op, 1); + assume v4.value_is(v2.__ctobpl_const_11, inline$v2.Eval$0$op); + goto inline$v2.Eval$0$label_13#2; + + inline$v2.Eval$0$label_13#2: + assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 27} true; + inline$v2.Eval$0$res := v4.PLUS(inline$v2.Eval$0$a1, 1, inline$v2.Eval$0$a2); + assume v4.value_is(v2.__ctobpl_const_15, inline$v2.Eval$0$res); + assume v4.value_is(v2.__ctobpl_const_16, inline$v2.Eval$0$a1); + assume v4.value_is(v2.__ctobpl_const_17, inline$v2.Eval$0$a2); + goto inline$v2.Eval$0$label_12#2; + + inline$v2.Eval$0$label_11_case_0#2: + assume v4.INT_NEQ(inline$v2.Eval$0$op, 1); + assume v4.INT_NEQ(inline$v2.Eval$0$op, 2); + assume v4.value_is(v2.__ctobpl_const_11, inline$v2.Eval$0$op); + goto inline$v2.Eval$0$label_12#2; + + inline$v2.Eval$0$label_12#2: + assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 35} true; + assert true; + v4.Mem_T.result__EXPR := v4.Mem_T.result__EXPR[v4.result__EXPR(inline$v2.Eval$0$e) := inline$v2.Eval$0$res]; + assume v4.value_is(v2.__ctobpl_const_12, inline$v2.Eval$0$e); + assume v4.value_is(v2.__ctobpl_const_13, v4.Mem_T.result__EXPR[v4.result__EXPR(inline$v2.Eval$0$e)]); + assume v4.value_is(v2.__ctobpl_const_14, inline$v2.Eval$0$res); + goto inline$v2.Eval$0$label_1#2; + + inline$v2.Eval$0$label_1#2: + assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 36} true; + goto inline$v2.Eval$0$Return; + + inline$v2.Eval$0$Return: + goto AA_INSTR_EQ_BODY$1; + + AA_INSTR_EQ_BODY$1: + AA_TEMP10 := v4.Mem_T.result__EXPR; + v4.Mem_T.result__EXPR := AA_TEMP00; + goto inline$v4.Eval$0$Entry; + + inline$v4.Eval$0$Entry: + inline$v4.Eval$0$e_.1 := e_.1; + inline$v4.Eval$0$v4.Mem_T.result__EXPR := v4.Mem_T.result__EXPR; + goto inline$v4.Eval$0$anon0#2; + + inline$v4.Eval$0$anon0#2: + inline$v4.Eval$0$havoc_stringTemp := 0; + goto inline$v4.Eval$0$start#2; + + inline$v4.Eval$0$start#2: + assume v4.INT_LT(inline$v4.Eval$0$e_.1, v4.alloc); + inline$v4.Eval$0$a1 := 0; + inline$v4.Eval$0$a2 := 0; + inline$v4.Eval$0$e := 0; + inline$v4.Eval$0$op := 0; + inline$v4.Eval$0$res := 0; + inline$v4.Eval$0$result.UnsignedAdd$1 := 0; + inline$v4.Eval$0$result.UnsignedSub$2 := 0; + inline$v4.Eval$0$e := inline$v4.Eval$0$e_.1; + goto inline$v4.Eval$0$label_3#2; + + inline$v4.Eval$0$label_3#2: + assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 19} true; + goto inline$v4.Eval$0$label_4#2; + + inline$v4.Eval$0$label_4#2: + assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 19} true; + goto inline$v4.Eval$0$label_5#2; + + inline$v4.Eval$0$label_5#2: + assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 19} true; + goto inline$v4.Eval$0$label_6#2; + + inline$v4.Eval$0$label_6#2: + assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 19} true; + goto inline$v4.Eval$0$label_7#2; + + inline$v4.Eval$0$label_7#2: + assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 21} true; + assert true; + inline$v4.Eval$0$op := v4.Mem_T.oper__EXPR[v4.oper__EXPR(inline$v4.Eval$0$e)]; + assume v4.value_is(v4.__ctobpl_const_1, inline$v4.Eval$0$op); + assume v4.value_is(v4.__ctobpl_const_2, inline$v4.Eval$0$e); + assume v4.value_is(v4.__ctobpl_const_3, v4.Mem_T.oper__EXPR[v4.oper__EXPR(inline$v4.Eval$0$e)]); + goto inline$v4.Eval$0$label_8#2; + + inline$v4.Eval$0$label_8#2: + assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 22} true; + assert true; + inline$v4.Eval$0$a1 := v4.Mem_T.op1__EXPR[v4.op1__EXPR(inline$v4.Eval$0$e)]; + assume v4.value_is(v4.__ctobpl_const_4, inline$v4.Eval$0$a1); + assume v4.value_is(v4.__ctobpl_const_5, inline$v4.Eval$0$e); + assume v4.value_is(v4.__ctobpl_const_6, v4.Mem_T.op1__EXPR[v4.op1__EXPR(inline$v4.Eval$0$e)]); + goto inline$v4.Eval$0$label_9#2; + + inline$v4.Eval$0$label_9#2: + assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 23} true; + assert true; + inline$v4.Eval$0$a2 := v4.Mem_T.op2__EXPR[v4.op2__EXPR(inline$v4.Eval$0$e)]; + assume v4.value_is(v4.__ctobpl_const_7, inline$v4.Eval$0$a2); + assume v4.value_is(v4.__ctobpl_const_8, inline$v4.Eval$0$e); + assume v4.value_is(v4.__ctobpl_const_9, v4.Mem_T.op2__EXPR[v4.op2__EXPR(inline$v4.Eval$0$e)]); + goto inline$v4.Eval$0$label_10#2; + + inline$v4.Eval$0$label_10#2: + assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 24} true; + inline$v4.Eval$0$res := 0 - 1; + assume v4.value_is(v4.__ctobpl_const_10, inline$v4.Eval$0$res); + goto inline$v4.Eval$0$label_11#2; + + inline$v4.Eval$0$label_11#2: + assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 26} true; + goto inline$v4.Eval$0$label_11_case_0#2, inline$v4.Eval$0$label_11_case_1#2, inline$v4.Eval$0$label_11_case_2#2; + + inline$v4.Eval$0$label_11_case_2#2: + assume v4.INT_EQ(inline$v4.Eval$0$op, 2); + assume v4.value_is(v4.__ctobpl_const_11, inline$v4.Eval$0$op); + goto inline$v4.Eval$0$label_14#2; + + inline$v4.Eval$0$label_14#2: + assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 35} true; + goto inline$v4.Eval$0$label_14_true#2, inline$v4.Eval$0$label_14_false#2; + + inline$v4.Eval$0$label_14_false#2: + assume v4.isUnsigned == 0; + assume v4.value_is(v4.__ctobpl_const_16, v4.isUnsigned); + goto inline$v4.Eval$0$label_15#2; + + inline$v4.Eval$0$label_15#2: + assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 38} true; + inline$v4.Eval$0$res := v4.MINUS_BOTH_PTR_OR_BOTH_INT(inline$v4.Eval$0$a1, inline$v4.Eval$0$a2, 1); + assume v4.value_is(v4.__ctobpl_const_17, inline$v4.Eval$0$res); + assume v4.value_is(v4.__ctobpl_const_18, inline$v4.Eval$0$a1); + assume v4.value_is(v4.__ctobpl_const_19, inline$v4.Eval$0$a2); + goto inline$v4.Eval$0$label_12#2; + + inline$v4.Eval$0$label_14_true#2: + assume v4.isUnsigned != 0; + assume v4.value_is(v4.__ctobpl_const_16, v4.isUnsigned); + goto inline$v4.Eval$0$label_16#2; + + inline$v4.Eval$0$label_16#2: + assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 36} true; + call inline$v4.Eval$0$result.UnsignedSub$2 := v4.UnsignedSub(inline$v4.Eval$0$a1, inline$v4.Eval$0$a2); + assume v4.value_is(v4.__ctobpl_const_20, inline$v4.Eval$0$a1); + assume v4.value_is(v4.__ctobpl_const_21, inline$v4.Eval$0$a2); + assume v4.value_is(v4.__ctobpl_const_22, inline$v4.Eval$0$a1); + assume v4.value_is(v4.__ctobpl_const_23, inline$v4.Eval$0$a2); + goto inline$v4.Eval$0$label_19#2; + + inline$v4.Eval$0$label_19#2: + assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 36} true; + inline$v4.Eval$0$res := inline$v4.Eval$0$result.UnsignedSub$2; + assume v4.value_is(v4.__ctobpl_const_24, inline$v4.Eval$0$res); + assume v4.value_is(v4.__ctobpl_const_25, inline$v4.Eval$0$result.UnsignedSub$2); + goto inline$v4.Eval$0$label_12#2; + + inline$v4.Eval$0$label_11_case_1#2: + assume v4.INT_EQ(inline$v4.Eval$0$op, 1); + assume v4.value_is(v4.__ctobpl_const_11, inline$v4.Eval$0$op); + goto inline$v4.Eval$0$label_13#2; + + inline$v4.Eval$0$label_13#2: + assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 29} true; + goto inline$v4.Eval$0$label_13_true#2, inline$v4.Eval$0$label_13_false#2; + + inline$v4.Eval$0$label_13_false#2: + assume v4.isUnsigned == 0; + assume v4.value_is(v4.__ctobpl_const_15, v4.isUnsigned); + goto inline$v4.Eval$0$label_20#2; + + inline$v4.Eval$0$label_20#2: + assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 32} true; + inline$v4.Eval$0$res := v4.PLUS(inline$v4.Eval$0$a1, 1, inline$v4.Eval$0$a2); + assume v4.value_is(v4.__ctobpl_const_26, inline$v4.Eval$0$res); + assume v4.value_is(v4.__ctobpl_const_27, inline$v4.Eval$0$a1); + assume v4.value_is(v4.__ctobpl_const_28, inline$v4.Eval$0$a2); + goto inline$v4.Eval$0$label_12#2; + + inline$v4.Eval$0$label_13_true#2: + assume v4.isUnsigned != 0; + assume v4.value_is(v4.__ctobpl_const_15, v4.isUnsigned); + goto inline$v4.Eval$0$label_21#2; + + inline$v4.Eval$0$label_21#2: + assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 30} true; + call inline$v4.Eval$0$result.UnsignedAdd$1 := v4.UnsignedAdd(inline$v4.Eval$0$a1, inline$v4.Eval$0$a2); + assume v4.value_is(v4.__ctobpl_const_29, inline$v4.Eval$0$a1); + assume v4.value_is(v4.__ctobpl_const_30, inline$v4.Eval$0$a2); + assume v4.value_is(v4.__ctobpl_const_31, inline$v4.Eval$0$a1); + assume v4.value_is(v4.__ctobpl_const_32, inline$v4.Eval$0$a2); + goto inline$v4.Eval$0$label_24#2; + + inline$v4.Eval$0$label_24#2: + assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 30} true; + inline$v4.Eval$0$res := inline$v4.Eval$0$result.UnsignedAdd$1; + assume v4.value_is(v4.__ctobpl_const_33, inline$v4.Eval$0$res); + assume v4.value_is(v4.__ctobpl_const_34, inline$v4.Eval$0$result.UnsignedAdd$1); + goto inline$v4.Eval$0$label_12#2; + + inline$v4.Eval$0$label_11_case_0#2: + assume v4.INT_NEQ(inline$v4.Eval$0$op, 1); + assume v4.INT_NEQ(inline$v4.Eval$0$op, 2); + assume v4.value_is(v4.__ctobpl_const_11, inline$v4.Eval$0$op); + goto inline$v4.Eval$0$label_12#2; + + inline$v4.Eval$0$label_12#2: + assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 41} true; + assert true; + v4.Mem_T.result__EXPR := v4.Mem_T.result__EXPR[v4.result__EXPR(inline$v4.Eval$0$e) := inline$v4.Eval$0$res]; + assume v4.value_is(v4.__ctobpl_const_12, inline$v4.Eval$0$e); + assume v4.value_is(v4.__ctobpl_const_13, v4.Mem_T.result__EXPR[v4.result__EXPR(inline$v4.Eval$0$e)]); + assume v4.value_is(v4.__ctobpl_const_14, inline$v4.Eval$0$res); + goto inline$v4.Eval$0$label_1#2; + + inline$v4.Eval$0$label_1#2: + assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 42} true; + goto inline$v4.Eval$0$Return; + + inline$v4.Eval$0$Return: + goto AA_INSTR_EQ_BODY$2; + + AA_INSTR_EQ_BODY$2: + Output_of_v2.Eval_v4.Mem_T.result__EXPR := AA_TEMP10; + Output_of_v4.Eval_v4.Mem_T.result__EXPR := v4.Mem_T.result__EXPR; + AA_TEMP30 := AA_TEMP10 == v4.Mem_T.result__EXPR || (forall _x0: int :: AA_TEMP10[_x0] == v4.Mem_T.result__EXPR[_x0]); + return; +} + + + +var Output_of_v2.EvalEntry1_v4.Mem_T.result__EXPR: [int]int; + +var Output_of_v4.EvalEntry1_v4.Mem_T.result__EXPR: [int]int; + +var Output_of_v2.EvalEntry1_v4.Mem_T.INT4: [int]int; + +var Output_of_v4.EvalEntry1_v4.Mem_T.INT4: [int]int; + +var Output_of_v2.EvalEntry1_v4.isUnsigned: int; + +var Output_of_v4.EvalEntry1_v4.isUnsigned: int; + +procedure EQ_v2.EvalEntry1__v4.EvalEntry1(e_.1: int, outval_.1: int) returns (AA_TEMP80: bool, AA_TEMP81: bool, AA_TEMP82: bool); + modifies v4.Mem_T.result__EXPR, v4.Mem_T.INT4, v4.isUnsigned, Output_of_v2.EvalEntry1_v4.Mem_T.result__EXPR, Output_of_v4.EvalEntry1_v4.Mem_T.result__EXPR, Output_of_v2.EvalEntry1_v4.Mem_T.INT4, Output_of_v4.EvalEntry1_v4.Mem_T.INT4, Output_of_v2.EvalEntry1_v4.isUnsigned, Output_of_v4.EvalEntry1_v4.isUnsigned; + ensures AA_TEMP82 && AA_TEMP81 && AA_TEMP80; + + + +implementation EQ_v2.EvalEntry1__v4.EvalEntry1(e_.1: int, outval_.1: int) returns (AA_TEMP80: bool, AA_TEMP81: bool, AA_TEMP82: bool) +{ + var AA_TEMP60: [int]int; + var AA_TEMP61: [int]int; + var AA_TEMP62: int; + var AA_TEMP50: [int]int; + var AA_TEMP51: [int]int; + var AA_TEMP52: int; + + AA_INSTR_EQ_BODY: + AA_TEMP50 := v4.Mem_T.result__EXPR; + AA_TEMP51 := v4.Mem_T.INT4; + AA_TEMP52 := v4.isUnsigned; + call v2.EvalEntry1(e_.1, outval_.1); + AA_TEMP60 := v4.Mem_T.result__EXPR; + AA_TEMP61 := v4.Mem_T.INT4; + AA_TEMP62 := v4.isUnsigned; + v4.Mem_T.result__EXPR := AA_TEMP50; + v4.Mem_T.INT4 := AA_TEMP51; + v4.isUnsigned := AA_TEMP52; + call v4.EvalEntry1(e_.1, outval_.1); + Output_of_v2.EvalEntry1_v4.Mem_T.result__EXPR := AA_TEMP60; + Output_of_v4.EvalEntry1_v4.Mem_T.result__EXPR := v4.Mem_T.result__EXPR; + Output_of_v2.EvalEntry1_v4.Mem_T.INT4 := AA_TEMP61; + Output_of_v4.EvalEntry1_v4.Mem_T.INT4 := v4.Mem_T.INT4; + Output_of_v2.EvalEntry1_v4.isUnsigned := AA_TEMP62; + Output_of_v4.EvalEntry1_v4.isUnsigned := v4.isUnsigned; + AA_TEMP80, AA_TEMP81, AA_TEMP82 := AA_TEMP60 == v4.Mem_T.result__EXPR || (forall _x0: int :: AA_TEMP60[_x0] == v4.Mem_T.result__EXPR[_x0]), AA_TEMP61 == v4.Mem_T.INT4 || (forall _x0: int :: AA_TEMP61[_x0] == v4.Mem_T.INT4[_x0]), AA_TEMP62 == v4.isUnsigned; + return; +} + + + +var Output_of_v2.EvalEntry2_v4.Mem_T.result__EXPR: [int]int; + +var Output_of_v4.EvalEntry2_v4.Mem_T.result__EXPR: [int]int; + +var Output_of_v2.EvalEntry2_v4.isUnsigned: int; + +var Output_of_v4.EvalEntry2_v4.isUnsigned: int; + +procedure EQ_v2.EvalEntry2__v4.EvalEntry2(e_.1: int) returns (AA_TEMP130: bool, AA_TEMP131: bool); + modifies v4.Mem_T.result__EXPR, v4.isUnsigned, Output_of_v2.EvalEntry2_v4.Mem_T.result__EXPR, Output_of_v4.EvalEntry2_v4.Mem_T.result__EXPR, Output_of_v2.EvalEntry2_v4.isUnsigned, Output_of_v4.EvalEntry2_v4.isUnsigned; + ensures AA_TEMP131 && AA_TEMP130; + + + +implementation EQ_v2.EvalEntry2__v4.EvalEntry2(e_.1: int) returns (AA_TEMP130: bool, AA_TEMP131: bool) +{ + var AA_TEMP110: [int]int; + var AA_TEMP111: int; + var AA_TEMP100: [int]int; + var AA_TEMP101: int; + + AA_INSTR_EQ_BODY: + AA_TEMP100 := v4.Mem_T.result__EXPR; + AA_TEMP101 := v4.isUnsigned; + call v2.EvalEntry2(e_.1); + AA_TEMP110 := v4.Mem_T.result__EXPR; + AA_TEMP111 := v4.isUnsigned; + v4.Mem_T.result__EXPR := AA_TEMP100; + v4.isUnsigned := AA_TEMP101; + call v4.EvalEntry2(e_.1); + Output_of_v2.EvalEntry2_v4.Mem_T.result__EXPR := AA_TEMP110; + Output_of_v4.EvalEntry2_v4.Mem_T.result__EXPR := v4.Mem_T.result__EXPR; + Output_of_v2.EvalEntry2_v4.isUnsigned := AA_TEMP111; + Output_of_v4.EvalEntry2_v4.isUnsigned := v4.isUnsigned; + AA_TEMP130, AA_TEMP131 := AA_TEMP110 == v4.Mem_T.result__EXPR || (forall _x0: int :: AA_TEMP110[_x0] == v4.Mem_T.result__EXPR[_x0]), AA_TEMP111 == v4.isUnsigned; + return; +} + + + +function _uf_v4.__HAVOC_malloc_new(arg_0: int) : int; + +function _uf_v2.__HAVOC_malloc_new(arg_0: int) : int; + +function _uf_v4.__HAVOC_det_malloc_new(arg_0: int) : int; + +function _uf_v2.__HAVOC_det_malloc_new(arg_0: int) : int; + +function _uf_v4.__HAVOC_memset_split_1_ret(arg_0: [int]int, arg_1: int, arg_2: int, arg_3: int) : [int]int; + +function _uf_v2.__HAVOC_memset_split_1_ret(arg_0: [int]int, arg_1: int, arg_2: int, arg_3: int) : [int]int; + +function _uf_v4.__HAVOC_memset_split_2_ret(arg_0: [int]int, arg_1: int, arg_2: int, arg_3: int) : [int]int; + +function _uf_v2.__HAVOC_memset_split_2_ret(arg_0: [int]int, arg_1: int, arg_2: int, arg_3: int) : [int]int; + +function _uf_v4.__HAVOC_memset_split_4_ret(arg_0: [int]int, arg_1: int, arg_2: int, arg_3: int) : [int]int; + +function _uf_v2.__HAVOC_memset_split_4_ret(arg_0: [int]int, arg_1: int, arg_2: int, arg_3: int) : [int]int; + +function _uf_v4.nondet_choice_x() : int; + +function _uf_v2.nondet_choice_x() : int; + +function _uf_v4.det_choice_x() : int; + +function _uf_v2.det_choice_x() : int; + +function _uf_v4._strdup_new(arg_0: int) : int; + +function _uf_v2._strdup_new(arg_0: int) : int; + +function _uf_v4._xstrcasecmp_ret(arg_0: int, arg_1: int) : int; + +function _uf_v2._xstrcasecmp_ret(arg_0: int, arg_1: int) : int; + +function _uf_v4._xstrcmp_ret(arg_0: int, arg_1: int) : int; + +function _uf_v2._xstrcmp_ret(arg_0: int, arg_1: int) : int; + +function _uf_v4.Eval_v4.Mem_T.result__EXPR(arg_0: int, arg_1: int, arg_2: [int]int, arg_3: [int]int, arg_4: [int]int, arg_5: [int]int, arg_6: int) : [int]int; + +function _uf_v2.Eval_v4.Mem_T.result__EXPR(arg_0: int, arg_1: int, arg_2: [int]int, arg_3: [int]int, arg_4: [int]int, arg_5: [int]int, arg_6: int) : [int]int; + +function _uf_v4.EvalEntry1_v4.Mem_T.result__EXPR(arg_0: int, arg_1: int, arg_2: int, arg_3: [int]int, arg_4: [int]int, arg_5: [int]int, arg_6: [int]int, arg_7: [int]int, arg_8: int) : [int]int; + +function _uf_v4.EvalEntry1_v4.Mem_T.INT4(arg_0: int, arg_1: int, arg_2: int, arg_3: [int]int, arg_4: [int]int, arg_5: [int]int, arg_6: [int]int, arg_7: [int]int, arg_8: int) : [int]int; + +function _uf_v4.EvalEntry1_v4.isUnsigned(arg_0: int, arg_1: int, arg_2: int, arg_3: [int]int, arg_4: [int]int, arg_5: [int]int, arg_6: [int]int, arg_7: [int]int, arg_8: int) : int; + +function _uf_v2.EvalEntry1_v4.Mem_T.result__EXPR(arg_0: int, arg_1: int, arg_2: int, arg_3: [int]int, arg_4: [int]int, arg_5: [int]int, arg_6: [int]int, arg_7: [int]int, arg_8: int) : [int]int; + +function _uf_v2.EvalEntry1_v4.Mem_T.INT4(arg_0: int, arg_1: int, arg_2: int, arg_3: [int]int, arg_4: [int]int, arg_5: [int]int, arg_6: [int]int, arg_7: [int]int, arg_8: int) : [int]int; + +function _uf_v4.EvalEntry2_v4.Mem_T.result__EXPR(arg_0: int, arg_1: int, arg_2: [int]int, arg_3: [int]int, arg_4: [int]int, arg_5: [int]int, arg_6: int) : [int]int; + +function _uf_v4.EvalEntry2_v4.isUnsigned(arg_0: int, arg_1: int, arg_2: [int]int, arg_3: [int]int, arg_4: [int]int, arg_5: [int]int, arg_6: int) : int; + +function _uf_v2.EvalEntry2_v4.Mem_T.result__EXPR(arg_0: int, arg_1: int, arg_2: [int]int, arg_3: [int]int, arg_4: [int]int, arg_5: [int]int, arg_6: int) : [int]int; diff --git a/Test/prover/z3mutl.bpl b/Test/prover/z3mutl.bpl index f42f7bb4..84b82ed6 100644 --- a/Test/prover/z3mutl.bpl +++ b/Test/prover/z3mutl.bpl @@ -1,24 +1,24 @@ -// RUN: %boogie -typeEncoding:m -z3multipleErrors "%s" > "%t" -// RUN: %diff "%s.expect" "%t" -var x:int; - -procedure Foo(){ - -start: - - goto L1, L2, L3, L4; -L1: assume x == 1; - goto L5; - -L2: assume x == 2; - goto L5; - -L3: assume x == 3; - goto L5; - -L4: assume x > 10; - goto L5; - -L5: assert (x > 4); - +// RUN: %boogie -typeEncoding:m -z3multipleErrors "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +var x:int; + +procedure Foo(){ + +start: + + goto L1, L2, L3, L4; +L1: assume x == 1; + goto L5; + +L2: assume x == 2; + goto L5; + +L3: assume x == 3; + goto L5; + +L4: assume x > 10; + goto L5; + +L5: assert (x > 4); + } \ No newline at end of file -- cgit v1.2.3