diff --git a/src/plugins/instantiate/global_context.ml b/src/plugins/instantiate/global_context.ml
index d28b409a52f87647dc991fddbd57582cf79928a2..9a6d4ff32d6ff6cf6e9e7c9b37db0e9bfb726fc7 100644
--- a/src/plugins/instantiate/global_context.ml
+++ b/src/plugins/instantiate/global_context.ml
@@ -21,19 +21,70 @@
(**************************************************************************)
module Table = Datatype.String.Hashtbl
-let table = Table.create 13
+
+let varinfos = Table.create 13
+let logic_functions = Table.create 13
+let axiomatics = Table.create 13
let get_variable name make =
- if Table.mem table name then Table.find table name
+ if Table.mem varinfos name then Table.find varinfos name
else begin
try Globals.Vars.find_from_astinfo name VGlobal
with Not_found ->
let vi = make () in
- Table.add table name vi ;
+ Table.add varinfos name vi ;
vi
end
-let clear () = Table.clear table
+let get_logic_function name make =
+ if Table.mem logic_functions name then Table.find logic_functions name
+ else begin
+ match Logic_env.find_all_logic_functions name with
+ | [] ->
+ let li = make () in
+ Table.add logic_functions name li ;
+ Logic_utils.add_logic_function li ;
+ li
+ | [x] -> x
+ | _ :: _ -> Options.not_yet_implemented "Logic function overloading"
+ end
+
+let in_axiomatic_functions = Table.create 13
+
+let get_logic_function_in_axiomatic name make =
+ if Table.mem in_axiomatic_functions name then
+ Table.find in_axiomatic_functions name
+ else begin
+ let make_then_find name =
+ let open Cil_types in
+ let (ax_name, ax_list), functions = make () in
+ List.iter
+ (fun f ->
+ Table.add in_axiomatic_functions f.l_var_info.lv_name f ;
+ Logic_utils.add_logic_function f)
+ functions ;
+ Table.add axiomatics ax_name ax_list ;
+ Table.find in_axiomatic_functions name
+ in
+ try match Logic_env.find_all_logic_functions name with
+ | [] -> make_then_find name
+ | [x] -> x
+ | _ :: _ -> Options.not_yet_implemented "Logic function overloading"
+ with Not_found ->
+ Options.fatal "Failed to build %s" name
+ end
+
+let clear () = Table.clear varinfos
let globals loc =
- Table.fold (fun _ x l -> Cil_types.GVarDecl(x, loc) :: l) table []
+ let open Cil_types in
+ let l = [] in
+ let l =
+ Table.fold (fun _ x l -> GVarDecl(x, loc) :: l) varinfos l
+ in
+ let annot x loc = GAnnot(x, loc) in
+ let fun_or_pred x loc = annot (Dfun_or_pred (x, loc)) loc in
+ let axiomatic name list loc = annot(Daxiomatic(name, list, [], loc)) loc in
+ let l = Table.fold (fun _ x l -> fun_or_pred x loc :: l) logic_functions l in
+ let l = Table.fold (fun n x l -> axiomatic n x loc :: l) axiomatics l in
+ l
\ No newline at end of file
diff --git a/src/plugins/instantiate/global_context.mli b/src/plugins/instantiate/global_context.mli
index 66e600361950f022101b39f1a09e106b89eab7a4..89f3a2124493da562f1fb01dd8e955b37b3f1f6a 100644
--- a/src/plugins/instantiate/global_context.mli
+++ b/src/plugins/instantiate/global_context.mli
@@ -22,8 +22,8 @@
open Cil_types
-(** The purpose of this module is to create global variables when it is needed
- by instantiation modules.
+(** The purpose of this module global definitions when it is needed by
+ instantiation modules.
*)
(** [get_variable name f] searches for an existing variable [name]. If this
@@ -34,6 +34,30 @@ open Cil_types
*)
val get_variable: string -> (unit -> varinfo) -> varinfo
+(** [get_logic_function name f] searches for an existing logic function [name].
+ If this function does not exists, it is created using [f]. If the logic
+ function must be part of an axiomatic block **DO NOT** use this function,
+ use [get_logic_function_in_axiomatic].
+
+ Note that function overloading is not supported.
+*)
+val get_logic_function: string -> (unit -> logic_info) -> logic_info
+
+(** [get_logic_function_in_axiomatic name f] searches for an existing logic
+ function [name]. If this function does not exists, an axiomatic definition
+ is created using [f].
+
+ [f] must return:
+ - the axiomatic in a form [name, list of the defintions (incl. functions)]
+ - all functions that are part of the axiomatic definition
+
+ Note that function overloading is not supported.
+*)
+val get_logic_function_in_axiomatic:
+ string ->
+ (unit -> (string * global_annotation list) * logic_info list) ->
+ logic_info
+
(** Clears internal tables *)
val clear: unit -> unit
diff --git a/src/plugins/instantiate/stdlib/basic_alloc.ml b/src/plugins/instantiate/stdlib/basic_alloc.ml
index ec54907d18f893e63fe77b54ebaa0d4dde15ecb5..3f9ced7c231c90ccc69f6782abddb0d012d47790 100644
--- a/src/plugins/instantiate/stdlib/basic_alloc.ml
+++ b/src/plugins/instantiate/stdlib/basic_alloc.ml
@@ -47,19 +47,6 @@ let valid_size ?loc typ size =
in
new_predicate { p with pred_name = ["correct_size"] }
-let pis_allocable ?loc size =
- let is_allocable = Logic_env.find_all_logic_functions "is_allocable" in
- let is_allocable = as_singleton is_allocable in
- papp ?loc (is_allocable, [here_label], [size])
-
-let is_allocable ?loc size =
- let p = pis_allocable ?loc size in
- new_predicate { p with pred_name = [ "allocable" ]}
-
-let isnt_allocable ?loc size =
- let p = pnot ?loc (pis_allocable ?loc size) in
- new_predicate { p with pred_name = [ "allocable" ]}
-
let heap_status () =
let name = "__fc_heap_status" in
let make () =
@@ -70,6 +57,55 @@ let heap_status () =
let vi = Global_context.get_variable name make in
Basic_blocks.cvar_to_tvar vi
+let make_is_allocable () =
+ let name = "is_allocable" in
+ {
+ l_var_info = Cil_const.make_logic_var_global name (Ctype Cil.voidType) ;
+ l_type = None ;
+ l_tparams = [];
+ l_labels = [FormalLabel("L")];
+ l_profile = [Cil_const.make_logic_var_formal "i" Linteger] ;
+ l_body = LBreads [new_identified_term (heap_status())];
+ }
+
+let make_axiomatic_is_allocable loc () =
+ let is_allocable = make_is_allocable () in
+ let lv_i = Cil_const.make_logic_var_quant "i" Linteger in
+ let t_i = tvar lv_i in
+ let zero = tinteger 0 in
+ let max =
+ tinteger
+ (Integer.to_int
+ (Cil.max_unsigned_number (Cil.bitsSizeOf (size_t ()))))
+ in
+ let label = FormalLabel("L") in
+ let cond = pand (prel (Rlt, t_i, zero), prel (Rgt, t_i, max)) in
+ let app = pnot (papp (is_allocable,[label],[t_i])) in
+ let prop = pforall ([lv_i], pimplies (cond, app)) in
+ let gfun = Dfun_or_pred(is_allocable, loc) in
+ let axiom = Dlemma("never_allocable", true, [label],[],prop,[], loc) in
+ ("dynamic_allocation", [gfun ; axiom]), [is_allocable]
+
+let get_is_allocable loc =
+ Global_context.get_logic_function_in_axiomatic
+ "is_allocable" (make_axiomatic_is_allocable loc)
+
+let pis_allocable ?loc size =
+ let loc = match loc with
+ | None -> Cil_datatype.Location.unknown
+ | Some l -> l
+ in
+ let is_allocable = get_is_allocable loc in
+ papp ~loc (is_allocable, [here_label], [size])
+
+let is_allocable ?loc size =
+ let p = pis_allocable ?loc size in
+ new_predicate { p with pred_name = [ "allocable" ]}
+
+let isnt_allocable ?loc size =
+ let p = pnot ?loc (pis_allocable ?loc size) in
+ new_predicate { p with pred_name = [ "allocable" ]}
+
let assigns_result ?loc typ deps =
let heap_status = new_identified_term (heap_status ()) in
let deps = match deps with
diff --git a/src/plugins/instantiate/string/mem_utils.mli b/src/plugins/instantiate/string/mem_utils.mli
index a6bbb923b7c7a39ff64c7ce5233de5abb414d4a1..2a580c48732ada81908001ff088e88858048da53 100644
--- a/src/plugins/instantiate/string/mem_utils.mli
+++ b/src/plugins/instantiate/string/mem_utils.mli
@@ -32,7 +32,7 @@ module type Function = sig
val prototype: unit -> proto
- (** receives the type of the lvalue and the types of the arguments recieved
+ (** receives the type of the lvalue and the types of the arguments received
for a call to the function and returns [true] iff they are correct.
The received types depend on the [prototype] of the module.
- if the kind is [Data t] -> it is the exact type of the expr/lvalue
diff --git a/src/plugins/instantiate/tests/stdlib/no_fc_stdlib.c b/src/plugins/instantiate/tests/stdlib/no_fc_stdlib.c
new file mode 100644
index 0000000000000000000000000000000000000000..21498c2ef2b5ab29516316267bc33c5af6d46bbd
--- /dev/null
+++ b/src/plugins/instantiate/tests/stdlib/no_fc_stdlib.c
@@ -0,0 +1,12 @@
+#include <stddef.h>
+
+void* malloc(size_t s);
+void* calloc(size_t num, size_t size);
+void free(void* ptr);
+
+void foo(void){
+ int * p = malloc(sizeof(int));
+ int * q = calloc(2, sizeof(int));
+ free(p);
+ free(q);
+}
\ No newline at end of file
diff --git a/src/plugins/instantiate/tests/stdlib/oracle/no_fc_stdlib.res.oracle b/src/plugins/instantiate/tests/stdlib/oracle/no_fc_stdlib.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..baa036c870fb4e23d59d27155db86156ea9f5bfb
--- /dev/null
+++ b/src/plugins/instantiate/tests/stdlib/oracle/no_fc_stdlib.res.oracle
@@ -0,0 +1,253 @@
+[kernel] Parsing tests/stdlib/no_fc_stdlib.c (with preprocessing)
+/* Generated by Frama-C */
+#include "stddef.h"
+/*@ ghost extern int __fc_heap_status; */
+
+/*@
+axiomatic dynamic_allocation {
+ predicate is_allocable{L}(ℤ i)
+ reads __fc_heap_status;
+
+ axiom never_allocable{L}:
+ ∀ ℤ i; i < 0 ∧ i > 4294967295 ⇒ ¬is_allocable(i);
+
+ }
+
+*/
+void *malloc(size_t s);
+
+void *calloc(size_t num, size_t size);
+
+void free(void *ptr);
+
+/*@ requires freeable: ptr ≡ \null ∨ \freeable(ptr);
+ assigns __fc_heap_status;
+ assigns __fc_heap_status \from __fc_heap_status, ptr;
+ frees ptr;
+
+ behavior allocation:
+ assumes ptr ≢ \null;
+ ensures freed: \allocable(ptr);
+ assigns __fc_heap_status;
+ assigns __fc_heap_status \from __fc_heap_status, ptr;
+ frees ptr;
+
+ behavior no_allocation:
+ assumes ptr ≡ \null;
+ assigns \nothing;
+ allocates \nothing;
+
+ complete behaviors no_allocation, allocation;
+ disjoint behaviors no_allocation, allocation;
+ */
+void free_int(int *ptr)
+{
+ free((void *)ptr);
+ return;
+}
+
+/*@ requires correct_size: 0 ≡ size % 4;
+ assigns \result, __fc_heap_status;
+ assigns \result \from __fc_heap_status, num, size;
+ assigns __fc_heap_status \from __fc_heap_status, num, size;
+ allocates \result;
+
+ behavior allocation:
+ assumes allocable: is_allocable(num * size);
+ ensures fresh_result: \fresh{Old, Here}(\result,num * size);
+ ensures
+ zero_initialization:
+ ∀ ℤ j0; 0 ≤ j0 < num ⇒ *(\result + j0) ≡ 0;
+ ensures
+ initialization:
+ ∀ ℤ j0; 0 ≤ j0 < num ⇒ \initialized(\result + j0);
+ assigns \result, __fc_heap_status;
+ assigns \result \from __fc_heap_status, num, size;
+ assigns __fc_heap_status \from __fc_heap_status, num, size;
+ allocates \result;
+
+ behavior no_allocation:
+ assumes allocable: ¬is_allocable(num * size);
+ ensures null_result: \result ≡ \null;
+ assigns \result;
+ assigns \result \from \nothing;
+ allocates \nothing;
+
+ complete behaviors no_allocation, allocation;
+ disjoint behaviors no_allocation, allocation;
+ */
+int *calloc_int(size_t num, size_t size)
+{
+ int *__retres;
+ __retres = (int *)calloc(num,size);
+ return __retres;
+}
+
+/*@ requires correct_size: 0 ≡ size % 4;
+ assigns \result, __fc_heap_status;
+ assigns \result \from __fc_heap_status, size;
+ assigns __fc_heap_status \from __fc_heap_status, size;
+ allocates \result;
+
+ behavior allocation:
+ assumes allocable: is_allocable(size);
+ ensures fresh_result: \fresh{Old, Here}(\result,size);
+ assigns \result, __fc_heap_status;
+ assigns \result \from __fc_heap_status, size;
+ assigns __fc_heap_status \from __fc_heap_status, size;
+ allocates \result;
+
+ behavior no_allocation:
+ assumes allocable: ¬is_allocable(size);
+ ensures null_result: \result ≡ \null;
+ assigns \result;
+ assigns \result \from \nothing;
+ allocates \nothing;
+
+ complete behaviors no_allocation, allocation;
+ disjoint behaviors no_allocation, allocation;
+ */
+int *malloc_int(size_t size)
+{
+ int *__retres;
+ __retres = (int *)malloc(size);
+ return __retres;
+}
+
+void foo(void)
+{
+ int *p = malloc_int(sizeof(int));
+ int *q = calloc_int((unsigned int)2,sizeof(int));
+ free_int(p);
+ free_int(q);
+ return;
+}
+
+
+[kernel] Parsing tests/stdlib/result/no_fc_stdlib.c (with preprocessing)
+/* Generated by Frama-C */
+#include "stddef.h"
+/*@ ghost extern int __fc_heap_status; */
+
+/*@
+axiomatic dynamic_allocation {
+ predicate is_allocable{L}(ℤ i)
+ reads __fc_heap_status;
+
+ axiom never_allocable{L}:
+ ∀ ℤ i; i < 0 ∧ i > 4294967295 ⇒ ¬is_allocable(i);
+
+ }
+
+*/
+void *malloc(size_t s);
+
+void *calloc(size_t num, size_t size);
+
+void free(void *ptr);
+
+/*@ requires freeable: ptr ≡ \null ∨ \freeable(ptr);
+ assigns __fc_heap_status;
+ assigns __fc_heap_status \from __fc_heap_status, ptr;
+ frees ptr;
+
+ behavior allocation:
+ assumes ptr ≢ \null;
+ ensures freed: \allocable(\old(ptr));
+ assigns __fc_heap_status;
+ assigns __fc_heap_status \from __fc_heap_status, ptr;
+ frees ptr;
+
+ behavior no_allocation:
+ assumes ptr ≡ \null;
+ assigns \nothing;
+ allocates \nothing;
+
+ complete behaviors no_allocation, allocation;
+ disjoint behaviors no_allocation, allocation;
+ */
+void free_int(int *ptr)
+{
+ free((void *)ptr);
+ return;
+}
+
+/*@ requires correct_size: 0 ≡ size % 4;
+ assigns \result, __fc_heap_status;
+ assigns \result \from __fc_heap_status, num, size;
+ assigns __fc_heap_status \from __fc_heap_status, num, size;
+ allocates \result;
+
+ behavior allocation:
+ assumes allocable: is_allocable(num * size);
+ ensures
+ fresh_result: \fresh{Old, Here}(\result,\old(num) * \old(size));
+ ensures
+ zero_initialization:
+ ∀ ℤ j0; 0 ≤ j0 < \old(num) ⇒ *(\result + j0) ≡ 0;
+ ensures
+ initialization:
+ ∀ ℤ j0; 0 ≤ j0 < \old(num) ⇒ \initialized(\result + j0);
+ assigns \result, __fc_heap_status;
+ assigns \result \from __fc_heap_status, num, size;
+ assigns __fc_heap_status \from __fc_heap_status, num, size;
+ allocates \result;
+
+ behavior no_allocation:
+ assumes allocable: ¬is_allocable(num * size);
+ ensures null_result: \result ≡ \null;
+ assigns \result;
+ assigns \result \from \nothing;
+ allocates \nothing;
+
+ complete behaviors no_allocation, allocation;
+ disjoint behaviors no_allocation, allocation;
+ */
+int *calloc_int(size_t num, size_t size)
+{
+ int *__retres;
+ __retres = (int *)calloc(num,size);
+ return __retres;
+}
+
+/*@ requires correct_size: 0 ≡ size % 4;
+ assigns \result, __fc_heap_status;
+ assigns \result \from __fc_heap_status, size;
+ assigns __fc_heap_status \from __fc_heap_status, size;
+ allocates \result;
+
+ behavior allocation:
+ assumes allocable: is_allocable(size);
+ ensures fresh_result: \fresh{Old, Here}(\result,\old(size));
+ assigns \result, __fc_heap_status;
+ assigns \result \from __fc_heap_status, size;
+ assigns __fc_heap_status \from __fc_heap_status, size;
+ allocates \result;
+
+ behavior no_allocation:
+ assumes allocable: ¬is_allocable(size);
+ ensures null_result: \result ≡ \null;
+ assigns \result;
+ assigns \result \from \nothing;
+ allocates \nothing;
+
+ complete behaviors no_allocation, allocation;
+ disjoint behaviors no_allocation, allocation;
+ */
+int *malloc_int(size_t size)
+{
+ int *__retres;
+ __retres = (int *)malloc(size);
+ return __retres;
+}
+
+void foo(void)
+{
+ int *p = malloc_int(sizeof(int));
+ int *q = calloc_int((unsigned int)2,sizeof(int));
+ free_int(p);
+ free_int(q);
+ return;
+}
+
+