From 907f516a09c392f24271951243cf495888cf322c Mon Sep 17 00:00:00 2001 From: Rob Lorch Date: Wed, 1 May 2024 10:05:44 -0500 Subject: [PATCH 1/2] Filter out props generated by abstract interpretation --- src/Kind2.ts | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/Kind2.ts b/src/Kind2.ts index 075d446..e188ca2 100644 --- a/src/Kind2.ts +++ b/src/Kind2.ts @@ -310,6 +310,10 @@ export class Kind2 implements TreeDataProvider, CodeLensProvider { for (const analysisResult of nodeResult.analyses) { let analysis: Analysis = new Analysis(analysisResult.abstract, analysisResult.concrete, component); for (const propertyResult of analysisResult.properties) { + // Filter out properties generated by abstract interpretation + if (propertyResult.source === 'Generated') { + continue + } let property = new Property(propertyResult.name, propertyResult.line - 1, propertyResult.file, analysis); switch (propertyResult.answer.value) { case "valid": From 6bb39ab244018c8e16c0548e9cfa759c8bf47ddf Mon Sep 17 00:00:00 2001 From: Rob Lorch Date: Mon, 6 May 2024 10:56:51 -0500 Subject: [PATCH 2/2] Filter out only candidate properties --- src/Kind2.ts | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Kind2.ts b/src/Kind2.ts index e188ca2..6217397 100644 --- a/src/Kind2.ts +++ b/src/Kind2.ts @@ -310,8 +310,8 @@ export class Kind2 implements TreeDataProvider, CodeLensProvider { for (const analysisResult of nodeResult.analyses) { let analysis: Analysis = new Analysis(analysisResult.abstract, analysisResult.concrete, component); for (const propertyResult of analysisResult.properties) { - // Filter out properties generated by abstract interpretation - if (propertyResult.source === 'Generated') { + // Filter out candidate properties + if (propertyResult.isCandidate === "true") { continue } let property = new Property(propertyResult.name, propertyResult.line - 1, propertyResult.file, analysis);