From 3d3bbdf0bae806179c0906c8fe4d43cd6d8f0664 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Thu, 13 Jun 2019 16:19:58 +0100 Subject: [PATCH 01/14] Inline variable used only once This intermediary variable doesn't help understanding and slows down reading the code. --- src/goto-symex/symex_assign.cpp | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp index 2be9a9262cf..0b3b64e59d1 100644 --- a/src/goto-symex/symex_assign.cpp +++ b/src/goto-symex/symex_assign.cpp @@ -395,8 +395,7 @@ void goto_symext::symex_assign_from_struct( const exprt::operandst &guard, assignment_typet assignment_type) { - const struct_typet &type = to_struct_type(ns.follow(lhs.type())); - const struct_union_typet::componentst &components = type.components(); + const auto &components = to_struct_type(ns.follow(lhs.type())).components(); PRECONDITION(rhs.operands().size() == components.size()); for(std::size_t i = 0; i < components.size(); ++i) From 389df45cee11e15e66ba14907df84d7fe9ca305c Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Thu, 13 Jun 2019 16:32:48 +0100 Subject: [PATCH 02/14] Simplify assignment of l2_rhs --- src/goto-symex/symex_assign.cpp | 19 +++++++++---------- 1 file changed, 9 insertions(+), 10 deletions(-) diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp index 0b3b64e59d1..4b103f6705f 100644 --- a/src/goto-symex/symex_assign.cpp +++ b/src/goto-symex/symex_assign.cpp @@ -434,16 +434,15 @@ void goto_symext::symex_assign_symbol( return; } - exprt l2_rhs = [&]() { - exprt guarded_rhs = rhs; - // put assignment guard into the rhs - if(!guard.empty()) - { - guarded_rhs = - if_exprt{conjunction(guard), std::move(guarded_rhs), lhs, rhs.type()}; - } - return state.rename(std::move(guarded_rhs), ns).get(); - }(); + exprt l2_rhs = + state + .rename( + // put assignment guard into the rhs + guard.empty() + ? rhs + : static_cast(if_exprt{conjunction(guard), rhs, lhs}), + ns) + .get(); // Note the following two calls are specifically required for // field-sensitivity. For example, with-expressions, which may have just been From 0c068ca9bf8b73a58e7be6bd0d97833c1d5036c4 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Thu, 13 Jun 2019 16:35:58 +0100 Subject: [PATCH 03/14] Declare variable closer to where it is used Makes it clearer why it is declared. --- src/goto-symex/symex_assign.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp index 4b103f6705f..d3d0c6e832c 100644 --- a/src/goto-symex/symex_assign.cpp +++ b/src/goto-symex/symex_assign.cpp @@ -455,7 +455,6 @@ void goto_symext::symex_assign_symbol( do_simplify(assignment.rhs); - const ssa_exprt &l1_lhs = assignment.lhs; const ssa_exprt l2_lhs = state .assignment( assignment.lhs, @@ -497,6 +496,7 @@ void goto_symext::symex_assign_symbol( state.source, assignment_type); + const ssa_exprt &l1_lhs = assignment.lhs; if(field_sensitivityt::is_divisible(l1_lhs)) { // Split composite symbol lhs into its components From 2c5ef55be0b3852d0425e85eb3e1d9f1af08c60a Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Thu, 13 Jun 2019 16:38:06 +0100 Subject: [PATCH 04/14] Inline variable that is immediately moved --- src/goto-symex/symex_assign.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp index d3d0c6e832c..677bd6e70f9 100644 --- a/src/goto-symex/symex_assign.cpp +++ b/src/goto-symex/symex_assign.cpp @@ -465,9 +465,9 @@ void goto_symext::symex_assign_symbol( symex_config.allow_pointer_unsoundness) .get(); - exprt ssa_full_lhs = add_to_lhs(full_lhs, l2_lhs); state.record_events.push(false); - const exprt l2_full_lhs = state.rename(std::move(ssa_full_lhs), ns).get(); + const exprt l2_full_lhs = + state.rename(add_to_lhs(full_lhs, l2_lhs), ns).get(); state.record_events.pop(); // do the assignment From 98e7146dadf776025d93d2166a3c5821b410f018 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Thu, 13 Jun 2019 16:38:34 +0100 Subject: [PATCH 05/14] Remove misleading comment ns.lookup doesn't do the assignment --- src/goto-symex/symex_assign.cpp | 1 - 1 file changed, 1 deletion(-) diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp index 677bd6e70f9..bc5a828d752 100644 --- a/src/goto-symex/symex_assign.cpp +++ b/src/goto-symex/symex_assign.cpp @@ -470,7 +470,6 @@ void goto_symext::symex_assign_symbol( state.rename(add_to_lhs(full_lhs, l2_lhs), ns).get(); state.record_events.pop(); - // do the assignment const symbolt &symbol = ns.lookup(l2_lhs.get_object_name()); if(symbol.is_auxiliary) From 360eb4ade06fc8c377be806d4a1cc40327d9d907 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Thu, 13 Jun 2019 16:39:44 +0100 Subject: [PATCH 06/14] Inline reference used only once The definition of this reference is not useful. --- src/goto-symex/symex_assign.cpp | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp index bc5a828d752..4a2ef19d736 100644 --- a/src/goto-symex/symex_assign.cpp +++ b/src/goto-symex/symex_assign.cpp @@ -470,9 +470,7 @@ void goto_symext::symex_assign_symbol( state.rename(add_to_lhs(full_lhs, l2_lhs), ns).get(); state.record_events.pop(); - const symbolt &symbol = ns.lookup(l2_lhs.get_object_name()); - - if(symbol.is_auxiliary) + if(ns.lookup(l2_lhs.get_object_name()).is_auxiliary) assignment_type=symex_targett::assignment_typet::HIDDEN; log.conditional_output( From a8af4d34056d375bade46730b457188104bf0c0d Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Thu, 13 Jun 2019 16:48:49 +0100 Subject: [PATCH 07/14] Infer hidden field in SSA_assignment_stept We can deduce it from the assignment type rather than having to give it to the constructor. --- src/goto-symex/ssa_step.cpp | 8 +++++--- src/goto-symex/ssa_step.h | 3 +-- src/goto-symex/symex_target_equation.cpp | 4 +--- 3 files changed, 7 insertions(+), 8 deletions(-) diff --git a/src/goto-symex/ssa_step.cpp b/src/goto-symex/ssa_step.cpp index 3deac1253ac..b839634f1bb 100644 --- a/src/goto-symex/ssa_step.cpp +++ b/src/goto-symex/ssa_step.cpp @@ -222,8 +222,7 @@ SSA_assignment_stept::SSA_assignment_stept( exprt _original_full_lhs, exprt _ssa_rhs, exprt _cond_expr, - symex_targett::assignment_typet _assignment_type, - bool _hidden) + symex_targett::assignment_typet _assignment_type) : SSA_stept(source, goto_trace_stept::typet::ASSIGNMENT) { guard = std::move(_guard); @@ -233,5 +232,8 @@ SSA_assignment_stept::SSA_assignment_stept( ssa_rhs = std::move(_ssa_rhs); assignment_type = _assignment_type; cond_expr = std::move(_cond_expr); - hidden = _hidden; + hidden = + assignment_type != symex_targett::assignment_typet::STATE && + assignment_type != + symex_targett::assignment_typet::VISIBLE_ACTUAL_PARAMETER; } diff --git a/src/goto-symex/ssa_step.h b/src/goto-symex/ssa_step.h index 84bcbe92642..8cae5976834 100644 --- a/src/goto-symex/ssa_step.h +++ b/src/goto-symex/ssa_step.h @@ -206,8 +206,7 @@ class SSA_assignment_stept : public SSA_stept exprt original_full_lhs, exprt ssa_rhs, exprt cond_expr, - symex_targett::assignment_typet assignment_type, - bool hidden); + symex_targett::assignment_typet assignment_type); }; #endif // CPROVER_GOTO_SYMEX_SSA_STEP_H diff --git a/src/goto-symex/symex_target_equation.cpp b/src/goto-symex/symex_target_equation.cpp index affa572a95e..33d64186500 100644 --- a/src/goto-symex/symex_target_equation.cpp +++ b/src/goto-symex/symex_target_equation.cpp @@ -122,9 +122,7 @@ void symex_target_equationt::assignment( original_full_lhs, ssa_rhs, equal_exprt(ssa_lhs, ssa_rhs), - assignment_type, - assignment_type != assignment_typet::STATE && - assignment_type != assignment_typet::VISIBLE_ACTUAL_PARAMETER}); + assignment_type}); merge_ireps(SSA_steps.back()); } From 093ee52f3e141c6163d8431456a0bca2bc31d9ea Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Thu, 13 Jun 2019 16:51:31 +0100 Subject: [PATCH 08/14] Infer cond_expr in SSA_assignment_step This can be deduced fro lhs and rhs without having to give it to the constructor. --- src/goto-symex/ssa_step.cpp | 3 +-- src/goto-symex/ssa_step.h | 1 - src/goto-symex/symex_target_equation.cpp | 1 - 3 files changed, 1 insertion(+), 4 deletions(-) diff --git a/src/goto-symex/ssa_step.cpp b/src/goto-symex/ssa_step.cpp index b839634f1bb..d61bc7ad5a1 100644 --- a/src/goto-symex/ssa_step.cpp +++ b/src/goto-symex/ssa_step.cpp @@ -221,7 +221,6 @@ SSA_assignment_stept::SSA_assignment_stept( exprt _ssa_full_lhs, exprt _original_full_lhs, exprt _ssa_rhs, - exprt _cond_expr, symex_targett::assignment_typet _assignment_type) : SSA_stept(source, goto_trace_stept::typet::ASSIGNMENT) { @@ -231,7 +230,7 @@ SSA_assignment_stept::SSA_assignment_stept( original_full_lhs = std::move(_original_full_lhs); ssa_rhs = std::move(_ssa_rhs); assignment_type = _assignment_type; - cond_expr = std::move(_cond_expr); + cond_expr = equal_exprt{ssa_lhs, ssa_rhs}; hidden = assignment_type != symex_targett::assignment_typet::STATE && assignment_type != diff --git a/src/goto-symex/ssa_step.h b/src/goto-symex/ssa_step.h index 8cae5976834..93b124c724a 100644 --- a/src/goto-symex/ssa_step.h +++ b/src/goto-symex/ssa_step.h @@ -205,7 +205,6 @@ class SSA_assignment_stept : public SSA_stept exprt ssa_full_lhs, exprt original_full_lhs, exprt ssa_rhs, - exprt cond_expr, symex_targett::assignment_typet assignment_type); }; diff --git a/src/goto-symex/symex_target_equation.cpp b/src/goto-symex/symex_target_equation.cpp index 33d64186500..61b898560f8 100644 --- a/src/goto-symex/symex_target_equation.cpp +++ b/src/goto-symex/symex_target_equation.cpp @@ -121,7 +121,6 @@ void symex_target_equationt::assignment( ssa_full_lhs, original_full_lhs, ssa_rhs, - equal_exprt(ssa_lhs, ssa_rhs), assignment_type}); merge_ireps(SSA_steps.back()); From 56d7bba531bb590ef9e62f434c03d42dbad6489c Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Fri, 14 Jun 2019 07:08:41 +0100 Subject: [PATCH 09/14] Inline variables used immediatly after Declaring variables for these values doesn't add clarity and makes the function longer. --- src/goto-symex/symex_assign.cpp | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp index 4a2ef19d736..a05369efb6b 100644 --- a/src/goto-symex/symex_assign.cpp +++ b/src/goto-symex/symex_assign.cpp @@ -480,15 +480,11 @@ void goto_symext::symex_assign_symbol( << messaget::eom; }); - const exprt assignment_guard = - make_and(state.guard.as_expr(), conjunction(guard)); - - const exprt original_lhs = get_original_name(l2_full_lhs); target.assignment( - assignment_guard, + make_and(state.guard.as_expr(), conjunction(guard)), l2_lhs, l2_full_lhs, - original_lhs, + get_original_name(l2_full_lhs), assignment.rhs, state.source, assignment_type); From a97d61e17d0df67a815ee01ad52e04f4f5f32712 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Fri, 14 Jun 2019 07:29:52 +0100 Subject: [PATCH 10/14] Clean-up increase_generation Add missing const, necessary narrow and insert if and else to make r_opt scoped to only the if branch. --- src/goto-symex/goto_state.cpp | 14 ++++++-------- 1 file changed, 6 insertions(+), 8 deletions(-) diff --git a/src/goto-symex/goto_state.cpp b/src/goto-symex/goto_state.cpp index a03ebfdffef..38544b3d9b3 100644 --- a/src/goto-symex/goto_state.cpp +++ b/src/goto-symex/goto_state.cpp @@ -31,19 +31,17 @@ std::size_t goto_statet::increase_generation( const ssa_exprt &lhs, std::function fresh_l2_name_provider) { - std::size_t n = fresh_l2_name_provider(l1_identifier); + const std::size_t n = fresh_l2_name_provider(l1_identifier); - const auto r_opt = level2.current_names.find(l1_identifier); - - if(!r_opt) + if(const auto r_opt = level2.current_names.find(l1_identifier)) { - level2.current_names.insert(l1_identifier, std::make_pair(lhs, n)); + std::pair copy = r_opt->get(); + copy.second = narrow(n); + level2.current_names.replace(l1_identifier, std::move(copy)); } else { - std::pair copy = r_opt->get(); - copy.second = n; - level2.current_names.replace(l1_identifier, std::move(copy)); + level2.current_names.insert(l1_identifier, std::make_pair(lhs, n)); } return n; From a577ed26cfbeea54cffd7c167a4683e7ca12f683 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Fri, 14 Jun 2019 07:31:09 +0100 Subject: [PATCH 11/14] Add missing slash No functional changes. Necessary for doxygen comment --- src/goto-symex/goto_symex_state.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/goto-symex/goto_symex_state.h b/src/goto-symex/goto_symex_state.h index 35c7188c493..4101dd84037 100644 --- a/src/goto-symex/goto_symex_state.h +++ b/src/goto-symex/goto_symex_state.h @@ -217,7 +217,7 @@ class goto_symex_statet final : public goto_statet unsigned remaining_vccs = 0; /// Allocates a fresh L2 name for the given L1 identifier, and makes it the - // latest generation on this path. + /// latest generation on this path. std::size_t increase_generation(const irep_idt l1_identifier, const ssa_exprt &lhs) { From 7a8f8c77b0d8e9336daec7529905745eae64f506 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Fri, 14 Jun 2019 07:56:50 +0100 Subject: [PATCH 12/14] Document l2_thread_write_encoding --- src/goto-symex/goto_symex_state.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp index d8cb995077d..245b3655e26 100644 --- a/src/goto-symex/goto_symex_state.cpp +++ b/src/goto-symex/goto_symex_state.cpp @@ -514,6 +514,7 @@ goto_symex_statet::write_is_shared_resultt goto_symex_statet::write_is_shared( } /// thread encoding +/// \return true if \p expr is shared between threads bool goto_symex_statet::l2_thread_write_encoding( const ssa_exprt &expr, const namespacet &ns) From 3e9c60f7da70c17ecdcc49ce9dc546a44cb4e537 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Fri, 14 Jun 2019 10:38:11 +0100 Subject: [PATCH 13/14] Formatting changes suggested by clang-format This is necessary for CI --- src/goto-symex/ssa_step.cpp | 7 +++---- src/goto-symex/symex_target_equation.cpp | 15 +++++++-------- 2 files changed, 10 insertions(+), 12 deletions(-) diff --git a/src/goto-symex/ssa_step.cpp b/src/goto-symex/ssa_step.cpp index d61bc7ad5a1..5d92a5516f4 100644 --- a/src/goto-symex/ssa_step.cpp +++ b/src/goto-symex/ssa_step.cpp @@ -231,8 +231,7 @@ SSA_assignment_stept::SSA_assignment_stept( ssa_rhs = std::move(_ssa_rhs); assignment_type = _assignment_type; cond_expr = equal_exprt{ssa_lhs, ssa_rhs}; - hidden = - assignment_type != symex_targett::assignment_typet::STATE && - assignment_type != - symex_targett::assignment_typet::VISIBLE_ACTUAL_PARAMETER; + hidden = assignment_type != symex_targett::assignment_typet::STATE && + assignment_type != + symex_targett::assignment_typet::VISIBLE_ACTUAL_PARAMETER; } diff --git a/src/goto-symex/symex_target_equation.cpp b/src/goto-symex/symex_target_equation.cpp index 61b898560f8..ff7e1f6a382 100644 --- a/src/goto-symex/symex_target_equation.cpp +++ b/src/goto-symex/symex_target_equation.cpp @@ -114,14 +114,13 @@ void symex_target_equationt::assignment( { PRECONDITION(ssa_lhs.is_not_nil()); - SSA_steps.emplace_back(SSA_assignment_stept{ - source, - guard, - ssa_lhs, - ssa_full_lhs, - original_full_lhs, - ssa_rhs, - assignment_type}); + SSA_steps.emplace_back(SSA_assignment_stept{source, + guard, + ssa_lhs, + ssa_full_lhs, + original_full_lhs, + ssa_rhs, + assignment_type}); merge_ireps(SSA_steps.back()); } From 71caf32f40eb7701d1072807d19ca19991d86955 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Mon, 17 Jun 2019 07:41:32 +0100 Subject: [PATCH 14/14] Make index in renamings be of std::size_t type This avoids some conversions, in particular when assigning from the return value of fresh_l2_name_provider. --- src/goto-symex/goto_state.cpp | 4 ++-- src/goto-symex/renamed.h | 2 +- src/goto-symex/renaming_level.cpp | 12 +++++++----- src/goto-symex/renaming_level.h | 10 +++++----- src/util/ssa_expr.cpp | 6 +++--- src/util/ssa_expr.h | 6 +++--- 6 files changed, 21 insertions(+), 19 deletions(-) diff --git a/src/goto-symex/goto_state.cpp b/src/goto-symex/goto_state.cpp index 38544b3d9b3..7bf811bb87b 100644 --- a/src/goto-symex/goto_state.cpp +++ b/src/goto-symex/goto_state.cpp @@ -35,8 +35,8 @@ std::size_t goto_statet::increase_generation( if(const auto r_opt = level2.current_names.find(l1_identifier)) { - std::pair copy = r_opt->get(); - copy.second = narrow(n); + std::pair copy = r_opt->get(); + copy.second = n; level2.current_names.replace(l1_identifier, std::move(copy)); } else diff --git a/src/goto-symex/renamed.h b/src/goto-symex/renamed.h index 4781271da15..58fe9ed9818 100644 --- a/src/goto-symex/renamed.h +++ b/src/goto-symex/renamed.h @@ -50,7 +50,7 @@ class renamedt : private underlyingt }; friend renamedt - symex_level0(ssa_exprt, const namespacet &, unsigned); + symex_level0(ssa_exprt, const namespacet &, std::size_t); friend struct symex_level1t; friend struct symex_level2t; friend class goto_symex_statet; diff --git a/src/goto-symex/renaming_level.cpp b/src/goto-symex/renaming_level.cpp index 1653e93df57..26e8b98af78 100644 --- a/src/goto-symex/renaming_level.cpp +++ b/src/goto-symex/renaming_level.cpp @@ -31,7 +31,7 @@ void get_variables( } renamedt -symex_level0(ssa_exprt ssa_expr, const namespacet &ns, unsigned thread_nr) +symex_level0(ssa_exprt ssa_expr, const namespacet &ns, std::size_t thread_nr) { // already renamed? if(!ssa_expr.get_level_0().empty()) @@ -56,21 +56,23 @@ symex_level0(ssa_exprt ssa_expr, const namespacet &ns, unsigned thread_nr) return renamedt{ssa_expr}; } -void symex_level1t::insert(const renamedt &ssa, unsigned index) +void symex_level1t::insert( + const renamedt &ssa, + std::size_t index) { current_names.insert( ssa.get().get_identifier(), std::make_pair(ssa.get(), index)); } -optionalt> symex_level1t::insert_or_replace( +optionalt> symex_level1t::insert_or_replace( const renamedt &ssa, - unsigned index) + std::size_t index) { const irep_idt &identifier = ssa.get().get_identifier(); const auto old_value = current_names.find(identifier); if(old_value) { - std::pair result = *old_value; + std::pair result = *old_value; current_names.replace(identifier, std::make_pair(ssa.get(), index)); return result; } diff --git a/src/goto-symex/renaming_level.h b/src/goto-symex/renaming_level.h index 168e7031237..428299e0797 100644 --- a/src/goto-symex/renaming_level.h +++ b/src/goto-symex/renaming_level.h @@ -29,7 +29,7 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com /// This is extended by the different symex_level structures which are used /// during symex to ensure static single assignment (SSA) form. using symex_renaming_levelt = - sharing_mapt>; + sharing_mapt>; /// Add the \c ssa_exprt of current_names to vars DEPRECATED(SINCE(2019, 6, 5, "Unused")) @@ -44,7 +44,7 @@ void get_variables( /// a guard, a shared variable or a function. \p ns is queried to decide /// whether we are in one of these cases. renamedt -symex_level0(ssa_exprt ssa_expr, const namespacet &ns, unsigned thread_nr); +symex_level0(ssa_exprt ssa_expr, const namespacet &ns, std::size_t thread_nr); /// Functor to set the level 1 renaming of SSA expressions. /// Level 1 corresponds to function frames. @@ -52,13 +52,13 @@ symex_level0(ssa_exprt ssa_expr, const namespacet &ns, unsigned thread_nr); struct symex_level1t { /// Assume \p ssa is not already known - void insert(const renamedt &ssa, unsigned index); + void insert(const renamedt &ssa, std::size_t index); /// Set the index for \p ssa to index. /// \return if an index for \p ssa was already know, returns it's previous /// value. - optionalt> - insert_or_replace(const renamedt &ssa, unsigned index); + optionalt> + insert_or_replace(const renamedt &ssa, std::size_t index); /// \return true if \p ssa has an associated index bool has(const renamedt &ssa) const; diff --git a/src/util/ssa_expr.cpp b/src/util/ssa_expr.cpp index 42894c0cefc..53acec47310 100644 --- a/src/util/ssa_expr.cpp +++ b/src/util/ssa_expr.cpp @@ -178,19 +178,19 @@ const irep_idt ssa_exprt::get_l1_object_identifier() const #endif } -void ssa_exprt::set_level_0(unsigned i) +void ssa_exprt::set_level_0(std::size_t i) { set(ID_L0, i); ::update_identifier(*this); } -void ssa_exprt::set_level_1(unsigned i) +void ssa_exprt::set_level_1(std::size_t i) { set(ID_L1, i); ::update_identifier(*this); } -void ssa_exprt::set_level_2(unsigned i) +void ssa_exprt::set_level_2(std::size_t i) { set(ID_L2, i); ::update_identifier(*this); diff --git a/src/util/ssa_expr.h b/src/util/ssa_expr.h index b3503821d8a..a7902db8ab9 100644 --- a/src/util/ssa_expr.h +++ b/src/util/ssa_expr.h @@ -52,11 +52,11 @@ class ssa_exprt:public symbol_exprt return o.get_identifier(); } - void set_level_0(unsigned i); + void set_level_0(std::size_t i); - void set_level_1(unsigned i); + void set_level_1(std::size_t i); - void set_level_2(unsigned i); + void set_level_2(std::size_t i); void remove_level_2();