Merge branch 'bugfix/basile/999-rtl-spec-merge' into 'master'

[eacsl] Merge contracts between RTL and stdlib

Closes #999

See merge request frama-c/frama-c!3032

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;*)

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. 

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));

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 ()
 
 (*

src/plugins/e-acsl/tests/memory/memsize.c

-/* run.config
+/* run.config_ci
    COMMENT: Checking heap memory size
+   STDOPT: +"-eva-no-builtins-auto"
 */
 
 #include <stdlib.h>

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)

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();

src/plugins/e-acsl/tests/memory/oracle_ci/memsize.res.oracle

 [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.