update expected files

UQ-PAC · Oct 13, 2023 · c6a411f · c6a411f
1 parent 96b6d13
commit c6a411f
Show file tree

Hide file tree

Showing 63 changed files with 441 additions and 70 deletions.
diff --git a/src/test/correct/basicfree/clang/basicfree.expected b/src/test/correct/basicfree/clang/basicfree.expected
@@ -1,4 +1,6 @@
 var Gamma_R0: bool;
+var Gamma_R16: bool;
+var Gamma_R17: bool;
 var Gamma_R29: bool;
 var Gamma_R30: bool;
 var Gamma_R31: bool;
@@ -7,6 +9,8 @@ var Gamma_R9: bool;
 var Gamma_mem: [bv64]bool;
 var Gamma_stack: [bv64]bool;
 var R0: bv64;
+var R16: bv64;
+var R17: bv64;
 var R29: bv64;
 var R30: bv64;
 var R31: bv64;
@@ -70,9 +74,10 @@ procedure guarantee_reflexive();
   modifies mem, Gamma_mem;
 
 procedure #free();
+  modifies Gamma_R16, Gamma_R17, R16, R17;
 
 procedure main()
-  modifies Gamma_R0, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_R8, Gamma_R9, Gamma_mem, Gamma_stack, R0, R29, R30, R31, R8, R9, mem, stack;
+  modifies Gamma_R0, Gamma_R16, Gamma_R17, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_R8, Gamma_R9, Gamma_mem, Gamma_stack, R0, R16, R17, R29, R30, R31, R8, R9, mem, stack;
   free requires (memory_load8_le(mem, 2080bv64) == 1bv8);
   free requires (memory_load8_le(mem, 2081bv64) == 0bv8);
   free requires (memory_load8_le(mem, 2082bv64) == 2bv8);
@@ -180,3 +185,4 @@ procedure main()
 }
 
 procedure malloc();
+  modifies Gamma_R16, Gamma_R17, R16, R17;
diff --git a/src/test/correct/basicfree/clang_no_plt_no_pic/basicfree.expected b/src/test/correct/basicfree/clang_no_plt_no_pic/basicfree.expected
@@ -1,4 +1,6 @@
 var Gamma_R0: bool;
+var Gamma_R16: bool;
+var Gamma_R17: bool;
 var Gamma_R29: bool;
 var Gamma_R30: bool;
 var Gamma_R31: bool;
@@ -7,6 +9,8 @@ var Gamma_R9: bool;
 var Gamma_mem: [bv64]bool;
 var Gamma_stack: [bv64]bool;
 var R0: bv64;
+var R16: bv64;
+var R17: bv64;
 var R29: bv64;
 var R30: bv64;
 var R31: bv64;
@@ -70,9 +74,10 @@ procedure guarantee_reflexive();
   modifies mem, Gamma_mem;
 
 procedure #free();
+  modifies Gamma_R16, Gamma_R17, R16, R17;
 
 procedure main()
-  modifies Gamma_R0, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_R8, Gamma_R9, Gamma_mem, Gamma_stack, R0, R29, R30, R31, R8, R9, mem, stack;
+  modifies Gamma_R0, Gamma_R16, Gamma_R17, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_R8, Gamma_R9, Gamma_mem, Gamma_stack, R0, R16, R17, R29, R30, R31, R8, R9, mem, stack;
   free requires (memory_load8_le(mem, 2080bv64) == 1bv8);
   free requires (memory_load8_le(mem, 2081bv64) == 0bv8);
   free requires (memory_load8_le(mem, 2082bv64) == 2bv8);
@@ -180,3 +185,4 @@ procedure main()
 }
 
 procedure malloc();
+  modifies Gamma_R16, Gamma_R17, R16, R17;
diff --git a/src/test/correct/basicfree/clang_pic/basicfree.expected b/src/test/correct/basicfree/clang_pic/basicfree.expected
@@ -1,4 +1,6 @@
 var Gamma_R0: bool;
+var Gamma_R16: bool;
+var Gamma_R17: bool;
 var Gamma_R29: bool;
 var Gamma_R30: bool;
 var Gamma_R31: bool;
