Skip to content

Commit

Permalink
Handle pthread_rwlock_t as opaque mutex in base analysis
Browse files Browse the repository at this point in the history
Avoids unsound rwlock struct content invariants in witnesses.
  • Loading branch information
sim642 committed Jun 18, 2024
1 parent 36ff621 commit 7fcb10c
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/cdomain/value/cdomains/valueDomain.ml
Original file line number Diff line number Diff line change
Expand Up @@ -120,7 +120,7 @@ struct
| _ -> false

let is_mutex_type (t: typ): bool = match t with
| TNamed (info, attr) -> info.tname = "pthread_mutex_t" || info.tname = "spinlock_t" || info.tname = "pthread_spinlock_t" || info.tname = "pthread_cond_t"
| TNamed (info, attr) -> info.tname = "pthread_mutex_t" || info.tname = "spinlock_t" || info.tname = "pthread_spinlock_t" || info.tname = "pthread_cond_t" || info.tname = "pthread_rwlock_t"
| TInt (IInt, attr) -> hasAttribute "mutex" attr
| _ -> false

Expand Down

0 comments on commit 7fcb10c

Please sign in to comment.