update expected

UQ-PAC · Oct 27, 2023 · a60c354 · a60c354
1 parent b3d0260
commit a60c354
Show file tree

Hide file tree

Showing 349 changed files with 14,711 additions and 12,234 deletions.
diff --git a/src/test/correct/arrays_simple/clang/arrays_simple.expected b/src/test/correct/arrays_simple/clang/arrays_simple.expected
@@ -1,38 +1,38 @@
-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 {:extern } ($_IO_stdin_used_addr == 1872bv64);
-function {:extern } {:bvbuiltin "bvadd"} bvadd64(bv64, bv64) returns (bv64);
-function {:extern } gamma_load32(gammaMap: [bv64]bool, index: bv64) returns (bool) {
+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 {:extern }($_IO_stdin_used_addr == 1872bv64);
+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 {:extern } 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 {:extern } 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 {:extern } 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 {:extern } 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 {:extern } {:bvbuiltin "zero_extend 32"} zero_extend32_32(bv32) returns (bv64);
-procedure {:extern } 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));
@@ -73,7 +73,7 @@ procedure {:extern } rely();
   free ensures (memory_load8_le(mem, 69678bv64) == 0bv8);
   free ensures (memory_load8_le(mem, 69679bv64) == 0bv8);
 
-procedure {:extern } rely_transitive()
+procedure {:extern }rely_transitive()
   modifies Gamma_mem, mem;
   ensures (mem == old(mem));
   ensures (Gamma_mem == old(Gamma_mem));
@@ -82,12 +82,12 @@ procedure {:extern } rely_transitive()
   call rely();
 }
 
-procedure {:extern } rely_reflexive();
+procedure {:extern }rely_reflexive();
 
-procedure {:extern } guarantee_reflexive();
+procedure {:extern }guarantee_reflexive();
   modifies Gamma_mem, mem;
 
-procedure  main()
+procedure main()
   modifies Gamma_R0, Gamma_R31, Gamma_R8, Gamma_stack, R0, R31, R8, stack;
   free requires (memory_load8_le(mem, 69664bv64) == 0bv8);
   free requires (memory_load8_le(mem, 69665bv64) == 0bv8);