@@ -7,6 +9,8 @@ var Gamma_R9: bool;
 var Gamma_mem: [bv64]bool;
 var Gamma_stack: [bv64]bool;
 var R0: bv64;
+var R16: bv64;
+var R17: bv64;
 var R29: bv64;
 var R30: bv64;
 var R31: bv64;
@@ -70,9 +74,10 @@ procedure guarantee_reflexive();
   modifies mem, Gamma_mem;
 
 procedure #free();
+  modifies Gamma_R16, Gamma_R17, R16, R17;
 
 procedure main()
-  modifies Gamma_R0, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_R8, Gamma_R9, Gamma_mem, Gamma_stack, R0, R29, R30, R31, R8, R9, mem, stack;
+  modifies Gamma_R0, Gamma_R16, Gamma_R17, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_R8, Gamma_R9, Gamma_mem, Gamma_stack, R0, R16, R17, R29, R30, R31, R8, R9, mem, stack;
   free requires (memory_load8_le(mem, 2080bv64) == 1bv8);
   free requires (memory_load8_le(mem, 2081bv64) == 0bv8);
   free requires (memory_load8_le(mem, 2082bv64) == 2bv8);
@@ -180,3 +185,4 @@ procedure main()
 }
 
 procedure malloc();
+  modifies Gamma_R16, Gamma_R17, R16, R17;
diff --git a/src/test/correct/basicfree/gcc/basicfree.expected b/src/test/correct/basicfree/gcc/basicfree.expected
@@ -1,12 +1,16 @@
 var Gamma_R0: bool;
 var Gamma_R1: bool;
+var Gamma_R16: bool;
+var Gamma_R17: bool;
 var Gamma_R29: bool;
 var Gamma_R30: bool;
 var Gamma_R31: bool;
 var Gamma_mem: [bv64]bool;
 var Gamma_stack: [bv64]bool;
 var R0: bv64;
 var R1: bv64;
+var R16: bv64;
+var R17: bv64;
 var R29: bv64;
 var R30: bv64;
 var R31: bv64;
@@ -68,9 +72,10 @@ procedure guarantee_reflexive();
   modifies mem, Gamma_mem;
 
 procedure #free();
+  modifies Gamma_R16, Gamma_R17, R16, R17;
 
 procedure main()
-  modifies Gamma_R0, Gamma_R1, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_mem, Gamma_stack, R0, R1, R29, R30, R31, mem, stack;
+  modifies Gamma_R0, Gamma_R1, Gamma_R16, Gamma_R17, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_mem, Gamma_stack, R0, R1, R16, R17, R29, R30, R31, mem, stack;
   free requires (memory_load8_le(mem, 2076bv64) == 1bv8);
   free requires (memory_load8_le(mem, 2077bv64) == 0bv8);
   free requires (memory_load8_le(mem, 2078bv64) == 2bv8);
@@ -247,3 +252,4 @@ procedure main()
 }
 
 procedure malloc();
+  modifies Gamma_R16, Gamma_R17, R16, R17;
diff --git a/src/test/correct/basicfree/gcc_no_plt_no_pic/basicfree.expected b/src/test/correct/basicfree/gcc_no_plt_no_pic/basicfree.expected
@@ -1,12 +1,16 @@
 var Gamma_R0: bool;
 var Gamma_R1: bool;
+var Gamma_R16: bool;
+var Gamma_R17: bool;
 var Gamma_R29: bool;
 var Gamma_R30: bool;
 var Gamma_R31: bool;
 var Gamma_mem: [bv64]bool;
 var Gamma_stack: [bv64]bool;
 var R0: bv64;
 var R1: bv64;
+var R16: bv64;
+var R17: bv64;
 var R29: bv64;
 var R30: bv64;
 var R31: bv64;
@@ -68,9 +72,10 @@ procedure guarantee_reflexive();
   modifies mem, Gamma_mem;
 
 procedure #free();
+  modifies Gamma_R16, Gamma_R17, R16, R17;
 
 procedure main()
