Termination Plugin: deactivated flag set to false when decreases removed from code

[aterga]

In particular, TerminationPlugin.mapVerificationResult in https://github.com/viperproject/silver/blob/master/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala#L125 performs a non-trivial transformation in the following case:

method foo()
{
    assert false
}

[aterga]

Is this the intended behaviour?

[mschwerhoff]

Which behaviour?

[aterga]

From the discussions about the termination plugin that we had, I concluded that the deactivated flag should be switched on if there are no decreases clauses in the program, but I'm not 100% sure.

[mschwerhoff]

Thanks for clarifying, sounds OK to me.

Out of curiosity: does the transformation, in absence of decreases clauses, actually do something (that affects the IDE)?

[aterga]

Yes, when caching is enabled, the transformations affect the information about which nodes have been cached. I files a separate issue for that one: #451