From 726e1225b1e61c11231dfa20bff8cb1b1c1c6ce3 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Fri, 10 Jul 2020 15:12:41 +0200
Subject: [PATCH] [kernel] Add a test that status_by_call terminates
---
.../status_by_call_issue_890.res.oracle | 24 +++++++++++++++++++
tests/spec/status_by_call_issue_890.i | 12 ++++++++++
tests/spec/status_by_call_issue_890.ml | 3 +++
3 files changed, 39 insertions(+)
create mode 100644 tests/spec/oracle/status_by_call_issue_890.res.oracle
create mode 100644 tests/spec/status_by_call_issue_890.i
create mode 100644 tests/spec/status_by_call_issue_890.ml
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 00000000000..33e76da4d07
--- /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 00000000000..d3209b6bea9
--- /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 00000000000..374e927700b
--- /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)
--
GitLab