A | |
Admitted_not_proved [ProverCoq] | |
C | |
COLLECTED [CfgWP.VC] | |
Contradiction [Conditions] | |
E | |
Error [Warning] |
Source, Reason
|
Error [Wp_error] |
To be raised a feature of C/ACSL cannot be supported by a memory model
or is not implemented, or ...
|
F | |
FIRST [GuiNavigator] | |
Found [WpPropId] | |
Found [Cil2cfg] | |
L | |
LabelError [NormAtLabels] | |
LoadError [Why3_session] |
Read/Write
|
N | |
NoSize [VarUsage] | |
P | |
Parse_error [Why3_xml] | |
S | |
Stop [GuiPanel] | |
Stop [Calculus.Cfg] |
detect if the computation of the result at
edge is possible,
or if it will loop.
|
U | |
Unknown_option [LogicBuiltins] |