Skip to content

Commit

Permalink
CN: add a test for the self-ref init case
Browse files Browse the repository at this point in the history
Cerberus treats this as UB, whereas some Linux code seems to assume
it works. Add an "unknown" category to the CN tests for code where
it's not clear if it should be rejected or not.
  • Loading branch information
talsewell committed Aug 16, 2023
1 parent 07d4c4b commit 9270fcf
Show file tree
Hide file tree
Showing 2 changed files with 20 additions and 1 deletion.
19 changes: 19 additions & 0 deletions tests/cn/self_ref_init.unknown.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,19 @@

/* based on a problematic example from linux kvm/pgtable.c */

struct str {
int x;
int y;
};

int f (int x)
/*@ requires (0 <= x) && (x < 200) @*/
{
struct str str_inst = {
.x = x + 2,
.y = str_inst.x + 3,
};

return str_inst.y;
}

2 changes: 1 addition & 1 deletion tests/run-cn.sh
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@ DIRNAME=$(dirname $0)

set -e

SUCC=$(find $DIRNAME/cn -name '*.c' | grep -v '\.error\.c')
SUCC=$(find $DIRNAME/cn -name '*.c' | grep -v '\.error\.c' | grep -v '\.unknown\.c')

for TEST in $SUCC
do
Expand Down

0 comments on commit 9270fcf

Please sign in to comment.