From 5eff574f16124022c8048bf61d1e41f95c3c9926 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Fri, 22 Jan 2021 12:13:55 +0100
Subject: [PATCH] [aorai] moving back Error translation to initial guard in
serial.ya
---
.../aorai/tests/ya/oracle/serial.res.oracle | 262 +++++++++++++++---
.../tests/ya/oracle_prove/serial.res.oracle | 6 +-
src/plugins/aorai/tests/ya/serial.ya | 2 +-
src/plugins/aorai/tests/ya/serial_wp.ya | 2 +-
4 files changed, 227 insertions(+), 45 deletions(-)
diff --git a/src/plugins/aorai/tests/ya/oracle/serial.res.oracle b/src/plugins/aorai/tests/ya/oracle/serial.res.oracle
index 6cc4d3484ec..668ee72c09b 100644
--- a/src/plugins/aorai/tests/ya/oracle/serial.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/serial.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing tests/ya/serial.c (with preprocessing)
-[kernel:annot:missing-spec] tests/ya/serial.c:43: Warning:
+[kernel:annot:missing-spec] tests/ya/serial.c:56: Warning:
Neither code nor specification for function Frama_C_show_aorai_state, generating default assigns from the prototype
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
@@ -18,36 +18,36 @@
aorai_StatesHistory_1 ∈ {19}
aorai_StatesHistory_2 ∈ {19}
[eva] using specification for function Frama_C_interval
-[eva] tests/ya/serial.c:45: starting to merge loop iterations
-[eva] tests/ya/serial.c:50: Trace partitioning superposing up to 100 states
-[eva] tests/ya/serial.c:50: Trace partitioning superposing up to 300 states
-[aorai] tests/ya/serial.c:79: Wait1 <- Wait1 <- Complete
-[aorai] tests/ya/serial.c:79: n in {5},x in [0..16383],y in [8192..16383]
-[aorai] tests/ya/serial.c:79: Error <- Error <- Complete
-[aorai] tests/ya/serial.c:79: n in {5},x in [0..16383],y in [8192..16383]
-[aorai] tests/ya/serial.c:79: Complete <- Complete <- Complete
-[aorai] tests/ya/serial.c:79: n in {5},x in [0..16383],y in [8192..16383]
-[aorai] tests/ya/serial.c:79: Wait1 <- Wait1 <- Complete
-[aorai] tests/ya/serial.c:79: n in {5},x in [0..16383],y in [0..8191]
-[aorai] tests/ya/serial.c:79: Error <- Error <- Complete
-[aorai] tests/ya/serial.c:79: n in {5},x in [0..16383],y in [0..8191]
-[aorai] tests/ya/serial.c:79: Complete <- Complete <- Complete
-[aorai] tests/ya/serial.c:79: n in {5},x in [0..16383],y in [0..8191]
-[eva] tests/ya/serial.c:50: Trace partitioning superposing up to 500 states
-[eva:alarm] tests/ya/serial.c:52: Warning:
+[eva] tests/ya/serial.c:58: starting to merge loop iterations
+[eva] tests/ya/serial.c:63: Trace partitioning superposing up to 100 states
+[eva] tests/ya/serial.c:63: Trace partitioning superposing up to 300 states
+[aorai] tests/ya/serial.c:92: Wait1 <- Wait1 <- Complete
+[aorai] tests/ya/serial.c:92: n in {5},x in [0..16383],y in [8192..16383]
+[aorai] tests/ya/serial.c:92: Error <- Error <- Complete
+[aorai] tests/ya/serial.c:92: n in {5},x in [0..16383],y in [8192..16383]
+[aorai] tests/ya/serial.c:92: Complete <- Complete <- Complete
+[aorai] tests/ya/serial.c:92: n in {5},x in [0..16383],y in [8192..16383]
+[aorai] tests/ya/serial.c:92: Wait1 <- Wait1 <- Complete
+[aorai] tests/ya/serial.c:92: n in {5},x in [0..16383],y in [0..8191]
+[aorai] tests/ya/serial.c:92: Error <- Error <- Complete
+[aorai] tests/ya/serial.c:92: n in {5},x in [0..16383],y in [0..8191]
+[aorai] tests/ya/serial.c:92: Complete <- Complete <- Complete
+[aorai] tests/ya/serial.c:92: n in {5},x in [0..16383],y in [0..8191]
+[eva] tests/ya/serial.c:63: Trace partitioning superposing up to 500 states
+[eva:alarm] tests/ya/serial.c:65: Warning:
accessing uninitialized left-value. assert \initialized(&status);
-[eva] tests/ya/serial.c:50: Trace partitioning superposing up to 700 states
-[eva] tests/ya/serial.c:50: Trace partitioning superposing up to 900 states
-[eva] tests/ya/serial.c:50: Trace partitioning superposing up to 1200 states
-[eva] tests/ya/serial.c:50: Trace partitioning superposing up to 1500 states
-[aorai] tests/ya/serial.c:79: Error <- Error <- Error
-[aorai] tests/ya/serial.c:79: n in {5},x in [0..16383],y in [8192..16383]
-[aorai] tests/ya/serial.c:79: Error <- Error <- Error
-[aorai] tests/ya/serial.c:79: n in {5},x in [0..16383],y in [0..8191]
-[eva] tests/ya/serial.c:50: Trace partitioning superposing up to 1700 states
-[eva] tests/ya/serial.c:50: Trace partitioning superposing up to 1900 states
-[eva] tests/ya/serial.c:50: Trace partitioning superposing up to 2000 states
-[eva] tests/ya/serial.c:50: Trace partitioning superposing up to 2100 states
+[eva] tests/ya/serial.c:63: Trace partitioning superposing up to 700 states
+[eva] tests/ya/serial.c:63: Trace partitioning superposing up to 900 states
+[eva] tests/ya/serial.c:63: Trace partitioning superposing up to 1200 states
+[eva] tests/ya/serial.c:63: Trace partitioning superposing up to 1500 states
+[aorai] tests/ya/serial.c:92: Error <- Error <- Error
+[aorai] tests/ya/serial.c:92: n in {5},x in [0..16383],y in [8192..16383]
+[aorai] tests/ya/serial.c:92: Error <- Error <- Error
+[aorai] tests/ya/serial.c:92: n in {5},x in [0..16383],y in [0..8191]
+[eva] tests/ya/serial.c:63: Trace partitioning superposing up to 1700 states
+[eva] tests/ya/serial.c:63: Trace partitioning superposing up to 1900 states
+[eva] tests/ya/serial.c:63: Trace partitioning superposing up to 2000 states
+[eva] tests/ya/serial.c:63: Trace partitioning superposing up to 2100 states
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function input_data_post_func:
@@ -304,9 +304,8 @@
100% of the logical properties reached have been proven.
----------------------------------------------------------------------------
[kernel] Parsing TMPDIR/aorai_serial_0.i (no preprocessing)
-[kernel:typing:implicit-function-declaration] TMPDIR/aorai_serial_0.i:174: Warning:
- Calling undeclared function Frama_C_interval. Old style K&R code?
/* Generated by Frama-C */
+typedef unsigned long size_t;
enum aorai_States {
aorai_reject_state = -2,
Complete = 0,
@@ -345,6 +344,193 @@ enum aorai_OpStatusList {
};
/* compiler builtin:
void Frama_C_show_aorai_state(...); */
+extern int volatile Frama_C_entropy_source __attribute__((__unused__));
+
+/*@ requires valid_p: \valid(p + (0 .. l - 1));
+ ensures initialization: \initialized(\old(p) + (0 .. \old(l) - 1));
+ assigns *(p + (0 .. l - 1)), Frama_C_entropy_source;
+ assigns *(p + (0 .. l - 1)) \from Frama_C_entropy_source;
+ assigns Frama_C_entropy_source \from Frama_C_entropy_source;
+ */
+extern void Frama_C_make_unknown(char *p, size_t l);
+
+/*@ ensures result_a_or_b: \result ≡ \old(a) ∨ \result ≡ \old(b);
+ assigns \result, Frama_C_entropy_source;
+ assigns \result \from a, b, Frama_C_entropy_source;
+ assigns Frama_C_entropy_source \from Frama_C_entropy_source;
+ */
+extern int Frama_C_nondet(int a, int b);
+
+/*@ ensures result_a_or_b: \result ≡ \old(a) ∨ \result ≡ \old(b);
+ assigns \result, Frama_C_entropy_source;
+ assigns \result \from a, b, Frama_C_entropy_source;
+ assigns Frama_C_entropy_source \from Frama_C_entropy_source;
+ */
+extern void *Frama_C_nondet_ptr(void *a, void *b);
+
+/*@ requires order: min ≤ max;
+ ensures result_bounded: \old(min) ≤ \result ≤ \old(max);
+ assigns \result, Frama_C_entropy_source;
+ assigns \result \from min, max, Frama_C_entropy_source;
+ assigns Frama_C_entropy_source \from Frama_C_entropy_source;
+ */
+extern int Frama_C_interval(int min, int max);
+
+/*@ requires order: min ≤ max;
+ ensures result_bounded: \old(min) ≤ \result ≤ \old(max);
+ assigns \result, Frama_C_entropy_source;
+ assigns \result \from min, max, Frama_C_entropy_source;
+ assigns Frama_C_entropy_source \from Frama_C_entropy_source;
+ */
+extern int Frama_C_interval_split(int min, int max);
+
+/*@ requires order: min ≤ max;
+ ensures result_bounded: \old(min) ≤ \result ≤ \old(max);
+ assigns \result, Frama_C_entropy_source;
+ assigns \result \from min, max, Frama_C_entropy_source;
+ assigns Frama_C_entropy_source \from Frama_C_entropy_source;
+ */
+extern unsigned char Frama_C_unsigned_char_interval(unsigned char min,
+ unsigned char max);
+
+/*@ requires order: min ≤ max;
+ ensures result_bounded: \old(min) ≤ \result ≤ \old(max);
+ assigns \result, Frama_C_entropy_source;
+ assigns \result \from min, max, Frama_C_entropy_source;
+ assigns Frama_C_entropy_source \from Frama_C_entropy_source;
+ */
+extern char Frama_C_char_interval(char min, char max);
+
+/*@ requires order: min ≤ max;
+ ensures result_bounded: \old(min) ≤ \result ≤ \old(max);
+ assigns \result, Frama_C_entropy_source;
+ assigns \result \from min, max, Frama_C_entropy_source;
+ assigns Frama_C_entropy_source \from Frama_C_entropy_source;
+ */
+extern unsigned short Frama_C_unsigned_short_interval(unsigned short min,
+ unsigned short max);
+
+/*@ requires order: min ≤ max;
+ ensures result_bounded: \old(min) ≤ \result ≤ \old(max);
+ assigns \result, Frama_C_entropy_source;
+ assigns \result \from min, max, Frama_C_entropy_source;
+ assigns Frama_C_entropy_source \from Frama_C_entropy_source;
+ */
+extern short Frama_C_short_interval(short min, short max);
+
+/*@ requires order: min ≤ max;
+ ensures result_bounded: \old(min) ≤ \result ≤ \old(max);
+ assigns \result, Frama_C_entropy_source;
+ assigns \result \from min, max, Frama_C_entropy_source;
+ assigns Frama_C_entropy_source \from Frama_C_entropy_source;
+ */
+extern unsigned int Frama_C_unsigned_int_interval(unsigned int min,
+ unsigned int max);
+
+/*@ requires order: min ≤ max;
+ ensures result_bounded: \old(min) ≤ \result ≤ \old(max);
+ assigns \result, Frama_C_entropy_source;
+ assigns \result \from min, max, Frama_C_entropy_source;
+ assigns Frama_C_entropy_source \from Frama_C_entropy_source;
+ */
+extern int Frama_C_int_interval(int min, int max);
+
+/*@ requires order: min ≤ max;
+ ensures result_bounded: \old(min) ≤ \result ≤ \old(max);
+ assigns \result, Frama_C_entropy_source;
+ assigns \result \from min, max, Frama_C_entropy_source;
+ assigns Frama_C_entropy_source \from Frama_C_entropy_source;
+ */
+extern unsigned long Frama_C_unsigned_long_interval(unsigned long min,
+ unsigned long max);
+
+/*@ requires order: min ≤ max;
+ ensures result_bounded: \old(min) ≤ \result ≤ \old(max);
+ assigns \result, Frama_C_entropy_source;
+ assigns \result \from min, max, Frama_C_entropy_source;
+ assigns Frama_C_entropy_source \from Frama_C_entropy_source;
+ */
+extern long Frama_C_long_interval(long min, long max);
+
+/*@ requires order: min ≤ max;
+ ensures result_bounded: \old(min) ≤ \result ≤ \old(max);
+ assigns \result, Frama_C_entropy_source;
+ assigns \result \from min, max, Frama_C_entropy_source;
+ assigns Frama_C_entropy_source \from Frama_C_entropy_source;
+ */
+extern unsigned long long Frama_C_unsigned_long_long_interval(unsigned long long min,
+ unsigned long long max);
+
+/*@ requires order: min ≤ max;
+ ensures result_bounded: \old(min) ≤ \result ≤ \old(max);
+ assigns \result, Frama_C_entropy_source;
+ assigns \result \from min, max, Frama_C_entropy_source;
+ assigns Frama_C_entropy_source \from Frama_C_entropy_source;
+ */
+extern long long Frama_C_long_long_interval(long long min, long long max);
+
+/*@ requires order: min ≤ max;
+ ensures result_bounded: \old(min) ≤ \result ≤ \old(max);
+ assigns \result, Frama_C_entropy_source;
+ assigns \result \from min, max, Frama_C_entropy_source;
+ assigns Frama_C_entropy_source \from Frama_C_entropy_source;
+ */
+extern size_t Frama_C_size_t_interval(size_t min, size_t max);
+
+/*@ requires finite: \is_finite(min) ∧ \is_finite(max);
+ requires order: min ≤ max;
+ ensures
+ result_bounded:
+ \is_finite(\result) ∧ \old(min) ≤ \result ≤ \old(max);
+ assigns \result, Frama_C_entropy_source;
+ assigns \result \from min, max, Frama_C_entropy_source;
+ assigns Frama_C_entropy_source \from Frama_C_entropy_source;
+ */
+extern float Frama_C_float_interval(float min, float max);
+
+/*@ requires finite: \is_finite(min) ∧ \is_finite(max);
+ requires order: min ≤ max;
+ ensures
+ result_bounded:
+ \is_finite(\result) ∧ \old(min) ≤ \result ≤ \old(max);
+ assigns \result, Frama_C_entropy_source;
+ assigns \result \from min, max, Frama_C_entropy_source;
+ assigns Frama_C_entropy_source \from Frama_C_entropy_source;
+ */
+extern double Frama_C_double_interval(double min, double max);
+
+/*@ requires finite: \is_finite(min) ∧ \is_finite(max);
+ requires order: min ≤ max;
+ ensures
+ result_bounded:
+ \is_finite(\result) ∧ \old(min) ≤ \result ≤ \old(max);
+ assigns \result, Frama_C_entropy_source;
+ assigns \result \from min, max, Frama_C_entropy_source;
+ assigns Frama_C_entropy_source \from Frama_C_entropy_source;
+ */
+extern double Frama_C_real_interval_as_double(double min, double max);
+
+/*@ terminates \false;
+ ensures never_terminates: \false;
+ assigns \nothing; */
+extern __attribute__((__noreturn__)) void Frama_C_abort(void);
+
+/*@ assigns \result;
+ assigns \result \from p; */
+extern size_t Frama_C_offset(void const *p);
+
+/*@ assigns \result;
+ assigns \result \from i; */
+extern long long Frama_C_abstract_cardinal(long long i);
+
+/*@ assigns \result;
+ assigns \result \from i; */
+extern long long Frama_C_abstract_max(long long i);
+
+/*@ assigns \result;
+ assigns \result \from i; */
+extern long long Frama_C_abstract_min(long long i);
+
int volatile indefinitely;
int buffer[5];
int n = 0;
@@ -445,11 +631,10 @@ int n = 0;
*/
-extern int ( /* missing proto */ Frama_C_interval)(int x_0, int x_1);
-
/*@ ensures 0 ≤ \result < 0x100;
- assigns \result;
- assigns \result \from \nothing;
+ assigns \result, Frama_C_entropy_source;
+ assigns \result \from Frama_C_entropy_source;
+ assigns Frama_C_entropy_source \from Frama_C_entropy_source;
*/
int input_status(void)
{
@@ -555,8 +740,9 @@ int input_status(void)
*/
/*@ ensures 0 ≤ \result < 0x100;
- assigns \result;
- assigns \result \from \nothing;
+ assigns \result, Frama_C_entropy_source;
+ assigns \result \from Frama_C_entropy_source;
+ assigns Frama_C_entropy_source \from Frama_C_entropy_source;
*/
int input_data(void)
{
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/serial.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/serial.res.oracle
index 23c84d0e899..ea3fc004743 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/serial.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/serial.res.oracle
@@ -1,9 +1,5 @@
[kernel] Parsing tests/ya/serial.c (with preprocessing)
[kernel] Parsing TMPDIR/aorai_serial_0.i (no preprocessing)
-[kernel:typing:implicit-function-declaration] TMPDIR/aorai_serial_0.i:1359: Warning:
- Calling undeclared function Frama_C_interval. Old style K&R code?
-[kernel:annot:missing-spec] TMPDIR/aorai_serial_0.i:851: Warning:
- Neither code nor specification for function Frama_C_interval, generating default assigns from the prototype
-[kernel:annot:missing-spec] TMPDIR/aorai_serial_0.i:851: Warning:
+[kernel:annot:missing-spec] TMPDIR/aorai_serial_0.i:1036: Warning:
Neither code nor specification for function Frama_C_show_aorai_state, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ya/serial.ya b/src/plugins/aorai/tests/ya/serial.ya
index fed4f5cf370..6e893819100 100644
--- a/src/plugins/aorai/tests/ya/serial.ya
+++ b/src/plugins/aorai/tests/ya/serial.ya
@@ -7,7 +7,7 @@ $x2 : int;
$y1 : int;
$y2 : int;
-Error : { true } -> Error;
+Error : { 0 == 1 } -> Error;
Wait1 :
{ CALL(input_status) } -> StatusReq1
diff --git a/src/plugins/aorai/tests/ya/serial_wp.ya b/src/plugins/aorai/tests/ya/serial_wp.ya
index a796279cdbd..e915c3cbbd9 100644
--- a/src/plugins/aorai/tests/ya/serial_wp.ya
+++ b/src/plugins/aorai/tests/ya/serial_wp.ya
@@ -7,7 +7,7 @@ $x2 : int;
$y1 : int;
$y2 : int;
-Error : { true } -> Error;
+Error : { 0 == 1 } -> Error;
Wait1 :
{ CALL(input_status) } -> StatusReq1
--
GitLab