From d3981bf3ae87d3b2b2d91a8cb3e4c7f4ff6fbc26 Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Mon, 13 Nov 2023 10:17:42 +0100 Subject: [PATCH] Parse poison values as non-deterministic values (#565) Signed-off-by: Hernan Ponce de Leon Co-authored-by: Hernan Ponce de Leon --- .../dartagnan/parsers/program/visitors/VisitorLlvm.java | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLlvm.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLlvm.java index f13a110ee6..26b9583332 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLlvm.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLlvm.java @@ -865,6 +865,12 @@ public Expression visitArrayConst(ArrayConstContext ctx) { return expressions.makeArray(elementType, arrayValues, true); } + @Override + public Expression visitPoisonConst(PoisonConstContext ctx) { + // It is correct to replace a poison value with an undef value or any value of the type. + return makeNonDetOfType(expectedType); + } + @Override public Expression visitStructConst(StructConstContext ctx) { List structMembers = new ArrayList<>();