Organize methods for KCFG node creation #2575
Labels
Comments
|
@tothtamas28 can you update the description of this issue so we can process it properly in the KDev meeting? |
|
Closing in favor of batching this with other upstream changes: https://github.com/runtimeverification/erc20-verification/issues/431 |
h0nzZik
pushed a commit
to h0nzZik/k
that referenced
this issue
Nov 24, 2022
…untimeverification#1939) * haskell-backend/src/main/native/haskell-backend: 39a42a5a - Validate function definitions (runtimeverification#2168) * haskell-backend/src/main/native/haskell-backend: 97336086 - Issue 2100 follow up (runtimeverification#2574) * haskell-backend/src/main/native/haskell-backend: 5dcac768 - Update dependency: deps/k_release (runtimeverification#2576) * haskell-backend/src/main/native/haskell-backend: b16b0417 - NormalizedAc.concreteElements, InternalMap, InternalSet: use HashMap and HashSet (runtimeverification#2543) * haskell-backend/src/main/native/haskell-backend: 7330ab77 - Update regression tests (runtimeverification#2575) * haskell-backend/src/main/native/haskell-backend: fc0ae5f7 - Make SideCondition.assumeDefined total (runtimeverification#2577) * haskell-backend/src/main/native/haskell-backend: 37120f76 - Update dependency: deps/k_release (runtimeverification#2579) * haskell-backend/src/main/native/haskell-backend: ab0d48cb - Docker build update (runtimeverification#2578) * haskell-backend/src/main/native/haskell-backend: 314b81b6 - Remove outdated guidance for developers (#2563) * haskell-backend/src/main/native/haskell-backend: b199d525 - Revert function validation (runtimeverification#2582) * haskell-backend/src/main/native/haskell-backend: cb2c54e8 - Update dependency: deps/k_release (runtimeverification#2583) * haskell-backend/src/main/native/haskell-backend: 486dfd5d - kore-repl: call `warnIfLowProductivity` before throwing `ExitSuccess` or `ExitFailure` (runtimeverification#2581) * haskell-backend/src/main/native/haskell-backend: b0e48e43 - Trim source paths in regression tests (runtimeverification#2588) * haskell-backend/src/main/native/haskell-backend: 9686e3ca - Remove support for C semantics (#2598) * haskell-backend/src/main/native/haskell-backend: e439a425 - remove-import-groups.sh: Handle files without terminal newlines (runtimeverification#2590) * haskell-backend/src/main/native/haskell-backend: f77318a5 - Fix unparsing built-ins (runtimeverification#2540) * haskell-backend/src/main/native/haskell-backend: 1fede2ca - Use Makefile for generating regression tests (runtimeverification#2580) * haskell-backend/src/main/native/haskell-backend: 0362ccec - Update dependency: deps/k_release (runtimeverification#2600) * haskell-backend/src/main/native/haskell-backend: 8cf981da - Validate functions (runtimeverification#2585) * haskell-backend/src/main/native/haskell-backend: 9ef9184f - kore-0.45.0.0 (runtimeverification#2609) * haskell-backend/src/main/native/haskell-backend: 6c84752c - Distribute \next over \or in simplifier (runtimeverification#2608) * haskell-backend/src/main/native/haskell-backend: 8d69854d - Add location information to `WarnIfLowProductivity` (runtimeverification#2594) * haskell-backend/src/main/native/haskell-backend: d976c2d1 - kore-repl: add session commands when generating a bug report (runtimeverification#2614) * haskell-backend/src/main/native/haskell-backend: 81cf49ce - Keep Key attributes in KeyAttributes (runtimeverification#2603) * haskell-backend/src/main/native/haskell-backend: 9099b483 - Implement hooks string2base and base2string over 2 <= base <= 36 (runtimeverification#2618) * haskell-backend/src/main/native/haskell-backend: ba52e5fc - Update dependency: deps/k_release (runtimeverification#2613) * haskell-backend/src/main/native/haskell-backend: 7eaef393 - Update dependency: deps/k_release (runtimeverification#2622) * haskell-backend/src/main/native/haskell-backend: 3cb69096 - Overhaul pattern smart constructors (runtimeverification#2615) * haskell-backend/src/main/native/haskell-backend: 601f0cb5 - Move Attribute.Pattern to TermLike (runtimeverification#2607) * haskell-backend/src/main/native/haskell-backend: b39f7e86 - prelude.kore: Fix function equations for LLVM backend (runtimeverification#2629) * map-symbolic-tests-haskell/assignment-11-spec.k.out: Update results Co-authored-by: Thomas Tuegel <thomas.tuegel@runtimeverification.com> Co-authored-by: Thomas Tuegel <ttuegel@mailbox.org>
# for free
to join this conversation on GitHub.
Already have an account?
# to comment
Context: https://github.com/runtimeverification/erc20-verification/pull/425#discussion_r862659454
Potential solutions: in
pyk.kcfg.KCFG,get_or_create_node(node_id)(instead offind_or_create_node), orcreate_node(node_id, allow_exists=True),get_node(node_id) or create_node(node_id).Something to consider: before creating a node, it probably makes sense to check whether the node already exists (to handle the two cases accordingly, to avoid looping behavior, etc). If
create_nodedoes not raise an exception, this is not enforced.The text was updated successfully, but these errors were encountered: