diff --git a/tests/spec/oracle/status_by_call_issue_890.res.oracle b/tests/spec/oracle/status_by_call_issue_890.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..33e76da4d07f848c16531e3c1fa56d9c8828261c --- /dev/null +++ b/tests/spec/oracle/status_by_call_issue_890.res.oracle @@ -0,0 +1,24 @@ +[kernel] Parsing tests/spec/status_by_call_issue_890.i (no preprocessing) +/* Generated by Frama-C */ +struct list { + struct list *next ; +}; +/*@ axiomatic Ax { + predicate P(struct list *root) ; + + } + */ +/*@ requires P(l); */ +int len(struct list *l) +{ + int tmp_0; + if (l == (struct list *)0) tmp_0 = 0; + else { + int tmp; + tmp = len(l->next); + tmp_0 = 1 + tmp; + } + return tmp_0; +} + + diff --git a/tests/spec/status_by_call_issue_890.i b/tests/spec/status_by_call_issue_890.i new file mode 100644 index 0000000000000000000000000000000000000000..d3209b6bea950aca95d9ac3a3ec582596fade641 --- /dev/null +++ b/tests/spec/status_by_call_issue_890.i @@ -0,0 +1,12 @@ +/* run.config + MODULE: @PTEST_DIR@/@PTEST_NAME@.cmxs +*/ + +struct list { struct list *next; }; + +/*@ axiomatic Ax { predicate P(struct list * root) ; } */ + +/*@ requires P(l); @*/ +int len(struct list * l){ + return (l == (void*)0) ? 0 : 1 + len(l->next); +} diff --git a/tests/spec/status_by_call_issue_890.ml b/tests/spec/status_by_call_issue_890.ml new file mode 100644 index 0000000000000000000000000000000000000000..374e927700b937885f27c029f3d1744110d9ea39 --- /dev/null +++ b/tests/spec/status_by_call_issue_890.ml @@ -0,0 +1,3 @@ +let () = + Db.Main.extend + (fun () -> Globals.Functions.iter Statuses_by_call.setup_all_preconditions_proxies)