Skip to content

Commit

Permalink
Clean alias for utility_context in SymbolicUtility
Browse files Browse the repository at this point in the history
  • Loading branch information
benozol committed Apr 9, 2020
1 parent 6b85408 commit 5a53b0f
Show file tree
Hide file tree
Showing 4 changed files with 13 additions and 16 deletions.
13 changes: 6 additions & 7 deletions src/symbolic/symbolicUtility.ml
Original file line number Diff line number Diff line change
Expand Up @@ -315,12 +315,6 @@ module MakeInterpreter (Filesystem: FILESYSTEM) = struct
end
end

module UtilityContext = struct
type context = utility_context = {
cwd: Path.normal;
env: string Env.SMap.t;
args: string list;
}
end

(* Constraints *)
Expand Down Expand Up @@ -434,6 +428,12 @@ module Mixed = struct
include MakeInterpreter (MixedImplementation)
include MakeSpecifications (MixedImplementation)

type context = utility_context = {
cwd: Path.normal;
env: string Env.SMap.t;
args: string list;
}

let state_from_constraints (s : Constraints.state) : state = {
filesystem=MixedImplementation.Constraints s.filesystem;
stdin=s.stdin;
Expand Down Expand Up @@ -486,7 +486,6 @@ end
module ConstraintsCompatibility = struct

include Mixed
include UtilityContext

let success_case ~descr ?stdout constraints =
success_case ~descr ?stdout (case_spec ~constraints ())
Expand Down
13 changes: 6 additions & 7 deletions src/symbolic/symbolicUtility.mli
Original file line number Diff line number Diff line change
Expand Up @@ -199,12 +199,6 @@ module MakeInterpreter (Filesystem: FILESYSTEM) : sig
end
end

module UtilityContext : sig
type context = utility_context = {
cwd: Path.normal;
env: string Env.SMap.t;
args: string list;
}
end

(** {1 Constraints backend} *)
Expand Down Expand Up @@ -288,6 +282,12 @@ module Mixed : sig
include module type of MakeInterpreter (MixedImplementation)
include module type of MakeSpecifications (MixedImplementation)

type context = utility_context = {
cwd: Path.normal;
env: string Env.SMap.t;
args: string list;
}

(** Symbolically interprete a program using the constraints backend *)
val interp_program_constraints : input -> Constraints.sym_state list -> program -> (Constraints.state list * Constraints.state list * Constraints.state list)

Expand All @@ -299,7 +299,6 @@ end
engine: Create mixed utilities with the interface of constraints-based utilities *)
module ConstraintsCompatibility : sig
include module type of Mixed
include module type of UtilityContext

val success_case: descr:string -> ?stdout:Stdout.t -> Constraints.case_spec -> case
val error_case: descr:string -> ?stdout:Stdout.t -> ?error_message:string -> Constraints.case_spec -> case
Expand Down
1 change: 0 additions & 1 deletion src/symbolic/utilities/mkdir.ml
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
open Format
open Colis_constraints
open Clause
open SymbolicUtility.UtilityContext
open SymbolicUtility.Mixed

let name = "mkdir"
Expand Down
2 changes: 1 addition & 1 deletion src/symbolic/utilities/mkdir.mli
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
(** Symbolic execution of mkdir *)
open SymbolicUtility.ConstraintsCompatibility
open SymbolicUtility.Mixed

val name : string
val interprete : context -> utility

0 comments on commit 5a53b0f

Please sign in to comment.