Skip to content

Commit

Permalink
update expected
Browse files Browse the repository at this point in the history
  • Loading branch information
l-kent committed Oct 25, 2023
1 parent a8296a6 commit 7e19902
Show file tree
Hide file tree
Showing 349 changed files with 9,588 additions and 9,588 deletions.
44 changes: 22 additions & 22 deletions src/test/correct/arrays_simple/clang/arrays_simple.expected
View file
Original file line number Diff line number Diff line change
@@ -1,38 +1,38 @@
var Gamma_R0: bool;
var Gamma_R31: bool;
var Gamma_R8: bool;
var Gamma_mem: [bv64]bool;
var Gamma_stack: [bv64]bool;
var R0: bv64;
var R31: bv64;
var R8: bv64;
var mem: [bv64]bv8;
var stack: [bv64]bv8;
const $_IO_stdin_used_addr: bv64;
var {:extern} Gamma_R0: bool;
var {:extern} Gamma_R31: bool;
var {:extern} Gamma_R8: bool;
var {:extern} Gamma_mem: [bv64]bool;
var {:extern} Gamma_stack: [bv64]bool;
var {:extern} R0: bv64;
var {:extern} R31: bv64;
var {:extern} R8: bv64;
var {:extern} mem: [bv64]bv8;
var {:extern} stack: [bv64]bv8;
const {:extern} $_IO_stdin_used_addr: bv64;
axiom ($_IO_stdin_used_addr == 1872bv64);
function {:bvbuiltin "bvadd"} bvadd64(bv64, bv64) returns (bv64);
function gamma_load32(gammaMap: [bv64]bool, index: bv64) returns (bool) {
function {:extern} {:bvbuiltin "bvadd"} bvadd64(bv64, bv64) returns (bv64);
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 gamma_store32(gammaMap: [bv64]bool, index: bv64, value: bool) returns ([bv64]bool) {
function {:extern} gamma_store32(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]
}

function memory_load32_le(memory: [bv64]bv8, index: bv64) returns (bv32) {
function {:extern} memory_load32_le(memory: [bv64]bv8, index: bv64) returns (bv32) {
(memory[bvadd64(index, 3bv64)] ++ (memory[bvadd64(index, 2bv64)] ++ (memory[bvadd64(index, 1bv64)] ++ memory[index])))
}

function memory_load8_le(memory: [bv64]bv8, index: bv64) returns (bv8) {
function {:extern} memory_load8_le(memory: [bv64]bv8, index: bv64) returns (bv8) {
memory[index]
}

function memory_store32_le(memory: [bv64]bv8, index: bv64, value: bv32) returns ([bv64]bv8) {
function {:extern} memory_store32_le(memory: [bv64]bv8, index: bv64, value: bv32) 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]]
}

function {:bvbuiltin "zero_extend 32"} zero_extend32_32(bv32) returns (bv64);
procedure rely();
function {:extern} {:bvbuiltin "zero_extend 32"} zero_extend32_32(bv32) returns (bv64);
procedure {:extern} rely();
modifies Gamma_mem, mem;
ensures (mem == old(mem));
ensures (Gamma_mem == old(Gamma_mem));
Expand Down Expand Up @@ -73,7 +73,7 @@ procedure rely();
free ensures (memory_load8_le(mem, 69678bv64) == 0bv8);
free ensures (memory_load8_le(mem, 69679bv64) == 0bv8);

procedure rely_transitive()
procedure {:extern} rely_transitive()
modifies Gamma_mem, mem;
ensures (mem == old(mem));
ensures (Gamma_mem == old(Gamma_mem));
Expand All @@ -82,9 +82,9 @@ procedure rely_transitive()
call rely();
}

procedure rely_reflexive();
procedure {:extern} rely_reflexive();

procedure guarantee_reflexive();
procedure {:extern} guarantee_reflexive();
modifies Gamma_mem, mem;

procedure main()
Expand Down
20 changes: 10 additions & 10 deletions src/test/correct/arrays_simple/clang_O2/arrays_simple.expected
View file
Original file line number Diff line number Diff line change
@@ -1,14 +1,14 @@
var Gamma_R0: bool;
var Gamma_mem: [bv64]bool;
var R0: bv64;
var mem: [bv64]bv8;
const $_IO_stdin_used_addr: bv64;
var {:extern} Gamma_R0: bool;
var {:extern} Gamma_mem: [bv64]bool;
var {:extern} R0: bv64;
var {:extern} mem: [bv64]bv8;
const {:extern} $_IO_stdin_used_addr: bv64;
axiom ($_IO_stdin_used_addr == 1840bv64);
function memory_load8_le(memory: [bv64]bv8, index: bv64) returns (bv8) {
function {:extern} memory_load8_le(memory: [bv64]bv8, index: bv64) returns (bv8) {
memory[index]
}

procedure rely();
procedure {:extern} rely();
modifies Gamma_mem, mem;
ensures (mem == old(mem));
ensures (Gamma_mem == old(Gamma_mem));
Expand Down Expand Up @@ -49,7 +49,7 @@ procedure rely();
free ensures (memory_load8_le(mem, 69678bv64) == 0bv8);
free ensures (memory_load8_le(mem, 69679bv64) == 0bv8);

procedure rely_transitive()
procedure {:extern} rely_transitive()
modifies Gamma_mem, mem;
ensures (mem == old(mem));
ensures (Gamma_mem == old(Gamma_mem));
Expand All @@ -58,9 +58,9 @@ procedure rely_transitive()
call rely();
}

