[Builtin] Adds calloc

headers/header_spec.txt

@@ -939,6 +939,8 @@ src/plugins/builtin/configure.ac: CEA_LGPL_OR_PROPRIETARY
 src/plugins/builtin/Makefile.in: CEA_LGPL_OR_PROPRIETARY
 src/plugins/builtin/stdlib/basic_alloc.ml: CEA_LGPL_OR_PROPRIETARY
 src/plugins/builtin/stdlib/basic_alloc.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/builtin/stdlib/calloc.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/builtin/stdlib/calloc.mli: CEA_LGPL_OR_PROPRIETARY
 src/plugins/builtin/stdlib/malloc.ml: CEA_LGPL_OR_PROPRIETARY
 src/plugins/builtin/stdlib/malloc.mli: CEA_LGPL_OR_PROPRIETARY
 src/plugins/builtin/string/memcmp.ml: CEA_LGPL_OR_PROPRIETARY

src/plugins/builtin/Makefile.in

@@ -38,6 +38,7 @@ SRC_STRING:=$(addprefix string/, $(SRC_STRING))
 
 SRC_STDLIB:= \
 	basic_alloc \
+	calloc \
 	malloc
 SRC_STDLIB:=$(addprefix stdlib/, $(SRC_STDLIB))
 

src/plugins/builtin/stdlib/calloc.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of Frama-C.                                         *)
+(*                                                                        *)
+(*  Copyright (C) 2007-2019                                               *)
+(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
+(*         alternatives)                                                  *)
+(*                                                                        *)
+(*  you can redistribute it and/or modify it under the terms of the GNU   *)
+(*  Lesser General Public License as published by the Free Software       *)
+(*  Foundation, version 2.1.                                              *)
+(*                                                                        *)
+(*  It is distributed in the hope that it will be useful,                 *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
+(*  GNU Lesser General Public License for more details.                   *)
+(*                                                                        *)
+(*  See the GNU Lesser General Public License version 2.1                 *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+open Basic_blocks
+open Basic_alloc
+open Cil_types
+open Logic_const
+
+let function_name = "calloc"
+
+let pset_len_to_zero ?loc ptr_type len =
+  let result = tresult ?loc ptr_type in
+  let eq_value ?loc t =
+    let value = match t.term_type with
+      | Ctype(TPtr(_)) -> term Tnull t.term_type
+      | Ctype(TFloat(_)) -> treal ?loc 0.
+      | Ctype(TInt(_)) -> tinteger ?loc 0
+      | _ -> assert false
+    in
+    prel ?loc (Req, t, value)
+  in
+  let p = punfold_all_elems_pred ?loc result len eq_value in
+  new_predicate { p with pred_name = [ "zero_initialization" ] }
+
+let pinitialized_len ?loc ptr_type len =
+  let result = tresult ?loc ptr_type in
+  let initialized ?loc t = pinitialized ?loc (here_label, t) in
+  let p = punfold_all_elems_pred ?loc result len initialized in
+  new_predicate { p with pred_name = [ "initialization" ] }
+
+let generate_requires loc ptr_type len =
+  [ new_predicate
+      { (pcorrect_len_bytes ~loc ptr_type len)
+        with pred_name = ["aligned_end"] } ]
+
+let generate_global_assigns loc ptr_type num size =
+  let assigns_result = assigns_result ~loc ptr_type [ num ; size ] in
+  let assigns_heap = assigns_heap [ num ; size ] in
+  Writes [ assigns_result ; assigns_heap ]
+
+let make_behavior_allocation loc ptr_type num size =
+  let len = term ~loc (TBinOp(Mult, num, size)) Linteger in
+  let assumes = [ is_allocable ~loc len ] in
+  let assigns = generate_global_assigns loc ptr_type num size in
+  let alloc   = allocates_result ~loc ptr_type in
+  let ensures = [
+    Normal, fresh_result ~loc ptr_type len ;
+    Normal, pset_len_to_zero ~loc ptr_type num ;
+    Normal, pinitialized_len ~loc ptr_type num
+  ] in
+  make_behavior ~name:"allocation" ~assumes ~assigns ~alloc ~ensures ()
+
+let make_behavior_no_allocation loc ptr_type num size =
+  let len = term ~loc (TBinOp(Mult, num, size)) Linteger in
+  let assumes = [ isnt_allocable ~loc len ] in
+  let assigns = Writes [assigns_result ~loc ptr_type []] in
+  let ensures = [ Normal, null_result ~loc ptr_type ] in
+  let alloc = allocates_nothing () in
+  make_behavior ~name:"no_allocation" ~assumes ~assigns ~ensures ~alloc ()
+
+let generate_spec alloc_typ { svar = vi } loc =
+  let (cnum, csize) = match Cil.getFormalsDecl vi with
+    | [ cnum ; csize ] -> cnum, csize
+    | _ -> assert false
+  in
+  let num = tlogic_coerce ~loc (cvar_to_tvar cnum) Linteger in
+  let size = tlogic_coerce ~loc (cvar_to_tvar csize) Linteger in
+  let requires = generate_requires loc (Ctype (ptr_of alloc_typ)) size in
+  let assigns = generate_global_assigns loc (ptr_of alloc_typ) num size in
+  let alloc = allocates_result ~loc (ptr_of alloc_typ) in
+  make_funspec [
+    make_behavior ~requires ~assigns ~alloc () ;
+    make_behavior_allocation loc (ptr_of alloc_typ) num size ;
+    make_behavior_no_allocation loc (ptr_of alloc_typ) num size
+  ] ()
+
+let generate_prototype alloc_t =
+  let name = function_name ^ "_" ^ (string_of_typ alloc_t) in
+  let params = [
+    ("num", size_t (), []) ;
+    ("size", size_t (), [])
+  ] in
+  name, (TFun((ptr_of alloc_t), Some params, false, []))
+
+let well_typed_call ret args =
+  match ret, args with
+  | Some ret, [ _ ; _ ] -> Cil.isPointerType (Cil.typeOfLval ret)
+  | _ -> false
+
+let key_from_call ret _ =
+  match ret with
+  | Some ret ->
+    let ret_t = Cil.unrollTypeDeep (Cil.typeOfLval ret) in
+    let ret_t = Cil.type_remove_qualifier_attributes_deep ret_t in
+    Cil.typeOf_pointed ret_t
+  | None -> assert false
+
+let retype_args _typ args = args
+let args_for_original _typ fd =
+  List.map Cil.evar fd.sformals
+
+let () = Transform.register (module struct
+    module Hashtbl = Cil_datatype.Typ.Hashtbl
+    type override_key = typ
+
+    let function_name = function_name
+    let well_typed_call = well_typed_call
+    let key_from_call = key_from_call
+    let retype_args = retype_args
+    let generate_prototype = generate_prototype
+    let generate_spec = generate_spec
+    let args_for_original = args_for_original
+  end)

src/plugins/builtin/stdlib/calloc.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of Frama-C.                                         *)
+(*                                                                        *)
+(*  Copyright (C) 2007-2019                                               *)
+(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
+(*         alternatives)                                                  *)
+(*                                                                        *)
+(*  you can redistribute it and/or modify it under the terms of the GNU   *)
+(*  Lesser General Public License as published by the Free Software       *)
+(*  Foundation, version 2.1.                                              *)
+(*                                                                        *)
+(*  It is distributed in the hope that it will be useful,                 *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
+(*  GNU Lesser General Public License for more details.                   *)
+(*                                                                        *)
+(*  See the GNU Lesser General Public License version 2.1                 *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
+(*                                                                        *)
+(**************************************************************************)