From_scratch (gillian.Engine.Abductor.From

Parameters

module SMemory : SMemory.S

module PC : 
  Gillian.Command_line.ParserAndCompiler.S
    with type init_data = SMemory.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