Skip to content

Commit

Permalink
Fix test annotation.
Browse files Browse the repository at this point in the history
n-> next != NULL is actually unknown, as other thread may manipulate n concurrently.
  • Loading branch information
jerhard committed Nov 29, 2023
1 parent 58c8945 commit 57eac77
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions tests/regression/79-modular/28-return-void-allocated.c
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ typedef struct node {

node_t *allocate_node(){
// Changing the pointer type to node_t* resolves the issue
int* n = malloc(sizeof(node_t));
node_t* n = malloc(sizeof(node_t));
return (node_t*) n;
}

Expand All @@ -30,7 +30,7 @@ node_t *add_node(node_t *n){
__goblint_check(new_node != NULL);

n->next = new_node;
__goblint_check(n->next != NULL);
__goblint_check(n->next != NULL); //UNKNOWN!

new_node = init_node(new_node);
__goblint_check(new_node != NULL); //UNKNOWN
Expand Down

0 comments on commit 57eac77

Please sign in to comment.