procedure rely_reflexive();
procedure {:extern} rely_reflexive();

procedure guarantee_reflexive();
procedure {:extern} guarantee_reflexive();
modifies Gamma_mem, mem;

procedure main()
Expand Down
44 changes: 22 additions & 22 deletions src/test/correct/arrays_simple/clang_no_plt_no_pic/arrays_simple.expected
View file
Original file line number Diff line number Diff line change
@@ -1,38 +1,38 @@
var Gamma_R0: bool;
var Gamma_R31: bool;
var Gamma_R8: bool;
var Gamma_mem: [bv64]bool;
var Gamma_stack: [bv64]bool;
var R0: bv64;
var R31: bv64;
var R8: bv64;
var mem: [bv64]bv8;
var stack: [bv64]bv8;
const $_IO_stdin_used_addr: bv64;
var {:extern} Gamma_R0: bool;
var {:extern} Gamma_R31: bool;
var {:extern} Gamma_R8: bool;
var {:extern} Gamma_mem: [bv64]bool;
var {:extern} Gamma_stack: [bv64]bool;
var {:extern} R0: bv64;
var {:extern} R31: bv64;
var {:extern} R8: bv64;
var {:extern} mem: [bv64]bv8;
var {:extern} stack: [bv64]bv8;
const {:extern} $_IO_stdin_used_addr: bv64;
axiom ($_IO_stdin_used_addr == 1872bv64);
function {:bvbuiltin "bvadd"} bvadd64(bv64, bv64) returns (bv64);
function gamma_load32(gammaMap: [bv64]bool, index: bv64) returns (bool) {
function {:extern} {:bvbuiltin "bvadd"} bvadd64(bv64, bv64) returns (bv64);
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 gamma_store32(gammaMap: [bv64]bool, index: bv64, value: bool) returns ([bv64]bool) {
function {:extern} gamma_store32(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]
}

function memory_load32_le(memory: [bv64]bv8, index: bv64) returns (bv32) {
function {:extern} memory_load32_le(memory: [bv64]bv8, index: bv64) returns (bv32) {
(memory[bvadd64(index, 3bv64)] ++ (memory[bvadd64(index, 2bv64)] ++ (memory[bvadd64(index, 1bv64)] ++ memory[index])))
}

function memory_load8_le(memory: [bv64]bv8, index: bv64) returns (bv8) {
function {:extern} memory_load8_le(memory: [bv64]bv8, index: bv64) returns (bv8) {
memory[index]
}

function memory_store32_le(memory: [bv64]bv8, index: bv64, value: bv32) returns ([bv64]bv8) {
function {:extern} memory_store32_le(memory: [bv64]bv8, index: bv64, value: bv32) 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]]
}

function {:bvbuiltin "zero_extend 32"} zero_extend32_32(bv32) returns (bv64);
procedure rely();
function {:extern} {:bvbuiltin "zero_extend 32"} zero_extend32_32(bv32) returns (bv64);
procedure {:extern} rely();
modifies Gamma_mem, mem;
ensures (mem == old(mem));
ensures (Gamma_mem == old(Gamma_mem));
Expand Down Expand Up @@ -73,7 +73,7 @@ procedure rely();
free ensures (memory_load8_le(mem, 69678bv64) == 0bv8);
free ensures (memory_load8_le(mem, 69679bv64) == 0bv8);

procedure rely_transitive()
procedure {:extern} rely_transitive()
modifies Gamma_mem, mem;
ensures (mem == old(mem));
ensures (Gamma_mem == old(Gamma_mem));
Expand All @@ -82,9 +82,9 @@ procedure rely_transitive()
call rely();
}

procedure rely_reflexive();
procedure {:extern} rely_reflexive();

procedure guarantee_reflexive();
procedure {:extern} guarantee_reflexive();
modifies Gamma_mem, mem;

procedure main()
Expand Down
44 changes: 22 additions & 22 deletions src/test/correct/arrays_simple/clang_pic/arrays_simple.expected
View file
Original file line number Diff line number Diff line change
@@ -1,38 +1,38 @@
var Gamma_R0: bool;
var Gamma_R31: bool;
var Gamma_R8: bool;
var Gamma_mem: [bv64]bool;
var Gamma_stack: [bv64]bool;
var R0: bv64;
var R31: bv64;
var R8: bv64;
var mem: [bv64]bv8;
var stack: [bv64]bv8;
const $_IO_stdin_used_addr: bv64;
var {:extern} Gamma_R0: bool;
var {:extern} Gamma_R31: bool;
var {:extern} Gamma_R8: bool;
var {:extern} Gamma_mem: [bv64]bool;
var {:extern} Gamma_stack: [bv64]bool;
var {:extern} R0: bv64;
var {:extern} R31: bv64;
var {:extern} R8: bv64;
var {:extern} mem: [bv64]bv8;
var {:extern} stack: [bv64]bv8;
const {:extern} $_IO_stdin_used_addr: bv64;
axiom ($_IO_stdin_used_addr == 1872bv64);
function {:bvbuiltin "bvadd"} bvadd64(bv64, bv64) returns (bv64);
function gamma_load32(gammaMap: [bv64]bool, index: bv64) returns (bool) {
function {:extern} {:bvbuiltin "bvadd"} bvadd64(bv64, bv64) returns (bv64);
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 gamma_store32(gammaMap: [bv64]bool, index: bv64, value: bool) returns ([bv64]bool) {
function {:extern} gamma_store32(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]
}

function memory_load32_le(memory: [bv64]bv8, index: bv64) returns (bv32) {
function {:extern} memory_load32_le(memory: [bv64]bv8, index: bv64) returns (bv32) {
(memory[bvadd64(index, 3bv64)] ++ (memory[bvadd64(index, 2bv64)] ++ (memory[bvadd64(index, 1bv64)] ++ memory[index])))
}

function memory_load8_le(memory: [bv64]bv8, index: bv64) returns (bv8) {
function {:extern} memory_load8_le(memory: [bv64]bv8, index: bv64) returns (bv8) {
memory[index]
}

function memory_store32_le(memory: [bv64]bv8, index: bv64, value: bv32) returns ([bv64]bv8) {
function {:extern} memory_store32_le(memory: [bv64]bv8, index: bv64, value: bv32) 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]]
}

function {:bvbuiltin "zero_extend 32"} zero_extend32_32(bv32) returns (bv64);
procedure rely();
function {:extern} {:bvbuiltin "zero_extend 32"} zero_extend32_32(bv32) returns (bv64);
procedure {:extern} rely();
modifies Gamma_mem, mem;
ensures (mem == old(mem));
ensures (Gamma_mem == old(Gamma_mem));
Expand Down Expand Up @@ -73,7 +73,7 @@ procedure rely();
free ensures (memory_load8_le(mem, 69678bv64) == 0bv8);
free ensures (memory_load8_le(mem, 69679bv64) == 0bv8);

procedure rely_transitive()
procedure {:extern} rely_transitive()
modifies Gamma_mem, mem;
ensures (mem == old(mem));
ensures (Gamma_mem == old(Gamma_mem));
Expand All @@ -82,9 +82,9 @@ procedure rely_transitive()
call rely();
}

procedure rely_reflexive();
procedure {:extern} rely_reflexive();

procedure guarantee_reflexive();
procedure {:extern} guarantee_reflexive();
modifies Gamma_mem, mem;

procedure main()
Expand Down
20 changes: 10 additions & 10 deletions src/test/correct/arrays_simple/gcc_O2/arrays_simple.expected
View file
Original file line number Diff line number Diff line change
@@ -1,14 +1,14 @@
var Gamma_R0: bool;
var Gamma_mem: [bv64]bool;
var R0: bv64;
var mem: [bv64]bv8;
const $_IO_stdin_used_addr: bv64;
var {:extern} Gamma_R0: bool;
var {:extern} Gamma_mem: [bv64]bool;
var {:extern} R0: bv64;
var {:extern} mem: [bv64]bv8;
const {:extern} $_IO_stdin_used_addr: bv64;
axiom ($_IO_stdin_used_addr == 1896bv64);
function memory_load8_le(memory: [bv64]bv8, index: bv64) returns (bv8) {
function {:extern} memory_load8_le(memory: [bv64]bv8, index: bv64) returns (bv8) {
memory[index]
}

procedure rely();
procedure {:extern} rely();
modifies Gamma_mem, mem;
ensures (mem == old(mem));
ensures (Gamma_mem == old(Gamma_mem));
Expand Down Expand Up @@ -49,7 +49,7 @@ procedure rely();
free ensures (memory_load8_le(mem, 69646bv64) == 0bv8);
free ensures (memory_load8_le(mem, 69647bv64) == 0bv8);

procedure rely_transitive()
procedure {:extern} rely_transitive()
modifies Gamma_mem, mem;
ensures (mem == old(mem));
ensures (Gamma_mem == old(Gamma_mem));
Expand All @@ -58,9 +58,9 @@ procedure rely_transitive()
call rely();
}

procedure rely_reflexive();
procedure {:extern} rely_reflexive();

procedure guarantee_reflexive();
procedure {:extern} guarantee_reflexive();
modifies Gamma_mem, mem;

procedure main()
Expand Down
Loading

0 comments on commit 7e19902

Please sign in to comment.