Make (gillian.Engine.Abductor.Make)

Parameters

module SPState : PState.S

module PC : 
  Gillian.Command_line.ParserAndCompiler.S
    with type init_data = SPState.init_data

module External : Engine.External.T(PC.Annot).S

Signature

type init_data = PC.init_data

type annot = PC.Annot.t

val test_prog : 
  init_data:init_data ->
  ?call_graph:Gillian.Utils.Call_graph.t ->
  annot MP.prog ->
  bool ->
  IncrementalAnalysis.SourceFiles.t option ->
  unit