diff --git a/.Makefile.lint b/.Makefile.lint
index c2648ca66aafcbf1311b68871dfb983d47a9fbd4..80fb691a8370490eea2a7db9b60c1fae64ab498a 100644
--- a/.Makefile.lint
+++ b/.Makefile.lint
@@ -52,7 +52,6 @@ ML_LINT_KO+=src/kernel_services/analysis/dataflow2.mli
ML_LINT_KO+=src/kernel_services/analysis/dataflows.ml
ML_LINT_KO+=src/kernel_services/analysis/dataflows.mli
ML_LINT_KO+=src/kernel_services/analysis/dominators.ml
-ML_LINT_KO+=src/kernel_services/analysis/exn_flow.ml
ML_LINT_KO+=src/kernel_services/analysis/interpreted_automata.ml
ML_LINT_KO+=src/kernel_services/analysis/interpreted_automata.mli
ML_LINT_KO+=src/kernel_services/analysis/logic_interp.ml
diff --git a/src/kernel_internals/typing/allocates.ml b/src/kernel_internals/typing/allocates.ml
index 7b732f4edf83cefc6aa9e672b86c541c014648b6..21d04239663de36f3e20c3b6e81bc6a4e9a292be 100644
--- a/src/kernel_internals/typing/allocates.ml
+++ b/src/kernel_internals/typing/allocates.ml
@@ -35,7 +35,7 @@ let add_allocates_loop stmt =
let all_default = Annotations.fold_code_annot all_default stmt true in
if all_default then
let ca = AAllocation ([], FreeAlloc ([], [])) in
- Annotations.add_code_annot Emitter.kernel stmt
+ Annotations.add_code_annot ~keep_empty:false Emitter.kernel stmt
(Logic_const.new_code_annotation ca)
let add_allocates_nothing_funspec kf =
diff --git a/src/kernel_internals/typing/asm_contracts.ml b/src/kernel_internals/typing/asm_contracts.ml
index d87771d648f135516e46dbb69a3eb2c97856afb8..b61d0d1c2b343fee034e3bf7e7c162d7affd86e3 100644
--- a/src/kernel_internals/typing/asm_contracts.ml
+++ b/src/kernel_internals/typing/asm_contracts.ml
@@ -184,7 +184,7 @@ class visit_assembly =
let ca =
Logic_const.new_code_annotation (AStmtSpec ([],spec))
in
- Annotations.add_code_annot emitter ~kf stmt ca;
+ Annotations.add_code_annot ~keep_empty:false emitter ~kf stmt ca;
if not mem_clobbered && Kernel.AsmContractsAutoValidate.get()
then begin
let active = [] in
diff --git a/src/kernel_services/analysis/exn_flow.ml b/src/kernel_services/analysis/exn_flow.ml
index a75151352f640348731a343532d6cfa4da1a5646..f31a727c80275794f9265fc86312e1fd673e7dbf 100644
--- a/src/kernel_services/analysis/exn_flow.ml
+++ b/src/kernel_services/analysis/exn_flow.ml
@@ -23,20 +23,20 @@
open Cil
open Cil_types
-(* all exceptions that can be raised somewhere in the AST.
+(* all exceptions that can be raised somewhere in the AST.
Used to handle function pointers without exn specification
- *)
+*)
module All_exn =
State_builder.Option_ref(Cil_datatype.Typ.Set)
(struct let name = "Exn_flow.All_exn" let dependencies = [Ast.self] end)
-
+
module Exns =
State_builder.Hashtbl(Kernel_function.Hashtbl)(Cil_datatype.Typ.Set)
(struct
- let name = "Exn_flow.Exns"
- let dependencies = [Ast.self; All_exn.self]
- let size = 47
- end)
+ let name = "Exn_flow.Exns"
+ let dependencies = [Ast.self; All_exn.self]
+ let size = 47
+ end)
module ExnsStmt =
State_builder.Hashtbl(Cil_datatype.Stmt.Hashtbl)(Cil_datatype.Typ.Set)
@@ -61,10 +61,10 @@ class all_exn =
method get_exn = all_exn
method! vstmt_aux s =
match s.skind with
- | Throw (Some (_,t),_) ->
- all_exn <- Cil_datatype.Typ.Set.add (purify t) all_exn;
- SkipChildren
- | _ -> DoChildren
+ | Throw (Some (_,t),_) ->
+ all_exn <- Cil_datatype.Typ.Set.add (purify t) all_exn;
+ SkipChildren
+ | _ -> DoChildren
end
let compute_all_exn () =
@@ -82,41 +82,41 @@ let add_exn_var exns v =
let add_exn_clause exns (v,_) = add_exn_var exns v
(* We're not really interested by intra-procedural Dataflow here: all the
- interesting stuff happens at inter-procedural level (except for Throw
+ interesting stuff happens at inter-procedural level (except for Throw
encapsulated directly in a TryCatch, but even then it is easily captured
- at syntactical level). Therefore, we can as well use a syntactic pass
+ at syntactical level). Therefore, we can as well use a syntactic pass
at intra-procedural level
- *)
+*)
class exn_visit =
-object (self)
- inherit Visitor.frama_c_inplace
- val stack = Stack.create ()
- val possible_exn = Stack.create ()
- (* current set of exn included in a catch-all clause. Used to
- handle Throw None;
- *)
- val current_exn = Stack.create ()
-
- method private recursive_call kf =
- try
- Stack.iter
- (fun (kf',_) -> if Kernel_function.equal kf kf' then raise Exit) stack;
- false
- with Exit -> true
-
- method private add_exn t =
- let current_uncaught = Stack.top possible_exn in
- current_uncaught:= Cil_datatype.Typ.Set.add t !current_uncaught
-
- method private union_exn s =
- let current_uncaught = Stack.top possible_exn in
- current_uncaught := Cil_datatype.Typ.Set.union s !current_uncaught
-
- method! vstmt_aux s =
- match s.skind with
+ object (self)
+ inherit Visitor.frama_c_inplace
+ val stack = Stack.create ()
+ val possible_exn = Stack.create ()
+ (* current set of exn included in a catch-all clause. Used to
+ handle Throw None;
+ *)
+ val current_exn = Stack.create ()
+
+ method private recursive_call kf =
+ try
+ Stack.iter
+ (fun (kf',_) -> if Kernel_function.equal kf kf' then raise Exit) stack;
+ false
+ with Exit -> true
+
+ method private add_exn t =
+ let current_uncaught = Stack.top possible_exn in
+ current_uncaught:= Cil_datatype.Typ.Set.add t !current_uncaught
+
+ method private union_exn s =
+ let current_uncaught = Stack.top possible_exn in
+ current_uncaught := Cil_datatype.Typ.Set.union s !current_uncaught
+
+ method! vstmt_aux s =
+ match s.skind with
| Throw (None,_) ->
- let my_exn = Stack.top current_exn in
- self#union_exn my_exn; ExnsStmt.replace s my_exn; SkipChildren
+ let my_exn = Stack.top current_exn in
+ self#union_exn my_exn; ExnsStmt.replace s my_exn; SkipChildren
| Throw(Some (_,t),_) ->
let t = Cil.unrollTypeDeep t in
let t = Cil.type_remove_qualifier_attributes t in
@@ -127,14 +127,14 @@ object (self)
let catch, catch_all =
List.fold_left
(fun (catch, catch_all) ->
- function
- | (Catch_all,_) -> catch, true
- | (Catch_exn(v,[]),_) ->
- let catch = add_exn_var catch v in
- catch, catch_all
- | (Catch_exn(_,aux), _) ->
- let catch = List.fold_left add_exn_clause catch aux in
- catch, catch_all)
+ function
+ | (Catch_all,_) -> catch, true
+ | (Catch_exn(v,[]),_) ->
+ let catch = add_exn_var catch v in
+ catch, catch_all
+ | (Catch_exn(_,aux), _) ->
+ let catch = List.fold_left add_exn_clause catch aux in
+ catch, catch_all)
(Cil_datatype.Typ.Set.empty,false) c
in
Stack.push (ref Cil_datatype.Typ.Set.empty) possible_exn;
@@ -147,7 +147,7 @@ object (self)
if not catch_all then self#union_exn uncaught;
List.iter
(fun (v,b) ->
- (match v with
+ (match v with
| Catch_all ->
(* catch_all will catch all exceptions that are not
already handled by a previous clause. It must be the
@@ -164,9 +164,9 @@ object (self)
add_exn_clause Cil_datatype.Typ.Set.empty aux
in
Stack.push catch current_exn);
- ignore
- (Visitor.visitFramacBlock (self:>Visitor.frama_c_inplace) b);
- ignore (Stack.pop current_exn))
+ ignore
+ (Visitor.visitFramacBlock (self:>Visitor.frama_c_inplace) b);
+ ignore (Stack.pop current_exn))
c;
let my_exn = !(Stack.pop possible_exn) in
ExnsStmt.replace s my_exn;
@@ -175,34 +175,34 @@ object (self)
| If _ | Switch _ | Loop _ | Block _ | UnspecifiedSequence _
| TryFinally _ | TryExcept _
| Instr _ -> (* must take into account exceptions thrown by a fun call*)
- Stack.push (ref Cil_datatype.Typ.Set.empty) possible_exn;
- DoChildrenPost
- (fun s ->
+ Stack.push (ref Cil_datatype.Typ.Set.empty) possible_exn;
+ DoChildrenPost
+ (fun s ->
let my_exn = !(Stack.pop possible_exn) in
ExnsStmt.replace s my_exn;
self#union_exn my_exn;
s)
(* No exception can be thrown here. *)
| Return _ | Goto _ | Break _ | Continue _ ->
- ExnsStmt.replace s Cil_datatype.Typ.Set.empty;
- SkipChildren
+ ExnsStmt.replace s Cil_datatype.Typ.Set.empty;
+ SkipChildren
- method! vinst =
- function
+ method! vinst =
+ function
| Call(_,{ enode = Lval(Var f,NoOffset) },_,_)
| Local_init(_, ConsInit(f, _, _), _) ->
let kf = Globals.Functions.get f in
if self#recursive_call kf then begin
let module Found =
- struct
- exception F of Cil_datatype.Typ.Set.t
- end
+ struct
+ exception F of Cil_datatype.Typ.Set.t
+ end
in
let computed_exn =
try
Stack.iter
(fun (kf', exns) ->
- if Kernel_function.equal kf kf' then raise (Found.F !exns))
+ if Kernel_function.equal kf kf' then raise (Found.F !exns))
stack;
Kernel.fatal "No cycle found!"
with Found.F exns -> exns
@@ -220,7 +220,7 @@ object (self)
let kf_exn = Cil_datatype.Typ.Set.union computed_exn known_exn in
Exns.replace kf kf_exn;
ignore
- (Visitor.visitFramacFunction
+ (Visitor.visitFramacFunction
(self:>Visitor.frama_c_visitor)
(Kernel_function.get_definition kf));
let callee_exn = Exns.find kf in
@@ -236,9 +236,9 @@ object (self)
self#union_exn callee_exn
end else begin (* TODO: introduce extension to declare
exceptions that can be thrown by prototypes. *)
- Kernel.warning
- "Assuming declared function %a can't throw any exception"
- Kernel_function.pretty kf
+ Kernel.warning
+ "Assuming declared function %a can't throw any exception"
+ Kernel_function.pretty kf
end;
SkipChildren
| Call _ ->
@@ -247,60 +247,60 @@ object (self)
self#union_exn (all_exn()); SkipChildren
| _ -> SkipChildren
- method! vfunc f =
- let my_exns = ref Cil_datatype.Typ.Set.empty in
- let kf = Globals.Functions.get f.svar in
- Stack.push (kf,my_exns) stack;
- Stack.push my_exns possible_exn;
- let after_visit f =
- let callee_exn = Stack.pop possible_exn in
- Exns.add kf !callee_exn;
- ignore (Stack.pop stack); f
- in
- DoChildrenPost after_visit
+ method! vfunc f =
+ let my_exns = ref Cil_datatype.Typ.Set.empty in
+ let kf = Globals.Functions.get f.svar in
+ Stack.push (kf,my_exns) stack;
+ Stack.push my_exns possible_exn;
+ let after_visit f =
+ let callee_exn = Stack.pop possible_exn in
+ Exns.add kf !callee_exn;
+ ignore (Stack.pop stack); f
+ in
+ DoChildrenPost after_visit
-end
+ end
let compute_kf kf =
if Kernel_function.is_definition kf then
ignore
(Visitor.visitFramacFunction (new exn_visit)
(Kernel_function.get_definition kf))
- (* just ignore prototypes. *)
+(* just ignore prototypes. *)
let compute () = Globals.Functions.iter compute_kf
let get_type_tag t =
let rec aux t =
match t with
- | TVoid _ -> "v"
- | TInt (IBool,_) -> "B"
- | TInt (IChar,_) -> "c"
- | TInt (ISChar,_) -> "sc"
- | TInt (IUChar,_) -> "uc"
- | TInt (IInt,_) -> "i"
- | TInt (IUInt,_) -> "ui"
- | TInt (IShort,_) -> "s"
- | TInt (IUShort,_) -> "us"
- | TInt (ILong,_) -> "l"
- | TInt (IULong,_) -> "ul"
- | TInt (ILongLong,_) -> "ll"
- | TInt (IULongLong,_) -> "ull"
- | TFloat(FFloat,_) -> "f"
- | TFloat(FDouble,_) -> "d"
- | TFloat (FLongDouble,_) -> "ld"
- | TPtr(t,_) -> "p" ^ aux t
- | TArray(t,_,_,_) -> "a" ^ aux t
- | TFun(rt,l,_,_) ->
- let base = "fun" ^ aux rt in
- (match l with
- | None -> base
- | Some l ->
- List.fold_left (fun acc (_,t,_) -> acc ^ aux t) base l)
- | TNamed _ -> Kernel.fatal "named type not correctly unrolled"
- | TComp (s,_,_) -> (if s.cstruct then "S" else "U") ^ s.cname
- | TEnum (e,_) -> "E" ^ e.ename
- | TBuiltin_va_list _ -> "va"
+ | TVoid _ -> "v"
+ | TInt (IBool,_) -> "B"
+ | TInt (IChar,_) -> "c"
+ | TInt (ISChar,_) -> "sc"
+ | TInt (IUChar,_) -> "uc"
+ | TInt (IInt,_) -> "i"
+ | TInt (IUInt,_) -> "ui"
+ | TInt (IShort,_) -> "s"
+ | TInt (IUShort,_) -> "us"
+ | TInt (ILong,_) -> "l"
+ | TInt (IULong,_) -> "ul"
+ | TInt (ILongLong,_) -> "ll"
+ | TInt (IULongLong,_) -> "ull"
+ | TFloat(FFloat,_) -> "f"
+ | TFloat(FDouble,_) -> "d"
+ | TFloat (FLongDouble,_) -> "ld"
+ | TPtr(t,_) -> "p" ^ aux t
+ | TArray(t,_,_,_) -> "a" ^ aux t
+ | TFun(rt,l,_,_) ->
+ let base = "fun" ^ aux rt in
+ (match l with
+ | None -> base
+ | Some l ->
+ List.fold_left (fun acc (_,t,_) -> acc ^ aux t) base l)
+ | TNamed _ -> Kernel.fatal "named type not correctly unrolled"
+ | TComp (s,_,_) -> (if s.cstruct then "S" else "U") ^ s.cname
+ | TEnum (e,_) -> "E" ^ e.ename
+ | TBuiltin_va_list _ -> "va"
in "__fc_" ^ aux t
let get_type_enum t = "__fc_exn_kind_" ^ (get_type_tag t)
@@ -372,9 +372,9 @@ let generate_exn_union e exns =
let add_types_and_globals typs globs f =
let iter_globs (acc,added) g =
match g with
- | GVarDecl _ | GVar _ | GFun _ as g when not added ->
- (g :: List.rev_append globs (List.rev_append typs acc), true)
- | _ -> g :: acc, added
+ | GVarDecl _ | GVar _ | GFun _ as g when not added ->
+ (g :: List.rev_append globs (List.rev_append typs acc), true)
+ | _ -> g :: acc, added
in
let globs, added = List.fold_left iter_globs ([],false) f.globals in
let globs =
@@ -399,130 +399,130 @@ let find_exns_func v =
let find_exns e =
match e.enode with
- | Lval(Var v, NoOffset) -> find_exns_func v
- | _ -> all_exn ()
+ | Lval(Var v, NoOffset) -> find_exns_func v
+ | _ -> all_exn ()
class erase_exn =
-object(self)
- inherit Visitor.frama_c_inplace
- (* reverse before filling. *)
- val mutable new_types = []
-
- val exn_enum = Cil_datatype.Typ.Hashtbl.create 7
+ object(self)
+ inherit Visitor.frama_c_inplace
+ (* reverse before filling. *)
+ val mutable new_types = []
- val exn_union = Cil_datatype.Typ.Hashtbl.create 7
+ val exn_enum = Cil_datatype.Typ.Hashtbl.create 7
- val mutable modified_funcs = Cil_datatype.Fundec.Set.empty
+ val exn_union = Cil_datatype.Typ.Hashtbl.create 7
- val mutable exn_struct = None
+ val mutable modified_funcs = Cil_datatype.Fundec.Set.empty
- val mutable exn_var = None
+ val mutable exn_struct = None
- val mutable can_throw = false
+ val mutable exn_var = None
- val mutable fct_can_throw = false
+ val mutable can_throw = false
- val mutable catched_var = None
+ val mutable fct_can_throw = false
- val mutable label_counter = 0
+ val mutable catched_var = None
- val exn_labels = Cil_datatype.Typ.Hashtbl.create 7
- val catch_all_label = Stack.create ()
+ val mutable label_counter = 0
- method modified_funcs = modified_funcs
+ val exn_labels = Cil_datatype.Typ.Hashtbl.create 7
+ val catch_all_label = Stack.create ()
- method private update_enum_bindings enum exns =
- let update_one_binding t =
- let s = get_type_enum t in
- let ei = List.find (fun ei -> ei.einame = s) enum.eitems in
- Cil_datatype.Typ.Hashtbl.add exn_enum t ei
- in
- Cil_datatype.Typ.Set.iter update_one_binding exns
+ method modified_funcs = modified_funcs
- method private update_union_bindings union exns =
- let update_one_binding t =
- let s = get_type_tag t in
- Kernel.debug ~dkey:Kernel.dkey_exn_flow
- "Registering %a as possible exn type" Cil_datatype.Typ.pretty t;
- let fi = List.find (fun fi -> fi.fname = s) union.cfields in
- Cil_datatype.Typ.Hashtbl.add exn_union t fi
- in
- Cil_datatype.Typ.Set.iter update_one_binding exns
-
- method private exn_kind t = Cil_datatype.Typ.Hashtbl.find exn_enum t
-
- method private is_thrown t = Cil_datatype.Typ.Hashtbl.mem exn_enum t
+ method private update_enum_bindings enum exns =
+ let update_one_binding t =
+ let s = get_type_enum t in
+ let ei = List.find (fun ei -> ei.einame = s) enum.eitems in
+ Cil_datatype.Typ.Hashtbl.add exn_enum t ei
+ in
+ Cil_datatype.Typ.Set.iter update_one_binding exns
+
+ method private update_union_bindings union exns =
+ let update_one_binding t =
+ let s = get_type_tag t in
+ Kernel.debug ~dkey:Kernel.dkey_exn_flow
+ "Registering %a as possible exn type" Cil_datatype.Typ.pretty t;
+ let fi = List.find (fun fi -> fi.fname = s) union.cfields in
+ Cil_datatype.Typ.Hashtbl.add exn_union t fi
+ in
+ Cil_datatype.Typ.Set.iter update_one_binding exns
- method private exn_field_off name =
- List.find (fun fi -> fi.fname = name) (Extlib.the exn_struct).cfields
+ method private exn_kind t = Cil_datatype.Typ.Hashtbl.find exn_enum t
- method private exn_field name =
- Var (Extlib.the exn_var), Field(self#exn_field_off name, NoOffset)
+ method private is_thrown t = Cil_datatype.Typ.Hashtbl.mem exn_enum t
- method private exn_field_term name =
- TVar(Cil.cvar_to_lvar (Extlib.the exn_var)),
- TField(self#exn_field_off name, TNoOffset)
+ method private exn_field_off name =
+ List.find (fun fi -> fi.fname = name) (Extlib.the exn_struct).cfields
- method private exn_obj_field = self#exn_field exn_obj_name
+ method private exn_field name =
+ Var (Extlib.the exn_var), Field(self#exn_field_off name, NoOffset)
- method private exn_obj_field_term = self#exn_field_term exn_obj_name
+ method private exn_field_term name =
+ TVar(Cil.cvar_to_lvar (Extlib.the exn_var)),
+ TField(self#exn_field_off name, TNoOffset)
- method private exn_kind_field = self#exn_field exn_kind_name
+ method private exn_obj_field = self#exn_field exn_obj_name
- method private exn_kind_field_term = self#exn_field_term exn_kind_name
+ method private exn_obj_field_term = self#exn_field_term exn_obj_name
- method private uncaught_flag_field = self#exn_field exn_uncaught_name
+ method private exn_kind_field = self#exn_field exn_kind_name
- method private uncaught_flag_field_term =
- self#exn_field_term exn_uncaught_name
+ method private exn_kind_field_term = self#exn_field_term exn_kind_name
- method private exn_obj_kind_field t =
- Kernel.debug ~dkey:Kernel.dkey_exn_flow
- "Searching for %a as possible exn type" Cil_datatype.Typ.pretty t;
- Cil_datatype.Typ.Hashtbl.find exn_union t
+ method private uncaught_flag_field = self#exn_field exn_uncaught_name
- method private test_uncaught_flag loc b =
- let e1 = Cil.new_exp ~loc (Lval self#uncaught_flag_field) in
- let e2 = if b then Cil.one ~loc else Cil.zero ~loc in
- Cil.new_exp ~loc (BinOp(Eq,e1,e2,Cil.intType))
+ method private uncaught_flag_field_term =
+ self#exn_field_term exn_uncaught_name
- method private pred_uncaught_flag loc b =
- let e1 =
- Logic_const.term
- ~loc (TLval self#uncaught_flag_field_term) Linteger
- in
- let e2 =
- if b then Logic_const.tinteger ~loc 1
- else Logic_const.tinteger ~loc 0
- in
- Logic_const.prel ~loc (Req,e1,e2)
-
- method private set_uncaught_flag loc b =
- let e = if b then Cil.one ~loc else Cil.zero ~loc in
- Cil.mkStmtOneInstr (Set(self#uncaught_flag_field,e,loc))
-
- method private set_exn_kind loc t =
- let e = self#exn_kind (purify t) in
- let e = Cil.new_exp ~loc (Const (CEnum e)) in
- Cil.mkStmtOneInstr(Set(self#exn_kind_field,e,loc))
-
- method private set_exn_value loc t e =
- let lv = self#exn_obj_field in
- let union_field = self#exn_obj_kind_field (purify t) in
- let lv = Cil.addOffsetLval (Field (union_field, NoOffset)) lv in
- Cil.mkStmtOneInstr (Set(lv,e,loc))
-
- method private jumps_to_default_handler loc =
- if Stack.is_empty catch_all_label then begin
- (* no catch-all clause in the function: just go up in the stack. *)
- fct_can_throw <- true;
- let kf = Extlib.the self#current_kf in
- let ret = Kernel_function.find_return kf in
- let rtyp = Kernel_function.get_return_type kf in
- if ret.labels = [] then
- ret.labels <- [Label("__ret_label",Cil_datatype.Stmt.loc ret,false)];
- let goto = mkStmt (Goto (ref ret,loc)) in
- match ret.skind with
+ method private exn_obj_kind_field t =
+ Kernel.debug ~dkey:Kernel.dkey_exn_flow
+ "Searching for %a as possible exn type" Cil_datatype.Typ.pretty t;
+ Cil_datatype.Typ.Hashtbl.find exn_union t
+
+ method private test_uncaught_flag loc b =
+ let e1 = Cil.new_exp ~loc (Lval self#uncaught_flag_field) in
+ let e2 = if b then Cil.one ~loc else Cil.zero ~loc in
+ Cil.new_exp ~loc (BinOp(Eq,e1,e2,Cil.intType))
+
+ method private pred_uncaught_flag loc b =
+ let e1 =
+ Logic_const.term
+ ~loc (TLval self#uncaught_flag_field_term) Linteger
+ in
+ let e2 =
+ if b then Logic_const.tinteger ~loc 1
+ else Logic_const.tinteger ~loc 0
+ in
+ Logic_const.prel ~loc (Req,e1,e2)
+
+ method private set_uncaught_flag loc b =
+ let e = if b then Cil.one ~loc else Cil.zero ~loc in
+ Cil.mkStmtOneInstr (Set(self#uncaught_flag_field,e,loc))
+
+ method private set_exn_kind loc t =
+ let e = self#exn_kind (purify t) in
+ let e = Cil.new_exp ~loc (Const (CEnum e)) in
+ Cil.mkStmtOneInstr(Set(self#exn_kind_field,e,loc))
+
+ method private set_exn_value loc t e =
+ let lv = self#exn_obj_field in
+ let union_field = self#exn_obj_kind_field (purify t) in
+ let lv = Cil.addOffsetLval (Field (union_field, NoOffset)) lv in
+ Cil.mkStmtOneInstr (Set(lv,e,loc))
+
+ method private jumps_to_default_handler loc =
+ if Stack.is_empty catch_all_label then begin
+ (* no catch-all clause in the function: just go up in the stack. *)
+ fct_can_throw <- true;
+ let kf = Extlib.the self#current_kf in
+ let ret = Kernel_function.find_return kf in
+ let rtyp = Kernel_function.get_return_type kf in
+ if ret.labels = [] then
+ ret.labels <- [Label("__ret_label",Cil_datatype.Stmt.loc ret,false)];
+ let goto = mkStmt (Goto (ref ret,loc)) in
+ match ret.skind with
| Return (None,_) -> [goto]
(* rt is void: do not need to create a dummy return value *)
| Return (Some { enode = Lval(Var rv, NoOffset) },_) ->
@@ -532,232 +532,232 @@ object(self)
Kernel.fatal "exception removal should be used after oneRet"
| _ ->
Kernel.fatal "find_return did not give a Return statement"
- end else begin
- let stmt = Stack.top catch_all_label in
- [mkStmt (Goto (ref stmt, loc))]
- end
-
- method private jumps_to_handler loc t =
- let t = purify t in
- try
- let stmt = Cil_datatype.Typ.Hashtbl.find exn_labels t in
- [mkStmt (Goto (ref stmt, loc))]
- with
+ end else begin
+ let stmt = Stack.top catch_all_label in
+ [mkStmt (Goto (ref stmt, loc))]
+ end
+
+ method private jumps_to_handler loc t =
+ let t = purify t in
+ try
+ let stmt = Cil_datatype.Typ.Hashtbl.find exn_labels t in
+ [mkStmt (Goto (ref stmt, loc))]
+ with
| Not_found -> self#jumps_to_default_handler loc
- method! vfile f =
- let exns = all_exn () in
- if not (Cil_datatype.Typ.Set.is_empty exns) then begin
- let loc = Cil_datatype.Location.unknown in
- let e = generate_exn_enum exns in
- let u,s = generate_exn_union e exns in
- let exn =
- Cil.makeGlobalVar "__fc_exn" (TComp (s,{scache = Not_Computed},[]))
- in
- self#update_enum_bindings e exns;
- self#update_union_bindings u exns;
- exn_struct <- Some s;
- can_throw <- true;
- new_types <-
- GCompTag (s,loc) ::
- GCompTag (u,loc) ::
- GEnumTag (e,loc) :: new_types;
- exn_var <- Some exn;
- let exn_init = Cil.makeZeroInit ~loc (TComp(s,{scache=Not_Computed},[]))
- in
- let gexn_var = GVar(exn, { init = Some exn_init }, loc) in
- ChangeDoChildrenPost(
- f,add_types_and_globals (List.rev new_types) [gexn_var])
- end else (* nothing can be thrown in the first place, but we still have
- to get rid of (useless) try/catch blocks if any. *)
+ method! vfile f =
+ let exns = all_exn () in
+ if not (Cil_datatype.Typ.Set.is_empty exns) then begin
+ let loc = Cil_datatype.Location.unknown in
+ let e = generate_exn_enum exns in
+ let u,s = generate_exn_union e exns in
+ let exn =
+ Cil.makeGlobalVar "__fc_exn" (TComp (s,{scache = Not_Computed},[]))
+ in
+ self#update_enum_bindings e exns;
+ self#update_union_bindings u exns;
+ exn_struct <- Some s;
+ can_throw <- true;
+ new_types <-
+ GCompTag (s,loc) ::
+ GCompTag (u,loc) ::
+ GEnumTag (e,loc) :: new_types;
+ exn_var <- Some exn;
+ let exn_init = Cil.makeZeroInit ~loc (TComp(s,{scache=Not_Computed},[]))
+ in
+ let gexn_var = GVar(exn, { init = Some exn_init }, loc) in
+ ChangeDoChildrenPost(
+ f,add_types_and_globals (List.rev new_types) [gexn_var])
+ end else (* nothing can be thrown in the first place, but we still have
+ to get rid of (useless) try/catch blocks if any. *)
DoChildren
- method private visit_catch_clause loc (v,b) =
- let loc =
- match b.bstmts with
+ method private visit_catch_clause loc (v,b) =
+ let loc =
+ match b.bstmts with
| [] -> loc
| [x] -> Cil_datatype.Stmt.loc x
| x::tl ->
fst (Cil_datatype.Stmt.loc x),
snd (Cil_datatype.Stmt.loc (Extlib.last tl))
- in
- let add_unreachable_block b =
- Cil.mkStmt (If(Cil.zero ~loc, b, Cil.mkBlock [], loc))
- in
- let assign_catched_obj v b =
- let exn_obj = self#exn_obj_field in
- let kind_field = self#exn_obj_kind_field (purify v.vtype) in
- let lv = Cil.addOffsetLval (Field (kind_field,NoOffset)) exn_obj in
- let s =
- Cil.mkStmtOneInstr
- (Set ((Var v, NoOffset), Cil.new_exp ~loc (Lval lv), loc))
in
- b.bstmts <- s :: b.bstmts
- in
- let f = Extlib.the self#current_func in
- let update_locals v b =
- if not (List.memq v b.blocals) then b.blocals <- v::b.blocals;
- if not (List.memq v f.slocals) then f.slocals <- v::f.slocals
- in
- let b =
- (match v with
- | Catch_all -> b
- | Catch_exn (v,[]) ->
- Cil.update_var_type v (purify v.vtype);
- update_locals v b;
- assign_catched_obj v b; b
- | Catch_exn(v,aux) ->
- let add_one_aux stmts (v,b) =
- Cil.update_var_type v (purify v.vtype);
- update_locals v b;
- assign_catched_obj v b;
- add_unreachable_block b :: stmts
- in
- b.blocals <- List.filter (fun v' -> v!=v') b.blocals;
- let aux_blocks =
- List.fold_left add_one_aux [Cil.mkStmt (Block b)] aux
- in
- let main_block = Cil.mkBlock aux_blocks in
- Cil.update_var_type v (purify v.vtype);
- update_locals v main_block;
- main_block)
- in
- ignore (Visitor.visitFramacBlock (self :> Visitor.frama_c_visitor) b);
- add_unreachable_block b
-
- method! vfunc _ =
- label_counter <- 0;
- fct_can_throw <- false;
- let update_body f =
- if fct_can_throw then begin
- Oneret.encapsulate_local_vars f
- end;
- f
- in
- DoChildrenPost update_body
+ let add_unreachable_block b =
+ Cil.mkStmt (If(Cil.zero ~loc, b, Cil.mkBlock [], loc))
+ in
+ let assign_catched_obj v b =
+ let exn_obj = self#exn_obj_field in
+ let kind_field = self#exn_obj_kind_field (purify v.vtype) in
+ let lv = Cil.addOffsetLval (Field (kind_field,NoOffset)) exn_obj in
+ let s =
+ Cil.mkStmtOneInstr
+ (Set ((Var v, NoOffset), Cil.new_exp ~loc (Lval lv), loc))
+ in
+ b.bstmts <- s :: b.bstmts
+ in
+ let f = Extlib.the self#current_func in
+ let update_locals v b =
+ if not (List.memq v b.blocals) then b.blocals <- v::b.blocals;
+ if not (List.memq v f.slocals) then f.slocals <- v::f.slocals
+ in
+ let b =
+ (match v with
+ | Catch_all -> b
+ | Catch_exn (v,[]) ->
+ Cil.update_var_type v (purify v.vtype);
+ update_locals v b;
+ assign_catched_obj v b; b
+ | Catch_exn(v,aux) ->
+ let add_one_aux stmts (v,b) =
+ Cil.update_var_type v (purify v.vtype);
+ update_locals v b;
+ assign_catched_obj v b;
+ add_unreachable_block b :: stmts
+ in
+ b.blocals <- List.filter (fun v' -> v!=v') b.blocals;
+ let aux_blocks =
+ List.fold_left add_one_aux [Cil.mkStmt (Block b)] aux
+ in
+ let main_block = Cil.mkBlock aux_blocks in
+ Cil.update_var_type v (purify v.vtype);
+ update_locals v main_block;
+ main_block)
+ in
+ ignore (Visitor.visitFramacBlock (self :> Visitor.frama_c_visitor) b);
+ add_unreachable_block b
+
+ method! vfunc _ =
+ label_counter <- 0;
+ fct_can_throw <- false;
+ let update_body f =
+ if fct_can_throw then begin
+ Oneret.encapsulate_local_vars f
+ end;
+ f
+ in
+ DoChildrenPost update_body
- method private modify_current () =
- modified_funcs <-
- Cil_datatype.Fundec.Set.add (Extlib.the self#current_func) modified_funcs;
+ method private modify_current () =
+ modified_funcs <-
+ Cil_datatype.Fundec.Set.add (Extlib.the self#current_func) modified_funcs;
- method private aux_handler_goto target (v,b) =
- let loc = v.vdecl in
- let goto_main_handler = Cil.mkStmt (Goto (ref target,loc)) in
- let suf =
- if label_counter = 0 then "" else "_" ^ (string_of_int label_counter)
- in
- let lab = (get_type_tag (purify v.vtype)) ^ suf in
- label_counter <- label_counter + 1;
- b.bstmts <- b.bstmts @ [goto_main_handler];
- (* we have at least the goto statement in the block *)
- let s = List.hd b.bstmts in
- s.labels <- (Label(lab,loc,false)::s.labels);
- Cil_datatype.Typ.Hashtbl.add exn_labels (purify v.vtype) s
-
- method private guard_post_cond (kind,pred as orig) =
- match kind with
- (* If we exit explicitly with exit,
- we haven't seen an uncaught exception anyway. *)
+ method private aux_handler_goto target (v,b) =
+ let loc = v.vdecl in
+ let goto_main_handler = Cil.mkStmt (Goto (ref target,loc)) in
+ let suf =
+ if label_counter = 0 then "" else "_" ^ (string_of_int label_counter)
+ in
+ let lab = (get_type_tag (purify v.vtype)) ^ suf in
+ label_counter <- label_counter + 1;
+ b.bstmts <- b.bstmts @ [goto_main_handler];
+ (* we have at least the goto statement in the block *)
+ let s = List.hd b.bstmts in
+ s.labels <- (Label(lab,loc,false)::s.labels);
+ Cil_datatype.Typ.Hashtbl.add exn_labels (purify v.vtype) s
+
+ method private guard_post_cond (kind,pred as orig) =
+ match kind with
+ (* If we exit explicitly with exit,
+ we haven't seen an uncaught exception anyway. *)
| Exits | Breaks | Continues -> orig
| Returns | Normal ->
- let loc = pred.ip_content.pred_loc in
- let p = self#pred_uncaught_flag loc false in
- let pred' = Logic_const.pred_of_id_pred pred in
- (kind,
- (Logic_const.new_predicate
- (Logic_const.pimplies ~loc (p,pred'))))
-
- method! vbehavior b =
- match self#current_kf, self#current_stmt with
+ let loc = pred.ip_content.pred_loc in
+ let p = self#pred_uncaught_flag loc false in
+ let pred' = Logic_const.pred_of_id_pred pred in
+ (kind,
+ (Logic_const.new_predicate
+ (Logic_const.pimplies ~loc (p,pred'))))
+
+ method! vbehavior b =
+ match self#current_kf, self#current_stmt with
| None, None -> SkipChildren
- (* Prototype is assumed to not throw any exception. *)
+ (* Prototype is assumed to not throw any exception. *)
| None, Some _ ->
- Kernel.fatal
- "Inconsistent visitor state: visiting a statement \
- outside of any function."
- | Some f, None when not (Kernel_function.is_definition f) ->
- (* By hypothesis, prototypes do not throw anything. *)
- SkipChildren
+ Kernel.fatal
+ "Inconsistent visitor state: visiting a statement \
+ outside of any function."
+ | Some f, None when not (Kernel_function.is_definition f) ->
+ (* By hypothesis, prototypes do not throw anything. *)
+ SkipChildren
| Some f, None -> (* function contract *)
- let exns = Exns.find f in
- if Cil_datatype.Typ.Set.is_empty exns then SkipChildren
- else begin
- b.b_post_cond <- List.map self#guard_post_cond b.b_post_cond;
- ChangeTo b (* need to register the new clauses. *)
- end
+ let exns = Exns.find f in
+ if Cil_datatype.Typ.Set.is_empty exns then SkipChildren
+ else begin
+ b.b_post_cond <- List.map self#guard_post_cond b.b_post_cond;
+ ChangeTo b (* need to register the new clauses. *)
+ end
| Some _, Some s -> (* statement contract *)
- let exns = ExnsStmt.find s in
- if Cil_datatype.Typ.Set.is_empty exns then SkipChildren
- else begin
- b.b_post_cond <- List.map self#guard_post_cond b.b_post_cond;
- ChangeTo b
- end
-
- method private clean_catch_clause (bind,b as handler) acc =
- let remove_local v =
- let f =
- Visitor_behavior.Get.fundec self#behavior (Extlib.the self#current_func)
- in
- let v = Visitor_behavior.Get.varinfo self#behavior v in
- f.slocals <- List.filter (fun v' -> v!=v') f.slocals;
- in
- match bind with
- | Catch_all -> handler :: acc
- | Catch_exn (v, []) ->
- if self#is_thrown (purify v.vtype) then handler :: acc
- else begin remove_local v; acc end
- | Catch_exn (v, l) ->
- let caught, remove =
- List.partition (fun (v,_) -> self#is_thrown (purify v.vtype)) l
- in
- List.iter (fun (v,_) -> remove_local v) remove;
- if caught = [] then begin remove_local v; acc end
- else (Catch_exn (v,caught), b) :: acc
-
- method! vstmt_aux s =
- let generate_jumps instr exns loc =
- if Cil_datatype.Typ.Set.is_empty exns then SkipChildren
- else begin
- self#modify_current ();
- let make_jump t (stmts, uncaught) =
- let t = purify t in
- if Cil_datatype.Typ.Hashtbl.mem exn_labels t then begin
- let e = self#exn_kind t in
- let e = Cil.new_exp ~loc (Const (CEnum e)) in
- let b = self#jumps_to_handler loc t in
- let s = Cil.mkStmt (Block (Cil.mkBlock b)) in
- s.labels <- [Case (e,loc)];
- s::stmts, uncaught
- end else stmts, true
+ let exns = ExnsStmt.find s in
+ if Cil_datatype.Typ.Set.is_empty exns then SkipChildren
+ else begin
+ b.b_post_cond <- List.map self#guard_post_cond b.b_post_cond;
+ ChangeTo b
+ end
+
+ method private clean_catch_clause (bind,b as handler) acc =
+ let remove_local v =
+ let f =
+ Visitor_behavior.Get.fundec self#behavior (Extlib.the self#current_func)
in
- let stmts, uncaught =
- Cil_datatype.Typ.Set.fold make_jump exns ([],false)
+ let v = Visitor_behavior.Get.varinfo self#behavior v in
+ f.slocals <- List.filter (fun v' -> v!=v') f.slocals;
+ in
+ match bind with
+ | Catch_all -> handler :: acc
+ | Catch_exn (v, []) ->
+ if self#is_thrown (purify v.vtype) then handler :: acc
+ else begin remove_local v; acc end
+ | Catch_exn (v, l) ->
+ let caught, remove =
+ List.partition (fun (v,_) -> self#is_thrown (purify v.vtype)) l
in
- let stmts =
- if uncaught then begin
- let default =
+ List.iter (fun (v,_) -> remove_local v) remove;
+ if caught = [] then begin remove_local v; acc end
+ else (Catch_exn (v,caught), b) :: acc
+
+ method! vstmt_aux s =
+ let generate_jumps instr exns loc =
+ if Cil_datatype.Typ.Set.is_empty exns then SkipChildren
+ else begin
+ self#modify_current ();
+ let make_jump t (stmts, uncaught) =
+ let t = purify t in
+ if Cil_datatype.Typ.Hashtbl.mem exn_labels t then begin
+ let e = self#exn_kind t in
+ let e = Cil.new_exp ~loc (Const (CEnum e)) in
+ let b = self#jumps_to_handler loc t in
+ let s = Cil.mkStmt (Block (Cil.mkBlock b)) in
+ s.labels <- [Case (e,loc)];
+ s::stmts, uncaught
+ end else stmts, true
+ in
+ let stmts, uncaught =
+ Cil_datatype.Typ.Set.fold make_jump exns ([],false)
+ in
+ let stmts =
+ if uncaught then begin
+ let default =
Cil.mkStmt (
Block (Cil.mkBlock (self#jumps_to_default_handler loc)))
- in
- default.labels <- [Default loc];
- List.rev_append stmts [default]
- end else List.rev stmts
- in
- let test = self#test_uncaught_flag loc true in
- let cases = Cil.new_exp ~loc (Lval self#exn_kind_field) in
- let switch = Cil.mkStmt (Switch(cases,Cil.mkBlock stmts,stmts,loc)) in
- let handler =
- Cil.mkStmt (If(test,Cil.mkBlock [switch],Cil.mkBlock [],loc))
- in
- let instr =
- Visitor.visitFramacInstr (self:>Visitor.frama_c_visitor) instr
- in
- let call = Cil.mkStmtOneInstr (List.hd instr) in
- s.skind <- Block (Cil.mkBlockNonScoping [call;handler]);
- SkipChildren
- end
- in
- match s.skind with
+ in
+ default.labels <- [Default loc];
+ List.rev_append stmts [default]
+ end else List.rev stmts
+ in
+ let test = self#test_uncaught_flag loc true in
+ let cases = Cil.new_exp ~loc (Lval self#exn_kind_field) in
+ let switch = Cil.mkStmt (Switch(cases,Cil.mkBlock stmts,stmts,loc)) in
+ let handler =
+ Cil.mkStmt (If(test,Cil.mkBlock [switch],Cil.mkBlock [],loc))
+ in
+ let instr =
+ Visitor.visitFramacInstr (self:>Visitor.frama_c_visitor) instr
+ in
+ let call = Cil.mkStmtOneInstr (List.hd instr) in
+ s.skind <- Block (Cil.mkBlockNonScoping [call;handler]);
+ SkipChildren
+ end
+ in
+ match s.skind with
| Instr (Call (_,f,_,loc) as instr) ->
generate_jumps instr (find_exns f) loc
| Instr (Local_init(_, ConsInit(f,_,_), loc) as instr) ->
@@ -795,7 +795,7 @@ object(self)
than the current block. As we are adding statements in the
auxiliary blocks, we need to do that before adding labels to the
entry points of these blocks.
- *)
+ *)
let stmts = List.map (self#visit_catch_clause loc) c in
let suf =
if label_counter = 0 then "" else "_" ^ (string_of_int label_counter)
@@ -812,10 +812,10 @@ object(self)
stmt.labels <- [Label (label,v.vdecl,false)];
b.bstmts <- stmt :: b.bstmts;
(match aux with
- | [] ->
- Cil_datatype.Typ.Hashtbl.add exn_labels (purify v.vtype) stmt
- | _ :: _ ->
- List.iter (self#aux_handler_goto stmt) aux)
+ | [] ->
+ Cil_datatype.Typ.Hashtbl.add exn_labels (purify v.vtype) stmt
+ | _ :: _ ->
+ List.iter (self#aux_handler_goto stmt) aux)
| (Catch_all, b) ->
let loc =
match b.bstmts with [] -> loc | s::_ -> Cil_datatype.Stmt.loc s
@@ -837,7 +837,7 @@ object(self)
| Catch_exn(_,l), _ ->
List.iter
(fun (v,_) ->
- Cil_datatype.Typ.Hashtbl.remove exn_labels (purify v.vtype))
+ Cil_datatype.Typ.Hashtbl.remove exn_labels (purify v.vtype))
l
| Catch_all,_ -> ignore (Stack.pop catch_all_label))
c; (* we remove bindings in the reverse order as we added them,
@@ -846,8 +846,8 @@ object(self)
s.skind <- Block t;
SkipChildren
| _ -> DoChildren
-
-end
+
+ end
let prepare_file f =
if Kernel.SimplifyCfg.get () then begin
diff --git a/src/kernel_services/ast_data/annotations.ml b/src/kernel_services/ast_data/annotations.ml
index 9152b5e455fd39d1c64ef5e1836b8beb0872b28a..7f6f2802239ca20044ef97d8dbd18fd2146d74a1 100644
--- a/src/kernel_services/ast_data/annotations.ml
+++ b/src/kernel_services/ast_data/annotations.ml
@@ -290,85 +290,64 @@ module Behavior_set_map = Transitioning.Stdlib.Map.Make(Datatype.String.Set)
let is_same_behavior_set l1 l2 =
Datatype.String.Set.(equal (of_list l1) (of_list l2))
-let merge_stmt_contracts_emitters contracts =
- let add_one acc (c,e) =
- match c.annot_content with
- | AStmtSpec(bhvs, spec) ->
- let bhvs = Datatype.String.Set.of_list bhvs in
- (match Behavior_set_map.find_opt bhvs acc with
- | Some (spec', e') ->
- merge_funspec spec' spec;
- if Emitter.equal e e' then acc
- else
- Behavior_set_map.add bhvs (spec', Emitter.kernel) acc
- | None ->
- let spec' = Cil.empty_funspec () in
- merge_funspec spec' spec;
- Behavior_set_map.add bhvs (spec',e) acc
- (* avoid sharing directly the spec,
- as merge_funspec will modify it in place*))
- | _ -> acc
- in
- let merged_contracts =
- List.fold_left add_one Behavior_set_map.empty contracts
- in
- Behavior_set_map.fold
- (fun bhvs (spec,e) acc ->
- (Logic_const.new_code_annotation
- (AStmtSpec (Datatype.String.Set.elements bhvs, spec)),e)
- :: acc)
- merged_contracts []
-
-let merge_loop_assigns_emitters annots =
- let merge_assigns bhvs (a,e) acc =
+let merge_annots_emitters extract merge make annots =
+ let merge_same_bhvs bhvs (ca,a,e) acc =
let elt =
match Behavior_set_map.find_opt bhvs acc with
- | Some (a',e') ->
- let a' = merge_assigns ~keep_empty:false a a' in
+ | Some (ca', a',e') ->
+ let a' = merge a a' in
let e' = if Emitter.equal e e' then e else Emitter.kernel in
- a', e'
- | None -> a,e
+ let ca' =
+ if Cil_datatype.Code_annotation.compare ca' ca < 0 then ca' else ca
+ in
+ let annot_content = make (Datatype.String.Set.elements bhvs) a' in
+ let ca' = { ca' with annot_content } in
+ ca', a', e'
+ | None -> ca,a,e
in
Behavior_set_map.add bhvs elt acc
in
let treat_code_annot acc (ca,e) =
- match ca.annot_content with
- | AAssigns(bhvs,a) ->
- merge_assigns (Datatype.String.Set.of_list bhvs) (a,e) acc
- | _ -> acc
+ match extract ca with
+ | Some(bhvs,a) ->
+ merge_same_bhvs (Datatype.String.Set.of_list bhvs) (ca,a,e) acc
+ | None -> acc
in
let bhvs = List.fold_left treat_code_annot Behavior_set_map.empty annots in
- Behavior_set_map.fold
- (fun bhvs (a,e) acc ->
- (Logic_const.new_code_annotation
- (AAssigns (Datatype.String.Set.elements bhvs, a)),e)
- :: acc)
- bhvs []
-
-let merge_loop_allocation annots =
- let merge_allocates bhvs (a,e) acc =
- let elt =
- match Behavior_set_map.find_opt bhvs acc with
- | Some (a', e') ->
- let a' = merge_allocation ~keep_empty:false a a' in
- let e' = if Emitter.equal e e' then e else Emitter.kernel in
- a', e'
- | None -> a,e
- in Behavior_set_map.add bhvs elt acc
+ Behavior_set_map.fold (fun _ (ca,_,e) acc -> (ca,e) :: acc) bhvs []
+
+let merge_stmt_contracts_emitters =
+ let extract ca =
+ match ca.annot_content with
+ | AStmtSpec(bhvs, spec) -> Some (bhvs,spec)
+ | _ -> None
in
- let treat_code_annot acc (ca, e) =
+ let merge s s' =
+ let e = Cil.empty_funspec() in
+ merge_funspec e s;
+ merge_funspec e s';
+ e
+ in
+ let make bhvs s = AStmtSpec(bhvs,s) in
+ merge_annots_emitters extract merge make
+
+let merge_loop_assigns_emitter =
+ let extract ca =
match ca.annot_content with
- | AAllocation(bhvs,a) ->
- merge_allocates (Datatype.String.Set.of_list bhvs) (a,e) acc
- | _ -> acc
+ | AAssigns(bhvs,a) -> Some(bhvs,a)
+ | _ -> None
in
- let bhvs = List.fold_left treat_code_annot Behavior_set_map.empty annots in
- Behavior_set_map.fold
- (fun bhvs (a,e) acc ->
- (Logic_const.new_code_annotation
- (AAllocation (Datatype.String.Set.elements bhvs, a)),e)
- ::acc)
- bhvs []
+ let merge a a' = merge_assigns ~keep_empty:false a a' in
+ let make bhvs a = AAssigns(bhvs,a) in
+ merge_annots_emitters extract merge make
+
+let merge_loop_allocation_emitter =
+ let extract ca =
+ match ca.annot_content with AAllocation(bhvs,a) -> Some (bhvs,a) | _ -> None
+ in
+ let merge a a' = merge_allocation ~keep_empty:false a a' in
+ let make bhvs a = AAllocation(bhvs,a) in
+ merge_annots_emitters extract merge make
let partition_code_annot_emitter l =
let add_one_ca (contracts, assigns, alloc, others) (ca,_ as v) =
@@ -410,8 +389,8 @@ let code_annot_emitter ?filter stmt =
in
let contracts,assigns,allocation,others = partition_code_annot_emitter l in
merge_stmt_contracts_emitters contracts @
- merge_loop_assigns_emitters assigns @
- merge_loop_allocation allocation @
+ merge_loop_assigns_emitter assigns @
+ merge_loop_allocation_emitter allocation @
others
with Not_found ->
[]
@@ -541,25 +520,12 @@ let model_fields ?emitter t =
(**************************************************************************)
let iter_code_annot f stmt =
- try
- let tbl = Code_annots.find stmt in
- Emitter.Usable_emitter.Hashtbl.iter
- (fun e l -> List.iter (f (Emitter.Usable_emitter.get e)) !l)
- tbl
- with Not_found ->
- ()
+ let l = code_annot_emitter stmt in
+ List.iter (fun (a,e) -> f e a) l
let fold_code_annot f stmt acc =
- try
- let tbl = Code_annots.find stmt in
- Emitter.Usable_emitter.Hashtbl.fold
- (fun e l acc ->
- let e = Emitter.Usable_emitter.get e in
- List.fold_left (fun acc x -> f e x acc) acc !l)
- tbl
- acc
- with Not_found ->
- acc
+ let l = code_annot_emitter stmt in
+ List.fold_left (fun acc (a,e) -> f e a acc) acc l
let iter_all_code_annot ?(sorted=true) f =
let cmp s1 s2 =
@@ -1071,6 +1037,25 @@ let add_ensures e kf ?stmt ?active ?behavior l =
in
extend_behavior e kf ?stmt ?active ?behavior set_bhv
+let get_full_spec kf ?stmt ?(behavior=[]) () =
+ match stmt with
+ | None ->
+ (try funspec ~populate:false kf with Not_found -> Cil.empty_funspec())
+ | Some stmt ->
+ let filter a =
+ match a.annot_content with
+ | AStmtSpec(bhvs,_) when is_same_behavior_set bhvs behavior -> true
+ | _ -> false
+ in
+ (match code_annot ~filter stmt with
+ | [] -> Cil.empty_funspec ()
+ | [ { annot_content = AStmtSpec(_,s)} ] -> s
+ | _ -> Kernel.fatal "More than one contract associated to a statement")
+
+let get_spec_behavior s = function
+ | None -> Cil.find_default_behavior s
+ | Some name -> List.find_opt (fun { b_name } -> b_name = name) s.spec_behavior
+
let add_assigns ~keep_empty e kf ?stmt ?active ?behavior a =
let set_bhv full_bhv e_bhv =
let keep_empty = keep_empty && full_bhv.b_assigns = WritesAny in
@@ -1093,7 +1078,15 @@ let add_assigns ~keep_empty e kf ?stmt ?active ?behavior a =
(Property.ip_from_of_behavior kf ki active full_bhv);
)
in
- extend_behavior e kf ?stmt ?active ?behavior set_bhv
+ let old_spec = get_full_spec kf ?stmt ?behavior:active () in
+ let bhv = get_spec_behavior old_spec behavior in
+ let is_empty =
+ match bhv with
+ | None -> true
+ | Some b -> b.b_assigns = WritesAny
+ in
+ if not (keep_empty && is_empty) then
+ extend_behavior e kf ?stmt ?active ?behavior set_bhv
let add_allocates ~keep_empty e kf ?stmt ?active ?behavior a =
let ki = kinstr stmt in
@@ -1109,7 +1102,15 @@ let add_allocates ~keep_empty e kf ?stmt ?active ?behavior a =
Extlib.may Property_status.register
(Property.ip_allocation_of_behavior kf ki active full_bhv);
in
- extend_behavior e kf ?stmt ?active ?behavior set_bhv
+ let old_spec = get_full_spec kf ?stmt ?behavior:active () in
+ let bhv = get_spec_behavior old_spec behavior in
+ let is_empty =
+ match bhv with
+ | None -> true
+ | Some b -> b.b_allocation = FreeAllocAny
+ in
+ if not (keep_empty && is_empty) then
+ extend_behavior e kf ?stmt ?active ?behavior set_bhv
let add_extended e kf ?stmt ?active ?behavior ext =
let set_bhv _ e_bhv =
@@ -1121,212 +1122,165 @@ let add_extended e kf ?stmt ?active ?behavior ext =
(** {3 Adding code annotations} *)
-let add_code_annot emitter ?kf stmt ca =
+let add_code_annot ?(keep_empty=true) emitter ?kf stmt ca =
(* Kernel.feedback "%a: adding code annot %a with stmt %a (%d)"
Project.pretty (Project.current ())
Code_annotation.pretty ca
Stmt.pretty stmt
stmt.sid;*)
let kf = find_englobing_kf ?kf stmt in
- let convert a =
- match a.annot_content with
- | AAssert(l, kind, p) ->
- let a = { a with annot_content=AAssert(l,kind,extend_name emitter p) } in
- a, Property.ip_of_code_annot kf stmt a
- | AInvariant(l, b, p) ->
- let a={a with annot_content=AInvariant(l,b,extend_name emitter p)} in
- a, Property.ip_of_code_annot kf stmt a
- | AStmtSpec (bhvs, spec) ->
- let filter ca =
- match ca.annot_content with
- | AStmtSpec(bhvs',_) -> is_same_behavior_set bhvs bhvs'
- | _ -> false
- in
- let contract = code_annot ~filter stmt in
- (match contract with
- | [] -> a, Property.ip_of_code_annot kf stmt a
- | [ { annot_content = AStmtSpec _ } ] ->
- let register_children = true in
- let active = bhvs in
- add_behaviors
- ~register_children emitter kf ~stmt ~active spec.spec_behavior;
- if spec.spec_variant <> None then
- Kernel.fatal
- "statement contract cannot have a decrease clause";
- Extlib.may
- (add_terminates emitter kf ~stmt ~active) spec.spec_terminates;
- List.iter
- (add_complete emitter kf ~stmt ~active)
- spec.spec_complete_behaviors;
- List.iter
- (add_disjoint emitter kf ~stmt ~active)
- spec.spec_disjoint_behaviors;
- (* By construction, we have exactly one contract
- corresponding to our criterion and emitter. *)
- let ca = List.hd (code_annot ~emitter ~filter stmt) in
- (* remove the previous binding in order to replace it
- with the updated one. Statuses being attached to sub-elements
- of the contract, they do not need any update here.
- *)
- remove_code_annot_internal emitter ~remove_statuses:false ~kf stmt ca;
- { a with annot_content = ca.annot_content }, []
- | _ ->
- Kernel.fatal
- "more than one contract attached to a given statement for \
- emitter %a. Invariant of annotations management broken."
- Emitter.pretty emitter)
- | AVariant _ ->
- let v = code_annot ~filter:Logic_utils.is_variant stmt in
- (match v with
- | [] -> a, Property.ip_of_code_annot kf stmt a
- | _ ->
- let source = fst (Cil_datatype.Stmt.loc stmt) in
- Kernel.fatal ~source
- "trying to register a second variant for statement %a"
- Stmt.pretty stmt)
- | AAssigns (bhvs, assigns) ->
- let filter ca =
- match ca.annot_content with
- | AAssigns (bhvs', _) -> is_same_behavior_set bhvs bhvs'
- | _ -> false
- in
- let assigns' = code_annot ~filter stmt in
- (match assigns' with
- | [] -> a, Property.ip_of_code_annot kf stmt a
- | l ->
- let merge_assigns_ca acc ca =
- match ca.annot_content with
- | AAssigns(_,assigns') ->
- merge_assigns ~keep_empty:false assigns' acc
- | _ -> acc
- in
- let assigns' = List.fold_left merge_assigns_ca WritesAny l in
- let merged_ca = { a with annot_content = AAssigns(bhvs,assigns') }
- in
- let ip =
- Property.(
- ip_of_assigns
- kf (Kstmt stmt) (Id_loop merged_ca) assigns')
- in
- Extlib.may Property_status.remove ip;
- (match assigns' with
- | WritesAny -> ()
- | Writes l ->
- List.iter
- (fun from ->
- let ip =
- Property.(
- ip_of_from kf (Kstmt stmt)
- (Id_loop merged_ca) from)
- in
- Extlib.may Property_status.remove ip)
- l);
- let new_assigns =
- merge_assigns ~keep_empty:false assigns' assigns
- in
- let new_ca = { a with annot_content = AAssigns(bhvs,new_assigns) }
- in
- let ips =
- Extlib.list_of_opt
- Property.(
- ip_of_assigns
- kf (Kstmt stmt) (Id_loop new_ca) new_assigns)
- in
- let ips =
- match new_assigns with
- | WritesAny -> ips
- | Writes l ->
- List.fold_left
- (fun acc f ->
- Extlib.opt_fold
- (fun x y -> x::y)
- Property.(
- ip_of_from kf (Kstmt stmt)
- (Id_loop new_ca) f)
- acc)
- ips l
- in
- let ca' = code_annot ~filter stmt in
- let new_a =
- match ca' with
- | [] -> a
- | [ { annot_content = AAssigns(_, assigns') } as ca ] ->
- remove_code_annot_internal emitter ~kf stmt ca;
- let merged =
- merge_assigns ~keep_empty:false assigns' assigns
- in
- { a with annot_content = AAssigns (bhvs, merged) }
- | _ ->
- Kernel.fatal
- "More than one loop assigns clause for a statement. \
- Annotations internal state broken."
- in
- new_a, ips)
- | AAllocation (bhvs, alloc) ->
- let filter ca =
- match ca.annot_content with
- | AAllocation(bhvs',_) -> is_same_behavior_set bhvs bhvs'
- | _ -> false
- in
- (match code_annot ~filter stmt with
- | [] -> a, Property.ip_of_code_annot kf stmt a
- | l ->
- let merge_alloc_ca acc alloc =
- match alloc.annot_content with
- | AAllocation(_,a) -> merge_allocation ~keep_empty:false acc a
- | _ -> acc
- in
- let alloc' = List.fold_left merge_alloc_ca FreeAllocAny l in
- let merged_a =
- { a with annot_content = AAllocation(bhvs,alloc') }
- in
- let ip =
- Property.(
- ip_of_allocation kf (Kstmt stmt)
- (Id_loop merged_a) alloc')
- in
- Extlib.may Property_status.remove ip;
- let new_alloc = merge_allocation ~keep_empty:false alloc' alloc in
- let new_a =
- { a with annot_content = AAllocation(bhvs,new_alloc) }
- in
- let ip =
- Property.(
- ip_of_allocation
- kf (Kstmt stmt) (Id_loop new_a) new_alloc)
- in
- let emit_a =
- match code_annot ~emitter ~filter stmt with
- | [] -> a
- | [ { annot_content = AAllocation(_,alloc') } as ca ] ->
- remove_code_annot_internal emitter ~kf stmt ca;
- { a with annot_content =
- AAllocation(
- bhvs,
- merge_allocation ~keep_empty:false alloc' alloc) }
- | _ ->
- Kernel.fatal
- "More than one allocation clause for a statement. \
- Annotations internal state broken"
- in
- emit_a, Extlib.list_of_opt ip)
- | APragma _ | AExtended _ -> a, Property.ip_of_code_annot kf stmt a
- in
- let ca, ppts = convert ca in
- let e = Emitter.get emitter in
- List.iter Property_status.register ppts;
- let add_emitter tbl = Emitter.Usable_emitter.Hashtbl.add tbl e (ref [ ca ]) in
- try
- let tbl = Code_annots.find stmt in
+ let fill_tables ca ppts =
+ let e = Emitter.get emitter in
+ List.iter Property_status.register ppts;
+ let add_emitter tbl =
+ Emitter.Usable_emitter.Hashtbl.add tbl e (ref [ ca ]) in
try
- let l = Emitter.Usable_emitter.Hashtbl.find tbl e in
- l := ca :: !l;
+ let tbl = Code_annots.find stmt in
+ try
+ let l = Emitter.Usable_emitter.Hashtbl.find tbl e in
+ l := ca :: !l;
+ with Not_found ->
+ add_emitter tbl
with Not_found ->
- add_emitter tbl
- with Not_found ->
- let tbl = Emitter.Usable_emitter.Hashtbl.create 7 in
- add_emitter tbl;
- Code_annots.add stmt tbl
+ let tbl = Emitter.Usable_emitter.Hashtbl.create 7 in
+ add_emitter tbl;
+ Code_annots.add stmt tbl
+ in
+ match ca.annot_content with
+ | AAssert(l, kind, p) ->
+ let a = { ca with annot_content=AAssert(l,kind,extend_name emitter p) } in
+ fill_tables a (Property.ip_of_code_annot kf stmt a)
+ | AInvariant(l, b, p) ->
+ let a={ca with annot_content=AInvariant(l,b,extend_name emitter p)} in
+ fill_tables a (Property.ip_of_code_annot kf stmt a)
+ | AStmtSpec (bhvs, spec) ->
+ let filter ca =
+ match ca.annot_content with
+ | AStmtSpec(bhvs',_) -> is_same_behavior_set bhvs bhvs'
+ | _ -> false
+ in
+ let contract = code_annot ~filter stmt in
+ (match contract with
+ | [] ->
+ if not (keep_empty && Logic_utils.funspec_has_only_assigns spec) then
+ fill_tables ca (Property.ip_of_code_annot kf stmt ca)
+ | [ { annot_content = AStmtSpec _ } ] ->
+ let register_children = true in
+ let active = bhvs in
+ add_behaviors
+ ~register_children emitter kf ~stmt ~active spec.spec_behavior;
+ if spec.spec_variant <> None then
+ Kernel.fatal
+ "statement contract cannot have a decrease clause";
+ Extlib.may
+ (add_terminates emitter kf ~stmt ~active) spec.spec_terminates;
+ List.iter
+ (add_complete emitter kf ~stmt ~active)
+ spec.spec_complete_behaviors;
+ List.iter
+ (add_disjoint emitter kf ~stmt ~active)
+ spec.spec_disjoint_behaviors;
+ (* By construction, we have exactly one contract
+ corresponding to our criterion and emitter. *)
+ let ca' = List.hd (code_annot ~emitter ~filter stmt) in
+ (* remove the previous binding in order to replace it
+ with the updated one. Statuses being attached to sub-elements
+ of the contract, they do not need any update here.
+ *)
+ remove_code_annot_internal emitter ~remove_statuses:false ~kf stmt ca';
+ fill_tables ca' []
+ | _ ->
+ Kernel.fatal
+ "more than one contract attached to a given statement for \
+ emitter %a. Invariant of annotations management broken."
+ Emitter.pretty emitter)
+ | AVariant _ ->
+ let v = code_annot ~filter:Logic_utils.is_variant stmt in
+ (match v with
+ | [] -> fill_tables ca (Property.ip_of_code_annot kf stmt ca)
+ | _ ->
+ let source = fst (Cil_datatype.Stmt.loc stmt) in
+ Kernel.fatal ~source
+ "trying to register a second variant for statement %a"
+ Stmt.pretty stmt)
+ | AAssigns (bhvs, assigns) ->
+ let filter_ca ca =
+ match ca.annot_content with
+ | AAssigns (bhvs', _) -> is_same_behavior_set bhvs bhvs'
+ | _ -> false
+ in
+ let filter e ca = Emitter.equal e emitter && filter_ca ca in
+ let ca_e = code_annot_emitter ~filter stmt in
+ let ca_total = code_annot ~filter:filter_ca stmt in
+ (match ca_total with
+ | [] when keep_empty -> ()
+ | [] -> fill_tables ca (Property.ip_of_code_annot kf stmt ca)
+ | [{ annot_content = AAssigns(_,assigns_total)}] ->
+ let assigns_e =
+ match ca_e with
+ | [] -> WritesAny
+ | [ { annot_content = AAssigns(_, assigns') } as ca,_ ] ->
+ remove_code_annot_internal emitter ~kf stmt ca;
+ assigns'
+ | _ ->
+ Kernel.fatal
+ "More than one loop assigns clause for a statement. \
+ Annotations internal state broken."
+ in
+ (* we have assigns at statement level, just not from this
+ emitter yet, hence merge at emitter level regardless of keep_empty *)
+ let merged_e = merge_assigns ~keep_empty:false assigns_e assigns in
+ let new_a = { ca with annot_content = AAssigns(bhvs,merged_e) } in
+ let merged_total = merge_assigns ~keep_empty assigns_total assigns in
+ let ips =
+ Property.ip_of_code_annot kf stmt
+ { ca with annot_content = AAssigns(bhvs,merged_total) }
+ in
+ fill_tables new_a ips
+ | _ ->
+ Kernel.fatal
+ "More than one loop assigns clause for a statement. \
+ Annotations internal state broken.")
+ | AAllocation (bhvs, alloc) ->
+ let filter_ca ca =
+ match ca.annot_content with
+ | AAllocation(bhvs',_) -> is_same_behavior_set bhvs bhvs'
+ | _ -> false
+ in
+ let filter e ca = Emitter.equal e emitter && filter_ca ca in
+ let ca_e = code_annot_emitter ~filter stmt in
+ let ca_total = code_annot ~filter:filter_ca stmt in
+ (match ca_total with
+ | [] when keep_empty -> ()
+ | [] -> fill_tables ca (Property.ip_of_code_annot kf stmt ca)
+ | [{ annot_content = AAllocation(_,alloc_total)}] ->
+ let alloc_e =
+ match ca_e with
+ | [] -> FreeAllocAny
+ | [ { annot_content = AAllocation(_, alloc') } as ca,_ ] ->
+ remove_code_annot_internal emitter ~kf stmt ca;
+ alloc'
+ | _ ->
+ Kernel.fatal
+ "More than one loop assigns clause for a statement. \
+ Annotations internal state broken."
+ in
+ (* we have assigns at statement level, just not from this
+ emitter yet, hence merge at emitter level regardless of keep_empty *)
+ let merged_e = merge_allocation ~keep_empty:false alloc_e alloc in
+ let new_a = { ca with annot_content = AAllocation(bhvs,merged_e) } in
+ let merged_total = merge_allocation ~keep_empty alloc_total alloc in
+ let ips =
+ Property.ip_of_code_annot kf stmt
+ { ca with annot_content = AAllocation(bhvs,merged_total) }
+ in
+ fill_tables new_a ips
+ | _ ->
+ Kernel.fatal
+ "More than one loop assigns clause for a statement. \
+ Annotations internal state broken.")
+ | APragma _ | AExtended _ ->
+ fill_tables ca (Property.ip_of_code_annot kf stmt ca)
let add_assert e ?kf stmt a =
let a = Logic_const.new_code_annotation (AAssert ([],Assert,a)) in
diff --git a/src/kernel_services/ast_data/annotations.mli b/src/kernel_services/ast_data/annotations.mli
index 1b65f10d2efddf9672f05edb67d95f407c459c3c..4bc65d57621c0a9b55781d84375b210e71206629 100644
--- a/src/kernel_services/ast_data/annotations.mli
+++ b/src/kernel_services/ast_data/annotations.mli
@@ -261,6 +261,7 @@ val fold_decreases:
(**************************************************************************)
val add_code_annot:
+ ?keep_empty:bool ->
Emitter.t -> ?kf:kernel_function -> stmt -> code_annotation -> unit
(** Add a new code annotation attached to the given statement. If [kf] is
provided, the function runs faster.
@@ -270,9 +271,16 @@ val add_code_annot:
Trying to associate more than one will result in a merge of the contracts.
The same things happens with loop assigns and allocates/frees.
+ The [keep_empty] argument is only used for loop assigns
+ and loop allocates, where it is used to decide whether to add the given
+ code annot in case the corresponding category was empty. It defaults to
+ [true], which is sound wrt ACSL semantics of equating an absence of
+ annotation with assigns/allocates \everything.
There can be at most one loop variant registered per statement.
Attempting to register a second one will result in a fatal error.
+
+ @modify Frama-C+dev: add keep_empty argument
*)
val add_assert:
diff --git a/src/kernel_services/ast_queries/file.ml b/src/kernel_services/ast_queries/file.ml
index 676c7dbcf56e4c289c1ed465dc7d0b46cebce977..412c945293053724d86025b26b3ebab33b0905ce 100644
--- a/src/kernel_services/ast_queries/file.ml
+++ b/src/kernel_services/ast_queries/file.ml
@@ -701,7 +701,7 @@ let emit_all_statuses _ =
let () = Ast.apply_after_computed emit_all_statuses
let add_annotation kf st a =
- Annotations.add_code_annot Emitter.end_user ~kf st a;
+ Annotations.add_code_annot ~keep_empty:false Emitter.end_user ~kf st a;
(* Now check if the annotation is valid by construction
(provided normalization is correct). *)
match a.annot_content with
@@ -741,7 +741,7 @@ let synchronize_source_annot has_new_stmt kf =
st_ann.skind <- (Block (Cil.mkBlockNonScoping [st]));
has_new_stmt := true;
Annotations.add_code_annot
- Emitter.end_user ~kf st_ann annot;
+ ~keep_empty:false Emitter.end_user ~kf st_ann annot;
(true, st_ann)
end else begin
add_annotation kf st annot;
diff --git a/src/kernel_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml
index 242feb6c6a054e09f4016d0168be57a3e4a9c38f..bf0b1e828dbf5c66679c255ebaf1c2e306b066c2 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -676,6 +676,18 @@ let rec add_attribute_glob_annot a g =
| Dcustom_annot(c,n,al,l) -> Dcustom_annot(c,n,Cil.addAttribute a al, l)
| Dextended (e,al,l) -> Dextended(e,Cil.addAttribute a al,l)
+let behavior_has_only_assigns bhvs =
+ bhvs.b_requires = [] && bhvs.b_assumes = [] &&
+ bhvs.b_post_cond = [] && bhvs.b_allocation = FreeAllocAny &&
+ bhvs.b_extended = []
+
+let funspec_has_only_assigns spec =
+ List.for_all behavior_has_only_assigns spec.spec_behavior &&
+ spec.spec_variant = None &&
+ spec.spec_terminates = None &&
+ spec.spec_complete_behaviors = [] &&
+ spec.spec_disjoint_behaviors = []
+
let is_same_list f l1 l2 =
try List.for_all2 f l1 l2 with Invalid_argument _ -> false
diff --git a/src/kernel_services/ast_queries/logic_utils.mli b/src/kernel_services/ast_queries/logic_utils.mli
index 1394e8408fbb3f58bf5200c5413f5dd934ca236c..b1e4074364ff4216e5558b9c7b449678405f7df5 100644
--- a/src/kernel_services/ast_queries/logic_utils.mli
+++ b/src/kernel_services/ast_queries/logic_utils.mli
@@ -312,6 +312,18 @@ val is_annot_next_stmt: code_annotation -> bool
val add_attribute_glob_annot:
attribute -> global_annotation -> global_annotation
+(** {2 Contracts } *)
+
+(** [true] if the behavior has only an assigns clause.
+ @since Frama-C+dev
+*)
+val behavior_has_only_assigns: behavior -> bool
+
+(** [true] if the only non-empty fields of the contract are assigns clauses
+ @since Frama-C+dev
+*)
+val funspec_has_only_assigns: funspec -> bool
+
(** {2 Structural equality between annotations} *)
val is_same_list: ('a -> 'a -> bool) -> 'a list -> 'a list -> bool
diff --git a/src/kernel_services/ast_transformations/inline.ml b/src/kernel_services/ast_transformations/inline.ml
index 36adae8427fe37790298e9a576b3e4847eaba0a6..b50798b0e70b5fa79be73f4ff36a9cd19e35fbc3 100644
--- a/src/kernel_services/ast_transformations/inline.ml
+++ b/src/kernel_services/ast_transformations/inline.ml
@@ -123,7 +123,7 @@ let inline_call loc caller callee return args =
fd.sbody.bstmts <- inits @ fd.sbody.bstmts;
end else begin
(* put a statement contract on top of the function's body,
- but only after we have assigned the formals. Not that there
+ but only after we have assigned the formals. Note that there
is no need to rename behaviors: they will only shadow behaviors
of the caller within callee's body, just as we need.
*)
diff --git a/src/kernel_services/visitors/visitor.ml b/src/kernel_services/visitors/visitor.ml
index ce00bb69329b5755fcc162379f73ecaa3ce86d8e..cc918e122f511db3fe8acf500aaaa9c701204b9f 100644
--- a/src/kernel_services/visitors/visitor.ml
+++ b/src/kernel_services/visitors/visitor.ml
@@ -124,7 +124,8 @@ object(self)
remove;
List.iter
(fun (e, a) ->
- Annotations.add_code_annot e ~kf:new_kf stmt a)
+ Annotations.add_code_annot
+ ~keep_empty:false e ~kf:new_kf stmt a)
add)
self#get_filling_actions
end
diff --git a/src/plugins/aorai/aorai_visitors.ml b/src/plugins/aorai/aorai_visitors.ml
index 004941db6742cd482c8910fc0e7a1d3f3d0f197a..7ce63778b530c98bf41e20013662ec11946bf0c9 100644
--- a/src/plugins/aorai/aorai_visitors.ml
+++ b/src/plugins/aorai/aorai_visitors.ml
@@ -272,7 +272,10 @@ let update_loop_assigns kf stmt state vi code_annot =
(AAssigns (bhvs, Logic_utils.concat_assigns old_assigns assigns))
| _ -> Aorai_option.fatal "Expecting an assigns clause here"
in
- Annotations.add_code_annot Aorai_option.emitter ~kf stmt new_assigns
+ (* we're putting the annotation on a new statement, with an empty
+ loop assigns by construction. Don't keep_empty *)
+ Annotations.add_code_annot
+ ~keep_empty:false Aorai_option.emitter ~kf stmt new_assigns
let get_action_post_cond kf ?init_trans return_states =
let to_consider pre_state int_states =
diff --git a/src/plugins/aorai/tests/aorai/oracle/assigns.0.res.oracle b/src/plugins/aorai/tests/aorai/oracle/assigns.0.res.oracle
index 6c66a3027f5e460bd9c2f940af4e5161e5b44de4..ef6224bb447e03550381c8c205c6feb41da0f37e 100644
--- a/src/plugins/aorai/tests/aorai/oracle/assigns.0.res.oracle
+++ b/src/plugins/aorai/tests/aorai/oracle/assigns.0.res.oracle
@@ -275,8 +275,8 @@ int main(void)
/*@ ghost main_pre_func(); */
/*@ assigns X; */
X ++;
- /*@ assigns aorai_CurOpStatus, aorai_CurOperation, S1, S2, S_in_f, Sf,
- in_main, X;
+ /*@ assigns X, aorai_CurOpStatus, aorai_CurOperation, S1, S2, S_in_f, Sf,
+ in_main;
*/
f();
/*@ ghost main_post_func(X); */
diff --git a/src/plugins/aorai/tests/aorai/oracle/assigns.1.res.oracle b/src/plugins/aorai/tests/aorai/oracle/assigns.1.res.oracle
index 2434556b05d580bac96d12dfa195f2e84cc9ee09..7e00479c453e3e785b4726a59de9906430c04c39 100644
--- a/src/plugins/aorai/tests/aorai/oracle/assigns.1.res.oracle
+++ b/src/plugins/aorai/tests/aorai/oracle/assigns.1.res.oracle
@@ -213,7 +213,7 @@ int main(void)
/*@ ghost main_pre_func(); */
/*@ assigns X; */
X ++;
- /*@ assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates, X; */
+ /*@ assigns X, aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates; */
f();
/*@ ghost main_post_func(X); */
return X;
diff --git a/src/plugins/e-acsl/src/code_generator/label.ml b/src/plugins/e-acsl/src/code_generator/label.ml
index 9225fdb571810e50ef40d96f5953ffa23cf573aa..f06c2232dfc45e230fda88c989d10349a949426d 100644
--- a/src/plugins/e-acsl/src/code_generator/label.ml
+++ b/src/plugins/e-acsl/src/code_generator/label.ml
@@ -48,7 +48,7 @@ let move kf ~old new_stmt =
List.iter
(fun (e, ca) ->
Annotations.remove_code_annot ~kf e old ca;
- Annotations.add_code_annot ~kf e new_stmt ca)
+ Annotations.add_code_annot ~keep_empty:false ~kf e new_stmt ca)
l;
(* update the gotos of the function jumping to one of the labels *)
let f =
diff --git a/tests/spec/loop_assigns_generated.i b/tests/spec/loop_assigns_generated.i
index 79fba31ec9f994b9302948f03a58372f3ec0ab71..f85c8c5a1ccec3e842a459fe4f1df20aee349285 100644
--- a/tests/spec/loop_assigns_generated.i
+++ b/tests/spec/loop_assigns_generated.i
@@ -7,4 +7,6 @@ void f() {
int i = 0;
/*@ loop assigns i; */
while (i< 10) { i++; }
+
+ while (i>0) { i--; }
}
diff --git a/tests/spec/loop_assigns_generated.ml b/tests/spec/loop_assigns_generated.ml
index 30d64b3ffebd318e7ce1585b73f21428fc2e389e..7e9340737ab5ed66e19981bec6e1ba8d3d2b5de8 100644
--- a/tests/spec/loop_assigns_generated.ml
+++ b/tests/spec/loop_assigns_generated.ml
@@ -3,7 +3,7 @@ open Cil_types
let e1 = Emitter.(create "emitter1" [ Code_annot ] [] [])
let e2 = Emitter.(create "emitter2" [ Code_annot ] [] [])
-let add_assigns e kf stmt v =
+let mk_assigns e v =
let lv = Cil.cvar_to_lvar v in
let term_v = Logic_const.tvar lv in
let named_term_v =
@@ -11,12 +11,15 @@ let add_assigns e kf stmt v =
term_name = ("added_by_"^(Emitter.get_name e))::term_v.term_name }
in
let id_v = Logic_const.new_identified_term named_term_v in
- Annotations.add_code_annot e ~kf stmt
+ Writes[id_v,FromAny]
+
+let add_assigns ?(keep_empty=false) e kf stmt v =
+ Annotations.add_code_annot ~keep_empty e ~kf stmt
(Logic_const.new_code_annotation
- (AAssigns ([], Writes [id_v, FromAny])));
+ (AAssigns ([], mk_assigns e v)));
Filecheck.check_ast ("after insertion of loop assigns " ^ v.vname)
-let add_allocates e kf stmt v =
+let mk_allocates e v =
let lv = Cil.cvar_to_lvar v in
let term_v = Logic_const.tvar lv in
let named_term_v =
@@ -24,11 +27,23 @@ let add_allocates e kf stmt v =
term_name = ("added_by_"^(Emitter.get_name e))::term_v.term_name }
in
let id_v = Logic_const.new_identified_term named_term_v in
- Annotations.add_code_annot e ~kf stmt
- (Logic_const.new_code_annotation
- (AAllocation([],FreeAlloc ([],[id_v]))));
+ FreeAlloc ([],[id_v])
+
+let add_allocates ?(keep_empty=false) e kf stmt v =
+ Annotations.add_code_annot ~keep_empty e ~kf stmt
+ (Logic_const.new_code_annotation (AAllocation([],mk_allocates e v)));
Filecheck.check_ast ("after insertion of loop allocates " ^ v.vname )
+let check_only_one f =
+ let seen = ref false in
+ fun _ a ->
+ if f a then begin
+ assert (not !seen);
+ seen := true
+ end
+
+let filter_category f _ a acc = if f a then a :: acc else acc
+
let main () =
Ast.compute();
let kf = Globals.Functions.find_by_name "f" in
@@ -37,14 +52,44 @@ let main () =
List.find
(fun s -> match s.skind with Loop _ -> true | _ -> false) def.sallstmts
in
+ let s2 =
+ List.find
+ (fun s' -> s!=s' && (match s'.skind with Loop _ -> true | _ -> false))
+ def.sallstmts
+ in
+ let s3 = Kernel_function.find_return kf in
let j = Cil.makeLocalVar def ~insert:true "j" Cil.intType in
let k = Cil.makeLocalVar def ~insert:true "k" Cil.intType in
+ let l = Cil.makeLocalVar def ~insert:true "l" Cil.intType in
let p = Cil.makeLocalVar def ~insert:true "p" Cil.intPtrType in
let q = Cil.makeLocalVar def ~insert:true "q" Cil.intPtrType in
+ let r = Cil.makeLocalVar def ~insert:true "r" Cil.intPtrType in
add_assigns e1 kf s j;
add_assigns e2 kf s k;
+ add_assigns e1 kf s l;
+ add_assigns ~keep_empty:true e2 kf s2 j;
+ Annotations.add_assigns ~keep_empty:true e1 kf ~stmt:s3 (mk_assigns e1 k);
add_allocates e1 kf s p;
add_allocates e2 kf s q;
+ add_allocates e1 kf s r;
+ add_allocates ~keep_empty:true e2 kf s2 p;
+ Annotations.add_allocates ~keep_empty:true e1 kf ~stmt:s3 (mk_allocates e1 k);
+ Annotations.iter_code_annot (check_only_one Logic_utils.is_assigns) s;
+ Annotations.iter_code_annot (check_only_one Logic_utils.is_allocation) s;
+ let lassigns =
+ Annotations.fold_code_annot (filter_category Logic_utils.is_assigns) s []
+ in
+ assert (List.length lassigns = 1);
+ let lalloc =
+ Annotations.fold_code_annot (filter_category Logic_utils.is_allocation) s []
+ in
+ assert (List.length lalloc = 1);
+ ignore
+ (Property_status.get
+ (Property.ip_of_code_annot_single kf s (List.hd lassigns)));
+ ignore
+ (Property_status.get
+ (Property.ip_of_code_annot_single kf s (List.hd lalloc)));
File.pretty_ast ()
let () = Db.Main.extend main
diff --git a/tests/spec/oracle/assigns_array.res.oracle b/tests/spec/oracle/assigns_array.res.oracle
index 778268bcc22bfd3fab2ede1fbea4c8539be364f5..6e4846e218d9c35e30edec7a74b34aa5e7f1492c 100644
--- a/tests/spec/oracle/assigns_array.res.oracle
+++ b/tests/spec/oracle/assigns_array.res.oracle
@@ -36,8 +36,8 @@ int h(int reset, int n)
int i;
int r = 0;
i = 0;
- /*@ for bar: loop assigns \nothing;
- for foo: loop assigns Tab[0 .. i]; */
+ /*@ for foo: loop assigns Tab[0 .. i];
+ for bar: loop assigns \nothing; */
while (i < n) {
r += Tab[i];
if (reset) Tab[i] = 0;
diff --git a/tests/spec/oracle/bts0578.res.oracle b/tests/spec/oracle/bts0578.res.oracle
index f25516888c6bafe4e5e1910dfa516174a2f9c2d2..7c6d8517d86a1a289b4f02db5da2cf00e985955e 100644
--- a/tests/spec/oracle/bts0578.res.oracle
+++ b/tests/spec/oracle/bts0578.res.oracle
@@ -7,11 +7,11 @@ void main(void)
int i;
int t[10];
i = 0;
- /*@ loop invariant \true;
- loop assigns t[0 .. i];
+ /*@ loop assigns t[0 .. i];
+ loop invariant \true;
+ for foo: loop assigns t[0 .. i];
for foo: loop invariant \true;
for foo: loop invariant \true;
- for foo: loop assigns t[0 .. i];
loop variant 0;
*/
while (i < 10) {
diff --git a/tests/spec/oracle/loop_assigns_generated.res.oracle b/tests/spec/oracle/loop_assigns_generated.res.oracle
index a30771642fda30636515438444f889311c81bf84..64f6610b539d47a1612fa69853c4760b6970cae5 100644
--- a/tests/spec/oracle/loop_assigns_generated.res.oracle
+++ b/tests/spec/oracle/loop_assigns_generated.res.oracle
@@ -2,15 +2,20 @@
/* Generated by Frama-C */
void f(void)
{
+ int *r;
int *q;
int *p;
+ int l;
int k;
int j;
int i = 0;
- /*@ loop allocates (added_by_emitter1: p), (added_by_emitter2: q);
- loop assigns i, (added_by_emitter1: j), (added_by_emitter2: k);
+ /*@ loop assigns i, (added_by_emitter1: j), (added_by_emitter1: l),
+ (added_by_emitter2: k);
+ loop allocates
+ (added_by_emitter1: p), (added_by_emitter1: r), (added_by_emitter2: q);
*/
while (i < 10) i ++;
+ while (i > 0) i --;
return;
}
diff --git a/tests/syntax/oracle/asm_with_contracts.res.oracle b/tests/syntax/oracle/asm_with_contracts.res.oracle
index de45604755bf733ffeb4e6885baede947f7b9fb3..aab309b2eeb8fce6f14a24fcacbb3bd5d283cdc1 100644
--- a/tests/syntax/oracle/asm_with_contracts.res.oracle
+++ b/tests/syntax/oracle/asm_with_contracts.res.oracle
@@ -9,9 +9,9 @@ int f(int z)
int y = 2;
/*@ assigns y; */
__asm__ ("mov %1, %0\n\t" : "=r" (y) : "r" (x));
+ /*@ for b: assigns x, y; */
/*@ assigns x;
assigns x \from y; */
- /*@ for b: assigns x, y; */
__asm__ ("mov %1, %0\n\t" : "=r" (x) : "r" (y));
/*@ assigns x, y;