"Make_Assert_Call" likely redundant

[sonodtt]

It seems likely that the process of creating and then calling an assert function via "Make_Assert_Call" can be replaced with a 'make assert expression' via simple binding of an expression to an
New_Irep (I_Code_Assert) via ' Set_Assertion(A_Irep1, Make_Op_Eq(...) )'

This would avoid generating

• the assert function
• the function call at call site

While the code saving would be minor - it would be more consistent with other locations e.g. " Do_Pragma_Assert_or_Assume" where assertions are generated simply via
"Set_Assertion" as outlined above.

Another concern is that there may be cbmc warnings upon duplicated symbols in the symbol table when an asssert call is generated. This does not occur atm - just a potential issue along the lines of warnings we have seen before.

The json template has this
{
"parent": "code",
"sub": [
{"schema": "expr", "friendly_name": "assertion"}
],
"namedSub": {
"statement": {"constant": "assert", "type": "string"}
}
}

It might be preferable to go via this interface rather than generating an assert function directly via use of "__CPROVER_assert" - this seems to have been the original design elsewhere in "tree_walk.adb"

• In long form:
Creating a simple c assert statement requires only something along these lines:

     Op_Equal_Var1 :=
       Make_Op_Eq (Rhs             => Make_Int_Constant_Expr("0"),
                   Lhs             => Var1_Symbol_Irep,
                   Source_Location => 0,
                   Overflow_Check  => False,
                   I_Type          => Make_Bool_Type,
                   Range_Check     => False);

     A_Irep1 := New_Irep (I_Code_Assert);
     Set_Assertion(A_Irep1, Op_Equal_Var1);
     Append_Op (Dummy_Body, A_Irep1);

This creates e.g.
" assert(var1_user == 0);" in the generated code.

This was verified via
https://github.com/sonodtt/gnat2goto/tree/irep_debug_framework_v0