Merge pull request #7063 from remi-delmas-3000/contract-base-name-fix

CONTRACTS: filter out contract symbols when resolving entry points and interrupt handlers

Author: tautschnig

regression/contracts/entry_point/main.c

@@ -0,0 +1,9 @@
+int foo(char *arr, unsigned int size)
+  // clang-format off
+__CPROVER_requires(__CPROVER_is_fresh(arr, size))
+__CPROVER_assigns(arr &&size > 0: arr[0])
+// clang-format on
+{
+  if(arr && size > 0)
+    arr[0] = 1;
+}

regression/contracts/entry_point/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--enforce-contract foo _ --function foo
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test checks that we can use a function with a contract as entry point
+for the analysis when its contract gets enforced.

src/ansi-c/ansi_c_entry_point.cpp

@@ -130,7 +130,7 @@ bool ansi_c_entry_point(
       if(s_it==symbol_table.symbols.end())
         continue;
 
-      if(s_it->second.type.id()==ID_code)
+      if(s_it->second.type.id() == ID_code && !s_it->second.is_property)
         matches.push_back(symbol_name_entry.second);
     }
 

src/ansi-c/c_typecheck_base.cpp

@@ -877,8 +877,8 @@ void c_typecheck_baset::typecheck_declaration(
         // create a contract symbol
         symbolt contract;
         contract.name = "contract::" + id2string(new_symbol.name);
-        contract.base_name = new_symbol.name;
-        contract.pretty_name = new_symbol.name;
+        contract.base_name = new_symbol.base_name;
+        contract.pretty_name = new_symbol.pretty_name;
         contract.is_property = true;
         contract.type = code_type;
         contract.mode = new_symbol.mode;

src/goto-instrument/interrupt.cpp

@@ -165,7 +165,7 @@ get_isr(const symbol_tablet &symbol_table, const irep_idt &interrupt_handler)
     if(s_it==symbol_table.symbols.end())
       continue;
 
-    if(s_it->second.type.id()==ID_code)
+    if(s_it->second.type.id() == ID_code && !s_it->second.is_property)
       matches.push_back(s_it->second.symbol_expr());
   }
 

src/jsil/jsil_entry_point.cpp

@@ -74,7 +74,7 @@ bool jsil_entry_point(
       if(s_it==symbol_table.symbols.end())
         continue;
 
-      if(s_it->second.type.id()==ID_code)
+      if(s_it->second.type.id() == ID_code && !s_it->second.is_property)
         matches.push_back(symbol_name_entry.second);
     }