-  modifies Gamma_R0, Gamma_R1, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_mem, Gamma_stack, R0, R1, R29, R30, R31, mem, stack;
+  modifies Gamma_R0, Gamma_R1, Gamma_R16, Gamma_R17, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_mem, Gamma_stack, R0, R1, R16, R17, R29, R30, R31, mem, stack;
   free requires (memory_load8_le(mem, 2076bv64) == 1bv8);
   free requires (memory_load8_le(mem, 2077bv64) == 0bv8);
   free requires (memory_load8_le(mem, 2078bv64) == 2bv8);
@@ -247,3 +252,4 @@ procedure main()
 }
 
 procedure malloc();
+  modifies Gamma_R16, Gamma_R17, R16, R17;
diff --git a/src/test/correct/basicfree/gcc_pic/basicfree.expected b/src/test/correct/basicfree/gcc_pic/basicfree.expected
@@ -1,12 +1,16 @@
 var Gamma_R0: bool;
 var Gamma_R1: bool;
+var Gamma_R16: bool;
+var Gamma_R17: bool;
 var Gamma_R29: bool;
 var Gamma_R30: bool;
 var Gamma_R31: bool;
 var Gamma_mem: [bv64]bool;
 var Gamma_stack: [bv64]bool;
 var R0: bv64;
 var R1: bv64;
+var R16: bv64;
+var R17: bv64;
 var R29: bv64;
 var R30: bv64;
 var R31: bv64;
@@ -68,9 +72,10 @@ procedure guarantee_reflexive();
   modifies mem, Gamma_mem;
 
 procedure #free();
+  modifies Gamma_R16, Gamma_R17, R16, R17;
 
 procedure main()
-  modifies Gamma_R0, Gamma_R1, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_mem, Gamma_stack, R0, R1, R29, R30, R31, mem, stack;
+  modifies Gamma_R0, Gamma_R1, Gamma_R16, Gamma_R17, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_mem, Gamma_stack, R0, R1, R16, R17, R29, R30, R31, mem, stack;
   free requires (memory_load8_le(mem, 2076bv64) == 1bv8);
   free requires (memory_load8_le(mem, 2077bv64) == 0bv8);
   free requires (memory_load8_le(mem, 2078bv64) == 2bv8);
@@ -247,3 +252,4 @@ procedure main()
 }
 
 procedure malloc();
+  modifies Gamma_R16, Gamma_R17, R16, R17;
diff --git a/src/test/correct/function1/clang/function1.expected b/src/test/correct/function1/clang/function1.expected
@@ -1,5 +1,7 @@
 var Gamma_R0: bool;
 var Gamma_R1: bool;
+var Gamma_R16: bool;
+var Gamma_R17: bool;
 var Gamma_R2: bool;
 var Gamma_R29: bool;
 var Gamma_R30: bool;
@@ -10,6 +12,8 @@ var Gamma_mem: [bv64]bool;
 var Gamma_stack: [bv64]bool;
 var R0: bv64;
 var R1: bv64;
+var R16: bv64;
+var R17: bv64;
 var R2: bv64;
 var R29: bv64;
 var R30: bv64;
@@ -122,7 +126,7 @@ procedure get_two()
 }
 
 procedure main()
-  modifies Gamma_R0, Gamma_R1, Gamma_R2, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_R8, Gamma_R9, Gamma_mem, Gamma_stack, R0, R1, R2, R29, R30, R31, R8, R9, mem, stack;
+  modifies Gamma_R0, Gamma_R1, Gamma_R16, Gamma_R17, Gamma_R2, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_R8, Gamma_R9, Gamma_mem, Gamma_stack, R0, R1, R16, R17, R2, R29, R30, R31, R8, R9, mem, stack;
   free requires (memory_load8_le(mem, 2024bv64) == 1bv8);
   free requires (memory_load8_le(mem, 2025bv64) == 0bv8);
   free requires (memory_load8_le(mem, 2026bv64) == 2bv8);
@@ -241,3 +245,4 @@ procedure main()
 }
 
 procedure printf();
+  modifies Gamma_R16, Gamma_R17, R16, R17;
diff --git a/src/test/correct/function1/clang_O2/function1.expected b/src/test/correct/function1/clang_O2/function1.expected
@@ -2,6 +2,8 @@ var Gamma_R0: bool;
 var Gamma_R1: bool;
 var Gamma_R10: bool;
 var Gamma_R11: bool;
