-
Notifications
You must be signed in to change notification settings - Fork 76
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge pull request #1198 from goblint/race-ignorable
Check all offsets, attributes and `typedef`s for ignored race memory locations
- Loading branch information
Showing
9 changed files
with
264 additions
and
56 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,12 +1,11 @@ | ||
| # on `dune build` goblint.opam will be generated from goblint.opam.template and dune-project | ||
| # also remember to generate/adjust goblint.opam.locked! | ||
| available: os-distribution != "alpine" & arch != "arm64" | ||
| # pin-depends: [ | ||
| # published goblint-cil 2.0.2 is currently up-to-date, so no pin needed | ||
| # [ "goblint-cil.2.0.2" "git+https://github.com/goblint/cil.git#98598d94f796a63751e5a9d39c6b3a9fe1f32330" ] | ||
| pin-depends: [ | ||
| [ "goblint-cil.2.0.2" "git+https://github.com/goblint/cil.git#398dca3d94a06a9026b3737aabf100ee3498229f" ] | ||
| # TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252) | ||
| # [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ] | ||
| # ] | ||
| ] | ||
| post-messages: [ | ||
| "Do not benchmark Goblint on OCaml 5 (https://goblint.readthedocs.io/en/latest/user-guide/benchmarking/)." {ocaml:version >= "5.0.0"} | ||
| ] |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,24 +1,83 @@ | ||
| #include <pthread.h> | ||
| #include <stdio.h> | ||
| #include <stdatomic.h> | ||
|
|
||
| atomic_int myglobal; | ||
| pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER; | ||
| pthread_mutex_t mutex2 = PTHREAD_MUTEX_INITIALIZER; | ||
| atomic_int g1; | ||
| _Atomic int g2; | ||
| _Atomic(int) g3; | ||
|
|
||
| atomic_int a1[1]; | ||
| _Atomic int a2[1]; | ||
| _Atomic(int) a3[1]; | ||
|
|
||
| struct s { | ||
| int f0; | ||
| atomic_int f1; | ||
| _Atomic int f2; | ||
| _Atomic(int) f3; | ||
| }; | ||
|
|
||
| struct s s1; | ||
| _Atomic struct s s2; | ||
| _Atomic(struct s) s3; | ||
|
|
||
| typedef atomic_int t_int1; | ||
| typedef _Atomic int t_int2; | ||
| typedef _Atomic(int) t_int3; | ||
|
|
||
| t_int1 t1; | ||
| t_int2 t2; | ||
| t_int3 t3; | ||
|
|
||
| typedef int t_int0; | ||
|
|
||
| _Atomic t_int0 t0; | ||
| _Atomic(t_int0) t00; | ||
|
|
||
| atomic_int *p0 = &g1; | ||
| int x; | ||
| // int * _Atomic p1 = &x; // TODO: https://github.com/goblint/cil/issues/64 | ||
| // _Atomic(int*) p2 = &x; // TODO: https://github.com/goblint/cil/issues/64 | ||
| // atomic_int * _Atomic p3 = &g1; // TODO: https://github.com/goblint/cil/issues/64 | ||
|
|
||
| atomic_flag flag = ATOMIC_FLAG_INIT; | ||
|
|
||
| void *t_fun(void *arg) { | ||
| pthread_mutex_lock(&mutex1); | ||
| myglobal=myglobal+1; // NORACE | ||
| pthread_mutex_unlock(&mutex1); | ||
| g1++; // NORACE | ||
| g2++; // NORACE | ||
| g3++; // NORACE | ||
| a1[0]++; // NORACE | ||
| a2[0]++; // NORACE | ||
| a3[0]++; // NORACE | ||
| s1.f1++; // NORACE | ||
| s1.f2++; // NORACE | ||
| s1.f3++; // NORACE | ||
| s2.f0++; // NORACE | ||
| s3.f0++; // NORACE | ||
| t1++; // NORACE | ||
| t2++; // NORACE | ||
| t3++; // NORACE | ||
| t0++; // NORACE | ||
| t00++; // NORACE | ||
| (*p0)++; // NORACE | ||
| // p1++; // TODO NORACE: https://github.com/goblint/cil/issues/64 | ||
| // p2++; // TODO NORACE: https://github.com/goblint/cil/issues/64 | ||
| // p3++; // TODO NORACE: https://github.com/goblint/cil/issues/64 | ||
| // (*p3)++; // TODO NORACE: https://github.com/goblint/cil/issues/64 | ||
|
|
||
| struct s ss = {0}; | ||
| s2 = ss; // NORACE | ||
| s3 = ss; // NORACE | ||
|
|
||
| atomic_flag_clear(&flag); // NORACE | ||
| atomic_flag_test_and_set(&flag); // NORACE | ||
| return NULL; | ||
| } | ||
|
|
||
| int main(void) { | ||
| pthread_t id; | ||
| pthread_t id, id2; | ||
| pthread_create(&id, NULL, t_fun, NULL); | ||
| pthread_mutex_lock(&mutex2); | ||
| myglobal=myglobal+1; // NORACE | ||
| pthread_mutex_unlock(&mutex2); | ||
| pthread_join (id, NULL); | ||
| pthread_create(&id2, NULL, t_fun, NULL); | ||
| pthread_join(id, NULL); | ||
| pthread_join(id2, NULL); | ||
| return 0; | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,18 +1,53 @@ | ||
| // PARAM: --disable ana.race.volatile | ||
| #include <pthread.h> | ||
| #include <stdio.h> | ||
|
|
||
| volatile int myglobal; | ||
| volatile int g1; | ||
|
|
||
| volatile int a1[1]; | ||
|
|
||
| struct s { | ||
| int f0; | ||
| volatile int f1; | ||
| }; | ||
|
|
||
| struct s s1; | ||
| volatile struct s s2; | ||
|
|
||
| typedef volatile int t_int1; | ||
|
|
||
| t_int1 t1; | ||
|
|
||
| typedef int t_int0; | ||
|
|
||
| volatile t_int0 t0; | ||
|
|
||
| volatile int *p0 = &g1; | ||
| int x; | ||
| int * volatile p1 = &x; | ||
| volatile int * volatile p2 = &g1; | ||
|
|
||
| void *t_fun(void *arg) { | ||
| myglobal= 8; //NORACE | ||
| g1++; // NORACE | ||
| a1[0]++; // NORACE | ||
| s1.f1++; // NORACE | ||
| s2.f0++; // NORACE | ||
| t1++; // NORACE | ||
| t0++; // NORACE | ||
| (*p0)++; // NORACE | ||
| p1++; // NORACE | ||
| p2++; // NORACE | ||
| (*p2)++; // NORACE | ||
|
|
||
| struct s ss = {0}; | ||
| s2 = ss; // NORACE | ||
| return NULL; | ||
| } | ||
|
|
||
| int main(void) { | ||
| pthread_t id; | ||
| pthread_create(&id, NULL, t_fun, (void*) &myglobal); | ||
| myglobal = 42; //NORACE | ||
| pthread_join (id, NULL); | ||
| pthread_t id, id2; | ||
| pthread_create(&id, NULL, t_fun, NULL); | ||
| pthread_create(&id2, NULL, t_fun, NULL); | ||
| pthread_join(id, NULL); | ||
| pthread_join(id2, NULL); | ||
| return 0; | ||
| } | ||
| } |
Oops, something went wrong.