Skip to content
Snippets Groups Projects
Commit 5eff574f authored by Virgile Prevosto's avatar Virgile Prevosto
Browse files

[aorai] moving back Error translation to initial guard in serial.ya

parent 7d7027ce
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/plugins/aorai/tests/ya/oracle/serial.res.oracle
+ 224
− 38
View file @ 5eff574f
[kernel] Parsing tests/ya/serial.c (with preprocessing) [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 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] Analyzing a complete application starting at main
[eva] Computing initial state [eva] Computing initial state
...@@ -18,36 +18,36 @@ ...@@ -18,36 +18,36 @@
aorai_StatesHistory_1 ∈ {19} aorai_StatesHistory_1 ∈ {19}
aorai_StatesHistory_2 ∈ {19} aorai_StatesHistory_2 ∈ {19}
[eva] using specification for function Frama_C_interval [eva] using specification for function Frama_C_interval
[eva] tests/ya/serial.c:45: starting to merge loop iterations [eva] tests/ya/serial.c:58: starting to merge loop iterations
[eva] tests/ya/serial.c:50: Trace partitioning superposing up to 100 states [eva] tests/ya/serial.c:63: Trace partitioning superposing up to 100 states
[eva] tests/ya/serial.c:50: Trace partitioning superposing up to 300 states [eva] tests/ya/serial.c:63: Trace partitioning superposing up to 300 states
[aorai] tests/ya/serial.c:79: Wait1 <- Wait1 <- Complete [aorai] tests/ya/serial.c:92: 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:92: 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:92: 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:92: 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:92: 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:92: 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:92: 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:92: 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:92: 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:92: 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:92: Complete <- Complete <- Complete
[aorai] tests/ya/serial.c:79: n in {5},x in [0..16383],y in [0..8191] [aorai] tests/ya/serial.c:92: 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] tests/ya/serial.c:63: Trace partitioning superposing up to 500 states
[eva:alarm] tests/ya/serial.c:52: Warning: [eva:alarm] tests/ya/serial.c:65: Warning:
accessing uninitialized left-value. assert \initialized(&status); 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:63: 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:63: 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:63: Trace partitioning superposing up to 1200 states
[eva] tests/ya/serial.c:50: Trace partitioning superposing up to 1500 states [eva] tests/ya/serial.c:63: Trace partitioning superposing up to 1500 states
[aorai] tests/ya/serial.c:79: Error <- Error <- Error [aorai] tests/ya/serial.c:92: 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:92: 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:92: Error <- Error <- Error
[aorai] tests/ya/serial.c:79: n in {5},x in [0..16383],y in [0..8191] [aorai] tests/ya/serial.c:92: 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:63: 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:63: 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:63: 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 2100 states
[eva] done for function main [eva] done for function main
[eva] ====== VALUES COMPUTED ====== [eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function input_data_post_func: [eva:final-states] Values at end of function input_data_post_func:
...@@ -304,9 +304,8 @@ ...@@ -304,9 +304,8 @@
100% of the logical properties reached have been proven. 100% of the logical properties reached have been proven.
---------------------------------------------------------------------------- ----------------------------------------------------------------------------
[kernel] Parsing TMPDIR/aorai_serial_0.i (no preprocessing) [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 */ /* Generated by Frama-C */
typedef unsigned long size_t;
enum aorai_States { enum aorai_States {
aorai_reject_state = -2, aorai_reject_state = -2,
Complete = 0, Complete = 0,
...@@ -345,6 +344,193 @@ enum aorai_OpStatusList { ...@@ -345,6 +344,193 @@ enum aorai_OpStatusList {
}; };
/* compiler builtin: /* compiler builtin:
void Frama_C_show_aorai_state(...); */ 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 volatile indefinitely;
int buffer[5]; int buffer[5];
int n = 0; int n = 0;
...@@ -445,11 +631,10 @@ 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; /*@ ensures 0 ≤ \result < 0x100;
assigns \result; assigns \result, Frama_C_entropy_source;
assigns \result \from \nothing; assigns \result \from Frama_C_entropy_source;
assigns Frama_C_entropy_source \from Frama_C_entropy_source;
*/ */
int input_status(void) int input_status(void)
{ {
...@@ -555,8 +740,9 @@ int input_status(void) ...@@ -555,8 +740,9 @@ int input_status(void)
*/ */
/*@ ensures 0 ≤ \result < 0x100; /*@ ensures 0 ≤ \result < 0x100;
assigns \result; assigns \result, Frama_C_entropy_source;
assigns \result \from \nothing; assigns \result \from Frama_C_entropy_source;
assigns Frama_C_entropy_source \from Frama_C_entropy_source;
*/ */
int input_data(void) int input_data(void)
{ {
......
src/plugins/aorai/tests/ya/oracle_prove/serial.res.oracle
+ 1
− 5
View file @ 5eff574f
[kernel] Parsing tests/ya/serial.c (with preprocessing) [kernel] Parsing tests/ya/serial.c (with preprocessing)
[kernel] Parsing TMPDIR/aorai_serial_0.i (no preprocessing) [kernel] Parsing TMPDIR/aorai_serial_0.i (no preprocessing)
[kernel:typing:implicit-function-declaration] TMPDIR/aorai_serial_0.i:1359: Warning: [kernel:annot:missing-spec] TMPDIR/aorai_serial_0.i:1036: 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:
Neither code nor specification for function Frama_C_show_aorai_state, generating default assigns from the prototype Neither code nor specification for function Frama_C_show_aorai_state, generating default assigns from the prototype
[wp] Warning: Missing RTE guards [wp] Warning: Missing RTE guards
src/plugins/aorai/tests/ya/serial.ya
+ 1
− 1
View file @ 5eff574f
...@@ -7,7 +7,7 @@ $x2 : int; ...@@ -7,7 +7,7 @@ $x2 : int;
$y1 : int; $y1 : int;
$y2 : int; $y2 : int;
Error : { true } -> Error; Error : { 0 == 1 } -> Error;
Wait1 : Wait1 :
{ CALL(input_status) } -> StatusReq1 { CALL(input_status) } -> StatusReq1
......
src/plugins/aorai/tests/ya/serial_wp.ya
+ 1
− 1
View file @ 5eff574f
...@@ -7,7 +7,7 @@ $x2 : int; ...@@ -7,7 +7,7 @@ $x2 : int;
$y1 : int; $y1 : int;
$y2 : int; $y2 : int;
Error : { true } -> Error; Error : { 0 == 1 } -> Error;
Wait1 : Wait1 :
{ CALL(input_status) } -> StatusReq1 { CALL(input_status) } -> StatusReq1
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment