From 9b039ad60778c0b1faa498c437af0f3feee18218 Mon Sep 17 00:00:00 2001 From: Sadra Bayat Tork Date: Wed, 12 Mar 2025 17:41:35 +1000 Subject: [PATCH 1/3] set correct flags for jumptable test case --- src/test/scala/IntervalDSATest.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/test/scala/IntervalDSATest.scala b/src/test/scala/IntervalDSATest.scala index a2c5c1e93..67032afa4 100644 --- a/src/test/scala/IntervalDSATest.scala +++ b/src/test/scala/IntervalDSATest.scala @@ -40,7 +40,7 @@ class IntervalDSATest extends AnyFunSuite { staticAnalysis = None, boogieTranslation = BoogieGeneratorConfig(), outputPrefix = "boogie_out", - dsaConfig = Some(DSAConfig(Set.empty)) + dsaConfig = Some(DSAConfig(Set(Norm))) ) ) } From 7877cfec83294bb3d71fb0f4b22b383fa03c7946 Mon Sep 17 00:00:00 2001 From: Sadra Bayat Tork Date: Wed, 12 Mar 2025 17:42:14 +1000 Subject: [PATCH 2/3] ignore cloning recursive call resolution --- .../scala/analysis/data_structure_analysis/IntervalDSA.scala | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/main/scala/analysis/data_structure_analysis/IntervalDSA.scala b/src/main/scala/analysis/data_structure_analysis/IntervalDSA.scala index 4a854d486..b70052b4e 100644 --- a/src/main/scala/analysis/data_structure_analysis/IntervalDSA.scala +++ b/src/main/scala/analysis/data_structure_analysis/IntervalDSA.scala @@ -188,7 +188,7 @@ class IntervalGraph( callTransfer(phase, dcc, source, target) case dcc: DirectCallConstraint if dcc.target.name == "indirect_call_launchpad" => resolveIndirectCall(dcc) - .filterNot(proc => proc.isExternal.getOrElse(false) || proc.name.startsWith("_")) + .filterNot(proc => dcc.call.parent.parent == proc || proc.isExternal.getOrElse(false) || proc.name.startsWith("_")) .foreach(proc => val (source, target) = if phase == TD then (this, graphs(proc)) else (graphs(proc), this) @@ -238,6 +238,7 @@ class IntervalGraph( .exprToCells(sourceExpr) .map(source.find) .map(cell => + assert(cell.node.isUptoDate) val (node, offset) = target.findNode(cell.node.clone(target, true, oldToNew)) if offset == 0 then node.get(cell.interval) From cee36b6ee03a4a354239f85d4f2519035825b5b4 Mon Sep 17 00:00:00 2001 From: Sadra Bayat Tork Date: Wed, 12 Mar 2025 17:48:13 +1000 Subject: [PATCH 3/3] reformat --- .../scala/analysis/data_structure_analysis/IntervalDSA.scala | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/main/scala/analysis/data_structure_analysis/IntervalDSA.scala b/src/main/scala/analysis/data_structure_analysis/IntervalDSA.scala index b70052b4e..b03893459 100644 --- a/src/main/scala/analysis/data_structure_analysis/IntervalDSA.scala +++ b/src/main/scala/analysis/data_structure_analysis/IntervalDSA.scala @@ -188,7 +188,9 @@ class IntervalGraph( callTransfer(phase, dcc, source, target) case dcc: DirectCallConstraint if dcc.target.name == "indirect_call_launchpad" => resolveIndirectCall(dcc) - .filterNot(proc => dcc.call.parent.parent == proc || proc.isExternal.getOrElse(false) || proc.name.startsWith("_")) + .filterNot(proc => + dcc.call.parent.parent == proc || proc.isExternal.getOrElse(false) || proc.name.startsWith("_") + ) .foreach(proc => val (source, target) = if phase == TD then (this, graphs(proc)) else (graphs(proc), this)