From dfaa55babf015f0547468975240835bfea34f2a6 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sun, 28 Jan 2024 19:39:08 +0100 Subject: [PATCH 1/2] eval_rv_base: cast without torg when typeOf fails --- src/analyses/base.ml | 7 +++++-- tests/regression/46-apron2/60-issue-1338.c | 11 +++++++++++ 2 files changed, 16 insertions(+), 2 deletions(-) create mode 100644 tests/regression/46-apron2/60-issue-1338.c diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 42e43b623a..5a214562b8 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -877,8 +877,11 @@ struct Address (AD.map array_start (eval_lv ~ctx st lval)) | CastE (t, Const (CStr (x,e))) -> (* VD.top () *) eval_rv ~ctx st (Const (CStr (x,e))) (* TODO safe? *) | CastE (t, exp) -> - let v = eval_rv ~ctx st exp in - VD.cast ~torg:(Cilfacade.typeOf exp) t v + (let v = eval_rv ~ctx st exp in + try + VD.cast ~torg:(Cilfacade.typeOf exp) t v + with Cilfacade.TypeOfError _ -> + VD.cast t v) | SizeOf _ | Real _ | Imag _ diff --git a/tests/regression/46-apron2/60-issue-1338.c b/tests/regression/46-apron2/60-issue-1338.c new file mode 100644 index 0000000000..899fe613b3 --- /dev/null +++ b/tests/regression/46-apron2/60-issue-1338.c @@ -0,0 +1,11 @@ +// SKIP PARAM: --set ana.activated[+] apron +#include +int main() +{ + char *ptr = malloc(2); + char s = *(ptr+0)+0; + + char *arr; + arr = malloc(8); + int tmp = (int)*(arr+0); +} \ No newline at end of file From 1bb8d43bdcd3b4228d1671facc1df204a56e556d Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sun, 28 Jan 2024 19:39:52 +0100 Subject: [PATCH 2/2] Indent --- src/analyses/base.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 5a214562b8..b4f01d2188 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -878,10 +878,10 @@ struct | CastE (t, Const (CStr (x,e))) -> (* VD.top () *) eval_rv ~ctx st (Const (CStr (x,e))) (* TODO safe? *) | CastE (t, exp) -> (let v = eval_rv ~ctx st exp in - try - VD.cast ~torg:(Cilfacade.typeOf exp) t v - with Cilfacade.TypeOfError _ -> - VD.cast t v) + try + VD.cast ~torg:(Cilfacade.typeOf exp) t v + with Cilfacade.TypeOfError _ -> + VD.cast t v) | SizeOf _ | Real _ | Imag _