Merge pull request #7602 from qinheping/bugfix/synthesis-for-empty-loops

Ignore empty loops during loop-contracts synthesis

Author: qinheping

regression/goto-synthesizer/empty_loop/main.c

@@ -0,0 +1,10 @@
+void exit(int s)
+{
+_EXIT:
+  goto _EXIT;
+}
+
+int main()
+{
+  exit(1);
+}

regression/goto-synthesizer/empty_loop/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--pointer-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Check if empty loops are correctly skipped.

src/goto-instrument/contracts/contracts.cpp

@@ -869,7 +869,8 @@ void code_contractst::apply_loop_contract(
   for(const auto &loop_head_and_content : natural_loops.loop_map)
   {
     const auto &loop_content = loop_head_and_content.second;
-    if(loop_content.empty())
+    // Skip empty loops and self-looped node.
+    if(loop_content.size() <= 1)
       continue;
 
     auto loop_head = loop_head_and_content.first;

src/goto-synthesizer/enumerative_loop_contracts_synthesizer.cpp

@@ -88,6 +88,10 @@ void enumerative_loop_contracts_synthesizert::init_candidates()
     // Initialize invariants for unannotated loops as true
     for(const auto &loop_head_and_content : natural_loops.loop_map)
     {
+      // Ignore empty loops and self-looped node.
+      if(loop_head_and_content.second.size() <= 1)
+        continue;
+
       goto_programt::const_targett loop_end =
         get_loop_end_from_loop_head_and_content(
           loop_head_and_content.first, loop_head_and_content.second);