diff --git a/src/kernel_services/ast_data/annotations.ml b/src/kernel_services/ast_data/annotations.ml
index cc6c5221d3e88a2f0f0cf893a453e9cc80869625..90690303633e5645a68168a2d13dcf4a7c9cab9c 100644
--- a/src/kernel_services/ast_data/annotations.ml
+++ b/src/kernel_services/ast_data/annotations.ml
@@ -1001,6 +1001,19 @@ let add_disjoint e kf ?stmt ?active l =
Property_status.register (Property.ip_of_disjoint kf (kinstr stmt) active l)
end
+let add_spec ?register_children e kf ?stmt ?active spec =
+ add_behaviors ?register_children e kf ?stmt ?active spec.spec_behavior;
+ Option.iter (fun variant -> add_decreases e kf variant) spec.spec_variant;
+ Option.iter
+ (fun terminates -> add_terminates e kf ?stmt ?active terminates)
+ spec.spec_terminates;
+ List.iter
+ (fun complete -> add_complete e kf ?stmt ?active complete)
+ spec.spec_complete_behaviors;
+ List.iter
+ (fun disjoint -> add_disjoint e kf ?stmt ?active disjoint)
+ spec.spec_disjoint_behaviors
+
let extend_behavior
e kf ?stmt ?active ?(behavior=Cil.default_behavior_name) set_bhv =
(* Kernel.feedback "Function %a, behavior %s" Kf.pretty kf bhv_name;*)
diff --git a/src/kernel_services/ast_data/annotations.mli b/src/kernel_services/ast_data/annotations.mli
index c6b8e7d3f81dcf518e58918404d31c93da63d1af..1b7e315613ec5e5bd32073bb0b8eef9424d1218f 100644
--- a/src/kernel_services/ast_data/annotations.mli
+++ b/src/kernel_services/ast_data/annotations.mli
@@ -334,6 +334,14 @@ type 'a behavior_component_addition =
@since Aluminium-20160501
*)
+val add_spec: ?register_children:bool -> spec contract_component_addition
+(** Add new spec into the given contract.
+
+ [register_children] is directly given to the function [add_behaviors].
+
+ @since Frama-C+dev
+*)
+
val add_behaviors:
?register_children:bool -> funbehavior list contract_component_addition
(** Add new behaviors into the given contract.
diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/e_acsl_observation_model.h b/src/plugins/e-acsl/share/e-acsl/observation_model/e_acsl_observation_model.h
index f55417402c009ae4e15f44fb747d6d3be9a0f62e..4a5a8204afda7fc9457a9b68a8c7712c5290ee09 100644
--- a/src/plugins/e-acsl/share/e-acsl/observation_model/e_acsl_observation_model.h
+++ b/src/plugins/e-acsl/share/e-acsl/observation_model/e_acsl_observation_model.h
@@ -36,6 +36,19 @@
#include "../internals/e_acsl_alias.h"
#include "e_acsl_heap.h"
+/*@ ghost extern int __fc_heap_status; */
+
+/*@ axiomatic dynamic_allocation {
+ @ predicate is_allocable{L}(integer n) // Can a block of n bytes be allocated?
+ @ reads __fc_heap_status;
+ @ // The logic label L is not used, but it must be present because the
+ @ // predicate depends on the memory state
+ @ axiom never_allocable{L}:
+ @ \forall integer i;
+ @ i < 0 || i > __FC_SIZE_MAX ==> !is_allocable(i);
+ @ }
+*/
+
/************************************************************************/
/*** API Prefixes {{{ ***/
/************************************************************************/
@@ -83,8 +96,16 @@
* behaviour is as if the size were some non-zero value, except that the
* returned pointer shall not be used to access an object." */
/*@
- assigns __e_acsl_heap_allocation_size \from size, __e_acsl_heap_allocation_size;
- assigns __e_acsl_heap_allocated_blocks \from size, __e_acsl_heap_allocated_blocks;
+ assigns __e_acsl_heap_allocation_size \from indirect:size, __e_acsl_heap_allocation_size;
+ assigns __e_acsl_heap_allocated_blocks \from indirect:size, __e_acsl_heap_allocated_blocks;
+ behavior allocation:
+ assumes can_allocate: is_allocable(size);
+ assigns __e_acsl_heap_allocation_size \from indirect:size, __e_acsl_heap_allocation_size;
+ assigns __e_acsl_heap_allocated_blocks \from indirect:size, __e_acsl_heap_allocated_blocks;
+ behavior no_allocation:
+ assumes cannot_allocate: !is_allocable(size);
+ assigns __e_acsl_heap_allocation_size \from indirect:size, __e_acsl_heap_allocation_size;
+ assigns __e_acsl_heap_allocated_blocks \from size, __e_acsl_heap_allocated_blocks;
*/
void * malloc(size_t size)
__attribute__((FC_BUILTIN));
@@ -94,6 +115,14 @@ void * malloc(size_t size)
/*@
assigns __e_acsl_heap_allocation_size \from indirect:nbr_elt, indirect:size_elt, __e_acsl_heap_allocation_size;
assigns __e_acsl_heap_allocated_blocks \from indirect:nbr_elt, indirect:size_elt, __e_acsl_heap_allocated_blocks;
+ behavior allocation:
+ assumes can_allocate: is_allocable(nbr_elt * size_elt);
+ assigns __e_acsl_heap_allocation_size \from indirect:nbr_elt, indirect:size_elt, __e_acsl_heap_allocation_size;
+ assigns __e_acsl_heap_allocated_blocks \from indirect:nbr_elt, indirect:size_elt, __e_acsl_heap_allocated_blocks;
+ behavior no_allocation:
+ assumes cannot_allocate: !is_allocable(nbr_elt * size_elt);
+ assigns __e_acsl_heap_allocation_size \from indirect:nbr_elt, indirect:size_elt, __e_acsl_heap_allocation_size;
+ assigns __e_acsl_heap_allocated_blocks \from indirect:nbr_elt, indirect:size_elt, __e_acsl_heap_allocated_blocks;
*/
void * calloc(size_t nbr_elt, size_t size_elt)
__attribute__((FC_BUILTIN));
@@ -103,6 +132,19 @@ void * calloc(size_t nbr_elt, size_t size_elt)
/*@
assigns __e_acsl_heap_allocation_size \from __e_acsl_heap_allocation_size;
assigns __e_acsl_heap_allocated_blocks \from __e_acsl_heap_allocated_blocks;
+ behavior allocation:
+ assumes can_allocate: is_allocable(size);
+ assigns __e_acsl_heap_allocation_size \from __e_acsl_heap_allocation_size;
+ assigns __e_acsl_heap_allocated_blocks \from __e_acsl_heap_allocated_blocks;
+ behavior deallocation:
+ assumes nonnull_ptr: ptr != \null;
+ assumes can_allocate: is_allocable(size);
+ assigns __e_acsl_heap_allocation_size \from __e_acsl_heap_allocation_size;
+ assigns __e_acsl_heap_allocated_blocks \from __e_acsl_heap_allocated_blocks;
+ behavior fail:
+ assumes cannot_allocate: !is_allocable(size);
+ assigns __e_acsl_heap_allocation_size \from __e_acsl_heap_allocation_size;
+ assigns __e_acsl_heap_allocated_blocks \from __e_acsl_heap_allocated_blocks;
*/
void * realloc(void * ptr, size_t size)
__attribute__((FC_BUILTIN));
@@ -112,6 +154,14 @@ void * realloc(void * ptr, size_t size)
/*@
assigns __e_acsl_heap_allocation_size \from __e_acsl_heap_allocation_size;
assigns __e_acsl_heap_allocated_blocks \from __e_acsl_heap_allocated_blocks;
+ behavior deallocation:
+ assumes nonnull_p: ptr != \null;
+ assigns __e_acsl_heap_allocation_size \from __e_acsl_heap_allocation_size;
+ assigns __e_acsl_heap_allocated_blocks \from __e_acsl_heap_allocated_blocks;
+ behavior no_deallocation:
+ assumes null_p: ptr == \null;
+ assigns __e_acsl_heap_allocation_size \from __e_acsl_heap_allocation_size;
+ assigns __e_acsl_heap_allocated_blocks \from __e_acsl_heap_allocated_blocks;
*/
void free(void * ptr)
__attribute__((FC_BUILTIN));
@@ -137,6 +187,14 @@ void *aligned_alloc(size_t alignment, size_t size)
/*@
assigns __e_acsl_heap_allocation_size \from indirect:alignment, size, __e_acsl_heap_allocation_size;
assigns __e_acsl_heap_allocated_blocks \from indirect:alignment, size, __e_acsl_heap_allocated_blocks;
+ behavior allocation:
+ assumes can_allocate: is_allocable(size);
+ assigns __e_acsl_heap_allocation_size \from indirect:alignment, size, __e_acsl_heap_allocation_size;
+ assigns __e_acsl_heap_allocated_blocks \from indirect:alignment, size, __e_acsl_heap_allocated_blocks;
+ behavior no_allocation:
+ assumes cannot_allocate: !is_allocable(size);
+ assigns __e_acsl_heap_allocation_size \from indirect:alignment, size, __e_acsl_heap_allocation_size;
+ assigns __e_acsl_heap_allocated_blocks \from indirect:alignment, size, __e_acsl_heap_allocated_blocks;
*/
int posix_memalign(void **memptr, size_t alignment, size_t size)
__attribute__((FC_BUILTIN));
diff --git a/src/plugins/e-acsl/src/project_initializer/rtl.ml b/src/plugins/e-acsl/src/project_initializer/rtl.ml
index 07be50d1a64fb1cfbebc38c5a8351b25e03b7204..8c96f04f908c620773f0a2cb0bf2ca75df2d489d 100644
--- a/src/plugins/e-acsl/src/project_initializer/rtl.ml
+++ b/src/plugins/e-acsl/src/project_initializer/rtl.ml
@@ -100,6 +100,71 @@ end = struct
*)
end
+(* Internal module to store the associations between symbols in the RTL project
+ and their corresponding symbols in the user's project. *)
+module Assocs: sig
+ val clear: unit -> unit
+ (** Clear stored associations. *)
+
+ val add_kf: global -> kernel_function -> unit
+ (** Add an association between a global in the RTL project and the
+ corresponding kernel function in the user's project. *)
+
+ val mem_kf: global -> bool
+ (** Returns true if the given global from the RTL project has a corresponding
+ kernel function in the user's project. *)
+
+ val get_kf: global -> kernel_function
+ (** Returns the corresponding kernel function from the user's project for the
+ given global in the RTL project. *)
+
+ val add_vi: varinfo -> varinfo -> unit
+ (** [add_vi rtl_vi user_vi] adds an association between a [varinfo] in the
+ RTL project and the corresponding [varinfo] in the user's project. *)
+
+ val find_vi: varinfo -> varinfo
+ (** [find_vi rtl_vi] returns the corresponding [varinfo] from the user's
+ project for the given [varinfo] in the RTL project if it exists, or raise
+ [Not_found] otherwise. *)
+
+ val add_li: logic_info -> logic_info -> unit
+ (** [add_li rtl_li user_li] adds an association between a [logic_info] in the
+ RTL project and the corresponding [logic_info] in the user's project. *)
+
+ val find_li: logic_info -> logic_info
+ (** [find_li rtl_li] returns the corresponding [logic_info] from the user's
+ project for the given [logic_info] in the RTL project if it exists,
+ or raise [Not_found] otherwise. *)
+
+end = struct
+ let kfs: kernel_function Global.Hashtbl.t = Global.Hashtbl.create 17
+ let vars: varinfo Varinfo.Hashtbl.t = Varinfo.Hashtbl.create 17
+ let logic_vars: logic_info Logic_info.Hashtbl.t = Logic_info.Hashtbl.create 17
+
+ let clear () =
+ Global.Hashtbl.clear kfs;
+ Varinfo.Hashtbl.clear vars;
+ Logic_info.Hashtbl.clear logic_vars
+
+ let add_kf rtl_g user_kf = Global.Hashtbl.replace kfs rtl_g user_kf
+ let mem_kf rtl_g = Global.Hashtbl.mem kfs rtl_g
+ let get_kf rtl_g =
+ try
+ Global.Hashtbl.find kfs rtl_g
+ with Not_found ->
+ Options.fatal
+ "Unable to find user kf corresponding to %a. Assocs.mem_kf should be \
+ used before calling Assocs.get_kf"
+ Printer.pp_global rtl_g
+
+ let add_vi rtl_vi user_vi = Varinfo.Hashtbl.replace vars rtl_vi user_vi
+ let find_vi rtl_vi = Varinfo.Hashtbl.find vars rtl_vi
+
+ let add_li rtl_li user_li = Logic_info.Hashtbl.replace logic_vars rtl_li user_li
+ let find_li rtl_li = Logic_info.Hashtbl.find logic_vars rtl_li
+end
+
+
(* NOTE: do not use [Mergecil.merge] since all [ast]'s symbols must be kept
unchanged: so do it ourselves. Thanksfully, we merge in a particular
setting because we know what the RTL is. Therefore merging is far from being
@@ -109,11 +174,15 @@ end
tables.
@return the list of globals to be inserted into [ast], in reverse order. *)
let lookup_rtl_globals rtl_ast =
- (* [do_it ~add mem acc l g] checks whether the global does exist in the user's
- AST. If not, add it to the corresponding symbol table(s). *)
- let rec do_it ?(add=fun _g -> ()) mem acc l g =
- if mem g then do_globals (g :: acc) l
- else begin
+ (* [do_it ~add ~assoc mem acc l g] checks whether the global does exist in the
+ user's AST. If not, add it to the corresponding symbol table(s). If yes,
+ save the association between the global in the user's AST and the global in
+ the RTL. *)
+ let rec do_it ?(add=fun _g -> ()) ?(assoc=fun _g -> ()) mem acc l g =
+ if mem g then begin
+ assoc g;
+ do_globals (g :: acc) l
+ end else begin
add g;
Symbols.add_global g;
do_globals (g :: acc) l
@@ -134,8 +203,11 @@ let lookup_rtl_globals rtl_ast =
do_ty acc l g Logic_typing.Enum ei.ename
| GVarDecl(vi, (pos, _)) | GVar(vi, _, (pos, _)) as g :: l ->
let tunit = Translation_unit pos.Filepath.pos_path in
+ let get_old_vi_opt vi =
+ Globals.Syntactic_search.find_in_scope vi.vorig_name tunit
+ in
let mem _g =
- let g = Globals.Syntactic_search.find_in_scope vi.vorig_name tunit in
+ let g = get_old_vi_opt vi in
Option.is_some g
in
let add g =
@@ -145,16 +217,95 @@ let lookup_rtl_globals rtl_ast =
| GVar(_, ii, _) -> Globals.Vars.add vi ii
| _ -> assert false
in
- do_it ~add mem acc l g
+ let assoc _g =
+ (* [assoc] is called if [mem] returns true, so the option returned by
+ [get_old_vi_opt] is [Some] by construction. *)
+ let old_vi = get_old_vi_opt vi in
+ Assocs.add_vi vi (Option.get old_vi)
+ in
+ do_it ~add ~assoc mem acc l g
| GFunDecl(_, vi, _loc) | GFun({ svar = vi }, _loc) as g :: l ->
let add _g =
Symbols.add_vi vi.vname vi;
(* functions will be registered in kernel's table after substitution of
RTL's symbols inside them *)
in
- do_it ~add (fun _ -> Globals.Functions.mem_name vi.vname) acc l g
+ let assoc g =
+ let kf = Globals.Functions.find_by_name vi.vname in
+ Assocs.add_kf g kf
+ in
+ do_it ~add ~assoc (fun _ -> Globals.Functions.mem_name vi.vname) acc l g
+ | GAnnot (Daxiomatic (name, galist, _, _), _) as g :: l ->
+ (* processing axiomatics *)
+ let fun_or_preds =
+ (* extract the functions and predicates from the axiomatic *)
+ List.filter_map
+ (fun ga ->
+ match ga with
+ | Dfun_or_pred (li, _) -> Some li
+ | _ -> None)
+ galist
+ in
+ let mem _ =
+ (* check if some function or predicate of the axiomatic [exists] in the
+ user's project, if all the functions and predicates are in the user's
+ project ([forall]), and store which function and predicate are in the
+ user's project in [conflicting_lis]. *)
+ let exists, forall, conflicting_lis =
+ List.fold_left
+ (fun (exists, forall, conflicting_lis) li ->
+ let lv_name = li.l_var_info.lv_name in
+ let li_exists = Logic_env.Logic_info.mem lv_name in
+ let conflicting_lis =
+ if li_exists then li :: conflicting_lis else conflicting_lis
+ in
+ exists || li_exists, forall && li_exists, conflicting_lis)
+ (false, true, [])
+ fun_or_preds
+ in
+ (* The axiomatic is considered "in the user's project" if and only if
+ all its functions and predicates are in the user's project. If only
+ some of them are in it then it is an error, and if none of them are
+ then the axiomatic is not in the user's project. *)
+ if exists && not forall then
+ Options.abort
+ "@[The following logic functions or predicates@ \
+ are in conflict with logic functions or predicates from the@ \
+ axiomatic '%s' in the E-ACSL runtime library, please rename@ \
+ them:@ %a@]"
+ name
+ (Pretty_utils.pp_list
+ ~sep:",@ "
+ Printer.pp_logic_info)
+ conflicting_lis
+ else
+ forall
+ in
+ let assoc _g =
+ List.iter
+ (fun li ->
+ let lv_name = li.l_var_info.lv_name in
+ let old_lis = Logic_env.Logic_info.find lv_name in
+ let old_li =
+ try
+ List.find
+ (fun old_li -> Logic_utils.is_same_logic_info li old_li)
+ old_lis
+ with Not_found ->
+ Options.fatal
+ "Unable to find the logic_info in the user's AST \
+ corresponding to the logic_info %a in the RTL's AST. This \
+ most likely comes from a mismatch between the axiomatic %s \
+ in the RTL that is supposed to mirror one from the stdlib."
+ Printer.pp_logic_info li
+ name
+ in
+ Assocs.add_li li old_li)
+ fun_or_preds
+ in
+ do_it ~assoc mem acc l g
| GAnnot _ :: l ->
- (* ignoring annotations from the AST *)
+ (* ignoring other annotations from the AST *)
do_globals acc l
| GPragma _ as g :: l ->
do_it Symbols.mem_global acc l g
@@ -163,34 +314,86 @@ let lookup_rtl_globals rtl_ast =
in
do_globals [] rtl_ast.globals
+(** [get_kf vi] returns the kernel function corresponding to the given varinfo
+ in the current project. The varinfo must correspond to a kernel function. *)
+let get_kf vi =
+ try
+ Globals.Functions.get vi
+ with Not_found ->
+ Options.fatal "unknown function %s in project %a"
+ vi.vname
+ Project.pretty (Project.current ())
+
+(** [get_formals_and_spec prj vi] returns a couple with the formals and function
+ specification of the function corresponding to the varinfo [vi] in the
+ project [prj]. The varinfo must correspond to a function of the given
+ project. *)
+let get_formals_and_spec prj vi =
+ let selection =
+ State_selection.of_list
+ [ Globals.Functions.self; Annotations.funspec_state ]
+ in
+ Project.on
+ prj
+ ~selection
+ (fun vi ->
+ let kf = get_kf vi in
+ Kernel_function.get_formals kf,
+ Annotations.funspec ~populate:false kf)
+ vi
+
+(** Visitor to replace [varinfo] and [logic_info] leaves of an AST with
+ corresponding values from the [Assocs] tables.
+ If the visitor is created with the [formals] associating the [varinfo] of
+ the RTL formals with the [varinfo]Â of the user formals, then replace the
+ corresponding [varinfo] leaves. *)
+class vis_replace_leaves ?formals () =
+ object
+ (* Since we are already working on a copied project, we can use an inplace
+ visitor. *)
+ inherit Visitor.frama_c_inplace
+
+ val formals: varinfo Varinfo.Hashtbl.t =
+ match formals with
+ | None -> Varinfo.Hashtbl.create 7
+ | Some formals -> formals
+
+ (* Since the RTL project will be deleted at the end of the AST
+ merge, we can temporarily violate the Frama-C invariant that says
+ that a varinfo or logic_info must be in a single project and directly
+ replace the varinfo/logic_info of the RTL in the specification with the
+ logic_info/varinfo of the user's AST. *)
+
+ method! vlogic_info_use rtl_li =
+ try
+ (* Replace the logic_info if it is a logic_info from the RTL project. *)
+ let user_li = Assocs.find_li rtl_li in
+ Cil.ChangeTo user_li
+ with Not_found ->
+ Cil.SkipChildren
+
+ method! vvrbl rtl_vi =
+ try
+ (* Replace the varinfo if it is a global from the RTL project.*)
+ let user_vi = Assocs.find_vi rtl_vi in
+ Cil.ChangeTo user_vi
+ with Not_found ->
+ try
+ (* Replace the varinfo if it is a formal. *)
+ let user_vi = Varinfo.Hashtbl.find formals rtl_vi in
+ Cil.ChangeTo user_vi
+ with Not_found ->
+ (* Otherwise do nothing. *)
+ Cil.SkipChildren
+ end
+
(* [substitute_rtl_symbols] registers the correct symbols for RTL's functions *)
let substitute_rtl_symbols rtl_prj = function
| GVarDecl _ | GVar _ as g ->
g
| GFunDecl(_, vi, loc) | GFun({ svar = vi }, loc) as g ->
- let get_kf vi =
- try
- Globals.Functions.get vi
- with Not_found ->
- Options.fatal "unknown function %s in project %a"
- vi.vname
- Project.pretty (Project.current ())
- in
- let selection =
- State_selection.of_list
- [ Globals.Functions.self; Annotations.funspec_state ]
- in
(* get the RTL's formals and spec *)
- let formals, spec =
- Project.on
- rtl_prj
- ~selection
- (fun vi ->
- let kf = get_kf vi in
- Kernel_function.get_formals kf,
- Annotations.funspec ~populate:false kf)
- vi
- in
+ let formals, spec = get_formals_and_spec rtl_prj vi in
(match g with
| GFunDecl _ ->
Globals.Functions.replace_by_declaration spec vi loc
@@ -209,10 +412,47 @@ let substitute_rtl_symbols rtl_prj = function
Annotations.register_funspec ~emitter:Options.emitter kf;
Symbols.add_kf kf;
g
+ | GAnnot (Daxiomatic _ as ga, loc) ->
+ let vis_replace_leaves = new vis_replace_leaves () in
+ let ga = Visitor.visitFramacAnnotation vis_replace_leaves ga in
+ Annotations.add_global Options.emitter ga;
+ GAnnot (ga, loc)
| GType _ | GCompTag _ | GCompTagDecl _ | GEnumTag _ | GEnumTagDecl _
| GAnnot _ | GAsm _ | GPragma _ | GText _ ->
assert false
+(* [merge_rtl_spec rtl_prj rtl_global] adds the spec of the given global
+ function from the RTL project to the corresponding function in the current
+ project. Before adding the spec, the varinfos of the global variables and
+ formals in the spec are replaced with their corresponding varinfos in the
+ current project. *)
+let merge_rtl_spec rtl_prj rtl_global =
+ match rtl_global with
+ | GFunDecl(_, vi, _loc) | GFun({ svar = vi }, _loc) as g ->
+ (* get the RTL's formals and spec *)
+ let rtl_formals, spec = get_formals_and_spec rtl_prj vi in
+ (* if the spec is not empty, then merge it with the user's spec *)
+ if not (Cil.is_empty_funspec spec) then begin
+ (* get the user's kf *)
+ let user_kf = Assocs.get_kf g in
+ (* get the user's formals *)
+ let user_formals = Kernel_function.get_formals user_kf in
+ (* replace all the formals and global variables in the spec with the
+ formals and globals from the user's project. *)
+ let formals_assoc: varinfo Varinfo.Hashtbl.t = Varinfo.Hashtbl.create 7 in
+ List.iter2
+ (fun rtl_vi user_vi -> Varinfo.Hashtbl.add formals_assoc rtl_vi user_vi)
+ rtl_formals
+ user_formals;
+ let vis_replace_formals = new vis_replace_leaves ~formals:formals_assoc () in
+ let spec = Visitor.visitFramacFunspec vis_replace_formals spec in
+ (* Add the updated spec to the user's kf *)
+ Annotations.add_spec Options.emitter user_kf spec
+ end
+ | GVarDecl _ | GVar _ | GType _ | GCompTag _ | GCompTagDecl _ | GEnumTag _
+ | GEnumTagDecl _ | GAnnot _ | GAsm _ | GPragma _ | GText _ ->
+ assert false
+
(* [insert_rtl_globals] adds the rtl symbols into the user's AST *)
let insert_rtl_globals rtl_prj rtl_globals ast =
let add_ty acc old_g new_g =
@@ -238,12 +478,21 @@ let insert_rtl_globals rtl_prj rtl_globals ast =
only declared *)
let acc = add_ty acc g (GEnumTagDecl(ei, loc)) in
add acc l
- | GVarDecl _ | GVar _ | GFunDecl _ | GFun _ as g :: l ->
+ | GVarDecl _ | GVar _ | GFunDecl _ | GFun _
+ | GAnnot (Daxiomatic _, _) as g :: l ->
let acc =
if Symbols.mem_global g then
+ (* The symbol is in the RTL project, but not in the user's project.
+ Perform the symbols substitution and add the global to the user's
+ project. *)
let g = substitute_rtl_symbols rtl_prj g in
g :: acc
- else
+ else if Assocs.mem_kf g then begin
+ (* The symbol is in the RTL project and associated with a kf in the
+ user's project. Merge both contracts. *)
+ merge_rtl_spec rtl_prj g;
+ acc
+ end else
acc
in
add acc l
@@ -261,6 +510,7 @@ let link rtl_prj =
let rtl_globals = lookup_rtl_globals rtl_ast in
(* Symbols.debug ();*)
insert_rtl_globals rtl_prj rtl_globals ast;
+ Assocs.clear ();
Ast.mark_as_grown ()
(*
diff --git a/src/plugins/e-acsl/tests/memory/memsize.c b/src/plugins/e-acsl/tests/memory/memsize.c
index c214b60ebd4dcbb33a07b64bf3fddf3e7aec9a8e..2260a306878d6dfd4943d73ccbddc6436c2ec2f5 100644
--- a/src/plugins/e-acsl/tests/memory/memsize.c
+++ b/src/plugins/e-acsl/tests/memory/memsize.c
@@ -1,5 +1,6 @@
-/* run.config
+/* run.config_ci
COMMENT: Checking heap memory size
+ STDOPT: +"-eva-no-builtins-auto"
*/
#include <stdlib.h>
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_memalign.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_memalign.c
index 594eb809025228428f8d77a55c247c7157cab650..86b350d6bcd47ce810e3942357482c1a1697e052 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_memalign.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_memalign.c
@@ -40,6 +40,12 @@ extern int __e_acsl_sound_verdict;
*/
int __gen_e_acsl_posix_memalign(void **memptr, size_t alignment, size_t size);
+/*@ assigns __e_acsl_heap_allocation_size, __e_acsl_heap_allocated_blocks;
+ assigns __e_acsl_heap_allocation_size
+ \from (indirect: alignment), size, __e_acsl_heap_allocation_size;
+ assigns __e_acsl_heap_allocated_blocks
+ \from (indirect: alignment), size, __e_acsl_heap_allocated_blocks;
+ */
void *aligned_alloc(size_t alignment, size_t size);
int main(int argc, char const **argv)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_memsize.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_memsize.c
index 134e80f8dafed2dc211d27d63cf0ed3076a9c401..d31fa69d2a5df24b8d9189086ba15157c57864a5 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_memsize.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_memsize.c
@@ -11,73 +11,73 @@ int main(int argc, char **argv)
char *a = malloc((unsigned long)7);
__e_acsl_assert(__e_acsl_heap_allocation_size == 7UL,"Assertion","main",
"__e_acsl_heap_allocation_size == 7",
- "tests/memory/memsize.c",14);
+ "tests/memory/memsize.c",15);
/*@ assert __e_acsl_heap_allocation_size ≡ 7; */ ;
char *b = malloc((unsigned long)14);
__e_acsl_assert(__e_acsl_heap_allocation_size == 21UL,"Assertion","main",
"__e_acsl_heap_allocation_size == 21",
- "tests/memory/memsize.c",16);
+ "tests/memory/memsize.c",17);
/*@ assert __e_acsl_heap_allocation_size ≡ 21; */ ;
free((void *)a);
__e_acsl_assert(__e_acsl_heap_allocation_size == 14UL,"Assertion","main",
"__e_acsl_heap_allocation_size == 14",
- "tests/memory/memsize.c",20);
+ "tests/memory/memsize.c",21);
/*@ assert __e_acsl_heap_allocation_size ≡ 14; */ ;
a = (char *)0;
free((void *)a);
__e_acsl_assert(__e_acsl_heap_allocation_size == 14UL,"Assertion","main",
"__e_acsl_heap_allocation_size == 14",
- "tests/memory/memsize.c",25);
+ "tests/memory/memsize.c",26);
/*@ assert __e_acsl_heap_allocation_size ≡ 14; */ ;
b = (char *)realloc((void *)b,(unsigned long)9);
__e_acsl_assert(__e_acsl_heap_allocation_size == 9UL,"Assertion","main",
"__e_acsl_heap_allocation_size == 9",
- "tests/memory/memsize.c",29);
+ "tests/memory/memsize.c",30);
/*@ assert __e_acsl_heap_allocation_size ≡ 9; */ ;
b = (char *)realloc((void *)b,(unsigned long)18);
__e_acsl_assert(__e_acsl_heap_allocation_size == 18UL,"Assertion","main",
"__e_acsl_heap_allocation_size == 18",
- "tests/memory/memsize.c",33);
+ "tests/memory/memsize.c",34);
/*@ assert __e_acsl_heap_allocation_size ≡ 18; */ ;
b = (char *)realloc((void *)b,(unsigned long)0);
b = (char *)0;
__e_acsl_assert(__e_acsl_heap_allocation_size == 0UL,"Assertion","main",
"__e_acsl_heap_allocation_size == 0",
- "tests/memory/memsize.c",38);
+ "tests/memory/memsize.c",39);
/*@ assert __e_acsl_heap_allocation_size ≡ 0; */ ;
b = (char *)realloc((void *)b,(unsigned long)8);
__e_acsl_assert(__e_acsl_heap_allocation_size == 8UL,"Assertion","main",
"__e_acsl_heap_allocation_size == 8",
- "tests/memory/memsize.c",42);
+ "tests/memory/memsize.c",43);
/*@ assert __e_acsl_heap_allocation_size ≡ 8; */ ;
b = (char *)realloc((void *)0,(unsigned long)8);
__e_acsl_assert(__e_acsl_heap_allocation_size == 16UL,"Assertion","main",
"__e_acsl_heap_allocation_size == 16",
- "tests/memory/memsize.c",46);
+ "tests/memory/memsize.c",47);
/*@ assert __e_acsl_heap_allocation_size ≡ 16; */ ;
b = (char *)realloc((void *)0,18446744073709551615UL);
__e_acsl_assert(__e_acsl_heap_allocation_size == 16UL,"Assertion","main",
"__e_acsl_heap_allocation_size == 16",
- "tests/memory/memsize.c",50);
+ "tests/memory/memsize.c",51);
/*@ assert __e_acsl_heap_allocation_size ≡ 16; */ ;
__e_acsl_assert(b == (char *)0,"Assertion","main","b == (char *)0",
- "tests/memory/memsize.c",51);
+ "tests/memory/memsize.c",52);
/*@ assert b ≡ (char *)0; */ ;
b = (char *)calloc(18446744073709551615UL,18446744073709551615UL);
__e_acsl_assert(__e_acsl_heap_allocation_size == 16UL,"Assertion","main",
"__e_acsl_heap_allocation_size == 16",
- "tests/memory/memsize.c",55);
+ "tests/memory/memsize.c",56);
/*@ assert __e_acsl_heap_allocation_size ≡ 16; */ ;
__e_acsl_assert(b == (char *)0,"Assertion","main","b == (char *)0",
- "tests/memory/memsize.c",56);
+ "tests/memory/memsize.c",57);
/*@ assert b ≡ (char *)0; */ ;
b = (char *)malloc(18446744073709551615UL);
__e_acsl_assert(__e_acsl_heap_allocation_size == 16UL,"Assertion","main",
"__e_acsl_heap_allocation_size == 16",
- "tests/memory/memsize.c",60);
+ "tests/memory/memsize.c",61);
/*@ assert __e_acsl_heap_allocation_size ≡ 16; */ ;
__e_acsl_assert(b == (char *)0,"Assertion","main","b == (char *)0",
- "tests/memory/memsize.c",61);
+ "tests/memory/memsize.c",62);
/*@ assert b ≡ (char *)0; */ ;
__retres = 0;
__e_acsl_memory_clean();
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/memsize.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/memsize.res.oracle
index 2db55f248cb6caa7f38d1c46c8c93f5bdc964f5e..68e3cc47739f873c790ec413966607107df9a811 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/memsize.res.oracle
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/memsize.res.oracle
@@ -1,7 +1,66 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-[eva:alarm] tests/memory/memsize.c:14: Warning:
+[eva] tests/memory/memsize.c:14: Warning: ignoring unsupported \allocates clause
+[eva:alarm] tests/memory/memsize.c:15: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/memory/memsize.c:15: Warning: assertion got status unknown.
+[eva] tests/memory/memsize.c:16: Warning: ignoring unsupported \allocates clause
+[eva:alarm] tests/memory/memsize.c:17: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/memory/memsize.c:17: Warning: assertion got status unknown.
+[eva] tests/memory/memsize.c:20: Warning: ignoring unsupported \allocates clause
+[eva:alarm] tests/memory/memsize.c:20: Warning:
+ function free: precondition 'freeable' got status unknown.
+[eva:alarm] tests/memory/memsize.c:21: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/memory/memsize.c:21: Warning: assertion got status unknown.
+[eva] tests/memory/memsize.c:25: Warning: ignoring unsupported \allocates clause
+[eva:alarm] tests/memory/memsize.c:26: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/memory/memsize.c:26: Warning: assertion got status unknown.
+[eva] FRAMAC_SHARE/libc/stdlib.h:452: Warning:
+ no 'assigns \result \from ...' clause specified for function realloc
+[eva] tests/memory/memsize.c:29: Warning: ignoring unsupported \allocates clause
+[eva:alarm] tests/memory/memsize.c:29: Warning:
+ function realloc: precondition 'freeable' got status unknown.
+[eva:alarm] tests/memory/memsize.c:30: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/memory/memsize.c:30: Warning: assertion got status unknown.
+[eva] tests/memory/memsize.c:33: Warning: ignoring unsupported \allocates clause
+[eva:alarm] tests/memory/memsize.c:33: Warning:
+ function realloc: precondition 'freeable' got status unknown.
+[eva:alarm] tests/memory/memsize.c:34: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/memory/memsize.c:34: Warning: assertion got status unknown.
+[eva] tests/memory/memsize.c:37: Warning: ignoring unsupported \allocates clause
+[eva:alarm] tests/memory/memsize.c:37: Warning:
+ function realloc: precondition 'freeable' got status unknown.
+[eva:alarm] tests/memory/memsize.c:39: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/memory/memsize.c:39: Warning: assertion got status unknown.
+[eva] tests/memory/memsize.c:42: Warning: ignoring unsupported \allocates clause
+[eva:alarm] tests/memory/memsize.c:43: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/memory/memsize.c:43: Warning: assertion got status unknown.
+[eva] tests/memory/memsize.c:46: Warning: ignoring unsupported \allocates clause
+[eva:alarm] tests/memory/memsize.c:47: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/memory/memsize.c:47: Warning: assertion got status unknown.
+[eva] tests/memory/memsize.c:50: Warning: ignoring unsupported \allocates clause
+[eva:alarm] tests/memory/memsize.c:51: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/memory/memsize.c:51: Warning: assertion got status unknown.
+[eva:alarm] tests/memory/memsize.c:52: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva] FRAMAC_SHARE/libc/stdlib.h:385: Warning:
+ no 'assigns \result \from ...' clause specified for function calloc
+[eva] tests/memory/memsize.c:55: Warning: ignoring unsupported \allocates clause
+[eva:alarm] tests/memory/memsize.c:56: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/memory/memsize.c:56: Warning: assertion got status unknown.
+[eva] tests/memory/memsize.c:60: Warning: ignoring unsupported \allocates clause
+[eva:alarm] tests/memory/memsize.c:61: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/memory/memsize.c:61: Warning: assertion got status unknown.
+[eva:alarm] tests/memory/memsize.c:62: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/memory/memsize.c:14: Warning: assertion got status unknown.
-[eva:alarm] tests/memory/memsize.c:16: Warning:
- function __e_acsl_assert: precondition got status invalid.