Add no initialisation PRECONDITION to wp_decl

This function does not account for the case where a code_declt contains
`initialization`. Given that the test suite passes with this
PRECONDITION is in place, such statements must be separated out before
this function is reached. Should this condition be violated in future,
then the CONDITION can be removed and the handling of this case
implemented.

Author: thomasspriggs

src/goto-programs/wp.cpp

@@ -226,6 +226,7 @@ exprt wp_decl(
   const exprt &post,
   const namespacet &ns)
 {
+  PRECONDITION(!code.initial_value());
   // Model decl(var) as var = nondet()
   const exprt &var = code.symbol();
   side_effect_expr_nondett nondet(var.type(), source_locationt());