From afd399a8f159e59fdf840b7ecc74c5ca9653721e Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Tue, 12 Jan 2021 15:07:24 +0100
Subject: [PATCH] [aorai] remove completely obsolete mechanism for generating C
files
If you want to see instrumented code use `-then-last -print [-ocode file.c]`
like everyone else.
Also properly indent some files
---
.Makefile.lint | 2 -
src/plugins/aorai/aorai_option.ml | 157 ++++++++--------
src/plugins/aorai/aorai_option.mli | 1 -
src/plugins/aorai/aorai_register.ml | 173 ++++++------------
src/plugins/aorai/tests/ltl/goto.c | 2 +-
.../aorai/tests/ltl/oracle/goto.res.oracle | 1 -
.../tests/ltl/oracle/test_boucle.res.oracle | 1 -
.../tests/ltl/oracle/test_boucle1.res.oracle | 1 -
.../tests/ltl/oracle/test_boucle2.res.oracle | 1 -
.../tests/ltl/oracle/test_boucle3.res.oracle | 1 -
.../ltl/oracle/test_factorial.res.oracle | 1 -
.../ltl/oracle/test_recursion1.res.oracle | 1 -
.../ltl/oracle/test_recursion2.0.res.oracle | 1 -
.../ltl/oracle/test_recursion2.1.res.oracle | 1 -
.../tests/ltl/oracle/test_switch2.res.oracle | 1 -
.../tests/ltl/oracle/test_switch3.res.oracle | 1 -
.../test_switch3_et_recursion.res.oracle | 1 -
.../ltl/oracle/test_switch3_if.res.oracle | 1 -
.../ltl/oracle/test_switch3_return.res.oracle | 1 -
.../tests/ltl/oracle_prove/goto.res.oracle | 1 -
.../ltl/oracle_prove/test_boucle.res.oracle | 1 -
.../ltl/oracle_prove/test_boucle1.res.oracle | 1 -
.../ltl/oracle_prove/test_boucle2.res.oracle | 1 -
.../ltl/oracle_prove/test_boucle3.res.oracle | 1 -
.../oracle_prove/test_factorial.res.oracle | 1 -
.../oracle_prove/test_recursion1.res.oracle | 1 -
.../oracle_prove/test_recursion2.0.res.oracle | 1 -
.../oracle_prove/test_recursion2.1.res.oracle | 1 -
.../ltl/oracle_prove/test_switch2.res.oracle | 1 -
.../ltl/oracle_prove/test_switch3.res.oracle | 1 -
.../test_switch3_et_recursion.res.oracle | 1 -
.../oracle_prove/test_switch3_if.res.oracle | 1 -
.../test_switch3_return.res.oracle | 1 -
src/plugins/aorai/tests/ltl/test_boucle.c | 2 +-
src/plugins/aorai/tests/ltl/test_boucle1.c | 2 +-
src/plugins/aorai/tests/ltl/test_boucle2.c | 2 +-
src/plugins/aorai/tests/ltl/test_boucle3.c | 2 +-
src/plugins/aorai/tests/ltl/test_factorial.c | 2 +-
src/plugins/aorai/tests/ltl/test_recursion1.c | 2 +-
src/plugins/aorai/tests/ltl/test_recursion2.c | 4 +-
src/plugins/aorai/tests/ltl/test_switch2.c | 2 +-
src/plugins/aorai/tests/ltl/test_switch3.c | 2 +-
.../tests/ltl/test_switch3_et_recursion.c | 2 +-
src/plugins/aorai/tests/ltl/test_switch3_if.c | 2 +-
.../aorai/tests/ltl/test_switch3_return.c | 2 +-
src/plugins/aorai/tests/ya/assigns.c | 6 +-
src/plugins/aorai/tests/ya/bts1289.i | 4 +-
.../aorai/tests/ya/declared_function.i | 2 +-
src/plugins/aorai/tests/ya/deterministic.i | 2 +-
src/plugins/aorai/tests/ya/formals.i | 2 +-
.../aorai/tests/ya/generate_assigns_bts1290.i | 2 +-
src/plugins/aorai/tests/ya/hoare_seq.i | 2 +-
src/plugins/aorai/tests/ya/incorrect.i | 2 +-
src/plugins/aorai/tests/ya/loop_bts1050.i | 2 +-
.../tests/ya/metavariables-incompatible.i | 2 +-
.../aorai/tests/ya/metavariables-right.i | 2 +-
.../aorai/tests/ya/metavariables-wrong.i | 2 +-
src/plugins/aorai/tests/ya/monostate.i | 2 +-
src/plugins/aorai/tests/ya/not_prm.i | 2 +-
.../tests/ya/oracle/assigns.0.res.oracle | 1 -
.../tests/ya/oracle/assigns.1.res.oracle | 1 -
.../tests/ya/oracle/assigns.2.res.oracle | 1 -
.../tests/ya/oracle/bts1289.0.res.oracle | 1 -
.../tests/ya/oracle/bts1289.1.res.oracle | 1 -
.../ya/oracle/declared_function.res.oracle | 1 -
.../tests/ya/oracle/deterministic.res.oracle | 1 -
.../aorai/tests/ya/oracle/formals.res.oracle | 1 -
.../generate_assigns_bts1290.res.oracle | 1 -
.../tests/ya/oracle/hoare_seq.res.oracle | 1 -
.../tests/ya/oracle/incorrect.res.oracle | 1 -
.../tests/ya/oracle/loop_bts1050.res.oracle | 1 -
.../metavariables-incompatible.res.oracle | 1 -
.../ya/oracle/metavariables-right.res.oracle | 1 -
.../ya/oracle/metavariables-wrong.res.oracle | 1 -
.../tests/ya/oracle/monostate.res.oracle | 1 -
.../aorai/tests/ya/oracle/not_prm.res.oracle | 1 -
.../aorai/tests/ya/oracle/other.res.oracle | 1 -
.../aorai/tests/ya/oracle/seq.res.oracle | 1 -
.../aorai/tests/ya/oracle/seq_loop.res.oracle | 1 -
.../aorai/tests/ya/oracle/serial.res.oracle | 1 -
.../tests/ya/oracle/single_call.res.oracle | 1 -
.../oracle/singleassignment-right.res.oracle | 1 -
.../oracle/singleassignment-wrong.res.oracle | 1 -
.../aorai/tests/ya/oracle/stack.res.oracle | 1 -
.../ya/oracle/test_acces_params.res.oracle | 1 -
.../ya/oracle/test_acces_params2.res.oracle | 1 -
.../test_boucle_rechercheTableau.res.oracle | 1 -
.../tests/ya/oracle/test_factorial.res.oracle | 1 -
.../ya/oracle/test_recursion4.res.oracle | 1 -
.../ya/oracle/test_recursion5.res.oracle | 1 -
.../tests/ya/oracle/test_struct.res.oracle | 1 -
.../ya/oracle_prove/assigns.0.res.oracle | 1 -
.../ya/oracle_prove/assigns.1.res.oracle | 1 -
.../ya/oracle_prove/assigns.2.res.oracle | 1 -
.../ya/oracle_prove/bts1289.0.res.oracle | 1 -
.../ya/oracle_prove/bts1289.1.res.oracle | 1 -
.../oracle_prove/declared_function.res.oracle | 1 -
.../ya/oracle_prove/deterministic.res.oracle | 1 -
.../tests/ya/oracle_prove/formals.res.oracle | 1 -
.../generate_assigns_bts1290.res.oracle | 1 -
.../ya/oracle_prove/hoare_seq.res.oracle | 1 -
.../ya/oracle_prove/incorrect.res.oracle | 1 -
.../ya/oracle_prove/loop_bts1050.res.oracle | 1 -
.../metavariables-incompatible.res.oracle | 3 +-
.../metavariables-right.res.oracle | 1 -
.../metavariables-wrong.res.oracle | 1 -
.../tests/ya/oracle_prove/not_prm.res.oracle | 1 -
.../tests/ya/oracle_prove/other.res.oracle | 1 -
.../tests/ya/oracle_prove/seq.res.oracle | 1 -
.../tests/ya/oracle_prove/seq_loop.res.oracle | 1 -
.../tests/ya/oracle_prove/serial.res.oracle | 57 +++---
.../ya/oracle_prove/single_call.res.oracle | 1 -
.../singleassignment-right.res.oracle | 1 -
.../singleassignment-wrong.res.oracle | 1 -
.../tests/ya/oracle_prove/stack.res.oracle | 1 -
.../oracle_prove/test_acces_params.res.oracle | 1 -
.../test_acces_params2.res.oracle | 1 -
.../test_boucle_rechercheTableau.res.oracle | 1 -
.../ya/oracle_prove/test_factorial.res.oracle | 1 -
.../oracle_prove/test_recursion4.res.oracle | 1 -
.../oracle_prove/test_recursion5.res.oracle | 1 -
.../ya/oracle_prove/test_struct.res.oracle | 1 -
src/plugins/aorai/tests/ya/other.c | 2 +-
src/plugins/aorai/tests/ya/seq.i | 2 +-
src/plugins/aorai/tests/ya/seq_loop.i | 2 +-
src/plugins/aorai/tests/ya/serial.c | 2 +-
src/plugins/aorai/tests/ya/single_call.i | 2 +-
.../aorai/tests/ya/singleassignment-right.i | 2 +-
.../aorai/tests/ya/singleassignment-wrong.i | 2 +-
src/plugins/aorai/tests/ya/stack.i | 2 +-
.../aorai/tests/ya/test_acces_params.c | 2 +-
.../aorai/tests/ya/test_acces_params2.c | 2 +-
.../tests/ya/test_boucle_rechercheTableau.c | 2 +-
src/plugins/aorai/tests/ya/test_factorial.c | 2 +-
src/plugins/aorai/tests/ya/test_recursion4.c | 2 +-
src/plugins/aorai/tests/ya/test_recursion5.c | 2 +-
src/plugins/aorai/tests/ya/test_struct.c | 2 +-
137 files changed, 213 insertions(+), 361 deletions(-)
diff --git a/.Makefile.lint b/.Makefile.lint
index 4d510d83241..ba3d6165fce 100644
--- a/.Makefile.lint
+++ b/.Makefile.lint
@@ -146,8 +146,6 @@ ML_LINT_KO+=src/libraries/utils/wto.mli
ML_LINT_KO+=src/plugins/aorai/Aorai.mli
ML_LINT_KO+=src/plugins/aorai/aorai_dataflow.ml
ML_LINT_KO+=src/plugins/aorai/aorai_dataflow.mli
-ML_LINT_KO+=src/plugins/aorai/aorai_option.ml
-ML_LINT_KO+=src/plugins/aorai/aorai_register.ml
ML_LINT_KO+=src/plugins/aorai/data_for_aorai.ml
ML_LINT_KO+=src/plugins/aorai/data_for_aorai.mli
ML_LINT_KO+=src/plugins/aorai/logic_simplification.ml
diff --git a/src/plugins/aorai/aorai_option.ml b/src/plugins/aorai/aorai_option.ml
index 2bcf7c8129b..0920c5f83d1 100644
--- a/src/plugins/aorai/aorai_option.ml
+++ b/src/plugins/aorai/aorai_option.ml
@@ -24,95 +24,95 @@
(**************************************************************************)
include Plugin.Register
- (struct
- let name = "aorai"
- let shortname = "aorai"
- let help = "verification of behavioral properties (experimental)"
- end)
+ (struct
+ let name = "aorai"
+ let shortname = "aorai"
+ let help = "verification of behavioral properties (experimental)"
+ end)
module Ltl_File =
Filepath
(struct
- let option_name = "-aorai-ltl"
- let arg_name = ""
- let file_kind = "ltl"
- let existence = Fc_Filepath.Must_exist
- let help = "specifies file name for LTL property"
- end)
+ let option_name = "-aorai-ltl"
+ let arg_name = ""
+ let file_kind = "ltl"
+ let existence = Fc_Filepath.Must_exist
+ let help = "specifies file name for LTL property"
+ end)
module To_Buchi =
Filepath
(struct
- let option_name = "-aorai-to-buchi"
- let arg_name = "f"
- let file_kind = "Promela"
- let existence = Fc_Filepath.Indifferent
- let help =
- "only generates the buchi automata (in Promela language) in file <s>"
- end)
+ let option_name = "-aorai-to-buchi"
+ let arg_name = "f"
+ let file_kind = "Promela"
+ let existence = Fc_Filepath.Indifferent
+ let help =
+ "only generates the buchi automata (in Promela language) in file <s>"
+ end)
module Buchi =
Filepath
(struct
- let option_name = "-aorai-buchi"
- let arg_name = "f"
- let file_kind = "Promela"
- let existence = Fc_Filepath.Must_exist
- let help = "considers the property described by the buchi automata \
- (in Promela language) from file <f>."
- end)
+ let option_name = "-aorai-buchi"
+ let arg_name = "f"
+ let file_kind = "Promela"
+ let existence = Fc_Filepath.Must_exist
+ let help = "considers the property described by the buchi automata \
+ (in Promela language) from file <f>."
+ end)
module Ya =
Filepath
(struct
- let option_name = "-aorai-automata"
- let arg_name = "f"
- let file_kind = "Ya"
- let existence = Fc_Filepath.Must_exist
- let help = "considers the property described by the ya automata \
- (in Ya language) from file <f>."
- end)
+ let option_name = "-aorai-automata"
+ let arg_name = "f"
+ let file_kind = "Ya"
+ let existence = Fc_Filepath.Must_exist
+ let help = "considers the property described by the ya automata \
+ (in Ya language) from file <f>."
+ end)
module Output_C_File =
Filepath
(struct
- let option_name = "-aorai-output-c-file"
- let arg_name = ""
- let file_kind = "annotated C"
- let existence = Fc_Filepath.Indifferent
- let help = "specifies generated file name for annotated C code"
- end)
+ let option_name = "-aorai-output-c-file"
+ let arg_name = ""
+ let file_kind = "annotated C"
+ let existence = Fc_Filepath.Indifferent
+ let help = "specifies generated file name for annotated C code"
+ end)
module Dot =
False(struct
- let option_name = "-aorai-dot"
- let help = "generates a dot file of the Buchi automata"
- end)
+ let option_name = "-aorai-dot"
+ let help = "generates a dot file of the Buchi automata"
+ end)
module DotSeparatedLabels =
False(struct
- let option_name = "-aorai-dot-sep-labels"
- let help = "tells dot to not output guards directly over the edges"
- end)
+ let option_name = "-aorai-dot-sep-labels"
+ let help = "tells dot to not output guards directly over the edges"
+ end)
module AbstractInterpretation =
False(struct
- let option_name = "-aorai-simple-AI"
- let help = "use simple abstract interpretation"
- end)
+ let option_name = "-aorai-simple-AI"
+ let help = "use simple abstract interpretation"
+ end)
module AbstractInterpretationOff =
False(struct
- let option_name = "-aorai-AI-off"
- let help = "does not use abstract interpretation"
- end)
+ let option_name = "-aorai-AI-off"
+ let help = "does not use abstract interpretation"
+ end)
let () = Parameter_customize.set_negative_option_name "-aorai-spec-off"
module Axiomatization =
True(struct
- let option_name = "-aorai-spec-on"
- let help = "if set, does not axiomatize automata"
- end)
+ let option_name = "-aorai-spec-on"
+ let help = "if set, does not axiomatize automata"
+ end)
module GenerateAnnotations =
True
@@ -131,41 +131,34 @@ module GenerateDeterministicLemmas =
module ConsiderAcceptance =
False(struct
- let option_name = "-aorai-acceptance"
- let help = "if set, considers acceptation states"
- end)
+ let option_name = "-aorai-acceptance"
+ let help = "if set, considers acceptation states"
+ end)
let () = Parameter_customize.set_negative_option_name "-aorai-raw-auto"
module AutomataSimplification=
True
(struct
- let option_name = "-aorai-simplified-auto"
- let help = "If set, does not simplify automata"
- end)
-
-module Test =
- Zero(struct
- let option_name = "-aorai-test"
- let arg_name = ""
- let help = "Testing mode (0 = no test)"
- end)
+ let option_name = "-aorai-simplified-auto"
+ let help = "If set, does not simplify automata"
+ end)
module AddingOperationNameAndStatusInSpecification =
False
(struct
let option_name = "-aorai-add-oper"
let help = "Adding current operation name (and statut) in pre/post \
-conditions"
- end)
+ conditions"
+ end)
module Deterministic=
State_builder.Ref
(Datatype.Bool)
(struct
- let name = "Aorai_option.Deterministic"
- let dependencies = []
- let default () = false
- end)
+ let name = "Aorai_option.Deterministic"
+ let dependencies = []
+ let default () = false
+ end)
module InstrumentationHistory =
Int
@@ -187,20 +180,20 @@ let promela_file () =
let advance_abstract_interpretation () =
not (AbstractInterpretationOff.get ()) && not (AbstractInterpretation.get ())
-let emitter =
+let emitter =
Emitter.create
"Aorai"
- [ Emitter.Code_annot; Emitter.Funspec; Emitter.Global_annot ]
+ [ Emitter.Code_annot; Emitter.Funspec; Emitter.Global_annot ]
~correctness:
- [ Ltl_File.parameter; To_Buchi.parameter; Buchi.parameter;
- Ya.parameter; Axiomatization.parameter;
- ConsiderAcceptance.parameter;
- AutomataSimplification.parameter ]
+ [ Ltl_File.parameter; To_Buchi.parameter; Buchi.parameter;
+ Ya.parameter; Axiomatization.parameter;
+ ConsiderAcceptance.parameter;
+ AutomataSimplification.parameter ]
~tuning:
- [ AbstractInterpretation.parameter;
- AddingOperationNameAndStatusInSpecification.parameter;
- InstrumentationHistory.parameter;
- GenerateAnnotations.parameter ]
+ [ AbstractInterpretation.parameter;
+ AddingOperationNameAndStatusInSpecification.parameter;
+ InstrumentationHistory.parameter;
+ GenerateAnnotations.parameter ]
(*
diff --git a/src/plugins/aorai/aorai_option.mli b/src/plugins/aorai/aorai_option.mli
index 79482fd5f3b..4f8c3838eb4 100644
--- a/src/plugins/aorai/aorai_option.mli
+++ b/src/plugins/aorai/aorai_option.mli
@@ -38,7 +38,6 @@ module GenerateAnnotations: Parameter_sig.Bool
module GenerateDeterministicLemmas: Parameter_sig.Bool
module ConsiderAcceptance: Parameter_sig.Bool
module AutomataSimplification: Parameter_sig.Bool
-module Test: Parameter_sig.Int
module AddingOperationNameAndStatusInSpecification: Parameter_sig.Bool
(** [true] if the user declares that its ya automaton is deterministic. *)
diff --git a/src/plugins/aorai/aorai_register.ml b/src/plugins/aorai/aorai_register.ml
index fe4775a424c..d609113165c 100644
--- a/src/plugins/aorai/aorai_register.ml
+++ b/src/plugins/aorai/aorai_register.ml
@@ -33,7 +33,6 @@ let output_c_file = ref Filepath.Normalized.unknown
let ltl_tmp_file = ref Filepath.Normalized.unknown
let ltl_file = ref Filepath.Normalized.unknown
let dot_file = ref Filepath.Normalized.unknown
-let generatesCFile = ref true
let ltl2ba_params = " -l -p -o "
let ltl_to_promela = Hashtbl.create 7
@@ -45,15 +44,15 @@ let set_ltl_correspondence h =
let convert_ltl_exprs t =
let rec convert_cond cond =
match cond with
- POr(c1,c2) -> POr (convert_cond c1, convert_cond c2)
- | PAnd(c1,c2) -> PAnd(convert_cond c1, convert_cond c2)
- | PNot c -> PNot (convert_cond c)
- | PCall _ | PReturn _ | PTrue | PFalse -> cond
- | PRel(Neq,PVar x,PCst _) ->
- (try
- let (rel,t1,t2) = Hashtbl.find ltl_to_promela x in PRel(rel,t1,t2)
- with Not_found -> cond)
- | PRel _ -> cond
+ POr(c1,c2) -> POr (convert_cond c1, convert_cond c2)
+ | PAnd(c1,c2) -> PAnd(convert_cond c1, convert_cond c2)
+ | PNot c -> PNot (convert_cond c)
+ | PCall _ | PReturn _ | PTrue | PFalse -> cond
+ | PRel(Neq,PVar x,PCst _) ->
+ (try
+ let (rel,t1,t2) = Hashtbl.find ltl_to_promela x in PRel(rel,t1,t2)
+ with Not_found -> cond)
+ | PRel _ -> cond
in
let rec convert_seq_elt e =
{ e with
@@ -62,8 +61,8 @@ let convert_ltl_exprs t =
and convert_seq s = List.map convert_seq_elt s in
let convert_parsed c =
match c with
- Seq l -> Seq (convert_seq l)
- | Otherwise -> Otherwise
+ Seq l -> Seq (convert_seq l)
+ | Otherwise -> Otherwise
in
let convert_trans t = { t with cross = convert_parsed t.cross } in
List.map convert_trans t
@@ -117,7 +116,7 @@ let load_ya_file filename =
let channel = check_and_open_in filename "invalid Ya file" in
let lexbuf = Lexing.from_channel channel in
Lexing.(lexbuf.lex_curr_p <-
- { lexbuf.lex_curr_p with pos_fname = (filename :> string) });
+ { lexbuf.lex_curr_p with pos_fname = (filename :> string) });
try
let automata = Yaparser.main Yalexer.token lexbuf in
close_in channel;
@@ -136,7 +135,7 @@ let load_promela_file f =
let trans = convert_ltl_exprs auto.trans in
close_in c;
Data_for_aorai.setAutomata { auto with trans };
- with
+ with
| Promelalexer.Error(loc,msg) -> syntax_error loc msg
let load_promela_file_withexps f =
@@ -145,18 +144,16 @@ let load_promela_file_withexps f =
let automata = Promelalexer_withexps.parse c in
close_in c;
Data_for_aorai.setAutomata automata;
- with
+ with
| Promelalexer_withexps.Error(loc,msg) -> syntax_error loc msg
let display_status () =
if Aorai_option.verbose_atleast 2 then begin
Aorai_option.feedback "\n" ;
Aorai_option.feedback "C file: '%a'\n" Filepath.Normalized.pretty !c_file ;
- Aorai_option.feedback "Entry point: '%a'\n"
+ Aorai_option.feedback "Entry point: '%a'\n"
Kernel_function.pretty (fst (Globals.entry_point())) ;
Aorai_option.feedback "LTL property: '%a'\n" Filepath.Normalized.pretty !ltl_file ;
- Aorai_option.feedback "Files to generate: '%a' (Annotated code)\n"
- (if !generatesCFile then Filepath.Normalized.pretty else (fun fmt _ -> Format.fprintf fmt "(none)")) !output_c_file;
if Aorai_option.Dot.get () then
Aorai_option.feedback "Dot file: '%a'\n" Filepath.Normalized.pretty !dot_file;
Aorai_option.feedback "Tmp files: '%a' (Light LTL file)\n"
@@ -167,15 +164,8 @@ let display_status () =
end
let init_file_names () =
- (* Intermediate functions for error display or fresh name of file
- generation *)
- let err= ref false in
- let dispErr mesg f =
- Aorai_option.error "Error. File '%a' %s.\n" Filepath.Normalized.pretty f mesg;
- err:=true
- in
let freshname ?opt_suf file suf =
- let name = Filepath.Normalized.to_pretty_string file in
+ let name = (file:Filepath.Normalized.t:>string) in
let pre = Filename.remove_extension name in
let pre = match opt_suf with None -> pre | Some s -> pre ^ s in
let rec fn p s n =
@@ -185,30 +175,14 @@ let init_file_names () =
let name =
if not (Sys.file_exists (pre^suf)) then pre^suf
else fn pre suf 0
- in Filepath.Normalized.of_string name
+ in
+ Filepath.Normalized.of_string name
in
-
- (* c_file name is given and has to point out a valid file. *)
- c_file :=
- (match Kernel.Files.get () with
- | [] -> Filepath.Normalized.of_string "dummy.i"
- | f :: _ -> f);
- if (Filepath.Normalized.is_unknown !c_file) then dispErr ": invalid C file name" !c_file;
-
- (* The output C file has to be a valid file name if it is used. *)
- output_c_file := Aorai_option.Output_C_File.get ();
- if (Filepath.Normalized.is_unknown !output_c_file) then
- output_c_file := freshname ~opt_suf:"_annot" !c_file ".c";
- (* else if Sys.file_exists !output_c_file then dispErr "already exists" !output_c_file; *)
-
- if Aorai_option.Dot.get () then
- dot_file:= freshname !c_file ".dot";
-
if Filepath.Normalized.is_unknown (Aorai_option.Ya.get ()) then
if Filepath.Normalized.is_unknown (Aorai_option.Buchi.get ()) then begin
(* ltl_file name is given and has to point out a valid file. *)
ltl_file := Aorai_option.Ltl_File.get ();
-
+ if Aorai_option.Dot.get() then dot_file := freshname !ltl_file ".dot";
(* The LTL file is always used. *)
(* The promela file can be given or not. *)
if not (Filepath.Normalized.is_unknown (Aorai_option.To_Buchi.get ())) then begin
@@ -232,26 +206,25 @@ let init_file_names () =
if not (Filepath.Normalized.is_unknown (Aorai_option.To_Buchi.get ())) &&
not (Filepath.Normalized.is_unknown (Aorai_option.Ltl_File.get ()))
then begin
- Aorai_option.error
+ Aorai_option.abort
"Error. '-buchi' option is incompatible with '-to-buchi' and '-ltl' \
-options.";
- err:=true
+ options."
end;
(* The promela file is used only if the process does not terminate after
- LTL generation. *)
+ LTL generation. *)
promela_file := Aorai_option.promela_file ();
+ if Aorai_option.Dot.get() then
+ dot_file := freshname !promela_file ".dot";
end
else begin
- let ya_file = Aorai_option.Ya.get () in
- if (Filepath.Normalized.is_unknown ya_file) then dispErr ": invalid Ya file name" ya_file;
+ let ya_file = Aorai_option.Ya.get () in
+ if (Filepath.Normalized.is_unknown ya_file) then
+ Aorai_option.abort
+ "invalid Ya file name %a" Filepath.Normalized.pretty ya_file;
+ if Aorai_option.Dot.get() then
+ dot_file := freshname ya_file ".dot"
end;
- display_status ();
- !err
-
-let init_test () =
- match Aorai_option.Test.get () with
- | 1 -> generatesCFile := false;
- | _ -> generatesCFile := true
+ display_status ()
let printverb s = Aorai_option.feedback ~level:2 "%s" s
@@ -263,26 +236,8 @@ let output () =
(!dot_file:>string);
printverb "Generating dot file : done\n"
end;
-
- (* C file *)
- if (not !generatesCFile) then
- printverb "C file generation : skipped\n"
- else
- begin
- let cout = open_out (!output_c_file:>string) in
- let fmt = Format.formatter_of_out_channel cout in
- Kernel.Unicode.without_unicode
- (fun () ->
- File.pretty_ast ~fmt ();
- close_out cout;
- printverb "C file generation : done\n";
- ) ()
- end;
-
- printverb "Finished.\n";
(* Some test traces. *)
- Data_for_aorai.debug_computed_state ();
- if !generatesCFile then Kernel.Files.set [ !output_c_file ]
+ Data_for_aorai.debug_computed_state ()
let work () =
let file = Ast.get () in
@@ -297,15 +252,15 @@ let work () =
Filepath.Normalized.pretty !ltl_tmp_file
Filepath.Normalized.pretty !promela_file
in if Sys.command cmd <> 0 then
- Aorai_option.abort "failed to run: %s" cmd ;
+ Aorai_option.abort "failed to run: %s" cmd ;
printverb "LTL ~> Promela (ltl2ba): done\n"
end;
if not (Filepath.Normalized.is_unknown (Aorai_option.To_Buchi.get ())) then
printverb ("Finished.\nGenerated file: '"^(Filepath.Normalized.to_pretty_string !promela_file)^"'\n")
else
begin
- (* Step 3 : Loading promela_file and checking the consistency between informations from C code and LTL property *)
- (* Such as functions name and global variables. *)
+ (* Step 3 : Loading promela_file and checking the consistency between informations from C code and LTL property *)
+ (* Such as functions name and global variables. *)
if not (Filepath.Normalized.is_unknown (Aorai_option.Buchi.get ())) then
load_promela_file_withexps !promela_file
@@ -314,23 +269,23 @@ let work () =
else
load_promela_file !promela_file;
printverb "Loading promela : done\n";
- (* Computing the list of ignored functions *)
- (* Aorai_visitors.compute_ignored_functions file; *)
+ (* Computing the list of ignored functions *)
+ (* Aorai_visitors.compute_ignored_functions file; *)
- (* Promelaoutput.print_raw_automata (Data_for_aorai.getAutomata()); *)
- (* Data_for_aorai.debug_ltl_expressions (); *)
+ (* Promelaoutput.print_raw_automata (Data_for_aorai.getAutomata()); *)
+ (* Data_for_aorai.debug_ltl_expressions (); *)
(*let _ = Path_analysis.test (Data_for_aorai.getAutomata())in*)
let root = fst (Globals.entry_point ()) in
let axiomatization = Aorai_option.Axiomatization.get() in
if axiomatization then
begin
- (* Step 5 : incrementing pre/post
- conditions with states and transitions information *)
+ (* Step 5 : incrementing pre/post
+ conditions with states and transitions information *)
printverb "Refining pre/post : \n";
Aorai_dataflow.compute ();
- (* Step 6 : Removing transitions never crossed *)
+ (* Step 6 : Removing transitions never crossed *)
let automaton_has_states =
if (Aorai_option.AutomataSimplification.get()) then
begin
@@ -362,19 +317,19 @@ let work () =
end
else
begin
- (* Step 4': Computing the set of possible pre-states and post-states of each function *)
- (* And so for pre/post transitions *)
+ (* Step 4': Computing the set of possible pre-states and post-states of each function *)
+ (* And so for pre/post transitions *)
printverb "Abstracting pre/post : skipped\n";
- (* Step 5': incrementing pre/post conditions with states and transitions information *)
+ (* Step 5': incrementing pre/post conditions with states and transitions information *)
printverb "Refining pre/post : skipped\n";
- (* Step 6 : Removing transitions never crossed *)
+ (* Step 6 : Removing transitions never crossed *)
printverb "Removing unused trans : skipped\n";
- (* Step 7 : Labeling abstract file *)
- (* Finally the information is added into the Cil automata. *)
+ (* Step 7 : Labeling abstract file *)
+ (* Finally the information is added into the Cil automata. *)
Aorai_utils.initGlobals root axiomatization;
Aorai_visitors.add_sync_with_buch file;
printverb "Annotation of Cil : partial\n"
@@ -392,24 +347,16 @@ let work () =
end
let run () =
- Aorai_option.result "Welcome to the Aorai plugin@.";
- init_test ();
-
(* Step 1 : Capture files names *)
- let error_status = init_file_names () in
- (* Treatment is done only if parameters are valid *)
- if error_status then
- Aorai_option.error "Generation stopped."
- else
-
- (* Step 2 : Work in our own project, initialized by a copy of the main
- one. *)
- let work_prj =
- File.create_project_from_visitor "aorai"
- (fun prj -> new Visitor.frama_c_copy prj)
- in
- Project.copy ~selection:(Parameter_state.get_selection ()) work_prj;
- Project.on work_prj work ()
+ init_file_names ();
+ (* Step 2 : Work in our own project, initialized by a copy of the main
+ one. *)
+ let work_prj =
+ File.create_project_from_visitor "aorai"
+ (fun prj -> new Visitor.frama_c_copy prj)
+ in
+ Project.copy ~selection:(Parameter_state.get_selection ()) work_prj;
+ Project.on work_prj work ()
(* Plugin registration *)
@@ -426,9 +373,9 @@ let run, _ =
"Aorai"
(let module O = Aorai_option in
[ O.Ltl_File.self; O.To_Buchi.self; O.Buchi.self;
- O.Ya.self; O.Axiomatization.self; O.ConsiderAcceptance.self;
- O.AutomataSimplification.self; O.AbstractInterpretation.self;
- O.AddingOperationNameAndStatusInSpecification.self ])
+ O.Ya.self; O.Axiomatization.self; O.ConsiderAcceptance.self;
+ O.AutomataSimplification.self; O.AbstractInterpretation.self;
+ O.AddingOperationNameAndStatusInSpecification.self ])
run
let main () = if Aorai_option.is_on () then run ()
diff --git a/src/plugins/aorai/tests/ltl/goto.c b/src/plugins/aorai/tests/ltl/goto.c
index ccd31e28dbe..8cbd56c0842 100644
--- a/src/plugins/aorai/tests/ltl/goto.c
+++ b/src/plugins/aorai/tests/ltl/goto.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
int status=0;
diff --git a/src/plugins/aorai/tests/ltl/oracle/goto.res.oracle b/src/plugins/aorai/tests/ltl/oracle/goto.res.oracle
index e06220b829a..e8fddab9fac 100644
--- a/src/plugins/aorai/tests/ltl/oracle/goto.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/goto.res.oracle
@@ -1,5 +1,4 @@
[kernel] Parsing tests/ltl/goto.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
[aorai] tests/ltl/goto.c:28: Warning:
Call to opc does not follow automaton's specification. This path is assumed to be dead
[kernel] Parsing TMPDIR/aorai_goto_0.i (no preprocessing)
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 7504f14db91..04174d4018a 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_boucle.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_boucle.res.oracle
@@ -1,7 +1,6 @@
[kernel] Parsing tests/ltl/test_boucle.c (with preprocessing)
[kernel:typing:implicit-function-declaration] tests/ltl/test_boucle.c:16: Warning:
Calling undeclared function call_to_an_undefined_function. Old style K&R code?
-[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_test_boucle_0.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_ListOper {
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 810cc3f996f..aed1c6cbbf0 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_boucle1.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_boucle1.res.oracle
@@ -1,5 +1,4 @@
[kernel] Parsing tests/ltl/test_boucle1.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_test_boucle1_0.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_ListOper {
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 bf069fb7cfc..9ab4d87d9cc 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_boucle2.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_boucle2.res.oracle
@@ -1,5 +1,4 @@
[kernel] Parsing tests/ltl/test_boucle2.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_test_boucle2_0.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_ListOper {
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 bbf09f7914a..8b2d1dbb5f2 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_boucle3.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_boucle3.res.oracle
@@ -1,5 +1,4 @@
[kernel] Parsing tests/ltl/test_boucle3.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_test_boucle3_0.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_ListOper {
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 d434d1ddf70..4a0a9031b26 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_factorial.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_factorial.res.oracle
@@ -1,5 +1,4 @@
[kernel] Parsing tests/ltl/test_factorial.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_test_factorial_0.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_ListOper {
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 28c0b50dbab..a377f6f727c 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_recursion1.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_recursion1.res.oracle
@@ -5,7 +5,6 @@
parsing obsolete ACSL construct '\valid_range(addr,min,max)'. '\valid(addr+(min..max))' should be used instead.
[kernel] tests/ltl/test_recursion1.c:54: Warning:
parsing obsolete ACSL construct '\valid_range(addr,min,max)'. '\valid(addr+(min..max))' should be used instead.
-[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_test_recursion1_0.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_ListOper {
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 0c38acfaa75..6dda5c9d85b 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
@@ -1,5 +1,4 @@
[kernel] Parsing tests/ltl/test_recursion2.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_test_recursion2_0.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_ListOper {
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 97d6decf1f8..aabed966d5a 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
@@ -1,5 +1,4 @@
[kernel] Parsing tests/ltl/test_recursion2.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_test_recursion2_1.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_ListOper {
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 b3c85addc01..88e19cf5f59 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_switch2.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_switch2.res.oracle
@@ -1,5 +1,4 @@
[kernel] Parsing tests/ltl/test_switch2.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
[aorai] tests/ltl/test_switch2.c:34: Warning:
Call to opc not conforming to automaton (post-cond). Assuming it is on a dead path
[aorai] tests/ltl/test_switch2.c:23: Warning:
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 4d74ec69aeb..3b0822025db 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_switch3.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_switch3.res.oracle
@@ -1,5 +1,4 @@
[kernel] Parsing tests/ltl/test_switch3.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_test_switch3_0.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_ListOper {
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 96b9dc90c1e..94652a4ad73 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
@@ -1,5 +1,4 @@
[kernel] Parsing tests/ltl/test_switch3_et_recursion.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
[aorai] tests/ltl/test_switch3_et_recursion.c:26: Warning:
Call to countOne does not follow automaton's specification. This path is assumed to be dead
[kernel] Parsing TMPDIR/aorai_test_switch3_et_recursion_0.i (no preprocessing)
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 23495bc09b5..74f48874eb3 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
@@ -1,5 +1,4 @@
[kernel] Parsing tests/ltl/test_switch3_if.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_test_switch3_if_0.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_ListOper {
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 1c04d032f84..e4f973d66d5 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
@@ -1,5 +1,4 @@
[kernel] Parsing tests/ltl/test_switch3_return.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_test_switch3_return_0.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_ListOper {
diff --git a/src/plugins/aorai/tests/ltl/oracle_prove/goto.res.oracle b/src/plugins/aorai/tests/ltl/oracle_prove/goto.res.oracle
index a0b1d8ed006..8e07b35953f 100644
--- a/src/plugins/aorai/tests/ltl/oracle_prove/goto.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle_prove/goto.res.oracle
@@ -1,5 +1,4 @@
[kernel] Parsing tests/ltl/goto.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
[aorai] tests/ltl/goto.c:28: Warning:
Call to opc does not follow automaton's specification. This path is assumed to be dead
[kernel] Parsing TMPDIR/aorai_goto_0.i (no preprocessing)
diff --git a/src/plugins/aorai/tests/ltl/oracle_prove/test_boucle.res.oracle b/src/plugins/aorai/tests/ltl/oracle_prove/test_boucle.res.oracle
index 2d27926df0c..e3d5ec00773 100644
--- a/src/plugins/aorai/tests/ltl/oracle_prove/test_boucle.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle_prove/test_boucle.res.oracle
@@ -1,7 +1,6 @@
[kernel] Parsing tests/ltl/test_boucle.c (with preprocessing)
[kernel:typing:implicit-function-declaration] tests/ltl/test_boucle.c:16: Warning:
Calling undeclared function call_to_an_undefined_function. Old style K&R code?
-[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_test_boucle_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
[kernel:annot:missing-spec] TMPDIR/aorai_test_boucle_0.i:86: Warning:
diff --git a/src/plugins/aorai/tests/ltl/oracle_prove/test_boucle1.res.oracle b/src/plugins/aorai/tests/ltl/oracle_prove/test_boucle1.res.oracle
index 1569a5b398d..c7334dc7d0e 100644
--- a/src/plugins/aorai/tests/ltl/oracle_prove/test_boucle1.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle_prove/test_boucle1.res.oracle
@@ -1,5 +1,4 @@
[kernel] Parsing tests/ltl/test_boucle1.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_test_boucle1_0.i (no preprocessing)
[wp] TMPDIR/aorai_test_boucle1_0.i:3: Warning:
Global invariant not handled yet ('inv_cpt' ignored)
diff --git a/src/plugins/aorai/tests/ltl/oracle_prove/test_boucle2.res.oracle b/src/plugins/aorai/tests/ltl/oracle_prove/test_boucle2.res.oracle
index 6aff87fc8f0..1da39e22bb3 100644
--- a/src/plugins/aorai/tests/ltl/oracle_prove/test_boucle2.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle_prove/test_boucle2.res.oracle
@@ -1,5 +1,4 @@
[kernel] Parsing tests/ltl/test_boucle2.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_test_boucle2_0.i (no preprocessing)
[wp] TMPDIR/aorai_test_boucle2_0.i:4: Warning:
Global invariant not handled yet ('inv' ignored)
diff --git a/src/plugins/aorai/tests/ltl/oracle_prove/test_boucle3.res.oracle b/src/plugins/aorai/tests/ltl/oracle_prove/test_boucle3.res.oracle
index d42c00524da..8f6717a1e31 100644
--- a/src/plugins/aorai/tests/ltl/oracle_prove/test_boucle3.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle_prove/test_boucle3.res.oracle
@@ -1,5 +1,4 @@
[kernel] Parsing tests/ltl/test_boucle3.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_test_boucle3_0.i (no preprocessing)
[wp] TMPDIR/aorai_test_boucle3_0.i:4: Warning:
Global invariant not handled yet ('inv' ignored)
diff --git a/src/plugins/aorai/tests/ltl/oracle_prove/test_factorial.res.oracle b/src/plugins/aorai/tests/ltl/oracle_prove/test_factorial.res.oracle
index 6e1e98b9647..0a52966e046 100644
--- a/src/plugins/aorai/tests/ltl/oracle_prove/test_factorial.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle_prove/test_factorial.res.oracle
@@ -1,4 +1,3 @@
[kernel] Parsing tests/ltl/test_factorial.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_test_factorial_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ltl/oracle_prove/test_recursion1.res.oracle b/src/plugins/aorai/tests/ltl/oracle_prove/test_recursion1.res.oracle
index b41e5fc1a01..b5e9aba20ed 100644
--- a/src/plugins/aorai/tests/ltl/oracle_prove/test_recursion1.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle_prove/test_recursion1.res.oracle
@@ -5,7 +5,6 @@
parsing obsolete ACSL construct '\valid_range(addr,min,max)'. '\valid(addr+(min..max))' should be used instead.
[kernel] tests/ltl/test_recursion1.c:54: Warning:
parsing obsolete ACSL construct '\valid_range(addr,min,max)'. '\valid(addr+(min..max))' should be used instead.
-[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_test_recursion1_0.i (no preprocessing)
[wp] Warning: No definition for 'string_len' interpreted as reads nothing
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ltl/oracle_prove/test_recursion2.0.res.oracle b/src/plugins/aorai/tests/ltl/oracle_prove/test_recursion2.0.res.oracle
index ccdb613ba7d..9891c035100 100644
--- a/src/plugins/aorai/tests/ltl/oracle_prove/test_recursion2.0.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle_prove/test_recursion2.0.res.oracle
@@ -1,5 +1,4 @@
[kernel] Parsing tests/ltl/test_recursion2.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_test_recursion2_0.i (no preprocessing)
[wp] Warning: No definition for 'string_len' interpreted as reads nothing
[wp] Warning: No definition for 'sum_tab' interpreted as reads nothing
diff --git a/src/plugins/aorai/tests/ltl/oracle_prove/test_recursion2.1.res.oracle b/src/plugins/aorai/tests/ltl/oracle_prove/test_recursion2.1.res.oracle
index 8e71caf0deb..904f906300c 100644
--- a/src/plugins/aorai/tests/ltl/oracle_prove/test_recursion2.1.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle_prove/test_recursion2.1.res.oracle
@@ -1,5 +1,4 @@
[kernel] Parsing tests/ltl/test_recursion2.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_test_recursion2_1.i (no preprocessing)
[wp] Warning: No definition for 'string_len' interpreted as reads nothing
[wp] Warning: No definition for 'sum_tab' interpreted as reads nothing
diff --git a/src/plugins/aorai/tests/ltl/oracle_prove/test_switch2.res.oracle b/src/plugins/aorai/tests/ltl/oracle_prove/test_switch2.res.oracle
index 9964a15c39c..5e6c56778cf 100644
--- a/src/plugins/aorai/tests/ltl/oracle_prove/test_switch2.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle_prove/test_switch2.res.oracle
@@ -1,5 +1,4 @@
[kernel] Parsing tests/ltl/test_switch2.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
[aorai] tests/ltl/test_switch2.c:34: Warning:
Call to opc not conforming to automaton (post-cond). Assuming it is on a dead path
[aorai] tests/ltl/test_switch2.c:23: Warning:
diff --git a/src/plugins/aorai/tests/ltl/oracle_prove/test_switch3.res.oracle b/src/plugins/aorai/tests/ltl/oracle_prove/test_switch3.res.oracle
index bfe46c01065..1370ce59a99 100644
--- a/src/plugins/aorai/tests/ltl/oracle_prove/test_switch3.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle_prove/test_switch3.res.oracle
@@ -1,4 +1,3 @@
[kernel] Parsing tests/ltl/test_switch3.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_test_switch3_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ltl/oracle_prove/test_switch3_et_recursion.res.oracle b/src/plugins/aorai/tests/ltl/oracle_prove/test_switch3_et_recursion.res.oracle
index f13072d1a65..0c3127bafe5 100644
--- a/src/plugins/aorai/tests/ltl/oracle_prove/test_switch3_et_recursion.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle_prove/test_switch3_et_recursion.res.oracle
@@ -1,5 +1,4 @@
[kernel] Parsing tests/ltl/test_switch3_et_recursion.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
[aorai] tests/ltl/test_switch3_et_recursion.c:26: Warning:
Call to countOne does not follow automaton's specification. This path is assumed to be dead
[kernel] Parsing TMPDIR/aorai_test_switch3_et_recursion_0.i (no preprocessing)
diff --git a/src/plugins/aorai/tests/ltl/oracle_prove/test_switch3_if.res.oracle b/src/plugins/aorai/tests/ltl/oracle_prove/test_switch3_if.res.oracle
index 68de03d1b30..bf53ddf15ba 100644
--- a/src/plugins/aorai/tests/ltl/oracle_prove/test_switch3_if.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle_prove/test_switch3_if.res.oracle
@@ -1,4 +1,3 @@
[kernel] Parsing tests/ltl/test_switch3_if.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_test_switch3_if_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ltl/oracle_prove/test_switch3_return.res.oracle b/src/plugins/aorai/tests/ltl/oracle_prove/test_switch3_return.res.oracle
index 2bfc5074656..eb8fb8e27b5 100644
--- a/src/plugins/aorai/tests/ltl/oracle_prove/test_switch3_return.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle_prove/test_switch3_return.res.oracle
@@ -1,4 +1,3 @@
[kernel] Parsing tests/ltl/test_switch3_return.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_test_switch3_return_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ltl/test_boucle.c b/src/plugins/aorai/tests/ltl/test_boucle.c
index 72cf5e78ac9..db2f6bc0c3f 100644
--- a/src/plugins/aorai/tests/ltl/test_boucle.c
+++ b/src/plugins/aorai/tests/ltl/test_boucle.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
/*@ requires \true;
diff --git a/src/plugins/aorai/tests/ltl/test_boucle1.c b/src/plugins/aorai/tests/ltl/test_boucle1.c
index 0245ffedcfd..7b091c51b76 100644
--- a/src/plugins/aorai/tests/ltl/test_boucle1.c
+++ b/src/plugins/aorai/tests/ltl/test_boucle1.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
int cpt=3;
diff --git a/src/plugins/aorai/tests/ltl/test_boucle2.c b/src/plugins/aorai/tests/ltl/test_boucle2.c
index 9d4cf3a9aff..8aa77e6f8b0 100644
--- a/src/plugins/aorai/tests/ltl/test_boucle2.c
+++ b/src/plugins/aorai/tests/ltl/test_boucle2.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
int status=0;
diff --git a/src/plugins/aorai/tests/ltl/test_boucle3.c b/src/plugins/aorai/tests/ltl/test_boucle3.c
index 6c93a420264..6da17de07b2 100644
--- a/src/plugins/aorai/tests/ltl/test_boucle3.c
+++ b/src/plugins/aorai/tests/ltl/test_boucle3.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
diff --git a/src/plugins/aorai/tests/ltl/test_factorial.c b/src/plugins/aorai/tests/ltl/test_factorial.c
index 6a429a55e31..0ad64760026 100644
--- a/src/plugins/aorai/tests/ltl/test_factorial.c
+++ b/src/plugins/aorai/tests/ltl/test_factorial.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
diff --git a/src/plugins/aorai/tests/ltl/test_recursion1.c b/src/plugins/aorai/tests/ltl/test_recursion1.c
index ee0968101b1..14be685a47b 100644
--- a/src/plugins/aorai/tests/ltl/test_recursion1.c
+++ b/src/plugins/aorai/tests/ltl/test_recursion1.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
diff --git a/src/plugins/aorai/tests/ltl/test_recursion2.c b/src/plugins/aorai/tests/ltl/test_recursion2.c
index a13c39b9f88..7d93ab3fa3a 100644
--- a/src/plugins/aorai/tests/ltl/test_recursion2.c
+++ b/src/plugins/aorai/tests/ltl/test_recursion2.c
@@ -1,6 +1,6 @@
/* run.config*
- OPT: -aorai-buchi @PTEST_DIR@/@PTEST_NAME@.promela -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
- OPT: -aorai-buchi @PTEST_DIR@/test_recursion3.promela -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-buchi @PTEST_DIR@/@PTEST_NAME@.promela -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-buchi @PTEST_DIR@/test_recursion3.promela -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
/* Calcul de la longueur cumulee des chaines de caracteres prises en parametre */
diff --git a/src/plugins/aorai/tests/ltl/test_switch2.c b/src/plugins/aorai/tests/ltl/test_switch2.c
index f411cec23dc..2bb7284fbbd 100644
--- a/src/plugins/aorai/tests/ltl/test_switch2.c
+++ b/src/plugins/aorai/tests/ltl/test_switch2.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
int status=0;
diff --git a/src/plugins/aorai/tests/ltl/test_switch3.c b/src/plugins/aorai/tests/ltl/test_switch3.c
index 42e5fc6ba9a..5d9e8582f49 100644
--- a/src/plugins/aorai/tests/ltl/test_switch3.c
+++ b/src/plugins/aorai/tests/ltl/test_switch3.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
/* Calcul de la longueur cumulee des chaines de caracteres prises en parametre */
diff --git a/src/plugins/aorai/tests/ltl/test_switch3_et_recursion.c b/src/plugins/aorai/tests/ltl/test_switch3_et_recursion.c
index 00caa9826bb..352725ef984 100644
--- a/src/plugins/aorai/tests/ltl/test_switch3_et_recursion.c
+++ b/src/plugins/aorai/tests/ltl/test_switch3_et_recursion.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
/* Calcul de la longueur cumulee des chaines de caracteres prises en parametre */
diff --git a/src/plugins/aorai/tests/ltl/test_switch3_if.c b/src/plugins/aorai/tests/ltl/test_switch3_if.c
index f6375d4d859..93dd122636e 100644
--- a/src/plugins/aorai/tests/ltl/test_switch3_if.c
+++ b/src/plugins/aorai/tests/ltl/test_switch3_if.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-ltl @PTEST_DIR@/test_switch3.ltl -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-ltl @PTEST_DIR@/test_switch3.ltl -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
/* Calcul de la longueur cumulee des chaines de caracteres prises en parametre */
diff --git a/src/plugins/aorai/tests/ltl/test_switch3_return.c b/src/plugins/aorai/tests/ltl/test_switch3_return.c
index a105540b982..8df70979968 100644
--- a/src/plugins/aorai/tests/ltl/test_switch3_return.c
+++ b/src/plugins/aorai/tests/ltl/test_switch3_return.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-ltl @PTEST_DIR@/test_switch3.ltl -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-ltl @PTEST_DIR@/test_switch3.ltl -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
/* Calcul de la longueur cumulee des chaines de caracteres prises en parametre */
diff --git a/src/plugins/aorai/tests/ya/assigns.c b/src/plugins/aorai/tests/ya/assigns.c
index ce6fe159678..c760aa1537e 100644
--- a/src/plugins/aorai/tests/ya/assigns.c
+++ b/src/plugins/aorai/tests/ya/assigns.c
@@ -1,8 +1,8 @@
/* run.config*
- OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
- OPT: -aorai-automata @PTEST_DIR@/assigns_det.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata @PTEST_DIR@/assigns_det.ya -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
MODULE: @PTEST_DIR@/name_projects.cmxs
- OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -then -print
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -then -print
*/
int X;
diff --git a/src/plugins/aorai/tests/ya/bts1289.i b/src/plugins/aorai/tests/ya/bts1289.i
index 2c6c8f9aa59..93cf50233c6 100644
--- a/src/plugins/aorai/tests/ya/bts1289.i
+++ b/src/plugins/aorai/tests/ya/bts1289.i
@@ -1,6 +1,6 @@
/* run.config*
- OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-test 1 -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
- OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@-2.ya -load-module tests/Aorai_test.cmxs -aorai-test 1 -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@-2.ya -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
void a(void) {}
diff --git a/src/plugins/aorai/tests/ya/declared_function.i b/src/plugins/aorai/tests/ya/declared_function.i
index 53bcdfd71ad..12f50538eb3 100644
--- a/src/plugins/aorai/tests/ya/declared_function.i
+++ b/src/plugins/aorai/tests/ya/declared_function.i
@@ -1,5 +1,5 @@
/* run.config*
-OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
int f(void);
diff --git a/src/plugins/aorai/tests/ya/deterministic.i b/src/plugins/aorai/tests/ya/deterministic.i
index b92271127e2..d892d891378 100644
--- a/src/plugins/aorai/tests/ya/deterministic.i
+++ b/src/plugins/aorai/tests/ya/deterministic.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
int X;
diff --git a/src/plugins/aorai/tests/ya/formals.i b/src/plugins/aorai/tests/ya/formals.i
index 4a32df49b67..a463e4f7d37 100644
--- a/src/plugins/aorai/tests/ya/formals.i
+++ b/src/plugins/aorai/tests/ya/formals.i
@@ -1,5 +1,5 @@
/* run.config*
-OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
int f(int x) { return x; }
diff --git a/src/plugins/aorai/tests/ya/generate_assigns_bts1290.i b/src/plugins/aorai/tests/ya/generate_assigns_bts1290.i
index 2e92796ec06..d9333d415f6 100644
--- a/src/plugins/aorai/tests/ya/generate_assigns_bts1290.i
+++ b/src/plugins/aorai/tests/ya/generate_assigns_bts1290.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-test 1 -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
void main(void)
{
diff --git a/src/plugins/aorai/tests/ya/hoare_seq.i b/src/plugins/aorai/tests/ya/hoare_seq.i
index cc7e1484774..b60ae6082da 100644
--- a/src/plugins/aorai/tests/ya/hoare_seq.i
+++ b/src/plugins/aorai/tests/ya/hoare_seq.i
@@ -1,5 +1,5 @@
/* run.config*
-OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-acceptance -load-module tests/Aorai_test -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
void f(void) { }
diff --git a/src/plugins/aorai/tests/ya/incorrect.i b/src/plugins/aorai/tests/ya/incorrect.i
index fae082d3120..01f70280860 100644
--- a/src/plugins/aorai/tests/ya/incorrect.i
+++ b/src/plugins/aorai/tests/ya/incorrect.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
int f(void);
diff --git a/src/plugins/aorai/tests/ya/loop_bts1050.i b/src/plugins/aorai/tests/ya/loop_bts1050.i
index fdec741b7b3..86fe369e9f7 100644
--- a/src/plugins/aorai/tests/ya/loop_bts1050.i
+++ b/src/plugins/aorai/tests/ya/loop_bts1050.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
void f(){};
diff --git a/src/plugins/aorai/tests/ya/metavariables-incompatible.i b/src/plugins/aorai/tests/ya/metavariables-incompatible.i
index 26744167705..a32cefe9e95 100644
--- a/src/plugins/aorai/tests/ya/metavariables-incompatible.i
+++ b/src/plugins/aorai/tests/ya/metavariables-incompatible.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
void main(void) {}
diff --git a/src/plugins/aorai/tests/ya/metavariables-right.i b/src/plugins/aorai/tests/ya/metavariables-right.i
index cff3994c101..9d88e67323f 100644
--- a/src/plugins/aorai/tests/ya/metavariables-right.i
+++ b/src/plugins/aorai/tests/ya/metavariables-right.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
void f(int x) {}
diff --git a/src/plugins/aorai/tests/ya/metavariables-wrong.i b/src/plugins/aorai/tests/ya/metavariables-wrong.i
index 09ea4b6c4bc..a0542d20021 100644
--- a/src/plugins/aorai/tests/ya/metavariables-wrong.i
+++ b/src/plugins/aorai/tests/ya/metavariables-wrong.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
void f(int x) {}
diff --git a/src/plugins/aorai/tests/ya/monostate.i b/src/plugins/aorai/tests/ya/monostate.i
index 9dade69c092..0d72d9a431c 100644
--- a/src/plugins/aorai/tests/ya/monostate.i
+++ b/src/plugins/aorai/tests/ya/monostate.i
@@ -1,5 +1,5 @@
/* run.config
-OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
void f(void) {}
diff --git a/src/plugins/aorai/tests/ya/not_prm.i b/src/plugins/aorai/tests/ya/not_prm.i
index d96e123d6e6..8b5c4281608 100644
--- a/src/plugins/aorai/tests/ya/not_prm.i
+++ b/src/plugins/aorai/tests/ya/not_prm.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test -main f -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-acceptance -load-module tests/Aorai_test -main f -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
int f(int x) {
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 8c31757f7be..a0d1e8e9805 100644
--- a/src/plugins/aorai/tests/ya/oracle/assigns.0.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/assigns.0.res.oracle
@@ -1,5 +1,4 @@
[kernel] Parsing tests/ya/assigns.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_assigns_0.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_ListOper {
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 cdb19dd2762..067dda49b4d 100644
--- a/src/plugins/aorai/tests/ya/oracle/assigns.1.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/assigns.1.res.oracle
@@ -1,5 +1,4 @@
[kernel] Parsing tests/ya/assigns.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_assigns_1.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_States {
diff --git a/src/plugins/aorai/tests/ya/oracle/assigns.2.res.oracle b/src/plugins/aorai/tests/ya/oracle/assigns.2.res.oracle
index f5a60a3aac1..5a761e8ca86 100644
--- a/src/plugins/aorai/tests/ya/oracle/assigns.2.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/assigns.2.res.oracle
@@ -1,5 +1,4 @@
[kernel] Parsing tests/ya/assigns.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
/* Generated by Frama-C */
int X;
void f(void)
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 d694fc99a03..15f90358d6d 100644
--- a/src/plugins/aorai/tests/ya/oracle/bts1289.0.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/bts1289.0.res.oracle
@@ -1,5 +1,4 @@
[kernel] Parsing tests/ya/bts1289.i (no preprocessing)
-[aorai] Welcome to the Aorai plugin
[aorai] Warning: Call to main does not follow automaton's specification. This path is assumed to be dead
[kernel] Parsing TMPDIR/aorai_bts1289_0.i (no preprocessing)
/* Generated by Frama-C */
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 3c96ba01588..6fb3035c21a 100644
--- a/src/plugins/aorai/tests/ya/oracle/bts1289.1.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/bts1289.1.res.oracle
@@ -1,5 +1,4 @@
[kernel] Parsing tests/ya/bts1289.i (no preprocessing)
-[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_bts1289_1.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_ListOper {
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 162c17c6430..038d8c1a870 100644
--- a/src/plugins/aorai/tests/ya/oracle/declared_function.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/declared_function.res.oracle
@@ -1,5 +1,4 @@
[kernel] Parsing tests/ya/declared_function.i (no preprocessing)
-[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_declared_function_0.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_States {
diff --git a/src/plugins/aorai/tests/ya/oracle/deterministic.res.oracle b/src/plugins/aorai/tests/ya/oracle/deterministic.res.oracle
index 7d3f5aa8877..72d48028936 100644
--- a/src/plugins/aorai/tests/ya/oracle/deterministic.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/deterministic.res.oracle
@@ -1,5 +1,4 @@
[kernel] Parsing tests/ya/deterministic.i (no preprocessing)
-[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_deterministic_0.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_States {
diff --git a/src/plugins/aorai/tests/ya/oracle/formals.res.oracle b/src/plugins/aorai/tests/ya/oracle/formals.res.oracle
index cbe2ba005be..e93f5561f08 100644
--- a/src/plugins/aorai/tests/ya/oracle/formals.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/formals.res.oracle
@@ -1,5 +1,4 @@
[kernel] Parsing tests/ya/formals.i (no preprocessing)
-[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_formals_0.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_States {
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 818442d7618..6dba7900323 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
@@ -1,5 +1,4 @@
[kernel] Parsing tests/ya/generate_assigns_bts1290.i (no preprocessing)
-[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_generate_assigns_bts1290_0.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_ListOper {
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 6095d7964e2..29ffb1ff422 100644
--- a/src/plugins/aorai/tests/ya/oracle/hoare_seq.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/hoare_seq.res.oracle
@@ -1,5 +1,4 @@
[kernel] Parsing tests/ya/hoare_seq.i (no preprocessing)
-[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_hoare_seq_0.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_ListOper {
diff --git a/src/plugins/aorai/tests/ya/oracle/incorrect.res.oracle b/src/plugins/aorai/tests/ya/oracle/incorrect.res.oracle
index 21a5cd9feb5..22596de4c18 100644
--- a/src/plugins/aorai/tests/ya/oracle/incorrect.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/incorrect.res.oracle
@@ -1,5 +1,4 @@
[kernel] Parsing tests/ya/incorrect.i (no preprocessing)
-[aorai] Welcome to the Aorai plugin
[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)
/* Generated by Frama-C */
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 14b24d45cdd..6569b67175a 100644
--- a/src/plugins/aorai/tests/ya/oracle/loop_bts1050.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/loop_bts1050.res.oracle
@@ -1,5 +1,4 @@
[kernel] Parsing tests/ya/loop_bts1050.i (no preprocessing)
-[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_loop_bts1050_0.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_ListOper {
diff --git a/src/plugins/aorai/tests/ya/oracle/metavariables-incompatible.res.oracle b/src/plugins/aorai/tests/ya/oracle/metavariables-incompatible.res.oracle
index 1a257aa76d2..a682bee8a27 100644
--- a/src/plugins/aorai/tests/ya/oracle/metavariables-incompatible.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/metavariables-incompatible.res.oracle
@@ -1,4 +1,3 @@
[kernel] Parsing tests/ya/metavariables-incompatible.i (no preprocessing)
-[aorai] Welcome to the Aorai plugin
[aorai] User Error: The use of metavariables is incompatible with non-deterministic automata, such as automata using extended transitions.
[kernel] Plug-in aorai aborted: invalid user input.
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 e753f6649c4..ee94f69b384 100644
--- a/src/plugins/aorai/tests/ya/oracle/metavariables-right.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/metavariables-right.res.oracle
@@ -1,5 +1,4 @@
[kernel] Parsing tests/ya/metavariables-right.i (no preprocessing)
-[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_metavariables-right_0.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_States {
diff --git a/src/plugins/aorai/tests/ya/oracle/metavariables-wrong.res.oracle b/src/plugins/aorai/tests/ya/oracle/metavariables-wrong.res.oracle
index 44c1487fcf7..7aca51a51b2 100644
--- a/src/plugins/aorai/tests/ya/oracle/metavariables-wrong.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/metavariables-wrong.res.oracle
@@ -1,5 +1,4 @@
[kernel] Parsing tests/ya/metavariables-wrong.i (no preprocessing)
-[aorai] Welcome to the Aorai plugin
[aorai] User Error: The metavariables aorai_x may not be initialized before the transition from e to f_0:
{ (Call(h)) and ((aorai_x) > (0)) }
[kernel] Plug-in aorai aborted: invalid user input.
diff --git a/src/plugins/aorai/tests/ya/oracle/monostate.res.oracle b/src/plugins/aorai/tests/ya/oracle/monostate.res.oracle
index 4b5d328fbbe..984890928fa 100644
--- a/src/plugins/aorai/tests/ya/oracle/monostate.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/monostate.res.oracle
@@ -1,5 +1,4 @@
[kernel] Parsing tests/ya/monostate.i (no preprocessing)
-[aorai] Welcome to the Aorai plugin
[aorai] Warning: Call to main does not follow automaton's specification. This path is assumed to be dead
[aorai] tests/ya/monostate.i:8: Warning:
Call to main not conforming to automaton (pre-cond). Assuming it is on a dead path
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 a1315a44ec9..79d8cc18058 100644
--- a/src/plugins/aorai/tests/ya/oracle/not_prm.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/not_prm.res.oracle
@@ -1,5 +1,4 @@
[kernel] Parsing tests/ya/not_prm.i (no preprocessing)
-[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_not_prm_0.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_ListOper {
diff --git a/src/plugins/aorai/tests/ya/oracle/other.res.oracle b/src/plugins/aorai/tests/ya/oracle/other.res.oracle
index ea8efc3984f..d7146144fdf 100644
--- a/src/plugins/aorai/tests/ya/oracle/other.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/other.res.oracle
@@ -1,5 +1,4 @@
[kernel] Parsing tests/ya/other.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_other_0.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_ListOper {
diff --git a/src/plugins/aorai/tests/ya/oracle/seq.res.oracle b/src/plugins/aorai/tests/ya/oracle/seq.res.oracle
index 8a68e3c2894..92b8136c6f9 100644
--- a/src/plugins/aorai/tests/ya/oracle/seq.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/seq.res.oracle
@@ -1,5 +1,4 @@
[kernel] Parsing tests/ya/seq.i (no preprocessing)
-[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_seq_0.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_ListOper {
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 241908d1ee5..ea66b1d2bf7 100644
--- a/src/plugins/aorai/tests/ya/oracle/seq_loop.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/seq_loop.res.oracle
@@ -1,5 +1,4 @@
[kernel] Parsing tests/ya/seq_loop.i (no preprocessing)
-[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_seq_loop_0.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_ListOper {
diff --git a/src/plugins/aorai/tests/ya/oracle/serial.res.oracle b/src/plugins/aorai/tests/ya/oracle/serial.res.oracle
index 5f1197b44ca..6cc4d3484ec 100644
--- a/src/plugins/aorai/tests/ya/oracle/serial.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/serial.res.oracle
@@ -1,5 +1,4 @@
[kernel] Parsing tests/ya/serial.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
[kernel:annot:missing-spec] tests/ya/serial.c:43: Warning:
Neither code nor specification for function Frama_C_show_aorai_state, generating default assigns from the prototype
[eva] Analyzing a complete application starting at main
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 ea9bdd5f8c4..6264eea6c56 100644
--- a/src/plugins/aorai/tests/ya/oracle/single_call.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/single_call.res.oracle
@@ -1,5 +1,4 @@
[kernel] Parsing tests/ya/single_call.i (no preprocessing)
-[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_single_call_0.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_ListOper {
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 e76ec6fc3ca..311412524b5 100644
--- a/src/plugins/aorai/tests/ya/oracle/singleassignment-right.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/singleassignment-right.res.oracle
@@ -1,5 +1,4 @@
[kernel] Parsing tests/ya/singleassignment-right.i (no preprocessing)
-[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_singleassignment-right_0.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_States {
diff --git a/src/plugins/aorai/tests/ya/oracle/singleassignment-wrong.res.oracle b/src/plugins/aorai/tests/ya/oracle/singleassignment-wrong.res.oracle
index a24943fca98..9eca9305b90 100644
--- a/src/plugins/aorai/tests/ya/oracle/singleassignment-wrong.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/singleassignment-wrong.res.oracle
@@ -1,5 +1,4 @@
[kernel] Parsing tests/ya/singleassignment-wrong.i (no preprocessing)
-[aorai] Welcome to the Aorai plugin
[aorai] User Error: The metavariable aorai_x is assigned several times during the transition from a to b:
{ Call(main) } aorai_x <- x
aorai_x <- aorai_x + 1
diff --git a/src/plugins/aorai/tests/ya/oracle/stack.res.oracle b/src/plugins/aorai/tests/ya/oracle/stack.res.oracle
index b20f875ba14..7bb7948a156 100644
--- a/src/plugins/aorai/tests/ya/oracle/stack.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/stack.res.oracle
@@ -1,5 +1,4 @@
[kernel] Parsing tests/ya/stack.i (no preprocessing)
-[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_stack_0.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_States {
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 960ccd88bee..72d1dbd1b70 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
@@ -1,5 +1,4 @@
[kernel] Parsing tests/ya/test_acces_params.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_test_acces_params_0.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_ListOper {
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 0527f8f7b59..f20db94ee5b 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
@@ -1,5 +1,4 @@
[kernel] Parsing tests/ya/test_acces_params2.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_test_acces_params2_0.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_ListOper {
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 3e9c2f9103d..d9e7db7f803 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
@@ -3,7 +3,6 @@
parsing obsolete ACSL construct '\valid_range(addr,min,max)'. '\valid(addr+(min..max))' should be used instead.
[kernel] tests/ya/test_boucle_rechercheTableau.c:7: Warning:
parsing obsolete ACSL construct '\valid_range(addr,min,max)'. '\valid(addr+(min..max))' should be used instead.
-[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_test_boucle_rechercheTableau_0.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_ListOper {
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 70c686c2f89..ed5f20033ad 100644
--- a/src/plugins/aorai/tests/ya/oracle/test_factorial.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/test_factorial.res.oracle
@@ -1,5 +1,4 @@
[kernel] Parsing tests/ya/test_factorial.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_test_factorial_0.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_ListOper {
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 968521d3ad2..3f9a007d776 100644
--- a/src/plugins/aorai/tests/ya/oracle/test_recursion4.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/test_recursion4.res.oracle
@@ -1,5 +1,4 @@
[kernel] Parsing tests/ya/test_recursion4.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_test_recursion4_0.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_ListOper {
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 1a84302afcd..b3d197570e7 100644
--- a/src/plugins/aorai/tests/ya/oracle/test_recursion5.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/test_recursion5.res.oracle
@@ -3,7 +3,6 @@
parsing obsolete ACSL construct '\valid_range(addr,min,max)'. '\valid(addr+(min..max))' should be used instead.
[kernel] tests/ya/test_recursion5.c:28: Warning:
parsing obsolete ACSL construct '\valid_range(addr,min,max)'. '\valid(addr+(min..max))' should be used instead.
-[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_test_recursion5_0.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_ListOper {
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 e0b06bd1c0f..fa0bb669fc7 100644
--- a/src/plugins/aorai/tests/ya/oracle/test_struct.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/test_struct.res.oracle
@@ -1,5 +1,4 @@
[kernel] Parsing tests/ya/test_struct.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_test_struct_0.i (no preprocessing)
/* Generated by Frama-C */
struct People {
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/assigns.0.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/assigns.0.res.oracle
index 6e42468e3ad..982103df2da 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/assigns.0.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/assigns.0.res.oracle
@@ -1,4 +1,3 @@
[kernel] Parsing tests/ya/assigns.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_assigns_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/assigns.1.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/assigns.1.res.oracle
index bfa57eb1f30..19922b414f8 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/assigns.1.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/assigns.1.res.oracle
@@ -1,4 +1,3 @@
[kernel] Parsing tests/ya/assigns.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_assigns_1.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/assigns.2.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/assigns.2.res.oracle
index f5a60a3aac1..5a761e8ca86 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/assigns.2.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/assigns.2.res.oracle
@@ -1,5 +1,4 @@
[kernel] Parsing tests/ya/assigns.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
/* Generated by Frama-C */
int X;
void f(void)
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/bts1289.0.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/bts1289.0.res.oracle
index 8a21ce6dc7c..9e49047ac77 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/bts1289.0.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/bts1289.0.res.oracle
@@ -1,5 +1,4 @@
[kernel] Parsing tests/ya/bts1289.i (no preprocessing)
-[aorai] Welcome to the Aorai plugin
[aorai] Warning: Call to main does not follow automaton's specification. This path is assumed to be dead
[kernel] Parsing TMPDIR/aorai_bts1289_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/bts1289.1.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/bts1289.1.res.oracle
index 7455ed9f29a..09d835e8740 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/bts1289.1.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/bts1289.1.res.oracle
@@ -1,4 +1,3 @@
[kernel] Parsing tests/ya/bts1289.i (no preprocessing)
-[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_bts1289_1.i (no preprocessing)
[wp] Warning: Missing RTE guards
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 e961cfa00b2..dda7d91ed57 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,4 @@
[kernel] Parsing tests/ya/declared_function.i (no preprocessing)
-[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_declared_function_0.i (no preprocessing)
[kernel:annot:missing-spec] TMPDIR/aorai_declared_function_0.i:48: Warning:
Neither code nor specification for function f, generating default assigns from the prototype
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/deterministic.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/deterministic.res.oracle
index da8094d3368..8b53a748afa 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/deterministic.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/deterministic.res.oracle
@@ -1,4 +1,3 @@
[kernel] Parsing tests/ya/deterministic.i (no preprocessing)
-[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_deterministic_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/formals.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/formals.res.oracle
index 203e6f02f62..fbd3997a5e7 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/formals.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/formals.res.oracle
@@ -1,4 +1,3 @@
[kernel] Parsing tests/ya/formals.i (no preprocessing)
-[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_formals_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/generate_assigns_bts1290.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/generate_assigns_bts1290.res.oracle
index 8c689f78567..55b4a9433c8 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/generate_assigns_bts1290.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/generate_assigns_bts1290.res.oracle
@@ -1,4 +1,3 @@
[kernel] Parsing tests/ya/generate_assigns_bts1290.i (no preprocessing)
-[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_generate_assigns_bts1290_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/hoare_seq.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/hoare_seq.res.oracle
index 25f11ffa4fd..5f917f2df5c 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/hoare_seq.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/hoare_seq.res.oracle
@@ -1,4 +1,3 @@
[kernel] Parsing tests/ya/hoare_seq.i (no preprocessing)
-[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_hoare_seq_0.i (no preprocessing)
[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 16d8f0409c5..b8e7296acf0 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/incorrect.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/incorrect.res.oracle
@@ -1,5 +1,4 @@
[kernel] Parsing tests/ya/incorrect.i (no preprocessing)
-[aorai] Welcome to the Aorai plugin
[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
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/loop_bts1050.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/loop_bts1050.res.oracle
index 8830b5bd606..49b40bd6a11 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/loop_bts1050.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/loop_bts1050.res.oracle
@@ -1,4 +1,3 @@
[kernel] Parsing tests/ya/loop_bts1050.i (no preprocessing)
-[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_loop_bts1050_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/metavariables-incompatible.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/metavariables-incompatible.res.oracle
index 57c2d7eed1c..a682bee8a27 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/metavariables-incompatible.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/metavariables-incompatible.res.oracle
@@ -1,4 +1,3 @@
[kernel] Parsing tests/ya/metavariables-incompatible.i (no preprocessing)
-[aorai] Welcome to the Aorai plugin
-[aorai] User Error: The use of metavariables is incompatible with non-deterministic automata, such as automa using extended transitions.
+[aorai] User Error: The use of metavariables is incompatible with non-deterministic automata, such as automata using extended transitions.
[kernel] Plug-in aorai aborted: invalid user input.
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/metavariables-right.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/metavariables-right.res.oracle
index 6803c149a7b..54e1691625c 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/metavariables-right.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/metavariables-right.res.oracle
@@ -1,4 +1,3 @@
[kernel] Parsing tests/ya/metavariables-right.i (no preprocessing)
-[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_metavariables-right_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/metavariables-wrong.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/metavariables-wrong.res.oracle
index 44c1487fcf7..7aca51a51b2 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/metavariables-wrong.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/metavariables-wrong.res.oracle
@@ -1,5 +1,4 @@
[kernel] Parsing tests/ya/metavariables-wrong.i (no preprocessing)
-[aorai] Welcome to the Aorai plugin
[aorai] User Error: The metavariables aorai_x may not be initialized before the transition from e to f_0:
{ (Call(h)) and ((aorai_x) > (0)) }
[kernel] Plug-in aorai aborted: invalid user input.
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/not_prm.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/not_prm.res.oracle
index fd02e38e18a..9921e92ae87 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/not_prm.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/not_prm.res.oracle
@@ -1,4 +1,3 @@
[kernel] Parsing tests/ya/not_prm.i (no preprocessing)
-[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_not_prm_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/other.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/other.res.oracle
index 470d9d475b7..67ad5163c35 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/other.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/other.res.oracle
@@ -1,4 +1,3 @@
[kernel] Parsing tests/ya/other.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_other_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/seq.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/seq.res.oracle
index 750146c1ae6..7c0f0ef38ef 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/seq.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/seq.res.oracle
@@ -1,4 +1,3 @@
[kernel] Parsing tests/ya/seq.i (no preprocessing)
-[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_seq_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/seq_loop.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/seq_loop.res.oracle
index 37849cdec35..aaa9705b556 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/seq_loop.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/seq_loop.res.oracle
@@ -1,4 +1,3 @@
[kernel] Parsing tests/ya/seq_loop.i (no preprocessing)
-[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_seq_loop_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
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 2572e58edad..cc4a6cd6b2b 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/serial.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/serial.res.oracle
@@ -1,8 +1,5 @@
[kernel] Parsing tests/ya/serial.c (with preprocessing)
-[kernel:typing:implicit-function-declaration] tests/ya/serial.c:81: Warning:
- Calling undeclared function Frama_C_show_aorai_state. Old style K&R code?
-[aorai] Welcome to the Aorai plugin
-[kernel:annot:missing-spec] tests/ya/serial.c:45: Warning:
+[kernel:annot:missing-spec] tests/ya/serial.c:43: Warning:
Neither code nor specification for function Frama_C_show_aorai_state, generating default assigns from the prototype
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
@@ -21,28 +18,36 @@
aorai_StatesHistory_1 ∈ {19}
aorai_StatesHistory_2 ∈ {19}
[eva] using specification for function Frama_C_interval
-[eva] tests/ya/serial.c:47: starting to merge loop iterations
-[eva] tests/ya/serial.c:52: Trace partitioning superposing up to 100 states
-[eva] tests/ya/serial.c:52: Trace partitioning superposing up to 300 states
-[aorai] tests/ya/serial.c:81: Wait1 <- Wait1 <- Complete
-[aorai] tests/ya/serial.c:81: Error <- Error <- Complete
-[aorai] tests/ya/serial.c:81: Complete <- Complete <- Complete
-[aorai] tests/ya/serial.c:81: Wait1 <- Wait1 <- Complete
-[aorai] tests/ya/serial.c:81: Error <- Error <- Complete
-[aorai] tests/ya/serial.c:81: Complete <- Complete <- Complete
-[eva] tests/ya/serial.c:52: Trace partitioning superposing up to 500 states
-[eva:alarm] tests/ya/serial.c:54: Warning:
+[eva] tests/ya/serial.c:45: starting to merge loop iterations
+[eva] tests/ya/serial.c:50: Trace partitioning superposing up to 100 states
+[eva] tests/ya/serial.c:50: Trace partitioning superposing up to 300 states
+[aorai] tests/ya/serial.c:79: Wait1 <- Wait1 <- Complete
+[aorai] tests/ya/serial.c:79: n in {5},x in [0..16383],y in [8192..16383]
+[aorai] tests/ya/serial.c:79: Error <- Error <- Complete
+[aorai] tests/ya/serial.c:79: n in {5},x in [0..16383],y in [8192..16383]
+[aorai] tests/ya/serial.c:79: Complete <- Complete <- Complete
+[aorai] tests/ya/serial.c:79: n in {5},x in [0..16383],y in [8192..16383]
+[aorai] tests/ya/serial.c:79: Wait1 <- Wait1 <- Complete
+[aorai] tests/ya/serial.c:79: n in {5},x in [0..16383],y in [0..8191]
+[aorai] tests/ya/serial.c:79: Error <- Error <- Complete
+[aorai] tests/ya/serial.c:79: n in {5},x in [0..16383],y in [0..8191]
+[aorai] tests/ya/serial.c:79: Complete <- Complete <- Complete
+[aorai] tests/ya/serial.c:79: n in {5},x in [0..16383],y in [0..8191]
+[eva] tests/ya/serial.c:50: Trace partitioning superposing up to 500 states
+[eva:alarm] tests/ya/serial.c:52: Warning:
accessing uninitialized left-value. assert \initialized(&status);
-[eva] tests/ya/serial.c:52: Trace partitioning superposing up to 700 states
-[eva] tests/ya/serial.c:52: Trace partitioning superposing up to 900 states
-[eva] tests/ya/serial.c:52: Trace partitioning superposing up to 1200 states
-[eva] tests/ya/serial.c:52: Trace partitioning superposing up to 1500 states
-[aorai] tests/ya/serial.c:81: Error <- Error <- Error
-[aorai] tests/ya/serial.c:81: Error <- Error <- Error
-[eva] tests/ya/serial.c:52: Trace partitioning superposing up to 1700 states
-[eva] tests/ya/serial.c:52: Trace partitioning superposing up to 1900 states
-[eva] tests/ya/serial.c:52: Trace partitioning superposing up to 2000 states
-[eva] tests/ya/serial.c:52: Trace partitioning superposing up to 2100 states
+[eva] tests/ya/serial.c:50: Trace partitioning superposing up to 700 states
+[eva] tests/ya/serial.c:50: Trace partitioning superposing up to 900 states
+[eva] tests/ya/serial.c:50: Trace partitioning superposing up to 1200 states
+[eva] tests/ya/serial.c:50: Trace partitioning superposing up to 1500 states
+[aorai] tests/ya/serial.c:79: Error <- Error <- Error
+[aorai] tests/ya/serial.c:79: n in {5},x in [0..16383],y in [8192..16383]
+[aorai] tests/ya/serial.c:79: Error <- Error <- Error
+[aorai] tests/ya/serial.c:79: n in {5},x in [0..16383],y in [0..8191]
+[eva] tests/ya/serial.c:50: Trace partitioning superposing up to 1700 states
+[eva] tests/ya/serial.c:50: Trace partitioning superposing up to 1900 states
+[eva] tests/ya/serial.c:50: Trace partitioning superposing up to 2000 states
+[eva] tests/ya/serial.c:50: Trace partitioning superposing up to 2100 states
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function input_data_post_func:
@@ -299,7 +304,7 @@
100% of the logical properties reached have been proven.
----------------------------------------------------------------------------
[kernel] Parsing TMPDIR/aorai_serial_0.i (no preprocessing)
-[kernel:typing:implicit-function-declaration] TMPDIR/aorai_serial_0.i:176: Warning:
+[kernel:typing:implicit-function-declaration] TMPDIR/aorai_serial_0.i:174: Warning:
Calling undeclared function Frama_C_interval. Old style K&R code?
[wp] Warning: Missing RTE guards
[wp] Warning: No goal generated
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/single_call.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/single_call.res.oracle
index dbd60dc8fb5..ecbefc2abff 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/single_call.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/single_call.res.oracle
@@ -1,4 +1,3 @@
[kernel] Parsing tests/ya/single_call.i (no preprocessing)
-[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_single_call_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/singleassignment-right.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/singleassignment-right.res.oracle
index 79c1ae490e6..46c7832cef0 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/singleassignment-right.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/singleassignment-right.res.oracle
@@ -1,4 +1,3 @@
[kernel] Parsing tests/ya/singleassignment-right.i (no preprocessing)
-[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_singleassignment-right_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/singleassignment-wrong.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/singleassignment-wrong.res.oracle
index a24943fca98..9eca9305b90 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/singleassignment-wrong.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/singleassignment-wrong.res.oracle
@@ -1,5 +1,4 @@
[kernel] Parsing tests/ya/singleassignment-wrong.i (no preprocessing)
-[aorai] Welcome to the Aorai plugin
[aorai] User Error: The metavariable aorai_x is assigned several times during the transition from a to b:
{ Call(main) } aorai_x <- x
aorai_x <- aorai_x + 1
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/stack.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/stack.res.oracle
index ad8ddcef2ca..e56f27fc2b9 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/stack.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/stack.res.oracle
@@ -1,4 +1,3 @@
[kernel] Parsing tests/ya/stack.i (no preprocessing)
-[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_stack_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/test_acces_params.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/test_acces_params.res.oracle
index a20fbf3e28d..0bf1b088bf5 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/test_acces_params.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/test_acces_params.res.oracle
@@ -1,5 +1,4 @@
[kernel] Parsing tests/ya/test_acces_params.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_test_acces_params_0.i (no preprocessing)
[wp] TMPDIR/aorai_test_acces_params_0.i:4: Warning:
Global invariant not handled yet ('inv' ignored)
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/test_acces_params2.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/test_acces_params2.res.oracle
index c45f6f03706..82a83a9128b 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/test_acces_params2.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/test_acces_params2.res.oracle
@@ -1,5 +1,4 @@
[kernel] Parsing tests/ya/test_acces_params2.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_test_acces_params2_0.i (no preprocessing)
[wp] TMPDIR/aorai_test_acces_params2_0.i:3: Warning:
Global invariant not handled yet ('inv' ignored)
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/test_boucle_rechercheTableau.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/test_boucle_rechercheTableau.res.oracle
index d3038211509..8cab8fa7b81 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/test_boucle_rechercheTableau.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/test_boucle_rechercheTableau.res.oracle
@@ -3,6 +3,5 @@
parsing obsolete ACSL construct '\valid_range(addr,min,max)'. '\valid(addr+(min..max))' should be used instead.
[kernel] tests/ya/test_boucle_rechercheTableau.c:7: Warning:
parsing obsolete ACSL construct '\valid_range(addr,min,max)'. '\valid(addr+(min..max))' should be used instead.
-[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_test_boucle_rechercheTableau_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/test_factorial.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/test_factorial.res.oracle
index 533a909e627..0a55ec0fe94 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/test_factorial.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/test_factorial.res.oracle
@@ -1,4 +1,3 @@
[kernel] Parsing tests/ya/test_factorial.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_test_factorial_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/test_recursion4.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/test_recursion4.res.oracle
index 5ca3ac392fd..c87a3ebe4e9 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/test_recursion4.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/test_recursion4.res.oracle
@@ -1,4 +1,3 @@
[kernel] Parsing tests/ya/test_recursion4.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_test_recursion4_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/test_recursion5.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/test_recursion5.res.oracle
index 6d11db5117d..2cc98760865 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/test_recursion5.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/test_recursion5.res.oracle
@@ -3,6 +3,5 @@
parsing obsolete ACSL construct '\valid_range(addr,min,max)'. '\valid(addr+(min..max))' should be used instead.
[kernel] tests/ya/test_recursion5.c:28: Warning:
parsing obsolete ACSL construct '\valid_range(addr,min,max)'. '\valid(addr+(min..max))' should be used instead.
-[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_test_recursion5_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/test_struct.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/test_struct.res.oracle
index fe4190800bd..4c72fb29ede 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/test_struct.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/test_struct.res.oracle
@@ -1,4 +1,3 @@
[kernel] Parsing tests/ya/test_struct.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_test_struct_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ya/other.c b/src/plugins/aorai/tests/ya/other.c
index 4e13872dbf2..c4977e2a37d 100644
--- a/src/plugins/aorai/tests/ya/other.c
+++ b/src/plugins/aorai/tests/ya/other.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
int x=0;
diff --git a/src/plugins/aorai/tests/ya/seq.i b/src/plugins/aorai/tests/ya/seq.i
index f573a5491b3..1ba54569e12 100644
--- a/src/plugins/aorai/tests/ya/seq.i
+++ b/src/plugins/aorai/tests/ya/seq.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
void f() { }
diff --git a/src/plugins/aorai/tests/ya/seq_loop.i b/src/plugins/aorai/tests/ya/seq_loop.i
index 07cc7cf2a9b..bee4d37d3cf 100644
--- a/src/plugins/aorai/tests/ya/seq_loop.i
+++ b/src/plugins/aorai/tests/ya/seq_loop.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
void f() {}
diff --git a/src/plugins/aorai/tests/ya/serial.c b/src/plugins/aorai/tests/ya/serial.c
index 43d67d6540f..8e9624c36c4 100644
--- a/src/plugins/aorai/tests/ya/serial.c
+++ b/src/plugins/aorai/tests/ya/serial.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@ -aorai-no-acceptance -aorai-instrumentation-history 2 -aorai-no-generate-annotations -aorai-no-generate-deterministic-lemmas -then-last -eva -eva-partition-value n -eva-ilevel 256
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@ -aorai-no-acceptance -aorai-instrumentation-history 2 -aorai-no-generate-annotations -aorai-no-generate-deterministic-lemmas -then-last -eva -eva-partition-value n -eva-ilevel 256
*/
#include "__fc_builtin.h"
diff --git a/src/plugins/aorai/tests/ya/single_call.i b/src/plugins/aorai/tests/ya/single_call.i
index 257ce2b2c7a..51abf5a7ef3 100644
--- a/src/plugins/aorai/tests/ya/single_call.i
+++ b/src/plugins/aorai/tests/ya/single_call.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
int main () {}
diff --git a/src/plugins/aorai/tests/ya/singleassignment-right.i b/src/plugins/aorai/tests/ya/singleassignment-right.i
index 943c3e5e67c..4c5612f5107 100644
--- a/src/plugins/aorai/tests/ya/singleassignment-right.i
+++ b/src/plugins/aorai/tests/ya/singleassignment-right.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
void main(int *x, int *y)
diff --git a/src/plugins/aorai/tests/ya/singleassignment-wrong.i b/src/plugins/aorai/tests/ya/singleassignment-wrong.i
index c983ce03e45..4a88230c1c7 100644
--- a/src/plugins/aorai/tests/ya/singleassignment-wrong.i
+++ b/src/plugins/aorai/tests/ya/singleassignment-wrong.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
int main(int x)
diff --git a/src/plugins/aorai/tests/ya/stack.i b/src/plugins/aorai/tests/ya/stack.i
index b3a73417829..d911301c686 100644
--- a/src/plugins/aorai/tests/ya/stack.i
+++ b/src/plugins/aorai/tests/ya/stack.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
diff --git a/src/plugins/aorai/tests/ya/test_acces_params.c b/src/plugins/aorai/tests/ya/test_acces_params.c
index 884140ce9ca..dc673f9bc59 100644
--- a/src/plugins/aorai/tests/ya/test_acces_params.c
+++ b/src/plugins/aorai/tests/ya/test_acces_params.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
int status=0;
diff --git a/src/plugins/aorai/tests/ya/test_acces_params2.c b/src/plugins/aorai/tests/ya/test_acces_params2.c
index 86092179e3f..7f25f23facb 100644
--- a/src/plugins/aorai/tests/ya/test_acces_params2.c
+++ b/src/plugins/aorai/tests/ya/test_acces_params2.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
diff --git a/src/plugins/aorai/tests/ya/test_boucle_rechercheTableau.c b/src/plugins/aorai/tests/ya/test_boucle_rechercheTableau.c
index 7dcf436cfe3..da220198440 100644
--- a/src/plugins/aorai/tests/ya/test_boucle_rechercheTableau.c
+++ b/src/plugins/aorai/tests/ya/test_boucle_rechercheTableau.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
diff --git a/src/plugins/aorai/tests/ya/test_factorial.c b/src/plugins/aorai/tests/ya/test_factorial.c
index 9cb2213b68d..fbb9762854c 100644
--- a/src/plugins/aorai/tests/ya/test_factorial.c
+++ b/src/plugins/aorai/tests/ya/test_factorial.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
diff --git a/src/plugins/aorai/tests/ya/test_recursion4.c b/src/plugins/aorai/tests/ya/test_recursion4.c
index cf4c5d8523a..e88b8471fb7 100644
--- a/src/plugins/aorai/tests/ya/test_recursion4.c
+++ b/src/plugins/aorai/tests/ya/test_recursion4.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
# pragma JessieIntegerModel(math)
diff --git a/src/plugins/aorai/tests/ya/test_recursion5.c b/src/plugins/aorai/tests/ya/test_recursion5.c
index 241030e7112..0f902c0071f 100644
--- a/src/plugins/aorai/tests/ya/test_recursion5.c
+++ b/src/plugins/aorai/tests/ya/test_recursion5.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
diff --git a/src/plugins/aorai/tests/ya/test_struct.c b/src/plugins/aorai/tests/ya/test_struct.c
index 1b8ff3ec2ff..d94c75970eb 100644
--- a/src/plugins/aorai/tests/ya/test_struct.c
+++ b/src/plugins/aorai/tests/ya/test_struct.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
struct People{
--
GitLab