From 6f36d3b19f3dd34c8d4b9fae05e0f66a08c1d7bd Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 23 Feb 2021 17:54:19 +0100
Subject: [PATCH] [wp] non-regression test for issue pub. 49
---
src/plugins/wp/tests/wp_bts/issue_pub_49.i | 90 ++++++++
.../wp_bts/oracle/issue_pub_49.res.oracle | 208 ++++++++++++++++++
.../oracle_qualif/issue_pub_49.res.oracle | 49 +++++
3 files changed, 347 insertions(+)
create mode 100644 src/plugins/wp/tests/wp_bts/issue_pub_49.i
create mode 100644 src/plugins/wp/tests/wp_bts/oracle/issue_pub_49.res.oracle
create mode 100644 src/plugins/wp/tests/wp_bts/oracle_qualif/issue_pub_49.res.oracle
diff --git a/src/plugins/wp/tests/wp_bts/issue_pub_49.i b/src/plugins/wp/tests/wp_bts/issue_pub_49.i
new file mode 100644
index 00000000000..13edc0d932a
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bts/issue_pub_49.i
@@ -0,0 +1,90 @@
+/*
+ Postcondition postcs of function caller1 is proven (fixed value for codeCursor) while codeCursor may be updated in function is_class.
+ Similar issue for caller2.
+ Hint: proof not achieved when instruction at label_useless_cond is removed as in caller3.
+ Hint: proof not achieved when t3 is not declared in the block as in caller4.
+ Used command to run the proof:
+ frama-c-gui assigns_postconditions.c -wp -wp-check-memory-model -wp-rte
+*/
+
+
+
+int codeCursor;
+
+/*@
+ assigns codeCursor;
+*/
+int is_class(void){
+ if (codeCursor < 10)
+ codeCursor++;
+ return 0;
+}
+
+
+/*@
+ assigns codeCursor;
+ ensures postcs: codeCursor == \old(codeCursor);
+*/
+int caller1(void){
+ int t1=1;
+ int t2=0;
+ int t3;
+
+ label_useless_cond: if (t1 == 7) return 1;
+
+ label_cond_1: if (t2 == 0) {int t3 = is_class(); return t3;}
+ //label_cond_2:if (t2 == 0) {t3 = is_class(); return t3;}
+ else return is_class();
+}
+
+
+/*@
+ assigns codeCursor;
+ ensures postcs: codeCursor == \old(codeCursor);
+*/
+int caller2(void){
+ int t1=1;
+ int t2=0;
+ int t3;
+
+ label_useless_cond: if (t1 == 7) return 1;
+
+ label_cond_1: if (t2 == 0) {return is_class();}
+ //label_cond_2:if (t2 == 0) {t3 = is_class(); return t3;}
+ else return is_class();
+}
+
+
+/*@
+ assigns codeCursor;
+ ensures postcs: codeCursor == \old(codeCursor);
+*/
+int caller3(void){
+ int t1=1;
+ int t2=0;
+ int t3;
+
+ //label_useless_cond: if (t1 == 7) return 1;
+
+ label_cond_1: if (t2 == 0) {int t3 = is_class(); return t3;}
+ //label_cond_2:if (t2 == 0) {t3 = is_class(); return t3;}
+ else return is_class();
+}
+
+
+/*@
+ assigns codeCursor;
+ ensures postcs: codeCursor == \old(codeCursor);
+*/
+int caller4(void){
+ int t1=1;
+ int t2=0;
+ int t3;
+
+ label_useless_cond: if (t1 == 7) return 1;
+
+ //label_cond_1: if (t2 == 0) {int t3 = is_class(); return t3;}
+ label_cond_2:if (t2 == 0) {t3 = is_class(); return t3;}
+ else return is_class();
+}
+
diff --git a/src/plugins/wp/tests/wp_bts/oracle/issue_pub_49.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/issue_pub_49.res.oracle
new file mode 100644
index 00000000000..3ca32f21c6c
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bts/oracle/issue_pub_49.res.oracle
@@ -0,0 +1,208 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_bts/issue_pub_49.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+ Function caller1
+------------------------------------------------------------
+
+Goal Post-condition 'postcs' in 'caller1':
+Assume { Type: is_sint32(codeCursor_1) /\ is_sint32(codeCursor_0). }
+Prove: codeCursor_0 = codeCursor_1.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_bts/issue_pub_49.i, line 25) in 'caller1':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_bts/issue_pub_49.i, line 25) in 'caller1' (1/6):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_bts/issue_pub_49.i, line 25) in 'caller1' (2/6):
+Effect at line 33
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_bts/issue_pub_49.i, line 25) in 'caller1' (3/6):
+Call Result at line 35
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_bts/issue_pub_49.i, line 25) in 'caller1' (4/6):
+Effect at line 35
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_bts/issue_pub_49.i, line 25) in 'caller1' (5/6):
+Call Result at line 37
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_bts/issue_pub_49.i, line 25) in 'caller1' (6/6):
+Effect at line 37
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function caller2
+------------------------------------------------------------
+
+Goal Post-condition 'postcs' in 'caller2':
+Assume { Type: is_sint32(codeCursor_1) /\ is_sint32(codeCursor_0). }
+Prove: codeCursor_0 = codeCursor_1.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_bts/issue_pub_49.i, line 42) in 'caller2':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_bts/issue_pub_49.i, line 42) in 'caller2' (1/6):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_bts/issue_pub_49.i, line 42) in 'caller2' (2/6):
+Effect at line 50
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_bts/issue_pub_49.i, line 42) in 'caller2' (3/6):
+Call Result at line 52
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_bts/issue_pub_49.i, line 42) in 'caller2' (4/6):
+Effect at line 52
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_bts/issue_pub_49.i, line 42) in 'caller2' (5/6):
+Call Result at line 54
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_bts/issue_pub_49.i, line 42) in 'caller2' (6/6):
+Effect at line 54
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function caller3
+------------------------------------------------------------
+
+Goal Post-condition 'postcs' in 'caller3':
+Assume { Type: is_sint32(codeCursor_1) /\ is_sint32(codeCursor_0). }
+Prove: codeCursor_0 = codeCursor_1.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_bts/issue_pub_49.i, line 59) in 'caller3':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_bts/issue_pub_49.i, line 59) in 'caller3' (1/5):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_bts/issue_pub_49.i, line 59) in 'caller3' (2/5):
+Call Result at line 69
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_bts/issue_pub_49.i, line 59) in 'caller3' (3/5):
+Effect at line 69
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_bts/issue_pub_49.i, line 59) in 'caller3' (4/5):
+Call Result at line 71
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_bts/issue_pub_49.i, line 59) in 'caller3' (5/5):
+Effect at line 71
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function caller4
+------------------------------------------------------------
+
+Goal Post-condition 'postcs' in 'caller4':
+Assume { Type: is_sint32(codeCursor_1) /\ is_sint32(codeCursor_0). }
+Prove: codeCursor_0 = codeCursor_1.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_bts/issue_pub_49.i, line 76) in 'caller4':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_bts/issue_pub_49.i, line 76) in 'caller4' (1/6):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_bts/issue_pub_49.i, line 76) in 'caller4' (2/6):
+Effect at line 84
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_bts/issue_pub_49.i, line 76) in 'caller4' (3/6):
+Call Result at line 87
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_bts/issue_pub_49.i, line 76) in 'caller4' (4/6):
+Effect at line 87
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_bts/issue_pub_49.i, line 76) in 'caller4' (5/6):
+Call Result at line 88
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_bts/issue_pub_49.i, line 76) in 'caller4' (6/6):
+Effect at line 88
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function is_class
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_bts/issue_pub_49.i, line 15) in 'is_class' (1/2):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_bts/issue_pub_49.i, line 15) in 'is_class' (2/2):
+Effect at line 20
+Prove: true.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_pub_49.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_pub_49.res.oracle
new file mode 100644
index 00000000000..76e0835aa27
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_pub_49.res.oracle
@@ -0,0 +1,49 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_bts/issue_pub_49.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+[wp] 33 goals scheduled
+[wp] [Qed] Goal typed_is_class_assigns_part1 : Valid
+[wp] [Qed] Goal typed_is_class_assigns_part2 : Valid
+[wp] [Alt-Ergo] Goal typed_caller1_ensures_postcs : Unsuccess
+[wp] [Qed] Goal typed_caller1_assigns_exit : Valid
+[wp] [Qed] Goal typed_caller1_assigns_normal_part1 : Valid
+[wp] [Qed] Goal typed_caller1_assigns_normal_part2 : Valid
+[wp] [Qed] Goal typed_caller1_assigns_normal_part3 : Valid
+[wp] [Qed] Goal typed_caller1_assigns_normal_part4 : Valid
+[wp] [Qed] Goal typed_caller1_assigns_normal_part5 : Valid
+[wp] [Qed] Goal typed_caller1_assigns_normal_part6 : Valid
+[wp] [Alt-Ergo] Goal typed_caller2_ensures_postcs : Unsuccess
+[wp] [Qed] Goal typed_caller2_assigns_exit : Valid
+[wp] [Qed] Goal typed_caller2_assigns_normal_part1 : Valid
+[wp] [Qed] Goal typed_caller2_assigns_normal_part2 : Valid
+[wp] [Qed] Goal typed_caller2_assigns_normal_part3 : Valid
+[wp] [Qed] Goal typed_caller2_assigns_normal_part4 : Valid
+[wp] [Qed] Goal typed_caller2_assigns_normal_part5 : Valid
+[wp] [Qed] Goal typed_caller2_assigns_normal_part6 : Valid
+[wp] [Alt-Ergo] Goal typed_caller3_ensures_postcs : Unsuccess
+[wp] [Qed] Goal typed_caller3_assigns_exit : Valid
+[wp] [Qed] Goal typed_caller3_assigns_normal_part1 : Valid
+[wp] [Qed] Goal typed_caller3_assigns_normal_part2 : Valid
+[wp] [Qed] Goal typed_caller3_assigns_normal_part3 : Valid
+[wp] [Qed] Goal typed_caller3_assigns_normal_part4 : Valid
+[wp] [Qed] Goal typed_caller3_assigns_normal_part5 : Valid
+[wp] [Alt-Ergo] Goal typed_caller4_ensures_postcs : Unsuccess
+[wp] [Qed] Goal typed_caller4_assigns_exit : Valid
+[wp] [Qed] Goal typed_caller4_assigns_normal_part1 : Valid
+[wp] [Qed] Goal typed_caller4_assigns_normal_part2 : Valid
+[wp] [Qed] Goal typed_caller4_assigns_normal_part3 : Valid
+[wp] [Qed] Goal typed_caller4_assigns_normal_part4 : Valid
+[wp] [Qed] Goal typed_caller4_assigns_normal_part5 : Valid
+[wp] [Qed] Goal typed_caller4_assigns_normal_part6 : Valid
+[wp] Proved goals: 29 / 33
+ Qed: 29
+ Alt-Ergo: 0 (unsuccess: 4)
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ is_class 2 - 2 100%
+ caller1 7 - 8 87.5%
+ caller2 7 - 8 87.5%
+ caller3 6 - 7 85.7%
+ caller4 7 - 8 87.5%
+------------------------------------------------------------
--
GitLab