@@ -181,13 +181,17 @@ procedure  main()
   free ensures (memory_load8_le(mem, 69679bv64) == 0bv8);
 {
   lmain:
+    assume {:captureState "addr:0x714"}true;
     R31, Gamma_R31 := bvadd64(R31, 18446744073709551584bv64), Gamma_R31;
     R8, Gamma_R8 := 3bv64, true;
     stack, Gamma_stack := memory_store32_le(stack, bvadd64(R31, 20bv64), R8[32:0]), gamma_store32(Gamma_stack, bvadd64(R31, 20bv64), Gamma_R8);
+    assume {:captureState "addr:0x71c"}true;
     R8, Gamma_R8 := 7bv64, true;
     stack, Gamma_stack := memory_store32_le(stack, bvadd64(R31, 28bv64), R8[32:0]), gamma_store32(Gamma_stack, bvadd64(R31, 28bv64), Gamma_R8);
+    assume {:captureState "addr:0x724"}true;
     R8, Gamma_R8 := zero_extend32_32(memory_load32_le(stack, bvadd64(R31, 20bv64))), gamma_load32(Gamma_stack, bvadd64(R31, 20bv64));
     stack, Gamma_stack := memory_store32_le(stack, bvadd64(R31, 8bv64), R8[32:0]), gamma_store32(Gamma_stack, bvadd64(R31, 8bv64), Gamma_R8);
+    assume {:captureState "addr:0x72c"}true;
     R0, Gamma_R0 := 0bv64, true;
     R31, Gamma_R31 := bvadd64(R31, 32bv64), Gamma_R31;
     return;

diff --git a/src/test/correct/arrays_simple/clang_O2/arrays_simple.expected b/src/test/correct/arrays_simple/clang_O2/arrays_simple.expected
@@ -1,14 +1,14 @@
-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 {:extern } ($_IO_stdin_used_addr == 1840bv64);
-function {:extern } memory_load8_le(memory: [bv64]bv8, index: bv64) returns (bv8) {
+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 {:extern }($_IO_stdin_used_addr == 1840bv64);
+function {:extern }memory_load8_le(memory: [bv64]bv8, index: bv64) returns (bv8) {
   memory[index]
 }
 
-procedure {:extern } rely();
+procedure {:extern }rely();
   modifies Gamma_mem, mem;
   ensures (mem == old(mem));
   ensures (Gamma_mem == old(Gamma_mem));
@@ -49,7 +49,7 @@ procedure {:extern } rely();
   free ensures (memory_load8_le(mem, 69678bv64) == 0bv8);
   free ensures (memory_load8_le(mem, 69679bv64) == 0bv8);
 
-procedure {:extern } rely_transitive()
+procedure {:extern }rely_transitive()
   modifies Gamma_mem, mem;
   ensures (mem == old(mem));
   ensures (Gamma_mem == old(Gamma_mem));
@@ -58,12 +58,12 @@ procedure {:extern } rely_transitive()
   call rely();
 }
 
-procedure {:extern } rely_reflexive();
+procedure {:extern }rely_reflexive();
 
-procedure {:extern } guarantee_reflexive();
+procedure {:extern }guarantee_reflexive();
   modifies Gamma_mem, mem;
 
-procedure  main()
+procedure main()
   modifies Gamma_R0, R0;
   free requires (memory_load8_le(mem, 69664bv64) == 0bv8);
   free requires (memory_load8_le(mem, 69665bv64) == 0bv8);
@@ -155,6 +155,7 @@ procedure  main()
   free ensures (memory_load8_le(mem, 69679bv64) == 0bv8);
 {
   lmain:
+    assume {:captureState "addr:0x714"}true;
     R0, Gamma_R0 := 0bv64, true;
     return;
 }
diff --git a/src/test/correct/arrays_simple/clang_no_plt_no_pic/arrays_simple.expected b/src/test/correct/arrays_simple/clang_no_plt_no_pic/arrays_simple.expected
@@ -1,38 +1,38 @@
-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 {:extern } ($_IO_stdin_used_addr == 1872bv64);
-function {:extern } {:bvbuiltin "bvadd"} bvadd64(bv64, bv64) returns (bv64);
-function {:extern } gamma_load32(gammaMap: [bv64]bool, index: bv64) returns (bool) {
+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 {:extern }($_IO_stdin_used_addr == 1872bv64);
+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 {:extern } 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 {:extern } 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 {:extern } 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 {:extern } 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 {:extern } {:bvbuiltin "zero_extend 32"} zero_extend32_32(bv32) returns (bv64);
-procedure {:extern } 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));
@@ -73,7 +73,7 @@ procedure {:extern } rely();
   free ensures (memory_load8_le(mem, 69678bv64) == 0bv8);
   free ensures (memory_load8_le(mem, 69679bv64) == 0bv8);
 
-procedure {:extern } rely_transitive()
+procedure {:extern }rely_transitive()
   modifies Gamma_mem, mem;
   ensures (mem == old(mem));
   ensures (Gamma_mem == old(Gamma_mem));
@@ -82,12 +82,12 @@ procedure {:extern } rely_transitive()
   call rely();
 }
 
-procedure {:extern } rely_reflexive();
+procedure {:extern }rely_reflexive();
 
-procedure {:extern } guarantee_reflexive();
+procedure {:extern }guarantee_reflexive();
   modifies Gamma_mem, mem;
 
-procedure  main()
+procedure main()
   modifies Gamma_R0, Gamma_R31, Gamma_R8, Gamma_stack, R0, R31, R8, stack;
   free requires (memory_load8_le(mem, 69664bv64) == 0bv8);
   free requires (memory_load8_le(mem, 69665bv64) == 0bv8);
