From c6a411fa41ce868ce522fc21ce9b1482e7c52638 Mon Sep 17 00:00:00 2001 From: l-kent Date: Fri, 13 Oct 2023 16:18:10 +1000 Subject: [PATCH] update expected files --- src/test/correct/basicfree/clang/basicfree.expected | 8 +++++++- .../basicfree/clang_no_plt_no_pic/basicfree.expected | 8 +++++++- .../correct/basicfree/clang_pic/basicfree.expected | 8 +++++++- src/test/correct/basicfree/gcc/basicfree.expected | 8 +++++++- .../basicfree/gcc_no_plt_no_pic/basicfree.expected | 8 +++++++- src/test/correct/basicfree/gcc_pic/basicfree.expected | 8 +++++++- src/test/correct/function1/clang/function1.expected | 7 ++++++- .../correct/function1/clang_O2/function1.expected | 7 ++++++- .../function1/clang_no_plt_no_pic/function1.expected | 7 ++++++- .../correct/function1/clang_pic/function1.expected | 7 ++++++- src/test/correct/function1/gcc/function1.expected | 7 ++++++- src/test/correct/function1/gcc_O2/function1.expected | 7 ++++++- .../function1/gcc_no_plt_no_pic/function1.expected | 7 ++++++- src/test/correct/function1/gcc_pic/function1.expected | 7 ++++++- .../indirect_call/clang/indirect_call.expected | 7 ++++++- .../indirect_call/clang_O2/indirect_call.expected | 7 ++++++- .../clang_no_plt_no_pic/indirect_call.expected | 7 ++++++- .../indirect_call/clang_pic/indirect_call.expected | 7 ++++++- .../correct/indirect_call/gcc/indirect_call.expected | 7 ++++++- .../indirect_call/gcc_O2/indirect_call.expected | 9 +++++++-- .../gcc_no_plt_no_pic/indirect_call.expected | 7 ++++++- .../indirect_call/gcc_pic/indirect_call.expected | 7 ++++++- src/test/correct/jumptable/gcc/jumptable.expected | 7 ++++++- src/test/correct/jumptable/gcc_pic/jumptable.expected | 7 ++++++- .../clang/malloc_with_local.expected | 9 ++++++++- .../clang_O2/malloc_with_local.expected | 7 ++++++- .../clang_no_plt_no_pic/malloc_with_local.expected | 9 ++++++++- .../clang_pic/malloc_with_local.expected | 9 ++++++++- .../malloc_with_local/gcc/malloc_with_local.expected | 9 ++++++++- .../gcc_O2/malloc_with_local.expected | 7 ++++++- .../gcc_no_plt_no_pic/malloc_with_local.expected | 9 ++++++++- .../gcc_pic/malloc_with_local.expected | 9 ++++++++- .../clang/malloc_with_local2.expected | 9 ++++++++- .../clang_O2/malloc_with_local2.expected | 7 ++++++- .../clang_no_plt_no_pic/malloc_with_local2.expected | 9 ++++++++- .../clang_pic/malloc_with_local2.expected | 9 ++++++++- .../gcc/malloc_with_local2.expected | 9 ++++++++- .../gcc_O2/malloc_with_local2.expected | 7 ++++++- .../gcc_no_plt_no_pic/malloc_with_local2.expected | 9 ++++++++- .../gcc_pic/malloc_with_local2.expected | 9 ++++++++- .../clang/malloc_with_local3.expected | 11 +++++++++-- .../clang_O2/malloc_with_local3.expected | 7 ++++++- .../clang_no_plt_no_pic/malloc_with_local3.expected | 11 +++++++++-- .../clang_pic/malloc_with_local3.expected | 11 +++++++++-- .../gcc/malloc_with_local3.expected | 11 +++++++++-- .../gcc_O2/malloc_with_local3.expected | 11 +++++++++-- .../gcc_no_plt_no_pic/malloc_with_local3.expected | 11 +++++++++-- .../gcc_pic/malloc_with_local3.expected | 11 +++++++++-- .../correct/multi_malloc/clang/multi_malloc.expected | 9 ++++++++- .../multi_malloc/clang_O2/multi_malloc.expected | 7 ++++++- .../clang_no_plt_no_pic/multi_malloc.expected | 9 ++++++++- .../multi_malloc/clang_pic/multi_malloc.expected | 9 ++++++++- .../correct/multi_malloc/gcc/multi_malloc.expected | 9 ++++++++- .../correct/multi_malloc/gcc_O2/multi_malloc.expected | 7 ++++++- .../gcc_no_plt_no_pic/multi_malloc.expected | 9 ++++++++- .../multi_malloc/gcc_pic/multi_malloc.expected | 9 ++++++++- src/test/correct/syscall/clang/syscall.expected | 7 ++++++- .../syscall/clang_no_plt_no_pic/syscall.expected | 7 ++++++- src/test/correct/syscall/clang_pic/syscall.expected | 7 ++++++- src/test/correct/syscall/gcc/syscall.expected | 7 ++++++- src/test/correct/syscall/gcc_O2/syscall.expected | 5 +++++ .../syscall/gcc_no_plt_no_pic/syscall.expected | 7 ++++++- src/test/correct/syscall/gcc_pic/syscall.expected | 7 ++++++- 63 files changed, 441 insertions(+), 70 deletions(-) diff --git a/src/test/correct/basicfree/clang/basicfree.expected b/src/test/correct/basicfree/clang/basicfree.expected index 87c5c3d1f..89c314680 100644 --- 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 index b5eba12b4..617fb7185 100644 --- 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 index b5eba12b4..617fb7185 100644 --- 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 index 010eedb0c..3b441de64 100644 --- a/src/test/correct/basicfree/gcc/basicfree.expected +++ b/src/test/correct/basicfree/gcc/basicfree.expected @@ -1,5 +1,7 @@ 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; @@ -7,6 +9,8 @@ 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 index 3adf39eea..cb9aad643 100644 --- 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,5 +1,7 @@ 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; @@ -7,6 +9,8 @@ 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 index 3adf39eea..cb9aad643 100644 --- a/src/test/correct/basicfree/gcc_pic/basicfree.expected +++ b/src/test/correct/basicfree/gcc_pic/basicfree.expected @@ -1,5 +1,7 @@ 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; @@ -7,6 +9,8 @@ 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 index 2e7f57fcb..bf51edd95 100644 --- 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 index 3e52d5cda..d99cfb6ee 100644 --- 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 index 503457e11..b42878682 100644 --- 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 index b52d14a26..7fa9fba13 100644 --- 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 index 2cb4f37e0..8316af7bd 100644 --- 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 index dc3a201a1..2c1b48b82 100644 --- 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); diff --git a/src/test/correct/function1/gcc_no_plt_no_pic/function1.expected b/src/test/correct/function1/gcc_no_plt_no_pic/function1.expected index bd57a994a..a5f223f69 100644 --- a/src/test/correct/function1/gcc_no_plt_no_pic/function1.expected +++ b/src/test/correct/function1/gcc_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; @@ -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_pic/function1.expected b/src/test/correct/function1/gcc_pic/function1.expected index 3bb9f707b..aa8e4e0bd 100644 --- a/src/test/correct/function1/gcc_pic/function1.expected +++ b/src/test/correct/function1/gcc_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; @@ -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, 2112bv64) == 1bv8); free requires (memory_load8_le(mem, 2113bv64) == 0bv8); free requires (memory_load8_le(mem, 2114bv64) == 2bv8); @@ -326,3 +330,4 @@ procedure main() } procedure printf(); + modifies Gamma_R16, Gamma_R17, R16, R17; diff --git a/src/test/correct/indirect_call/clang/indirect_call.expected b/src/test/correct/indirect_call/clang/indirect_call.expected index 49128f199..b5c23c12e 100644 --- a/src/test/correct/indirect_call/clang/indirect_call.expected +++ b/src/test/correct/indirect_call/clang/indirect_call.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; @@ -6,6 +8,8 @@ var Gamma_R8: 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; @@ -73,7 +77,7 @@ procedure guarantee_reflexive(); modifies mem, Gamma_mem; procedure main() - modifies Gamma_R0, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_R8, Gamma_stack, R0, R29, R30, R31, R8, stack; + modifies Gamma_R0, Gamma_R16, Gamma_R17, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_R8, Gamma_stack, R0, R16, R17, R29, R30, R31, R8, stack; free requires (memory_load8_le(mem, 1996bv64) == 1bv8); free requires (memory_load8_le(mem, 1997bv64) == 0bv8); free requires (memory_load8_le(mem, 1998bv64) == 2bv8); @@ -228,3 +232,4 @@ procedure main() } procedure printf(); + modifies Gamma_R16, Gamma_R17, R16, R17; diff --git a/src/test/correct/indirect_call/clang_O2/indirect_call.expected b/src/test/correct/indirect_call/clang_O2/indirect_call.expected index d5bed1b45..0022a046e 100644 --- a/src/test/correct/indirect_call/clang_O2/indirect_call.expected +++ b/src/test/correct/indirect_call/clang_O2/indirect_call.expected @@ -1,10 +1,14 @@ var Gamma_R0: 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 R16: bv64; +var R17: bv64; var R29: bv64; var R30: bv64; var R31: bv64; @@ -54,7 +58,7 @@ procedure guarantee_reflexive(); modifies mem, Gamma_mem; procedure main() - modifies Gamma_R0, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_stack, R0, R29, R30, R31, stack; + modifies Gamma_R0, Gamma_R16, Gamma_R17, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_stack, R0, R16, R17, R29, R30, R31, stack; free requires (memory_load8_le(mem, 1952bv64) == 1bv8); free requires (memory_load8_le(mem, 1953bv64) == 0bv8); free requires (memory_load8_le(mem, 1954bv64) == 2bv8); @@ -198,3 +202,4 @@ procedure main() } procedure puts(); + modifies Gamma_R16, Gamma_R17, R16, R17; diff --git a/src/test/correct/indirect_call/clang_no_plt_no_pic/indirect_call.expected b/src/test/correct/indirect_call/clang_no_plt_no_pic/indirect_call.expected index 99adfe74a..a5bc1bece 100644 --- a/src/test/correct/indirect_call/clang_no_plt_no_pic/indirect_call.expected +++ b/src/test/correct/indirect_call/clang_no_plt_no_pic/indirect_call.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; @@ -6,6 +8,8 @@ var Gamma_R8: 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; @@ -73,7 +77,7 @@ procedure guarantee_reflexive(); modifies mem, Gamma_mem; procedure main() - modifies Gamma_R0, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_R8, Gamma_stack, R0, R29, R30, R31, R8, stack; + modifies Gamma_R0, Gamma_R16, Gamma_R17, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_R8, Gamma_stack, R0, R16, R17, R29, R30, R31, R8, stack; free requires (memory_load8_le(mem, 1996bv64) == 1bv8); free requires (memory_load8_le(mem, 1997bv64) == 0bv8); free requires (memory_load8_le(mem, 1998bv64) == 2bv8); @@ -228,3 +232,4 @@ procedure main() } procedure printf(); + modifies Gamma_R16, Gamma_R17, R16, R17; diff --git a/src/test/correct/indirect_call/clang_pic/indirect_call.expected b/src/test/correct/indirect_call/clang_pic/indirect_call.expected index 176415164..1e58c1ce2 100644 --- a/src/test/correct/indirect_call/clang_pic/indirect_call.expected +++ b/src/test/correct/indirect_call/clang_pic/indirect_call.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; @@ -6,6 +8,8 @@ var Gamma_R8: 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; @@ -77,7 +81,7 @@ procedure guarantee_reflexive(); modifies mem, Gamma_mem; procedure main() - modifies Gamma_R0, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_R8, Gamma_stack, R0, R29, R30, R31, R8, stack; + modifies Gamma_R0, Gamma_R16, Gamma_R17, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_R8, Gamma_stack, R0, R16, R17, R29, R30, R31, R8, stack; free requires (memory_load8_le(mem, 2060bv64) == 1bv8); free requires (memory_load8_le(mem, 2061bv64) == 0bv8); free requires (memory_load8_le(mem, 2062bv64) == 2bv8); @@ -240,3 +244,4 @@ procedure main() } procedure printf(); + modifies Gamma_R16, Gamma_R17, R16, R17; diff --git a/src/test/correct/indirect_call/gcc/indirect_call.expected b/src/test/correct/indirect_call/gcc/indirect_call.expected index 14b9c6fd8..9af8b7ff5 100644 --- a/src/test/correct/indirect_call/gcc/indirect_call.expected +++ b/src/test/correct/indirect_call/gcc/indirect_call.expected @@ -1,10 +1,14 @@ var Gamma_R0: 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 R16: bv64; +var R17: bv64; var R29: bv64; var R30: bv64; var R31: bv64; @@ -54,7 +58,7 @@ procedure guarantee_reflexive(); modifies mem, Gamma_mem; procedure main() - modifies Gamma_R0, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_stack, R0, R29, R30, R31, stack; + modifies Gamma_R0, Gamma_R16, Gamma_R17, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_stack, R0, R16, R17, R29, R30, R31, stack; free requires (memory_load8_le(mem, 1984bv64) == 1bv8); free requires (memory_load8_le(mem, 1985bv64) == 0bv8); free requires (memory_load8_le(mem, 1986bv64) == 2bv8); @@ -271,3 +275,4 @@ procedure main() } procedure puts(); + modifies Gamma_R16, Gamma_R17, R16, R17; diff --git a/src/test/correct/indirect_call/gcc_O2/indirect_call.expected b/src/test/correct/indirect_call/gcc_O2/indirect_call.expected index b1ed1ef3b..d325fb378 100644 --- a/src/test/correct/indirect_call/gcc_O2/indirect_call.expected +++ b/src/test/correct/indirect_call/gcc_O2/indirect_call.expected @@ -1,10 +1,14 @@ var Gamma_R0: 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 R16: bv64; +var R17: bv64; var R29: bv64; var R30: bv64; var R31: bv64; @@ -54,7 +58,7 @@ procedure guarantee_reflexive(); modifies mem, Gamma_mem; procedure greet() - modifies Gamma_R0, R0; + modifies Gamma_R0, Gamma_R16, Gamma_R17, R0, R16, R17; { lgreet: R0, Gamma_R0 := 0bv64, true; @@ -65,7 +69,7 @@ procedure greet() } procedure main() - modifies Gamma_R0, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_stack, R0, R29, R30, R31, stack; + modifies Gamma_R0, Gamma_R16, Gamma_R17, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_stack, R0, R16, R17, R29, R30, R31, stack; free requires (memory_load8_le(mem, 1984bv64) == 1bv8); free requires (memory_load8_le(mem, 1985bv64) == 0bv8); free requires (memory_load8_le(mem, 1986bv64) == 2bv8); @@ -277,3 +281,4 @@ procedure main() } procedure puts(); + modifies Gamma_R16, Gamma_R17, R16, R17; diff --git a/src/test/correct/indirect_call/gcc_no_plt_no_pic/indirect_call.expected b/src/test/correct/indirect_call/gcc_no_plt_no_pic/indirect_call.expected index 335910e44..cfb10d986 100644 --- a/src/test/correct/indirect_call/gcc_no_plt_no_pic/indirect_call.expected +++ b/src/test/correct/indirect_call/gcc_no_plt_no_pic/indirect_call.expected @@ -1,10 +1,14 @@ var Gamma_R0: 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 R16: bv64; +var R17: bv64; var R29: bv64; var R30: bv64; var R31: bv64; @@ -54,7 +58,7 @@ procedure guarantee_reflexive(); modifies mem, Gamma_mem; procedure main() - modifies Gamma_R0, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_stack, R0, R29, R30, R31, stack; + modifies Gamma_R0, Gamma_R16, Gamma_R17, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_stack, R0, R16, R17, R29, R30, R31, stack; free requires (memory_load8_le(mem, 1984bv64) == 1bv8); free requires (memory_load8_le(mem, 1985bv64) == 0bv8); free requires (memory_load8_le(mem, 1986bv64) == 2bv8); @@ -271,3 +275,4 @@ procedure main() } procedure puts(); + modifies Gamma_R16, Gamma_R17, R16, R17; diff --git a/src/test/correct/indirect_call/gcc_pic/indirect_call.expected b/src/test/correct/indirect_call/gcc_pic/indirect_call.expected index 3a0617538..48ffa6625 100644 --- a/src/test/correct/indirect_call/gcc_pic/indirect_call.expected +++ b/src/test/correct/indirect_call/gcc_pic/indirect_call.expected @@ -1,10 +1,14 @@ var Gamma_R0: 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 R16: bv64; +var R17: bv64; var R29: bv64; var R30: bv64; var R31: bv64; @@ -58,7 +62,7 @@ procedure guarantee_reflexive(); modifies mem, Gamma_mem; procedure main() - modifies Gamma_R0, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_stack, R0, R29, R30, R31, stack; + modifies Gamma_R0, Gamma_R16, Gamma_R17, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_stack, R0, R16, R17, R29, R30, R31, 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); @@ -283,3 +287,4 @@ procedure main() } procedure puts(); + modifies Gamma_R16, Gamma_R17, R16, R17; diff --git a/src/test/correct/jumptable/gcc/jumptable.expected b/src/test/correct/jumptable/gcc/jumptable.expected index 16a42e49a..9e8e26baf 100644 --- a/src/test/correct/jumptable/gcc/jumptable.expected +++ b/src/test/correct/jumptable/gcc/jumptable.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; @@ -83,9 +87,10 @@ procedure guarantee_reflexive(); modifies mem, Gamma_mem; procedure __stack_chk_fail(); + 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_stack, R0, R1, R2, R29, R3, R30, R31, stack; + modifies Gamma_R0, Gamma_R1, Gamma_R16, Gamma_R17, Gamma_R2, Gamma_R29, Gamma_R3, Gamma_R30, Gamma_R31, Gamma_stack, R0, R1, R16, R17, R2, R29, R3, R30, R31, stack; free requires (memory_load8_le(mem, 2404bv64) == 1bv8); free requires (memory_load8_le(mem, 2405bv64) == 0bv8); free requires (memory_load8_le(mem, 2406bv64) == 2bv8); diff --git a/src/test/correct/jumptable/gcc_pic/jumptable.expected b/src/test/correct/jumptable/gcc_pic/jumptable.expected index 258842523..eb451873d 100644 --- a/src/test/correct/jumptable/gcc_pic/jumptable.expected +++ b/src/test/correct/jumptable/gcc_pic/jumptable.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; @@ -83,9 +87,10 @@ procedure guarantee_reflexive(); modifies mem, Gamma_mem; procedure __stack_chk_fail(); + 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_stack, R0, R1, R2, R29, R3, R30, R31, stack; + modifies Gamma_R0, Gamma_R1, Gamma_R16, Gamma_R17, Gamma_R2, Gamma_R29, Gamma_R3, Gamma_R30, Gamma_R31, Gamma_stack, R0, R1, R16, R17, R2, R29, R3, R30, R31, stack; free requires (memory_load8_le(mem, 2404bv64) == 1bv8); free requires (memory_load8_le(mem, 2405bv64) == 0bv8); free requires (memory_load8_le(mem, 2406bv64) == 2bv8); diff --git a/src/test/correct/malloc_with_local/clang/malloc_with_local.expected b/src/test/correct/malloc_with_local/clang/malloc_with_local.expected index 65166f581..a6e6bb79a 100644 --- a/src/test/correct/malloc_with_local/clang/malloc_with_local.expected +++ b/src/test/correct/malloc_with_local/clang/malloc_with_local.expected @@ -1,5 +1,7 @@ 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; @@ -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 R29: bv64; var R30: bv64; var R31: bv64; @@ -94,9 +98,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_R8, Gamma_R9, Gamma_mem, Gamma_stack, R0, R1, R29, R30, R31, R8, R9, mem, stack; + modifies Gamma_R0, Gamma_R1, Gamma_R16, Gamma_R17, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_R8, Gamma_R9, Gamma_mem, Gamma_stack, R0, R1, R16, R17, R29, R30, R31, R8, R9, mem, stack; free requires (memory_load8_le(mem, 2256bv64) == 1bv8); free requires (memory_load8_le(mem, 2257bv64) == 0bv8); free requires (memory_load8_le(mem, 2258bv64) == 2bv8); @@ -309,5 +314,7 @@ procedure main() } procedure malloc(); + modifies Gamma_R16, Gamma_R17, R16, R17; procedure printf(); + modifies Gamma_R16, Gamma_R17, R16, R17; diff --git a/src/test/correct/malloc_with_local/clang_O2/malloc_with_local.expected b/src/test/correct/malloc_with_local/clang_O2/malloc_with_local.expected index 485223c2f..c126de600 100644 --- a/src/test/correct/malloc_with_local/clang_O2/malloc_with_local.expected +++ b/src/test/correct/malloc_with_local/clang_O2/malloc_with_local.expected @@ -1,5 +1,7 @@ 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; @@ -7,6 +9,8 @@ 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; @@ -56,7 +60,7 @@ procedure guarantee_reflexive(); modifies mem, Gamma_mem; procedure main() - modifies Gamma_R0, Gamma_R1, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_stack, R0, R1, R29, R30, R31, stack; + modifies Gamma_R0, Gamma_R1, Gamma_R16, Gamma_R17, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_stack, R0, R1, R16, R17, R29, R30, R31, stack; free requires (memory_load8_le(mem, 1964bv64) == 1bv8); free requires (memory_load8_le(mem, 1965bv64) == 0bv8); free requires (memory_load8_le(mem, 1966bv64) == 2bv8); @@ -227,3 +231,4 @@ procedure main() } procedure printf(); + modifies Gamma_R16, Gamma_R17, R16, R17; diff --git a/src/test/correct/malloc_with_local/clang_no_plt_no_pic/malloc_with_local.expected b/src/test/correct/malloc_with_local/clang_no_plt_no_pic/malloc_with_local.expected index 3e3920d2b..2a2a64139 100644 --- a/src/test/correct/malloc_with_local/clang_no_plt_no_pic/malloc_with_local.expected +++ b/src/test/correct/malloc_with_local/clang_no_plt_no_pic/malloc_with_local.expected @@ -1,5 +1,7 @@ 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; @@ -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 R29: bv64; var R30: bv64; var R31: bv64; @@ -94,9 +98,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_R8, Gamma_R9, Gamma_mem, Gamma_stack, R0, R1, R29, R30, R31, R8, R9, mem, stack; + modifies Gamma_R0, Gamma_R1, Gamma_R16, Gamma_R17, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_R8, Gamma_R9, Gamma_mem, Gamma_stack, R0, R1, R16, R17, R29, R30, R31, R8, R9, mem, stack; free requires (memory_load8_le(mem, 2256bv64) == 1bv8); free requires (memory_load8_le(mem, 2257bv64) == 0bv8); free requires (memory_load8_le(mem, 2258bv64) == 2bv8); @@ -309,5 +314,7 @@ procedure main() } procedure malloc(); + modifies Gamma_R16, Gamma_R17, R16, R17; procedure printf(); + modifies Gamma_R16, Gamma_R17, R16, R17; diff --git a/src/test/correct/malloc_with_local/clang_pic/malloc_with_local.expected b/src/test/correct/malloc_with_local/clang_pic/malloc_with_local.expected index 3e3920d2b..2a2a64139 100644 --- a/src/test/correct/malloc_with_local/clang_pic/malloc_with_local.expected +++ b/src/test/correct/malloc_with_local/clang_pic/malloc_with_local.expected @@ -1,5 +1,7 @@ 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; @@ -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 R29: bv64; var R30: bv64; var R31: bv64; @@ -94,9 +98,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_R8, Gamma_R9, Gamma_mem, Gamma_stack, R0, R1, R29, R30, R31, R8, R9, mem, stack; + modifies Gamma_R0, Gamma_R1, Gamma_R16, Gamma_R17, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_R8, Gamma_R9, Gamma_mem, Gamma_stack, R0, R1, R16, R17, R29, R30, R31, R8, R9, mem, stack; free requires (memory_load8_le(mem, 2256bv64) == 1bv8); free requires (memory_load8_le(mem, 2257bv64) == 0bv8); free requires (memory_load8_le(mem, 2258bv64) == 2bv8); @@ -309,5 +314,7 @@ procedure main() } procedure malloc(); + modifies Gamma_R16, Gamma_R17, R16, R17; procedure printf(); + modifies Gamma_R16, Gamma_R17, R16, R17; diff --git a/src/test/correct/malloc_with_local/gcc/malloc_with_local.expected b/src/test/correct/malloc_with_local/gcc/malloc_with_local.expected index 7614b458e..7aa8c91eb 100644 --- a/src/test/correct/malloc_with_local/gcc/malloc_with_local.expected +++ b/src/test/correct/malloc_with_local/gcc/malloc_with_local.expected @@ -1,5 +1,7 @@ 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; @@ -7,6 +9,8 @@ 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; @@ -90,9 +94,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, 2248bv64) == 1bv8); free requires (memory_load8_le(mem, 2249bv64) == 0bv8); free requires (memory_load8_le(mem, 2250bv64) == 2bv8); @@ -392,5 +397,7 @@ procedure main() } procedure malloc(); + modifies Gamma_R16, Gamma_R17, R16, R17; procedure printf(); + modifies Gamma_R16, Gamma_R17, R16, R17; diff --git a/src/test/correct/malloc_with_local/gcc_O2/malloc_with_local.expected b/src/test/correct/malloc_with_local/gcc_O2/malloc_with_local.expected index e1320ef06..837ae23ba 100644 --- a/src/test/correct/malloc_with_local/gcc_O2/malloc_with_local.expected +++ b/src/test/correct/malloc_with_local/gcc_O2/malloc_with_local.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; @@ -58,9 +62,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_R30, Gamma_R31, Gamma_stack, R0, R1, R2, R29, R30, R31, stack; + modifies Gamma_R0, Gamma_R1, Gamma_R16, Gamma_R17, Gamma_R2, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_stack, R0, R1, R16, R17, R2, R29, R30, R31, stack; free requires (memory_load8_le(mem, 2088bv64) == 1bv8); free requires (memory_load8_le(mem, 2089bv64) == 0bv8); free requires (memory_load8_le(mem, 2090bv64) == 2bv8); diff --git a/src/test/correct/malloc_with_local/gcc_no_plt_no_pic/malloc_with_local.expected b/src/test/correct/malloc_with_local/gcc_no_plt_no_pic/malloc_with_local.expected index 2e837d017..ab464f48c 100644 --- a/src/test/correct/malloc_with_local/gcc_no_plt_no_pic/malloc_with_local.expected +++ b/src/test/correct/malloc_with_local/gcc_no_plt_no_pic/malloc_with_local.expected @@ -1,5 +1,7 @@ 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; @@ -7,6 +9,8 @@ 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; @@ -90,9 +94,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, 2248bv64) == 1bv8); free requires (memory_load8_le(mem, 2249bv64) == 0bv8); free requires (memory_load8_le(mem, 2250bv64) == 2bv8); @@ -392,5 +397,7 @@ procedure main() } procedure malloc(); + modifies Gamma_R16, Gamma_R17, R16, R17; procedure printf(); + modifies Gamma_R16, Gamma_R17, R16, R17; diff --git a/src/test/correct/malloc_with_local/gcc_pic/malloc_with_local.expected b/src/test/correct/malloc_with_local/gcc_pic/malloc_with_local.expected index 2e837d017..ab464f48c 100644 --- a/src/test/correct/malloc_with_local/gcc_pic/malloc_with_local.expected +++ b/src/test/correct/malloc_with_local/gcc_pic/malloc_with_local.expected @@ -1,5 +1,7 @@ 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; @@ -7,6 +9,8 @@ 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; @@ -90,9 +94,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, 2248bv64) == 1bv8); free requires (memory_load8_le(mem, 2249bv64) == 0bv8); free requires (memory_load8_le(mem, 2250bv64) == 2bv8); @@ -392,5 +397,7 @@ procedure main() } procedure malloc(); + modifies Gamma_R16, Gamma_R17, R16, R17; procedure printf(); + modifies Gamma_R16, Gamma_R17, R16, R17; diff --git a/src/test/correct/malloc_with_local2/clang/malloc_with_local2.expected b/src/test/correct/malloc_with_local2/clang/malloc_with_local2.expected index f8123d14f..9fcbe894f 100644 --- a/src/test/correct/malloc_with_local2/clang/malloc_with_local2.expected +++ b/src/test/correct/malloc_with_local2/clang/malloc_with_local2.expected @@ -1,5 +1,7 @@ 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; @@ -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 R29: bv64; var R30: bv64; var R31: bv64; @@ -94,9 +98,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_R8, Gamma_R9, Gamma_mem, Gamma_stack, R0, R1, R29, R30, R31, R8, R9, mem, stack; + modifies Gamma_R0, Gamma_R1, Gamma_R16, Gamma_R17, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_R8, Gamma_R9, Gamma_mem, Gamma_stack, R0, R1, R16, R17, R29, R30, R31, R8, R9, mem, stack; free requires (memory_load8_le(mem, 2292bv64) == 1bv8); free requires (memory_load8_le(mem, 2293bv64) == 0bv8); free requires (memory_load8_le(mem, 2294bv64) == 2bv8); @@ -321,5 +326,7 @@ procedure main() } procedure malloc(); + modifies Gamma_R16, Gamma_R17, R16, R17; procedure printf(); + modifies Gamma_R16, Gamma_R17, R16, R17; diff --git a/src/test/correct/malloc_with_local2/clang_O2/malloc_with_local2.expected b/src/test/correct/malloc_with_local2/clang_O2/malloc_with_local2.expected index 485223c2f..c126de600 100644 --- a/src/test/correct/malloc_with_local2/clang_O2/malloc_with_local2.expected +++ b/src/test/correct/malloc_with_local2/clang_O2/malloc_with_local2.expected @@ -1,5 +1,7 @@ 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; @@ -7,6 +9,8 @@ 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; @@ -56,7 +60,7 @@ procedure guarantee_reflexive(); modifies mem, Gamma_mem; procedure main() - modifies Gamma_R0, Gamma_R1, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_stack, R0, R1, R29, R30, R31, stack; + modifies Gamma_R0, Gamma_R1, Gamma_R16, Gamma_R17, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_stack, R0, R1, R16, R17, R29, R30, R31, stack; free requires (memory_load8_le(mem, 1964bv64) == 1bv8); free requires (memory_load8_le(mem, 1965bv64) == 0bv8); free requires (memory_load8_le(mem, 1966bv64) == 2bv8); @@ -227,3 +231,4 @@ procedure main() } procedure printf(); + modifies Gamma_R16, Gamma_R17, R16, R17; diff --git a/src/test/correct/malloc_with_local2/clang_no_plt_no_pic/malloc_with_local2.expected b/src/test/correct/malloc_with_local2/clang_no_plt_no_pic/malloc_with_local2.expected index ef7a30a03..1f2c68000 100644 --- a/src/test/correct/malloc_with_local2/clang_no_plt_no_pic/malloc_with_local2.expected +++ b/src/test/correct/malloc_with_local2/clang_no_plt_no_pic/malloc_with_local2.expected @@ -1,5 +1,7 @@ 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; @@ -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 R29: bv64; var R30: bv64; var R31: bv64; @@ -94,9 +98,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_R8, Gamma_R9, Gamma_mem, Gamma_stack, R0, R1, R29, R30, R31, R8, R9, mem, stack; + modifies Gamma_R0, Gamma_R1, Gamma_R16, Gamma_R17, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_R8, Gamma_R9, Gamma_mem, Gamma_stack, R0, R1, R16, R17, R29, R30, R31, R8, R9, mem, stack; free requires (memory_load8_le(mem, 2292bv64) == 1bv8); free requires (memory_load8_le(mem, 2293bv64) == 0bv8); free requires (memory_load8_le(mem, 2294bv64) == 2bv8); @@ -321,5 +326,7 @@ procedure main() } procedure malloc(); + modifies Gamma_R16, Gamma_R17, R16, R17; procedure printf(); + modifies Gamma_R16, Gamma_R17, R16, R17; diff --git a/src/test/correct/malloc_with_local2/clang_pic/malloc_with_local2.expected b/src/test/correct/malloc_with_local2/clang_pic/malloc_with_local2.expected index ef7a30a03..1f2c68000 100644 --- a/src/test/correct/malloc_with_local2/clang_pic/malloc_with_local2.expected +++ b/src/test/correct/malloc_with_local2/clang_pic/malloc_with_local2.expected @@ -1,5 +1,7 @@ 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; @@ -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 R29: bv64; var R30: bv64; var R31: bv64; @@ -94,9 +98,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_R8, Gamma_R9, Gamma_mem, Gamma_stack, R0, R1, R29, R30, R31, R8, R9, mem, stack; + modifies Gamma_R0, Gamma_R1, Gamma_R16, Gamma_R17, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_R8, Gamma_R9, Gamma_mem, Gamma_stack, R0, R1, R16, R17, R29, R30, R31, R8, R9, mem, stack; free requires (memory_load8_le(mem, 2292bv64) == 1bv8); free requires (memory_load8_le(mem, 2293bv64) == 0bv8); free requires (memory_load8_le(mem, 2294bv64) == 2bv8); @@ -321,5 +326,7 @@ procedure main() } procedure malloc(); + modifies Gamma_R16, Gamma_R17, R16, R17; procedure printf(); + modifies Gamma_R16, Gamma_R17, R16, R17; diff --git a/src/test/correct/malloc_with_local2/gcc/malloc_with_local2.expected b/src/test/correct/malloc_with_local2/gcc/malloc_with_local2.expected index 68244ac00..28dd8b449 100644 --- a/src/test/correct/malloc_with_local2/gcc/malloc_with_local2.expected +++ b/src/test/correct/malloc_with_local2/gcc/malloc_with_local2.expected @@ -1,5 +1,7 @@ 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; @@ -7,6 +9,8 @@ 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; @@ -90,9 +94,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, 2272bv64) == 1bv8); free requires (memory_load8_le(mem, 2273bv64) == 0bv8); free requires (memory_load8_le(mem, 2274bv64) == 2bv8); @@ -402,5 +407,7 @@ procedure main() } procedure malloc(); + modifies Gamma_R16, Gamma_R17, R16, R17; procedure printf(); + modifies Gamma_R16, Gamma_R17, R16, R17; diff --git a/src/test/correct/malloc_with_local2/gcc_O2/malloc_with_local2.expected b/src/test/correct/malloc_with_local2/gcc_O2/malloc_with_local2.expected index e1320ef06..837ae23ba 100644 --- a/src/test/correct/malloc_with_local2/gcc_O2/malloc_with_local2.expected +++ b/src/test/correct/malloc_with_local2/gcc_O2/malloc_with_local2.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; @@ -58,9 +62,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_R30, Gamma_R31, Gamma_stack, R0, R1, R2, R29, R30, R31, stack; + modifies Gamma_R0, Gamma_R1, Gamma_R16, Gamma_R17, Gamma_R2, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_stack, R0, R1, R16, R17, R2, R29, R30, R31, stack; free requires (memory_load8_le(mem, 2088bv64) == 1bv8); free requires (memory_load8_le(mem, 2089bv64) == 0bv8); free requires (memory_load8_le(mem, 2090bv64) == 2bv8); diff --git a/src/test/correct/malloc_with_local2/gcc_no_plt_no_pic/malloc_with_local2.expected b/src/test/correct/malloc_with_local2/gcc_no_plt_no_pic/malloc_with_local2.expected index e581619be..36370ecdc 100644 --- a/src/test/correct/malloc_with_local2/gcc_no_plt_no_pic/malloc_with_local2.expected +++ b/src/test/correct/malloc_with_local2/gcc_no_plt_no_pic/malloc_with_local2.expected @@ -1,5 +1,7 @@ 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; @@ -7,6 +9,8 @@ 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; @@ -90,9 +94,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, 2272bv64) == 1bv8); free requires (memory_load8_le(mem, 2273bv64) == 0bv8); free requires (memory_load8_le(mem, 2274bv64) == 2bv8); @@ -402,5 +407,7 @@ procedure main() } procedure malloc(); + modifies Gamma_R16, Gamma_R17, R16, R17; procedure printf(); + modifies Gamma_R16, Gamma_R17, R16, R17; diff --git a/src/test/correct/malloc_with_local2/gcc_pic/malloc_with_local2.expected b/src/test/correct/malloc_with_local2/gcc_pic/malloc_with_local2.expected index e581619be..36370ecdc 100644 --- a/src/test/correct/malloc_with_local2/gcc_pic/malloc_with_local2.expected +++ b/src/test/correct/malloc_with_local2/gcc_pic/malloc_with_local2.expected @@ -1,5 +1,7 @@ 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; @@ -7,6 +9,8 @@ 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; @@ -90,9 +94,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, 2272bv64) == 1bv8); free requires (memory_load8_le(mem, 2273bv64) == 0bv8); free requires (memory_load8_le(mem, 2274bv64) == 2bv8); @@ -402,5 +407,7 @@ procedure main() } procedure malloc(); + modifies Gamma_R16, Gamma_R17, R16, R17; procedure printf(); + modifies Gamma_R16, Gamma_R17, R16, R17; diff --git a/src/test/correct/malloc_with_local3/clang/malloc_with_local3.expected b/src/test/correct/malloc_with_local3/clang/malloc_with_local3.expected index 692555c9a..150eb10aa 100644 --- a/src/test/correct/malloc_with_local3/clang/malloc_with_local3.expected +++ b/src/test/correct/malloc_with_local3/clang/malloc_with_local3.expected @@ -1,5 +1,7 @@ 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; @@ -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 R29: bv64; var R30: bv64; var R31: bv64; @@ -95,9 +99,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_R8, Gamma_R9, Gamma_mem, Gamma_stack, R0, R1, R29, R30, R31, R8, R9, mem, stack; + modifies Gamma_R0, Gamma_R1, Gamma_R16, Gamma_R17, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_R8, Gamma_R9, Gamma_mem, Gamma_stack, R0, R1, R16, R17, R29, R30, R31, R8, R9, mem, stack; free requires (memory_load8_le(mem, 2344bv64) == 1bv8); free requires (memory_load8_le(mem, 2345bv64) == 0bv8); free requires (memory_load8_le(mem, 2346bv64) == 2bv8); @@ -325,9 +330,10 @@ procedure main() } procedure malloc(); + modifies Gamma_R16, Gamma_R17, R16, R17; procedure printCharValue() - modifies Gamma_R0, Gamma_R1, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_R8, Gamma_R9, Gamma_mem, Gamma_stack, R0, R1, R29, R30, R31, R8, R9, mem, stack; + modifies Gamma_R0, Gamma_R1, Gamma_R16, Gamma_R17, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_R8, Gamma_R9, Gamma_mem, Gamma_stack, R0, R1, R16, R17, R29, R30, R31, R8, R9, mem, stack; free ensures (Gamma_R29 == old(Gamma_R29)); free ensures (Gamma_R31 == old(Gamma_R31)); free ensures (R29 == old(R29)); @@ -366,3 +372,4 @@ procedure printCharValue() } procedure printf(); + modifies Gamma_R16, Gamma_R17, R16, R17; diff --git a/src/test/correct/malloc_with_local3/clang_O2/malloc_with_local3.expected b/src/test/correct/malloc_with_local3/clang_O2/malloc_with_local3.expected index 6df6b8049..21fc319de 100644 --- a/src/test/correct/malloc_with_local3/clang_O2/malloc_with_local3.expected +++ b/src/test/correct/malloc_with_local3/clang_O2/malloc_with_local3.expected @@ -1,5 +1,7 @@ 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; @@ -7,6 +9,8 @@ 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; @@ -56,7 +60,7 @@ procedure guarantee_reflexive(); modifies mem, Gamma_mem; procedure main() - modifies Gamma_R0, Gamma_R1, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_stack, R0, R1, R29, R30, R31, stack; + modifies Gamma_R0, Gamma_R1, Gamma_R16, Gamma_R17, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_stack, R0, R1, R16, R17, R29, R30, R31, stack; free requires (memory_load8_le(mem, 1996bv64) == 1bv8); free requires (memory_load8_le(mem, 1997bv64) == 0bv8); free requires (memory_load8_le(mem, 1998bv64) == 2bv8); @@ -233,3 +237,4 @@ procedure main() } procedure printf(); + modifies Gamma_R16, Gamma_R17, R16, R17; diff --git a/src/test/correct/malloc_with_local3/clang_no_plt_no_pic/malloc_with_local3.expected b/src/test/correct/malloc_with_local3/clang_no_plt_no_pic/malloc_with_local3.expected index bf53027e4..c8da0d736 100644 --- a/src/test/correct/malloc_with_local3/clang_no_plt_no_pic/malloc_with_local3.expected +++ b/src/test/correct/malloc_with_local3/clang_no_plt_no_pic/malloc_with_local3.expected @@ -1,5 +1,7 @@ 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; @@ -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 R29: bv64; var R30: bv64; var R31: bv64; @@ -95,9 +99,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_R8, Gamma_R9, Gamma_mem, Gamma_stack, R0, R1, R29, R30, R31, R8, R9, mem, stack; + modifies Gamma_R0, Gamma_R1, Gamma_R16, Gamma_R17, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_R8, Gamma_R9, Gamma_mem, Gamma_stack, R0, R1, R16, R17, R29, R30, R31, R8, R9, mem, stack; free requires (memory_load8_le(mem, 2344bv64) == 1bv8); free requires (memory_load8_le(mem, 2345bv64) == 0bv8); free requires (memory_load8_le(mem, 2346bv64) == 2bv8); @@ -325,9 +330,10 @@ procedure main() } procedure malloc(); + modifies Gamma_R16, Gamma_R17, R16, R17; procedure printCharValue() - modifies Gamma_R0, Gamma_R1, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_R8, Gamma_R9, Gamma_mem, Gamma_stack, R0, R1, R29, R30, R31, R8, R9, mem, stack; + modifies Gamma_R0, Gamma_R1, Gamma_R16, Gamma_R17, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_R8, Gamma_R9, Gamma_mem, Gamma_stack, R0, R1, R16, R17, R29, R30, R31, R8, R9, mem, stack; free ensures (Gamma_R29 == old(Gamma_R29)); free ensures (Gamma_R31 == old(Gamma_R31)); free ensures (R29 == old(R29)); @@ -366,3 +372,4 @@ procedure printCharValue() } procedure printf(); + modifies Gamma_R16, Gamma_R17, R16, R17; diff --git a/src/test/correct/malloc_with_local3/clang_pic/malloc_with_local3.expected b/src/test/correct/malloc_with_local3/clang_pic/malloc_with_local3.expected index bf53027e4..c8da0d736 100644 --- a/src/test/correct/malloc_with_local3/clang_pic/malloc_with_local3.expected +++ b/src/test/correct/malloc_with_local3/clang_pic/malloc_with_local3.expected @@ -1,5 +1,7 @@ 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; @@ -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 R29: bv64; var R30: bv64; var R31: bv64; @@ -95,9 +99,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_R8, Gamma_R9, Gamma_mem, Gamma_stack, R0, R1, R29, R30, R31, R8, R9, mem, stack; + modifies Gamma_R0, Gamma_R1, Gamma_R16, Gamma_R17, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_R8, Gamma_R9, Gamma_mem, Gamma_stack, R0, R1, R16, R17, R29, R30, R31, R8, R9, mem, stack; free requires (memory_load8_le(mem, 2344bv64) == 1bv8); free requires (memory_load8_le(mem, 2345bv64) == 0bv8); free requires (memory_load8_le(mem, 2346bv64) == 2bv8); @@ -325,9 +330,10 @@ procedure main() } procedure malloc(); + modifies Gamma_R16, Gamma_R17, R16, R17; procedure printCharValue() - modifies Gamma_R0, Gamma_R1, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_R8, Gamma_R9, Gamma_mem, Gamma_stack, R0, R1, R29, R30, R31, R8, R9, mem, stack; + modifies Gamma_R0, Gamma_R1, Gamma_R16, Gamma_R17, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_R8, Gamma_R9, Gamma_mem, Gamma_stack, R0, R1, R16, R17, R29, R30, R31, R8, R9, mem, stack; free ensures (Gamma_R29 == old(Gamma_R29)); free ensures (Gamma_R31 == old(Gamma_R31)); free ensures (R29 == old(R29)); @@ -366,3 +372,4 @@ procedure printCharValue() } procedure printf(); + modifies Gamma_R16, Gamma_R17, R16, R17; diff --git a/src/test/correct/malloc_with_local3/gcc/malloc_with_local3.expected b/src/test/correct/malloc_with_local3/gcc/malloc_with_local3.expected index 796945222..51c22a0cd 100644 --- a/src/test/correct/malloc_with_local3/gcc/malloc_with_local3.expected +++ b/src/test/correct/malloc_with_local3/gcc/malloc_with_local3.expected @@ -1,5 +1,7 @@ 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; @@ -7,6 +9,8 @@ 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; @@ -91,9 +95,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, 2328bv64) == 1bv8); free requires (memory_load8_le(mem, 2329bv64) == 0bv8); free requires (memory_load8_le(mem, 2330bv64) == 2bv8); @@ -403,9 +408,10 @@ procedure main() } procedure malloc(); + modifies Gamma_R16, Gamma_R17, R16, R17; procedure printCharValue() - 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 ensures (Gamma_R29 == old(Gamma_R29)); free ensures (Gamma_R31 == old(Gamma_R31)); free ensures (R29 == old(R29)); @@ -444,3 +450,4 @@ procedure printCharValue() } procedure printf(); + modifies Gamma_R16, Gamma_R17, R16, R17; diff --git a/src/test/correct/malloc_with_local3/gcc_O2/malloc_with_local3.expected b/src/test/correct/malloc_with_local3/gcc_O2/malloc_with_local3.expected index 4e3b48bdf..04db23a6a 100644 --- a/src/test/correct/malloc_with_local3/gcc_O2/malloc_with_local3.expected +++ b/src/test/correct/malloc_with_local3/gcc_O2/malloc_with_local3.expected @@ -1,5 +1,7 @@ var Gamma_R0: bool; var Gamma_R1: bool; +var Gamma_R16: bool; +var Gamma_R17: bool; var Gamma_R19: bool; var Gamma_R2: bool; var Gamma_R29: 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 R19: bv64; var R2: bv64; var R29: bv64; @@ -81,11 +85,13 @@ procedure guarantee_reflexive(); modifies mem, Gamma_mem; procedure __printf_chk(); + modifies Gamma_R16, Gamma_R17, R16, R17; procedure #free(); + modifies Gamma_R16, Gamma_R17, R16, R17; procedure main() - modifies Gamma_R0, Gamma_R1, Gamma_R19, Gamma_R2, Gamma_R29, Gamma_R3, Gamma_R30, Gamma_R31, Gamma_mem, Gamma_stack, R0, R1, R19, R2, R29, R3, R30, R31, mem, stack; + modifies Gamma_R0, Gamma_R1, Gamma_R16, Gamma_R17, Gamma_R19, Gamma_R2, Gamma_R29, Gamma_R3, Gamma_R30, Gamma_R31, Gamma_mem, Gamma_stack, R0, R1, R16, R17, R19, R2, R29, R3, R30, R31, mem, stack; free requires (memory_load8_le(mem, 2264bv64) == 1bv8); free requires (memory_load8_le(mem, 2265bv64) == 0bv8); free requires (memory_load8_le(mem, 2266bv64) == 2bv8); @@ -365,9 +371,10 @@ procedure main() } procedure malloc(); + modifies Gamma_R16, Gamma_R17, R16, R17; procedure printCharValue() - modifies Gamma_R0, Gamma_R1, Gamma_R2, Gamma_R3, Gamma_mem, R0, R1, R2, R3, mem; + modifies Gamma_R0, Gamma_R1, Gamma_R16, Gamma_R17, Gamma_R2, Gamma_R3, Gamma_mem, R0, R1, R16, R17, R2, R3, mem; { lprintCharValue: R3, Gamma_R3 := R0, Gamma_R0; diff --git a/src/test/correct/malloc_with_local3/gcc_no_plt_no_pic/malloc_with_local3.expected b/src/test/correct/malloc_with_local3/gcc_no_plt_no_pic/malloc_with_local3.expected index 0926dfb6d..b2e598f86 100644 --- a/src/test/correct/malloc_with_local3/gcc_no_plt_no_pic/malloc_with_local3.expected +++ b/src/test/correct/malloc_with_local3/gcc_no_plt_no_pic/malloc_with_local3.expected @@ -1,5 +1,7 @@ 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; @@ -7,6 +9,8 @@ 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; @@ -91,9 +95,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, 2328bv64) == 1bv8); free requires (memory_load8_le(mem, 2329bv64) == 0bv8); free requires (memory_load8_le(mem, 2330bv64) == 2bv8); @@ -403,9 +408,10 @@ procedure main() } procedure malloc(); + modifies Gamma_R16, Gamma_R17, R16, R17; procedure printCharValue() - 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 ensures (Gamma_R29 == old(Gamma_R29)); free ensures (Gamma_R31 == old(Gamma_R31)); free ensures (R29 == old(R29)); @@ -444,3 +450,4 @@ procedure printCharValue() } procedure printf(); + modifies Gamma_R16, Gamma_R17, R16, R17; diff --git a/src/test/correct/malloc_with_local3/gcc_pic/malloc_with_local3.expected b/src/test/correct/malloc_with_local3/gcc_pic/malloc_with_local3.expected index 0926dfb6d..b2e598f86 100644 --- a/src/test/correct/malloc_with_local3/gcc_pic/malloc_with_local3.expected +++ b/src/test/correct/malloc_with_local3/gcc_pic/malloc_with_local3.expected @@ -1,5 +1,7 @@ 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; @@ -7,6 +9,8 @@ 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; @@ -91,9 +95,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, 2328bv64) == 1bv8); free requires (memory_load8_le(mem, 2329bv64) == 0bv8); free requires (memory_load8_le(mem, 2330bv64) == 2bv8); @@ -403,9 +408,10 @@ procedure main() } procedure malloc(); + modifies Gamma_R16, Gamma_R17, R16, R17; procedure printCharValue() - 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 ensures (Gamma_R29 == old(Gamma_R29)); free ensures (Gamma_R31 == old(Gamma_R31)); free ensures (R29 == old(R29)); @@ -444,3 +450,4 @@ procedure printCharValue() } procedure printf(); + modifies Gamma_R16, Gamma_R17, R16, R17; diff --git a/src/test/correct/multi_malloc/clang/multi_malloc.expected b/src/test/correct/multi_malloc/clang/multi_malloc.expected index 371dfa88b..b501c6abc 100644 --- a/src/test/correct/multi_malloc/clang/multi_malloc.expected +++ b/src/test/correct/multi_malloc/clang/multi_malloc.expected @@ -1,5 +1,7 @@ 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; @@ -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 R29: bv64; var R30: bv64; var R31: bv64; @@ -94,9 +98,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_R8, Gamma_R9, Gamma_mem, Gamma_stack, R0, R1, R29, R30, R31, R8, R9, mem, stack; + modifies Gamma_R0, Gamma_R1, Gamma_R16, Gamma_R17, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_R8, Gamma_R9, Gamma_mem, Gamma_stack, R0, R1, R16, R17, R29, R30, R31, R8, R9, mem, stack; free requires (memory_load8_le(mem, 2232bv64) == 1bv8); free requires (memory_load8_le(mem, 2233bv64) == 0bv8); free requires (memory_load8_le(mem, 2234bv64) == 2bv8); @@ -273,5 +278,7 @@ procedure main() } procedure malloc(); + modifies Gamma_R16, Gamma_R17, R16, R17; procedure printf(); + modifies Gamma_R16, Gamma_R17, R16, R17; diff --git a/src/test/correct/multi_malloc/clang_O2/multi_malloc.expected b/src/test/correct/multi_malloc/clang_O2/multi_malloc.expected index 103b95408..fd845a751 100644 --- a/src/test/correct/multi_malloc/clang_O2/multi_malloc.expected +++ b/src/test/correct/multi_malloc/clang_O2/multi_malloc.expected @@ -1,5 +1,7 @@ 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; @@ -7,6 +9,8 @@ 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; @@ -56,7 +60,7 @@ procedure guarantee_reflexive(); modifies mem, Gamma_mem; procedure main() - modifies Gamma_R0, Gamma_R1, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_stack, R0, R1, R29, R30, R31, stack; + modifies Gamma_R0, Gamma_R1, Gamma_R16, Gamma_R17, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_stack, R0, R1, R16, R17, R29, R30, R31, stack; free requires (memory_load8_le(mem, 1948bv64) == 1bv8); free requires (memory_load8_le(mem, 1949bv64) == 0bv8); free requires (memory_load8_le(mem, 1950bv64) == 2bv8); @@ -193,3 +197,4 @@ procedure main() } procedure printf(); + modifies Gamma_R16, Gamma_R17, R16, R17; diff --git a/src/test/correct/multi_malloc/clang_no_plt_no_pic/multi_malloc.expected b/src/test/correct/multi_malloc/clang_no_plt_no_pic/multi_malloc.expected index a7ee58695..9d07eca32 100644 --- a/src/test/correct/multi_malloc/clang_no_plt_no_pic/multi_malloc.expected +++ b/src/test/correct/multi_malloc/clang_no_plt_no_pic/multi_malloc.expected @@ -1,5 +1,7 @@ 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; @@ -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 R29: bv64; var R30: bv64; var R31: bv64; @@ -94,9 +98,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_R8, Gamma_R9, Gamma_mem, Gamma_stack, R0, R1, R29, R30, R31, R8, R9, mem, stack; + modifies Gamma_R0, Gamma_R1, Gamma_R16, Gamma_R17, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_R8, Gamma_R9, Gamma_mem, Gamma_stack, R0, R1, R16, R17, R29, R30, R31, R8, R9, mem, stack; free requires (memory_load8_le(mem, 2232bv64) == 1bv8); free requires (memory_load8_le(mem, 2233bv64) == 0bv8); free requires (memory_load8_le(mem, 2234bv64) == 2bv8); @@ -273,5 +278,7 @@ procedure main() } procedure malloc(); + modifies Gamma_R16, Gamma_R17, R16, R17; procedure printf(); + modifies Gamma_R16, Gamma_R17, R16, R17; diff --git a/src/test/correct/multi_malloc/clang_pic/multi_malloc.expected b/src/test/correct/multi_malloc/clang_pic/multi_malloc.expected index a7ee58695..9d07eca32 100644 --- a/src/test/correct/multi_malloc/clang_pic/multi_malloc.expected +++ b/src/test/correct/multi_malloc/clang_pic/multi_malloc.expected @@ -1,5 +1,7 @@ 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; @@ -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 R29: bv64; var R30: bv64; var R31: bv64; @@ -94,9 +98,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_R8, Gamma_R9, Gamma_mem, Gamma_stack, R0, R1, R29, R30, R31, R8, R9, mem, stack; + modifies Gamma_R0, Gamma_R1, Gamma_R16, Gamma_R17, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_R8, Gamma_R9, Gamma_mem, Gamma_stack, R0, R1, R16, R17, R29, R30, R31, R8, R9, mem, stack; free requires (memory_load8_le(mem, 2232bv64) == 1bv8); free requires (memory_load8_le(mem, 2233bv64) == 0bv8); free requires (memory_load8_le(mem, 2234bv64) == 2bv8); @@ -273,5 +278,7 @@ procedure main() } procedure malloc(); + modifies Gamma_R16, Gamma_R17, R16, R17; procedure printf(); + modifies Gamma_R16, Gamma_R17, R16, R17; diff --git a/src/test/correct/multi_malloc/gcc/multi_malloc.expected b/src/test/correct/multi_malloc/gcc/multi_malloc.expected index 60906b9a8..3c7b09b7d 100644 --- a/src/test/correct/multi_malloc/gcc/multi_malloc.expected +++ b/src/test/correct/multi_malloc/gcc/multi_malloc.expected @@ -1,5 +1,7 @@ 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; @@ -7,6 +9,8 @@ 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; @@ -90,9 +94,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, 2224bv64) == 1bv8); free requires (memory_load8_le(mem, 2225bv64) == 0bv8); free requires (memory_load8_le(mem, 2226bv64) == 2bv8); @@ -356,5 +361,7 @@ procedure main() } procedure malloc(); + modifies Gamma_R16, Gamma_R17, R16, R17; procedure printf(); + modifies Gamma_R16, Gamma_R17, R16, R17; diff --git a/src/test/correct/multi_malloc/gcc_O2/multi_malloc.expected b/src/test/correct/multi_malloc/gcc_O2/multi_malloc.expected index d45acb963..773c5d4e6 100644 --- a/src/test/correct/multi_malloc/gcc_O2/multi_malloc.expected +++ b/src/test/correct/multi_malloc/gcc_O2/multi_malloc.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; @@ -58,9 +62,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_R30, Gamma_R31, Gamma_stack, R0, R1, R2, R29, R30, R31, stack; + modifies Gamma_R0, Gamma_R1, Gamma_R16, Gamma_R17, Gamma_R2, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_stack, R0, R1, R16, R17, R2, R29, R30, R31, 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); diff --git a/src/test/correct/multi_malloc/gcc_no_plt_no_pic/multi_malloc.expected b/src/test/correct/multi_malloc/gcc_no_plt_no_pic/multi_malloc.expected index 8e3106dcb..35770119f 100644 --- a/src/test/correct/multi_malloc/gcc_no_plt_no_pic/multi_malloc.expected +++ b/src/test/correct/multi_malloc/gcc_no_plt_no_pic/multi_malloc.expected @@ -1,5 +1,7 @@ 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; @@ -7,6 +9,8 @@ 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; @@ -90,9 +94,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, 2224bv64) == 1bv8); free requires (memory_load8_le(mem, 2225bv64) == 0bv8); free requires (memory_load8_le(mem, 2226bv64) == 2bv8); @@ -356,5 +361,7 @@ procedure main() } procedure malloc(); + modifies Gamma_R16, Gamma_R17, R16, R17; procedure printf(); + modifies Gamma_R16, Gamma_R17, R16, R17; diff --git a/src/test/correct/multi_malloc/gcc_pic/multi_malloc.expected b/src/test/correct/multi_malloc/gcc_pic/multi_malloc.expected index 8e3106dcb..35770119f 100644 --- a/src/test/correct/multi_malloc/gcc_pic/multi_malloc.expected +++ b/src/test/correct/multi_malloc/gcc_pic/multi_malloc.expected @@ -1,5 +1,7 @@ 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; @@ -7,6 +9,8 @@ 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; @@ -90,9 +94,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, 2224bv64) == 1bv8); free requires (memory_load8_le(mem, 2225bv64) == 0bv8); free requires (memory_load8_le(mem, 2226bv64) == 2bv8); @@ -356,5 +361,7 @@ procedure main() } procedure malloc(); + modifies Gamma_R16, Gamma_R17, R16, R17; procedure printf(); + modifies Gamma_R16, Gamma_R17, R16, R17; diff --git a/src/test/correct/syscall/clang/syscall.expected b/src/test/correct/syscall/clang/syscall.expected index d61927f44..1a8c518d9 100644 --- a/src/test/correct/syscall/clang/syscall.expected +++ b/src/test/correct/syscall/clang/syscall.expected @@ -1,5 +1,7 @@ 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; @@ -7,6 +9,8 @@ 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; @@ -73,9 +77,10 @@ procedure guarantee_reflexive(); modifies mem, Gamma_mem; procedure fork(); + modifies Gamma_R16, Gamma_R17, R16, R17; procedure main() - modifies Gamma_R0, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_stack, R0, R29, R30, R31, stack; + modifies Gamma_R0, Gamma_R16, Gamma_R17, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_stack, R0, R16, R17, R29, R30, R31, stack; free requires (memory_load8_le(mem, 1944bv64) == 1bv8); free requires (memory_load8_le(mem, 1945bv64) == 0bv8); free requires (memory_load8_le(mem, 1946bv64) == 2bv8); diff --git a/src/test/correct/syscall/clang_no_plt_no_pic/syscall.expected b/src/test/correct/syscall/clang_no_plt_no_pic/syscall.expected index 831cea2df..64d1e7fd5 100644 --- a/src/test/correct/syscall/clang_no_plt_no_pic/syscall.expected +++ b/src/test/correct/syscall/clang_no_plt_no_pic/syscall.expected @@ -1,5 +1,7 @@ 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; @@ -7,6 +9,8 @@ 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; @@ -73,9 +77,10 @@ procedure guarantee_reflexive(); modifies mem, Gamma_mem; procedure fork(); + modifies Gamma_R16, Gamma_R17, R16, R17; procedure main() - modifies Gamma_R0, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_stack, R0, R29, R30, R31, stack; + modifies Gamma_R0, Gamma_R16, Gamma_R17, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_stack, R0, R16, R17, R29, R30, R31, stack; free requires (memory_load8_le(mem, 1944bv64) == 1bv8); free requires (memory_load8_le(mem, 1945bv64) == 0bv8); free requires (memory_load8_le(mem, 1946bv64) == 2bv8); diff --git a/src/test/correct/syscall/clang_pic/syscall.expected b/src/test/correct/syscall/clang_pic/syscall.expected index 831cea2df..64d1e7fd5 100644 --- a/src/test/correct/syscall/clang_pic/syscall.expected +++ b/src/test/correct/syscall/clang_pic/syscall.expected @@ -1,5 +1,7 @@ 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; @@ -7,6 +9,8 @@ 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; @@ -73,9 +77,10 @@ procedure guarantee_reflexive(); modifies mem, Gamma_mem; procedure fork(); + modifies Gamma_R16, Gamma_R17, R16, R17; procedure main() - modifies Gamma_R0, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_stack, R0, R29, R30, R31, stack; + modifies Gamma_R0, Gamma_R16, Gamma_R17, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_stack, R0, R16, R17, R29, R30, R31, stack; free requires (memory_load8_le(mem, 1944bv64) == 1bv8); free requires (memory_load8_le(mem, 1945bv64) == 0bv8); free requires (memory_load8_le(mem, 1946bv64) == 2bv8); diff --git a/src/test/correct/syscall/gcc/syscall.expected b/src/test/correct/syscall/gcc/syscall.expected index fdb932984..4307d62e1 100644 --- a/src/test/correct/syscall/gcc/syscall.expected +++ b/src/test/correct/syscall/gcc/syscall.expected @@ -1,5 +1,7 @@ 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; @@ -7,6 +9,8 @@ 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; @@ -73,9 +77,10 @@ procedure guarantee_reflexive(); modifies mem, Gamma_mem; procedure fork(); + modifies Gamma_R16, Gamma_R17, R16, R17; procedure main() - modifies Gamma_R0, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_stack, R0, R29, R30, R31, stack; + modifies Gamma_R0, Gamma_R16, Gamma_R17, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_stack, R0, R16, R17, R29, R30, R31, stack; free requires (memory_load8_le(mem, 1932bv64) == 1bv8); free requires (memory_load8_le(mem, 1933bv64) == 0bv8); free requires (memory_load8_le(mem, 1934bv64) == 2bv8); diff --git a/src/test/correct/syscall/gcc_O2/syscall.expected b/src/test/correct/syscall/gcc_O2/syscall.expected index 619bb12a0..09a469b75 100644 --- a/src/test/correct/syscall/gcc_O2/syscall.expected +++ b/src/test/correct/syscall/gcc_O2/syscall.expected @@ -1,4 +1,8 @@ +var Gamma_R16: bool; +var Gamma_R17: bool; var Gamma_mem: [bv64]bool; +var R16: bv64; +var R17: bv64; var mem: [bv64]bv8; const $_IO_stdin_used_addr: bv64; axiom ($_IO_stdin_used_addr == 1960bv64); @@ -27,6 +31,7 @@ procedure guarantee_reflexive(); modifies mem, Gamma_mem; procedure fork(); + modifies Gamma_R16, Gamma_R17, R16, R17; free requires (memory_load8_le(mem, 1960bv64) == 1bv8); free requires (memory_load8_le(mem, 1961bv64) == 0bv8); free requires (memory_load8_le(mem, 1962bv64) == 2bv8); diff --git a/src/test/correct/syscall/gcc_no_plt_no_pic/syscall.expected b/src/test/correct/syscall/gcc_no_plt_no_pic/syscall.expected index 2901c3ac3..de69bd13e 100644 --- a/src/test/correct/syscall/gcc_no_plt_no_pic/syscall.expected +++ b/src/test/correct/syscall/gcc_no_plt_no_pic/syscall.expected @@ -1,5 +1,7 @@ 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; @@ -7,6 +9,8 @@ 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; @@ -73,9 +77,10 @@ procedure guarantee_reflexive(); modifies mem, Gamma_mem; procedure fork(); + modifies Gamma_R16, Gamma_R17, R16, R17; procedure main() - modifies Gamma_R0, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_stack, R0, R29, R30, R31, stack; + modifies Gamma_R0, Gamma_R16, Gamma_R17, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_stack, R0, R16, R17, R29, R30, R31, stack; free requires (memory_load8_le(mem, 1932bv64) == 1bv8); free requires (memory_load8_le(mem, 1933bv64) == 0bv8); free requires (memory_load8_le(mem, 1934bv64) == 2bv8); diff --git a/src/test/correct/syscall/gcc_pic/syscall.expected b/src/test/correct/syscall/gcc_pic/syscall.expected index 2901c3ac3..de69bd13e 100644 --- a/src/test/correct/syscall/gcc_pic/syscall.expected +++ b/src/test/correct/syscall/gcc_pic/syscall.expected @@ -1,5 +1,7 @@ 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; @@ -7,6 +9,8 @@ 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; @@ -73,9 +77,10 @@ procedure guarantee_reflexive(); modifies mem, Gamma_mem; procedure fork(); + modifies Gamma_R16, Gamma_R17, R16, R17; procedure main() - modifies Gamma_R0, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_stack, R0, R29, R30, R31, stack; + modifies Gamma_R0, Gamma_R16, Gamma_R17, Gamma_R29, Gamma_R30, Gamma_R31, Gamma_stack, R0, R16, R17, R29, R30, R31, stack; free requires (memory_load8_le(mem, 1932bv64) == 1bv8); free requires (memory_load8_le(mem, 1933bv64) == 0bv8); free requires (memory_load8_le(mem, 1934bv64) == 2bv8);