<commit_before>(******************************************************************************)
(* Copyright (c) 2014-2017 ISPRAS (http://www.ispras.ru)                      *)
(* Institute for System Programming of the Russian Academy of Sciences        *)
(*                                                                            *)
(* Licensed under the Apache License, Version 2.0 (the "License");            *)
(* you may not use this file except in compliance with the License.           *)
(* You may obtain a copy of the License at                                    *)
(*                                                                            *)
(*     http://www.apache.org/licenses/LICENSE-2.0                             *)
(*                                                                            *)
(* Unless required by applicable law or agreed to in writing, software        *)
(* distributed under the License is distributed on an "AS IS" BASIS,          *)
(* WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.   *)
(* See the License for the specific language governing permissions and        *)
(* limitations under the License.                                             *)
(******************************************************************************)

include
  Plugin.Register
    (struct
       let name = "Crude_slicer"
       let shortname = "Crude_slicer"
       let help = "Crude slicer for preprocessing reachability verification tasks. Commit " ^ Version.commit ^
                  " compiled on " ^ Version.date
     end)

module Analysis =
  False
    (struct
      let option_name = "-crude_slicer"
      let help = "Perform crude slicing as preprocessing of a reachability verification task"
    end)

module Use_ghosts =
  False
    (struct
      let option_name = "-use_ghosts"
      let help = "Make sliced out statements ghost instead of removing them"
    end)

module Target_functions =
  Filled_string_set
    (struct
      let option_name = "-target_functions"
      let help = "Specify target (error) function name for reachability analysis"
      let arg_name = ""
      let default = Datatype.String.Set.of_list ["__VERIFIER_error"; "ldv_error"]
    end)

module Alloc_functions =
  Filled_string_set
    (struct
      let option_name = "-alloc_functions"
      let help = "Specify names of memory allocating functions"
      let arg_name = ""
      let default =
        Datatype.String.Set.of_list ["malloc"; "calloc"; "kmalloc"; "kzalloc";
                                     "ldv_malloc"; "ldv_zalloc"; "ldv_init_zalloc"]
    end)

module Required_bodies =
  Filled_string_set
    (struct
      let option_name = "-required_bodies"
      let help = "Special functions (allocation, error, assume...), which nontheless require implementations"
      let arg_name = ""
      let default =
        Datatype.String.Set.of_list ["ldv_error"; "ldv_assume"; "ldv_malloc"; "ldv_zalloc"; "ldv_init_zalloc"]
    end)

module Assume_functions =
  Filled_string_set<commit_msg>Fix: retain bodies of memory allocating functions, they can contain error locations!<commit_after>(******************************************************************************)
(* Copyright (c) 2014-2017 ISPRAS (http://www.ispras.ru)                      *)
(* Institute for System Programming of the Russian Academy of Sciences        *)
(*                                                                            *)
(* Licensed under the Apache License, Version 2.0 (the "License");            *)
(* you may not use this file except in compliance with the License.           *)
(* You may obtain a copy of the License at                                    *)
(*                                                                            *)
(*     http://www.apache.org/licenses/LICENSE-2.0                             *)
(*                                                                            *)
(* Unless required by applicable law or agreed to in writing, software        *)
(* distributed under the License is distributed on an "AS IS" BASIS,          *)
(* WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.   *)
(* See the License for the specific language governing permissions and        *)
(* limitations under the License.                                             *)
(******************************************************************************)

include
  Plugin.Register
    (struct
       let name = "Crude_slicer"
       let shortname = "Crude_slicer"
       let help = "Crude slicer for preprocessing reachability verification tasks. Commit " ^ Version.commit ^
                  " compiled on " ^ Version.date
     end)

module Analysis =
  False
    (struct
      let option_name = "-crude_slicer"
      let help = "Perform crude slicing as preprocessing of a reachability verification task"
    end)

module Use_ghosts =
  False
    (struct
      let option_name = "-use_ghosts"
      let help = "Make sliced out statements ghost instead of removing them"
    end)

module Target_functions =
  Filled_string_set
    (struct
      let option_name = "-target_functions"
      let help = "Specify target (error) function name for reachability analysis"
      let arg_name = ""
      let default = Datatype.String.Set.of_list ["__VERIFIER_error"; "ldv_error"]
    end)

module Alloc_functions =
  Filled_string_set
    (struct
      let option_name = "-alloc_functions"
      let help = "Specify names of memory allocating functions"
      let arg_name = ""
      let default =
        Datatype.String.Set.of_list ["malloc"; "calloc"; "kmalloc"; "kzalloc";
                                     "ldv_malloc"; "ldv_zalloc"; "ldv_init_zalloc"]
    end)

module Required_bodies =
  Filled_string_set
    (struct
      let option_name = "-required_bodies"
      let help = "Special functions (allocation, error, assume...), which nontheless require implementations"
      let arg_name = ""
      let default =
        Datatype.String.Set.of_list ["ldv_error"; "kmalloc"; "kzalloc";
                                     "ldv_assume"; "ldv_malloc"; "ldv_zalloc"; "ldv_init_zalloc"]
    end)

module Assume_functions =
  Filled_string_set
{'fraction_non_alphanumeric': 0.12977221687520052, 'fraction_numerical': 0.0038498556304138597, 'mean_word_length': 2.0106228874939642, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 3, 'https://': 0, 'lorem ipsum': 0, 'www.': 4, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 27, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '41936', 'n_tokens_mistral': 1553, 'n_tokens_neox': 1481, 'n_words': 496}