+var Gamma_R16: bool;
+var Gamma_R17: bool;
 var Gamma_R29: bool;
 var Gamma_R30: bool;
 var Gamma_R31: bool;
@@ -13,6 +15,8 @@ var R0: bv64;
 var R1: bv64;
 var R10: bv64;
 var R11: bv64;
+var R16: bv64;
+var R17: bv64;
 var R29: bv64;
 var R30: bv64;
 var R31: bv64;
@@ -81,7 +85,7 @@ procedure guarantee_reflexive();
   modifies mem, Gamma_mem;
 
 procedure main()
-  modifies Gamma_R0, Gamma_R1, Gamma_R10, Gamma_R11, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_R8, Gamma_R9, Gamma_mem, Gamma_stack, R0, R1, R10, R11, R29, R30, R31, R8, R9, mem, stack;
+  modifies Gamma_R0, Gamma_R1, Gamma_R10, Gamma_R11, Gamma_R16, Gamma_R17, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_R8, Gamma_R9, Gamma_mem, Gamma_stack, R0, R1, R10, R11, R16, R17, R29, R30, R31, R8, R9, mem, stack;
   free requires (memory_load8_le(mem, 1976bv64) == 1bv8);
   free requires (memory_load8_le(mem, 1977bv64) == 0bv8);
   free requires (memory_load8_le(mem, 1978bv64) == 2bv8);
@@ -194,3 +198,4 @@ procedure main()
 }
 
 procedure printf();
+  modifies Gamma_R16, Gamma_R17, R16, R17;
diff --git a/src/test/correct/function1/clang_no_plt_no_pic/function1.expected b/src/test/correct/function1/clang_no_plt_no_pic/function1.expected
@@ -1,5 +1,7 @@
 var Gamma_R0: bool;
 var Gamma_R1: bool;
+var Gamma_R16: bool;
+var Gamma_R17: bool;
 var Gamma_R2: bool;
 var Gamma_R29: bool;
 var Gamma_R30: bool;
@@ -10,6 +12,8 @@ var Gamma_mem: [bv64]bool;
 var Gamma_stack: [bv64]bool;
 var R0: bv64;
 var R1: bv64;
+var R16: bv64;
+var R17: bv64;
 var R2: bv64;
 var R29: bv64;
 var R30: bv64;
@@ -122,7 +126,7 @@ procedure get_two()
 }
 
 procedure main()
-  modifies Gamma_R0, Gamma_R1, Gamma_R2, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_R8, Gamma_R9, Gamma_mem, Gamma_stack, R0, R1, R2, R29, R30, R31, R8, R9, mem, stack;
+  modifies Gamma_R0, Gamma_R1, Gamma_R16, Gamma_R17, Gamma_R2, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_R8, Gamma_R9, Gamma_mem, Gamma_stack, R0, R1, R16, R17, R2, R29, R30, R31, R8, R9, mem, stack;
   free requires (memory_load8_le(mem, 2024bv64) == 1bv8);
   free requires (memory_load8_le(mem, 2025bv64) == 0bv8);
   free requires (memory_load8_le(mem, 2026bv64) == 2bv8);
@@ -241,3 +245,4 @@ procedure main()
 }
 
 procedure printf();
+  modifies Gamma_R16, Gamma_R17, R16, R17;
diff --git a/src/test/correct/function1/clang_pic/function1.expected b/src/test/correct/function1/clang_pic/function1.expected
@@ -1,5 +1,7 @@
 var Gamma_R0: bool;
 var Gamma_R1: bool;
+var Gamma_R16: bool;
+var Gamma_R17: bool;
 var Gamma_R2: bool;
 var Gamma_R29: bool;
 var Gamma_R30: bool;
@@ -10,6 +12,8 @@ var Gamma_mem: [bv64]bool;
 var Gamma_stack: [bv64]bool;
 var R0: bv64;
 var R1: bv64;
+var R16: bv64;
+var R17: bv64;
 var R2: bv64;
 var R29: bv64;
 var R30: bv64;
@@ -122,7 +126,7 @@ procedure get_two()
 }
 
 procedure main()
