diff --git a/tests/syntax/inline_stmt_contract.i b/tests/syntax/inline_stmt_contract.i new file mode 100644 index 0000000000000000000000000000000000000000..551a6c461a02df52d91495bef90d65cbd08fded5 --- /dev/null +++ b/tests/syntax/inline_stmt_contract.i @@ -0,0 +1,44 @@ +/* run.config +OPT: -inline-stmt-contracts -print +*/ + +int X; + +int f() { + /*@ requires X == 0; + ensures X == 1; + */ + X++; + return X; +} + +int g() { + + /*@ behavior b: + assumes X >= 0; + requires X > -1; + ensures X == 0; + */ + if (X >= 0) { X = 0; } else { X = -1; } + return X; +} + +int h() { + /*@ ensures \false; */ + return 1; +} + +int i() { + /*@ behavior b0: + assumes X == 0; + ensures X == 1; + */ + X++; + + /*@ behavior b1: + assumes X == 1; + ensures X == 2; + */ + X++; + return X; +} diff --git a/tests/syntax/oracle/inline_stmt_contract.res.oracle b/tests/syntax/oracle/inline_stmt_contract.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391