Update goto-analyzer tasks to take account of the ait API changes.

Author: martin

src/goto-analyzer/static_simplifier.cpp

@@ -66,7 +66,7 @@ bool static_simplifier(
       if(i_it->is_assert())
       {
         bool unchanged=
-          ai.abstract_state_before(i_it).ai_simplify(i_it->guard, ns);
+          ai.abstract_state_before(i_it)->ai_simplify(i_it->guard, ns);
 
         if(unchanged)
           unmodified.asserts++;
@@ -76,7 +76,7 @@ bool static_simplifier(
       else if(i_it->is_assume())
       {
         bool unchanged=
-          ai.abstract_state_before(i_it).ai_simplify(i_it->guard, ns);
+          ai.abstract_state_before(i_it)->ai_simplify(i_it->guard, ns);
 
         if(unchanged)
           unmodified.assumes++;
@@ -86,7 +86,7 @@ bool static_simplifier(
       else if(i_it->is_goto())
       {
         bool unchanged=
-          ai.abstract_state_before(i_it).ai_simplify(i_it->guard, ns);
+          ai.abstract_state_before(i_it)->ai_simplify(i_it->guard, ns);
 
         if(unchanged)
           unmodified.gotos++;
@@ -103,10 +103,10 @@ bool static_simplifier(
         // should simplify to i=1, not to 0=1.
 
         bool unchanged_lhs=
-          ai.abstract_state_before(i_it).ai_simplify_lhs(assign.lhs(), ns);
+          ai.abstract_state_before(i_it)->ai_simplify_lhs(assign.lhs(), ns);
 
         bool unchanged_rhs=
-          ai.abstract_state_before(i_it).ai_simplify(assign.rhs(), ns);
+          ai.abstract_state_before(i_it)->ai_simplify(assign.rhs(), ns);
 
         if(unchanged_lhs && unchanged_rhs)
           unmodified.assigns++;
@@ -118,12 +118,12 @@ bool static_simplifier(
         code_function_callt &fcall=to_code_function_call(i_it->code);
 
         bool unchanged=
-          ai.abstract_state_before(i_it).ai_simplify(fcall.function(), ns);
+          ai.abstract_state_before(i_it)->ai_simplify(fcall.function(), ns);
 
         exprt::operandst &args=fcall.arguments();
 
         for(auto &o : args)
-          unchanged&=ai.abstract_state_before(i_it).ai_simplify(o, ns);
+          unchanged&=ai.abstract_state_before(i_it)->ai_simplify(o, ns);
 
         if(unchanged)
           unmodified.function_calls++;

src/goto-analyzer/static_verifier.cpp

@@ -55,7 +55,8 @@ bool static_verifier(
           continue;
 
         exprt e(i_it->guard);
-        const ai_domain_baset &domain(ai.abstract_state_before(i_it));
+        auto dp=ai.abstract_state_before(i_it);
+        const ai_domain_baset &domain(*dp);
         domain.ai_simplify(e, ns);
 
         json_objectt &j=json_result.push_back().make_object();
@@ -104,7 +105,8 @@ bool static_verifier(
           continue;
 
         exprt e(i_it->guard);
-        const ai_domain_baset &domain(ai.abstract_state_before(i_it));
+        auto dp=ai.abstract_state_before(i_it);
+        const ai_domain_baset &domain(*dp);
         domain.ai_simplify(e, ns);
 
         xmlt &x=xml_result.new_element("result");
@@ -160,7 +162,8 @@ bool static_verifier(
           continue;
 
         exprt e(i_it->guard);
-        const ai_domain_baset &domain(ai.abstract_state_before(i_it));
+        auto dp=ai.abstract_state_before(i_it);
+        const ai_domain_baset &domain(*dp);
         domain.ai_simplify(e, ns);
 
         out << '[' << i_it->source_location.get_property_id()

src/goto-analyzer/unreachable_instructions.cpp

@@ -59,7 +59,7 @@ static void build_dead_map_from_ai(
   dead_mapt &dest)
 {
   forall_goto_program_instructions(it, goto_program)
-    if(ai.abstract_state_before(it).is_bottom())
+    if(ai.abstract_state_before(it)->is_bottom())
       dest.insert(std::make_pair(it->location_number, it));
 }
 
@@ -418,7 +418,7 @@ std::unordered_set<irep_idt> compute_called_functions_from_ai(
 
     const goto_programt &p = f_it->second.body;
 
-    if(!ai.abstract_state_before(p.instructions.begin()).is_bottom())
+    if(!ai.abstract_state_before(p.instructions.begin())->is_bottom())
       called.insert(f_it->first);
   }