From c55b78426d9b6810f5e424815ca129695dd35b48 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Fri, 18 Sep 2020 15:45:37 +0200
Subject: [PATCH] [wp] Test that RefUsage takes lemmas in account
---
.../oracle/ref-usage-lemmas.res.oracle | 19 +++++++++++
.../wp/tests/wp_usage/ref-usage-lemmas.i | 34 +++++++++++++++++++
2 files changed, 53 insertions(+)
create mode 100644 src/plugins/wp/tests/wp_usage/oracle/ref-usage-lemmas.res.oracle
create mode 100644 src/plugins/wp/tests/wp_usage/ref-usage-lemmas.i
diff --git a/src/plugins/wp/tests/wp_usage/oracle/ref-usage-lemmas.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/ref-usage-lemmas.res.oracle
new file mode 100644
index 00000000000..a22e16a5c31
--- /dev/null
+++ b/src/plugins/wp/tests/wp_usage/oracle/ref-usage-lemmas.res.oracle
@@ -0,0 +1,19 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_usage/ref-usage-lemmas.i (no preprocessing)
+[wp] Running WP plugin...
+.................................................
+... Ref Usage
+.................................................
+Init: { &a b }
+Function foo: { &a b *x }
+Function main: { &a b __retres }
+.................................................
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+ Function main
+------------------------------------------------------------
+
+Goal Pre-condition (file tests/wp_usage/ref-usage-lemmas.i, line 30) in 'main':
+Prove: true.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_usage/ref-usage-lemmas.i b/src/plugins/wp/tests/wp_usage/ref-usage-lemmas.i
new file mode 100644
index 00000000000..77c4c585522
--- /dev/null
+++ b/src/plugins/wp/tests/wp_usage/ref-usage-lemmas.i
@@ -0,0 +1,34 @@
+/* run.config
+ OPT: -wp-msg-key refusage
+*/
+/* run.config_qualif
+ DONTRUN:
+*/
+
+int a ;
+int b ;
+
+/*@ axiomatic A{
+ logic int* get reads \nothing ;
+ logic int* get_h = &a ;
+
+ axiom a: get_h == get ;
+ }
+
+*/
+
+/*@ axiomatic B{
+ logic integer value reads \nothing ;
+ axiom b: value == b ;
+ }
+*/
+
+void foo(int* x){
+ *x = a = b ;
+}
+
+/*@ requires a <= b ; */
+int main(void){
+ int e ;
+ foo(&e) ;
+}
--
GitLab