[kernel] Add a test that status_by_call terminates

tests/spec/oracle/status_by_call_issue_890.res.oracle

+[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;
+}
+
+

tests/spec/status_by_call_issue_890.i

+/* 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);
+}

tests/spec/status_by_call_issue_890.ml

+let () =
+  Db.Main.extend
+    (fun () -> Globals.Functions.iter Statuses_by_call.setup_all_preconditions_proxies)