From 60110de0eb849d4b33f21f16ed68a496b1f02f84 Mon Sep 17 00:00:00 2001 From: Ricardo Baratto Date: Thu, 12 Mar 2026 21:03:01 -0400 Subject: [PATCH] CHC: support pointer arithmetic on argv If the program did argv[x] (after checking x is valid) we would correctly mark that as safe. However, if the program did * (argv + x) then we would not be able to discharge it. --- CodeHawk/CHC/cchanalyze/cCHPOQuery.ml | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/CodeHawk/CHC/cchanalyze/cCHPOQuery.ml b/CodeHawk/CHC/cchanalyze/cCHPOQuery.ml index aba0464a..b420ed5f 100644 --- a/CodeHawk/CHC/cchanalyze/cCHPOQuery.ml +++ b/CodeHawk/CHC/cchanalyze/cCHPOQuery.ml @@ -476,7 +476,13 @@ object (self) | PPtrUpperBoundDeref (_, IndexPI, Lval (Var (_, vid), NoOffset), - Const (CInt (i64, _, _))) when is_argv vid -> + Const (CInt (i64, _, _))) + | PPtrUpperBoundDeref (_, + PlusPI, + Lval (Var (_, vid), NoOffset), + Const (CInt (i64, _, _))) + when is_argv vid -> + (* This supports argv[index] or * (argv + index) *) let index = Int64.to_int i64 in (match self#is_valid_argv_index index with | Some (ideps, imsg) ->