From 529093555a14d2031e4ca16a5b601da7dd88edc0 Mon Sep 17 00:00:00 2001
From: Thibault Martin <thi.martin.pro@pm.me>
Date: Tue, 1 Aug 2023 11:49:54 +0200
Subject: [PATCH] Add tests and oracles for Populate_spec
---
tests/spec/default_spec_combine.i | 67 +++++++++++++
tests/spec/default_spec_combine.ml | 28 ++++++
tests/spec/default_spec_custom.i | 20 ++++
tests/spec/default_spec_custom.ml | 42 ++++++++
tests/spec/default_spec_mode.i | 32 ++++++
.../oracle/default_spec_combine.0.res.oracle | 83 ++++++++++++++++
.../oracle/default_spec_combine.1.res.oracle | 90 +++++++++++++++++
.../oracle/default_spec_combine.2.res.oracle | 99 +++++++++++++++++++
.../oracle/default_spec_custom.0.res.oracle | 48 +++++++++
.../oracle/default_spec_custom.1.res.oracle | 39 ++++++++
.../oracle/default_spec_custom.2.res.oracle | 5 +
.../oracle/default_spec_mode.0.res.oracle | 22 +++++
.../oracle/default_spec_mode.1.res.oracle | 22 +++++
.../oracle/default_spec_mode.2.res.oracle | 30 ++++++
.../oracle/default_spec_mode.3.res.oracle | 34 +++++++
.../oracle/default_spec_mode.4.res.oracle | 40 ++++++++
.../oracle/default_spec_mode.5.res.oracle | 35 +++++++
.../oracle/default_spec_mode.6.res.oracle | 4 +
.../oracle/default_spec_mode.7.res.oracle | 4 +
19 files changed, 744 insertions(+)
create mode 100644 tests/spec/default_spec_combine.i
create mode 100644 tests/spec/default_spec_combine.ml
create mode 100644 tests/spec/default_spec_custom.i
create mode 100644 tests/spec/default_spec_custom.ml
create mode 100644 tests/spec/default_spec_mode.i
create mode 100644 tests/spec/oracle/default_spec_combine.0.res.oracle
create mode 100644 tests/spec/oracle/default_spec_combine.1.res.oracle
create mode 100644 tests/spec/oracle/default_spec_combine.2.res.oracle
create mode 100644 tests/spec/oracle/default_spec_custom.0.res.oracle
create mode 100644 tests/spec/oracle/default_spec_custom.1.res.oracle
create mode 100644 tests/spec/oracle/default_spec_custom.2.res.oracle
create mode 100644 tests/spec/oracle/default_spec_mode.0.res.oracle
create mode 100644 tests/spec/oracle/default_spec_mode.1.res.oracle
create mode 100644 tests/spec/oracle/default_spec_mode.2.res.oracle
create mode 100644 tests/spec/oracle/default_spec_mode.3.res.oracle
create mode 100644 tests/spec/oracle/default_spec_mode.4.res.oracle
create mode 100644 tests/spec/oracle/default_spec_mode.5.res.oracle
create mode 100644 tests/spec/oracle/default_spec_mode.6.res.oracle
create mode 100644 tests/spec/oracle/default_spec_mode.7.res.oracle
diff --git a/tests/spec/default_spec_combine.i b/tests/spec/default_spec_combine.i
new file mode 100644
index 00000000000..7910730ee26
--- /dev/null
+++ b/tests/spec/default_spec_combine.i
@@ -0,0 +1,67 @@
+/* run.config
+
+ MODULE: @PTEST_NAME@
+ STDOPT: +"-generated-spec-mode donothing"
+ STDOPT: +"-generated-spec-mode safe"
+ STDOPT: +"-generated-spec-mode frama-c"
+*/
+
+/*@ axiomatic a {
+ @ predicate P reads \nothing;
+ @ predicate Q reads \nothing;
+ @ predicate R reads \nothing;
+ }*/
+
+
+// Test combine exits
+/*@ behavior A:
+ @ exits P;
+ @ behavior B:
+ @ exits Q;
+ @ exits R;
+ @ complete behaviors;
+ @*/
+void f1(void);
+
+// Test combine assigns
+/*@ behavior A:
+ @ assigns *a;
+ @ behavior B:
+ @ assigns *b;
+ @ assigns *a \from c;
+ @ assigns *a \from d;
+ @ assigns *b \from c;
+ @ behavior C:
+ @ assigns *a, *b;
+ @ complete behaviors;
+ @*/
+void f2(int* a, int *b, int c, int d);
+
+// Test combine requires
+/*@ behavior A:
+ @ requires P;
+ @ requires Q;
+ @ behavior B:
+ @ requires P;
+ @ requires R;
+ @ requires R;
+ @ complete behaviors;
+ @*/
+void f3(void);
+
+// Test combine frees/allocates
+/*@ behavior A:
+ @ allocates \result;
+ @ allocates \old(a);
+ @ frees b;
+ @ behavior B:
+ @ allocates \result;
+ @ allocates \old(a);
+ @ allocates \old(b);
+ @ frees \nothing;
+ @ behavior C:
+ @ allocates \nothing;
+ @ frees a, b;
+ @ complete behaviors;
+ @*/
+int* f4(int* a, int* b);
diff --git a/tests/spec/default_spec_combine.ml b/tests/spec/default_spec_combine.ml
new file mode 100644
index 00000000000..dd81d458061
--- /dev/null
+++ b/tests/spec/default_spec_combine.ml
@@ -0,0 +1,28 @@
+open Cil_types
+
+let gen_exits _ _ = [ ]
+let status_exits = Property_status.Dont_know
+
+let gen_assigns _ _ = WritesAny
+let status_assigns = Property_status.Dont_know
+
+let gen_requires _ _ = [ ]
+
+let gen_allocates _ _ = FreeAllocAny
+let status_allocates = Property_status.Dont_know
+
+let gen_terminates _ _ = None
+let status_terminates = Property_status.Dont_know
+
+let populate () =
+ Format.printf "Registering an mode that does nothing@.";
+ Populate_spec.register
+ ~gen_exits ~status_exits
+ ~gen_assigns ~status_assigns
+ ~gen_requires
+ ~gen_allocates ~status_allocates
+ ~gen_terminates ~status_terminates
+ "donothing"
+
+
+ let () = Cmdline.run_after_configuring_stage populate
diff --git a/tests/spec/default_spec_custom.i b/tests/spec/default_spec_custom.i
new file mode 100644
index 00000000000..e7ccb0aff38
--- /dev/null
+++ b/tests/spec/default_spec_custom.i
@@ -0,0 +1,20 @@
+/* run.config
+ MODULE: @PTEST_NAME@
+ STDOPT: +"-generated-spec-mode emptymode"
+ STDOPT: +"-generated-spec-mode mymode"
+ EXIT: 1
+ STDOPT: +"-generated-spec-mode notregisteredmode"
+*/
+
+void f1(void);
+
+void f2(){
+ f1();
+ return;
+}
+
+int f3(int* a);
+
+int f4(int* b){
+ return f3(b);
+}
diff --git a/tests/spec/default_spec_custom.ml b/tests/spec/default_spec_custom.ml
new file mode 100644
index 00000000000..5220b814145
--- /dev/null
+++ b/tests/spec/default_spec_custom.ml
@@ -0,0 +1,42 @@
+open Cil_types
+
+let gen_exits _ _ =
+ [ Exits, Logic_const.(new_predicate pfalse) ]
+
+
+let gen_assigns kf _ =
+ if Kernel_function.has_definition kf then
+ WritesAny
+ else Writes (Infer_annotations.assigns_from_prototype kf)
+
+let gen_requires _ _ = [ Logic_const.(new_predicate pfalse) ]
+
+let gen_allocates kf _ =
+ if Kernel_function.has_definition kf
+ then FreeAlloc([],[])
+ else FreeAllocAny
+
+let gen_terminates kf _ =
+ if Kernel_function.has_definition kf then
+ None
+ else Some(Logic_const.(new_predicate pfalse))
+
+let status_exits = Property_status.Dont_know
+let status_assigns = Property_status.True
+let status_allocates = Property_status.Dont_know
+let status_terminates = Property_status.Dont_know
+
+let populate () =
+ Format.printf "Registering an empty spec generation mode@.";
+ Populate_spec.register "emptymode";
+ Format.printf "Registering a new spec generation mode@.";
+ Populate_spec.register
+ ~gen_exits ~status_exits
+ ~gen_assigns ~status_assigns
+ ~gen_requires
+ ~gen_allocates ~status_allocates
+ ~gen_terminates ~status_terminates
+ "mymode"
+
+
+ let () = Cmdline.run_after_configuring_stage populate
diff --git a/tests/spec/default_spec_mode.i b/tests/spec/default_spec_mode.i
new file mode 100644
index 00000000000..5ddda215b76
--- /dev/null
+++ b/tests/spec/default_spec_mode.i
@@ -0,0 +1,32 @@
+/* run.config
+ STDOPT: +"-no-generate-default-spec"
+ STDOPT: +"-generated-spec-mode skip"
+ STDOPT: +"-generated-spec-mode acsl"
+ STDOPT: +"-generated-spec-mode safe"
+ STDOPT: +"-generated-spec-mode frama-c"
+ STDOPT: +"-generated-spec-custom exits:acsl,assigns:frama-c,requires:safe,allocates:safe,terminates:acsl"
+
+ EXIT: 1
+ STDOPT: +"-generated-spec-custom wrong_clause:safe"
+ STDOPT: +"-generated-spec-custom wrong_clause:"
+*/
+
+// empty spec prototype
+void f1(void);
+
+// empty spec function
+void f2(){
+ f1();
+ return;
+}
+
+// Test for automatic assigns
+int f3(int* a);
+
+// Has behavior by default
+/*@ requires \true;
+ @ assigns *b;
+*/
+int f4(int* b){
+ return f3(b);
+}
diff --git a/tests/spec/oracle/default_spec_combine.0.res.oracle b/tests/spec/oracle/default_spec_combine.0.res.oracle
new file mode 100644
index 00000000000..35690113209
--- /dev/null
+++ b/tests/spec/oracle/default_spec_combine.0.res.oracle
@@ -0,0 +1,83 @@
+Registering an mode that does nothing
+[kernel] Parsing default_spec_combine.i (no preprocessing)
+/* Generated by Frama-C */
+/*@
+axiomatic a {
+ predicate P
+ reads \nothing;
+
+ predicate Q
+ reads \nothing;
+
+ predicate R
+ reads \nothing;
+
+ }
+ */
+/*@ exits P ∨ Q ∨ R;
+
+ behavior A:
+ exits P;
+
+ behavior B:
+ exits Q;
+ exits R;
+
+ complete behaviors B, A;
+ */
+void f1(void);
+
+/*@ assigns *a, *b;
+ assigns *a \from c;
+ assigns *a \from d;
+ assigns *b \from c;
+
+ behavior A:
+ assigns *a;
+
+ behavior B:
+ assigns *b, *a;
+ assigns *b \from c;
+ assigns *a \from c;
+ assigns *a \from d;
+
+ behavior C:
+ assigns *a, *b;
+
+ complete behaviors C, B, A;
+ */
+void f2(int *a, int *b, int c, int d);
+
+/*@ requires (P ∧ Q) ∨ (P ∧ R);
+
+ behavior A:
+ requires P;
+ requires Q;
+
+ behavior B:
+ requires P;
+ requires R;
+ requires R;
+
+ complete behaviors B, A;
+ */
+void f3(void);
+
+/*@ frees a, b;
+ allocates \result, \old(a), \old(b);
+
+ behavior A:
+ frees b;
+ allocates \result, \old(a);
+
+ behavior B:
+ allocates \result, \old(a), \old(b);
+
+ behavior C:
+ frees a, b;
+
+ complete behaviors C, B, A;
+ */
+int *f4(int *a, int *b);
+
+
diff --git a/tests/spec/oracle/default_spec_combine.1.res.oracle b/tests/spec/oracle/default_spec_combine.1.res.oracle
new file mode 100644
index 00000000000..0a1534d061e
--- /dev/null
+++ b/tests/spec/oracle/default_spec_combine.1.res.oracle
@@ -0,0 +1,90 @@
+Registering an mode that does nothing
+[kernel] Parsing default_spec_combine.i (no preprocessing)
+/* Generated by Frama-C */
+/*@
+axiomatic a {
+ predicate P
+ reads \nothing;
+
+ predicate Q
+ reads \nothing;
+
+ predicate R
+ reads \nothing;
+
+ }
+ */
+/*@ requires \false;
+ terminates \false;
+ exits P ∨ Q ∨ R;
+
+ behavior A:
+ exits P;
+
+ behavior B:
+ exits Q;
+ exits R;
+
+ complete behaviors B, A;
+ */
+void f1(void);
+
+/*@ requires \false;
+ terminates \false;
+ assigns *a, *b;
+ assigns *a \from c;
+ assigns *a \from d;
+ assigns *b \from c;
+
+ behavior A:
+ assigns *a;
+
+ behavior B:
+ assigns *b, *a;
+ assigns *b \from c;
+ assigns *a \from c;
+ assigns *a \from d;
+
+ behavior C:
+ assigns *a, *b;
+
+ complete behaviors C, B, A;
+ */
+void f2(int *a, int *b, int c, int d);
+
+/*@ requires (P ∧ Q) ∨ (P ∧ R);
+ terminates \false;
+
+ behavior A:
+ requires P;
+ requires Q;
+
+ behavior B:
+ requires P;
+ requires R;
+ requires R;
+
+ complete behaviors B, A;
+ */
+void f3(void);
+
+/*@ requires \false;
+ terminates \false;
+ frees a, b;
+ allocates \result, \old(a), \old(b);
+
+ behavior A:
+ frees b;
+ allocates \result, \old(a);
+
+ behavior B:
+ allocates \result, \old(a), \old(b);
+
+ behavior C:
+ frees a, b;
+
+ complete behaviors C, B, A;
+ */
+int *f4(int *a, int *b);
+
+
diff --git a/tests/spec/oracle/default_spec_combine.2.res.oracle b/tests/spec/oracle/default_spec_combine.2.res.oracle
new file mode 100644
index 00000000000..9d91be61fde
--- /dev/null
+++ b/tests/spec/oracle/default_spec_combine.2.res.oracle
@@ -0,0 +1,99 @@
+Registering an mode that does nothing
+[kernel] Parsing default_spec_combine.i (no preprocessing)
+/* Generated by Frama-C */
+/*@
+axiomatic a {
+ predicate P
+ reads \nothing;
+
+ predicate Q
+ reads \nothing;
+
+ predicate R
+ reads \nothing;
+
+ }
+ */
+/*@ terminates \true;
+ exits P ∨ Q ∨ R;
+ assigns \nothing;
+ allocates \nothing;
+
+ behavior A:
+ exits P;
+
+ behavior B:
+ exits Q;
+ exits R;
+
+ complete behaviors B, A;
+ */
+void f1(void);
+
+/*@ terminates \true;
+ exits \false;
+ assigns *a, *b;
+ assigns *a \from c;
+ assigns *a \from d;
+ assigns *b \from c;
+ allocates \nothing;
+
+ behavior A:
+ assigns *a;
+
+ behavior B:
+ assigns *b, *a;
+ assigns *b \from c;
+ assigns *a \from c;
+ assigns *a \from d;
+
+ behavior C:
+ assigns *a, *b;
+
+ complete behaviors C, B, A;
+ */
+void f2(int *a, int *b, int c, int d);
+
+/*@ requires (P ∧ Q) ∨ (P ∧ R);
+ terminates \true;
+ exits \false;
+ assigns \nothing;
+ allocates \nothing;
+
+ behavior A:
+ requires P;
+ requires Q;
+
+ behavior B:
+ requires P;
+ requires R;
+ requires R;
+
+ complete behaviors B, A;
+ */
+void f3(void);
+
+/*@ terminates \true;
+ exits \false;
+ assigns \result, *a, *b;
+ assigns \result \from *a, *b;
+ assigns *a \from *a, *b;
+ assigns *b \from *a, *b;
+ frees a, b;
+ allocates \result, \old(a), \old(b);
+
+ behavior A:
+ frees b;
+ allocates \result, \old(a);
+
+ behavior B:
+ allocates \result, \old(a), \old(b);
+
+ behavior C:
+ frees a, b;
+
+ complete behaviors C, B, A;
+ */
+int *f4(int *a, int *b);
+
+
diff --git a/tests/spec/oracle/default_spec_custom.0.res.oracle b/tests/spec/oracle/default_spec_custom.0.res.oracle
new file mode 100644
index 00000000000..72faead364b
--- /dev/null
+++ b/tests/spec/oracle/default_spec_custom.0.res.oracle
@@ -0,0 +1,48 @@
+Registering an empty spec generation mode
+Registering a new spec generation mode
+[kernel] Parsing default_spec_custom.i (no preprocessing)
+[kernel] Warning: Custom generation from mode emptymode not defined for exits, using frama-c mode instead
+[kernel] Warning: Custom generation from mode emptymode not defined for assigns, using frama-c mode instead
+[kernel] Warning: Custom generation from mode emptymode not defined for requires, using frama-c mode instead
+[kernel] Warning: Custom generation from mode emptymode not defined for allocates, using frama-c mode instead
+[kernel] Warning: Custom generation from mode emptymode not defined for terminates, using frama-c mode instead
+[kernel] Warning: Custom status from mode emptymode not defined for exits
+[kernel] Warning: Custom status from mode emptymode not defined for assigns
+[kernel] Warning: Custom status from mode emptymode not defined for allocates
+[kernel] Warning: Custom status from mode emptymode not defined for terminates
+/* Generated by Frama-C */
+/*@ terminates \true;
+ exits \false;
+ assigns \nothing;
+ allocates \nothing; */
+void f1(void);
+
+/*@ terminates \true;
+ exits \false;
+ allocates \nothing; */
+void f2(void)
+{
+ f1();
+ return;
+}
+
+/*@ terminates \true;
+ exits \false;
+ assigns \result, *a;
+ assigns \result \from *a;
+ assigns *a \from *a;
+ allocates \nothing;
+ */
+int f3(int *a);
+
+/*@ terminates \true;
+ exits \false;
+ allocates \nothing; */
+int f4(int *b)
+{
+ int tmp;
+ tmp = f3(b);
+ return tmp;
+}
+
+
diff --git a/tests/spec/oracle/default_spec_custom.1.res.oracle b/tests/spec/oracle/default_spec_custom.1.res.oracle
new file mode 100644
index 00000000000..7c6188e9550
--- /dev/null
+++ b/tests/spec/oracle/default_spec_custom.1.res.oracle
@@ -0,0 +1,39 @@
+Registering an empty spec generation mode
+Registering a new spec generation mode
+[kernel] Parsing default_spec_custom.i (no preprocessing)
+/* Generated by Frama-C */
+/*@ requires \false;
+ terminates \false;
+ exits \false;
+ assigns \nothing; */
+void f1(void);
+
+/*@ requires \false;
+ exits \false;
+ allocates \nothing; */
+void f2(void)
+{
+ f1();
+ return;
+}
+
+/*@ requires \false;
+ terminates \false;
+ exits \false;
+ assigns \result, *a;
+ assigns \result \from *a;
+ assigns *a \from *a;
+ */
+int f3(int *a);
+
+/*@ requires \false;
+ exits \false;
+ allocates \nothing; */
+int f4(int *b)
+{
+ int tmp;
+ tmp = f3(b);
+ return tmp;
+}
+
+
diff --git a/tests/spec/oracle/default_spec_custom.2.res.oracle b/tests/spec/oracle/default_spec_custom.2.res.oracle
new file mode 100644
index 00000000000..8838712c46e
--- /dev/null
+++ b/tests/spec/oracle/default_spec_custom.2.res.oracle
@@ -0,0 +1,5 @@
+Registering an empty spec generation mode
+Registering a new spec generation mode
+[kernel] Parsing default_spec_custom.i (no preprocessing)
+[kernel] User Error: Mode notregisteredmode is not registered
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/spec/oracle/default_spec_mode.0.res.oracle b/tests/spec/oracle/default_spec_mode.0.res.oracle
new file mode 100644
index 00000000000..9624686acc4
--- /dev/null
+++ b/tests/spec/oracle/default_spec_mode.0.res.oracle
@@ -0,0 +1,22 @@
+[kernel] Parsing default_spec_mode.i (no preprocessing)
+/* Generated by Frama-C */
+void f1(void);
+
+void f2(void)
+{
+ f1();
+ return;
+}
+
+int f3(int *a);
+
+/*@ requires \true;
+ assigns *b; */
+int f4(int *b)
+{
+ int tmp;
+ tmp = f3(b);
+ return tmp;
+}
+
+
diff --git a/tests/spec/oracle/default_spec_mode.1.res.oracle b/tests/spec/oracle/default_spec_mode.1.res.oracle
new file mode 100644
index 00000000000..9624686acc4
--- /dev/null
+++ b/tests/spec/oracle/default_spec_mode.1.res.oracle
@@ -0,0 +1,22 @@
+[kernel] Parsing default_spec_mode.i (no preprocessing)
+/* Generated by Frama-C */
+void f1(void);
+
+void f2(void)
+{
+ f1();
+ return;
+}
+
+int f3(int *a);
+
+/*@ requires \true;
+ assigns *b; */
+int f4(int *b)
+{
+ int tmp;
+ tmp = f3(b);
+ return tmp;
+}
+
+
diff --git a/tests/spec/oracle/default_spec_mode.2.res.oracle b/tests/spec/oracle/default_spec_mode.2.res.oracle
new file mode 100644
index 00000000000..ecda6945556
--- /dev/null
+++ b/tests/spec/oracle/default_spec_mode.2.res.oracle
@@ -0,0 +1,30 @@
+[kernel] Parsing default_spec_mode.i (no preprocessing)
+/* Generated by Frama-C */
+/*@ terminates \true;
+ allocates \nothing; */
+void f1(void);
+
+/*@ terminates \true;
+ allocates \nothing; */
+void f2(void)
+{
+ f1();
+ return;
+}
+
+/*@ terminates \true;
+ allocates \nothing; */
+int f3(int *a);
+
+/*@ requires \true;
+ terminates \true;
+ assigns *b;
+ allocates \nothing; */
+int f4(int *b)
+{
+ int tmp;
+ tmp = f3(b);
+ return tmp;
+}
+
+
diff --git a/tests/spec/oracle/default_spec_mode.3.res.oracle b/tests/spec/oracle/default_spec_mode.3.res.oracle
new file mode 100644
index 00000000000..9ae4d897289
--- /dev/null
+++ b/tests/spec/oracle/default_spec_mode.3.res.oracle
@@ -0,0 +1,34 @@
+[kernel] Parsing default_spec_mode.i (no preprocessing)
+/* Generated by Frama-C */
+/*@ requires \false;
+ terminates \false; */
+void f1(void);
+
+/*@ terminates \true;
+ exits \false;
+ assigns \nothing;
+ allocates \nothing; */
+void f2(void)
+{
+ f1();
+ return;
+}
+
+/*@ requires \false;
+ terminates \false; */
+int f3(int *a);
+
+/*@ requires \true;
+ terminates \true;
+ exits \false;
+ assigns *b;
+ allocates \nothing;
+ */
+int f4(int *b)
+{
+ int tmp;
+ tmp = f3(b);
+ return tmp;
+}
+
+
diff --git a/tests/spec/oracle/default_spec_mode.4.res.oracle b/tests/spec/oracle/default_spec_mode.4.res.oracle
new file mode 100644
index 00000000000..272ef95df50
--- /dev/null
+++ b/tests/spec/oracle/default_spec_mode.4.res.oracle
@@ -0,0 +1,40 @@
+[kernel] Parsing default_spec_mode.i (no preprocessing)
+/* Generated by Frama-C */
+/*@ terminates \true;
+ exits \false;
+ assigns \nothing;
+ allocates \nothing; */
+void f1(void);
+
+/*@ terminates \true;
+ exits \false;
+ allocates \nothing; */
+void f2(void)
+{
+ f1();
+ return;
+}
+
+/*@ terminates \true;
+ exits \false;
+ assigns \result, *a;
+ assigns \result \from *a;
+ assigns *a \from *a;
+ allocates \nothing;
+ */
+int f3(int *a);
+
+/*@ requires \true;
+ terminates \true;
+ exits \false;
+ assigns *b;
+ allocates \nothing;
+ */
+int f4(int *b)
+{
+ int tmp;
+ tmp = f3(b);
+ return tmp;
+}
+
+
diff --git a/tests/spec/oracle/default_spec_mode.5.res.oracle b/tests/spec/oracle/default_spec_mode.5.res.oracle
new file mode 100644
index 00000000000..1fa027e6baf
--- /dev/null
+++ b/tests/spec/oracle/default_spec_mode.5.res.oracle
@@ -0,0 +1,35 @@
+[kernel] Parsing default_spec_mode.i (no preprocessing)
+/* Generated by Frama-C */
+/*@ requires \false;
+ terminates \true;
+ assigns \nothing; */
+void f1(void);
+
+/*@ terminates \true;
+ allocates \nothing; */
+void f2(void)
+{
+ f1();
+ return;
+}
+
+/*@ requires \false;
+ terminates \true;
+ assigns \result, *a;
+ assigns \result \from *a;
+ assigns *a \from *a;
+ */
+int f3(int *a);
+
+/*@ requires \true;
+ terminates \true;
+ assigns *b;
+ allocates \nothing; */
+int f4(int *b)
+{
+ int tmp;
+ tmp = f3(b);
+ return tmp;
+}
+
+
diff --git a/tests/spec/oracle/default_spec_mode.6.res.oracle b/tests/spec/oracle/default_spec_mode.6.res.oracle
new file mode 100644
index 00000000000..0431517a924
--- /dev/null
+++ b/tests/spec/oracle/default_spec_mode.6.res.oracle
@@ -0,0 +1,4 @@
+[kernel] Parsing default_spec_mode.i (no preprocessing)
+[kernel] User Error: 'wrong_clause' is not a valid key for -generated-spec-custom.
+ Accepted keys are 'exits', 'assigns', 'requires', 'allocates' and 'terminates'.
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/spec/oracle/default_spec_mode.7.res.oracle b/tests/spec/oracle/default_spec_mode.7.res.oracle
new file mode 100644
index 00000000000..0431517a924
--- /dev/null
+++ b/tests/spec/oracle/default_spec_mode.7.res.oracle
@@ -0,0 +1,4 @@
+[kernel] Parsing default_spec_mode.i (no preprocessing)
+[kernel] User Error: 'wrong_clause' is not a valid key for -generated-spec-custom.
+ Accepted keys are 'exits', 'assigns', 'requires', 'allocates' and 'terminates'.
+[kernel] Frama-C aborted: invalid user input.
--
GitLab