diff --git a/tests/cn/self_ref_init.unknown.c b/tests/cn/self_ref_init.unknown.c new file mode 100644 index 000000000..d58091adb --- /dev/null +++ b/tests/cn/self_ref_init.unknown.c @@ -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; +} + diff --git a/tests/run-cn.sh b/tests/run-cn.sh index 787d58255..d94c88ce6 100755 --- a/tests/run-cn.sh +++ b/tests/run-cn.sh @@ -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