Skip to content

Commit

Permalink
Also fix atomic
Browse files Browse the repository at this point in the history
  • Loading branch information
michael-schwarz committed May 27, 2024
1 parent 9b4b255 commit 896f236
Show file tree
Hide file tree
Showing 2 changed files with 32 additions and 10 deletions.
21 changes: 11 additions & 10 deletions src/analyses/apron/relationPriv.apron.ml
Original file line number Diff line number Diff line change
Expand Up @@ -482,17 +482,18 @@ struct
let get_mutex_global_g_with_mutex_inits (ask:Q.ask) getg g =
let g_var = AV.global g in
let get_mutex_global_g =
if Param.handle_atomic then (
(* Unprotected invariant is one big relation. *)
RD.keep_vars (getg (V.mutex atomic_mutex)) [g_var]
)
else
let r = getg (V.global g) in
if RD.is_bot r && (ask.f (Queries.IsAllocVar g)) then
(* malloc'ed blobs may not have a value here yet *)
RD.top ()
let r =
if Param.handle_atomic then
(* Unprotected invariant is one big relation. *)
RD.keep_vars (getg (V.mutex atomic_mutex)) [g_var]
else
r
getg (V.global g)
in
if RD.is_bot r && (ask.f (Queries.IsAllocVar g)) then
(* malloc'ed blobs may not have a value here yet *)
RD.top ()
else
r
in
let get_mutex_inits = getg V.mutex_inits in
let get_mutex_inits' = RD.keep_vars get_mutex_inits [g_var] in
Expand Down
21 changes: 21 additions & 0 deletions tests/regression/46-apron2/91-malloc-atomic.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,21 @@
// SKIP PARAM: --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-atomic --set ana.apron.domain interval --set sem.int.signed_overflow assume_none
// Checks that assinging to malloc'ed memory does not cause both branches to be dead
#include <pthread.h>
#include <goblint.h>
void nop(void* arg) {
}

void main() {
pthread_t thread;
pthread_create(&thread, 0, &nop, 0);

long *k = malloc(sizeof(long));
*k = 5;
if (1)
;

__goblint_check(*k >= 5); // Reachable and true

*k = *k+1;
__goblint_check(*k >= 5); // Reachable and true
}

0 comments on commit 896f236

Please sign in to comment.