-  modifies Gamma_R0, Gamma_R1, Gamma_R2, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_R8, Gamma_R9, Gamma_mem, Gamma_stack, R0, R1, R2, R29, R30, R31, R8, R9, mem, stack;
+  modifies Gamma_R0, Gamma_R1, Gamma_R16, Gamma_R17, Gamma_R2, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_R8, Gamma_R9, Gamma_mem, Gamma_stack, R0, R1, R16, R17, R2, R29, R30, R31, R8, R9, mem, stack;
   free requires (memory_load8_le(mem, 2096bv64) == 1bv8);
   free requires (memory_load8_le(mem, 2097bv64) == 0bv8);
   free requires (memory_load8_le(mem, 2098bv64) == 2bv8);
@@ -259,3 +263,4 @@ procedure main()
 }
 
 procedure printf();
+  modifies Gamma_R16, Gamma_R17, R16, R17;
diff --git a/src/test/correct/function1/gcc/function1.expected b/src/test/correct/function1/gcc/function1.expected
@@ -1,5 +1,7 @@
 var Gamma_R0: bool;
 var Gamma_R1: bool;
+var Gamma_R16: bool;
+var Gamma_R17: bool;
 var Gamma_R2: bool;
 var Gamma_R29: bool;
 var Gamma_R30: bool;
@@ -8,6 +10,8 @@ var Gamma_mem: [bv64]bool;
 var Gamma_stack: [bv64]bool;
 var R0: bv64;
 var R1: bv64;
+var R16: bv64;
+var R17: bv64;
 var R2: bv64;
 var R29: bv64;
 var R30: bv64;
@@ -117,7 +121,7 @@ procedure get_two()
 }
 
 procedure main()
-  modifies Gamma_R0, Gamma_R1, Gamma_R2, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_mem, Gamma_stack, R0, R1, R2, R29, R30, R31, mem, stack;
+  modifies Gamma_R0, Gamma_R1, Gamma_R16, Gamma_R17, Gamma_R2, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_mem, Gamma_stack, R0, R1, R16, R17, R2, R29, R30, R31, mem, stack;
   free requires (memory_load8_le(mem, 2048bv64) == 1bv8);
   free requires (memory_load8_le(mem, 2049bv64) == 0bv8);
   free requires (memory_load8_le(mem, 2050bv64) == 2bv8);
@@ -310,3 +314,4 @@ procedure main()
 }
 
 procedure printf();
+  modifies Gamma_R16, Gamma_R17, R16, R17;
diff --git a/src/test/correct/function1/gcc_O2/function1.expected b/src/test/correct/function1/gcc_O2/function1.expected
@@ -1,5 +1,7 @@
 var Gamma_R0: bool;
 var Gamma_R1: bool;
+var Gamma_R16: bool;
+var Gamma_R17: bool;
 var Gamma_R2: bool;
 var Gamma_R29: bool;
 var Gamma_R3: bool;
@@ -9,6 +11,8 @@ var Gamma_mem: [bv64]bool;
 var Gamma_stack: [bv64]bool;
 var R0: bv64;
 var R1: bv64;
+var R16: bv64;
+var R17: bv64;
 var R2: bv64;
 var R29: bv64;
 var R3: bv64;
@@ -77,9 +81,10 @@ procedure guarantee_reflexive();
   modifies mem, Gamma_mem;
 
 procedure __printf_chk();
+  modifies Gamma_R16, Gamma_R17, R16, R17;
 
 procedure main()
-  modifies Gamma_R0, Gamma_R1, Gamma_R2, Gamma_R29, Gamma_R3, Gamma_R30, Gamma_R31, Gamma_mem, Gamma_stack, R0, R1, R2, R29, R3, R30, R31, mem, stack;
+  modifies Gamma_R0, Gamma_R1, Gamma_R16, Gamma_R17, Gamma_R2, Gamma_R29, Gamma_R3, Gamma_R30, Gamma_R31, Gamma_mem, Gamma_stack, R0, R1, R16, R17, R2, R29, R3, R30, R31, mem, stack;
   free requires (memory_load8_le(mem, 2048bv64) == 1bv8);
   free requires (memory_load8_le(mem, 2049bv64) == 0bv8);
   free requires (memory_load8_le(mem, 2050bv64) == 2bv8);