Skip to content

Commit

Permalink
Merge pull request #1345 from goblint/issue_1338
Browse files Browse the repository at this point in the history
`eval_rv_base`: cast without `torg` when `typeOf` fails
  • Loading branch information
michael-schwarz authored Jan 29, 2024
2 parents 5224948 + 1bb8d43 commit 10b18cf
Show file tree
Hide file tree
Showing 2 changed files with 16 additions and 2 deletions.
7 changes: 5 additions & 2 deletions src/analyses/base.ml
Original file line number Diff line number Diff line change
Expand Up @@ -876,8 +876,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 _
Expand Down
11 changes: 11 additions & 0 deletions tests/regression/46-apron2/60-issue-1338.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
// SKIP PARAM: --set ana.activated[+] apron
#include <stdlib.h>
int main()
{
char *ptr = malloc(2);
char s = *(ptr+0)+0;

char *arr;
arr = malloc(8);
int tmp = (int)*(arr+0);
}

0 comments on commit 10b18cf

Please sign in to comment.