diff --git a/src/plugins/aorai/data_for_aorai.ml b/src/plugins/aorai/data_for_aorai.ml
index bf0f05f91967628ee7717176885947da9bdd75e2..2615a5a92b6fb5dcff622af0adb7be9b2c6f18d8 100644
--- a/src/plugins/aorai/data_for_aorai.ml
+++ b/src/plugins/aorai/data_for_aorai.ml
@@ -31,6 +31,8 @@ open Logic_simplification
exception Empty_automaton
+let typing_dkey = Aorai_option.register_category "type-automaton"
+
module Aorai_state =
Datatype.Make_with_collections(
struct
@@ -112,11 +114,6 @@ module Max_value_counter =
let find_max_value t =
try Some (Max_value_counter.find t) with Not_found -> None
-let raise_error msg =
- Aorai_option.fatal "Aorai plugin internal error. \nStatus : %s.\n" msg;;
-(* Format.printf "Aorai plugin internal error. \nStatus : %s.\n" msg; *)
-(* assert false *)
-
let por t1 t2 =
match t1,t2 with
PTrue,_ | _,PTrue -> PTrue
@@ -165,7 +162,7 @@ let add_logic name log_info = Hashtbl.replace declared_logics name log_info
let get_logic name =
try Hashtbl.find declared_logics name
with Not_found ->
- raise_error ("Logic function '"^name^"' not declared in hashtbl")
+ Aorai_option.fatal "Logic function '%s' not declared in hashtbl" name
let declared_predicates = Hashtbl.create 97
@@ -174,7 +171,8 @@ let add_predicate name pred_info =
let get_predicate name =
try Hashtbl.find declared_predicates name
- with Not_found -> raise_error ("Predicate '"^name^"' not declared in hashtbl")
+ with Not_found ->
+ Aorai_option.fatal "Predicate '%s' not declared in hashtbl" name
(* ************************************************************************* *)
(* Some constant names used for generation *)
@@ -1003,6 +1001,7 @@ let add_if_needed states st =
else states
let rec type_seq default_state tr metaenv env needs_pebble curr_start curr_end seq =
+ let dkey = typing_dkey in
let loc = Cil_datatype.Location.unknown in
match seq with
| [] -> (* We identify start and end. *)
@@ -1049,7 +1048,7 @@ let rec type_seq default_state tr metaenv env needs_pebble curr_start curr_end s
|| is_single_trans || at_most_one -> curr_end
| _ -> new_intermediate_state ()
in
- Aorai_option.debug "Examining single elt:@\n%s -> %s:@[%a@]"
+ Aorai_option.debug ~dkey "Examining single elt:@\n%s -> %s:@[%a@]"
curr_start.name my_end.name Promelaoutput.Parsed.print_seq_elt elt;
let guard_exit_loop env current counter =
if is_opt then TTrue
@@ -1172,21 +1171,24 @@ let rec type_seq default_state tr metaenv env needs_pebble curr_start curr_end s
let make_counter_term st =
Logic_const.term (TLval (make_counter st)) (Ctype Cil.intType)
in
- Aorai_option.debug "Inner start is %s; Inner end is %s"
+ Aorai_option.debug ~dkey "Inner start is %s; Inner end is %s"
inner_start.name inner_end.name;
let treat_state (states, oth_trans) st =
let trans = Path_analysis.get_transitions_of_state st auto in
if st.nums = inner_start.nums then begin
let loop_trans =
- if needs_counter then begin
+ if has_loop then begin
List.fold_left
(fun acc tr ->
- let init_action = Counter_init (make_counter tr.stop) in
- let init_actions = init_action :: tr.actions in
+ let init_actions =
+ if needs_counter then
+ Counter_init (make_counter tr.stop) :: tr.actions
+ else tr.actions
+ in
let init_trans =
new_trans st tr.stop tr.cross init_actions
in
- Aorai_option.debug "New init trans %a"
+ Aorai_option.debug ~dkey "New init trans %a"
print_eps_trans init_trans;
if at_most_one then init_trans :: acc
else begin
@@ -1213,7 +1215,7 @@ let rec type_seq default_state tr metaenv env needs_pebble curr_start curr_end s
let loop_trans =
new_trans inner_end tr.stop loop_cross loop_actions
in
- Aorai_option.debug "New loop trans %a"
+ Aorai_option.debug ~dkey "New loop trans %a"
print_eps_trans loop_trans;
init_trans :: loop_trans :: acc
end)
@@ -1252,7 +1254,7 @@ let rec type_seq default_state tr metaenv env needs_pebble curr_start curr_end s
in
let min_cond = Epsilon min_cond in
let exit_trans = new_trans inner_end oth_start min_cond [] in
- Aorai_option.debug "New exit trans %a"
+ Aorai_option.debug ~dkey "New exit trans %a"
print_eps_trans exit_trans;
let trans = exit_trans :: trans @ oth_trans in
states, trans
@@ -1321,6 +1323,7 @@ let find_otherwise_trans auto st =
with Not_found -> None
let type_trans auto metaenv env tr =
+ let dkey = typing_dkey in
let needs_pebble = not (single_path auto tr) in
let has_siblings =
match Path_analysis.get_transitions_of_state tr.start auto with
@@ -1329,7 +1332,7 @@ let type_trans auto metaenv env tr =
| [ _ ] -> false (* We only have one sequence to exit from there anyway *)
| _::_::_ -> true
in
- Aorai_option.debug
+ Aorai_option.debug ~dkey
"Analyzing transition %s -> %s: %a (needs pebble: %B)"
tr.start.name tr.stop.name
Promelaoutput.Parsed.print_guard
@@ -1397,7 +1400,7 @@ let type_trans auto metaenv env tr =
| [] | [ _ ] -> false
| _::_::_ -> true
in
- Aorai_option.debug "Resulting transitions:@\n%a"
+ Aorai_option.debug ~dkey "Resulting transitions:@\n%a"
(Pretty_utils.pp_list ~sep:"@\n"
(fun fmt tr -> Format.fprintf fmt "%a"
print_eps_trans tr))
@@ -1421,7 +1424,7 @@ let add_reject_trans auto intermediate_states =
match cond with
TFalse -> states,trans
| _ ->
- Aorai_option.debug
+ Aorai_option.debug ~dkey:typing_dkey
"Adding default transition %s -> %s: %a"
st.name reject_state.name Promelaoutput.Typed.print_condition cond;
states, new_trans st reject_state cond [] :: trans
@@ -1429,6 +1432,7 @@ let add_reject_trans auto intermediate_states =
List.fold_left treat_one_state auto intermediate_states
let propagate_epsilon_transitions (states, _ as auto) =
+ let dkey = typing_dkey in
let rec transitive_closure start conds actions known_states curr =
let known_states = curr :: known_states in
let trans = Path_analysis.get_transitions_of_state curr auto in
@@ -1436,8 +1440,8 @@ let propagate_epsilon_transitions (states, _ as auto) =
(fun acc tr ->
match tr.cross with
| Epsilon cond ->
- Aorai_option.debug "Treating epsilon trans %s -> %s"
- curr.name tr.stop.name;
+ Aorai_option.debug ~dkey
+ "Treating epsilon trans %s -> %s" curr.name tr.stop.name;
if List.exists (fun st -> st.nums = tr.stop.nums) known_states
then acc
else
@@ -1445,7 +1449,8 @@ let propagate_epsilon_transitions (states, _ as auto) =
start (tand cond conds) (tr.actions @ actions)
known_states tr.stop @ acc
| Normal cond ->
- Aorai_option.debug "Adding transition %s -> %s from epsilon trans"
+ Aorai_option.debug ~dkey
+ "Adding transition %s -> %s from epsilon trans"
start.name tr.stop.name;
let tr =
new_trans start tr.stop (tand cond conds) (tr.actions @ actions)
@@ -1460,31 +1465,31 @@ let propagate_epsilon_transitions (states, _ as auto) =
(states, trans)
let add_default_trans (states, transitions as auto) otherwise =
+ let dkey = typing_dkey in
let add_one_trans acc tr =
let st = tr.start in
let my_trans = Path_analysis.get_transitions_of_state st auto in
- Aorai_option.debug "Considering new otherwise transition: %s -> %s"
+ Aorai_option.debug ~dkey "Considering new otherwise transition: %s -> %s"
st.name tr.stop.name;
let cond =
List.fold_left
(fun acc c ->
let cond = c.cross in
- Aorai_option.debug "considering trans %s -> %s: %a"
+ Aorai_option.debug ~dkey "considering trans %s -> %s: %a"
c.start.name c.stop.name Promelaoutput.Typed.print_condition cond;
let neg = tnot cond in
- Aorai_option.debug "negation: %a"
+ Aorai_option.debug ~dkey "negation: %a"
Promelaoutput.Typed.print_condition neg;
- Aorai_option.debug "acc: %a"
+ Aorai_option.debug ~dkey "acc: %a"
Promelaoutput.Typed.print_condition acc;
let res = tand acc (tnot cond) in
- Aorai_option.debug "partial result: %a"
+ Aorai_option.debug ~dkey "partial result: %a"
Promelaoutput.Typed.print_condition res;
- res
- )
+ res)
TTrue
my_trans
in
- Aorai_option.debug "resulting transition: %a"
+ Aorai_option.debug ~dkey "resulting transition: %a"
Promelaoutput.Typed.print_condition cond;
let cond,_ = Logic_simplification.simplifyCond cond in
let new_trans = new_trans st tr.stop cond [] in
@@ -1494,6 +1499,7 @@ let add_default_trans (states, transitions as auto) otherwise =
states, transitions
let type_cond_auto auto =
+ let dkey = typing_dkey in
let original_auto = auto in
let otherwise = List.filter (fun t -> t.cross = Otherwise) auto.trans in
let add_if_needed acc st =
@@ -1503,9 +1509,9 @@ let type_cond_auto auto =
let (intermediate_states, trans, needs_reject) =
type_trans (auto.states,auto.trans) auto.metavariables [] tr
in
- Aorai_option.debug
+ Aorai_option.debug ~dkey
"Considering parsed transition %s -> %s" tr.start.name tr.stop.name;
- Aorai_option.debug
+ Aorai_option.debug ~dkey
"Resulting transitions:@\n%a@\nEnd of transitions"
(Pretty_utils.pp_list ~sep:"@\n" print_eps_trans) trans;
let add_reject =
@@ -1537,7 +1543,7 @@ let type_cond_auto auto =
| None -> auto
in
let auto = { original_auto with states ; trans } in
- if Aorai_option.debug_atleast 1 then
+ if Aorai_option.is_debug_key_enabled typing_dkey then
Promelaoutput.Typed.output_dot_automata auto "aorai_debug_typed.dot";
let (_,trans) =
List.fold_left
@@ -1622,7 +1628,7 @@ let setAutomata auto =
Automaton.set (Some auto);
check_states "typed automaton";
check_observables auto;
- if Aorai_option.debug_atleast 1 then
+ if Aorai_option.is_debug_key_enabled typing_dkey then
Promelaoutput.Typed.output_dot_automata auto "aorai_debug_reduced.dot";
if (Array.length !cond_of_parametrizedTransitions) <
(getNumberOfTransitions ())
@@ -1716,7 +1722,7 @@ let set_varinfo = Aux_varinfos.add
let get_varinfo name =
try
Aux_varinfos.find name
- with Not_found -> raise_error ("Variable not declared ("^name^")")
+ with Not_found -> Aorai_option.fatal "Variable %s not declared" name
let get_logic_var name =
let vi = get_varinfo name in Cil.cvar_to_lvar vi
@@ -1740,8 +1746,8 @@ let get_paraminfo funcname paramname =
try
Paraminfos.find (funcname,paramname)
with Not_found ->
- raise_error
- ("Parameter '"^paramname^"' not declared for function '"^funcname^"'.")
+ Aorai_option.fatal
+ "Parameter '%s' not declared for function '%s'." paramname funcname
(* Add a new param into the association table funcname -> varinfo *)
let set_returninfo funcname vi =
@@ -1754,7 +1760,7 @@ let get_returninfo funcname =
try
Paraminfos.find (funcname,"\\return")
with Not_found ->
- raise_error ("Return varinfo not declared for function '"^funcname^"'.")
+ Aorai_option.fatal "Return varinfo not declared for function '%s'." funcname
type range =
| Fixed of int (** constant value *)
@@ -2040,10 +2046,10 @@ let set_kf_init_state kf state =
let set _ = state in
ignore (Pre_state.memo ~change set kf)
-let dkey = Aorai_option.register_category "dataflow"
+let dataflow_dkey = Aorai_option.register_category "dataflow"
let replace_kf_init_state kf state =
- Aorai_option.debug ~dkey
+ Aorai_option.debug ~dkey:dataflow_dkey
"Replacing pre-state of %a:@\n @[%a@]"
Kernel_function.pretty kf pretty_state state;
Pre_state.replace kf state
@@ -2149,7 +2155,7 @@ let pretty_loop_invariant fmt =
Format.fprintf fmt "Function %a, sid %d:@\n @[%a@]@\n"
Kernel_function.pretty kf stmt.sid pretty_state state)
-let debug_computed_state ?(dkey=dkey) () =
+let debug_computed_state ?(dkey=dataflow_dkey) () =
Aorai_option.debug ~dkey
"Computed state:@\nPre-states:@\n @[%t@]@\nPost-states:@\n @[%t@]@\n\
Loop init:@\n @[%t@]@\nLoop invariants:@\n @[%t@]"
@@ -2259,7 +2265,7 @@ let set_usedinfo name einfo =
let get_usedinfo name =
try Hashtbl.find used_enuminfo name
- with Not_found -> raise_error ("Incomplete enum information.")
+ with Not_found -> Aorai_option.fatal "Incomplete enum information."
let get_cenum_option name =
let opnamed = func_to_op_func name in
@@ -2298,12 +2304,13 @@ let func_to_cenum func =
let rec search = function
| {einame = n} as ei ::_ when n=name -> CEnum ei
| _::l -> search l
- | [] -> raise_error
- ("Operation '"^name^"' not found in operations enumeration")
+ | [] ->
+ Aorai_option.fatal
+ "Operation '%s' not found in operations enumeration" name
in
search ei.eitems
(* CEnum(ex,s,ei)*)
- with Not_found -> raise_error ("Operation not found")
+ with Not_found -> Aorai_option.fatal "Operation not found"
let op_status_to_cenum status =
try
@@ -2312,14 +2319,7 @@ let op_status_to_cenum status =
let rec search = function
| {einame=n} as ei ::_ when n=name -> CEnum ei
| _::l -> search l
- | [] -> raise_error ("Status not found")
+ | [] -> Aorai_option.fatal "Status not found"
in
search ei.eitems
- with Not_found -> raise_error ("Status not found")
-
-
-(*
-Local Variables:
-compile-command: "make -C ../../.."
-End:
-*)
+ with Not_found -> Aorai_option.fatal "Status not found"
diff --git a/src/plugins/aorai/tests/ya/oracle/seq_unlimited.err.oracle b/src/plugins/aorai/tests/ya/oracle/seq_unlimited.err.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/src/plugins/aorai/tests/ya/oracle/seq_unlimited.res.oracle b/src/plugins/aorai/tests/ya/oracle/seq_unlimited.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..34b512d70052d27304c093e5971904d4d1a2a1a0
--- /dev/null
+++ b/src/plugins/aorai/tests/ya/oracle/seq_unlimited.res.oracle
@@ -0,0 +1,452 @@
+[kernel] Parsing seq_unlimited.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_seq_unlimited_0.i (no preprocessing)
+/* Generated by Frama-C */
+enum aorai_States {
+ aorai_intermediate_state = 0,
+ aorai_intermediate_state_0 = 1,
+ aorai_intermediate_state_1 = 2,
+ aorai_reject = 3,
+ b = 4,
+ c = 5,
+ fst = 6,
+ ok = 7
+};
+enum aorai_ListOper {
+ op_find = 2,
+ op_init = 1,
+ op_main = 0
+};
+enum aorai_OpStatusList {
+ aorai_Terminated = 1,
+ aorai_Called = 0
+};
+/*@ check lemma ok_deterministic_trans{L}: \true;
+ */
+/*@ check lemma fst_deterministic_trans{L}: \true;
+ */
+/*@ check lemma c_deterministic_trans{L}: \true;
+ */
+/*@ check lemma b_deterministic_trans{L}: \true;
+ */
+/*@ check lemma aorai_reject_deterministic_trans{L}: \true;
+ */
+/*@ check lemma aorai_intermediate_state_deterministic_trans{L}: \true;
+ */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
+/*@
+check lemma aorai_intermediate_state_1_deterministic_trans{L}:
+ ¬(\at(aorai_CurOperation,L) ≡ op_find ∧
+ \at(aorai_CurOpStatus,L) ≡ aorai_Terminated ∧
+ ¬(\at(aorai_CurOperation,L) ≡ op_find ∧
+ \at(aorai_CurOpStatus,L) ≡ aorai_Terminated));
+ */
+/*@
+check lemma aorai_intermediate_state_0_deterministic_trans{L}:
+ ¬(\at(aorai_CurOperation,L) ≡ op_find ∧
+ \at(aorai_CurOpStatus,L) ≡ aorai_Called ∧
+ \at(aorai_CurOperation,L) ≡ op_main ∧
+ \at(aorai_CurOpStatus,L) ≡ aorai_Terminated);
+ */
+/*@ ghost int aorai_CurStates = fst; */
+/*@ ghost
+ /@ requires aorai_CurStates ≡ b;
+ ensures aorai_CurOpStatus ≡ aorai_Called;
+ ensures aorai_CurOperation ≡ op_init;
+ assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+
+ behavior buch_state_aorai_intermediate_state_in:
+ assumes aorai_CurStates ≡ b;
+ ensures aorai_CurStates ≡ aorai_intermediate_state;
+
+ behavior buch_state_aorai_intermediate_state_out:
+ assumes aorai_CurStates ≢ b;
+ ensures aorai_CurStates ≢ aorai_intermediate_state;
+
+ behavior buch_state_aorai_intermediate_state_0_out:
+ ensures aorai_CurStates ≢ aorai_intermediate_state_0;
+
+ behavior buch_state_aorai_intermediate_state_1_out:
+ ensures aorai_CurStates ≢ aorai_intermediate_state_1;
+
+ behavior buch_state_aorai_reject_out:
+ ensures aorai_CurStates ≢ aorai_reject;
+
+ behavior buch_state_b_out:
+ ensures aorai_CurStates ≢ b;
+
+ behavior buch_state_c_out:
+ ensures aorai_CurStates ≢ c;
+
+ behavior buch_state_fst_out:
+ ensures aorai_CurStates ≢ fst;
+
+ behavior buch_state_ok_out:
+ ensures aorai_CurStates ≢ ok;
+ @/
+ void init_pre_func(int *a, int n)
+ {
+ /@ slevel full; @/
+ aorai_CurOpStatus = aorai_Called;
+ aorai_CurOperation = op_init;
+ if (4 == aorai_CurStates) aorai_CurStates = aorai_intermediate_state;
+ else aorai_CurStates = aorai_reject;
+ return;
+ }
+
+*/
+
+/*@ ghost
+ /@ requires aorai_CurStates ≡ aorai_intermediate_state;
+ ensures aorai_CurOpStatus ≡ aorai_Terminated;
+ ensures aorai_CurOperation ≡ op_init;
+ assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+
+ behavior buch_state_aorai_intermediate_state_out:
+ ensures aorai_CurStates ≢ aorai_intermediate_state;
+
+ behavior buch_state_aorai_intermediate_state_0_out:
+ ensures aorai_CurStates ≢ aorai_intermediate_state_0;
+
+ behavior buch_state_aorai_intermediate_state_1_out:
+ ensures aorai_CurStates ≢ aorai_intermediate_state_1;
+
+ behavior buch_state_aorai_reject_out:
+ ensures aorai_CurStates ≢ aorai_reject;
+
+ behavior buch_state_b_out:
+ ensures aorai_CurStates ≢ b;
+
+ behavior buch_state_c_in:
+ assumes aorai_CurStates ≡ aorai_intermediate_state;
+ ensures aorai_CurStates ≡ c;
+
+ behavior buch_state_c_out:
+ assumes aorai_CurStates ≢ aorai_intermediate_state;
+ ensures aorai_CurStates ≢ c;
+
+ behavior buch_state_fst_out:
+ ensures aorai_CurStates ≢ fst;
+
+ behavior buch_state_ok_out:
+ ensures aorai_CurStates ≢ ok;
+ @/
+ void init_post_func(void)
+ {
+ /@ slevel full; @/
+ aorai_CurOpStatus = aorai_Terminated;
+ aorai_CurOperation = op_init;
+ if (0 == aorai_CurStates) aorai_CurStates = c;
+ else aorai_CurStates = aorai_reject;
+ return;
+ }
+
+*/
+
+/*@ requires aorai_CurStates ≡ b;
+
+ behavior Buchi_property_behavior:
+ ensures aorai_CurStates ≡ c;
+ */
+void init(int *a, int n)
+{
+ /*@ ghost int aorai_Loop_Init_2; */
+ /*@ ghost init_pre_func(a,n); */
+ int i = 0;
+ /*@ ghost aorai_Loop_Init_2 = 1; */
+ aorai_loop_2:
+ /*@ loop invariant Aorai: aorai_CurStates ≡ aorai_intermediate_state;
+ loop invariant Aorai: aorai_CurStates ≢ aorai_intermediate_state_0;
+ loop invariant Aorai: aorai_CurStates ≢ aorai_intermediate_state_1;
+ loop invariant Aorai: aorai_CurStates ≢ aorai_reject;
+ loop invariant Aorai: aorai_CurStates ≢ b;
+ loop invariant Aorai: aorai_CurStates ≢ c;
+ loop invariant Aorai: aorai_CurStates ≢ fst;
+ loop invariant Aorai: aorai_CurStates ≢ ok;
+ */
+ while (i < n) {
+ /*@ ghost aorai_Loop_Init_2 = 0; */
+ *(a + i) = i;
+ i ++;
+ }
+ /*@ ghost init_post_func(); */
+ return;
+}
+
+/*@ ghost
+ /@ requires
+ aorai_CurStates ≡ aorai_intermediate_state_0 ∨
+ aorai_CurStates ≡ c;
+ ensures aorai_CurOpStatus ≡ aorai_Called;
+ ensures aorai_CurOperation ≡ op_find;
+ assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+
+ behavior buch_state_aorai_intermediate_state_out:
+ ensures aorai_CurStates ≢ aorai_intermediate_state;
+
+ behavior buch_state_aorai_intermediate_state_0_out:
+ ensures aorai_CurStates ≢ aorai_intermediate_state_0;
+
+ behavior buch_state_aorai_intermediate_state_1_in:
+ assumes
+ aorai_CurStates ≡ c ∨
+ aorai_CurStates ≡ aorai_intermediate_state_0;
+ ensures aorai_CurStates ≡ aorai_intermediate_state_1;
+
+ behavior buch_state_aorai_intermediate_state_1_out:
+ assumes
+ aorai_CurStates ≢ c ∧
+ aorai_CurStates ≢ aorai_intermediate_state_0;
+ ensures aorai_CurStates ≢ aorai_intermediate_state_1;
+
+ behavior buch_state_aorai_reject_out:
+ ensures aorai_CurStates ≢ aorai_reject;
+
+ behavior buch_state_b_out:
+ ensures aorai_CurStates ≢ b;
+
+ behavior buch_state_c_out:
+ ensures aorai_CurStates ≢ c;
+
+ behavior buch_state_fst_out:
+ ensures aorai_CurStates ≢ fst;
+
+ behavior buch_state_ok_out:
+ ensures aorai_CurStates ≢ ok;
+ @/
+ void find_pre_func(int *a, int n, int k)
+ {
+ /@ slevel full; @/
+ aorai_CurOpStatus = aorai_Called;
+ aorai_CurOperation = op_find;
+ if (5 == aorai_CurStates) aorai_CurStates = aorai_intermediate_state_1;
+ else
+ if (1 == aorai_CurStates) aorai_CurStates = aorai_intermediate_state_1;
+ else aorai_CurStates = aorai_reject;
+ return;
+ }
+
+*/
+
+/*@ ghost
+ /@ requires aorai_CurStates ≡ aorai_intermediate_state_1;
+ ensures aorai_CurOpStatus ≡ aorai_Terminated;
+ ensures aorai_CurOperation ≡ op_find;
+ assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+
+ behavior buch_state_aorai_intermediate_state_out:
+ ensures aorai_CurStates ≢ aorai_intermediate_state;
+
+ behavior buch_state_aorai_intermediate_state_0_in:
+ assumes aorai_CurStates ≡ aorai_intermediate_state_1;
+ ensures aorai_CurStates ≡ aorai_intermediate_state_0;
+
+ behavior buch_state_aorai_intermediate_state_0_out:
+ assumes aorai_CurStates ≢ aorai_intermediate_state_1;
+ ensures aorai_CurStates ≢ aorai_intermediate_state_0;
+
+ behavior buch_state_aorai_intermediate_state_1_out:
+ ensures aorai_CurStates ≢ aorai_intermediate_state_1;
+
+ behavior buch_state_aorai_reject_out:
+ ensures aorai_CurStates ≢ aorai_reject;
+
+ behavior buch_state_b_out:
+ ensures aorai_CurStates ≢ b;
+
+ behavior buch_state_c_out:
+ ensures aorai_CurStates ≢ c;
+
+ behavior buch_state_fst_out:
+ ensures aorai_CurStates ≢ fst;
+
+ behavior buch_state_ok_out:
+ ensures aorai_CurStates ≢ ok;
+ @/
+ void find_post_func(int res)
+ {
+ /@ slevel full; @/
+ aorai_CurOpStatus = aorai_Terminated;
+ aorai_CurOperation = op_find;
+ if (2 == aorai_CurStates) aorai_CurStates = aorai_intermediate_state_0;
+ else aorai_CurStates = aorai_reject;
+ return;
+ }
+
+*/
+
+/*@ requires
+ aorai_CurStates ≡ aorai_intermediate_state_0 ∨
+ aorai_CurStates ≡ c;
+ requires aorai_CurStates ≡ c ∨ aorai_CurStates ≢ c;
+ requires
+ aorai_CurStates ≡ aorai_intermediate_state_0 ∨
+ aorai_CurStates ≢ aorai_intermediate_state_0;
+
+ behavior Buchi_property_behavior:
+ ensures aorai_CurStates ≡ aorai_intermediate_state_0;
+ */
+int find(int *a, int n, int k)
+{
+ int __retres;
+ /*@ ghost find_pre_func(a,n,k); */
+ {
+ /*@ ghost int aorai_Loop_Init_12; */
+ int i = 0;
+ /*@ ghost aorai_Loop_Init_12 = 1; */
+ aorai_loop_12:
+ /*@ loop invariant Aorai: aorai_CurStates ≢ aorai_intermediate_state;
+ loop invariant Aorai: aorai_CurStates ≢ aorai_intermediate_state_0;
+ loop invariant Aorai: aorai_CurStates ≡ aorai_intermediate_state_1;
+ loop invariant Aorai: aorai_CurStates ≢ aorai_reject;
+ loop invariant Aorai: aorai_CurStates ≢ b;
+ loop invariant Aorai: aorai_CurStates ≢ c;
+ loop invariant Aorai: aorai_CurStates ≢ fst;
+ loop invariant Aorai: aorai_CurStates ≢ ok;
+ loop invariant
+ Aorai:
+ aorai_Loop_Init_12 ≢ 0 ⇒
+ \at(aorai_CurStates ≢ aorai_intermediate_state_0,Pre) ∧
+ \at(aorai_CurStates ≢ c,Pre) ⇒
+ aorai_CurStates ≢ aorai_intermediate_state_1;
+ */
+ while (i < n) {
+ /*@ ghost aorai_Loop_Init_12 = 0; */
+ if (*(a + i) == k) {
+ __retres = i;
+ goto return_label;
+ }
+ i ++;
+ }
+ }
+ __retres = -1;
+ return_label: {
+ /*@ ghost find_post_func(__retres); */
+ return __retres;
+ }
+}
+
+/*@ ghost
+ /@ requires aorai_CurStates ≡ fst;
+ ensures aorai_CurOpStatus ≡ aorai_Called;
+ ensures aorai_CurOperation ≡ op_main;
+ assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+
+ behavior buch_state_aorai_intermediate_state_out:
+ ensures aorai_CurStates ≢ aorai_intermediate_state;
+
+ behavior buch_state_aorai_intermediate_state_0_out:
+ ensures aorai_CurStates ≢ aorai_intermediate_state_0;
+
+ behavior buch_state_aorai_intermediate_state_1_out:
+ ensures aorai_CurStates ≢ aorai_intermediate_state_1;
+
+ behavior buch_state_aorai_reject_out:
+ ensures aorai_CurStates ≢ aorai_reject;
+
+ behavior buch_state_b_in:
+ assumes aorai_CurStates ≡ fst;
+ ensures aorai_CurStates ≡ b;
+
+ behavior buch_state_b_out:
+ assumes aorai_CurStates ≢ fst;
+ ensures aorai_CurStates ≢ b;
+
+ behavior buch_state_c_out:
+ ensures aorai_CurStates ≢ c;
+
+ behavior buch_state_fst_out:
+ ensures aorai_CurStates ≢ fst;
+
+ behavior buch_state_ok_out:
+ ensures aorai_CurStates ≢ ok;
+ @/
+ void main_pre_func(void)
+ {
+ /@ slevel full; @/
+ aorai_CurOpStatus = aorai_Called;
+ aorai_CurOperation = op_main;
+ if (6 == aorai_CurStates) aorai_CurStates = b;
+ else aorai_CurStates = aorai_reject;
+ return;
+ }
+
+*/
+
+/*@ ghost
+ /@ requires aorai_CurStates ≡ aorai_intermediate_state_0;
+ ensures aorai_CurOpStatus ≡ aorai_Terminated;
+ ensures aorai_CurOperation ≡ op_main;
+ assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
+
+ behavior buch_state_aorai_intermediate_state_out:
+ ensures aorai_CurStates ≢ aorai_intermediate_state;
+
+ behavior buch_state_aorai_intermediate_state_0_out:
+ ensures aorai_CurStates ≢ aorai_intermediate_state_0;
+
+ behavior buch_state_aorai_intermediate_state_1_out:
+ ensures aorai_CurStates ≢ aorai_intermediate_state_1;
+
+ behavior buch_state_aorai_reject_out:
+ ensures aorai_CurStates ≢ aorai_reject;
+
+ behavior buch_state_b_out:
+ ensures aorai_CurStates ≢ b;
+
+ behavior buch_state_c_out:
+ ensures aorai_CurStates ≢ c;
+
+ behavior buch_state_fst_out:
+ ensures aorai_CurStates ≢ fst;
+
+ behavior buch_state_ok_in:
+ assumes aorai_CurStates ≡ aorai_intermediate_state_0;
+ ensures aorai_CurStates ≡ ok;
+
+ behavior buch_state_ok_out:
+ assumes aorai_CurStates ≢ aorai_intermediate_state_0;
+ ensures aorai_CurStates ≢ ok;
+ @/
+ void main_post_func(int res)
+ {
+ /@ slevel full; @/
+ aorai_CurOpStatus = aorai_Terminated;
+ aorai_CurOperation = op_main;
+ if (1 == aorai_CurStates) aorai_CurStates = ok;
+ else aorai_CurStates = aorai_reject;
+ return;
+ }
+
+*/
+
+/*@ requires aorai_CurStates ≡ fst;
+
+ behavior aorai_acceptance:
+ ensures aorai_CurStates ≡ ok;
+
+ behavior Buchi_property_behavior:
+ ensures aorai_CurStates ≡ ok;
+ */
+int main(void)
+{
+ int __retres;
+ int a[10];
+ int tmp_0;
+ /*@ ghost main_pre_func(); */
+ init(a,10);
+ tmp_0 = find(a,10,5);
+ if (tmp_0) {
+ int tmp;
+ tmp = find(a,10,11);
+ __retres = tmp;
+ goto return_label;
+ }
+ __retres = 0;
+ return_label: {
+ /*@ ghost main_post_func(__retres); */
+ return __retres;
+ }
+}
+
+
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/seq_unlimited.err.oracle b/src/plugins/aorai/tests/ya/oracle_prove/seq_unlimited.err.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/seq_unlimited.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/seq_unlimited.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..3bd12d5c212d4e6f54d11739fba841aebbe2c7ee
--- /dev/null
+++ b/src/plugins/aorai/tests/ya/oracle_prove/seq_unlimited.res.oracle
@@ -0,0 +1,3 @@
+[kernel] Parsing seq_unlimited.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_seq_unlimited_0_prove.i (no preprocessing)
+[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ya/seq_unlimited.i b/src/plugins/aorai/tests/ya/seq_unlimited.i
new file mode 100644
index 0000000000000000000000000000000000000000..950ffc1141c8ffe3123ed0b20becdd9a27b3e12c
--- /dev/null
+++ b/src/plugins/aorai/tests/ya/seq_unlimited.i
@@ -0,0 +1,23 @@
+/*run.config*
+ STDOPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-acceptance
+*/
+void init(int *a, int n)
+{
+ for(int i = 0; i < n; i++)
+ *(a+i) = i;
+}
+
+int find(int *a, int n, int k)
+{
+ for(int i = 0; i < n; i++)
+ if (a[i] == k) return i;
+ return -1;
+}
+
+int main(void)
+{
+ int a[10];
+ init(a, 10);
+ if (find(a, 10, 5))
+ return find(a, 10, 11);
+}
diff --git a/src/plugins/aorai/tests/ya/seq_unlimited.ya b/src/plugins/aorai/tests/ya/seq_unlimited.ya
new file mode 100644
index 0000000000000000000000000000000000000000..521e5168a94e18d73882e26c8e11338f476faf49
--- /dev/null
+++ b/src/plugins/aorai/tests/ya/seq_unlimited.ya
@@ -0,0 +1,8 @@
+%init: fst;
+%accept: ok;
+%deterministic;
+fst : { CALL(main) } -> b;
+b : { init() } -> c;
+c: { find()+ } -> ok;
+ok: { RETURN(main) } -> ok;
+