search

runtimeverification / k

K Framework Tools 7.0
BSD 3-Clause "New" or "Revised" License
430 stars 141 forks source link

Pyk crash when accessing kompiled definition #4475

Open Baltoli opened 1 week ago

Baltoli commented 1 week ago

A user on Discord reports a crash in Pyk:

module PROGRAM-SYNTAX
    syntax Exp

    syntax Stmt ::= 
        "start" Exp "middle" Exp "end"    [seqstrict(1, 2)] 

    syntax KResult

endmodule

module PROGRAM
    imports PROGRAM-SYNTAX

endmodule
from pyk.ktool.kprove  import KProve
from pyk.ktool.kompile import HaskellKompile, KompileArgs
from pathlib           import Path

source_dir   = '/home/alex/repos_from2024/k/kprover/records/'
main_file    = source_dir + '/program.k'
kompiled_dir = source_dir + '/program-kompile2/'

base_args    = KompileArgs(main_file = main_file)
kompile      = HaskellKompile(base_args=base_args)    
kompile_res  = kompile.__call__(output_dir=kompiled_dir)

kprove = KProve(Path(kompiled_dir))
kprove.definition

I haven't triaged this at all; not sure what's happening.