DFCC instrumentation: ensure programs are well-formed

We must not pass to analyses goto programs that aren't terminated by
END_FUNCTION (i.e., really just sequences of statements). On this
occasion, local_may_aliast was the one relying on well-formedness. We
now make sure that sequences of instructions are terminated by
END_FUNCTION when we pass them around as goto programs.

To catch these kinds of problems in regression tests, amend
check-ubuntu-22_04-cmake-gcc-13 to include standard library assertions.

Fixes: #7866

Author: tautschnig

.github/workflows/pull-request-checks.yaml

@@ -432,7 +432,7 @@ jobs:
           echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
           echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
       - name: Configure using CMake
-        run: cmake -S . -Bbuild -G Ninja -DCMAKE_BUILD_TYPE=Release
+        run: cmake -S . -Bbuild -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_CXX_FLAGS=-Wp,-D_GLIBCXX_ASSERTIONS
       - name: Zero ccache stats and limit in size
         run: ccache -z --max-size=500M
       - name: Build with Ninja

src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp

@@ -578,11 +578,15 @@ void dfcc_wrapper_programt::encode_requires_clauses()
   memory_predicates.fix_calls(requires_program);
 
   // instrument for side effects
+  // make the program well-formed
+  requires_program.add(goto_programt::make_end_function());
   instrument.instrument_goto_program(
     wrapper_id,
     requires_program,
     addr_of_requires_write_set,
     function_pointer_contracts);
+  // turn it back into a sequence of statements
+  requires_program.instructions.back().turn_into_skip();
 
   // append resulting program to preconditions section
   preconditions.destructive_append(requires_program);
@@ -637,11 +641,15 @@ void dfcc_wrapper_programt::encode_ensures_clauses()
   memory_predicates.fix_calls(ensures_program);
 
   // instrument for side effects
+  // make the program well-formed
+  ensures_program.add(goto_programt::make_end_function());
   instrument.instrument_goto_program(
     wrapper_id,
     ensures_program,
     addr_of_ensures_write_set,
     function_pointer_contracts);
+  // turn it back into a sequence of statements
+  ensures_program.instructions.back().turn_into_skip();
 
   // add the ensures program to the postconditions section
   postconditions.destructive_append(ensures_program);