diff --git a/src/test/correct/malloc_memcpy_strlen_memset_free/clang_O2/malloc_memcpy_strlen_memset_free.expected b/src/test/correct/malloc_memcpy_strlen_memset_free/clang_O2/malloc_memcpy_strlen_memset_free.expected new file mode 100644 index 000000000..0bd0a291a --- /dev/null +++ b/src/test/correct/malloc_memcpy_strlen_memset_free/clang_O2/malloc_memcpy_strlen_memset_free.expected @@ -0,0 +1,809 @@ +var {:extern} Gamma_R0: bool; +var {:extern} Gamma_R1: bool; +var {:extern} Gamma_R16: bool; +var {:extern} Gamma_R17: bool; +var {:extern} Gamma_R19: bool; +var {:extern} Gamma_R2: bool; +var {:extern} Gamma_R20: bool; +var {:extern} Gamma_R21: bool; +var {:extern} Gamma_R29: bool; +var {:extern} Gamma_R30: bool; +var {:extern} Gamma_R31: bool; +var {:extern} Gamma_malloc_base: [bv64]bool; +var {:extern} Gamma_malloc_count: [bv64]bool; +var {:extern} Gamma_malloc_end: [bv64]bool; +var {:extern} Gamma_mem: [bv64]bool; +var {:extern} Gamma_stack: [bv64]bool; +var {:extern} R0: bv64; +var {:extern} R1: bv64; +var {:extern} R16: bv64; +var {:extern} R17: bv64; +var {:extern} R19: bv64; +var {:extern} R2: bv64; +var {:extern} R20: bv64; +var {:extern} R21: bv64; +var {:extern} R29: bv64; +var {:extern} R30: bv64; +var {:extern} R31: bv64; +var {:extern} malloc_base: [bv64]bv8; +var {:extern} malloc_count: [bv64]bv8; +var {:extern} malloc_end: [bv64]bv8; +var {:extern} mem: [bv64]bv8; +var {:extern} stack: [bv64]bv8; +const {:extern} $buf_addr: bv64; +axiom ($buf_addr == 131192bv64); +const {:extern} $password_addr: bv64; +axiom ($password_addr == 131168bv64); +const {:extern} $stext_addr: bv64; +axiom ($stext_addr == 131169bv64); +function {:extern} L(memory: [bv64]bv8, index: bv64) returns (bool) { + false +} + +function {:extern} {:bvbuiltin "bvadd"} bvadd64(bv64, bv64) returns (bv64); +function {:extern} {:bvbuiltin "bvsub"} bvsub64(bv64, bv64) returns (bv64); +function {:extern} {:bvbuiltin "bvuge"} bvuge64(bv64, bv64) returns (bool); +function {:extern} {:bvbuiltin "bvugt"} bvugt64(bv64, bv64) returns (bool); +function {:extern} {:bvbuiltin "bvule"} bvule64(bv64, bv64) returns (bool); +function {:extern} {:bvbuiltin "bvult"} bvult64(bv64, bv64) returns (bool); +function {:extern} gamma_load32(gammaMap: [bv64]bool, index: bv64) returns (bool) { + (gammaMap[bvadd64(index, 3bv64)] && (gammaMap[bvadd64(index, 2bv64)] && (gammaMap[bvadd64(index, 1bv64)] && gammaMap[index]))) +} + +function {:extern} gamma_load64(gammaMap: [bv64]bool, index: bv64) returns (bool) { + (gammaMap[bvadd64(index, 7bv64)] && (gammaMap[bvadd64(index, 6bv64)] && (gammaMap[bvadd64(index, 5bv64)] && (gammaMap[bvadd64(index, 4bv64)] && (gammaMap[bvadd64(index, 3bv64)] && (gammaMap[bvadd64(index, 2bv64)] && (gammaMap[bvadd64(index, 1bv64)] && gammaMap[index]))))))) +} + +function {:extern} gamma_load8(gammaMap: [bv64]bool, index: bv64) returns (bool) { + gammaMap[index] +} + +function {:extern} gamma_store64(gammaMap: [bv64]bool, index: bv64, value: bool) returns ([bv64]bool) { + gammaMap[index := value][bvadd64(index, 1bv64) := value][bvadd64(index, 2bv64) := value][bvadd64(index, 3bv64) := value][bvadd64(index, 4bv64) := value][bvadd64(index, 5bv64) := value][bvadd64(index, 6bv64) := value][bvadd64(index, 7bv64) := value] +} + +function {:extern} memory_load64_le(memory: [bv64]bv8, index: bv64) returns (bv64) { + (memory[bvadd64(index, 7bv64)] ++ (memory[bvadd64(index, 6bv64)] ++ (memory[bvadd64(index, 5bv64)] ++ (memory[bvadd64(index, 4bv64)] ++ (memory[bvadd64(index, 3bv64)] ++ (memory[bvadd64(index, 2bv64)] ++ (memory[bvadd64(index, 1bv64)] ++ memory[index]))))))) +} + +function {:extern} memory_load8_le(memory: [bv64]bv8, index: bv64) returns (bv8) { + memory[index] +} + +function {:extern} memory_store64_le(memory: [bv64]bv8, index: bv64, value: bv64) returns ([bv64]bv8) { + memory[index := value[8:0]][bvadd64(index, 1bv64) := value[16:8]][bvadd64(index, 2bv64) := value[24:16]][bvadd64(index, 3bv64) := value[32:24]][bvadd64(index, 4bv64) := value[40:32]][bvadd64(index, 5bv64) := value[48:40]][bvadd64(index, 6bv64) := value[56:48]][bvadd64(index, 7bv64) := value[64:56]] +} + +procedure {:extern} rely(); + modifies Gamma_mem, mem; + ensures (mem == old(mem)); + ensures (Gamma_mem == old(Gamma_mem)); + free ensures (memory_load8_le(mem, 2476bv64) == 1bv8); + free ensures (memory_load8_le(mem, 2477bv64) == 0bv8); + free ensures (memory_load8_le(mem, 2478bv64) == 2bv8); + free ensures (memory_load8_le(mem, 2479bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130488bv64) == 16bv8); + free ensures (memory_load8_le(mem, 130489bv64) == 9bv8); + free ensures (memory_load8_le(mem, 130490bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130491bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130492bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130493bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130494bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130495bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130496bv64) == 192bv8); + free ensures (memory_load8_le(mem, 130497bv64) == 8bv8); + free ensures (memory_load8_le(mem, 130498bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130499bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130500bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130501bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130502bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130503bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131032bv64) == 20bv8); + free ensures (memory_load8_le(mem, 131033bv64) == 9bv8); + free ensures (memory_load8_le(mem, 131034bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131035bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131036bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131037bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131038bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131039bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131160bv64) == 88bv8); + free ensures (memory_load8_le(mem, 131161bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131162bv64) == 2bv8); + free ensures (memory_load8_le(mem, 131163bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131164bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131165bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131166bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131167bv64) == 0bv8); + +procedure {:extern} rely_transitive() + modifies Gamma_mem, mem; + ensures (mem == old(mem)); + ensures (Gamma_mem == old(Gamma_mem)); +{ + call rely(); + call rely(); +} + +procedure {:extern} rely_reflexive(); + +procedure {:extern} guarantee_reflexive(); + modifies Gamma_mem, mem; + +procedure #free(); + modifies Gamma_R16, Gamma_R17, R16, R17; + requires (forall i : int, j: bv64 :: (malloc_base[i] == R0 && bvuge64(j, R0) && bvult64(j, malloc_end[i])) ==> Gamma_mem[j]); + free requires (memory_load8_le(mem, 2476bv64) == 1bv8); + free requires (memory_load8_le(mem, 2477bv64) == 0bv8); + free requires (memory_load8_le(mem, 2478bv64) == 2bv8); + free requires (memory_load8_le(mem, 2479bv64) == 0bv8); + free requires (memory_load8_le(mem, 130488bv64) == 16bv8); + free requires (memory_load8_le(mem, 130489bv64) == 9bv8); + free requires (memory_load8_le(mem, 130490bv64) == 0bv8); + free requires (memory_load8_le(mem, 130491bv64) == 0bv8); + free requires (memory_load8_le(mem, 130492bv64) == 0bv8); + free requires (memory_load8_le(mem, 130493bv64) == 0bv8); + free requires (memory_load8_le(mem, 130494bv64) == 0bv8); + free requires (memory_load8_le(mem, 130495bv64) == 0bv8); + free requires (memory_load8_le(mem, 130496bv64) == 192bv8); + free requires (memory_load8_le(mem, 130497bv64) == 8bv8); + free requires (memory_load8_le(mem, 130498bv64) == 0bv8); + free requires (memory_load8_le(mem, 130499bv64) == 0bv8); + free requires (memory_load8_le(mem, 130500bv64) == 0bv8); + free requires (memory_load8_le(mem, 130501bv64) == 0bv8); + free requires (memory_load8_le(mem, 130502bv64) == 0bv8); + free requires (memory_load8_le(mem, 130503bv64) == 0bv8); + free requires (memory_load8_le(mem, 131032bv64) == 20bv8); + free requires (memory_load8_le(mem, 131033bv64) == 9bv8); + free requires (memory_load8_le(mem, 131034bv64) == 0bv8); + free requires (memory_load8_le(mem, 131035bv64) == 0bv8); + free requires (memory_load8_le(mem, 131036bv64) == 0bv8); + free requires (memory_load8_le(mem, 131037bv64) == 0bv8); + free requires (memory_load8_le(mem, 131038bv64) == 0bv8); + free requires (memory_load8_le(mem, 131039bv64) == 0bv8); + free requires (memory_load8_le(mem, 131160bv64) == 88bv8); + free requires (memory_load8_le(mem, 131161bv64) == 0bv8); + free requires (memory_load8_le(mem, 131162bv64) == 2bv8); + free requires (memory_load8_le(mem, 131163bv64) == 0bv8); + free requires (memory_load8_le(mem, 131164bv64) == 0bv8); + free requires (memory_load8_le(mem, 131165bv64) == 0bv8); + free requires (memory_load8_le(mem, 131166bv64) == 0bv8); + free requires (memory_load8_le(mem, 131167bv64) == 0bv8); + free ensures (memory_load8_le(mem, 2476bv64) == 1bv8); + free ensures (memory_load8_le(mem, 2477bv64) == 0bv8); + free ensures (memory_load8_le(mem, 2478bv64) == 2bv8); + free ensures (memory_load8_le(mem, 2479bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130488bv64) == 16bv8); + free ensures (memory_load8_le(mem, 130489bv64) == 9bv8); + free ensures (memory_load8_le(mem, 130490bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130491bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130492bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130493bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130494bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130495bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130496bv64) == 192bv8); + free ensures (memory_load8_le(mem, 130497bv64) == 8bv8); + free ensures (memory_load8_le(mem, 130498bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130499bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130500bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130501bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130502bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130503bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131032bv64) == 20bv8); + free ensures (memory_load8_le(mem, 131033bv64) == 9bv8); + free ensures (memory_load8_le(mem, 131034bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131035bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131036bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131037bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131038bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131039bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131160bv64) == 88bv8); + free ensures (memory_load8_le(mem, 131161bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131162bv64) == 2bv8); + free ensures (memory_load8_le(mem, 131163bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131164bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131165bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131166bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131167bv64) == 0bv8); + +procedure main() + modifies Gamma_R0, Gamma_R1, Gamma_R16, Gamma_R17, Gamma_R19, Gamma_R2, Gamma_R20, Gamma_R21, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_malloc_base, Gamma_malloc_count, Gamma_malloc_end, Gamma_mem, Gamma_stack, R0, R1, R16, R17, R19, R2, R20, R21, R29, R30, R31, malloc_base, malloc_count, malloc_end, mem, stack; + requires (gamma_load8(Gamma_mem, $password_addr) == false); + requires malloc_count == 0; + requires gamma_load32(Gamma_mem, memory_load64_le(mem, $stext_addr)); + requires R31 == 100bv64; + free requires (memory_load8_le(mem, 131152bv64) == 0bv8); + free requires (memory_load8_le(mem, 131153bv64) == 0bv8); + free requires (memory_load8_le(mem, 131154bv64) == 0bv8); + free requires (memory_load8_le(mem, 131155bv64) == 0bv8); + free requires (memory_load8_le(mem, 131156bv64) == 0bv8); + free requires (memory_load8_le(mem, 131157bv64) == 0bv8); + free requires (memory_load8_le(mem, 131158bv64) == 0bv8); + free requires (memory_load8_le(mem, 131159bv64) == 0bv8); + free requires (memory_load8_le(mem, 131160bv64) == 88bv8); + free requires (memory_load8_le(mem, 131161bv64) == 0bv8); + free requires (memory_load8_le(mem, 131162bv64) == 2bv8); + free requires (memory_load8_le(mem, 131163bv64) == 0bv8); + free requires (memory_load8_le(mem, 131164bv64) == 0bv8); + free requires (memory_load8_le(mem, 131165bv64) == 0bv8); + free requires (memory_load8_le(mem, 131166bv64) == 0bv8); + free requires (memory_load8_le(mem, 131167bv64) == 0bv8); + free requires (memory_load8_le(mem, 131168bv64) == 7bv8); + free requires (memory_load8_le(mem, 131169bv64) == 117bv8); + free requires (memory_load8_le(mem, 131170bv64) == 115bv8); + free requires (memory_load8_le(mem, 131171bv64) == 101bv8); + free requires (memory_load8_le(mem, 131172bv64) == 114bv8); + free requires (memory_load8_le(mem, 131173bv64) == 58bv8); + free requires (memory_load8_le(mem, 131174bv64) == 112bv8); + free requires (memory_load8_le(mem, 131175bv64) == 97bv8); + free requires (memory_load8_le(mem, 131176bv64) == 115bv8); + free requires (memory_load8_le(mem, 131177bv64) == 115bv8); + free requires (memory_load8_le(mem, 131178bv64) == 0bv8); + free requires (memory_load8_le(mem, 131179bv64) == 0bv8); + free requires (memory_load8_le(mem, 2476bv64) == 1bv8); + free requires (memory_load8_le(mem, 2477bv64) == 0bv8); + free requires (memory_load8_le(mem, 2478bv64) == 2bv8); + free requires (memory_load8_le(mem, 2479bv64) == 0bv8); + free requires (memory_load8_le(mem, 130488bv64) == 16bv8); + free requires (memory_load8_le(mem, 130489bv64) == 9bv8); + free requires (memory_load8_le(mem, 130490bv64) == 0bv8); + free requires (memory_load8_le(mem, 130491bv64) == 0bv8); + free requires (memory_load8_le(mem, 130492bv64) == 0bv8); + free requires (memory_load8_le(mem, 130493bv64) == 0bv8); + free requires (memory_load8_le(mem, 130494bv64) == 0bv8); + free requires (memory_load8_le(mem, 130495bv64) == 0bv8); + free requires (memory_load8_le(mem, 130496bv64) == 192bv8); + free requires (memory_load8_le(mem, 130497bv64) == 8bv8); + free requires (memory_load8_le(mem, 130498bv64) == 0bv8); + free requires (memory_load8_le(mem, 130499bv64) == 0bv8); + free requires (memory_load8_le(mem, 130500bv64) == 0bv8); + free requires (memory_load8_le(mem, 130501bv64) == 0bv8); + free requires (memory_load8_le(mem, 130502bv64) == 0bv8); + free requires (memory_load8_le(mem, 130503bv64) == 0bv8); + free requires (memory_load8_le(mem, 131032bv64) == 20bv8); + free requires (memory_load8_le(mem, 131033bv64) == 9bv8); + free requires (memory_load8_le(mem, 131034bv64) == 0bv8); + free requires (memory_load8_le(mem, 131035bv64) == 0bv8); + free requires (memory_load8_le(mem, 131036bv64) == 0bv8); + free requires (memory_load8_le(mem, 131037bv64) == 0bv8); + free requires (memory_load8_le(mem, 131038bv64) == 0bv8); + free requires (memory_load8_le(mem, 131039bv64) == 0bv8); + free requires (memory_load8_le(mem, 131160bv64) == 88bv8); + free requires (memory_load8_le(mem, 131161bv64) == 0bv8); + free requires (memory_load8_le(mem, 131162bv64) == 2bv8); + free requires (memory_load8_le(mem, 131163bv64) == 0bv8); + free requires (memory_load8_le(mem, 131164bv64) == 0bv8); + free requires (memory_load8_le(mem, 131165bv64) == 0bv8); + free requires (memory_load8_le(mem, 131166bv64) == 0bv8); + free requires (memory_load8_le(mem, 131167bv64) == 0bv8); + free ensures (Gamma_R19 == old(Gamma_R19)); + free ensures (Gamma_R20 == old(Gamma_R20)); + free ensures (Gamma_R21 == old(Gamma_R21)); + free ensures (Gamma_R29 == old(Gamma_R29)); + free ensures (Gamma_R31 == old(Gamma_R31)); + free ensures (R19 == old(R19)); + free ensures (R20 == old(R20)); + free ensures (R21 == old(R21)); + free ensures (R29 == old(R29)); + free ensures (R31 == old(R31)); + free ensures (memory_load8_le(mem, 2476bv64) == 1bv8); + free ensures (memory_load8_le(mem, 2477bv64) == 0bv8); + free ensures (memory_load8_le(mem, 2478bv64) == 2bv8); + free ensures (memory_load8_le(mem, 2479bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130488bv64) == 16bv8); + free ensures (memory_load8_le(mem, 130489bv64) == 9bv8); + free ensures (memory_load8_le(mem, 130490bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130491bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130492bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130493bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130494bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130495bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130496bv64) == 192bv8); + free ensures (memory_load8_le(mem, 130497bv64) == 8bv8); + free ensures (memory_load8_le(mem, 130498bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130499bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130500bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130501bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130502bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130503bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131032bv64) == 20bv8); + free ensures (memory_load8_le(mem, 131033bv64) == 9bv8); + free ensures (memory_load8_le(mem, 131034bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131035bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131036bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131037bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131038bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131039bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131160bv64) == 88bv8); + free ensures (memory_load8_le(mem, 131161bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131162bv64) == 2bv8); + free ensures (memory_load8_le(mem, 131163bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131164bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131165bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131166bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131167bv64) == 0bv8); +{ + var #4: bv64; + var #5: bv64; + var #6: bv64; + var Gamma_#4: bool; + var Gamma_#5: bool; + var Gamma_#6: bool; + lmain: + assume {:captureState "lmain"} true; + #4, Gamma_#4 := bvadd64(R31, 18446744073709551568bv64), Gamma_R31; + stack, Gamma_stack := memory_store64_le(stack, #4, R29), gamma_store64(Gamma_stack, #4, Gamma_R29); + assume {:captureState "%00000338"} true; + stack, Gamma_stack := memory_store64_le(stack, bvadd64(#4, 8bv64), R30), gamma_store64(Gamma_stack, bvadd64(#4, 8bv64), Gamma_R30); + assume {:captureState "%0000033e"} true; + R31, Gamma_R31 := #4, Gamma_#4; + stack, Gamma_stack := memory_store64_le(stack, bvadd64(R31, 16bv64), R21), gamma_store64(Gamma_stack, bvadd64(R31, 16bv64), Gamma_R21); + assume {:captureState "%0000034a"} true; + #5, Gamma_#5 := bvadd64(R31, 32bv64), Gamma_R31; + stack, Gamma_stack := memory_store64_le(stack, #5, R20), gamma_store64(Gamma_stack, #5, Gamma_R20); + assume {:captureState "%00000356"} true; + stack, Gamma_stack := memory_store64_le(stack, bvadd64(#5, 8bv64), R19), gamma_store64(Gamma_stack, bvadd64(#5, 8bv64), Gamma_R19); + assume {:captureState "%0000035c"} true; + R29, Gamma_R29 := R31, Gamma_R31; + R0, Gamma_R0 := 11bv64, true; + R30, Gamma_R30 := 2348bv64, true; + call malloc(); + goto l00000371; + l00000371: + assume {:captureState "l00000371"} true; + R21, Gamma_R21 := 131072bv64, true; + R20, Gamma_R20 := 131072bv64, true; + R20, Gamma_R20 := bvadd64(R20, 97bv64), Gamma_R20; + R19, Gamma_R19 := R0, Gamma_R0; + call rely(); + assert (L(mem, bvadd64(R21, 120bv64)) ==> Gamma_R0); + mem, Gamma_mem := memory_store64_le(mem, bvadd64(R21, 120bv64), R0), gamma_store64(Gamma_mem, bvadd64(R21, 120bv64), Gamma_R0); + assume {:captureState "%0000038d"} true; + R0, Gamma_R0 := R20, Gamma_R20; + R30, Gamma_R30 := 2376bv64, true; + call strlen(); + goto l0000039d; + l0000039d: + assume {:captureState "l0000039d"} true; + R2, Gamma_R2 := R0, Gamma_R0; + R0, Gamma_R0 := R19, Gamma_R19; + R1, Gamma_R1 := R20, Gamma_R20; + R30, Gamma_R30 := 2392bv64, true; + call memcpy(); + goto l000003b7; + l000003b7: + assume {:captureState "l000003b7"} true; + R0, Gamma_R0 := R19, Gamma_R19; + R30, Gamma_R30 := 2400bv64, true; + call puts(); + goto l000003c5; + l000003c5: + assume {:captureState "l000003c5"} true; + call rely(); + R19, Gamma_R19 := memory_load64_le(mem, bvadd64(R21, 120bv64)), (gamma_load64(Gamma_mem, bvadd64(R21, 120bv64)) || L(mem, bvadd64(R21, 120bv64))); + R0, Gamma_R0 := R19, Gamma_R19; + R30, Gamma_R30 := 2412bv64, true; + call strlen(); + goto l000003d9; + l000003d9: + assume {:captureState "l000003d9"} true; + R2, Gamma_R2 := R0, Gamma_R0; + R0, Gamma_R0 := R19, Gamma_R19; + R1, Gamma_R1 := 1bv64, true; + R30, Gamma_R30 := 2428bv64, true; + call memset(); + goto l000003f2; + l000003f2: + assume {:captureState "l000003f2"} true; + call rely(); + R0, Gamma_R0 := memory_load64_le(mem, bvadd64(R21, 120bv64)), (gamma_load64(Gamma_mem, bvadd64(R21, 120bv64)) || L(mem, bvadd64(R21, 120bv64))); + R30, Gamma_R30 := 2436bv64, true; + call #free(); + goto l00000401; + l00000401: + assume {:captureState "l00000401"} true; + R0, Gamma_R0 := 0bv64, true; + #6, Gamma_#6 := bvadd64(R31, 32bv64), Gamma_R31; + R20, Gamma_R20 := memory_load64_le(stack, #6), gamma_load64(Gamma_stack, #6); + R19, Gamma_R19 := memory_load64_le(stack, bvadd64(#6, 8bv64)), gamma_load64(Gamma_stack, bvadd64(#6, 8bv64)); + R21, Gamma_R21 := memory_load64_le(stack, bvadd64(R31, 16bv64)), gamma_load64(Gamma_stack, bvadd64(R31, 16bv64)); + R29, Gamma_R29 := memory_load64_le(stack, R31), gamma_load64(Gamma_stack, R31); + R30, Gamma_R30 := memory_load64_le(stack, bvadd64(R31, 8bv64)), gamma_load64(Gamma_stack, bvadd64(R31, 8bv64)); + R31, Gamma_R31 := bvadd64(R31, 48bv64), Gamma_R31; + return; +} + +procedure malloc(); + modifies Gamma_R0, Gamma_R16, Gamma_R17, Gamma_malloc_base, Gamma_malloc_count, Gamma_malloc_end, R0, R16, R17, malloc_base, malloc_count, malloc_end; + requires bvugt64(R0, 0bv64); + requires Gamma_R0 == true; + free requires (memory_load8_le(mem, 2476bv64) == 1bv8); + free requires (memory_load8_le(mem, 2477bv64) == 0bv8); + free requires (memory_load8_le(mem, 2478bv64) == 2bv8); + free requires (memory_load8_le(mem, 2479bv64) == 0bv8); + free requires (memory_load8_le(mem, 130488bv64) == 16bv8); + free requires (memory_load8_le(mem, 130489bv64) == 9bv8); + free requires (memory_load8_le(mem, 130490bv64) == 0bv8); + free requires (memory_load8_le(mem, 130491bv64) == 0bv8); + free requires (memory_load8_le(mem, 130492bv64) == 0bv8); + free requires (memory_load8_le(mem, 130493bv64) == 0bv8); + free requires (memory_load8_le(mem, 130494bv64) == 0bv8); + free requires (memory_load8_le(mem, 130495bv64) == 0bv8); + free requires (memory_load8_le(mem, 130496bv64) == 192bv8); + free requires (memory_load8_le(mem, 130497bv64) == 8bv8); + free requires (memory_load8_le(mem, 130498bv64) == 0bv8); + free requires (memory_load8_le(mem, 130499bv64) == 0bv8); + free requires (memory_load8_le(mem, 130500bv64) == 0bv8); + free requires (memory_load8_le(mem, 130501bv64) == 0bv8); + free requires (memory_load8_le(mem, 130502bv64) == 0bv8); + free requires (memory_load8_le(mem, 130503bv64) == 0bv8); + free requires (memory_load8_le(mem, 131032bv64) == 20bv8); + free requires (memory_load8_le(mem, 131033bv64) == 9bv8); + free requires (memory_load8_le(mem, 131034bv64) == 0bv8); + free requires (memory_load8_le(mem, 131035bv64) == 0bv8); + free requires (memory_load8_le(mem, 131036bv64) == 0bv8); + free requires (memory_load8_le(mem, 131037bv64) == 0bv8); + free requires (memory_load8_le(mem, 131038bv64) == 0bv8); + free requires (memory_load8_le(mem, 131039bv64) == 0bv8); + free requires (memory_load8_le(mem, 131160bv64) == 88bv8); + free requires (memory_load8_le(mem, 131161bv64) == 0bv8); + free requires (memory_load8_le(mem, 131162bv64) == 2bv8); + free requires (memory_load8_le(mem, 131163bv64) == 0bv8); + free requires (memory_load8_le(mem, 131164bv64) == 0bv8); + free requires (memory_load8_le(mem, 131165bv64) == 0bv8); + free requires (memory_load8_le(mem, 131166bv64) == 0bv8); + free requires (memory_load8_le(mem, 131167bv64) == 0bv8); + ensures Gamma_R0 == true; + ensures malloc_count == old(malloc_count) + 1; + ensures bvugt64(malloc_end[malloc_count], malloc_base[malloc_count]); + ensures R0 == malloc_base[malloc_count]; + ensures malloc_end[malloc_count] == bvadd64(R0, old(R0)); + ensures (forall i: int :: i != malloc_count ==> bvugt64(malloc_base[malloc_count], malloc_end[i]) || bvult64(malloc_end[malloc_count], malloc_base[i])); + ensures (forall i: int :: i != malloc_count ==> malloc_base[i] == old(malloc_base[i]) && malloc_end[i] == old(malloc_end[i])); + ensures bvuge64(R0, 100000000bv64); + ensures (forall i : bv64 :: (bvuge64(i, R0) && bvult64(i, bvadd64(R0, old(R0)))) ==> (Gamma_mem[i] && gamma_load8(Gamma_mem, i))); + free ensures (memory_load8_le(mem, 2476bv64) == 1bv8); + free ensures (memory_load8_le(mem, 2477bv64) == 0bv8); + free ensures (memory_load8_le(mem, 2478bv64) == 2bv8); + free ensures (memory_load8_le(mem, 2479bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130488bv64) == 16bv8); + free ensures (memory_load8_le(mem, 130489bv64) == 9bv8); + free ensures (memory_load8_le(mem, 130490bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130491bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130492bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130493bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130494bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130495bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130496bv64) == 192bv8); + free ensures (memory_load8_le(mem, 130497bv64) == 8bv8); + free ensures (memory_load8_le(mem, 130498bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130499bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130500bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130501bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130502bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130503bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131032bv64) == 20bv8); + free ensures (memory_load8_le(mem, 131033bv64) == 9bv8); + free ensures (memory_load8_le(mem, 131034bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131035bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131036bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131037bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131038bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131039bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131160bv64) == 88bv8); + free ensures (memory_load8_le(mem, 131161bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131162bv64) == 2bv8); + free ensures (memory_load8_le(mem, 131163bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131164bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131165bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131166bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131167bv64) == 0bv8); + +procedure memcpy(); + modifies Gamma_R16, Gamma_R17, Gamma_mem, R16, R17, mem; + free requires (memory_load8_le(mem, 2476bv64) == 1bv8); + free requires (memory_load8_le(mem, 2477bv64) == 0bv8); + free requires (memory_load8_le(mem, 2478bv64) == 2bv8); + free requires (memory_load8_le(mem, 2479bv64) == 0bv8); + free requires (memory_load8_le(mem, 130488bv64) == 16bv8); + free requires (memory_load8_le(mem, 130489bv64) == 9bv8); + free requires (memory_load8_le(mem, 130490bv64) == 0bv8); + free requires (memory_load8_le(mem, 130491bv64) == 0bv8); + free requires (memory_load8_le(mem, 130492bv64) == 0bv8); + free requires (memory_load8_le(mem, 130493bv64) == 0bv8); + free requires (memory_load8_le(mem, 130494bv64) == 0bv8); + free requires (memory_load8_le(mem, 130495bv64) == 0bv8); + free requires (memory_load8_le(mem, 130496bv64) == 192bv8); + free requires (memory_load8_le(mem, 130497bv64) == 8bv8); + free requires (memory_load8_le(mem, 130498bv64) == 0bv8); + free requires (memory_load8_le(mem, 130499bv64) == 0bv8); + free requires (memory_load8_le(mem, 130500bv64) == 0bv8); + free requires (memory_load8_le(mem, 130501bv64) == 0bv8); + free requires (memory_load8_le(mem, 130502bv64) == 0bv8); + free requires (memory_load8_le(mem, 130503bv64) == 0bv8); + free requires (memory_load8_le(mem, 131032bv64) == 20bv8); + free requires (memory_load8_le(mem, 131033bv64) == 9bv8); + free requires (memory_load8_le(mem, 131034bv64) == 0bv8); + free requires (memory_load8_le(mem, 131035bv64) == 0bv8); + free requires (memory_load8_le(mem, 131036bv64) == 0bv8); + free requires (memory_load8_le(mem, 131037bv64) == 0bv8); + free requires (memory_load8_le(mem, 131038bv64) == 0bv8); + free requires (memory_load8_le(mem, 131039bv64) == 0bv8); + free requires (memory_load8_le(mem, 131160bv64) == 88bv8); + free requires (memory_load8_le(mem, 131161bv64) == 0bv8); + free requires (memory_load8_le(mem, 131162bv64) == 2bv8); + free requires (memory_load8_le(mem, 131163bv64) == 0bv8); + free requires (memory_load8_le(mem, 131164bv64) == 0bv8); + free requires (memory_load8_le(mem, 131165bv64) == 0bv8); + free requires (memory_load8_le(mem, 131166bv64) == 0bv8); + free requires (memory_load8_le(mem, 131167bv64) == 0bv8); + ensures (forall i: bv64 :: (Gamma_mem[i] == if (bvule64(R0, i) && bvult64(i, bvadd64(R0, R2))) then gamma_load8((Gamma_mem), bvadd64(bvsub64(i, R0), R1)) else old(gamma_load8(Gamma_mem, i)))); + ensures (forall i: bv64 :: (mem[i] == if (bvule64(R0, i) && bvult64(i,bvadd64(R0, R2))) then memory_load8_le((mem), bvadd64(bvsub64(i, R0), R1)) else old(memory_load8_le(mem, i)))); + free ensures (memory_load8_le(mem, 2476bv64) == 1bv8); + free ensures (memory_load8_le(mem, 2477bv64) == 0bv8); + free ensures (memory_load8_le(mem, 2478bv64) == 2bv8); + free ensures (memory_load8_le(mem, 2479bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130488bv64) == 16bv8); + free ensures (memory_load8_le(mem, 130489bv64) == 9bv8); + free ensures (memory_load8_le(mem, 130490bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130491bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130492bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130493bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130494bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130495bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130496bv64) == 192bv8); + free ensures (memory_load8_le(mem, 130497bv64) == 8bv8); + free ensures (memory_load8_le(mem, 130498bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130499bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130500bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130501bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130502bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130503bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131032bv64) == 20bv8); + free ensures (memory_load8_le(mem, 131033bv64) == 9bv8); + free ensures (memory_load8_le(mem, 131034bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131035bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131036bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131037bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131038bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131039bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131160bv64) == 88bv8); + free ensures (memory_load8_le(mem, 131161bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131162bv64) == 2bv8); + free ensures (memory_load8_le(mem, 131163bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131164bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131165bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131166bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131167bv64) == 0bv8); + +procedure memset(); + modifies Gamma_R16, Gamma_R17, Gamma_mem, R16, R17, mem; + requires Gamma_R1; + free requires (memory_load8_le(mem, 2476bv64) == 1bv8); + free requires (memory_load8_le(mem, 2477bv64) == 0bv8); + free requires (memory_load8_le(mem, 2478bv64) == 2bv8); + free requires (memory_load8_le(mem, 2479bv64) == 0bv8); + free requires (memory_load8_le(mem, 130488bv64) == 16bv8); + free requires (memory_load8_le(mem, 130489bv64) == 9bv8); + free requires (memory_load8_le(mem, 130490bv64) == 0bv8); + free requires (memory_load8_le(mem, 130491bv64) == 0bv8); + free requires (memory_load8_le(mem, 130492bv64) == 0bv8); + free requires (memory_load8_le(mem, 130493bv64) == 0bv8); + free requires (memory_load8_le(mem, 130494bv64) == 0bv8); + free requires (memory_load8_le(mem, 130495bv64) == 0bv8); + free requires (memory_load8_le(mem, 130496bv64) == 192bv8); + free requires (memory_load8_le(mem, 130497bv64) == 8bv8); + free requires (memory_load8_le(mem, 130498bv64) == 0bv8); + free requires (memory_load8_le(mem, 130499bv64) == 0bv8); + free requires (memory_load8_le(mem, 130500bv64) == 0bv8); + free requires (memory_load8_le(mem, 130501bv64) == 0bv8); + free requires (memory_load8_le(mem, 130502bv64) == 0bv8); + free requires (memory_load8_le(mem, 130503bv64) == 0bv8); + free requires (memory_load8_le(mem, 131032bv64) == 20bv8); + free requires (memory_load8_le(mem, 131033bv64) == 9bv8); + free requires (memory_load8_le(mem, 131034bv64) == 0bv8); + free requires (memory_load8_le(mem, 131035bv64) == 0bv8); + free requires (memory_load8_le(mem, 131036bv64) == 0bv8); + free requires (memory_load8_le(mem, 131037bv64) == 0bv8); + free requires (memory_load8_le(mem, 131038bv64) == 0bv8); + free requires (memory_load8_le(mem, 131039bv64) == 0bv8); + free requires (memory_load8_le(mem, 131160bv64) == 88bv8); + free requires (memory_load8_le(mem, 131161bv64) == 0bv8); + free requires (memory_load8_le(mem, 131162bv64) == 2bv8); + free requires (memory_load8_le(mem, 131163bv64) == 0bv8); + free requires (memory_load8_le(mem, 131164bv64) == 0bv8); + free requires (memory_load8_le(mem, 131165bv64) == 0bv8); + free requires (memory_load8_le(mem, 131166bv64) == 0bv8); + free requires (memory_load8_le(mem, 131167bv64) == 0bv8); + ensures ((memory_load64_le(mem, $buf_addr) == old(memory_load64_le(mem, $buf_addr))) && (memory_load8_le(mem, $password_addr) == old(memory_load8_le(mem, $password_addr)))); + ensures (forall i: bv64 :: (Gamma_mem[i] == if (bvule64(R0, i) && bvult64(i,bvadd64(R0, R2))) then Gamma_R1 else old(gamma_load8(Gamma_mem, i)))); + ensures (forall i: bv64 :: (mem[i] == if (bvule64(R0, i) && bvult64(i,bvadd64(R0, R2))) then R1[8:0] else old(memory_load8_le(mem, i)))); + free ensures (memory_load8_le(mem, 2476bv64) == 1bv8); + free ensures (memory_load8_le(mem, 2477bv64) == 0bv8); + free ensures (memory_load8_le(mem, 2478bv64) == 2bv8); + free ensures (memory_load8_le(mem, 2479bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130488bv64) == 16bv8); + free ensures (memory_load8_le(mem, 130489bv64) == 9bv8); + free ensures (memory_load8_le(mem, 130490bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130491bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130492bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130493bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130494bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130495bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130496bv64) == 192bv8); + free ensures (memory_load8_le(mem, 130497bv64) == 8bv8); + free ensures (memory_load8_le(mem, 130498bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130499bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130500bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130501bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130502bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130503bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131032bv64) == 20bv8); + free ensures (memory_load8_le(mem, 131033bv64) == 9bv8); + free ensures (memory_load8_le(mem, 131034bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131035bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131036bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131037bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131038bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131039bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131160bv64) == 88bv8); + free ensures (memory_load8_le(mem, 131161bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131162bv64) == 2bv8); + free ensures (memory_load8_le(mem, 131163bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131164bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131165bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131166bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131167bv64) == 0bv8); + +procedure puts(); + modifies Gamma_R16, Gamma_R17, R16, R17; + free requires (memory_load8_le(mem, 2476bv64) == 1bv8); + free requires (memory_load8_le(mem, 2477bv64) == 0bv8); + free requires (memory_load8_le(mem, 2478bv64) == 2bv8); + free requires (memory_load8_le(mem, 2479bv64) == 0bv8); + free requires (memory_load8_le(mem, 130488bv64) == 16bv8); + free requires (memory_load8_le(mem, 130489bv64) == 9bv8); + free requires (memory_load8_le(mem, 130490bv64) == 0bv8); + free requires (memory_load8_le(mem, 130491bv64) == 0bv8); + free requires (memory_load8_le(mem, 130492bv64) == 0bv8); + free requires (memory_load8_le(mem, 130493bv64) == 0bv8); + free requires (memory_load8_le(mem, 130494bv64) == 0bv8); + free requires (memory_load8_le(mem, 130495bv64) == 0bv8); + free requires (memory_load8_le(mem, 130496bv64) == 192bv8); + free requires (memory_load8_le(mem, 130497bv64) == 8bv8); + free requires (memory_load8_le(mem, 130498bv64) == 0bv8); + free requires (memory_load8_le(mem, 130499bv64) == 0bv8); + free requires (memory_load8_le(mem, 130500bv64) == 0bv8); + free requires (memory_load8_le(mem, 130501bv64) == 0bv8); + free requires (memory_load8_le(mem, 130502bv64) == 0bv8); + free requires (memory_load8_le(mem, 130503bv64) == 0bv8); + free requires (memory_load8_le(mem, 131032bv64) == 20bv8); + free requires (memory_load8_le(mem, 131033bv64) == 9bv8); + free requires (memory_load8_le(mem, 131034bv64) == 0bv8); + free requires (memory_load8_le(mem, 131035bv64) == 0bv8); + free requires (memory_load8_le(mem, 131036bv64) == 0bv8); + free requires (memory_load8_le(mem, 131037bv64) == 0bv8); + free requires (memory_load8_le(mem, 131038bv64) == 0bv8); + free requires (memory_load8_le(mem, 131039bv64) == 0bv8); + free requires (memory_load8_le(mem, 131160bv64) == 88bv8); + free requires (memory_load8_le(mem, 131161bv64) == 0bv8); + free requires (memory_load8_le(mem, 131162bv64) == 2bv8); + free requires (memory_load8_le(mem, 131163bv64) == 0bv8); + free requires (memory_load8_le(mem, 131164bv64) == 0bv8); + free requires (memory_load8_le(mem, 131165bv64) == 0bv8); + free requires (memory_load8_le(mem, 131166bv64) == 0bv8); + free requires (memory_load8_le(mem, 131167bv64) == 0bv8); + free ensures (memory_load8_le(mem, 2476bv64) == 1bv8); + free ensures (memory_load8_le(mem, 2477bv64) == 0bv8); + free ensures (memory_load8_le(mem, 2478bv64) == 2bv8); + free ensures (memory_load8_le(mem, 2479bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130488bv64) == 16bv8); + free ensures (memory_load8_le(mem, 130489bv64) == 9bv8); + free ensures (memory_load8_le(mem, 130490bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130491bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130492bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130493bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130494bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130495bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130496bv64) == 192bv8); + free ensures (memory_load8_le(mem, 130497bv64) == 8bv8); + free ensures (memory_load8_le(mem, 130498bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130499bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130500bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130501bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130502bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130503bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131032bv64) == 20bv8); + free ensures (memory_load8_le(mem, 131033bv64) == 9bv8); + free ensures (memory_load8_le(mem, 131034bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131035bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131036bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131037bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131038bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131039bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131160bv64) == 88bv8); + free ensures (memory_load8_le(mem, 131161bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131162bv64) == 2bv8); + free ensures (memory_load8_le(mem, 131163bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131164bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131165bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131166bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131167bv64) == 0bv8); + +procedure strlen(); + modifies Gamma_R0, Gamma_R16, Gamma_R17, R0, R16, R17; + free requires (memory_load8_le(mem, 2476bv64) == 1bv8); + free requires (memory_load8_le(mem, 2477bv64) == 0bv8); + free requires (memory_load8_le(mem, 2478bv64) == 2bv8); + free requires (memory_load8_le(mem, 2479bv64) == 0bv8); + free requires (memory_load8_le(mem, 130488bv64) == 16bv8); + free requires (memory_load8_le(mem, 130489bv64) == 9bv8); + free requires (memory_load8_le(mem, 130490bv64) == 0bv8); + free requires (memory_load8_le(mem, 130491bv64) == 0bv8); + free requires (memory_load8_le(mem, 130492bv64) == 0bv8); + free requires (memory_load8_le(mem, 130493bv64) == 0bv8); + free requires (memory_load8_le(mem, 130494bv64) == 0bv8); + free requires (memory_load8_le(mem, 130495bv64) == 0bv8); + free requires (memory_load8_le(mem, 130496bv64) == 192bv8); + free requires (memory_load8_le(mem, 130497bv64) == 8bv8); + free requires (memory_load8_le(mem, 130498bv64) == 0bv8); + free requires (memory_load8_le(mem, 130499bv64) == 0bv8); + free requires (memory_load8_le(mem, 130500bv64) == 0bv8); + free requires (memory_load8_le(mem, 130501bv64) == 0bv8); + free requires (memory_load8_le(mem, 130502bv64) == 0bv8); + free requires (memory_load8_le(mem, 130503bv64) == 0bv8); + free requires (memory_load8_le(mem, 131032bv64) == 20bv8); + free requires (memory_load8_le(mem, 131033bv64) == 9bv8); + free requires (memory_load8_le(mem, 131034bv64) == 0bv8); + free requires (memory_load8_le(mem, 131035bv64) == 0bv8); + free requires (memory_load8_le(mem, 131036bv64) == 0bv8); + free requires (memory_load8_le(mem, 131037bv64) == 0bv8); + free requires (memory_load8_le(mem, 131038bv64) == 0bv8); + free requires (memory_load8_le(mem, 131039bv64) == 0bv8); + free requires (memory_load8_le(mem, 131160bv64) == 88bv8); + free requires (memory_load8_le(mem, 131161bv64) == 0bv8); + free requires (memory_load8_le(mem, 131162bv64) == 2bv8); + free requires (memory_load8_le(mem, 131163bv64) == 0bv8); + free requires (memory_load8_le(mem, 131164bv64) == 0bv8); + free requires (memory_load8_le(mem, 131165bv64) == 0bv8); + free requires (memory_load8_le(mem, 131166bv64) == 0bv8); + free requires (memory_load8_le(mem, 131167bv64) == 0bv8); + ensures Gamma_R0 == true; + ensures (forall i: bv64 :: (bvule64(old(R0), i)) && (bvult64(i, bvadd64(old(R0), R0))) ==> mem[i] != 0bv8); + ensures (memory_load8_le(mem, bvadd64(old(R0), R0)) == 0bv8); + ensures (bvult64(old(R0), bvadd64(bvadd64(old(R0), R0), 1bv64))); + free ensures (memory_load8_le(mem, 2476bv64) == 1bv8); + free ensures (memory_load8_le(mem, 2477bv64) == 0bv8); + free ensures (memory_load8_le(mem, 2478bv64) == 2bv8); + free ensures (memory_load8_le(mem, 2479bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130488bv64) == 16bv8); + free ensures (memory_load8_le(mem, 130489bv64) == 9bv8); + free ensures (memory_load8_le(mem, 130490bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130491bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130492bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130493bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130494bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130495bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130496bv64) == 192bv8); + free ensures (memory_load8_le(mem, 130497bv64) == 8bv8); + free ensures (memory_load8_le(mem, 130498bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130499bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130500bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130501bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130502bv64) == 0bv8); + free ensures (memory_load8_le(mem, 130503bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131032bv64) == 20bv8); + free ensures (memory_load8_le(mem, 131033bv64) == 9bv8); + free ensures (memory_load8_le(mem, 131034bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131035bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131036bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131037bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131038bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131039bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131160bv64) == 88bv8); + free ensures (memory_load8_le(mem, 131161bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131162bv64) == 2bv8); + free ensures (memory_load8_le(mem, 131163bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131164bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131165bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131166bv64) == 0bv8); + free ensures (memory_load8_le(mem, 131167bv64) == 0bv8); diff --git a/src/test/correct/malloc_memcpy_strlen_memset_free/gcc_O2/malloc_memcpy_strlen_memset_free.expected b/src/test/correct/malloc_memcpy_strlen_memset_free/gcc_O2/malloc_memcpy_strlen_memset_free.expected index a1729ce76..e24a49e85 100644 --- a/src/test/correct/malloc_memcpy_strlen_memset_free/gcc_O2/malloc_memcpy_strlen_memset_free.expected +++ b/src/test/correct/malloc_memcpy_strlen_memset_free/gcc_O2/malloc_memcpy_strlen_memset_free.expected @@ -322,33 +322,35 @@ procedure main() free ensures (memory_load8_le(mem, 131166bv64) == 0bv8); free ensures (memory_load8_le(mem, 131167bv64) == 0bv8); { - var #14: bv64; - var #9: bv64; - var Gamma_#14: bool; - var Gamma_#9: bool; + var #1: bv64; + var #2: bv64; + var #3: bv64; + var Gamma_#1: bool; + var Gamma_#2: bool; + var Gamma_#3: bool; lmain: assume {:captureState "lmain"} true; - #9, Gamma_#9 := bvadd64(R31, 18446744073709551568bv64), Gamma_R31; - stack, Gamma_stack := memory_store64_le(stack, #9, R29), gamma_store64(Gamma_stack, #9, Gamma_R29); - assume {:captureState "%00000238"} true; - stack, Gamma_stack := memory_store64_le(stack, bvadd64(#9, 8bv64), R30), gamma_store64(Gamma_stack, bvadd64(#9, 8bv64), Gamma_R30); - assume {:captureState "%0000023d"} true; - R31, Gamma_R31 := #9, Gamma_#9; + #1, Gamma_#1 := bvadd64(R31, 18446744073709551568bv64), Gamma_R31; + stack, Gamma_stack := memory_store64_le(stack, #1, R29), gamma_store64(Gamma_stack, #1, Gamma_R29); + assume {:captureState "%00000233"} true; + stack, Gamma_stack := memory_store64_le(stack, bvadd64(#1, 8bv64), R30), gamma_store64(Gamma_stack, bvadd64(#1, 8bv64), Gamma_R30); + assume {:captureState "%00000239"} true; + R31, Gamma_R31 := #1, Gamma_#1; R0, Gamma_R0 := 11bv64, true; R29, Gamma_R29 := R31, Gamma_R31; stack, Gamma_stack := memory_store64_le(stack, bvadd64(R31, 32bv64), R21), gamma_store64(Gamma_stack, bvadd64(R31, 32bv64), Gamma_R21); - assume {:captureState "%00000256"} true; + assume {:captureState "%00000250"} true; R21, Gamma_R21 := 131072bv64, true; - #14, Gamma_#14 := bvadd64(R31, 16bv64), Gamma_R31; - stack, Gamma_stack := memory_store64_le(stack, #14, R19), gamma_store64(Gamma_stack, #14, Gamma_R19); - assume {:captureState "%00000269"} true; - stack, Gamma_stack := memory_store64_le(stack, bvadd64(#14, 8bv64), R20), gamma_store64(Gamma_stack, bvadd64(#14, 8bv64), Gamma_R20); - assume {:captureState "%0000026e"} true; + #2, Gamma_#2 := bvadd64(R31, 16bv64), Gamma_R31; + stack, Gamma_stack := memory_store64_le(stack, #2, R19), gamma_store64(Gamma_stack, #2, Gamma_R19); + assume {:captureState "%00000261"} true; + stack, Gamma_stack := memory_store64_le(stack, bvadd64(#2, 8bv64), R20), gamma_store64(Gamma_stack, bvadd64(#2, 8bv64), Gamma_R20); + assume {:captureState "%00000267"} true; R30, Gamma_R30 := 2012bv64, true; call malloc(); - goto l00000278; - l00000278: - assume {:captureState "l00000278"} true; + goto l00000271; + l00000271: + assume {:captureState "l00000271"} true; R20, Gamma_R20 := 131072bv64, true; R20, Gamma_R20 := bvadd64(R20, 96bv64), Gamma_R20; R19, Gamma_R19 := R0, Gamma_R0; @@ -356,51 +358,52 @@ procedure main() call rely(); assert (L(mem, bvadd64(R21, 120bv64)) ==> Gamma_R19); mem, Gamma_mem := memory_store64_le(mem, bvadd64(R21, 120bv64), R19), gamma_store64(Gamma_mem, bvadd64(R21, 120bv64), Gamma_R19); - assume {:captureState "%0000029b"} true; + assume {:captureState "%0000028e"} true; R30, Gamma_R30 := 2036bv64, true; call strlen(); - goto l000002a5; - l000002a5: - assume {:captureState "l000002a5"} true; + goto l00000298; + l00000298: + assume {:captureState "l00000298"} true; R2, Gamma_R2 := R0, Gamma_R0; R1, Gamma_R1 := R20, Gamma_R20; R0, Gamma_R0 := R19, Gamma_R19; R30, Gamma_R30 := 2052bv64, true; call memcpy(); - goto l000002c5; - l000002c5: - assume {:captureState "l000002c5"} true; + goto l000002b2; + l000002b2: + assume {:captureState "l000002b2"} true; R0, Gamma_R0 := R19, Gamma_R19; R30, Gamma_R30 := 2060bv64, true; call puts(); - goto l000002d5; - l000002d5: - assume {:captureState "l000002d5"} true; + goto l000002c0; + l000002c0: + assume {:captureState "l000002c0"} true; call rely(); R19, Gamma_R19 := memory_load64_le(mem, bvadd64(R21, 120bv64)), (gamma_load64(Gamma_mem, bvadd64(R21, 120bv64)) || L(mem, bvadd64(R21, 120bv64))); R0, Gamma_R0 := R19, Gamma_R19; R30, Gamma_R30 := 2072bv64, true; call strlen(); - goto l000002ec; - l000002ec: - assume {:captureState "l000002ec"} true; + goto l000002d4; + l000002d4: + assume {:captureState "l000002d4"} true; R1, Gamma_R1 := 1bv64, true; R2, Gamma_R2 := R0, Gamma_R0; R0, Gamma_R0 := R19, Gamma_R19; R30, Gamma_R30 := 2088bv64, true; call memset(); - goto l0000030b; - l0000030b: - assume {:captureState "l0000030b"} true; + goto l000002ed; + l000002ed: + assume {:captureState "l000002ed"} true; call rely(); R0, Gamma_R0 := memory_load64_le(mem, bvadd64(R21, 120bv64)), (gamma_load64(Gamma_mem, bvadd64(R21, 120bv64)) || L(mem, bvadd64(R21, 120bv64))); R30, Gamma_R30 := 2096bv64, true; call #free(); - goto l0000031b; - l0000031b: - assume {:captureState "l0000031b"} true; - R19, Gamma_R19 := memory_load64_le(stack, bvadd64(R31, 16bv64)), gamma_load64(Gamma_stack, bvadd64(R31, 16bv64)); - R20, Gamma_R20 := memory_load64_le(stack, bvadd64(R31, 24bv64)), gamma_load64(Gamma_stack, bvadd64(R31, 24bv64)); + goto l000002fc; + l000002fc: + assume {:captureState "l000002fc"} true; + #3, Gamma_#3 := bvadd64(R31, 16bv64), Gamma_R31; + R19, Gamma_R19 := memory_load64_le(stack, #3), gamma_load64(Gamma_stack, #3); + R20, Gamma_R20 := memory_load64_le(stack, bvadd64(#3, 8bv64)), gamma_load64(Gamma_stack, bvadd64(#3, 8bv64)); R0, Gamma_R0 := 0bv64, true; R21, Gamma_R21 := memory_load64_le(stack, bvadd64(R31, 32bv64)), gamma_load64(Gamma_stack, bvadd64(R31, 32bv64)); R29, Gamma_R29 := memory_load64_le(stack, R31), gamma_load64(Gamma_stack, R31); diff --git a/src/test/incorrect/malloc_memcpy_strlen_memset_free/clang_O2/malloc_memcpy_strlen_memset_free.expected b/src/test/incorrect/malloc_memcpy_strlen_memset_free/clang_O2/malloc_memcpy_strlen_memset_free.expected index 332b58eaf..8296ed8eb 100644 --- a/src/test/incorrect/malloc_memcpy_strlen_memset_free/clang_O2/malloc_memcpy_strlen_memset_free.expected +++ b/src/test/incorrect/malloc_memcpy_strlen_memset_free/clang_O2/malloc_memcpy_strlen_memset_free.expected @@ -80,7 +80,7 @@ function {:extern} memory_store64_le(memory: [bv64]bv8, index: bv64, value: bv64 memory[index := value[8:0]][bvadd64(index, 1bv64) := value[16:8]][bvadd64(index, 2bv64) := value[24:16]][bvadd64(index, 3bv64) := value[32:24]][bvadd64(index, 4bv64) := value[40:32]][bvadd64(index, 5bv64) := value[48:40]][bvadd64(index, 6bv64) := value[56:48]][bvadd64(index, 7bv64) := value[64:56]] } -function {:extern} memory_store8_be(memory: [bv64]bv8, index: bv64, value: bv8) returns ([bv64]bv8) { +function {:extern} memory_store8_le(memory: [bv64]bv8, index: bv64, value: bv8) returns ([bv64]bv8) { memory[index := value[8:0]] } @@ -332,32 +332,34 @@ procedure main() free ensures (memory_load8_le(mem, 131166bv64) == 0bv8); free ensures (memory_load8_le(mem, 131167bv64) == 0bv8); { - var #42: bv64; - var #47: bv64; - var Gamma_#42: bool; - var Gamma_#47: bool; + var #4: bv64; + var #5: bv64; + var #6: bv64; + var Gamma_#4: bool; + var Gamma_#5: bool; + var Gamma_#6: bool; lmain: assume {:captureState "lmain"} true; - #42, Gamma_#42 := bvadd64(R31, 18446744073709551568bv64), Gamma_R31; - stack, Gamma_stack := memory_store64_le(stack, #42, R29), gamma_store64(Gamma_stack, #42, Gamma_R29); - assume {:captureState "%00000371"} true; - stack, Gamma_stack := memory_store64_le(stack, bvadd64(#42, 8bv64), R30), gamma_store64(Gamma_stack, bvadd64(#42, 8bv64), Gamma_R30); - assume {:captureState "%00000376"} true; - R31, Gamma_R31 := #42, Gamma_#42; + #4, Gamma_#4 := bvadd64(R31, 18446744073709551568bv64), Gamma_R31; + stack, Gamma_stack := memory_store64_le(stack, #4, R29), gamma_store64(Gamma_stack, #4, Gamma_R29); + assume {:captureState "%00000340"} true; + stack, Gamma_stack := memory_store64_le(stack, bvadd64(#4, 8bv64), R30), gamma_store64(Gamma_stack, bvadd64(#4, 8bv64), Gamma_R30); + assume {:captureState "%00000346"} true; + R31, Gamma_R31 := #4, Gamma_#4; stack, Gamma_stack := memory_store64_le(stack, bvadd64(R31, 16bv64), R21), gamma_store64(Gamma_stack, bvadd64(R31, 16bv64), Gamma_R21); - assume {:captureState "%00000382"} true; - #47, Gamma_#47 := bvadd64(R31, 32bv64), Gamma_R31; - stack, Gamma_stack := memory_store64_le(stack, #47, R20), gamma_store64(Gamma_stack, #47, Gamma_R20); - assume {:captureState "%0000038f"} true; - stack, Gamma_stack := memory_store64_le(stack, bvadd64(#47, 8bv64), R19), gamma_store64(Gamma_stack, bvadd64(#47, 8bv64), Gamma_R19); - assume {:captureState "%00000394"} true; + assume {:captureState "%00000352"} true; + #5, Gamma_#5 := bvadd64(R31, 32bv64), Gamma_R31; + stack, Gamma_stack := memory_store64_le(stack, #5, R20), gamma_store64(Gamma_stack, #5, Gamma_R20); + assume {:captureState "%0000035e"} true; + stack, Gamma_stack := memory_store64_le(stack, bvadd64(#5, 8bv64), R19), gamma_store64(Gamma_stack, bvadd64(#5, 8bv64), Gamma_R19); + assume {:captureState "%00000364"} true; R29, Gamma_R29 := R31, Gamma_R31; R0, Gamma_R0 := 11bv64, true; R30, Gamma_R30 := 2348bv64, true; call malloc(); - goto l000003ac; - l000003ac: - assume {:captureState "l000003ac"} true; + goto l00000379; + l00000379: + assume {:captureState "l00000379"} true; R21, Gamma_R21 := 131072bv64, true; R20, Gamma_R20 := 131072bv64, true; R20, Gamma_R20 := bvadd64(R20, 97bv64), Gamma_R20; @@ -365,59 +367,60 @@ procedure main() call rely(); assert (L(mem, bvadd64(R21, 120bv64)) ==> Gamma_R0); mem, Gamma_mem := memory_store64_le(mem, bvadd64(R21, 120bv64), R0), gamma_store64(Gamma_mem, bvadd64(R21, 120bv64), Gamma_R0); - assume {:captureState "%000003cd"} true; + assume {:captureState "%00000395"} true; R0, Gamma_R0 := R20, Gamma_R20; R30, Gamma_R30 := 2376bv64, true; call strlen(); - goto l000003df; - l000003df: - assume {:captureState "l000003df"} true; + goto l000003a5; + l000003a5: + assume {:captureState "l000003a5"} true; R2, Gamma_R2 := R0, Gamma_R0; R0, Gamma_R0 := R19, Gamma_R19; R1, Gamma_R1 := R20, Gamma_R20; R30, Gamma_R30 := 2392bv64, true; call memcpy(); - goto l000003ff; - l000003ff: - assume {:captureState "l000003ff"} true; + goto l000003bf; + l000003bf: + assume {:captureState "l000003bf"} true; R0, Gamma_R0 := R19, Gamma_R19; R30, Gamma_R30 := 2400bv64, true; call puts(); - goto l0000040f; - l0000040f: - assume {:captureState "l0000040f"} true; + goto l000003cd; + l000003cd: + assume {:captureState "l000003cd"} true; call rely(); R8, Gamma_R8 := memory_load64_le(mem, bvadd64(R21, 120bv64)), (gamma_load64(Gamma_mem, bvadd64(R21, 120bv64)) || L(mem, bvadd64(R21, 120bv64))); call rely(); assert (L(mem, bvadd64(R8, 4bv64)) ==> true); - mem, Gamma_mem := memory_store8_be(mem, bvadd64(R8, 4bv64), 0bv8), gamma_store8(Gamma_mem, bvadd64(R8, 4bv64), true); - assume {:captureState "%0000041d"} true; + mem, Gamma_mem := memory_store8_le(mem, bvadd64(R8, 4bv64), 0bv8), gamma_store8(Gamma_mem, bvadd64(R8, 4bv64), true); + assume {:captureState "%000003d9"} true; call rely(); R19, Gamma_R19 := memory_load64_le(mem, bvadd64(R21, 120bv64)), (gamma_load64(Gamma_mem, bvadd64(R21, 120bv64)) || L(mem, bvadd64(R21, 120bv64))); R0, Gamma_R0 := R19, Gamma_R19; R30, Gamma_R30 := 2420bv64, true; call strlen(); - goto l00000436; - l00000436: - assume {:captureState "l00000436"} true; + goto l000003ef; + l000003ef: + assume {:captureState "l000003ef"} true; R2, Gamma_R2 := R0, Gamma_R0; R0, Gamma_R0 := R19, Gamma_R19; R1, Gamma_R1 := 1bv64, true; R30, Gamma_R30 := 2436bv64, true; call memset(); - goto l00000455; - l00000455: - assume {:captureState "l00000455"} true; + goto l00000408; + l00000408: + assume {:captureState "l00000408"} true; call rely(); R0, Gamma_R0 := memory_load64_le(mem, bvadd64(R21, 120bv64)), (gamma_load64(Gamma_mem, bvadd64(R21, 120bv64)) || L(mem, bvadd64(R21, 120bv64))); R30, Gamma_R30 := 2444bv64, true; call #free(); - goto l00000465; - l00000465: - assume {:captureState "l00000465"} true; - R0, Gamma_R0 := 0bv32, true; - R20, Gamma_R20 := memory_load64_le(stack, bvadd64(R31, 32bv64)), gamma_load64(Gamma_stack, bvadd64(R31, 32bv64)); - R19, Gamma_R19 := memory_load64_le(stack, bvadd64(R31, 40bv64)), gamma_load64(Gamma_stack, bvadd64(R31, 40bv64)); + goto l00000417; + l00000417: + assume {:captureState "l00000417"} true; + R0, Gamma_R0 := 0bv64, true; + #6, Gamma_#6 := bvadd64(R31, 32bv64), Gamma_R31; + R20, Gamma_R20 := memory_load64_le(stack, #6), gamma_load64(Gamma_stack, #6); + R19, Gamma_R19 := memory_load64_le(stack, bvadd64(#6, 8bv64)), gamma_load64(Gamma_stack, bvadd64(#6, 8bv64)); R21, Gamma_R21 := memory_load64_le(stack, bvadd64(R31, 16bv64)), gamma_load64(Gamma_stack, bvadd64(R31, 16bv64)); R29, Gamma_R29 := memory_load64_le(stack, R31), gamma_load64(Gamma_stack, R31); R30, Gamma_R30 := memory_load64_le(stack, bvadd64(R31, 8bv64)), gamma_load64(Gamma_stack, bvadd64(R31, 8bv64)); diff --git a/src/test/incorrect/malloc_memcpy_strlen_memset_free/gcc_O2/malloc_memcpy_strlen_memset_free.expected b/src/test/incorrect/malloc_memcpy_strlen_memset_free/gcc_O2/malloc_memcpy_strlen_memset_free.expected index 455a7193f..a05348e17 100644 --- a/src/test/incorrect/malloc_memcpy_strlen_memset_free/gcc_O2/malloc_memcpy_strlen_memset_free.expected +++ b/src/test/incorrect/malloc_memcpy_strlen_memset_free/gcc_O2/malloc_memcpy_strlen_memset_free.expected @@ -78,7 +78,7 @@ function {:extern} memory_store64_le(memory: [bv64]bv8, index: bv64, value: bv64 memory[index := value[8:0]][bvadd64(index, 1bv64) := value[16:8]][bvadd64(index, 2bv64) := value[24:16]][bvadd64(index, 3bv64) := value[32:24]][bvadd64(index, 4bv64) := value[40:32]][bvadd64(index, 5bv64) := value[48:40]][bvadd64(index, 6bv64) := value[56:48]][bvadd64(index, 7bv64) := value[64:56]] } -function {:extern} memory_store8_be(memory: [bv64]bv8, index: bv64, value: bv8) returns ([bv64]bv8) { +function {:extern} memory_store8_le(memory: [bv64]bv8, index: bv64, value: bv8) returns ([bv64]bv8) { memory[index := value[8:0]] } @@ -330,33 +330,35 @@ procedure main() free ensures (memory_load8_le(mem, 131166bv64) == 0bv8); free ensures (memory_load8_le(mem, 131167bv64) == 0bv8); { - var #14: bv64; - var #9: bv64; - var Gamma_#14: bool; - var Gamma_#9: bool; + var #1: bv64; + var #2: bv64; + var #3: bv64; + var Gamma_#1: bool; + var Gamma_#2: bool; + var Gamma_#3: bool; lmain: assume {:captureState "lmain"} true; - #9, Gamma_#9 := bvadd64(R31, 18446744073709551568bv64), Gamma_R31; - stack, Gamma_stack := memory_store64_le(stack, #9, R29), gamma_store64(Gamma_stack, #9, Gamma_R29); - assume {:captureState "%00000238"} true; - stack, Gamma_stack := memory_store64_le(stack, bvadd64(#9, 8bv64), R30), gamma_store64(Gamma_stack, bvadd64(#9, 8bv64), Gamma_R30); - assume {:captureState "%0000023d"} true; - R31, Gamma_R31 := #9, Gamma_#9; + #1, Gamma_#1 := bvadd64(R31, 18446744073709551568bv64), Gamma_R31; + stack, Gamma_stack := memory_store64_le(stack, #1, R29), gamma_store64(Gamma_stack, #1, Gamma_R29); + assume {:captureState "%00000233"} true; + stack, Gamma_stack := memory_store64_le(stack, bvadd64(#1, 8bv64), R30), gamma_store64(Gamma_stack, bvadd64(#1, 8bv64), Gamma_R30); + assume {:captureState "%00000239"} true; + R31, Gamma_R31 := #1, Gamma_#1; R0, Gamma_R0 := 11bv64, true; R29, Gamma_R29 := R31, Gamma_R31; - #14, Gamma_#14 := bvadd64(R31, 16bv64), Gamma_R31; - stack, Gamma_stack := memory_store64_le(stack, #14, R19), gamma_store64(Gamma_stack, #14, Gamma_R19); - assume {:captureState "%0000025b"} true; - stack, Gamma_stack := memory_store64_le(stack, bvadd64(#14, 8bv64), R20), gamma_store64(Gamma_stack, bvadd64(#14, 8bv64), Gamma_R20); - assume {:captureState "%00000260"} true; + #2, Gamma_#2 := bvadd64(R31, 16bv64), Gamma_R31; + stack, Gamma_stack := memory_store64_le(stack, #2, R19), gamma_store64(Gamma_stack, #2, Gamma_R19); + assume {:captureState "%00000254"} true; + stack, Gamma_stack := memory_store64_le(stack, bvadd64(#2, 8bv64), R20), gamma_store64(Gamma_stack, bvadd64(#2, 8bv64), Gamma_R20); + assume {:captureState "%0000025a"} true; R20, Gamma_R20 := 131072bv64, true; stack, Gamma_stack := memory_store64_le(stack, bvadd64(R31, 32bv64), R21), gamma_store64(Gamma_stack, bvadd64(R31, 32bv64), Gamma_R21); - assume {:captureState "%0000026e"} true; + assume {:captureState "%00000267"} true; R30, Gamma_R30 := 2012bv64, true; call malloc(); - goto l00000278; - l00000278: - assume {:captureState "l00000278"} true; + goto l00000271; + l00000271: + assume {:captureState "l00000271"} true; R21, Gamma_R21 := 131072bv64, true; R21, Gamma_R21 := bvadd64(R21, 96bv64), Gamma_R21; R19, Gamma_R19 := R0, Gamma_R0; @@ -364,57 +366,58 @@ procedure main() call rely(); assert (L(mem, bvadd64(R20, 120bv64)) ==> Gamma_R19); mem, Gamma_mem := memory_store64_le(mem, bvadd64(R20, 120bv64), R19), gamma_store64(Gamma_mem, bvadd64(R20, 120bv64), Gamma_R19); - assume {:captureState "%0000029b"} true; + assume {:captureState "%0000028e"} true; R30, Gamma_R30 := 2036bv64, true; call strlen(); - goto l000002a5; - l000002a5: - assume {:captureState "l000002a5"} true; + goto l00000298; + l00000298: + assume {:captureState "l00000298"} true; R1, Gamma_R1 := R21, Gamma_R21; R2, Gamma_R2 := R0, Gamma_R0; R0, Gamma_R0 := R19, Gamma_R19; R30, Gamma_R30 := 2052bv64, true; call memcpy(); - goto l000002c5; - l000002c5: - assume {:captureState "l000002c5"} true; + goto l000002b2; + l000002b2: + assume {:captureState "l000002b2"} true; R0, Gamma_R0 := R19, Gamma_R19; R30, Gamma_R30 := 2060bv64, true; call puts(); - goto l000002d5; - l000002d5: - assume {:captureState "l000002d5"} true; + goto l000002c0; + l000002c0: + assume {:captureState "l000002c0"} true; call rely(); R0, Gamma_R0 := memory_load64_le(mem, bvadd64(R20, 120bv64)), (gamma_load64(Gamma_mem, bvadd64(R20, 120bv64)) || L(mem, bvadd64(R20, 120bv64))); call rely(); assert (L(mem, bvadd64(R0, 4bv64)) ==> true); - mem, Gamma_mem := memory_store8_be(mem, bvadd64(R0, 4bv64), 0bv8), gamma_store8(Gamma_mem, bvadd64(R0, 4bv64), true); - assume {:captureState "%000002e3"} true; + mem, Gamma_mem := memory_store8_le(mem, bvadd64(R0, 4bv64), 0bv8), gamma_store8(Gamma_mem, bvadd64(R0, 4bv64), true); + assume {:captureState "%000002cc"} true; call rely(); R19, Gamma_R19 := memory_load64_le(mem, bvadd64(R20, 120bv64)), (gamma_load64(Gamma_mem, bvadd64(R20, 120bv64)) || L(mem, bvadd64(R20, 120bv64))); R0, Gamma_R0 := R19, Gamma_R19; R30, Gamma_R30 := 2080bv64, true; call strlen(); - goto l000002fc; - l000002fc: - assume {:captureState "l000002fc"} true; + goto l000002e2; + l000002e2: + assume {:captureState "l000002e2"} true; R1, Gamma_R1 := 1bv64, true; R2, Gamma_R2 := R0, Gamma_R0; R0, Gamma_R0 := R19, Gamma_R19; R30, Gamma_R30 := 2096bv64, true; call memset(); - goto l0000031b; - l0000031b: - assume {:captureState "l0000031b"} true; + goto l000002fb; + l000002fb: + assume {:captureState "l000002fb"} true; call rely(); R0, Gamma_R0 := memory_load64_le(mem, bvadd64(R20, 120bv64)), (gamma_load64(Gamma_mem, bvadd64(R20, 120bv64)) || L(mem, bvadd64(R20, 120bv64))); R30, Gamma_R30 := 2104bv64, true; call #free(); - goto l0000032b; - l0000032b: - assume {:captureState "l0000032b"} true; - R19, Gamma_R19 := memory_load64_le(stack, bvadd64(R31, 16bv64)), gamma_load64(Gamma_stack, bvadd64(R31, 16bv64)); - R20, Gamma_R20 := memory_load64_le(stack, bvadd64(R31, 24bv64)), gamma_load64(Gamma_stack, bvadd64(R31, 24bv64)); + goto l0000030a; + l0000030a: + assume {:captureState "l0000030a"} true; + #3, Gamma_#3 := bvadd64(R31, 16bv64), Gamma_R31; + R19, Gamma_R19 := memory_load64_le(stack, #3), gamma_load64(Gamma_stack, #3); + R20, Gamma_R20 := memory_load64_le(stack, bvadd64(#3, 8bv64)), gamma_load64(Gamma_stack, bvadd64(#3, 8bv64)); R0, Gamma_R0 := 0bv64, true; R21, Gamma_R21 := memory_load64_le(stack, bvadd64(R31, 32bv64)), gamma_load64(Gamma_stack, bvadd64(R31, 32bv64)); R29, Gamma_R29 := memory_load64_le(stack, R31), gamma_load64(Gamma_stack, R31);