Commit c49edb0b authored by Boris Yakobowski's avatar Boris Yakobowski
Browse files

Update w.r.t. corresponding kernel branch

parent b0f5f13a
......@@ -59,7 +59,7 @@ type t =
env_stack: local_env list;
init_env: local_env;
var_mapping: Varinfo.t Logic_var.Map.t; (* bind logic var to C var *)
loop_invariants: predicate named list list;
loop_invariants: predicate list list;
(* list of loop invariants for each currently visited loops *)
cpt: int; (* counter used when generating variables *) }
......
......@@ -66,7 +66,7 @@ module Logic_binding: sig
val remove: t -> logic_var -> t
end
val add_assert: t -> stmt -> predicate named -> unit
val add_assert: t -> stmt -> predicate -> unit
(** [add_assert env s p] associates the assertion [p] to the statement [s] in
the environment [env]. *)
......@@ -119,8 +119,8 @@ val set_annotation_kind: t -> Misc.annotation_kind -> t
(* ************************************************************************** *)
val push_loop: t -> t
val add_loop_invariant: t -> predicate named -> t
val pop_loop: t -> predicate named list * t
val add_loop_invariant: t -> predicate -> t
val pop_loop: t -> predicate list * t
(* ************************************************************************** *)
(** {2 RTEs} *)
......
......@@ -191,7 +191,7 @@ let predicate_to_exp =
~journalize:false
"predicate_to_exp"
(Datatype.func2
Kernel_function.ty Cil_datatype.Predicate_named.ty Cil_datatype.Exp.ty)
Kernel_function.ty Cil_datatype.Predicate.ty Cil_datatype.Exp.ty)
Translate.predicate_to_exp
let add_e_acsl_library _files =
......
......@@ -143,10 +143,10 @@ let mk_gen_name name =
(* Build a C conditional doing a runtime assertion check. *)
let mk_e_acsl_guard ?(reverse=false) kind kf e p =
let loc = p.loc in
let loc = p.pred_loc in
let msg =
Kernel.Unicode.without_unicode
(Pretty_utils.sfprintf "%a@?" Printer.pp_predicate_named) p
(Pretty_utils.sfprintf "%a@?" Printer.pp_predicate) p
in
let line = (fst loc).Lexing.pos_lnum in
let e =
......@@ -267,4 +267,4 @@ let term_addr_of ~loc tlv ty =
Local Variables:
compile-command: "make"
End:
*)
\ No newline at end of file
*)
......@@ -46,7 +46,7 @@ type annotation_kind =
| RTE
val mk_e_acsl_guard:
?reverse:bool -> annotation_kind -> kernel_function -> exp -> predicate named
?reverse:bool -> annotation_kind -> kernel_function -> exp -> predicate
-> stmt
val mk_block: Project.t -> stmt -> block -> stmt
......@@ -111,4 +111,4 @@ val is_generated_kf: kernel_function -> bool
Local Variables:
compile-command: "make"
End:
*)
\ No newline at end of file
*)
......@@ -309,7 +309,7 @@ module rec Transfer
let register_object kf state_ref = object
inherit Visitor.frama_c_inplace
method !vpredicate = function
method !vpredicate_node = function
| Pvalid(_, t) | Pvalid_read(_, t) | Pvalid_function t
| Pinitialized(_, t) | Pfreeable(_, t) ->
(* Options.feedback "REGISTER %a" Cil.d_term t;*)
......
......@@ -24,8 +24,8 @@ open Cil_types
open Cil
open Cil_datatype
let named_predicate_to_exp_ref
: (kernel_function -> Env.t -> predicate named -> exp * Env.t) ref
let predicate_to_exp_ref
: (kernel_function -> Env.t -> predicate -> exp * Env.t) ref
= Extlib.mk_fun "named_predicate_to_exp_ref"
let term_to_exp_ref
......@@ -37,7 +37,7 @@ let compute_quantif_guards quantif bounded_vars hyps =
let msg1 = Pretty_utils.sfprintf msg pp x in
let msg2 =
Pretty_utils.sfprintf "@[ in quantification@ %a@]"
Printer.pp_predicate_named quantif
Printer.pp_predicate quantif
in
Error.untypable (msg1 ^ msg2)
in
......@@ -58,8 +58,8 @@ let compute_quantif_guards quantif bounded_vars hyps =
else error "@[invalid binder %a@]" Printer.pp_term t
| _ -> error "@[invalid binder %a@]" Printer.pp_term t
in
let rec parse acc vars p = match p.content with
| Pand(p, { content = Prel((Rlt | Rle) as r, t1, t2) }) ->
let rec parse acc vars p = match p.pred_content with
| Pand(p, { pred_content = Prel((Rlt | Rle) as r, t1, t2) }) ->
(* && is left-associative in the AST *)
let acc, partial, vars = parse acc vars p in
(match partial with
......@@ -82,7 +82,7 @@ let compute_quantif_guards quantif bounded_vars hyps =
| Prel((Rlt | Rle) as r, t1, t2) ->
(* left-most predicate: the searched variable is [t2] *)
left_term acc vars (t1, r) t2
| _ -> error "@[invalid guard %a@]" Printer.pp_predicate_named p
| _ -> error "@[invalid guard %a@]" Printer.pp_predicate p
in
let acc, partial, vars = parse [] bounded_vars hyps in
(match partial with
......@@ -100,7 +100,7 @@ let compute_quantif_guards quantif bounded_vars hyps =
List.iter
(fun v -> Format.fprintf fmt "@[%a @]" Printer.pp_logic_var v)
vars)
Printer.pp_predicate_named quantif
Printer.pp_predicate quantif
in
Error.untypable msg);
List.rev acc
......@@ -119,7 +119,7 @@ let convert kf env loc is_forall p bounded_vars hyps goal =
if is_forall then o, z, (fun x -> x)
else z, o, (fun e -> new_exp ~loc:e.eloc (UnOp(LNot, e, intType)))
in
let named_predicate_to_exp = !named_predicate_to_exp_ref in
let named_predicate_to_exp = !predicate_to_exp_ref in
let term_to_exp = !term_to_exp_ref in
(* universal quantification over integers (or a subtype of integer) *)
let guards = compute_quantif_guards p bounded_vars hyps in
......@@ -281,12 +281,12 @@ let convert kf env loc is_forall p bounded_vars hyps goal =
res, env
let quantif_to_exp kf env p =
let loc = p.loc in
match p.content with
| Pforall(bounded_vars, { content = Pimplies(hyps, goal) }) ->
let loc = p.pred_loc in
match p.pred_content with
| Pforall(bounded_vars, { pred_content = Pimplies(hyps, goal) }) ->
convert kf env loc true p bounded_vars hyps goal
| Pforall _ -> Error.not_yet "unguarded \\forall quantification"
| Pexists(bounded_vars, { content = Pand(hyps, goal) }) ->
| Pexists(bounded_vars, { pred_content = Pand(hyps, goal) }) ->
convert kf env loc false p bounded_vars hyps goal
| Pexists _ -> Error.not_yet "unguarded \\exists quantification"
| _ -> assert false
......
......@@ -24,15 +24,15 @@
open Cil_types
val quantif_to_exp: kernel_function -> Env.t -> predicate named -> exp * Env.t
val quantif_to_exp: kernel_function -> Env.t -> predicate -> exp * Env.t
(** The given predicate must be a quantification. *)
(* ***********************************************************************)
(** {2 Forward references} *)
(* ***********************************************************************)
val named_predicate_to_exp_ref:
(kernel_function -> Env.t -> predicate named -> exp * Env.t) ref
val predicate_to_exp_ref:
(kernel_function -> Env.t -> predicate -> exp * Env.t) ref
val term_to_exp_ref:
(kernel_function -> Env.t -> term -> exp * Env.t) ref
......
......@@ -623,8 +623,8 @@ and at_to_exp env t_opt label e =
any) in the given environment. Also extend this environment which includes
the generating constructs. *)
and named_predicate_content_to_exp ?name kf env p =
let loc = p.loc in
match p.content with
let loc = p.pred_loc in
match p.pred_content with
| Pfalse -> Cil.zero ~loc, env
| Ptrue -> Cil.one ~loc, env
| Papp _ -> not_yet env "logic function application"
......@@ -736,7 +736,7 @@ and named_predicate_to_exp ?name kf ?rte env p =
let env = if rte then translate_rte kf env e else env in
let cast = Typing.get_cast_of_predicate p in
add_cast
~loc:p.loc
~loc:p.pred_loc
?name
env
cast
......@@ -774,7 +774,7 @@ and translate_rte kf env e =
and translate_named_predicate kf env p =
Options.feedback ~dkey ~level:3 "translating predicate %a"
Printer.pp_predicate_named p;
Printer.pp_predicate p;
let rte = Env.generate_rte env in
Typing.type_named_predicate ~must_clear:rte p;
let e, env = named_predicate_to_exp kf ~rte env p in
......@@ -788,7 +788,7 @@ let named_predicate_to_exp ?name kf env p =
let () =
Quantif.term_to_exp_ref := term_to_exp;
Quantif.named_predicate_to_exp_ref := named_predicate_to_exp
Quantif.predicate_to_exp_ref := named_predicate_to_exp
(* This function is used by Guillaume.
However, it is correct to use it only in specific contexts. *)
......@@ -830,10 +830,10 @@ let term_to_exp typ t =
let assumes_predicate bhv =
List.fold_left
(fun acc p ->
Logic_const.pand
~loc:p.ip_loc
(acc, Logic_const.unamed ~loc:p.ip_loc p.ip_content))
(fun acc p ->
let loc = p.ip_content.pred_loc in
Logic_const.pand ~loc (acc,
Logic_const.unamed ~loc p.ip_content.pred_content))
Logic_const.ptrue
bhv.b_assumes
......@@ -858,13 +858,14 @@ let translate_preconditions kf kinstr env behaviors =
let assumes_pred = assumes_predicate b in
List.fold_left
(fun env p ->
let do_it env =
if must_translate (Property.ip_of_requires kf kinstr b p) then
let loc = p.ip_loc in
let p =
Logic_const.pimplies
~loc
(assumes_pred, Logic_const.unamed ~loc p.ip_content)
let do_it env =
if must_translate (Property.ip_of_requires kf kinstr b p) then
let loc = p.ip_content.pred_loc in
let p =
Logic_const.pimplies
~loc
(assumes_pred,
Logic_const.unamed ~loc p.ip_content.pred_content)
in
translate_named_predicate kf env p
else
......@@ -897,13 +898,13 @@ let translate_postconditions kf kinstr env behaviors =
let do_it env =
match t with
| Normal ->
let loc = p.ip_loc in
let loc = p.ip_content.pred_loc in
let p = p.ip_content in
let p =
Logic_const.pimplies
~loc
(Logic_const.pold ~loc assumes_pred,
Logic_const.unamed ~loc p)
Logic_const.unamed ~loc p.pred_content)
in
translate_named_predicate kf env p
| Exits | Breaks | Continues | Returns ->
......
......@@ -33,7 +33,7 @@ val translate_pre_code_annotation:
val translate_post_code_annotation:
kernel_function -> stmt -> Env.t -> code_annotation -> Env.t
val translate_named_predicate:
kernel_function -> Env.t -> predicate named -> Env.t
kernel_function -> Env.t -> predicate -> Env.t
val translate_rte_annots:
(Format.formatter -> 'a -> unit) ->
......@@ -46,7 +46,7 @@ val translate_rte_annots:
exception No_simple_translation of term
val term_to_exp: typ option -> term -> exp
val predicate_to_exp: kernel_function -> predicate named -> exp
val predicate_to_exp: kernel_function -> predicate -> exp
val set_original_project: Project.t -> unit
......
......@@ -28,7 +28,7 @@ open Cil_types
let dkey = Options.dkey_typing
let compute_quantif_guards_ref
: (predicate named -> logic_var list -> predicate named ->
: (predicate -> logic_var list -> predicate ->
(term * relation * logic_var * relation * term) list) ref
= Extlib.mk_fun "compute_quantif_guards_ref"
......@@ -442,10 +442,10 @@ and type_term_offset = function
ignore (type_term ~force:true ~ctx:(size_t ()) t);
type_term_offset toff
let rec type_predicate_named p =
Cil.CurrentLoc.set p.loc;
let rec type_predicate p =
Cil.CurrentLoc.set p.pred_loc;
(* this pattern matching also follows the formal rules of the JFLA's paper *)
let op = match p.content with
let op = match p.pred_content with
| Pfalse | Ptrue -> c_int
| Papp _ -> Error.not_yet "logic function application"
| Pseparated _ -> Error.not_yet "\\separated"
......@@ -470,22 +470,22 @@ let rec type_predicate_named p =
| Pxor(p1, p2)
| Pimplies(p1, p2)
| Piff(p1, p2) ->
ignore (type_predicate_named p1);
ignore (type_predicate_named p2);
ignore (type_predicate p1);
ignore (type_predicate p2);
c_int
| Pnot p ->
ignore (type_predicate_named p);
ignore (type_predicate p);
c_int
| Pif(t, p1, p2) ->
let ctx = mk_ctx ~force:true c_int in
ignore (type_term ~force:true ~ctx t);
ignore (type_predicate_named p1);
ignore (type_predicate_named p2);
ignore (type_predicate p1);
ignore (type_predicate p2);
c_int
| Plet _ -> Error.not_yet "let _ = _ in _"
| Pforall(bounded_vars, { content = Pimplies(hyps, goal) })
| Pexists(bounded_vars, { content = Pand(hyps, goal) }) ->
| Pforall(bounded_vars, { pred_content = Pimplies(hyps, goal) })
| Pexists(bounded_vars, { pred_content = Pand(hyps, goal) }) ->
let guards = !compute_quantif_guards_ref p bounded_vars hyps in
List.iter
(fun (t1, r1, x, r2, t2) ->
......@@ -524,7 +524,7 @@ let rec type_predicate_named p =
ignore (type_term ~force:true ~ctx t2);
Interval.Env.add x i)
guards;
(type_predicate_named goal).ty
(type_predicate goal).ty
| Pinitialized(_, t)
| Pfreeable(_, t)
......@@ -537,7 +537,7 @@ let rec type_predicate_named p =
| Pforall _ -> Error.not_yet "unguarded \\forall quantification"
| Pexists _ -> Error.not_yet "unguarded \\exists quantification"
| Pat(p, _) -> (type_predicate_named p).ty
| Pat(p, _) -> (type_predicate p).ty
| Pfresh _ -> Error.not_yet "\\fresh"
| Psubtype _ -> Error.not_yet "subtyping relation" (* Jessie specific *)
in
......@@ -550,12 +550,12 @@ let type_term ~force ?ctx t =
let type_named_predicate ?(must_clear=true) p =
Options.feedback ~dkey ~level:3 "typing predicate '%a'."
Printer.pp_predicate_named p;
Printer.pp_predicate p;
if must_clear then begin
Interval.Env.clear ();
Memo.clear ()
end;
ignore (type_predicate_named p)
ignore (type_predicate p)
(******************************************************************************)
(** {2 Getters} *)
......@@ -563,7 +563,7 @@ let type_named_predicate ?(must_clear=true) p =
let get_integer_ty t = (Memo.get t).ty
let get_integer_op t = (Memo.get t).op
let get_integer_op_of_predicate p = (type_predicate_named p).op
let get_integer_op_of_predicate p = (type_predicate p).op
(* {!typ_of_integer}, but handle the not-integer cases. *)
let extract_typ t ty =
......@@ -592,7 +592,7 @@ let get_cast t =
with Not_an_integer -> None
let get_cast_of_predicate p =
let info = type_predicate_named p in
let info = type_predicate p in
try Extlib.opt_map typ_of_integer_ty info.cast
with Not_an_integer -> assert false
......
......@@ -86,7 +86,7 @@ val type_term: force:bool -> ?ctx:integer_ty -> term -> unit
[force] is true, then the conversion to the given context is done even if
-e-acsl-gmp-only is set. *)
val type_named_predicate: ?must_clear:bool -> predicate named -> unit
val type_named_predicate: ?must_clear:bool -> predicate -> unit
(** Compute the type of each term of the given predicate.
Set {!must_clear} to false in order to not reset the environment. *)
......@@ -107,7 +107,7 @@ val get_integer_op: term -> integer_ty
It is meaningless to call this function over a non-arithmetical/logical
operator. *)
val get_integer_op_of_predicate: predicate named -> integer_ty
val get_integer_op_of_predicate: predicate -> integer_ty
(** @return the infered type for the top operation of the given predicate. *)
val get_typ: term -> typ
......@@ -120,7 +120,7 @@ val get_op: term -> typ
val get_cast: term -> typ option
(** Get the type which the given term must be converted to (if any). *)
val get_cast_of_predicate: predicate named -> typ option
val get_cast_of_predicate: predicate -> typ option
(** Like {!get_cast}, but for predicates. *)
(******************************************************************************)
......@@ -128,7 +128,7 @@ val get_cast_of_predicate: predicate named -> typ option
(******************************************************************************)
val compute_quantif_guards_ref
: (predicate named -> logic_var list -> predicate named ->
: (predicate -> logic_var list -> predicate ->
(term * relation * logic_var * relation * term) list) ref
(** Forward reference. *)
......
......@@ -737,7 +737,7 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
| _ -> ());
t)
method !vpredicate _ =
method !vpredicate_node _ =
Cil.DoChildrenPost
(function
| Pat(_, StmtLabel s_ref) as p ->
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment