Skip to content

Commit 2c69f46

Browse files
Try to replace pointr derefs with variables also in query
1 parent 2d48d5b commit 2c69f46

File tree

2 files changed

+29
-1
lines changed

2 files changed

+29
-1
lines changed

src/analyses/apron/apronAnalysis.apron.ml

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -425,9 +425,10 @@ struct
425425
let open Queries in
426426
let st = ctx.local in
427427
let eval_int e =
428+
let esimple = replace_deref_exps ctx.ask e in
428429
read_from_globals_wrapper
429430
(Analyses.ask_of_ctx ctx)
430-
ctx.global st e
431+
ctx.global st esimple
431432
(fun apr' e' -> AD.eval_int apr' e')
432433
in
433434
match q with
Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,27 @@
1+
// SKIP PARAM: --set solver td3 --set ana.activated "['base','threadid','threadflag','mallocWrapper','apron','escape']" --set ana.path_sens[+] threadflag --set ana.base.privatization none --set ana.apron.privatization mutex-meet-tid --set ana.base.arrays.domain partitioned
2+
#include <pthread.h>
3+
#include <assert.h>
4+
#include <stdio.h>
5+
#include <unistd.h>
6+
7+
8+
int main(){
9+
int arr[] = {2, 4};
10+
11+
int x,y;
12+
13+
int* ptr = &y;
14+
x = y;
15+
16+
int z = *ptr == x;
17+
assert(x==y);
18+
assert(z == 1);
19+
assert(*ptr == x);
20+
assert(*ptr == y);
21+
assert(y == y);
22+
23+
assert(arr[*ptr == x] == 4);
24+
25+
26+
return 0;
27+
}

0 commit comments

Comments
 (0)