Report invariants enforced by vacuous requirements #675
+152
−0
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,58 @@ | ||
| /* | ||
| * Copyright (C) 2024 University of Freiburg | ||
|
There was a problem hiding this comment. Please also add your name and email address if you create a new file. |
||
| * | ||
| * This file is part of the ULTIMATE PEAtoBoogie plug-in. | ||
| * | ||
| * The ULTIMATE PEAtoBoogie plug-in is free software: you can redistribute it and/or modify | ||
| * it under the terms of the GNU Lesser General Public License as published | ||
| * by the Free Software Foundation, either version 3 of the License, or | ||
| * (at your option) any later version. | ||
| * | ||
| * The ULTIMATE PEAtoBoogie plug-in is distributed in the hope that it will be useful, | ||
| * but WITHOUT ANY WARRANTY; without even the implied warranty of | ||
| * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the | ||
| * GNU Lesser General Public License for more details. | ||
| * | ||
| * You should have received a copy of the GNU Lesser General Public License | ||
| * along with the ULTIMATE PEAtoBoogie plug-in. If not, see <http://www.gnu.org/licenses/>. | ||
| * | ||
| * Additional permission under GNU GPL version 3 section 7: | ||
| * If you modify the ULTIMATE PEAtoBoogie plug-in, or any covered work, by linking | ||
| * or combining it with Eclipse RCP (or a modified version of Eclipse RCP), | ||
| * containing parts covered by the terms of the Eclipse Public License, the | ||
| * licensors of the ULTIMATE PEAtoBoogie plug-in grant you additional permission | ||
| * to convey the resulting work. | ||
| */ | ||
| package de.uni_freiburg.informatik.ultimate.pea2boogie.results; | ||
|
|
||
| import de.uni_freiburg.informatik.ultimate.core.model.models.IElement; | ||
| import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.structure.IAction; | ||
| import de.uni_freiburg.informatik.ultimate.lib.pea.CDD; | ||
| import de.uni_freiburg.informatik.ultimate.util.CoreUtil; | ||
|
|
||
|
|
||
| public final class ReqCheckVacuousResult<LOC extends IElement, TE extends IAction, E> | ||
| extends ReqCheckFailResult<LOC> { | ||
|
|
||
| private final String mEnforcedInvariant; | ||
|
|
||
| public ReqCheckVacuousResult(final LOC element, final String plugin, final String enforcedInvariant) { | ||
| super(element, plugin); | ||
| mEnforcedInvariant = enforcedInvariant; | ||
| } | ||
|
|
||
| public ReqCheckVacuousResult(final LOC element, final String plugin) { | ||
| this(element, plugin, null); | ||
| } | ||
|
|
||
| @Override | ||
| public String getLongDescription() { | ||
| final StringBuilder sb = new StringBuilder(); | ||
| sb.append(getShortDescription()); | ||
| if (mEnforcedInvariant != CDD.TRUE.toString()) { | ||
|
There was a problem hiding this comment. Check for null instead of CDD.TRUE.toString(), and move stringbuilder into the if, e.g.: |
||
| sb.append(CoreUtil.getPlatformLineSeparator()); | ||
| sb.append("Vacous requirement silently enforces invariant: " + mEnforcedInvariant); | ||
| } | ||
| return sb.toString(); | ||
| } | ||
| } | ||
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,61 @@ | ||
| /* | ||
| * Copyright (C) 2024 University of Freiburg | ||
| * | ||
|
|
||
| * This file is part of the ULTIMATE Core. | ||
| * | ||
| * The ULTIMATE Core is free software: you can redistribute it and/or modify | ||
| * it under the terms of the GNU Lesser General Public License as published | ||
| * by the Free Software Foundation, either version 3 of the License, or | ||
| * (at your option) any later version. | ||
| * | ||
| * The ULTIMATE Core is distributed in the hope that it will be useful, | ||
| * but WITHOUT ANY WARRANTY; without even the implied warranty of | ||
| * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the | ||
| * GNU Lesser General Public License for more details. | ||
| * | ||
| * You should have received a copy of the GNU Lesser General Public License | ||
| * along with the ULTIMATE Core. If not, see <http://www.gnu.org/licenses/>. | ||
| * | ||
| * Additional permission under GNU GPL version 3 section 7: | ||
| * If you modify the ULTIMATE Core, or any covered work, by linking | ||
| * or combining it with Eclipse RCP (or a modified version of Eclipse RCP), | ||
| * containing parts covered by the terms of the Eclipse Public License, the | ||
| * licensors of the ULTIMATE Core grant you additional permission | ||
| * to convey the resulting work. | ||
| */ | ||
| package de.uni_freiburg.informatik.ultimate.pea2boogie.translator; | ||
|
|
||
| import de.uni_freiburg.informatik.ultimate.core.lib.models.annotation.ModernAnnotations; | ||
| import de.uni_freiburg.informatik.ultimate.core.model.models.IElement; | ||
| import de.uni_freiburg.informatik.ultimate.core.model.models.ModelUtils; | ||
| import de.uni_freiburg.informatik.ultimate.core.model.models.annotation.IAnnotations; | ||
| import de.uni_freiburg.informatik.ultimate.lib.pea.CDD; | ||
|
|
||
| /** | ||
| * | ||
| * Annotation for vacuity checks. This marks whether a vacuous requirement | ||
| * enforces a trivial invariant. | ||
| * | ||
| */ | ||
|
|
||
| public class VacuityAnnotation extends ModernAnnotations { | ||
|
|
||
| private static final long serialVersionUID = 1L; | ||
| private final CDD mEnforcedInvariant; | ||
|
|
||
| public VacuityAnnotation(final CDD enforcedInv) { | ||
| mEnforcedInvariant = enforcedInv; | ||
| } | ||
|
|
||
| public CDD getInvariant() { | ||
| return mEnforcedInvariant; | ||
| } | ||
|
|
||
| public IAnnotations annotate(final IElement elem) { | ||
| return elem.getPayload().getAnnotations().put(VacuityAnnotation.class.getName(), this); | ||
| } | ||
|
|
||
| public static VacuityAnnotation getAnnotation(final IElement node) { | ||
| return ModelUtils.getAnnotation(node, VacuityAnnotation.class); | ||
| } | ||
| } | ||
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Should be
final-- do you have your save actions configured correctly?