Skip to content

Commit

Permalink
Add Printable.Failwith for Analyses.control_spec_c initial value
Browse files Browse the repository at this point in the history
  • Loading branch information
sim642 committed Jul 28, 2022
1 parent fc45f2c commit e4812fc
Show file tree
Hide file tree
Showing 2 changed files with 33 additions and 1 deletion.
25 changes: 25 additions & 0 deletions src/domains/printable.ml
Original file line number Diff line number Diff line change
Expand Up @@ -567,6 +567,31 @@ struct
end


module type FailwithMessage =
sig
val message: string
end

module Failwith (Message: FailwithMessage): S =
struct
type t = |

let name () = "failwith"
let equal _ _ = failwith Message.message
let compare _ _ = failwith Message.message
let hash _ = failwith Message.message
let tag _ = failwith Message.message

let show _ = failwith Message.message
let pretty _ _ = failwith Message.message
let printXml _ _ = failwith Message.message
let to_yojson _ = failwith Message.message

let arbitrary _ = failwith Message.message
let relift _ = failwith Message.message
end


(** Concatenates a list of strings that
fit in the given character constraint *)
let get_short_list begin_str end_str list =
Expand Down
9 changes: 8 additions & 1 deletion src/framework/analyses.ml
Original file line number Diff line number Diff line change
Expand Up @@ -269,8 +269,15 @@ struct
end


let control_spec_c: (module Printable.S) ref = ref (module Printable.Unit: Printable.S) (* TODO: some failing printable instead *)
(** Reference to top-level Control Spec context first-class module. *)
let control_spec_c: (module Printable.S) ref =
let module Failwith = Printable.Failwith (
struct
let message = "uninitialized control_spec_c"
end
)
in
ref (module Failwith: Printable.S)

(** Top-level Control Spec context as static module, which delegates to {!control_spec_c}.
This allows using top-level context values inside individual analyses. *)
Expand Down

0 comments on commit e4812fc

Please sign in to comment.