Open vprevosto opened 7 years ago
I don't really understand the question, but I can say that arithmetic never overflow into ACSL (signed as well as unsigned, even for arithmetic shift operation). That could have to be highlighted.
Also, we could say that the verification of the mentioned ensures clause requires the verification of the precondition of the C operation. ACSL document is there to gives the semantics of ACSL properties, not on how we can prove them. The major question is: does the ACSL document have to present what are C run time errors and how to consider them ?
if
e1
ande2
are two expressions of C arithmetic typetau
and we do in Cres = e1 op e2;
(with res also of typetau
and res an arithmetic operation), do we always have in ACSL(tau) (e1 op e2) == res
.This is probably wrong for signed arithmetic where overflow results in undefined behavior. What about unsigned arithmetic?