Merge pull request #4260 from peterschrammel/fix-set-properties-inline

Consider properties of inline functions

Author: tautschnig

regression/cbmc/set-property-inline1/main.c

@@ -0,0 +1,10 @@
+static inline short inc(short x)
+{
+  return x + 1;
+}
+
+void main()
+{
+  short z;
+  inc(z);
+}

regression/cbmc/set-property-inline1/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--property inc.overflow.1 --property inc.overflow.2 --slice-formula --signed-overflow-check --conversion-check
+^EXIT=10$
+^SIGNAL=0$
+VERIFICATION FAILED
+\[inc\.overflow\.2\] line 3 arithmetic overflow on signed type conversion in \(signed short int\)\(\(signed int\)x \+ 1\): FAILURE
+\[inc\.overflow\.1\] line 3 arithmetic overflow on signed \+ in \(signed int\)x \+ 1: SUCCESS
+--
+^warning: ignoring

src/goto-programs/set_properties.cpp

@@ -109,8 +109,7 @@ void set_properties(
   property_set.insert(properties.begin(), properties.end());
 
   Forall_goto_functions(it, goto_functions)
-    if(!it->second.is_inlined())
-      set_properties(it->second.body, property_set);
+    set_properties(it->second.body, property_set);
 
   if(!property_set.empty())
     throw invalid_command_line_argument_exceptiont(