diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 4bc7199b1bedb2b59684124bda7553ac9e29bffc..d340e7572f66efab588f1b5fe54c89c27c123302 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -636,14 +636,14 @@ let process_pragmas_pack_align_field_attributes fi fattrs cattr =
match !current_packing_pragma, align_pragma_for_struct fi.forig_name with
| None, None -> check_aligned fattrs
| Some n, apragma ->
- warn_incompatible_pragmas_attributes apragma (fattrs <> []);
+ warn_incompatible_pragmas_attributes apragma (fattrs <> []);
let field_align = combine_aligned_attributes fattrs in
(* If this field has no valid aligned attributes and the composite type
has a packed attribute, nothing needs to be done: the composite will
have the "packed" attribute anyway. *)
if field_align = None && Cil.hasAttribute "packed" cattr then
dropAttribute "aligned" fattrs
- else
+ else
(* Otherwise, align on min(n, max(field alignment, type alignment)):
the field alignment attribute (if there is one) may be smaller than
its type alignment, so we get the maximum of both. Then, we apply
@@ -652,9 +652,9 @@ let process_pragmas_pack_align_field_attributes fi fattrs cattr =
let type_align = Integer.of_int (Cil.bytesAlignOf fi.ftype) in
let existing_align =
Option.fold field_align ~none:type_align ~some:(Integer.max type_align)
- in
+ in
let new_align = Integer.min n existing_align in
- Kernel.feedback ~dkey:Kernel.dkey_typing_pragma ~current:true
+ Kernel.feedback ~dkey:Kernel.dkey_typing_pragma ~current:true
"%s aligned(%a) attribute to field '%s.%s' due to packing pragma"
(if Option.is_none field_align then "adding" else "setting")
Integer.pretty new_align fi.fcomp.cname fi.fname;
@@ -2739,7 +2739,7 @@ let makeGlobalVarinfo (isadef: bool) (vi: varinfo) : varinfo * bool =
prototypes. Logic specifications refer to the varinfo in this table. *)
begin
match vi.vtype with
- | TFun (_,Some formals , _, _ ) ->
+ | TFun (_,Some formals , _, _) ->
(try
let old_formals_env = getFormalsDecl oldvi in
List.iter2
@@ -2760,7 +2760,7 @@ let makeGlobalVarinfo (isadef: bool) (vi: varinfo) : varinfo * bool =
old.vattr <- attr;
end;
match old.vlogic_var_assoc with
- | None -> ()
+ | None -> ()
| Some old_lv -> old_lv.lv_name <- name
end)
old_formals_env
@@ -4815,7 +4815,7 @@ and doType (ghost:bool) (context: type_context)
else begin
match context with
| `FieldDecl ->
- Kernel.error ~once:true ~current:true
+ Kernel.error ~once:true ~current:true
"\"Variable length array in structure\" extension \
is not supported"
| `GlobalDecl ->
@@ -6483,7 +6483,7 @@ and doExp local_env
*)
if not isSpecialBuiltin && not are_ghost then begin
warn_no_proto f;
- let typ = TFun (resType, Some [], false, attrs) in
+ let typ = TFun (resType, Some [], false,attrs) in
Cil.update_var_type f typ;
end
| None, _ (* TODO: treat function pointers. *)
@@ -7957,19 +7957,19 @@ and doInitializer loc local_env (vi: varinfo) (inite: Cabs.init_expression)
let checkArrayInit ty init =
let init_ok =
- if Cil.isArrayType ty then
- match init with
+ if Cil.isArrayType ty then
+ match init with
| COMPOUND_INIT _ -> true
| SINGLE_INIT e ->
(match stripParen e with
- { expr_node =
+ { expr_node =
CONSTANT (CONST_STRING _ | CONST_WSTRING _)} -> true
| _ -> false)
| _ -> false
else true
in
if not init_ok then
- Kernel.error ~current:true ~once:true
+ Kernel.error ~current:true ~once:true
"Array initializer must be an initializer list or string literal";
in
Kernel.debug ~dkey:Kernel.dkey_typing_init
@@ -8655,15 +8655,15 @@ and createGlobal loc ghost logic_spec ((t,s,b,attr_list) : (typ * storage * bool
let<> UpdatedCurrentLoc = loc in
let loc = Current_loc.get () in
let res =
- try
- (* it can not have old behavior names, since this is the
- first time we see the declaration.
- *)
- Ltyping.funspec [] vi None vi.vtype spec
- with LogicTypeError ((source,_),msg) ->
- Kernel.warning ~wkey:Kernel.wkey_annot_error ~source
- "%s. Ignoring specification of function %s" msg vi.vname;
- empty_funspec ()
+ try
+ (* it can not have old behavior names, since this is the
+ first time we see the declaration.
+ *)
+ Ltyping.funspec [] vi None vi.vtype spec
+ with LogicTypeError ((source,_),msg) ->
+ Kernel.warning ~wkey:Kernel.wkey_annot_error ~source
+ "%s. Ignoring specification of function %s" msg vi.vname;
+ empty_funspec ()
in
res, loc
end
@@ -9608,14 +9608,15 @@ and doDecl local_env (isglobal: bool) (def: Cabs.definition) : chunk =
dl;
empty
- | Cabs.GLOBANNOT (decl) when isglobal ->
- begin
+ | Cabs.GLOBANNOT decls when isglobal ->
List.iter
(fun decl ->
let loc = convLoc decl.Logic_ptree.decl_loc in
let<> UpdatedCurrentLoc = loc in
try
- let tdecl = Ltyping.annot decl in
+ match Ltyping.annot decl with
+ | None -> ()
+ | Some tdecl ->
let attr = fc_stdlib_attribute [] in
let tdecl =
List.fold_left
@@ -9627,8 +9628,7 @@ and doDecl local_env (isglobal: bool) (def: Cabs.definition) : chunk =
~wkey:Kernel.wkey_annot_error ~source
"%s. Ignoring global annotation" msg
)
- decl;
- end;
+ decls;
empty
| Cabs.GLOBANNOT _ | Cabs.PRAGMA _ | Cabs.GLOBASM _ | Cabs.FUNDEF _ ->
@@ -10420,9 +10420,3 @@ let convFile (path, f) =
(* export function without internal `relaxed' argument. *)
let areCompatibleTypes t1 t2 = areCompatibleTypes t1 t2
-
-(*
-Local Variables:
-compile-command: "make -C ../../.."
-End:
-*)
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index ee1ddf4eb651b814e849e2eb0094bf57edb4f5f8..6cc728e2ea9a3ffad42af30bc56c8d33af56ca6e 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -661,7 +661,7 @@ sig
Cil_types.logic_type -> Logic_ptree.code_annot -> code_annotation
val type_annot : location -> Logic_ptree.type_annot -> logic_info
val model_annot : location -> Logic_ptree.model_annot -> model_info
- val annot : Logic_ptree.decl -> global_annotation
+ val annot : Logic_ptree.decl -> global_annotation option
val funspec :
string list ->
varinfo -> (varinfo list) option -> typ -> Logic_ptree.spec -> funspec
@@ -4066,11 +4066,12 @@ struct
| TDsum cons -> LTsum (List.map (type_datacons loc env my_info) cons)
| TDsyn typ -> LTsyn (plain_logic_type loc env typ)
- let rec annot in_axiomatic a =
+ let rec decl in_axiomatic a =
let open Current_loc.Operators in
let loc = a.decl_loc in
let<> UpdatedCurrentLoc = loc in
match a.decl_node with
+
| LDlogic_reads (f, labels, poly, t, p, l) ->
let env,info = logic_decl loc f labels poly ~return_type:t p in
info.l_body <-
@@ -4085,7 +4086,8 @@ struct
| None -> LBnone);
(* potential creation of label w.r.t. reads clause *)
update_info_wrt_default_label info;
- Dfun_or_pred (info,loc)
+ Some (Dfun_or_pred (info,loc))
+
| LDpredicate_reads (f, labels, poly, p, l) ->
let env,info = logic_decl loc f labels poly p in
info.l_body <-
@@ -4100,7 +4102,8 @@ struct
| None -> LBnone);
(* potential creation of label w.r.t. reads clause *)
update_info_wrt_default_label info;
- Dfun_or_pred (info,loc)
+ Some (Dfun_or_pred (info,loc))
+
| LDlogic_def(f, labels, poly,t,p,e) ->
let env,info = logic_decl loc f labels poly ~return_type:t p in
let rt = match info.l_type with
@@ -4114,20 +4117,21 @@ struct
info.l_body <- LBterm (update_term_wrt_default_label new_term);
(* potential creation of label w.r.t. def *)
update_info_wrt_default_label info;
- Dfun_or_pred (info,loc)
+ Some (Dfun_or_pred (info,loc))
end else
C.error loc
- "return type of logic function %s is %a but %a was expected"
- f
+ "return type of logic function %s is %a but %a was expected" f
Cil_printer.pp_logic_type new_typ
Cil_printer.pp_logic_type rt
+
| LDpredicate_def (f, labels, poly, p, e) ->
let env,info = logic_decl loc f labels poly p in
let e = update_predicate_wrt_default_label (predicate env e) in
info.l_body <- LBpred e;
(* potential creation of label w.r.t. def *)
update_info_wrt_default_label info;
- Dfun_or_pred (info,loc)
+ Some (Dfun_or_pred (info,loc))
+
| LDinductive_def (f, input_labels, poly, p, indcases) ->
let _env,info = logic_decl loc f input_labels poly p in
(* env is ignored: because params names are indeed useless...*)
@@ -4154,28 +4158,26 @@ struct
Update the inductive cases that need it (i.e. do not define
their own label(s)).
*)
- let l =
- List.rev_map update_ind_case_wrt_default_label l
- in
+ let l = List.rev_map update_ind_case_wrt_default_label l in
info.l_body <- LBinductive l;
update_info_wrt_default_label info;
- Dfun_or_pred (info,loc)
+ Some (Dfun_or_pred (info,loc))
+
| LDaxiomatic(id,decls) ->
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 begin
+ C.error loc "Nested axiomatic. Ignoring body of %s" id ;
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
+ id Cil_printer.pp_location oldloc in
+ let l = List.filter_map (decl true) decls in
ignore (Logic_env.Axiomatics.memo ~change (fun _ -> loc) id);
- Daxiomatic(id,l,[],loc)
- end
+ Some (Daxiomatic(id,l,[],loc))
+
| LDmodule _ -> C.error loc "Unsupported module declaration"
| LDimport _ -> C.error loc "Unsupported module import"
+
| LDtype(s,l,def) ->
let env = init_type_variables loc l in
let my_info =
@@ -4183,14 +4185,14 @@ struct
lt_params = l;
lt_def = None; (* will be updated later *)
lt_attr = [];
- }
- in
+ } in
add_logic_type loc my_info;
let tdef = Option.map (typedef loc env my_info) def in
if is_cyclic_typedef s tdef then
C.error loc "Definition of %s is cyclic" s;
my_info.lt_def <- tdef;
- Dtype (my_info,loc)
+ Some (Dtype (my_info,loc))
+
| LDlemma (x,labels, poly, {tp_kind = kind; tp_statement = e}) ->
if Logic_env.Lemmas.mem x then begin
let old_def = Logic_env.Lemmas.find x in
@@ -4211,7 +4213,8 @@ struct
in
let def = Dlemma (x,labels, poly, p, [], loc) in
Logic_env.Lemmas.add x def;
- def
+ Some def
+
| LDinvariant (s, e) ->
let labels,env = annot_env loc [] [] in
let li = Cil_const.make_logic_info s in
@@ -4224,11 +4227,11 @@ struct
li.l_body <- LBpred p;
add_logic_function loc li;
update_info_wrt_default_label li;
- Dinvariant (li,loc)
- | LDtype_annot l ->
- Dtype_annot (type_annot loc l,loc)
- | LDmodel_annot l ->
- Dmodel_annot (model_annot loc l,loc);
+ Some (Dinvariant (li,loc))
+
+ | LDtype_annot l -> Some (Dtype_annot (type_annot loc l,loc))
+ | LDmodel_annot l -> Some (Dmodel_annot (model_annot loc l,loc))
+
| LDvolatile (tsets, (rd_opt, wr_opt)) ->
let env = keep_qualifiers (Lenv.empty ()) in
let ctxt = base_ctxt env in
@@ -4316,25 +4319,27 @@ struct
let tsets = List.map (Logic_const.new_identified_term) tsets in
let rvi_opt = get_volatile_fct checks_reads_fct rd_opt in
let wvi_opt = get_volatile_fct checks_writes_fct wr_opt in
- Dvolatile (tsets, rvi_opt, wvi_opt, [], loc)
+ Some (Dvolatile (tsets, rvi_opt, wvi_opt, [], loc))
+
| LDextended (Ext_lexpr(kind, content)) ->
let typing_context = base_ctxt (Lenv.empty ()) in
let status,tcontent = Extensions.typer kind ~typing_context ~loc content in
let textended = Logic_const.new_acsl_extension kind loc status tcontent in
- Dextended (textended, [], loc)
+ Some (Dextended (textended, [], loc))
+
| LDextended (Ext_extension (kind, name, content)) ->
let typing_context = base_ctxt (Lenv.empty ()) in
let status,tcontent =
Extensions.typer_block kind ~typing_context ~loc (name,content)
in
let textended = Logic_const.new_acsl_extension kind loc status tcontent in
- Dextended (textended, [], loc)
+ Some (Dextended (textended, [], loc))
- let annot a =
+ let annot = C.on_error
+ (fun a ->
start_transaction ();
- let res = annot false a in
- finish_transaction (); res
-
- let annot = C.on_error annot (fun _ -> rollback_transaction ())
+ let res = decl false a in
+ finish_transaction (); res)
+ (fun _ -> rollback_transaction ())
end
diff --git a/src/kernel_services/ast_queries/logic_typing.mli b/src/kernel_services/ast_queries/logic_typing.mli
index 8d44d679d4d7d06078a8683078b140ff981ce1a6..a8393a7e53ec9749c0ba4525891122b4abed77a8 100644
--- a/src/kernel_services/ast_queries/logic_typing.mli
+++ b/src/kernel_services/ast_queries/logic_typing.mli
@@ -202,7 +202,7 @@ sig
val model_annot :
location -> Logic_ptree.model_annot -> model_info
- val annot : Logic_ptree.decl -> global_annotation
+ val annot : Logic_ptree.decl -> global_annotation option
(** [funspec behaviors f prms typ spec] type-checks a function contract.
@param behaviors list of existing behaviors (outside of the current