diff --git a/src/plugins/aorai/aorai_utils.ml b/src/plugins/aorai/aorai_utils.ml
index d1c5ef527a98fd75da0478c56cb11c4e7d3f31b8..d2691257484207183f5c671ce3d886bb67db2531 100644
--- a/src/plugins/aorai/aorai_utils.ml
+++ b/src/plugins/aorai/aorai_utils.ml
@@ -1073,18 +1073,6 @@ let make_enum_states () =
let state_list =
List.map (fun x -> (x.Promelaast.name, x.Promelaast.nums)) state_list
in
- let state_list =
- if not (Aorai_option.Deterministic.get ()) then state_list
- else
- (*[VP] Strictly speaking this is not needed, but Jessie tends
- to consider that a value of enum type can only be one of the
- tags, so that we must add this dummy state that is always a
- possible value, even when a contract concludes that curState
- is none of the others. Note that ISO C does not impose this
- limitation to values of enum types.
- *)
- (get_fresh "aorai_reject_state", -2)::state_list
- in
let enum = mk_global_c_enum_type_tagged states state_list in
let mapping =
List.map
@@ -2042,7 +2030,9 @@ let mk_deterministic_body generated_kf loc f st status res =
List.fold_right
(mk_deterministic_stmt generated_kf loc auto f st status res)
states
- ([], Cil_datatype.Varinfo.Set.empty, [],[])
+ ([], Cil_datatype.Varinfo.Set.empty, [],
+ (* if all else fails, go to reject state. *)
+ [is_state_det_stmt (Data_for_aorai.get_reject_state()) loc])
in
aux_funcs, aux_vars, aux_stmts @ trans_stmts
diff --git a/src/plugins/aorai/data_for_aorai.ml b/src/plugins/aorai/data_for_aorai.ml
index b18b1886af1af3c35160154835431e97e254ebfd..b1423f97bef4baa66534e326e85340364dd9ef14 100644
--- a/src/plugins/aorai/data_for_aorai.ml
+++ b/src/plugins/aorai/data_for_aorai.ml
@@ -984,7 +984,7 @@ module Reject_state =
(struct
let name = "Data_for_aorai.Reject_state"
let dependencies =
- [ Ast.self; Aorai_option.Ltl_File.self; Aorai_option.Buchi.self;
+ [ Aorai_option.Ltl_File.self; Aorai_option.Buchi.self;
Aorai_option.Ya.self]
end)
@@ -992,6 +992,14 @@ let get_reject_state () =
let create () = new_state "aorai_reject" in
Reject_state.memo create
+let is_reject_state state =
+ match Reject_state.get_option () with
+ None -> false
+ | Some state' -> Aorai_state.equal state state'
+
+let has_reject_state () =
+ match Reject_state.get_option () with None -> false | Some _ -> true
+
let add_if_needed states st =
if List.for_all (fun x -> not (Aorai_state.equal x st)) states
then st::states
@@ -1540,10 +1548,16 @@ let type_cond_auto auto =
| _ -> (i+1,{ t with cross = cond; numt = i } :: l))
(0,[]) trans
in
+ let states =
+ if Aorai_option.Deterministic.get () then
+ add_if_needed states (get_reject_state())
+ else states
+ in
let _, states =
List.fold_left
(fun (i,l as acc) s ->
if
+ is_reject_state s ||
List.exists
(fun t -> t.start.nums = s.nums || t.stop.nums = s.nums)
trans
@@ -1663,11 +1677,6 @@ let getObservablesFunctions () =
let getIgnoredFunctions () =
List.filter isDeclaredObservable !ignored_functions
-let is_reject_state state =
- match Reject_state.get_option () with
- None -> false
- | Some state' -> Aorai_state.equal state state'
-
(* ************************************************************************* *)
(* Table giving the varinfo structure associated to a given variable name *)
(* In practice it contains all variables (from promela and globals from C file) and only variables *)
@@ -2170,6 +2179,12 @@ let removeUnusedTransitionsAndStates () =
let reached_states = Loop_invariant_state.fold reached reached_states in
if Aorai_state.Set.is_empty reached_states then
raise Empty_automaton;
+ let reached_states =
+ if Aorai_option.Deterministic.get() then
+ (* keep the rejecting state anyways. *)
+ Aorai_state.Set.add (get_reject_state()) reached_states
+ else reached_states
+ in
(* Step 2 : computation of translation tables *)
let state_list =
List.sort
diff --git a/src/plugins/aorai/data_for_aorai.mli b/src/plugins/aorai/data_for_aorai.mli
index 71ecd72e1752b529ccfbb37c90e5afb0a125840a..b90f1272235d81fde644a06240b92930ab5132c4 100644
--- a/src/plugins/aorai/data_for_aorai.mli
+++ b/src/plugins/aorai/data_for_aorai.mli
@@ -244,6 +244,12 @@ val getStateName : int -> string
sequences. *)
val is_reject_state: state -> bool
+(** [true] iff a rejecting state already exists. *)
+val has_reject_state: unit -> bool
+
+(** return the rejecting state of the graph, creating it if needed. *)
+val get_reject_state: unit -> state
+
(** returns the transition having the corresponding id.
@raise Not_found if this is not the case.
*)
diff --git a/src/plugins/aorai/tests/ya/oracle/assigns.1.res.oracle b/src/plugins/aorai/tests/ya/oracle/assigns.1.res.oracle
index 067dda49b4da26140d890bff0562197c4771c561..5b81ca1fbe6f2c2ac6b2c327455daeb0f91c696e 100644
--- a/src/plugins/aorai/tests/ya/oracle/assigns.1.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/assigns.1.res.oracle
@@ -2,12 +2,12 @@
[kernel] Parsing TMPDIR/aorai_assigns_1.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_States {
- aorai_reject_state = -2,
S1 = 0,
S2 = 1,
S_in_f = 2,
Sf = 3,
- in_main = 4
+ aorai_reject = 4,
+ in_main = 5
};
enum aorai_ListOper {
op_f = 1,
@@ -19,6 +19,8 @@ enum aorai_OpStatusList {
};
/*@ check lemma in_main_deterministic_trans{L}: \true;
*/
+/*@ check lemma aorai_reject_deterministic_trans{L}: \true;
+ */
/*@ check lemma Sf_deterministic_trans{L}: \true;
*/
/*@ check lemma S_in_f_deterministic_trans{L}: \true;
@@ -54,6 +56,9 @@ int X;
behavior buch_state_Sf_out:
ensures aorai_CurStates ≢ Sf;
+ behavior buch_state_aorai_reject_out:
+ ensures aorai_CurStates ≢ aorai_reject;
+
behavior buch_state_in_main_out:
ensures aorai_CurStates ≢ in_main;
@/
@@ -63,6 +68,7 @@ int X;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_f;
if (3 == aorai_CurStates) aorai_CurStates = S_in_f;
+ else aorai_CurStates = aorai_reject;
return;
}
@@ -86,6 +92,9 @@ int X;
behavior buch_state_Sf_out:
ensures aorai_CurStates ≢ Sf;
+ behavior buch_state_aorai_reject_out:
+ ensures aorai_CurStates ≢ aorai_reject;
+
behavior buch_state_in_main_in:
assumes aorai_CurStates ≡ S_in_f;
ensures aorai_CurStates ≡ in_main;
@@ -100,6 +109,7 @@ int X;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_f;
if (2 == aorai_CurStates) aorai_CurStates = in_main;
+ else aorai_CurStates = aorai_reject;
return;
}
@@ -141,6 +151,9 @@ void f(void)
assumes aorai_CurStates ≢ S1;
ensures aorai_CurStates ≢ Sf;
+ behavior buch_state_aorai_reject_out:
+ ensures aorai_CurStates ≢ aorai_reject;
+
behavior buch_state_in_main_out:
ensures aorai_CurStates ≢ in_main;
@/
@@ -150,6 +163,7 @@ void f(void)
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
if (0 == aorai_CurStates) aorai_CurStates = Sf;
+ else aorai_CurStates = aorai_reject;
return;
}
@@ -178,6 +192,9 @@ void f(void)
behavior buch_state_Sf_out:
ensures aorai_CurStates ≢ Sf;
+ behavior buch_state_aorai_reject_out:
+ ensures aorai_CurStates ≢ aorai_reject;
+
behavior buch_state_in_main_out:
ensures aorai_CurStates ≢ in_main;
@/
@@ -186,7 +203,8 @@ void f(void)
/@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
- if (4 == aorai_CurStates) aorai_CurStates = S2;
+ if (5 == aorai_CurStates) aorai_CurStates = S2;
+ else aorai_CurStates = aorai_reject;
return;
}
diff --git a/src/plugins/aorai/tests/ya/oracle/declared_function.res.oracle b/src/plugins/aorai/tests/ya/oracle/declared_function.res.oracle
index 038d8c1a87087eae5fdcc7596b0515b6f7265d70..0b0ae22a40090a44b7c3bceaba53c7d1d945881e 100644
--- a/src/plugins/aorai/tests/ya/oracle/declared_function.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/declared_function.res.oracle
@@ -2,8 +2,8 @@
[kernel] Parsing TMPDIR/aorai_declared_function_0.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_States {
- aorai_reject_state = -2,
- I = 0
+ I = 0,
+ aorai_reject = 1
};
enum aorai_ListOper {
op_f = 1,
@@ -13,6 +13,8 @@ enum aorai_OpStatusList {
aorai_Terminated = 1,
aorai_Called = 0
};
+/*@ check lemma aorai_reject_deterministic_trans{L}: \true;
+ */
int f(void);
/*@ ghost enum aorai_ListOper aorai_CurOperation; */
@@ -57,6 +59,9 @@ check lemma I_deterministic_trans{L}:
behavior buch_state_I_out:
assumes aorai_CurStates ≢ I;
ensures aorai_CurStates ≢ I;
+
+ behavior buch_state_aorai_reject_out:
+ ensures aorai_CurStates ≢ aorai_reject;
@/
void main_pre_func(void)
{
@@ -64,6 +69,7 @@ check lemma I_deterministic_trans{L}:
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
if (0 == aorai_CurStates) aorai_CurStates = I;
+ else aorai_CurStates = aorai_reject;
return;
}
@@ -82,6 +88,9 @@ check lemma I_deterministic_trans{L}:
behavior buch_state_I_out:
assumes aorai_CurStates ≢ I;
ensures aorai_CurStates ≢ I;
+
+ behavior buch_state_aorai_reject_out:
+ ensures aorai_CurStates ≢ aorai_reject;
@/
void main_post_func(void)
{
@@ -89,6 +98,7 @@ check lemma I_deterministic_trans{L}:
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
if (0 == aorai_CurStates) aorai_CurStates = I;
+ else aorai_CurStates = aorai_reject;
return;
}
diff --git a/src/plugins/aorai/tests/ya/oracle/deterministic.res.oracle b/src/plugins/aorai/tests/ya/oracle/deterministic.res.oracle
index 72d480289360a25c758af89999a1d516a13bc578..7982cfe7c164fba8bf8e9d1f82290612f4c4ac4c 100644
--- a/src/plugins/aorai/tests/ya/oracle/deterministic.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/deterministic.res.oracle
@@ -2,7 +2,6 @@
[kernel] Parsing TMPDIR/aorai_deterministic_0.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_States {
- aorai_reject_state = -2,
S0 = 0,
S1 = 1,
S2 = 2,
@@ -10,7 +9,8 @@ enum aorai_States {
S4 = 4,
S5 = 5,
Sf = 6,
- Si = 7
+ Si = 7,
+ aorai_reject = 8
};
enum aorai_ListOper {
op_f = 3,
@@ -22,6 +22,8 @@ enum aorai_OpStatusList {
aorai_Terminated = 1,
aorai_Called = 0
};
+/*@ check lemma aorai_reject_deterministic_trans{L}: \true;
+ */
/*@ check lemma Si_deterministic_trans{L}: \true;
*/
/*@ check lemma Sf_deterministic_trans{L}: \true;
@@ -101,6 +103,9 @@ check lemma S0_deterministic_trans{L}:
behavior buch_state_Si_out:
ensures aorai_CurStates ≢ Si;
+
+ behavior buch_state_aorai_reject_out:
+ ensures aorai_CurStates ≢ aorai_reject;
@/
void g_pre_func(int x)
{
@@ -110,6 +115,7 @@ check lemma S0_deterministic_trans{L}:
if (3 == aorai_CurStates && x == 4) aorai_CurStates = S4;
else
if (3 == aorai_CurStates && x == 5) aorai_CurStates = S5;
+ else aorai_CurStates = aorai_reject;
return;
}
@@ -154,6 +160,9 @@ check lemma S0_deterministic_trans{L}:
behavior buch_state_Si_out:
ensures aorai_CurStates ≢ Si;
+
+ behavior buch_state_aorai_reject_out:
+ ensures aorai_CurStates ≢ aorai_reject;
@/
void g_post_func(void)
{
@@ -163,6 +172,7 @@ check lemma S0_deterministic_trans{L}:
if (5 == aorai_CurStates) aorai_CurStates = S1;
else
if (4 == aorai_CurStates) aorai_CurStates = S3;
+ else aorai_CurStates = aorai_reject;
return;
}
@@ -222,6 +232,9 @@ void g(int x)
behavior buch_state_Si_out:
ensures aorai_CurStates ≢ Si;
+
+ behavior buch_state_aorai_reject_out:
+ ensures aorai_CurStates ≢ aorai_reject;
@/
void f_pre_func(int x)
{
@@ -229,6 +242,7 @@ void g(int x)
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_f;
if (1 == aorai_CurStates && x == 4) aorai_CurStates = S3;
+ else aorai_CurStates = aorai_reject;
return;
}
@@ -269,6 +283,9 @@ void g(int x)
behavior buch_state_Si_out:
ensures aorai_CurStates ≢ Si;
+
+ behavior buch_state_aorai_reject_out:
+ ensures aorai_CurStates ≢ aorai_reject;
@/
void f_post_func(int res)
{
@@ -276,6 +293,7 @@ void g(int x)
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_f;
if (1 == aorai_CurStates && (res == 0 && X == 5)) aorai_CurStates = S2;
+ else aorai_CurStates = aorai_reject;
return;
}
@@ -341,6 +359,9 @@ int f(int x)
behavior buch_state_Si_out:
ensures aorai_CurStates ≢ Si;
+
+ behavior buch_state_aorai_reject_out:
+ ensures aorai_CurStates ≢ aorai_reject;
@/
void real_main_pre_func(int c)
{
@@ -350,6 +371,7 @@ int f(int x)
if (0 == aorai_CurStates && c != 0) aorai_CurStates = S1;
else
if (0 == aorai_CurStates && c == 0) aorai_CurStates = S2;
+ else aorai_CurStates = aorai_reject;
return;
}
@@ -389,6 +411,9 @@ int f(int x)
behavior buch_state_Si_out:
ensures aorai_CurStates ≢ Si;
+
+ behavior buch_state_aorai_reject_out:
+ ensures aorai_CurStates ≢ aorai_reject;
@/
void real_main_post_func(int res)
{
@@ -396,6 +421,7 @@ int f(int x)
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_real_main;
if (2 == aorai_CurStates) aorai_CurStates = Sf;
+ else aorai_CurStates = aorai_reject;
return;
}
@@ -451,6 +477,9 @@ int real_main(int c)
behavior buch_state_Si_out:
ensures aorai_CurStates ≢ Si;
+
+ behavior buch_state_aorai_reject_out:
+ ensures aorai_CurStates ≢ aorai_reject;
@/
void main_pre_func(int c)
{
@@ -458,6 +487,7 @@ int real_main(int c)
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
if (7 == aorai_CurStates) aorai_CurStates = S0;
+ else aorai_CurStates = aorai_reject;
return;
}
@@ -497,6 +527,9 @@ int real_main(int c)
behavior buch_state_Si_out:
ensures aorai_CurStates ≢ Si;
+
+ behavior buch_state_aorai_reject_out:
+ ensures aorai_CurStates ≢ aorai_reject;
@/
void main_post_func(int res)
{
@@ -504,6 +537,7 @@ int real_main(int c)
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
if (6 == aorai_CurStates) aorai_CurStates = Sf;
+ else aorai_CurStates = aorai_reject;
return;
}
diff --git a/src/plugins/aorai/tests/ya/oracle/formals.res.oracle b/src/plugins/aorai/tests/ya/oracle/formals.res.oracle
index e93f5561f0807a14d00498c42c24d8ba4ff50589..2d0f4d7bd8a2b0705c729447d09852dccb1f85e3 100644
--- a/src/plugins/aorai/tests/ya/oracle/formals.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/formals.res.oracle
@@ -2,7 +2,6 @@
[kernel] Parsing TMPDIR/aorai_formals_0.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_States {
- aorai_reject_state = -2,
OK = 0,
aorai_intermediate_state = 1,
aorai_intermediate_state_0 = 2,
@@ -141,6 +140,7 @@ check lemma aorai_intermediate_state_deterministic_trans{L}:
aorai_CurStates = aorai_intermediate_state_2;
aorai_x_0 = x;
}
+ else aorai_CurStates = aorai_reject;
return;
}
@@ -221,6 +221,7 @@ check lemma aorai_intermediate_state_deterministic_trans{L}:
if (4 == aorai_CurStates && aorai_x_0 != 3) aorai_CurStates = aorai_reject;
else
if (1 == aorai_CurStates && aorai_x != 1) aorai_CurStates = aorai_reject;
+ else aorai_CurStates = aorai_reject;
return;
}
@@ -355,6 +356,7 @@ int f(int x)
}
else
if (5 == aorai_CurStates) aorai_CurStates = aorai_reject;
+ else aorai_CurStates = aorai_reject;
return;
}
@@ -427,6 +429,7 @@ int f(int x)
if (5 == aorai_CurStates) aorai_CurStates = aorai_reject;
else
if (3 == aorai_CurStates && aorai_y != 2) aorai_CurStates = aorai_reject;
+ else aorai_CurStates = aorai_reject;
return;
}
@@ -509,6 +512,7 @@ int g(int y)
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
if (6 == aorai_CurStates) aorai_CurStates = main_0;
+ else aorai_CurStates = aorai_reject;
return;
}
@@ -562,6 +566,7 @@ int g(int y)
if (0 == aorai_CurStates) aorai_CurStates = OK;
else
if (5 == aorai_CurStates) aorai_CurStates = aorai_reject;
+ else aorai_CurStates = aorai_reject;
return;
}
diff --git a/src/plugins/aorai/tests/ya/oracle/incorrect.res.oracle b/src/plugins/aorai/tests/ya/oracle/incorrect.res.oracle
index 22596de4c18a3aa77dbb683b11aa7707bfd7e550..7c674204cb3013c0438b059705c8952bbd3c3998 100644
--- a/src/plugins/aorai/tests/ya/oracle/incorrect.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/incorrect.res.oracle
@@ -3,8 +3,8 @@
[kernel] Parsing TMPDIR/aorai_incorrect_0.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_States {
- aorai_reject_state = -2,
- s0 = 0
+ aorai_reject = 0,
+ s0 = 1
};
enum aorai_ListOper {
op_f = 1,
@@ -16,6 +16,8 @@ enum aorai_OpStatusList {
};
/*@ check lemma s0_deterministic_trans{L}: \true;
*/
+/*@ check lemma aorai_reject_deterministic_trans{L}: \true;
+ */
int f(void);
/*@ ghost enum aorai_ListOper aorai_CurOperation; */
@@ -27,6 +29,9 @@ int f(void);
ensures aorai_CurOperation ≡ op_main;
assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ behavior buch_state_aorai_reject_out:
+ ensures aorai_CurStates ≢ aorai_reject;
+
behavior buch_state_s0_out:
ensures aorai_CurStates ≢ s0;
@/
@@ -35,6 +40,7 @@ int f(void);
/@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
+ aorai_CurStates = aorai_reject;
return;
}
@@ -46,6 +52,9 @@ int f(void);
ensures aorai_CurOperation ≡ op_main;
assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+ behavior buch_state_aorai_reject_out:
+ ensures aorai_CurStates ≢ aorai_reject;
+
behavior buch_state_s0_out:
ensures aorai_CurStates ≢ s0;
@/
@@ -54,6 +63,7 @@ int f(void);
/@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
+ aorai_CurStates = aorai_reject;
return;
}
diff --git a/src/plugins/aorai/tests/ya/oracle/metavariables-right.res.oracle b/src/plugins/aorai/tests/ya/oracle/metavariables-right.res.oracle
index ee94f69b3848bbc6b9b26950a0b9736b328bbe99..1ad02912fd111f3df968455278a5dfbb2ae8e8f7 100644
--- a/src/plugins/aorai/tests/ya/oracle/metavariables-right.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/metavariables-right.res.oracle
@@ -2,16 +2,16 @@
[kernel] Parsing TMPDIR/aorai_metavariables-right_0.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_States {
- aorai_reject_state = -2,
a = 0,
- b = 1,
- c = 2,
- d = 3,
- e = 4,
- f_0 = 5,
- g_0 = 6,
- h_0 = 7,
- i_0 = 8
+ aorai_reject = 1,
+ b = 2,
+ c = 3,
+ d = 4,
+ e = 5,
+ f_0 = 6,
+ g_0 = 7,
+ h_0 = 8,
+ i_0 = 9
};
enum aorai_ListOper {
op_f = 4,
@@ -36,6 +36,8 @@ enum aorai_OpStatusList {
*/
/*@ check lemma c_deterministic_trans{L}: \true;
*/
+/*@ check lemma aorai_reject_deterministic_trans{L}: \true;
+ */
/*@ check lemma a_deterministic_trans{L}: \true;
*/
/*@ ghost enum aorai_ListOper aorai_CurOperation; */
@@ -67,6 +69,9 @@ check lemma e_deterministic_trans{L}:
behavior buch_state_a_out:
ensures aorai_CurStates ≢ a;
+ behavior buch_state_aorai_reject_out:
+ ensures aorai_CurStates ≢ aorai_reject;
+
behavior buch_state_b_out:
ensures aorai_CurStates ≢ b;
@@ -111,11 +116,12 @@ check lemma e_deterministic_trans{L}:
/@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_f;
- if (1 == aorai_CurStates) {
+ if (2 == aorai_CurStates) {
aorai_CurStates = c;
aorai_x = x;
aorai_y = aorai_x;
}
+ else aorai_CurStates = aorai_reject;
return;
}
@@ -130,6 +136,9 @@ check lemma e_deterministic_trans{L}:
behavior buch_state_a_out:
ensures aorai_CurStates ≢ a;
+ behavior buch_state_aorai_reject_out:
+ ensures aorai_CurStates ≢ aorai_reject;
+
behavior buch_state_b_out:
ensures aorai_CurStates ≢ b;
@@ -164,7 +173,8 @@ check lemma e_deterministic_trans{L}:
/@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_f;
- if (2 == aorai_CurStates) aorai_CurStates = e;
+ if (3 == aorai_CurStates) aorai_CurStates = e;
+ else aorai_CurStates = aorai_reject;
return;
}
@@ -197,6 +207,9 @@ void f(int x)
behavior buch_state_a_out:
ensures aorai_CurStates ≢ a;
+ behavior buch_state_aorai_reject_out:
+ ensures aorai_CurStates ≢ aorai_reject;
+
behavior buch_state_b_out:
ensures aorai_CurStates ≢ b;
@@ -231,7 +244,8 @@ void f(int x)
/@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_g;
- if (1 == aorai_CurStates) aorai_CurStates = d;
+ if (2 == aorai_CurStates) aorai_CurStates = d;
+ else aorai_CurStates = aorai_reject;
return;
}
@@ -246,6 +260,9 @@ void f(int x)
behavior buch_state_a_out:
ensures aorai_CurStates ≢ a;
+ behavior buch_state_aorai_reject_out:
+ ensures aorai_CurStates ≢ aorai_reject;
+
behavior buch_state_b_out:
ensures aorai_CurStates ≢ b;
@@ -280,7 +297,8 @@ void f(int x)
/@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_g;
- if (3 == aorai_CurStates) aorai_CurStates = g_0;
+ if (4 == aorai_CurStates) aorai_CurStates = g_0;
+ else aorai_CurStates = aorai_reject;
return;
}
@@ -308,6 +326,9 @@ void g(void)
behavior buch_state_a_out:
ensures aorai_CurStates ≢ a;
+ behavior buch_state_aorai_reject_out:
+ ensures aorai_CurStates ≢ aorai_reject;
+
behavior buch_state_b_out:
ensures aorai_CurStates ≢ b;
@@ -342,7 +363,8 @@ void g(void)
/@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_h;
- if (4 == aorai_CurStates && aorai_x > 0) aorai_CurStates = f_0;
+ if (5 == aorai_CurStates && aorai_x > 0) aorai_CurStates = f_0;
+ else aorai_CurStates = aorai_reject;
return;
}
@@ -357,6 +379,9 @@ void g(void)
behavior buch_state_a_out:
ensures aorai_CurStates ≢ a;
+ behavior buch_state_aorai_reject_out:
+ ensures aorai_CurStates ≢ aorai_reject;
+
behavior buch_state_b_out:
ensures aorai_CurStates ≢ b;
@@ -391,7 +416,8 @@ void g(void)
/@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_h;
- if (5 == aorai_CurStates) aorai_CurStates = g_0;
+ if (6 == aorai_CurStates) aorai_CurStates = g_0;
+ else aorai_CurStates = aorai_reject;
return;
}
@@ -419,6 +445,9 @@ void h(int x)
behavior buch_state_a_out:
ensures aorai_CurStates ≢ a;
+ behavior buch_state_aorai_reject_out:
+ ensures aorai_CurStates ≢ aorai_reject;
+
behavior buch_state_b_out:
ensures aorai_CurStates ≢ b;
@@ -453,7 +482,8 @@ void h(int x)
/@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_i;
- if (6 == aorai_CurStates) aorai_CurStates = h_0;
+ if (7 == aorai_CurStates) aorai_CurStates = h_0;
+ else aorai_CurStates = aorai_reject;
return;
}
@@ -469,6 +499,9 @@ void h(int x)
behavior buch_state_a_out:
ensures aorai_CurStates ≢ a;
+ behavior buch_state_aorai_reject_out:
+ ensures aorai_CurStates ≢ aorai_reject;
+
behavior buch_state_b_out:
ensures aorai_CurStates ≢ b;
@@ -513,11 +546,12 @@ void h(int x)
/@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_i;
- if (7 == aorai_CurStates) {
+ if (8 == aorai_CurStates) {
aorai_CurStates = e;
aorai_y = 0;
aorai_x = 1;
}
+ else aorai_CurStates = aorai_reject;
return;
}
@@ -550,6 +584,9 @@ void i(void)
behavior buch_state_a_out:
ensures aorai_CurStates ≢ a;
+ behavior buch_state_aorai_reject_out:
+ ensures aorai_CurStates ≢ aorai_reject;
+
behavior buch_state_b_in:
assumes aorai_CurStates ≡ a;
ensures aorai_CurStates ≡ b;
@@ -585,6 +622,7 @@ void i(void)
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
if (0 == aorai_CurStates) aorai_CurStates = b;
+ else aorai_CurStates = aorai_reject;
return;
}
@@ -599,6 +637,9 @@ void i(void)
behavior buch_state_a_out:
ensures aorai_CurStates ≢ a;
+ behavior buch_state_aorai_reject_out:
+ ensures aorai_CurStates ≢ aorai_reject;
+
behavior buch_state_b_out:
ensures aorai_CurStates ≢ b;
@@ -633,7 +674,8 @@ void i(void)
/@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
- if (4 == aorai_CurStates) aorai_CurStates = i_0;
+ if (5 == aorai_CurStates) aorai_CurStates = i_0;
+ else aorai_CurStates = aorai_reject;
return;
}
@@ -663,6 +705,7 @@ void main(int t)
/*@ ghost aorai_Loop_Init_15 = 1; */
aorai_loop_15:
/*@ loop invariant Aorai: aorai_CurStates ≢ a;
+ loop invariant Aorai: aorai_CurStates ≢ aorai_reject;
loop invariant Aorai: aorai_CurStates ≢ b;
loop invariant Aorai: aorai_CurStates ≢ c;
loop invariant Aorai: aorai_CurStates ≢ d;
diff --git a/src/plugins/aorai/tests/ya/oracle/monostate.res.oracle b/src/plugins/aorai/tests/ya/oracle/monostate.res.oracle
index 984890928fa440a12a69183ee4d138aae1306960..9ee345cafbfbc284e6862d953d00e7412e1773f6 100644
--- a/src/plugins/aorai/tests/ya/oracle/monostate.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/monostate.res.oracle
@@ -5,7 +5,6 @@
[kernel] Parsing TMPDIR/aorai_monostate_0.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_States {
- aorai_reject_state = -2,
Init = 0,
aorai_intermediate_state = 1,
aorai_reject = 2
@@ -69,6 +68,7 @@ check lemma Init_deterministic_trans{L}:
if (2 == aorai_CurStates) aorai_CurStates = aorai_reject;
else
if (1 == aorai_CurStates) aorai_CurStates = aorai_reject;
+ else aorai_CurStates = aorai_reject;
return;
}
@@ -100,6 +100,7 @@ check lemma Init_deterministic_trans{L}:
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_f;
if (2 == aorai_CurStates) aorai_CurStates = aorai_reject;
+ else aorai_CurStates = aorai_reject;
return;
}
@@ -143,6 +144,7 @@ void f(void)
/@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
+ aorai_CurStates = aorai_reject;
return;
}
@@ -168,6 +170,7 @@ void f(void)
/@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
+ aorai_CurStates = aorai_reject;
return;
}
diff --git a/src/plugins/aorai/tests/ya/oracle/saveload.res.1.log b/src/plugins/aorai/tests/ya/oracle/saveload.res.1.log
index 7c430b30808840987417a7cd958f782340bc6e7f..8c7beb3ffd181c92a0cebea295fe4cc7db971e47 100644
--- a/src/plugins/aorai/tests/ya/oracle/saveload.res.1.log
+++ b/src/plugins/aorai/tests/ya/oracle/saveload.res.1.log
@@ -6,7 +6,7 @@
[eva:initial-state] Values of globals at initialization
aorai_CurOperation ∈ {0}
aorai_CurOpStatus ∈ {0}
- aorai_CurStates ∈ {1}
+ aorai_CurStates ∈ {2}
[aorai] tests/ya/saveload.i:14: accept
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
@@ -38,7 +38,7 @@
[eva:summary] ====== ANALYSIS SUMMARY ======
----------------------------------------------------------------------------
6 functions analyzed (out of 6): 100% coverage.
- In these functions, 31 statements reached (out of 31): 100% coverage.
+ In these functions, 31 statements reached (out of 35): 88% coverage.
----------------------------------------------------------------------------
Some errors and warnings have been raised during the analysis:
by the Eva analyzer: 0 errors 0 warnings
diff --git a/src/plugins/aorai/tests/ya/oracle/serial.res.oracle b/src/plugins/aorai/tests/ya/oracle/serial.res.oracle
index 668ee72c09b59fa54db0b2b770f31c001972b301..2692e58379bd450ecc23cd5b49b267ac72b54d97 100644
--- a/src/plugins/aorai/tests/ya/oracle/serial.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/serial.res.oracle
@@ -21,17 +21,17 @@
[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: aorai_reject <- aorai_reject <- 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: aorai_reject <- 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: 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: aorai_reject <- aorai_reject <- 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: aorai_reject <- 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: Wait1 <- Wait1 <- 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:
@@ -39,15 +39,15 @@
[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
+[eva] tests/ya/serial.c:63: Trace partitioning superposing up to 1400 states
+[aorai] tests/ya/serial.c:92: aorai_reject <- aorai_reject <- aorai_reject
[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: aorai_reject <- aorai_reject <- aorai_reject
[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 1500 states
+[eva] tests/ya/serial.c:63: Trace partitioning superposing up to 1600 states
[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] tests/ya/serial.c:63: Trace partitioning superposing up to 1800 states
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function input_data_post_func:
@@ -84,15 +84,15 @@
aorai_y2 ∈ [0..2147483647]
aorai_CurOperation ∈ {2}
aorai_CurOpStatus ∈ {1}
- aorai_CurStates ∈ {0; 7; 19; 20; 21; 22; 23}
- aorai_StatesHistory_1 ∈ {1; 2; 3; 4; 5; 6; 7}
- aorai_StatesHistory_2 ∈ {7; 8; 9; 10; 11; 12; 13}
+ aorai_CurStates ∈ {0; 19; 20; 21; 22; 23; 24}
+ aorai_StatesHistory_1 ∈ {1; 2; 3; 4; 5; 6; 24}
+ aorai_StatesHistory_2 ∈ {8; 9; 10; 11; 12; 13; 24}
[eva:final-states] Values at end of function input_data_pre_func:
aorai_CurOperation ∈ {2}
aorai_CurOpStatus ∈ {0}
- aorai_CurStates ∈ {1; 2; 3; 4; 5; 6; 7}
- aorai_StatesHistory_1 ∈ {7; 8; 9; 10; 11; 12; 13}
- aorai_StatesHistory_2 ∈ {7; 14; 15; 16; 17; 18}
+ aorai_CurStates ∈ {1; 2; 3; 4; 5; 6; 24}
+ aorai_StatesHistory_1 ∈ {8; 9; 10; 11; 12; 13; 24}
+ aorai_StatesHistory_2 ∈ {14; 15; 16; 17; 18; 24}
[eva:final-states] Values at end of function input_data:
Frama_C_entropy_source ∈ [--..--]
aorai_x1 ∈
@@ -128,46 +128,46 @@
aorai_y2 ∈ [0..2147483647]
aorai_CurOperation ∈ {2}
aorai_CurOpStatus ∈ {1}
- aorai_CurStates ∈ {0; 7; 19; 20; 21; 22; 23}
- aorai_StatesHistory_1 ∈ {1; 2; 3; 4; 5; 6; 7}
- aorai_StatesHistory_2 ∈ {7; 8; 9; 10; 11; 12; 13}
+ aorai_CurStates ∈ {0; 19; 20; 21; 22; 23; 24}
+ aorai_StatesHistory_1 ∈ {1; 2; 3; 4; 5; 6; 24}
+ aorai_StatesHistory_2 ∈ {8; 9; 10; 11; 12; 13; 24}
[eva:final-states] Values at end of function input_status_post_func:
aorai_CurOperation ∈ {1}
aorai_CurOpStatus ∈ {1}
- aorai_CurStates ∈ {7; 8; 9; 10; 11; 12; 13; 19; 20; 21; 22; 23}
- aorai_StatesHistory_1 ∈ {7; 14; 15; 16; 17; 18}
- aorai_StatesHistory_2 ∈ {0; 7; 19; 20; 21; 22; 23}
+ aorai_CurStates ∈ {8; 9; 10; 11; 12; 13; 19; 20; 21; 22; 23; 24}
+ aorai_StatesHistory_1 ∈ {14; 15; 16; 17; 18; 24}
+ aorai_StatesHistory_2 ∈ {0; 19; 20; 21; 22; 23; 24}
[eva:final-states] Values at end of function input_status_pre_func:
aorai_CurOperation ∈ {1}
aorai_CurOpStatus ∈ {0}
- aorai_CurStates ∈ {7; 14; 15; 16; 17; 18}
- aorai_StatesHistory_1 ∈ {0; 7; 19; 20; 21; 22; 23}
- aorai_StatesHistory_2 ∈ {0; 1; 2; 3; 4; 5; 6; 7; 14; 15; 16; 17; 18; 19}
+ aorai_CurStates ∈ {14; 15; 16; 17; 18; 24}
+ aorai_StatesHistory_1 ∈ {0; 19; 20; 21; 22; 23; 24}
+ aorai_StatesHistory_2 ∈ {1; 2; 3; 4; 5; 6; 7; 14; 15; 16; 17; 18; 19; 24}
[eva:final-states] Values at end of function input_status:
Frama_C_entropy_source ∈ [--..--]
aorai_CurOperation ∈ {1}
aorai_CurOpStatus ∈ {1}
- aorai_CurStates ∈ {7; 8; 9; 10; 11; 12; 13; 19; 20; 21; 22; 23}
- aorai_StatesHistory_1 ∈ {7; 14; 15; 16; 17; 18}
- aorai_StatesHistory_2 ∈ {0; 7; 19; 20; 21; 22; 23}
+ aorai_CurStates ∈ {8; 9; 10; 11; 12; 13; 19; 20; 21; 22; 23; 24}
+ aorai_StatesHistory_1 ∈ {14; 15; 16; 17; 18; 24}
+ aorai_StatesHistory_2 ∈ {0; 19; 20; 21; 22; 23; 24}
[eva:final-states] Values at end of function output_post_func:
aorai_CurOperation ∈ {0}
aorai_CurOpStatus ∈ {1}
- aorai_CurStates ∈ {0; 7; 19}
- aorai_StatesHistory_1 ∈ {0; 7; 19}
- aorai_StatesHistory_2 ∈ {0; 7}
+ aorai_CurStates ∈ {19; 24}
+ aorai_StatesHistory_1 ∈ {7; 19; 24}
+ aorai_StatesHistory_2 ∈ {0; 24}
[eva:final-states] Values at end of function output_pre_func:
aorai_CurOperation ∈ {0}
aorai_CurOpStatus ∈ {0}
- aorai_CurStates ∈ {0; 7; 19}
- aorai_StatesHistory_1 ∈ {0; 7}
- aorai_StatesHistory_2 ∈ {5; 7}
+ aorai_CurStates ∈ {7; 19; 24}
+ aorai_StatesHistory_1 ∈ {0; 24}
+ aorai_StatesHistory_2 ∈ {5; 24}
[eva:final-states] Values at end of function output:
aorai_CurOperation ∈ {0}
aorai_CurOpStatus ∈ {1}
- aorai_CurStates ∈ {0; 7; 19}
- aorai_StatesHistory_1 ∈ {0; 7; 19}
- aorai_StatesHistory_2 ∈ {0; 7}
+ aorai_CurStates ∈ {19; 24}
+ aorai_StatesHistory_1 ∈ {7; 19; 24}
+ aorai_StatesHistory_2 ∈ {0; 24}
[eva:final-states] Values at end of function read:
Frama_C_entropy_source ∈ [--..--]
s ∈
@@ -223,9 +223,9 @@
aorai_y2 ∈ [0..2147483647]
aorai_CurOperation ∈ {1; 2}
aorai_CurOpStatus ∈ {1}
- aorai_CurStates ∈ {0; 7; 19; 20; 21; 22; 23}
- aorai_StatesHistory_1 ∈ {1; 2; 3; 4; 5; 6; 7; 14; 15; 16; 17; 18}
- aorai_StatesHistory_2 ∈ {0; 7; 8; 9; 10; 11; 12; 13; 19; 20; 21; 22; 23}
+ aorai_CurStates ∈ {0; 19; 20; 21; 22; 23; 24}
+ aorai_StatesHistory_1 ∈ {1; 2; 3; 4; 5; 6; 14; 15; 16; 17; 18; 24}
+ aorai_StatesHistory_2 ∈ {0; 8; 9; 10; 11; 12; 13; 19; 20; 21; 22; 23; 24}
[eva:final-states] Values at end of function main:
Frama_C_entropy_source ∈ [--..--]
buffer[0] ∈
@@ -283,13 +283,13 @@
aorai_y2 ∈ [0..2147483647]
aorai_CurOperation ∈ {0; 1; 2}
aorai_CurOpStatus ∈ {0; 1}
- aorai_CurStates ∈ {0; 7; 19; 20; 21; 22; 23}
- aorai_StatesHistory_1 ∈ {0; 1; 2; 3; 4; 5; 6; 7; 14; 15; 16; 17; 18; 19}
- aorai_StatesHistory_2 ∈ {0; 7; 8; 9; 10; 11; 12; 13; 19; 20; 21; 22; 23}
+ aorai_CurStates ∈ {0; 19; 20; 21; 22; 23; 24}
+ aorai_StatesHistory_1 ∈ {1; 2; 3; 4; 5; 6; 7; 14; 15; 16; 17; 18; 19; 24}
+ aorai_StatesHistory_2 ∈ {0; 8; 9; 10; 11; 12; 13; 19; 20; 21; 22; 23; 24}
[eva:summary] ====== ANALYSIS SUMMARY ======
----------------------------------------------------------------------------
11 functions analyzed (out of 11): 100% coverage.
- In these functions, 216 statements reached (out of 255): 84% coverage.
+ In these functions, 222 statements reached (out of 261): 85% coverage.
----------------------------------------------------------------------------
Some errors and warnings have been raised during the analysis:
by the Eva analyzer: 0 errors 0 warnings
@@ -307,7 +307,6 @@
/* Generated by Frama-C */
typedef unsigned long size_t;
enum aorai_States {
- aorai_reject_state = -2,
Complete = 0,
DataReq1 = 1,
DataReq2 = 2,
@@ -331,7 +330,8 @@ enum aorai_States {
Wait2 = 20,
Wait3 = 21,
Wait4 = 22,
- Wait5 = 23
+ Wait5 = 23,
+ aorai_reject = 24
};
enum aorai_ListOper {
op_input_data = 2,
@@ -574,6 +574,7 @@ int n = 0;
if (23 == aorai_CurStates) aorai_CurStates = StatusReq5;
else
if (13 == aorai_CurStates) aorai_CurStates = StatusReq5;
+ else aorai_CurStates = aorai_reject;
return;
}
@@ -626,6 +627,7 @@ int n = 0;
else
if (18 == aorai_CurStates && (res & 1) == 0)
aorai_CurStates = Wait5;
+ else aorai_CurStates = aorai_reject;
return;
}
@@ -674,6 +676,7 @@ int input_status(void)
if (20 == aorai_CurStates) aorai_CurStates = Error;
else
if (19 == aorai_CurStates) aorai_CurStates = Error;
+ else aorai_CurStates = aorai_reject;
return;
}
@@ -734,6 +737,7 @@ int input_status(void)
aorai_CurStates = Wait5;
aorai_y1 = res;
}
+ else aorai_CurStates = aorai_reject;
return;
}
@@ -794,6 +798,7 @@ int input_data(void)
y == aorai_y1 +
128 * aorai_y2))
aorai_CurStates = Wait1;
+ else aorai_CurStates = aorai_reject;
return;
}
@@ -808,6 +813,7 @@ int input_data(void)
aorai_StatesHistory_2 = aorai_StatesHistory_1;
aorai_StatesHistory_1 = aorai_CurStates;
if (19 == aorai_CurStates) aorai_CurStates = Wait1;
+ else aorai_CurStates = aorai_reject;
return;
}
diff --git a/src/plugins/aorai/tests/ya/oracle/singleassignment-right.res.oracle b/src/plugins/aorai/tests/ya/oracle/singleassignment-right.res.oracle
index 311412524b5009aba4debf1e643b10fbb91dc723..067d521b9343014601ca3fe534174c42e4c083eb 100644
--- a/src/plugins/aorai/tests/ya/oracle/singleassignment-right.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/singleassignment-right.res.oracle
@@ -2,10 +2,10 @@
[kernel] Parsing TMPDIR/aorai_singleassignment-right_0.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_States {
- aorai_reject_state = -2,
a = 0,
- b = 1,
- c = 2
+ aorai_reject = 1,
+ b = 2,
+ c = 3
};
enum aorai_ListOper {
op_main = 0
@@ -18,6 +18,8 @@ enum aorai_OpStatusList {
*/
/*@ check lemma b_deterministic_trans{L}: \true;
*/
+/*@ check lemma aorai_reject_deterministic_trans{L}: \true;
+ */
/*@ check lemma a_deterministic_trans{L}: \true;
*/
/*@ ghost enum aorai_ListOper aorai_CurOperation; */
@@ -35,6 +37,9 @@ enum aorai_OpStatusList {
behavior buch_state_a_out:
ensures aorai_CurStates ≢ a;
+ behavior buch_state_aorai_reject_out:
+ ensures aorai_CurStates ≢ aorai_reject;
+
behavior buch_state_b_in_0:
assumes aorai_CurStates ≡ a;
ensures aorai_CurStates ≡ b;
@@ -66,6 +71,7 @@ enum aorai_OpStatusList {
aorai_x = *x;
aorai_y = *y;
}
+ else aorai_CurStates = aorai_reject;
return;
}
@@ -81,6 +87,9 @@ enum aorai_OpStatusList {
behavior buch_state_a_out:
ensures aorai_CurStates ≢ a;
+ behavior buch_state_aorai_reject_out:
+ ensures aorai_CurStates ≢ aorai_reject;
+
behavior buch_state_b_out:
ensures aorai_CurStates ≢ b;
@@ -107,11 +116,12 @@ enum aorai_OpStatusList {
/@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
- if (1 == aorai_CurStates) {
+ if (2 == aorai_CurStates) {
aorai_CurStates = c;
aorai_x = aorai_y;
aorai_y = aorai_x;
}
+ else aorai_CurStates = aorai_reject;
return;
}
diff --git a/src/plugins/aorai/tests/ya/oracle/stack.res.oracle b/src/plugins/aorai/tests/ya/oracle/stack.res.oracle
index 7bb7948a156df11a03f6795a73ed979157a58b1e..1c87bd335767554b3c662d504f66f15913c08133 100644
--- a/src/plugins/aorai/tests/ya/oracle/stack.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/stack.res.oracle
@@ -2,13 +2,13 @@
[kernel] Parsing TMPDIR/aorai_stack_0.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_States {
- aorai_reject_state = -2,
accept = 0,
- empty_stack = 1,
- emptying_stack = 2,
- filled_stack = 3,
- filling_stack = 4,
- init = 5
+ aorai_reject = 1,
+ empty_stack = 2,
+ emptying_stack = 3,
+ filled_stack = 4,
+ filling_stack = 5,
+ init = 6
};
enum aorai_ListOper {
op_main = 2,
@@ -23,6 +23,8 @@ enum aorai_OpStatusList {
*/
/*@ check lemma filling_stack_deterministic_trans{L}: \true;
*/
+/*@ check lemma aorai_reject_deterministic_trans{L}: \true;
+ */
/*@ check lemma accept_deterministic_trans{L}: \true;
*/
int g = 0;
@@ -61,6 +63,9 @@ check lemma emptying_stack_deterministic_trans{L}:
behavior buch_state_accept_out:
ensures aorai_CurStates ≢ accept;
+ behavior buch_state_aorai_reject_out:
+ ensures aorai_CurStates ≢ aorai_reject;
+
behavior buch_state_empty_stack_out:
ensures aorai_CurStates ≢ empty_stack;
@@ -88,9 +93,10 @@ check lemma emptying_stack_deterministic_trans{L}:
/@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_push;
- if (3 == aorai_CurStates) aorai_CurStates = filling_stack;
+ if (4 == aorai_CurStates) aorai_CurStates = filling_stack;
else
- if (1 == aorai_CurStates) aorai_CurStates = filling_stack;
+ if (2 == aorai_CurStates) aorai_CurStates = filling_stack;
+ else aorai_CurStates = aorai_reject;
return;
}
@@ -105,6 +111,9 @@ check lemma emptying_stack_deterministic_trans{L}:
behavior buch_state_accept_out:
ensures aorai_CurStates ≢ accept;
+ behavior buch_state_aorai_reject_out:
+ ensures aorai_CurStates ≢ aorai_reject;
+
behavior buch_state_empty_stack_out:
ensures aorai_CurStates ≢ empty_stack;
@@ -136,10 +145,11 @@ check lemma emptying_stack_deterministic_trans{L}:
/@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_push;
- if (4 == aorai_CurStates) {
+ if (5 == aorai_CurStates) {
aorai_CurStates = filled_stack;
aorai_n ++;
}
+ else aorai_CurStates = aorai_reject;
return;
}
@@ -181,6 +191,9 @@ void push(void)
behavior buch_state_accept_out:
ensures aorai_CurStates ≢ accept;
+ behavior buch_state_aorai_reject_out:
+ ensures aorai_CurStates ≢ aorai_reject;
+
behavior buch_state_empty_stack_out:
ensures aorai_CurStates ≢ empty_stack;
@@ -206,7 +219,8 @@ void push(void)
/@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_pop;
- if (3 == aorai_CurStates && aorai_n > 0) aorai_CurStates = emptying_stack;
+ if (4 == aorai_CurStates && aorai_n > 0) aorai_CurStates = emptying_stack;
+ else aorai_CurStates = aorai_reject;
return;
}
@@ -223,6 +237,9 @@ void push(void)
behavior buch_state_accept_out:
ensures aorai_CurStates ≢ accept;
+ behavior buch_state_aorai_reject_out:
+ ensures aorai_CurStates ≢ aorai_reject;
+
behavior buch_state_empty_stack_in_0:
assumes aorai_CurStates ≡ emptying_stack ∧ aorai_n ≡ 1;
ensures aorai_CurStates ≡ empty_stack;
@@ -260,15 +277,16 @@ void push(void)
/@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_pop;
- if (2 == aorai_CurStates && aorai_n == 1) {
+ if (3 == aorai_CurStates && aorai_n == 1) {
aorai_CurStates = empty_stack;
aorai_n --;
}
else
- if (2 == aorai_CurStates && aorai_n > 1) {
+ if (3 == aorai_CurStates && aorai_n > 1) {
aorai_CurStates = filled_stack;
aorai_n --;
}
+ else aorai_CurStates = aorai_reject;
return;
}
@@ -310,6 +328,9 @@ void pop(void)
behavior buch_state_accept_out:
ensures aorai_CurStates ≢ accept;
+ behavior buch_state_aorai_reject_out:
+ ensures aorai_CurStates ≢ aorai_reject;
+
behavior buch_state_empty_stack_in_0:
assumes aorai_CurStates ≡ init;
ensures aorai_CurStates ≡ empty_stack;
@@ -340,10 +361,11 @@ void pop(void)
/@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
- if (5 == aorai_CurStates) {
+ if (6 == aorai_CurStates) {
aorai_CurStates = empty_stack;
aorai_n = 0;
}
+ else aorai_CurStates = aorai_reject;
return;
}
@@ -363,6 +385,9 @@ void pop(void)
assumes aorai_CurStates ≢ empty_stack;
ensures aorai_CurStates ≢ accept;
+ behavior buch_state_aorai_reject_out:
+ ensures aorai_CurStates ≢ aorai_reject;
+
behavior buch_state_empty_stack_out:
ensures aorai_CurStates ≢ empty_stack;
@@ -383,7 +408,8 @@ void pop(void)
/@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
- if (1 == aorai_CurStates) aorai_CurStates = accept;
+ if (2 == aorai_CurStates) aorai_CurStates = accept;
+ else aorai_CurStates = aorai_reject;
return;
}
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/declared_function.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/declared_function.res.oracle
index dda7d91ed57dc422451bd64176a91eecefad7558..500161bb9b87f344c719102b69b2fca48fd92521 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/declared_function.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/declared_function.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing tests/ya/declared_function.i (no preprocessing)
[kernel] Parsing TMPDIR/aorai_declared_function_0.i (no preprocessing)
-[kernel:annot:missing-spec] TMPDIR/aorai_declared_function_0.i:48: Warning:
+[kernel:annot:missing-spec] TMPDIR/aorai_declared_function_0.i:50: Warning:
Neither code nor specification for function f, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/incorrect.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/incorrect.res.oracle
index b8e7296acf003802517f2ff5211e7afc68b42a11..30ba0541d811ba71dc98cdebc6793c7e0d12e87e 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/incorrect.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/incorrect.res.oracle
@@ -2,5 +2,5 @@
[aorai] Warning: Call to main does not follow automaton's specification. This path is assumed to be dead
[kernel] Parsing TMPDIR/aorai_incorrect_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
-[kernel:annot:missing-spec] TMPDIR/aorai_incorrect_0.i:63: Warning:
+[kernel:annot:missing-spec] TMPDIR/aorai_incorrect_0.i:69: Warning:
Neither code nor specification for function f, generating default assigns from the prototype
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 ea3fc004743eb66c56c69b5095ca59d5248afc83..2dd3de37879294166ef9a7e0f933bf3cc88c7339 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/serial.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/serial.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing tests/ya/serial.c (with preprocessing)
[kernel] Parsing TMPDIR/aorai_serial_0.i (no preprocessing)
-[kernel:annot:missing-spec] TMPDIR/aorai_serial_0.i:1036: Warning:
+[kernel:annot:missing-spec] TMPDIR/aorai_serial_0.i:738: 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_wp.ya b/src/plugins/aorai/tests/ya/serial_wp.ya
index e915c3cbbd964b574641a0d47b174e0ab6a23159..1a28de31009827dd8d4018f2f53cc67816a6b661 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 : { 0 == 1 } -> Error;
+Error : { false } -> Error;
Wait1 :
{ CALL(input_status) } -> StatusReq1