From f786e99de759893c2922f2893e29374fdbbda21a Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Wed, 12 Dec 2018 20:51:00 +0100
Subject: [PATCH] [Aorai] Add a list of observables
- add an "observables" option at the begining of ya files
- multiple "observables" options merges together (union of symbols)
- check that every function referred to is inside the observable list
- remove the initial curOperation and curOpStatus : the main function is
not necessarily observable and the pre/post function will set those
variables anyway
- ignore unobservables functions inside the relevant visitors
---
src/plugins/aorai/aorai_dataflow.ml | 12 +-
src/plugins/aorai/aorai_utils.ml | 56 ++----
src/plugins/aorai/aorai_visitors.ml | 176 +++++++++---------
src/plugins/aorai/data_for_aorai.ml | 82 ++++----
src/plugins/aorai/data_for_aorai.mli | 18 +-
src/plugins/aorai/promelaast.mli | 1 +
src/plugins/aorai/promelaparser.mly | 11 +-
src/plugins/aorai/promelaparser_withexps.mly | 11 +-
.../aorai/tests/ltl/oracle/goto.res.oracle | 4 +-
.../tests/ltl/oracle/test_boucle.res.oracle | 4 +-
.../tests/ltl/oracle/test_boucle1.res.oracle | 4 +-
.../tests/ltl/oracle/test_boucle2.res.oracle | 4 +-
.../tests/ltl/oracle/test_boucle3.res.oracle | 4 +-
.../ltl/oracle/test_factorial.res.oracle | 4 +-
.../ltl/oracle/test_recursion1.res.oracle | 4 +-
.../ltl/oracle/test_recursion2.0.res.oracle | 4 +-
.../ltl/oracle/test_recursion2.1.res.oracle | 4 +-
.../tests/ltl/oracle/test_switch2.res.oracle | 4 +-
.../tests/ltl/oracle/test_switch3.res.oracle | 4 +-
.../test_switch3_et_recursion.res.oracle | 4 +-
.../ltl/oracle/test_switch3_if.res.oracle | 4 +-
.../ltl/oracle/test_switch3_return.res.oracle | 4 +-
.../tests/ya/oracle/assigns.0.res.oracle | 4 +-
.../tests/ya/oracle/assigns.1.res.oracle | 4 +-
.../tests/ya/oracle/bts1289.0.res.oracle | 4 +-
.../tests/ya/oracle/bts1289.1.res.oracle | 4 +-
.../ya/oracle/declared_function.res.oracle | 4 +-
.../tests/ya/oracle/deterministic.res.oracle | 4 +-
.../aorai/tests/ya/oracle/formals.res.oracle | 4 +-
.../generate_assigns_bts1290.res.oracle | 4 +-
.../tests/ya/oracle/hoare_seq.res.oracle | 4 +-
.../tests/ya/oracle/incorrect.res.oracle | 4 +-
.../tests/ya/oracle/loop_bts1050.res.oracle | 4 +-
.../ya/oracle/metavariables-right.res.oracle | 4 +-
.../tests/ya/oracle/monostate.res.oracle | 4 +-
.../aorai/tests/ya/oracle/not_prm.res.oracle | 4 +-
.../aorai/tests/ya/oracle/other.res.oracle | 4 +-
.../aorai/tests/ya/oracle/seq.res.oracle | 4 +-
.../aorai/tests/ya/oracle/seq_loop.res.oracle | 4 +-
.../tests/ya/oracle/single_call.res.oracle | 4 +-
.../oracle/singleassignment-right.res.oracle | 4 +-
.../aorai/tests/ya/oracle/stack.res.oracle | 4 +-
.../ya/oracle/test_acces_params.res.oracle | 4 +-
.../ya/oracle/test_acces_params2.res.oracle | 4 +-
.../test_boucle_rechercheTableau.res.oracle | 4 +-
.../tests/ya/oracle/test_factorial.res.oracle | 4 +-
.../ya/oracle/test_recursion4.res.oracle | 4 +-
.../ya/oracle/test_recursion5.res.oracle | 4 +-
.../tests/ya/oracle/test_struct.res.oracle | 4 +-
src/plugins/aorai/yaparser.mly | 30 ++-
50 files changed, 299 insertions(+), 262 deletions(-)
diff --git a/src/plugins/aorai/aorai_dataflow.ml b/src/plugins/aorai/aorai_dataflow.ml
index 13bf13719f7..35cd5f132a0 100644
--- a/src/plugins/aorai/aorai_dataflow.ml
+++ b/src/plugins/aorai/aorai_dataflow.ml
@@ -430,7 +430,7 @@ module Computer(I: Init) = struct
let do_call s f args (state,loops as d) =
let kf = Globals.Functions.get f in
- if Data_for_aorai.isIgnoredFunction (Kernel_function.get_name kf)
+ if Data_for_aorai.isIgnoredFunction kf
then d (* we simply skip ignored functions. *)
else begin
set_call_state s state;
@@ -532,7 +532,7 @@ module Computer(I: Init) = struct
end
let compute_func_aux stack call_site kf init_state =
- if Data_for_aorai.isIgnoredFunction (Kernel_function.get_name kf) then
+ if Data_for_aorai.isIgnoredFunction kf then
Aorai_option.fatal "compute_func on function %a which is ignored by Aorai"
Kernel_function.pretty kf
else if List.mem_assq kf stack then begin
@@ -620,7 +620,7 @@ let () = compute_func := compute_func_aux
let compute_forward () =
let kf = Globals.Functions.find_by_name (Kernel.MainFunction.get()) in
- if Data_for_aorai.isIgnoredFunction (Kernel_function.get_name kf) then
+ if Data_for_aorai.isIgnoredFunction kf then
Aorai_option.abort "Main function %a is ignored by Aorai"
Kernel_function.pretty kf;
let (states,_) = Data_for_aorai.getGraph () in
@@ -757,7 +757,7 @@ struct
let do_call s f state =
let kf = Globals.Functions.get f in
- if Data_for_aorai.isIgnoredFunction (Kernel_function.get_name kf)
+ if Data_for_aorai.isIgnoredFunction kf
then Dataflow2.Default (* we simply skip ignored functions. *)
else begin
try
@@ -912,7 +912,7 @@ let filter_init_state restrict initial map acc =
with Not_found -> acc
let backward_analysis_aux stack kf ret_state =
- if (Data_for_aorai.isIgnoredFunction (Kernel_function.get_name kf)) then
+ if Data_for_aorai.isIgnoredFunction kf then
Aorai_option.fatal
"Call backward analysis on ignored function %a" Kernel_function.pretty kf
else if List.memq kf stack then begin
@@ -1002,7 +1002,7 @@ let () = backward_analysis := backward_analysis_aux
let compute_backward () =
let kf = Globals.Functions.find_by_name (Kernel.MainFunction.get()) in
- if Data_for_aorai.isIgnoredFunction (Kernel_function.get_name kf) then
+ if Data_for_aorai.isIgnoredFunction kf then
Aorai_option.abort "Main function %a is ignored by Aorai"
Kernel_function.pretty kf;
let final_state = Data_for_aorai.get_kf_return_state kf in
diff --git a/src/plugins/aorai/aorai_utils.ml b/src/plugins/aorai/aorai_utils.ml
index 341fb420f6d..7615b72d83c 100644
--- a/src/plugins/aorai/aorai_utils.ml
+++ b/src/plugins/aorai/aorai_utils.ml
@@ -629,6 +629,16 @@ let crosscond_to_exp generated_kf curr_f curr_status loc cond res =
(** Local copy of the file pointer *)
let file = ref Cil.dummyFile
+let initFunction kf =
+ let fname = Kernel_function.get_name kf in
+ List.iter
+ (fun vi -> set_paraminfo fname vi.vname vi)
+ (Kernel_function.get_formals kf);
+ match (Kernel_function.find_return kf).skind with
+ | Cil_types.Return (Some { enode = Lval (Var vi,NoOffset) },_) ->
+ set_returninfo fname vi (* Add the vi of return stmt *)
+ | exception Kernel_function.No_Statement | _ -> () (* function without returned value *)
+
(** Copy the file pointer locally in the class in order to ease globals
management and initializes some tables. *)
let initFile f =
@@ -636,27 +646,7 @@ let initFile f =
Data_for_aorai.setCData ();
(* Adding C variables into our hashtable *)
Globals.Vars.iter (fun vi _ -> set_varinfo vi.vname vi);
- Globals.Functions.iter
- (fun kf ->
- let fname = Kernel_function.get_name kf in
- List.iter
- (fun vi -> set_paraminfo fname vi.vname vi)
- (Kernel_function.get_formals kf);
- if not (Data_for_aorai.isIgnoredFunction fname) then
- begin
- try
- let ret = Kernel_function.find_return kf in
- match ret.skind with
- | Cil_types.Return (Some e,_) ->
- (match e.enode with
- | Lval (Var vi,NoOffset) ->
- set_returninfo fname vi (* Add the vi of return stmt *)
- | _ -> () (* function without returned value *))
- | _ -> () (* function without returned value *)
- with Kernel_function.No_Statement ->
- Aorai_option.fatal
- "Don't know what to do with a function declaration"
- end)
+ Globals.Functions.iter initFunction
(** List of globals awaiting for adding into C file globals *)
let globals_queue = ref []
@@ -760,6 +750,11 @@ let mk_global_c_enum_type name elements =
let mk_global_c_initialized_enum name name_enuminfo ini =
mk_global_c_initialized_vars name (TEnum(get_usedinfo name_enuminfo,[])) ini
+let mk_global_c_enum name name_enuminfo =
+ let init = {Cil_types.init=None} in
+ mk_global_c_initialized_enum name name_enuminfo init
+
+
(* ************************************************************************* *)
(** {b Terms management / computation} *)
@@ -913,15 +908,6 @@ let mk_global_states_init root =
mk_global_var_init var { Cil_types.init = Some init})
states
-let func_to_init name =
- {Cil_types.init=
- Some(SingleInit(
- new_exp ~loc:(CurrentLoc.get()) (Const(func_to_cenum (name)))))}
-
-let funcStatus_to_init st =
- {Cil_types.init=Some(SingleInit(new_exp ~loc:(CurrentLoc.get())
- (Const(op_status_to_cenum (st)))))}
-
class visit_decl_loops_init () =
object(self)
inherit Visitor.frama_c_inplace
@@ -1138,13 +1124,11 @@ let initGlobals root complete =
mk_global_c_enum_type
listOp
(List.map
- (fun e -> func_to_op_func e)
- (getFunctions_from_c() @ getIgnoredFunctions()));
- mk_global_c_initialized_enum curOp listOp
- (func_to_init (Kernel_function.get_name root));
+ (fun kf -> func_to_op_func (Kernel_function.get_name kf))
+ (getObservablesFunctions() @ getIgnoredFunctions()));
+ mk_global_c_enum curOp listOp;
mk_global_c_enum_type listStatus (callStatus::[termStatus]);
- mk_global_c_initialized_enum
- curOpStatus listStatus (funcStatus_to_init Promelaast.Call);
+ mk_global_c_enum curOpStatus listStatus;
mk_global_comment "//* ";
mk_global_comment "//* States and Trans Variables";
diff --git a/src/plugins/aorai/aorai_visitors.ml b/src/plugins/aorai/aorai_visitors.ml
index f771e840669..7ceadc22a61 100644
--- a/src/plugins/aorai/aorai_visitors.ml
+++ b/src/plugins/aorai/aorai_visitors.ml
@@ -118,100 +118,106 @@ class visit_adding_code_for_synchronisation =
val aux_post_table = Kernel_function.Hashtbl.create 17
+ method do_fundec fundec loc =
+ let kf = Extlib.the self#current_kf in
+ let vi = Kernel_function.get_vi kf in
+ let vi_pre = Cil_const.copy_with_new_vid vi in
+ vi_pre.vname <- Data_for_aorai.get_fresh (vi_pre.vname ^ "_pre_func");
+ vi_pre.vdefined <- true;
+ vi_pre.vghost <- true;
+ Cil_datatype.Varinfo.Hashtbl.add func_orig_table vi_pre (Pre_func kf);
+ (* TODO:
+ - what about protos that have no specified args
+ (NB: cannot be identified here because of implem of Kernel_function).
+ - what about varargs?
+ *)
+ let (rettype,args,varargs,_) = Cil.splitFunctionTypeVI vi_pre in
+ Cil.update_var_type vi_pre (TFun(Cil.voidType, args, varargs,[]));
+ vi_pre.vattr <- [];
+
+ (* in particular get rid of __no_return if set in vi*)
+
+ let arg =
+ if Cil.isVoidType rettype
+ then []
+ else ["res",rettype,[]]
+ in
+ let vi_post =
+ Cil.makeGlobalVar ~ghost:true
+ (Data_for_aorai.get_fresh (vi.vname ^ "_post_func"))
+ (TFun(voidType,Some arg,false,[]))
+ in
+ Kernel_function.Hashtbl.add aux_post_table kf vi_post;
+ Cil_datatype.Varinfo.Hashtbl.add func_orig_table vi_post (Post_func kf);
+ let fun_dec_pre = Cil.emptyFunctionFromVI vi_pre in
+ let fun_dec_post = Cil.emptyFunctionFromVI vi_post in
+ (* For a future analysis of function arguments,
+ we have to update the function's formals. Search
+ for LBLsformals. *)
+ Cil.setFunctionTypeMakeFormals
+ fun_dec_pre (TFun(Cil.voidType, args, varargs,[]));
+ Cil.setFunctionTypeMakeFormals
+ fun_dec_post (TFun(voidType,Some arg,false,[]));
+ (* We will now fill the function with the result
+ of the automaton's analysis. *)
+ Globals.Functions.replace_by_definition
+ (Cil.empty_funspec()) fun_dec_pre loc;
+ Globals.Functions.replace_by_definition
+ (Cil.empty_funspec()) fun_dec_post loc;
+ let kf_pre = Globals.Functions.get vi_pre in
+ let kf_post = Globals.Functions.get vi_post in
+ let aux_func_pre, pre_block,pre_locals = mk_pre_fct_block kf_pre kf in
+ let aux_func_post, post_block,post_locals =
+ mk_post_fct_block
+ kf_post kf (Extlib.opt_of_list fun_dec_post.sformals)
+ in
+ fun_dec_pre.slocals <- pre_locals;
+ fun_dec_pre.sbody <- pre_block;
+ fun_dec_pre.svar.vdefined <- true;
+ fun_dec_post.slocals <- post_locals;
+ fun_dec_post.sbody <- post_block;
+ fun_dec_post.svar.vdefined <- true;
+ let aux_funcs =
+ Cil_datatype.Varinfo.Set.union aux_func_pre aux_func_post
+ in
+ let globs =
+ Cil_datatype.Varinfo.Set.fold
+ (fun x acc ->
+ GFunDecl(Cil.empty_funspec(),x,loc) :: acc) aux_funcs
+ [ GFun(fun_dec_pre,loc); GFun(fun_dec_post,loc)]
+ in
+ Cil_datatype.Varinfo.Set.iter (add_aux_bhv kf) aux_funcs;
+ fundec.sbody.bstmts <-
+ Cil.mkStmtOneInstr ~ghost:true
+ (Call(None,Cil.evar ~loc vi_pre,
+ List.map (fun x -> Cil.evar ~loc x)
+ (Kernel_function.get_formals kf),
+ loc))
+ :: fundec.sbody.bstmts;
+ (* Finally, we update the CFG for the new fundec *)
+ let keepSwitch = Kernel.KeepSwitch.get() in
+ Cfg.prepareCFG ~keepSwitch fun_dec_pre;
+ Cfg.cfgFun fun_dec_pre;
+ Cfg.prepareCFG ~keepSwitch fun_dec_post;
+ Cfg.cfgFun fun_dec_post;
+ globs
+
method! vglob_aux g =
match g with
| GFun (fundec,loc) ->
- let kf = Option.get self#current_kf in
- let vi = Kernel_function.get_vi kf in
- let vi_pre = Cil_const.copy_with_new_vid vi in
- vi_pre.vname <- Data_for_aorai.get_fresh (vi_pre.vname ^ "_pre_func");
- vi_pre.vdefined <- true;
- vi_pre.vghost <- true;
- Cil_datatype.Varinfo.Hashtbl.add func_orig_table vi_pre (Pre_func kf);
- (* TODO:
- - what about protos that have no specified args
- (NB: cannot be identified here because of implem of Kernel_function).
- - what about varargs?
- *)
- let (rettype,args,varargs,_) = Cil.splitFunctionTypeVI vi_pre in
- Cil.update_var_type vi_pre (TFun(Cil.voidType, args, varargs,[]));
- vi_pre.vattr <- [];
-
- (* in particular get rid of __no_return if set in vi*)
-
- let arg =
- if Cil.isVoidType rettype
- then []
- else ["res",rettype,[]]
- in
- let vi_post =
- Cil.makeGlobalVar ~ghost:true
- (Data_for_aorai.get_fresh (vi.vname ^ "_post_func"))
- (TFun(voidType,Some arg,false,[]))
- in
- Kernel_function.Hashtbl.add aux_post_table kf vi_post;
- Cil_datatype.Varinfo.Hashtbl.add func_orig_table vi_post (Post_func kf);
- let fun_dec_pre = Cil.emptyFunctionFromVI vi_pre in
- let fun_dec_post = Cil.emptyFunctionFromVI vi_post in
- (* For a future analysis of function arguments,
- we have to update the function's formals. Search
- for LBLsformals. *)
- Cil.setFunctionTypeMakeFormals
- fun_dec_pre (TFun(Cil.voidType, args, varargs,[]));
- Cil.setFunctionTypeMakeFormals
- fun_dec_post (TFun(voidType,Some arg,false,[]));
- (* We will now fill the function with the result
- of the automaton's analysis. *)
- Globals.Functions.replace_by_definition
- (Cil.empty_funspec()) fun_dec_pre loc;
- Globals.Functions.replace_by_definition
- (Cil.empty_funspec()) fun_dec_post loc;
- let kf_pre = Globals.Functions.get vi_pre in
- let kf_post = Globals.Functions.get vi_post in
- let aux_func_pre, pre_block,pre_locals = mk_pre_fct_block kf_pre kf in
- let aux_func_post, post_block,post_locals =
- mk_post_fct_block
- kf_post kf (Extlib.opt_of_list fun_dec_post.sformals)
- in
- fun_dec_pre.slocals <- pre_locals;
- fun_dec_pre.sbody <- pre_block;
- fun_dec_pre.svar.vdefined <- true;
- fun_dec_post.slocals <- post_locals;
- fun_dec_post.sbody <- post_block;
- fun_dec_post.svar.vdefined <- true;
- let aux_funcs =
- Cil_datatype.Varinfo.Set.union aux_func_pre aux_func_post
- in
- let globs =
- Cil_datatype.Varinfo.Set.fold
- (fun x acc ->
- GFunDecl(Cil.empty_funspec(),x,loc) :: acc) aux_funcs
- [ GFun(fun_dec_pre,loc); GFun(fun_dec_post,loc)]
- in
- Cil_datatype.Varinfo.Set.iter (add_aux_bhv kf) aux_funcs;
- fundec.sbody.bstmts <-
- Cil.mkStmtOneInstr ~ghost:true
- (Call(None,Cil.evar ~loc vi_pre,
- List.map (fun x -> Cil.evar ~loc x)
- (Kernel_function.get_formals kf),
- loc))
- :: fundec.sbody.bstmts;
- (* Finally, we update the CFG for the new fundec *)
- let keepSwitch = Kernel.KeepSwitch.get() in
- Cfg.prepareCFG ~keepSwitch fun_dec_pre;
- Cfg.cfgFun fun_dec_pre;
- Cfg.prepareCFG ~keepSwitch fun_dec_post;
- Cfg.cfgFun fun_dec_post;
- ChangeDoChildrenPost([g], fun x -> globs @ x)
+ let kf = Globals.Functions.get fundec.svar in
+ if Data_for_aorai.isObservableFunction kf then
+ let globs = self#do_fundec fundec loc in
+ ChangeDoChildrenPost([g], fun x -> globs @ x)
+ else
+ DoChildren
| _ -> DoChildren
method! vstmt_aux stmt =
match stmt.skind with
| Return (res,loc) ->
let kf = Option.get self#current_kf in
- let vi = Kernel_function.get_vi kf in
- let current_function = vi.vname in
- if not (Data_for_aorai.isIgnoredFunction current_function) then begin
+ if Data_for_aorai.isObservableFunction kf then begin
let args = match res with
| None -> []
| Some exp -> [Cil.copy_exp exp]
diff --git a/src/plugins/aorai/data_for_aorai.ml b/src/plugins/aorai/data_for_aorai.ml
index ec4242b8b79..157f44778f2 100644
--- a/src/plugins/aorai/data_for_aorai.ml
+++ b/src/plugins/aorai/data_for_aorai.ml
@@ -211,11 +211,9 @@ let automata = ref None
(* Each transition with a parametrized cross condition (call param access or return value access) has its parametrized part stored in this array. *)
let cond_of_parametrizedTransitions = ref (Array.make (1) [[]])
-(* List of variables name observed in the C file *)
-let variables_from_c = ref []
-(* List of functions name observed in the C file *)
-let functions_from_c = ref []
-(* List of functions call observed in the C file without declaration *)
+(* List of functions defined in the C file *)
+let defined_functions = ref []
+(* List of functions without declaration *)
let ignored_functions = ref []
(** Return the buchi automata as stored after parsing *)
@@ -1545,6 +1543,27 @@ let checkMetavariableCompatibility auto =
"The use of metavariables is incompatible with non-deterministic \
automata, such as automa using extended transitions."
+let check_observables auto =
+ match auto.observables with
+ | None -> () (* No observable list set, everything is observable *)
+ | Some set ->
+ let is_relevant name =
+ try
+ ignore (Globals.Functions.find_by_name name)
+ with Not_found ->
+ Aorai_option.fatal "Observable %s doesn't match any function" name
+ in
+ let rec check = function
+ | TAnd (c1,c2) | TOr (c1,c2) -> check c1; check c2
+ | TNot (c) -> check c
+ | TRel _ | TTrue | TFalse -> ()
+ | TCall (kf,_) | TReturn kf ->
+ let name = Kernel_function.get_name kf in
+ if not (Datatype.String.Set.mem name set) then
+ Aorai_option.fatal "Function %s is not observable" name
+ in
+ Datatype.String.Set.iter is_relevant set;
+ List.iter (fun tr -> check tr.cross) auto.trans
(** Stores the buchi automaton and its variables and
functions as it is returned by the parsing *)
@@ -1553,6 +1572,7 @@ let setAutomata auto =
let auto = type_cond_auto auto in
automata:=Some auto;
check_states "typed automata";
+ check_observables auto;
if Aorai_option.debug_atleast 1 then
Promelaoutput.Typed.output_dot_automata auto "aorai_debug_reduced.dot";
if (Array.length !cond_of_parametrizedTransitions) <
@@ -1577,41 +1597,39 @@ let setCData () =
let (f_decl,f_def) =
Globals.Functions.fold
(fun f (lf_decl,lf_def) ->
- let name = (Kernel_function.get_name f) in
match f.fundec with
- | Definition _ -> (lf_decl,name::lf_def)
- | Declaration _ -> (name::lf_decl,lf_def))
+ | Definition _ -> (lf_decl, f :: lf_def)
+ | Declaration _ -> (f :: lf_decl, lf_def))
([],[])
in
- functions_from_c:=f_def;
- ignored_functions:=f_decl;
- variables_from_c:=
- Globals.Vars.fold
- (fun v _ lv ->
- Format.asprintf "%a" Cil_datatype.Varinfo.pretty v :: lv)
- []
+ defined_functions := f_def;
+ ignored_functions := f_decl
-(** Return the list of all function name observed in the C file, except ignored functions. *)
-let getFunctions_from_c () =
- (!functions_from_c)
+let addIgnoredFunction kf =
+ ignored_functions := kf :: !ignored_functions
-(** Return the list of all variables name observed in the C file. *)
-let getVariables_from_c () =
- (!variables_from_c)
+(** Return true if and only if the given string fname denotes an ignored function. *)
+let isIgnoredFunction kf =
+ List.exists (Kernel_function.equal kf) !ignored_functions
-(** Return the list of names of all ignored functions. A function is ignored if it is used in C file and if its declaration is unavailable. *)
-let getIgnoredFunctions () =
- (!ignored_functions)
+let isDeclaredObservable kf =
+ let auto = getAutomata () in
+ let fname = Kernel_function.get_name kf in
+ match auto.observables with
+ | None -> true
+ | Some set ->
+ Datatype.String.Set.mem fname set
-(** Return the list of names of all ignored functions. A function is ignored if it is used in C file and if its declaration is unavailable. *)
-let addIgnoredFunction fname =
- ignored_functions:=fname::(!ignored_functions)
+let isObservableFunction kf =
+ not (isIgnoredFunction kf) && isDeclaredObservable kf
-(** Return true if and only if the given string fname denotes an ignored function. *)
-let isIgnoredFunction fname =
- List.exists
- (fun s -> (String.compare fname s)=0)
- (!ignored_functions)
+(** Return the list of all function name observed in the C file, except ignored functions. *)
+let getObservablesFunctions () =
+ List.filter isDeclaredObservable !defined_functions
+
+(** Return the list of names of observable but ignored functions. A function is ignored if it is used in C file and if its declaration is unavailable. *)
+let getIgnoredFunctions () =
+ List.filter isDeclaredObservable !ignored_functions
let is_reject_state state =
match Reject_state.get_option () with
diff --git a/src/plugins/aorai/data_for_aorai.mli b/src/plugins/aorai/data_for_aorai.mli
index 8c7ed586075..786ca7217fb 100644
--- a/src/plugins/aorai/data_for_aorai.mli
+++ b/src/plugins/aorai/data_for_aorai.mli
@@ -218,20 +218,20 @@ val getNumberOfTransitions : unit -> int
(** return the number of states of the automata *)
val getNumberOfStates : unit -> int
-(** Return the list of all function name observed in the C file. *)
-val getFunctions_from_c : unit -> string list
+(** Return the list of all function name observed in the C file, except ignored functions. *)
+val getObservablesFunctions : unit -> Cil_types.kernel_function list
-(** Return the list of all variables name observed in the C file. *)
-val getVariables_from_c : unit -> string list
+(** Return the list of names of observable but ignored functions. A function is ignored if it is used in C file and if its declaration is unavailable. *)
+val getIgnoredFunctions : unit -> Cil_types.kernel_function list
(** Return the list of names of all ignored functions. A function is ignored if it is used in C file and if its declaration is unavailable. *)
-val getIgnoredFunctions : unit -> string list
-
-(** Return the list of names of all ignored functions. A function is ignored if it is used in C file and if its declaration is unavailable. *)
-val addIgnoredFunction : string -> unit
+val addIgnoredFunction : Cil_types.kernel_function -> unit
(** Return true if and only if the given string fname denotes an ignored function. *)
-val isIgnoredFunction : string -> bool
+val isIgnoredFunction : Cil_types.kernel_function -> bool
+
+(** Return true if and onfly if the given function can be observed *)
+val isObservableFunction : Cil_types.kernel_function -> bool
(** returns the state of given index.
@since Nitrogen-20111001
diff --git a/src/plugins/aorai/promelaast.mli b/src/plugins/aorai/promelaast.mli
index fe0bdcfe677..833e13eddde 100644
--- a/src/plugins/aorai/promelaast.mli
+++ b/src/plugins/aorai/promelaast.mli
@@ -142,6 +142,7 @@ type ('c,'a) automaton = {
states: state list;
trans: (('c,'a) trans) list;
metavariables: Cil_types.varinfo Datatype.String.Map.t;
+ observables: Datatype.String.Set.t option;
}
type parsed_automaton = (guard, action) automaton
diff --git a/src/plugins/aorai/promelaparser.mly b/src/plugins/aorai/promelaparser.mly
index 4bcac643722..1badbbe38a9 100644
--- a/src/plugins/aorai/promelaparser.mly
+++ b/src/plugins/aorai/promelaparser.mly
@@ -77,7 +77,10 @@ promela
st::l
) observed_states []
in
- { states; trans = $3; metavariables = Datatype.String.Map.empty }
+ { states; trans = $3;
+ metavariables = Datatype.String.Map.empty;
+ observables = None;
+ }
}
| PROMELA_NEVER PROMELA_LBRACE states PROMELA_SEMICOLON
PROMELA_RBRACE EOF {
@@ -91,7 +94,11 @@ promela
st::l
) observed_states []
in
- { states; trans = $3; metavariables = Datatype.String.Map.empty } }
+ { states; trans = $3;
+ metavariables = Datatype.String.Map.empty;
+ observables = None;
+ }
+ }
;
states
diff --git a/src/plugins/aorai/promelaparser_withexps.mly b/src/plugins/aorai/promelaparser_withexps.mly
index bf852a65f37..4f8abab8a0e 100644
--- a/src/plugins/aorai/promelaparser_withexps.mly
+++ b/src/plugins/aorai/promelaparser_withexps.mly
@@ -88,7 +88,10 @@ promela
st::l
) observed_states []
in
- { states; trans = $3; metavariables = Datatype.String.Map.empty }
+ { states; trans = $3;
+ metavariables = Datatype.String.Map.empty;
+ observables = None;
+ }
}
| PROMELA_NEVER PROMELA_LBRACE states
PROMELA_SEMICOLON PROMELA_RBRACE EOF {
@@ -102,7 +105,11 @@ promela
st::l
) observed_states []
in
- { states; trans = $3; metavariables = Datatype.String.Map.empty } }
+ { states; trans = $3;
+ metavariables = Datatype.String.Map.empty;
+ observables = None;
+ }
+ }
;
states
diff --git a/src/plugins/aorai/tests/ltl/oracle/goto.res.oracle b/src/plugins/aorai/tests/ltl/oracle/goto.res.oracle
index c1554953000..265c294b60c 100644
--- a/src/plugins/aorai/tests/ltl/oracle/goto.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/goto.res.oracle
@@ -18,8 +18,8 @@ int status = 0;
int rr = 1;
/*@ global invariant inv: 0 ≤ rr ≤ 5000;
*/
-/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
-/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
/*@ ghost int accept_S2 = 0; */
/*@ ghost int accept_S3 = 0; */
/*@ ghost int accept_S4 = 0; */
diff --git a/src/plugins/aorai/tests/ltl/oracle/test_boucle.res.oracle b/src/plugins/aorai/tests/ltl/oracle/test_boucle.res.oracle
index af9bc71a2b3..84419238102 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_boucle.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_boucle.res.oracle
@@ -16,8 +16,8 @@ enum aorai_OpStatusList {
};
extern int call_to_an_undefined_function(void);
-/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
-/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
/*@ ghost int T0_S2 = 0; */
/*@ ghost int T0_init = 1; */
/*@ ghost int accept_S1 = 0; */
diff --git a/src/plugins/aorai/tests/ltl/oracle/test_boucle1.res.oracle b/src/plugins/aorai/tests/ltl/oracle/test_boucle1.res.oracle
index 9da27b6622e..d48aaf2d91e 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_boucle1.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_boucle1.res.oracle
@@ -17,8 +17,8 @@ int cpt = 3;
int status = 0;
/*@ global invariant inv_status: 0 ≤ status ≤ 1;
*/
-/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
-/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
/*@ ghost int accept_S1 = 0; */
/*@ ghost int accept_S2 = 0; */
/*@ ghost int accept_S3 = 0; */
diff --git a/src/plugins/aorai/tests/ltl/oracle/test_boucle2.res.oracle b/src/plugins/aorai/tests/ltl/oracle/test_boucle2.res.oracle
index 3b6f510bb85..8491e8c23ed 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_boucle2.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_boucle2.res.oracle
@@ -15,8 +15,8 @@ int status = 0;
int rr = 1;
/*@ global invariant inv: 0 ≤ rr ≤ 50;
*/
-/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
-/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
/*@ ghost int T0_S2 = 0; */
/*@ ghost int T0_init = 1; */
/*@ ghost int accept_S3 = 0; */
diff --git a/src/plugins/aorai/tests/ltl/oracle/test_boucle3.res.oracle b/src/plugins/aorai/tests/ltl/oracle/test_boucle3.res.oracle
index 0e2861364d6..4521080b3e1 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_boucle3.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_boucle3.res.oracle
@@ -15,8 +15,8 @@ int status = 0;
int rr = 1;
/*@ global invariant inv: 0 ≤ rr ≤ 50;
*/
-/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
-/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
/*@ ghost int T0_S4 = 0; */
/*@ ghost int T0_init = 1; */
/*@ ghost int T1_S2 = 0; */
diff --git a/src/plugins/aorai/tests/ltl/oracle/test_factorial.res.oracle b/src/plugins/aorai/tests/ltl/oracle/test_factorial.res.oracle
index 76309462d15..c1aac176071 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_factorial.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_factorial.res.oracle
@@ -11,8 +11,8 @@ enum aorai_OpStatusList {
aorai_Terminated = 1,
aorai_Called = 0
};
-/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
-/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
/*@ ghost int accept_S1 = 0; */
/*@ ghost int accept_S2 = 0; */
/*@ ghost int accept_init = 1; */
diff --git a/src/plugins/aorai/tests/ltl/oracle/test_recursion1.res.oracle b/src/plugins/aorai/tests/ltl/oracle/test_recursion1.res.oracle
index c3757b98233..eaaac90fdb2 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_recursion1.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_recursion1.res.oracle
@@ -45,8 +45,8 @@ axiomatic string_len {
predicate valid_string{L}(char *s) =
\valid(s) ∧ \valid(s + (0 .. string_len(s)));
*/
-/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
-/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
/*@ ghost int T0_S2 = 0; */
/*@ ghost int T0_init = 1; */
/*@ ghost int accept_S1 = 0; */
diff --git a/src/plugins/aorai/tests/ltl/oracle/test_recursion2.0.res.oracle b/src/plugins/aorai/tests/ltl/oracle/test_recursion2.0.res.oracle
index fd43837e998..eb681fba1c9 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_recursion2.0.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_recursion2.0.res.oracle
@@ -60,8 +60,8 @@ axiomatic sum_tab {
}
*/
int global_argc = 0;
-/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
-/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
/*@ ghost int S1 = 0; */
/*@ ghost int T0_init = 1; */
/*@ ghost int T1 = 0; */
diff --git a/src/plugins/aorai/tests/ltl/oracle/test_recursion2.1.res.oracle b/src/plugins/aorai/tests/ltl/oracle/test_recursion2.1.res.oracle
index a40a3eae304..e92778bcb0c 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_recursion2.1.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_recursion2.1.res.oracle
@@ -60,8 +60,8 @@ axiomatic sum_tab {
}
*/
int global_argc = 0;
-/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
-/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
/*@ ghost int S1 = 0; */
/*@ ghost int T0_init = 1; */
/*@ ghost int T1 = 0; */
diff --git a/src/plugins/aorai/tests/ltl/oracle/test_switch2.res.oracle b/src/plugins/aorai/tests/ltl/oracle/test_switch2.res.oracle
index 2ceecc16fc1..41a59d023f0 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_switch2.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_switch2.res.oracle
@@ -20,8 +20,8 @@ int status = 0;
int rr = 1;
/*@ global invariant inv: 0 ≤ rr ≤ 50;
*/
-/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
-/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
/*@ ghost int accept_S2 = 0; */
/*@ ghost int accept_S3 = 0; */
/*@ ghost int accept_S4 = 0; */
diff --git a/src/plugins/aorai/tests/ltl/oracle/test_switch3.res.oracle b/src/plugins/aorai/tests/ltl/oracle/test_switch3.res.oracle
index d81509eb536..4ed3b4a39a1 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_switch3.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_switch3.res.oracle
@@ -11,8 +11,8 @@ enum aorai_OpStatusList {
aorai_Terminated = 1,
aorai_Called = 0
};
-/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
-/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
/*@ ghost int T0_S2 = 0; */
/*@ ghost int T0_init = 1; */
/*@ ghost int accept_S1 = 0; */
diff --git a/src/plugins/aorai/tests/ltl/oracle/test_switch3_et_recursion.res.oracle b/src/plugins/aorai/tests/ltl/oracle/test_switch3_et_recursion.res.oracle
index e5154fb8581..62566d6ad71 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_switch3_et_recursion.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_switch3_et_recursion.res.oracle
@@ -13,8 +13,8 @@ enum aorai_OpStatusList {
aorai_Terminated = 1,
aorai_Called = 0
};
-/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
-/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
/*@ ghost int T0_S2 = 0; */
/*@ ghost int T0_init = 1; */
/*@ ghost int accept_S1 = 0; */
diff --git a/src/plugins/aorai/tests/ltl/oracle/test_switch3_if.res.oracle b/src/plugins/aorai/tests/ltl/oracle/test_switch3_if.res.oracle
index 5cc019fcad4..88b0352589b 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_switch3_if.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_switch3_if.res.oracle
@@ -11,8 +11,8 @@ enum aorai_OpStatusList {
aorai_Terminated = 1,
aorai_Called = 0
};
-/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
-/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
/*@ ghost int T0_S2 = 0; */
/*@ ghost int T0_init = 1; */
/*@ ghost int accept_S1 = 0; */
diff --git a/src/plugins/aorai/tests/ltl/oracle/test_switch3_return.res.oracle b/src/plugins/aorai/tests/ltl/oracle/test_switch3_return.res.oracle
index 0fb781bb704..9e0438a0e71 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_switch3_return.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_switch3_return.res.oracle
@@ -11,8 +11,8 @@ enum aorai_OpStatusList {
aorai_Terminated = 1,
aorai_Called = 0
};
-/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
-/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
/*@ ghost int T0_S2 = 0; */
/*@ ghost int T0_init = 1; */
/*@ ghost int accept_S1 = 0; */
diff --git a/src/plugins/aorai/tests/ya/oracle/assigns.0.res.oracle b/src/plugins/aorai/tests/ya/oracle/assigns.0.res.oracle
index 09b37de9a73..f4acc040245 100644
--- a/src/plugins/aorai/tests/ya/oracle/assigns.0.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/assigns.0.res.oracle
@@ -11,8 +11,8 @@ enum aorai_OpStatusList {
aorai_Called = 0
};
int X;
-/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
-/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
/*@ ghost int S1 = 1; */
/*@ ghost int S2 = 0; */
/*@ ghost int S_in_f = 0; */
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 fd7526444df..28be1b6491e 100644
--- a/src/plugins/aorai/tests/ya/oracle/assigns.1.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/assigns.1.res.oracle
@@ -29,8 +29,8 @@ enum aorai_OpStatusList {
/*@ check lemma S1_deterministic_trans{L}: \true;
*/
int X;
-/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
-/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
/*@ ghost int aorai_CurStates = S1; */
/*@ ghost
/@ requires aorai_CurStates ≡ Sf;
diff --git a/src/plugins/aorai/tests/ya/oracle/bts1289.0.res.oracle b/src/plugins/aorai/tests/ya/oracle/bts1289.0.res.oracle
index 74d55944211..ded70303a39 100644
--- a/src/plugins/aorai/tests/ya/oracle/bts1289.0.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/bts1289.0.res.oracle
@@ -11,8 +11,8 @@ enum aorai_OpStatusList {
aorai_Terminated = 1,
aorai_Called = 0
};
-/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
-/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
/*@ ghost int S = 0; */
/*@ ghost
/@ requires \false;
diff --git a/src/plugins/aorai/tests/ya/oracle/bts1289.1.res.oracle b/src/plugins/aorai/tests/ya/oracle/bts1289.1.res.oracle
index adebb6ca55a..c7ab7fc71c4 100644
--- a/src/plugins/aorai/tests/ya/oracle/bts1289.1.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/bts1289.1.res.oracle
@@ -10,8 +10,8 @@ enum aorai_OpStatusList {
aorai_Terminated = 1,
aorai_Called = 0
};
-/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
-/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
/*@ ghost int S = 0; */
/*@ ghost int T = 0; */
/*@ ghost int aorai_intermediate_state = 0; */
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 7141a6e1958..9aac8e4561e 100644
--- a/src/plugins/aorai/tests/ya/oracle/declared_function.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/declared_function.res.oracle
@@ -16,8 +16,8 @@ enum aorai_OpStatusList {
};
int f(void);
-/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
-/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
/*@
check lemma I_deterministic_trans{L}:
(∀ int __retres_f;
diff --git a/src/plugins/aorai/tests/ya/oracle/deterministic.res.oracle b/src/plugins/aorai/tests/ya/oracle/deterministic.res.oracle
index 6b9c9095bc9..eac5b5331de 100644
--- a/src/plugins/aorai/tests/ya/oracle/deterministic.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/deterministic.res.oracle
@@ -35,8 +35,8 @@ enum aorai_OpStatusList {
*/
int X;
int Y;
-/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
-/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
/*@
check lemma S3_deterministic_trans{L}:
∀ int x;
diff --git a/src/plugins/aorai/tests/ya/oracle/formals.res.oracle b/src/plugins/aorai/tests/ya/oracle/formals.res.oracle
index 52323f131b7..1b5982df2b9 100644
--- a/src/plugins/aorai/tests/ya/oracle/formals.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/formals.res.oracle
@@ -28,8 +28,8 @@ enum aorai_OpStatusList {
*/
/*@ check lemma OK_deterministic_trans{L}: \true;
*/
-/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
-/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
/*@
check lemma main_0_deterministic_trans{L}:
∀ int x;
diff --git a/src/plugins/aorai/tests/ya/oracle/generate_assigns_bts1290.res.oracle b/src/plugins/aorai/tests/ya/oracle/generate_assigns_bts1290.res.oracle
index 6d8dc5b0067..a409f76aa7a 100644
--- a/src/plugins/aorai/tests/ya/oracle/generate_assigns_bts1290.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/generate_assigns_bts1290.res.oracle
@@ -9,8 +9,8 @@ enum aorai_OpStatusList {
aorai_Terminated = 1,
aorai_Called = 0
};
-/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
-/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
/*@ ghost int S = 1; */
/*@ ghost
/@ requires 1 ≡ S;
diff --git a/src/plugins/aorai/tests/ya/oracle/hoare_seq.res.oracle b/src/plugins/aorai/tests/ya/oracle/hoare_seq.res.oracle
index ea603b7e865..b8271b7f370 100644
--- a/src/plugins/aorai/tests/ya/oracle/hoare_seq.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/hoare_seq.res.oracle
@@ -10,8 +10,8 @@ enum aorai_OpStatusList {
aorai_Terminated = 1,
aorai_Called = 0
};
-/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
-/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
/*@ ghost int S0 = 1; */
/*@ ghost int Sf = 0; */
/*@ ghost int aorai_intermediate_state = 0; */
diff --git a/src/plugins/aorai/tests/ya/oracle/incorrect.res.oracle b/src/plugins/aorai/tests/ya/oracle/incorrect.res.oracle
index ccfb249eba5..bcd7dddbbf4 100644
--- a/src/plugins/aorai/tests/ya/oracle/incorrect.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/incorrect.res.oracle
@@ -19,8 +19,8 @@ enum aorai_OpStatusList {
*/
int f(void);
-/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
-/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
/*@ ghost int aorai_CurStates = s0; */
/*@ ghost
/@ requires \false;
diff --git a/src/plugins/aorai/tests/ya/oracle/loop_bts1050.res.oracle b/src/plugins/aorai/tests/ya/oracle/loop_bts1050.res.oracle
index ccc98a41d83..926ceb3efd8 100644
--- a/src/plugins/aorai/tests/ya/oracle/loop_bts1050.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/loop_bts1050.res.oracle
@@ -11,8 +11,8 @@ enum aorai_OpStatusList {
aorai_Terminated = 1,
aorai_Called = 0
};
-/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
-/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
/*@ ghost int S0 = 1; */
/*@ ghost int Sf = 0; */
/*@ ghost int aorai_intermediate_state = 0; */
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 39843d1a28e..f9cbea2f85d 100644
--- a/src/plugins/aorai/tests/ya/oracle/metavariables-right.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/metavariables-right.res.oracle
@@ -39,8 +39,8 @@ enum aorai_OpStatusList {
*/
/*@ check lemma a_deterministic_trans{L}: \true;
*/
-/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
-/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
/*@
check lemma b_deterministic_trans{L}:
¬(\at(aorai_CurOperation,L) ≡ op_g ∧
diff --git a/src/plugins/aorai/tests/ya/oracle/monostate.res.oracle b/src/plugins/aorai/tests/ya/oracle/monostate.res.oracle
index 86ceb3e9912..b0789f55dee 100644
--- a/src/plugins/aorai/tests/ya/oracle/monostate.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/monostate.res.oracle
@@ -21,8 +21,8 @@ enum aorai_OpStatusList {
};
/*@ check lemma aorai_reject_deterministic_trans{L}: \true;
*/
-/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
-/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
/*@
check lemma aorai_intermediate_state_deterministic_trans{L}:
¬(\at(aorai_CurOperation,L) ≡ op_main ∧
diff --git a/src/plugins/aorai/tests/ya/oracle/not_prm.res.oracle b/src/plugins/aorai/tests/ya/oracle/not_prm.res.oracle
index 1d964840b06..e2b8af2f5f8 100644
--- a/src/plugins/aorai/tests/ya/oracle/not_prm.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/not_prm.res.oracle
@@ -9,8 +9,8 @@ enum aorai_OpStatusList {
aorai_Terminated = 1,
aorai_Called = 0
};
-/*@ ghost enum aorai_ListOper aorai_CurOperation = op_f; */
-/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
/*@ ghost int S0 = 1; */
/*@ ghost int Sf = 0; */
/*@ ghost
diff --git a/src/plugins/aorai/tests/ya/oracle/other.res.oracle b/src/plugins/aorai/tests/ya/oracle/other.res.oracle
index 8f230ecadb2..24195e41f5e 100644
--- a/src/plugins/aorai/tests/ya/oracle/other.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/other.res.oracle
@@ -12,8 +12,8 @@ enum aorai_OpStatusList {
aorai_Called = 0
};
int x = 0;
-/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
-/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
/*@ ghost int init = 1; */
/*@ ghost int last = 0; */
/*@ ghost int step1 = 0; */
diff --git a/src/plugins/aorai/tests/ya/oracle/seq.res.oracle b/src/plugins/aorai/tests/ya/oracle/seq.res.oracle
index 506dca121a3..ad8e58e2c0a 100644
--- a/src/plugins/aorai/tests/ya/oracle/seq.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/seq.res.oracle
@@ -11,8 +11,8 @@ enum aorai_OpStatusList {
aorai_Terminated = 1,
aorai_Called = 0
};
-/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
-/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
/*@ ghost int S0 = 1; */
/*@ ghost int Sf = 0; */
/*@ ghost int aorai_intermediate_state = 0; */
diff --git a/src/plugins/aorai/tests/ya/oracle/seq_loop.res.oracle b/src/plugins/aorai/tests/ya/oracle/seq_loop.res.oracle
index 91097fdf88b..74c4b90d5d2 100644
--- a/src/plugins/aorai/tests/ya/oracle/seq_loop.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/seq_loop.res.oracle
@@ -11,8 +11,8 @@ enum aorai_OpStatusList {
aorai_Terminated = 1,
aorai_Called = 0
};
-/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
-/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
/*@ ghost int S0 = 1; */
/*@ ghost int Sf = 0; */
/*@ ghost int aorai_intermediate_state = 0; */
diff --git a/src/plugins/aorai/tests/ya/oracle/single_call.res.oracle b/src/plugins/aorai/tests/ya/oracle/single_call.res.oracle
index ee4213fd46c..8140ad900ee 100644
--- a/src/plugins/aorai/tests/ya/oracle/single_call.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/single_call.res.oracle
@@ -9,8 +9,8 @@ enum aorai_OpStatusList {
aorai_Terminated = 1,
aorai_Called = 0
};
-/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
-/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
/*@ ghost int S0 = 1; */
/*@ ghost int Sf = 0; */
/*@ ghost int aorai_intermediate_state = 0; */
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 47bd37cf3ee..964d18945b2 100644
--- a/src/plugins/aorai/tests/ya/oracle/singleassignment-right.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/singleassignment-right.res.oracle
@@ -21,8 +21,8 @@ enum aorai_OpStatusList {
*/
/*@ check lemma a_deterministic_trans{L}: \true;
*/
-/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
-/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
/*@ ghost int aorai_CurStates = a; */
/*@ ghost int aorai_x = 0; */
/*@ ghost int aorai_y = 0; */
diff --git a/src/plugins/aorai/tests/ya/oracle/stack.res.oracle b/src/plugins/aorai/tests/ya/oracle/stack.res.oracle
index 6ca094fa00c..9ff7ca0aecd 100644
--- a/src/plugins/aorai/tests/ya/oracle/stack.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/stack.res.oracle
@@ -27,8 +27,8 @@ enum aorai_OpStatusList {
/*@ check lemma accept_deterministic_trans{L}: \true;
*/
int g = 0;
-/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
-/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
/*@
check lemma empty_stack_deterministic_trans{L}:
¬(\at(aorai_CurOperation,L) ≡ op_push ∧
diff --git a/src/plugins/aorai/tests/ya/oracle/test_acces_params.res.oracle b/src/plugins/aorai/tests/ya/oracle/test_acces_params.res.oracle
index 89553036d1a..20787049401 100644
--- a/src/plugins/aorai/tests/ya/oracle/test_acces_params.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/test_acces_params.res.oracle
@@ -15,8 +15,8 @@ int status = 0;
int rr = 1;
/*@ global invariant inv: 0 ≤ rr ≤ 5000;
*/
-/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
-/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
/*@ ghost int S1 = 0; */
/*@ ghost int S2 = 0; */
/*@ ghost int S3 = 0; */
diff --git a/src/plugins/aorai/tests/ya/oracle/test_acces_params2.res.oracle b/src/plugins/aorai/tests/ya/oracle/test_acces_params2.res.oracle
index 16997723976..c6d27622ae3 100644
--- a/src/plugins/aorai/tests/ya/oracle/test_acces_params2.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/test_acces_params2.res.oracle
@@ -15,8 +15,8 @@ enum aorai_OpStatusList {
int rr = 1;
/*@ global invariant inv: 0 ≤ rr ≤ 5000;
*/
-/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
-/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
/*@ ghost int S1 = 1; */
/*@ ghost int S2 = 0; */
/*@ ghost int S3 = 0; */
diff --git a/src/plugins/aorai/tests/ya/oracle/test_boucle_rechercheTableau.res.oracle b/src/plugins/aorai/tests/ya/oracle/test_boucle_rechercheTableau.res.oracle
index 6bd1a0b39b8..6bb7bed4d31 100644
--- a/src/plugins/aorai/tests/ya/oracle/test_boucle_rechercheTableau.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/test_boucle_rechercheTableau.res.oracle
@@ -15,8 +15,8 @@ enum aorai_OpStatusList {
aorai_Terminated = 1,
aorai_Called = 0
};
-/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
-/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
/*@ ghost int End = 0; */
/*@ ghost int Idle = 1; */
/*@ ghost int WillDoFoo = 0; */
diff --git a/src/plugins/aorai/tests/ya/oracle/test_factorial.res.oracle b/src/plugins/aorai/tests/ya/oracle/test_factorial.res.oracle
index 009f14f70dd..ef459e69225 100644
--- a/src/plugins/aorai/tests/ya/oracle/test_factorial.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/test_factorial.res.oracle
@@ -11,8 +11,8 @@ enum aorai_OpStatusList {
aorai_Terminated = 1,
aorai_Called = 0
};
-/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
-/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
/*@ ghost int S1 = 0; */
/*@ ghost int S2 = 0; */
/*@ ghost int main_0 = 1; */
diff --git a/src/plugins/aorai/tests/ya/oracle/test_recursion4.res.oracle b/src/plugins/aorai/tests/ya/oracle/test_recursion4.res.oracle
index cdfe4aba74b..9ff8daac4d0 100644
--- a/src/plugins/aorai/tests/ya/oracle/test_recursion4.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/test_recursion4.res.oracle
@@ -12,8 +12,8 @@ enum aorai_OpStatusList {
aorai_Called = 0
};
#pragma JessieIntegerModel(math)
-/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
-/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
/*@ ghost int End = 0; */
/*@ ghost int Idle = 1; */
/*@ ghost int WillDoFoo = 0; */
diff --git a/src/plugins/aorai/tests/ya/oracle/test_recursion5.res.oracle b/src/plugins/aorai/tests/ya/oracle/test_recursion5.res.oracle
index bc9334eec11..6510597aa4d 100644
--- a/src/plugins/aorai/tests/ya/oracle/test_recursion5.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/test_recursion5.res.oracle
@@ -16,8 +16,8 @@ enum aorai_OpStatusList {
aorai_Terminated = 1,
aorai_Called = 0
};
-/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
-/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
/*@ ghost int End = 0; */
/*@ ghost int Idle = 1; */
/*@ ghost int IgnoreFoo = 0; */
diff --git a/src/plugins/aorai/tests/ya/oracle/test_struct.res.oracle b/src/plugins/aorai/tests/ya/oracle/test_struct.res.oracle
index 0e102ceda96..b73119bb700 100644
--- a/src/plugins/aorai/tests/ya/oracle/test_struct.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/test_struct.res.oracle
@@ -16,8 +16,8 @@ enum aorai_OpStatusList {
};
struct People nobody;
int myAge = 0;
-/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
-/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost enum aorai_ListOper aorai_CurOperation; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
/*@ ghost int S1 = 0; */
/*@ ghost int main_0 = 1; */
/*@ ghost
diff --git a/src/plugins/aorai/yaparser.mly b/src/plugins/aorai/yaparser.mly
index 3a88ed02f8f..699489687f3 100644
--- a/src/plugins/aorai/yaparser.mly
+++ b/src/plugins/aorai/yaparser.mly
@@ -32,7 +32,11 @@ open Logic_ptree
open Promelaast
open Bool3
-type options = Deterministic | Init of string list | Accept of string list
+type options =
+ | Deterministic
+ | Init of string list
+ | Accept of string list
+ | Observables of string list
let to_seq c =
[{ condition = Some c;
@@ -104,13 +108,22 @@ let check_state st =
Aorai_option.abort
"Error: the state '%s' is used but never defined." st.name
-let interpret_option = function
+let interpret_option auto = function
| Init states ->
- List.iter set_init_state states
+ List.iter set_init_state states; auto
| Accept states ->
- List.iter set_accept_state states
+ List.iter set_accept_state states; auto
| Deterministic ->
- Aorai_option.Deterministic.set true
+ Aorai_option.Deterministic.set true; auto
+ | Observables names ->
+ let module Set = Datatype.String.Set in
+ let new_set = Set.of_list names in
+ let observables =
+ match auto.observables with
+ | None -> Some new_set
+ | Some set -> Some (Set.union set new_set)
+ in
+ { auto with observables }
let build_automaton options metavariables trans =
let htable_to_list table = Hashtbl.fold (fun _ st l -> st :: l) table [] in
@@ -119,15 +132,15 @@ let build_automaton options metavariables trans =
and metavariables =
List.fold_left add_metavariable Datatype.String.Map.empty metavariables
in
- List.iter interpret_option options;
+ let auto = { states; trans; metavariables; observables = None } in
+ let auto = List.fold_left interpret_option auto options in
List.iter check_state states;
if not (List.exists (fun st -> st.init=True) states) then
Aorai_option.abort "Automaton does not declare an initial state";
if undefined_states <> [] then
Aorai_option.abort "Error: the state(s) %a are used but never defined."
(Pretty_utils.pp_list ~sep:"," Format.pp_print_string) undefined_states;
- { states; trans; metavariables }
-
+ auto
type pre_cond = Behavior of string | Pre of Promelaast.condition
@@ -169,6 +182,7 @@ option
| "init" -> Init $3
| "accept" -> Accept $3
| "deterministic" -> Deterministic
+ | "observables" -> Observables $3
| _ -> Aorai_option.abort "unknown option: '%s'" $2
}
--
GitLab