Skip to content

Commit f33df7e

Browse files
committed
Support else-if predicate syntax
Backwards-compatible frontend only change (bumping cerberus-lib, adding and updating tests).
1 parent b41bad6 commit f33df7e

5 files changed

+27
-3
lines changed

Makefile

-1
Original file line numberDiff line numberDiff line change
@@ -29,7 +29,6 @@ full-build:
2929
cn:
3030
@echo "[DUNE] $@"
3131
$(Q)dune build -p cn
32-
@echo -e "\nDONE"
3332

3433
.PHONY: clean
3534
clean:

cn.opam

+1-1
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,7 @@ depends: [
2323
"zarith" {>= "1.13"}
2424
]
2525
pin-depends: [
26-
["cerberus-lib.dev" "git+https://github.com/rems-project/cerberus.git#2d84326"]
26+
["cerberus-lib.dev" "git+https://github.com/rems-project/cerberus.git#62f0fcf"]
2727
]
2828
build: [
2929
["dune" "subst"] {pinned}
+1-1
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
return code: 2
22
tests/cn/list_literal_type.error.c:3:15: error: unexpected token after 'list' and before '<'
3-
Please add error message for state 1842 to parsers/c/c_parser_error.messages
3+
Please add error message for state 1844 to parsers/c/c_parser_error.messages
44
function (list<integer>) nonempty_list() {
55
^

tests/cn/predicate_else_if.c

+20
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
/*@
2+
predicate i32 IfChain(pointer p, i32 i) {
3+
if (i <= 0i32) {
4+
return 0i32;
5+
} else if (i == 1i32) {
6+
take X = Owned<int>(p);
7+
return 0i32;
8+
} else {
9+
take X = Owned<int>(p);
10+
take X2 = Owned(array_shift<int>(p,1u64));
11+
return 0i32;
12+
}
13+
}
14+
@*/
15+
16+
int main()
17+
{
18+
19+
return 0;
20+
}

tests/cn/predicate_else_if.c.verify

+5
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
return code: 0
2+
tests/cn/predicate_else_if.c:6:16: warning: deprecated keyword 'Owned', use 'RW' instead
3+
take X = Owned<int>(p);
4+
^~~~~
5+
[1/1]: main -- pass

0 commit comments

Comments
 (0)