diff --git a/src/kernel_services/ast_queries/logic_env.ml b/src/kernel_services/ast_queries/logic_env.ml index 18381986562fe7c5de69f1f331691a93e229792b..fe1d9504c6a7956e5e1d269a7fb53ddb91191aea 100644 --- a/src/kernel_services/ast_queries/logic_env.ml +++ b/src/kernel_services/ast_queries/logic_env.ml @@ -146,6 +146,14 @@ module Lemmas = let size = 17 end) +module Axiomatics = + State_builder.Hashtbl(Datatype.String.Hashtbl)(Cil_datatype.Location) + (struct + let name = "Logic_env.Axiomatics" + let dependencies = [] + let size = 17 + end) + module Model_info = State_builder.Hashtbl (Datatype.String.Hashtbl) @@ -164,6 +172,7 @@ let init_dependencies from = Logic_type_info.self; Logic_ctor_info.self; Lemmas.self; + Axiomatics.self; Model_info.self; ] @@ -330,6 +339,7 @@ let prepare_tables () = Logic_type_info.clear (); Logic_info.clear (); Lemmas.clear (); + Axiomatics.clear(); Model_info.clear (); Logic_type_builtin.iter Logic_type_info.add; Logic_ctor_builtin.iter Logic_ctor_info.add; diff --git a/src/kernel_services/ast_queries/logic_env.mli b/src/kernel_services/ast_queries/logic_env.mli index 954eb3645d1e73961b39b7cb1e0c11a9ab2cb0ff..e3fcee6b3b750e8bce3929a37f690c21a3f17469 100644 --- a/src/kernel_services/ast_queries/logic_env.mli +++ b/src/kernel_services/ast_queries/logic_env.mli @@ -57,6 +57,10 @@ module Model_info: State_builder.Hashtbl module Lemmas: State_builder.Hashtbl with type key = string and type data = Cil_types.global_annotation +(** @since Frama-C+dev *) +module Axiomatics: State_builder.Hashtbl + with type key = string and type data = Cil_types.location + val builtin_states: State.t list (** {2 Shortcuts to the functions of the modules above} *) diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml index 9cc3ddbd61863c0bf1cc3354dbc8222987f1217d..4785bb01b5423f62615d1d30673151866b67ac28 100644 --- a/src/kernel_services/ast_queries/logic_typing.ml +++ b/src/kernel_services/ast_queries/logic_typing.ml @@ -4163,9 +4163,16 @@ struct if in_axiomatic then (* Not supported yet. See issue 43 on ACSL's github repository. *) C.error loc "Nested axiomatic. Ignoring body of %s" id - else + else begin + let change oldloc = + C.error loc + "Duplicated axiomatics %s (first occurrence at %a)" + id Cil_printer.pp_location oldloc + in let l = List.map (annot true) decls in + ignore (Logic_env.Axiomatics.memo ~change (fun _ -> loc) id); Daxiomatic(id,l,[],loc) + end | LDtype(s,l,def) -> let env = init_type_variables loc l in let my_info = diff --git a/tests/spec/axiomatic_same_name.c b/tests/spec/axiomatic_same_name.c new file mode 100644 index 0000000000000000000000000000000000000000..5572552a84b2f967471e3b7b8f73f75766836261 --- /dev/null +++ b/tests/spec/axiomatic_same_name.c @@ -0,0 +1,13 @@ +/* run.config* +STDOPT: +"-kernel-warn-key annot-error:active" +*/ + +/*@ axiomatic A { +lemma foo: \true; +} +*/ + +/*@ axiomatic A { // should be rejected: Axiomatic A already exists +lemma bar: \true; +} +*/ diff --git a/tests/spec/oracle/axiomatic_same_name.res.oracle b/tests/spec/oracle/axiomatic_same_name.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..8628ef4033e626c185fdaaf1257a9cb8c7f3074f --- /dev/null +++ b/tests/spec/oracle/axiomatic_same_name.res.oracle @@ -0,0 +1,11 @@ +[kernel] Warning: Unknown warning key annot-error:active +[kernel] Parsing tests/spec/axiomatic_same_name.c (with preprocessing) +[kernel:annot-error] tests/spec/axiomatic_same_name.c:10: Warning: + Duplicated axiomatics A (first occurrence at tests/spec/axiomatic_same_name.c:5). Ignoring global annotation +/* Generated by Frama-C */ +/*@ axiomatic A { + lemma foo: \true; + + } + */ +