This repository was archived by the owner on Apr 25, 2024. It is now read-only.

More simplifications to the KCFG class#503

Merged

ehildenb merged 34 commits intomasterfrom

kcfg-remove-target

Jun 20, 2023

Commits on Jun 19, 2023

kcfg/kcfg: KCFG.prune takes list of nodes to keep, not keep_target and keep_init
ehildenb
committed
proof/reachability: update how pending sets are calculated to use predicates
ehildenb
committed
kcfg/kcfg: simplify definition of KCFG.is_init and KCFG.is_leaf
ehildenb
committed
kcfg/: remove notion of KCFG.frontier, replace with uses of KCFG.leaves
ehildenb
committed
kcfg/kcfg: remove explicit KCFG._init set
ehildenb
committed
kcfg/show: remove some special handling of target in KCFGShow.pretty_segments
ehildenb
committed
kcfg/show: factor out KCFGShow.make_unique_segments for ensuring unique segment ids
ehildenb
committed
kcfg/show: do not pass in cfgid to KCFG.{show,to_module}, instead pass in module_name directly
ehildenb
committed
kcfg/kcfg: move method path_length as static method KCFG.path_length
ehildenb
committed
kast/{manip,pretty}, kcfg/show: make it so sort_ac_collections does not need KDefinition
ehildenb
committed
kcfg/{kcfg,show}: add KCFG.to_module, and use in KCFGShow.show
ehildenb
committed
kcfg/{kcfg,explore,show}, proof/reachability: remove expanded notion in favor of stuck
ehildenb
committed
proof/show: add APRProofShow class for displaying APRProof
ehildenb
committed
kcfg/show: make sure to write dot source, not dot directly
ehildenb
committed
kcfg/{kcfg,show}, proof/reachability: remove notion of target nodes
ehildenb
committed
proof/reachability: remove redundant check for is_covered in pending sets
ehildenb
committed
Merge 36477fb601192ce5cc8308111d5b43fab5a85399 into b1f057583b4fb335b68258a5b6278ebb8f12b1f7
ehildenb
authored
Set Version: 0.1.338
rv-auditor
committed
kcfg/show: allow omitting cells in module production in KCFGShow as well
ehildenb
committed
proof/show: formatting
ehildenb
committed
kcfg/show: slighly more spacing on node printing
ehildenb
committed
src/tests/integration/kcfg/test_imp: correct test for terminal/stuck
ehildenb
committed
.github/test-pr: upgrade from macos-11 => macos-13
ehildenb
committed
Merge branch 'master' into kcfg-remove-target
ehildenb
authored
Merge 84f6167e0583dadec0bf8f60a9251fcfe325fede into be262783d22ac29ab7c65d91b0658c56449497bb
ehildenb
authored
Set Version: 0.1.340
rv-auditor
committed

Commits

Commits on Jun 19, 2023

Commits on Jun 20, 2023