Skip to content

Commit

Permalink
Fixes
Browse files Browse the repository at this point in the history
  • Loading branch information
keyboardDrummer committed Jul 1, 2024
1 parent d623f3d commit ee992ed
Show file tree
Hide file tree
Showing 4 changed files with 12 additions and 4 deletions.
2 changes: 2 additions & 0 deletions Source/AbstractInterpretation/NativeLattice.cs
Original file line number Diff line number Diff line change
Expand Up @@ -379,6 +379,8 @@ NativeLattice.Element Step(NativeLattice lattice, Cmd cmd, NativeLattice.Element
}
else if (cmd is HideRevealCmd) {
// skip
} else if (cmd is ChangeScope) {
// skip
}
else
{
Expand Down
3 changes: 3 additions & 0 deletions Source/Core/AST/HideRevealCmd.cs
Original file line number Diff line number Diff line change
Expand Up @@ -29,6 +29,9 @@ public override void Typecheck(TypecheckingContext tc)

public override void Emit(TokenTextWriter stream, int level)
{
stream.Write(this, level, Hide ? "hide " : "reveal ");
stream.Write(this, level, Function == null ? "*" : Function.Name);
stream.WriteLine(";");
}

public override void AddAssignedVariables(List<Variable> vars)
Expand Down
8 changes: 6 additions & 2 deletions Source/Graph/Graph.cs
Original file line number Diff line number Diff line change
Expand Up @@ -1182,18 +1182,22 @@ public static IEnumerable<object> FindReachableNodesInGraphWithMergeNodes(
continue;
}


IReadOnlyList<object> parents;
if (node is IEnumerable<object> objects) {
if (!visitedEdges.IsSupersetOf(objects)) {
continue;
}

parents = objects.ToList();
} else {
parents = new[] { node };
}
visitedEdges.Add(node);

var outgoing = edges.GetValueOrDefault(node) ?? new List<object>();
foreach (var child in outgoing)
{
if (visitChild != null && !visitChild(node, child))
if (visitChild != null && parents.Any(p => !visitChild(p, child)))
{
continue;
}
Expand Down
3 changes: 1 addition & 2 deletions Source/VCGeneration/Prune/DataflowAnalysis.cs
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@
using System.Linq;

abstract class DataflowAnalysis<TNode, TState> {
protected readonly Dictionary<TNode, TState> states;
protected readonly Dictionary<TNode, TState> states = new();
protected readonly Dictionary<TNode, TState> inStates = new();
private readonly Func<TNode, IEnumerable<TNode>> getNext;
private readonly Func<TNode, IEnumerable<TNode>> getPrevious;
Expand All @@ -15,7 +15,6 @@ protected DataflowAnalysis(IReadOnlyList<TNode> roots,
this.getNext = getNext;
this.getPrevious = getPrevious;
this.roots = roots;
states = roots.ToDictionary(n => n, n => Empty);
}

public IReadOnlyDictionary<TNode, TState> States => states;
Expand Down

0 comments on commit ee992ed

Please sign in to comment.