@@ -181,13 +181,17 @@ procedure  main()
   free ensures (memory_load8_le(mem, 69679bv64) == 0bv8);
 {
   lmain:
+    assume {:captureState "addr:0x714"}true;
     R31, Gamma_R31 := bvadd64(R31, 18446744073709551584bv64), Gamma_R31;
     R8, Gamma_R8 := 3bv64, true;
     stack, Gamma_stack := memory_store32_le(stack, bvadd64(R31, 20bv64), R8[32:0]), gamma_store32(Gamma_stack, bvadd64(R31, 20bv64), Gamma_R8);
+    assume {:captureState "addr:0x71c"}true;
     R8, Gamma_R8 := 7bv64, true;
     stack, Gamma_stack := memory_store32_le(stack, bvadd64(R31, 28bv64), R8[32:0]), gamma_store32(Gamma_stack, bvadd64(R31, 28bv64), Gamma_R8);
+    assume {:captureState "addr:0x724"}true;
     R8, Gamma_R8 := zero_extend32_32(memory_load32_le(stack, bvadd64(R31, 20bv64))), gamma_load32(Gamma_stack, bvadd64(R31, 20bv64));
     stack, Gamma_stack := memory_store32_le(stack, bvadd64(R31, 8bv64), R8[32:0]), gamma_store32(Gamma_stack, bvadd64(R31, 8bv64), Gamma_R8);
+    assume {:captureState "addr:0x72c"}true;
     R0, Gamma_R0 := 0bv64, true;
     R31, Gamma_R31 := bvadd64(R31, 32bv64), Gamma_R31;
     return;

diff --git a/src/test/correct/arrays_simple/clang_pic/arrays_simple.expected b/src/test/correct/arrays_simple/clang_pic/arrays_simple.expected
@@ -1,38 +1,38 @@
-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 {:extern } ($_IO_stdin_used_addr == 1872bv64);
-function {:extern } {:bvbuiltin "bvadd"} bvadd64(bv64, bv64) returns (bv64);
-function {:extern } gamma_load32(gammaMap: [bv64]bool, index: bv64) returns (bool) {
+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 {:extern }($_IO_stdin_used_addr == 1872bv64);
+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 {:extern } 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 {:extern } 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 {:extern } 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 {:extern } 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 {:extern } {:bvbuiltin "zero_extend 32"} zero_extend32_32(bv32) returns (bv64);
-procedure {:extern } 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));
@@ -73,7 +73,7 @@ procedure {:extern } rely();
   free ensures (memory_load8_le(mem, 69678bv64) == 0bv8);
   free ensures (memory_load8_le(mem, 69679bv64) == 0bv8);
 
-procedure {:extern } rely_transitive()
+procedure {:extern }rely_transitive()
   modifies Gamma_mem, mem;
   ensures (mem == old(mem));
   ensures (Gamma_mem == old(Gamma_mem));
@@ -82,12 +82,12 @@ procedure {:extern } rely_transitive()
   call rely();
 }
 
-procedure {:extern } rely_reflexive();
+procedure {:extern }rely_reflexive();
 
-procedure {:extern } guarantee_reflexive();
+procedure {:extern }guarantee_reflexive();
   modifies Gamma_mem, mem;
 
-procedure  main()
+procedure main()
   modifies Gamma_R0, Gamma_R31, Gamma_R8, Gamma_stack, R0, R31, R8, stack;
   free requires (memory_load8_le(mem, 69664bv64) == 0bv8);
   free requires (memory_load8_le(mem, 69665bv64) == 0bv8);
@@ -181,13 +181,17 @@ procedure  main()
   free ensures (memory_load8_le(mem, 69679bv64) == 0bv8);
 {
   lmain:
+    assume {:captureState "addr:0x714"}true;
     R31, Gamma_R31 := bvadd64(R31, 18446744073709551584bv64), Gamma_R31;
     R8, Gamma_R8 := 3bv64, true;
     stack, Gamma_stack := memory_store32_le(stack, bvadd64(R31, 20bv64), R8[32:0]), gamma_store32(Gamma_stack, bvadd64(R31, 20bv64), Gamma_R8);
+    assume {:captureState "addr:0x71c"}true;
     R8, Gamma_R8 := 7bv64, true;
     stack, Gamma_stack := memory_store32_le(stack, bvadd64(R31, 28bv64), R8[32:0]), gamma_store32(Gamma_stack, bvadd64(R31, 28bv64), Gamma_R8);
+    assume {:captureState "addr:0x724"}true;
     R8, Gamma_R8 := zero_extend32_32(memory_load32_le(stack, bvadd64(R31, 20bv64))), gamma_load32(Gamma_stack, bvadd64(R31, 20bv64));
     stack, Gamma_stack := memory_store32_le(stack, bvadd64(R31, 8bv64), R8[32:0]), gamma_store32(Gamma_stack, bvadd64(R31, 8bv64), Gamma_R8);
+    assume {:captureState "addr:0x72c"}true;
     R0, Gamma_R0 := 0bv64, true;
     R31, Gamma_R31 := bvadd64(R31, 32bv64), Gamma_R31;
     return;