Documentation

Strata.Backends.CBMC.GOTO.CoreToCProverGOTO

source
structure CoreToGOTO.CProverGOTO.Json :
Type
Instances For
    source
    def CoreToGOTO.CProverGOTO.Context.toJson (programName : String) (ctx : Context) :
    Except String Json
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def CoreToGOTO.getGotoJson (programName : String) (env : StrataDDM.Program) :
      IO CProverGOTO.Json
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def CoreToGOTO.writeToGotoJson (programName symTabFileName gotoFileName : String) (env : StrataDDM.Program) :
        IO Unit
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For