Skip to content

Commit

Permalink
Add paper example
Browse files Browse the repository at this point in the history
  • Loading branch information
karoliineh committed Sep 13, 2024
1 parent fff58cc commit bce39b4
Show file tree
Hide file tree
Showing 3 changed files with 66 additions and 0 deletions.
38 changes: 38 additions & 0 deletions adb_examples/debt-24-demo/paper-example/example.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,38 @@
#include <stdio.h>
#include <pthread.h>

pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER;
typedef enum { PUBLISH, CACHE } ThreadAction;
int global;

int f(ThreadAction action) {
int cache = 0;
switch (action) {
case CACHE:
printf("Store in local cache!\n");
cache = 42;
break; // remove for flawed version
case PUBLISH:
printf("Publish work!\n");
global = 42;
}
}

void *t(void *arg) {
if (pthread_mutex_lock(&mutex)) {
f(CACHE);
} else {
f(PUBLISH);
pthread_mutex_unlock(&mutex);
}
}


int main() {
pthread_t t1, t2;
pthread_create(&t1, NULL, t, NULL);
pthread_create(&t2, NULL, t, NULL);
pthread_join(t1, NULL);
pthread_join(t2, NULL);
return 0;
}
22 changes: 22 additions & 0 deletions adb_examples/debt-24-demo/paper-example/goblint.json
Original file line number Diff line number Diff line change
@@ -0,0 +1,22 @@
{
"files": [
"example.c"
],
"ana": {
"int": {
"def_exc" : false,
"interval": true
}
},
"sem": {
"lock": {
"fail": true
}
},
"warn": {
"imprecise": false,
"deadcode": false,
"info": false
},
"allglobs": true
}
6 changes: 6 additions & 0 deletions adb_examples/debt-24-demo/paper-example/gobpie.json
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
{
"goblintConf" : "goblint.json",
"abstractDebugging": true,
"showCfg": true,
"incrementalAnalysis": false
}

0 comments on commit bce39b4

Please sign in to comment.