From 519826e51f0887747ba913f1ec08669d2d740162 Mon Sep 17 00:00:00 2001 From: nick_battle Date: Sat, 28 Oct 2023 20:41:37 +0100 Subject: [PATCH 1/8] Allow annotated exp/stmts to be suspended for QC --- .../vdmj/in/annotations/INAnnotatedExpression.java | 11 +++++++++-- .../vdmj/in/annotations/INAnnotatedStatement.java | 11 +++++++++-- .../com/fujitsu/vdmj/plugins/commands/PogCommand.java | 10 +++++++--- 3 files changed, 25 insertions(+), 7 deletions(-) diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/in/annotations/INAnnotatedExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/in/annotations/INAnnotatedExpression.java index b33242fe9..8ac9e1715 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/in/annotations/INAnnotatedExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/in/annotations/INAnnotatedExpression.java @@ -37,6 +37,8 @@ public class INAnnotatedExpression extends INExpression public final INAnnotation annotation; public final INExpression expression; + private static boolean suspended = false; + public INAnnotatedExpression(LexLocation location, INAnnotation annotation, INExpression expression) { super(location); @@ -50,13 +52,18 @@ public String toString() return annotation + " " + expression; } + public static void suspend(boolean flag) + { + suspended = flag; + } + @Override public Value eval(Context ctxt) { breakpoint.check(location, ctxt); - annotation.inBefore(this, ctxt); + if (!suspended) annotation.inBefore(this, ctxt); Value rv = expression.eval(ctxt); - annotation.inAfter(this, rv, ctxt); + if (!suspended) annotation.inAfter(this, rv, ctxt); return rv; } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/in/annotations/INAnnotatedStatement.java b/vdmj/src/main/java/com/fujitsu/vdmj/in/annotations/INAnnotatedStatement.java index 1d29492b4..6e977da10 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/in/annotations/INAnnotatedStatement.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/in/annotations/INAnnotatedStatement.java @@ -37,6 +37,8 @@ public class INAnnotatedStatement extends INStatement public final INAnnotation annotation; public final INStatement statement; + private static boolean suspended = false; + public INAnnotatedStatement(LexLocation location, INAnnotation annotation, INStatement statement) { super(location); @@ -50,13 +52,18 @@ public String toString() return annotation + " " + statement; } + public static void suspend(boolean flag) + { + suspended = flag; + } + @Override public Value eval(Context ctxt) { breakpoint.check(location, ctxt); - annotation.inBefore(this, ctxt); + if (!suspended) annotation.inBefore(this, ctxt); Value rv = statement.eval(ctxt); - annotation.inAfter(this, rv, ctxt); + if (!suspended) annotation.inAfter(this, rv, ctxt); return rv; } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/plugins/commands/PogCommand.java b/vdmj/src/main/java/com/fujitsu/vdmj/plugins/commands/PogCommand.java index 904fa2c6c..e4bcee908 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/plugins/commands/PogCommand.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/plugins/commands/PogCommand.java @@ -35,7 +35,7 @@ public class PogCommand extends AnalysisCommand { - private final static String USAGE = "Usage: pog [ | | ]"; + private final static String USAGE = "Usage: pog [ | | ]"; public PogCommand(String line) { @@ -58,9 +58,9 @@ public String run(String line) { list = all; } - else + else if (argv.length == 2) { - String match = line.substring(line.indexOf(' ') + 1); + String match = argv[1]; list = new ProofObligationList(); for (ProofObligation obligation: all) @@ -73,6 +73,10 @@ public String run(String line) } } } + else + { + return USAGE; + } if (list.isEmpty()) { From fe7b7eeee8949a7737a0ff8e0f031f3c7f8e6a82 Mon Sep 17 00:00:00 2001 From: nick_battle Date: Sat, 28 Oct 2023 20:42:03 +0100 Subject: [PATCH 2/8] Suspend annotated exp/stmt during QC --- .../src/main/java/quickcheck/QuickCheck.java | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/examples/quickcheck/src/main/java/quickcheck/QuickCheck.java b/examples/quickcheck/src/main/java/quickcheck/QuickCheck.java index 2de1b1864..a8376dabe 100644 --- a/examples/quickcheck/src/main/java/quickcheck/QuickCheck.java +++ b/examples/quickcheck/src/main/java/quickcheck/QuickCheck.java @@ -39,6 +39,8 @@ import com.fujitsu.vdmj.Settings; import com.fujitsu.vdmj.ast.lex.LexBooleanToken; import com.fujitsu.vdmj.in.INNode; +import com.fujitsu.vdmj.in.annotations.INAnnotatedExpression; +import com.fujitsu.vdmj.in.annotations.INAnnotatedStatement; import com.fujitsu.vdmj.in.definitions.INClassDefinition; import com.fujitsu.vdmj.in.expressions.INBooleanLiteralExpression; import com.fujitsu.vdmj.in.expressions.INExpression; @@ -456,6 +458,12 @@ else if (results.provedBy != null) do { ictxt.next(); + + // Suspend annotation execution by the interpreter, because the + // expressions and statements in the PO can invoke them. + INAnnotatedExpression.suspend(true); + INAnnotatedStatement.suspend(true); + execResult = poexp.eval(ictxt); } while (ictxt.hasNext() && execResult.boolValue(ctxt)); @@ -472,6 +480,11 @@ else if (results.provedBy != null) exception = e; } } + finally + { + INAnnotatedExpression.suspend(false); + INAnnotatedStatement.suspend(false); + } long after = System.currentTimeMillis() + results.duration; From 8964644be90114ca3e7765eb9ce97ca1b97cc1d0 Mon Sep 17 00:00:00 2001 From: nick_battle Date: Sun, 29 Oct 2023 09:34:44 +0000 Subject: [PATCH 3/8] Tweak pog help --- .../main/java/com/fujitsu/vdmj/plugins/commands/PogCommand.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/plugins/commands/PogCommand.java b/vdmj/src/main/java/com/fujitsu/vdmj/plugins/commands/PogCommand.java index e4bcee908..74d25e034 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/plugins/commands/PogCommand.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/plugins/commands/PogCommand.java @@ -108,6 +108,6 @@ else if (argv.length == 2) public static void help() { - println("pog [] - generate proof obligations"); + println("pog [ | | ] - generate proof obligations"); } } From 6c140489c43f62ce8f6be53e2793bd3ed1425680 Mon Sep 17 00:00:00 2001 From: nick_battle Date: Sun, 29 Oct 2023 10:33:05 +0000 Subject: [PATCH 4/8] Include counterexamples and message in PO JSON response --- .../main/java/workspace/plugins/POPlugin.java | 25 ++++++++++++++++--- 1 file changed, 22 insertions(+), 3 deletions(-) diff --git a/lsp/src/main/java/workspace/plugins/POPlugin.java b/lsp/src/main/java/workspace/plugins/POPlugin.java index f7871e85f..29771807b 100644 --- a/lsp/src/main/java/workspace/plugins/POPlugin.java +++ b/lsp/src/main/java/workspace/plugins/POPlugin.java @@ -30,6 +30,7 @@ import com.fujitsu.vdmj.mapper.Mappable; import com.fujitsu.vdmj.pog.ProofObligation; import com.fujitsu.vdmj.pog.ProofObligationList; +import com.fujitsu.vdmj.tc.lex.TCNameToken; import json.JSONArray; import json.JSONObject; @@ -183,14 +184,32 @@ else if (file.isDirectory()) name.add(part); } - results.add( - new JSONObject( + JSONObject json = new JSONObject( "id", Long.valueOf(po.number), "kind", po.kind.toString(), "name", name, "location", Utils.lexLocationToLocation(po.location), "source", splitPO(po.value), - "status", po.status.toString())); + "status", po.status.toString()); + + if (!po.counterexample.isEmpty()) + { + JSONObject values = new JSONObject(); + + for (TCNameToken vname: po.counterexample.keySet()) + { + values.put(vname.getName(), po.counterexample.get(vname).toString()); + } + + json.put("counterexample", values); + } + + if (po.countermessage != null) + { + json.put("message", po.countermessage); + } + + results.add(json); } return results; From dceccefc6621dc6ce0a6b833c8178a3b9516ec8c Mon Sep 17 00:00:00 2001 From: nick_battle Date: Sun, 29 Oct 2023 11:39:29 +0000 Subject: [PATCH 5/8] Set annotated exp/stmt types in constructor --- .../com/fujitsu/vdmj/po/annotations/POAnnotatedExpression.java | 1 + .../com/fujitsu/vdmj/po/annotations/POAnnotatedStatement.java | 1 + 2 files changed, 2 insertions(+) diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/annotations/POAnnotatedExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/annotations/POAnnotatedExpression.java index c5d1a3fcf..84afe927d 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/annotations/POAnnotatedExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/annotations/POAnnotatedExpression.java @@ -43,6 +43,7 @@ public POAnnotatedExpression(LexLocation location, POAnnotation annotation, POEx super(location); this.annotation = (annotation != null) ? annotation : new PONoAnnotation(); this.expression = expression; + setExptype(expression.getExptype()); } @Override diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/annotations/POAnnotatedStatement.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/annotations/POAnnotatedStatement.java index add72d1d3..0b04f6f2d 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/annotations/POAnnotatedStatement.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/annotations/POAnnotatedStatement.java @@ -43,6 +43,7 @@ public POAnnotatedStatement(LexLocation location, POAnnotation annotation, POSta super(location); this.annotation = (annotation != null) ? annotation : new PONoAnnotation(); this.statement = statement; + setStmttype(statement.getStmttype()); } @Override From 756f8fe4ee35516ceaff8f08f13735d539283754 Mon Sep 17 00:00:00 2001 From: nick_battle Date: Sun, 29 Oct 2023 12:03:54 +0000 Subject: [PATCH 6/8] Fix POs with annotations --- .../src/main/java/quickcheck/QuickCheck.java | 9 +++------ .../vdmj/in/annotations/INAnnotatedExpression.java | 11 ++--------- .../vdmj/in/annotations/INAnnotatedStatement.java | 11 ++--------- .../com/fujitsu/vdmj/in/annotations/INAnnotation.java | 9 ++++++++- .../vdmj/po/annotations/POAnnotatedExpression.java | 2 +- .../vdmj/po/annotations/POAnnotatedStatement.java | 2 +- .../com/fujitsu/vdmj/pog/ProofObligationList.java | 8 +++++--- 7 files changed, 22 insertions(+), 30 deletions(-) diff --git a/examples/quickcheck/src/main/java/quickcheck/QuickCheck.java b/examples/quickcheck/src/main/java/quickcheck/QuickCheck.java index a8376dabe..b02f7730b 100644 --- a/examples/quickcheck/src/main/java/quickcheck/QuickCheck.java +++ b/examples/quickcheck/src/main/java/quickcheck/QuickCheck.java @@ -39,8 +39,7 @@ import com.fujitsu.vdmj.Settings; import com.fujitsu.vdmj.ast.lex.LexBooleanToken; import com.fujitsu.vdmj.in.INNode; -import com.fujitsu.vdmj.in.annotations.INAnnotatedExpression; -import com.fujitsu.vdmj.in.annotations.INAnnotatedStatement; +import com.fujitsu.vdmj.in.annotations.INAnnotation; import com.fujitsu.vdmj.in.definitions.INClassDefinition; import com.fujitsu.vdmj.in.expressions.INBooleanLiteralExpression; import com.fujitsu.vdmj.in.expressions.INExpression; @@ -461,8 +460,7 @@ else if (results.provedBy != null) // Suspend annotation execution by the interpreter, because the // expressions and statements in the PO can invoke them. - INAnnotatedExpression.suspend(true); - INAnnotatedStatement.suspend(true); + INAnnotation.suspend(true); execResult = poexp.eval(ictxt); } @@ -482,8 +480,7 @@ else if (results.provedBy != null) } finally { - INAnnotatedExpression.suspend(false); - INAnnotatedStatement.suspend(false); + INAnnotation.suspend(false); } long after = System.currentTimeMillis() + results.duration; diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/in/annotations/INAnnotatedExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/in/annotations/INAnnotatedExpression.java index 8ac9e1715..c46c02b5b 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/in/annotations/INAnnotatedExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/in/annotations/INAnnotatedExpression.java @@ -37,8 +37,6 @@ public class INAnnotatedExpression extends INExpression public final INAnnotation annotation; public final INExpression expression; - private static boolean suspended = false; - public INAnnotatedExpression(LexLocation location, INAnnotation annotation, INExpression expression) { super(location); @@ -52,18 +50,13 @@ public String toString() return annotation + " " + expression; } - public static void suspend(boolean flag) - { - suspended = flag; - } - @Override public Value eval(Context ctxt) { breakpoint.check(location, ctxt); - if (!suspended) annotation.inBefore(this, ctxt); + if (!INAnnotation.suspended) annotation.inBefore(this, ctxt); Value rv = expression.eval(ctxt); - if (!suspended) annotation.inAfter(this, rv, ctxt); + if (!INAnnotation.suspended) annotation.inAfter(this, rv, ctxt); return rv; } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/in/annotations/INAnnotatedStatement.java b/vdmj/src/main/java/com/fujitsu/vdmj/in/annotations/INAnnotatedStatement.java index 6e977da10..afdf748f9 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/in/annotations/INAnnotatedStatement.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/in/annotations/INAnnotatedStatement.java @@ -37,8 +37,6 @@ public class INAnnotatedStatement extends INStatement public final INAnnotation annotation; public final INStatement statement; - private static boolean suspended = false; - public INAnnotatedStatement(LexLocation location, INAnnotation annotation, INStatement statement) { super(location); @@ -52,18 +50,13 @@ public String toString() return annotation + " " + statement; } - public static void suspend(boolean flag) - { - suspended = flag; - } - @Override public Value eval(Context ctxt) { breakpoint.check(location, ctxt); - if (!suspended) annotation.inBefore(this, ctxt); + if (!INAnnotation.suspended) annotation.inBefore(this, ctxt); Value rv = statement.eval(ctxt); - if (!suspended) annotation.inAfter(this, rv, ctxt); + if (!INAnnotation.suspended) annotation.inAfter(this, rv, ctxt); return rv; } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/in/annotations/INAnnotation.java b/vdmj/src/main/java/com/fujitsu/vdmj/in/annotations/INAnnotation.java index f35f0c0a3..4e9fb3a1c 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/in/annotations/INAnnotation.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/in/annotations/INAnnotation.java @@ -49,7 +49,9 @@ public abstract class INAnnotation extends INNode implements MappingOptional public final INExpressionList args; private static final Set> declared = new HashSet>(); - private static final List instances = new Vector(); + private static final List instances = new Vector(); + + public static boolean suspended = false; public INAnnotation(TCIdentifierToken name, INExpressionList args) { @@ -65,6 +67,11 @@ public static void reset() declared.clear(); instances.clear(); } + + public static void suspend(boolean flag) + { + suspended = flag; // Used in INAnnotatedExpression and Statement + } public static void init(Context ctxt) { diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/annotations/POAnnotatedExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/annotations/POAnnotatedExpression.java index 84afe927d..72da7110c 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/annotations/POAnnotatedExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/annotations/POAnnotatedExpression.java @@ -49,7 +49,7 @@ public POAnnotatedExpression(LexLocation location, POAnnotation annotation, POEx @Override public String toString() { - return "/* " + annotation + " */ " + expression; + return expression.toString(); // Don't include annotation in PO sources } @Override diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/annotations/POAnnotatedStatement.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/annotations/POAnnotatedStatement.java index 0b04f6f2d..07f9f019a 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/annotations/POAnnotatedStatement.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/annotations/POAnnotatedStatement.java @@ -49,7 +49,7 @@ public POAnnotatedStatement(LexLocation location, POAnnotation annotation, POSta @Override public String toString() { - return "/* " + annotation + " */ " + statement; + return statement.toString(); // Don't include annotation in PO source } @Override diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligationList.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligationList.java index 93d637ad5..426e90d1a 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligationList.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligationList.java @@ -174,10 +174,12 @@ private void typeCheck(ProofObligation obligation, String mname, Environment env LexTokenReader ltr = new LexTokenReader(obligation.getValue(), Settings.dialect); ExpressionReader reader = new ExpressionReader(ltr); reader.setCurrentModule(mname); - boolean old = Properties.parser_maximal_types; - Properties.parser_maximal_types = true; // For parse of PO on inv_T2 + + boolean oldmax = Properties.parser_maximal_types; + Properties.parser_maximal_types = true; // For parse of PO on inv_T(T!) ASTExpression ast = reader.readExpression(); - Properties.parser_maximal_types = old; + Properties.parser_maximal_types = oldmax; + LexToken end = ltr.getLast(); if (!end.is(Token.EOF)) From 29a1e57d1c79c3ff9591b1796a9f1ddf747238dd Mon Sep 17 00:00:00 2001 From: nick_battle Date: Sun, 29 Oct 2023 19:09:43 +0000 Subject: [PATCH 7/8] Send PO counterexample messages with POG --- .../java/workspace/LSPXWorkspaceManager.java | 2 -- lsp/src/main/java/workspace/MessageHub.java | 14 --------- .../main/java/workspace/plugins/POPlugin.java | 31 ++++++++++++++++++- 3 files changed, 30 insertions(+), 17 deletions(-) diff --git a/lsp/src/main/java/workspace/LSPXWorkspaceManager.java b/lsp/src/main/java/workspace/LSPXWorkspaceManager.java index bb99c96fb..c3f092108 100644 --- a/lsp/src/main/java/workspace/LSPXWorkspaceManager.java +++ b/lsp/src/main/java/workspace/LSPXWorkspaceManager.java @@ -121,7 +121,6 @@ public void enablePlugins() throws Exception Method factory = clazz.getMethod("factory", Dialect.class); AnalysisPlugin instance = (AnalysisPlugin)factory.invoke(null, Settings.dialect); registry.registerPlugin(instance); - messagehub.addPlugin(instance); Diag.info("Registered LSPX plugin %s", plugin); } catch (NoSuchMethodException e) // Try default constructor @@ -137,7 +136,6 @@ public void enablePlugins() throws Exception Constructor ctor = clazz.getConstructor(); AnalysisPlugin instance = (AnalysisPlugin) ctor.newInstance(); registry.registerPlugin(instance); - messagehub.addPlugin(instance); Diag.info("Registered LSPX plugin %s", plugin); } catch (Throwable th) diff --git a/lsp/src/main/java/workspace/MessageHub.java b/lsp/src/main/java/workspace/MessageHub.java index 8028168f4..df27b955d 100644 --- a/lsp/src/main/java/workspace/MessageHub.java +++ b/lsp/src/main/java/workspace/MessageHub.java @@ -78,20 +78,6 @@ public static void reset() } } - /** - * This is used by the LSPX workspace manager to add new lspx.plugins. - */ - public synchronized void addPlugin(AnalysisPlugin plugin) - { - for (File file: messageMap.keySet()) - { - Map> pmap = messageMap.get(file); - pmap.put(plugin.getName(), new HashSet()); - } - - Diag.info("Added plugin %s to MessageHub", plugin.getName()); - } - /** * This is used by the workspace manager to populate a blank plugin map for a * new file. diff --git a/lsp/src/main/java/workspace/plugins/POPlugin.java b/lsp/src/main/java/workspace/plugins/POPlugin.java index 29771807b..ea39b28ab 100644 --- a/lsp/src/main/java/workspace/plugins/POPlugin.java +++ b/lsp/src/main/java/workspace/plugins/POPlugin.java @@ -25,9 +25,15 @@ package workspace.plugins; import java.io.File; +import java.util.HashSet; +import java.util.List; +import java.util.Set; +import java.util.Vector; import com.fujitsu.vdmj.lex.Dialect; import com.fujitsu.vdmj.mapper.Mappable; +import com.fujitsu.vdmj.messages.VDMMessage; +import com.fujitsu.vdmj.messages.VDMWarning; import com.fujitsu.vdmj.pog.ProofObligation; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.tc.lex.TCNameToken; @@ -152,9 +158,12 @@ protected JSONArray splitPO(String value) public JSONArray getObligations(File file) { ProofObligationList poGeneratedList = getProofObligations(); - poGeneratedList.renumber(); JSONArray results = new JSONArray(); + messagehub.clearPluginMessages(this); + List messages = new Vector(); + Set errFiles = new HashSet(); + for (ProofObligation po: poGeneratedList) { if (file != null) @@ -202,16 +211,36 @@ else if (file.isDirectory()) } json.put("counterexample", values); + + StringBuilder sb = new StringBuilder("Counterexample: "); + String sep = ""; + + for (TCNameToken vname: po.counterexample.keySet()) + { + sb.append(sep); + sb.append(vname.getName()); + sb.append(" = "); + sb.append(po.counterexample.get(vname)); + sep = ", "; + } + + messages.add(new VDMWarning(9000, sb.toString(), po.location)); + errFiles.add(po.location.file); } if (po.countermessage != null) { json.put("message", po.countermessage); + messages.add(new VDMWarning(9001, po.countermessage, po.location)); + errFiles.add(po.location.file); } results.add(json); } + messagehub.addPluginMessages(this, messages); + results.addAll(messagehub.getDiagnosticResponses(errFiles)); + return results; } } From b58c0bb8f9557c574288129bbb6c930493ee1d38 Mon Sep 17 00:00:00 2001 From: nick_battle Date: Sun, 29 Oct 2023 22:31:07 +0000 Subject: [PATCH 8/8] Update POPlugin to send notifications correctly, and lsp.sh --- .../main/java/workspace/plugins/POPlugin.java | 25 ++++++++++++++++--- lsp/src/main/scripts/lsp.sh | 3 ++- .../fujitsu/vdmj/pog/ProofObligationList.java | 2 +- 3 files changed, 24 insertions(+), 6 deletions(-) diff --git a/lsp/src/main/java/workspace/plugins/POPlugin.java b/lsp/src/main/java/workspace/plugins/POPlugin.java index ea39b28ab..b5ed49862 100644 --- a/lsp/src/main/java/workspace/plugins/POPlugin.java +++ b/lsp/src/main/java/workspace/plugins/POPlugin.java @@ -25,6 +25,7 @@ package workspace.plugins; import java.io.File; +import java.io.IOException; import java.util.HashSet; import java.util.List; import java.util.Set; @@ -40,6 +41,7 @@ import json.JSONArray; import json.JSONObject; +import lsp.LSPServer; import lsp.Utils; import rpc.RPCMessageList; import rpc.RPCRequest; @@ -212,7 +214,10 @@ else if (file.isDirectory()) json.put("counterexample", values); - StringBuilder sb = new StringBuilder("Counterexample: "); + StringBuilder sb = new StringBuilder(); + sb.append("PO #"); + sb.append(po.number); + sb.append(" counterexample: "); String sep = ""; for (TCNameToken vname: po.counterexample.keySet()) @@ -230,7 +235,7 @@ else if (file.isDirectory()) if (po.countermessage != null) { - json.put("message", po.countermessage); + json.put("message", "PO #" + po.number + ": " + po.countermessage); messages.add(new VDMWarning(9001, po.countermessage, po.location)); errFiles.add(po.location.file); } @@ -239,8 +244,20 @@ else if (file.isDirectory()) } messagehub.addPluginMessages(this, messages); - results.addAll(messagehub.getDiagnosticResponses(errFiles)); + RPCMessageList errs = messagehub.getDiagnosticResponses(errFiles); - return results; + for (JSONObject err: errs) + { + try + { + LSPServer.getInstance().writeMessage(err); + } + catch (IOException e) + { + Diag.error(e); + } + } + + return results; // Just POG display results } } diff --git a/lsp/src/main/scripts/lsp.sh b/lsp/src/main/scripts/lsp.sh index 8723272f0..a6386804b 100755 --- a/lsp/src/main/scripts/lsp.sh +++ b/lsp/src/main/scripts/lsp.sh @@ -54,8 +54,9 @@ VDMJ_JAR=$MAVENREPO/vdmj/${VERSION}/vdmj-${VERSION}.jar ANNOTATIONS_JAR=$MAVENREPO/annotations/${VERSION}/annotations-${VERSION}.jar LSP_JAR=$MAVENREPO/lsp/${VERSION}/lsp-${VERSION}.jar STDLIB_JAR=$MAVENREPO/stdlib/${VERSION}/stdlib-${VERSION}.jar +QUICKCHECK_JAR=$MAVENREPO/quickcheck/${VERSION}/quickcheck-${VERSION}.jar exec java ${JAVA64_VMOPTS} \ - -cp $VDMJ_JAR:$ANNOTATIONS_JAR:$LSP_JAR:$STDLIB_JAR \ + -cp $VDMJ_JAR:$ANNOTATIONS_JAR:$LSP_JAR:$STDLIB_JAR:$QUICKCHECK_JAR \ lsp.LSPServerDebug $DIALECT -lsp 8000 -dap 8001 diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligationList.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligationList.java index 426e90d1a..3057a6193 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligationList.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligationList.java @@ -215,7 +215,7 @@ private void typeCheck(ProofObligation obligation, String mname, Environment env iter.remove(); obligation.status = POStatus.FAILED; obligation.isCheckable = false; - obligation.countermessage = "Error: Missing measure function"; + obligation.countermessage = "PO #" + obligation.number + ": Missing measure function"; } break;