Skip to content
Snippets Groups Projects
Select Git revision
  • master default protected
  • stable/zinc protected
  • stable/copper protected
  • stable/nickel protected
  • stable/cobalt protected
  • stable/iron protected
  • stable/manganese protected
  • stable/chromium protected
  • stable/titanium protected
  • 0.8
  • 0.8-beta
  • 0.7
  • 0.6
  • 0.5.1
  • 0.5
  • feature-callee-assigns
  • 0.5-beta
  • 0.4
  • 0.4-beta
  • pre-dune
  • 0.3
  • 2022-03-23
  • 0.2
  • 24.0-beta
  • 0.1.2
  • 0.1.1
  • 0.1
  • compat-fc-22.0-beta-1
  • compat-fc-22.0-beta
29 results
Blame Permalink
meta_run.mli 2.02 KiB 
(**************************************************************************)
(*                                                                        *)
(*  This file is part of the Frama-C's MetACSL plug-in.                   *)
(*                                                                        *)
(*  Copyright (C) 2018-2022                                               *)
(*    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 LICENSE)                       *)
(*                                                                        *)
(**************************************************************************)

(** main entry point *)

(** generate a new project in which the HILARE have been instantiated according
    to the given flags.
*)
val generate: Meta_options.meta_flags -> Project.t


(** same as above, but each option can be set individually. *)
val translate:
  ?check_external:bool ->
  ?simpl: bool ->
  ?target_set: Meta_utils.StrSet.t ->
  ?number_assertions: bool ->
  ?prefix_meta: bool ->
  ?static_bindings: int ->
  unit ->
  Project.t