Source file wp_error.ml

(**************************************************************************)
(*                                                                        *)
(*  SPDX-License-Identifier LGPL-2.1                                      *)
(*  Copyright (C)                                                         *)
(*  CEA (Commissariat à l'énergie atomique et aux énergies alternatives)  *)
(*                                                                        *)
(**************************************************************************)

(* ------------------------------------------------------------------------ *)
(* ---  Exception Handling in WP                                        --- *)
(* ------------------------------------------------------------------------ *)

exception Error of string * string

let current = ref "wp"
let set_model m = current := m

let unsupported ?(model= !current) fmt =
  let b = Buffer.create 80 in
  Buffer.add_string b "unsupported " ;
  let kf fmt =
    Format.pp_print_flush fmt () ;
    raise (Error(model,Buffer.contents b))
  in Format.kfprintf kf (Format.formatter_of_buffer b) fmt

let not_yet_implemented ?(model= !current) fmt =
  let b = Buffer.create 80 in
  let kf fmt =
    Format.pp_print_string fmt " not yet implemented" ;
    Format.pp_print_flush fmt () ;
    raise (Error(model,Buffer.contents b))
  in Format.kfprintf kf (Format.formatter_of_buffer b) fmt

open Cil_types

let pp_logic_label fmt label =
  match label with
  | BuiltinLabel l -> Printer.pp_logic_builtin_label fmt l
  | FormalLabel s -> Format.pp_print_string fmt s
  | StmtLabel {contents=stmt} ->
    Format.pp_print_string fmt
      (let rec pickLabel = function
          | [] -> Printf.sprintf "__unknown_label_%d" stmt.sid
          | Label (l, _, _) :: _ -> l
          | _ :: rest -> pickLabel rest
       in pickLabel stmt.labels)

let pp_assigns fmt asgns =
  match asgns with
  | WritesAny -> Format.fprintf fmt "<undef>"
  | _ -> Format.fprintf fmt "@[<hov 2>%a@]" (Printer.pp_full_assigns "") asgns

let pp_string_list ?(sep=format_of_string "@ ") ~empty fmt l =
  match l with [] ->  Format.fprintf fmt "%s" empty
             | _ -> Format.fprintf fmt "%a"
                      (Pretty_utils.pp_list ~sep Format.pp_print_string) l

let name = function
  | [] -> ""
  | [x] -> x
  | x::xs ->
    let buffer = Buffer.create 80 in
    Buffer.add_string buffer x ;
    List.iter
      (fun y -> if y <> "" then
          ( Buffer.add_char buffer '-' ;
            Buffer.add_string buffer y )) xs ;
    Buffer.contents buffer