Results of transform for function call and function return must end up as

  transforming target state, not source state.

git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@5783 6afb6bc1-c8e4-404c-8f48-9ae832c5b171

Author: kroening

src/analyses/ai.cpp

@@ -260,6 +260,9 @@ bool ai_baset::visit(
     }
     else
     {
+      // initialize state, if necessary
+      get_state(to_l);
+
       new_values.transform(l, to_l, *this, ns);
 
       if(merge(new_values, l, to_l))
@@ -295,25 +298,48 @@ bool ai_baset::do_function_call(
   const exprt::operandst &arguments,
   const namespacet &ns)
 {
+  // initialize state, if necessary
+  get_state(l_return);
+
   const goto_functionst::goto_functiont &goto_function=
     f_it->second;
 
   if(!goto_function.body_available)
-    return false; // do nothing, no change
+  {
+    std::unique_ptr<statet> tmp_state(make_temporary_state(get_state(l_call)));
+    tmp_state->transform(l_call, l_return, *this, ns);
+
+    return merge(*tmp_state, l_call, l_return);
+  }
 
   assert(!goto_function.body.instructions.empty());
 
   {
     // get the state at the beginning of the function
     locationt l_begin=goto_function.body.instructions.begin();
+    // initialize state, if necessary
+    get_state(l_begin);
 
     // do the edge from the call site to the beginning of the function
-    std::unique_ptr<statet> state(make_temporary_state(get_state(l_call)));
+    std::unique_ptr<statet> tmp_state(make_temporary_state(get_state(l_call)));
+    tmp_state->transform(l_call, l_begin, *this, ns);
+
+    bool new_data=false;
 
-    state->transform(l_call, l_begin, *this, ns);
-    
     // merge the new stuff
-    if(merge(*state, l_call, l_begin))
+    if(merge(*tmp_state, l_call, l_begin))
+      new_data=true;
+
+    // do each function at least once
+    if(functions_done.find(f_it->first)==
+       functions_done.end())
+    {
+      new_data=true;
+      functions_done.insert(f_it->first);
+    }
+
+    // do we need to do the fixedpoint of the body?
+    if(new_data)
     {
       // also do the fixedpoint of the body via a recursive call
       fixedpoint(goto_function.body, goto_functions, ns);
@@ -326,15 +352,13 @@ bool ai_baset::do_function_call(
     assert(l_end->is_end_function());
 
     // do edge from end of function to instruction after call
-    locationt l_next=l_call;
-    l_next++;
-
-    std::unique_ptr<statet> state(make_temporary_state(get_state(l_end)));
-
-    state->transform(l_end, l_next, *this, ns);
+    std::unique_ptr<statet> tmp_state(make_temporary_state(get_state(l_end)));
+    tmp_state->transform(l_end, l_return, *this, ns);
 
-    // Propagate those -- not exceedingly precise, this is.
-    return merge(*state, l_end, l_next);
+    // Propagate those -- not exceedingly precise, this is,
+    // as still it contains all the state from the
+    // call site
+    return merge(*tmp_state, l_end, l_return);
   }
 }    
 

src/analyses/ai.h

@@ -172,13 +172,10 @@ class ai_baset
     const goto_programt &goto_program,
     const goto_functionst &goto_functions,
     const namespacet &ns);
-    
-  static locationt successor(locationt l)
-  {
-    l++;
-    return l;
-  }
 
+  typedef std::set<irep_idt> functions_donet;
+  functions_donet functions_done;
+
   typedef std::set<irep_idt> recursion_sett;
   recursion_sett recursion_set;
 

src/analyses/static_analysis.cpp

@@ -444,14 +444,15 @@ void static_analysis_baset::do_function_call(
     locationt l_begin=goto_function.body.instructions.begin();
 
     // do the edge from the call site to the beginning of the function
-    new_state.transform(ns, l_call, l_begin);  
+    std::unique_ptr<statet> tmp_state(make_temporary_state(new_state));
+    tmp_state->transform(ns, l_call, l_begin);  
 
     statet &begin_state=get_state(l_begin);
 
     bool new_data=false;
 
     // merge the new stuff
-    if(merge(begin_state, new_state, l_begin))
+    if(merge(begin_state, *tmp_state, l_begin))
       new_data=true;
 
     // do each function at least once
@@ -479,14 +480,19 @@ void static_analysis_baset::do_function_call(
     statet &end_of_function=get_state(l_end);
 
     // do edge from end of function to instruction after call
-    locationt l_next=l_call;
-    l_next++;
-    end_of_function.transform(ns, l_end, l_next);
+    std::unique_ptr<statet> tmp_state(
+      make_temporary_state(end_of_function));
+    tmp_state->transform(ns, l_end, l_return);
 
     // propagate those -- not exceedingly precise, this is,
     // as still it contains all the state from the
     // call site
-    merge(new_state, end_of_function, l_end);
+    merge(new_state, *tmp_state, l_return);
+  }
+
+  {
+    // effect on current procedure (if any)
+    new_state.transform(ns, l_call, l_return);
   }
 }    
 
@@ -585,7 +591,8 @@ void static_analysis_baset::do_function_call_rec(
       }
     }
   }
-  else if(function.id()=="NULL-object")
+  else if(function.id()=="NULL-object" ||
+          function.id()==ID_integer_address)
   {
     // ignore, can't be a function
   }