Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Floating point simplification for goto-analyzer constants domain #2081

Merged
merged 3 commits into from
May 17, 2018
Merged

Floating point simplification for goto-analyzer constants domain #2081

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
3dc2244
Move adjust_float_expressions to goto-programs
hannes-steffenhagen-diffblue Apr 26, 2018
5f7bc15
Add float support to constant propagator domain
hannes-steffenhagen-diffblue Apr 17, 2018
a055454
Try all rounding modes when domain is unknown
hannes-steffenhagen-diffblue Apr 18, 2018
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 9 additions & 0 deletions regression/goto-analyzer/constant_propagation_floating_point_div/main.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
#include <assert.h>

#define ROUND_F(x) ((int)((x) + 0.5f))
int eight = ROUND_F(100.0f / 12.0f);

int main()
{
assert(eight == 8);
}
8 changes: 8 additions & 0 deletions regression/goto-analyzer/constant_propagation_floating_point_div/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
CORE
main.c
--constants --verify
^EXIT=0$
^SIGNAL=0$
^\[main.assertion.1\] file main.c line 8 function main, assertion eight == 8: Success$
--
^warning: ignoring
27 changes: 27 additions & 0 deletions regression/goto-analyzer/constant_propagation_nondet_rounding_mode/main.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,27 @@
#include <assert.h>
#include <fenv.h>
#include <stdio.h>

int nondet_rounding_mode(void);

int main(void)
{
// slightly bigger than 0.1
float f = 1.0f / 10.0f;

// now we don't know what rounding mode we're in
__CPROVER_rounding_mode = nondet_rounding_mode();
// depending on rounding mode 1.0f/10.0f could
// be greater or smaller than 0.1

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I disagree with the comment. 1.0f/10.0f will either be equal or less than f;

The division produces a repeating bit-string. h denotes the hidden bit, m are the 23 bits of significand that single precision float stores, g is the guard bit, s is the stick bits. As g = 1, s = 1, it rounds up giving

1.10011001100110011001100110011...
h.mmmmmmmmmmmmmmmmmmmmmmmgsssss
   10011001100110011001101

Round towards zero or round towards zero will round down giving the result 1 ulp less.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I disagree with the comment. 1.0f/10.0f will either be equal or less than f;

That's what I meant to say. FE_TONEAREST (default) and FE_UPWARD will yield the same result (slightly bigger than 0.1) and FE_DOWNWARD and FE_TOWARDZERO will also yield the same result (slightly less than 0.1). So overall, the result could either be slightly less than 0.1 or slightly more than 0.1 (but not more than f).

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I see what you are getting at but in this case 0.1 is quite ambiguous. You might say "the real value of 0.1" or something similar.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah yes, 0.1 is meant to be 0.1 as in the real number, not any floating point approximation of it.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I would be grateful if you can add a comment to clarify that. Also, see the general point that if you want specific floating-point numbers, hex format is the most reliable way to specify them.

// definitely not smaller than -0.1
assert((1.0f / 10.0f) - f < -0.1f);
// might be smaller than 0
assert((1.0f / 10.0f) - f < 0.0f);
// definitely smaller or equal to 0
assert((1.0f / 10.0f) - f <= 0.0f);
// might be greater or equal to 0
assert((1.0f / 10.0f) - f >= 0.0f);
// definitely not greater than 0
assert((1.0f / 10.0f) - f > 0.0f);
}
13 changes: 13 additions & 0 deletions regression/goto-analyzer/constant_propagation_nondet_rounding_mode/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
CORE
main.c
--constants --verify
^EXIT=0$
^SIGNAL=0$
\[main.assertion.1\] file main.c line 18 function main, assertion \(1.0f / 10.0f\) - f < -0.1f: Failure \(if reachable\)
\[main.assertion.2\] file main.c line 20 function main, assertion \(1.0f / 10.0f\) - f < 0.0f: Unknown
\[main.assertion.3\] file main.c line 22 function main, assertion \(1.0f / 10.0f\) - f <= 0.0f: Success
\[main.assertion.4\] file main.c line 24 function main, assertion \(1.0f / 10.0f\) - f >= 0.0f: Unknown
\[main.assertion.5\] file main.c line 26 function main, assertion \(1.0f / 10.0f\) - f > 0.0f: Failure \(if reachable\)

--
^warning: ignoring
12 changes: 12 additions & 0 deletions regression/goto-analyzer/constant_propagation_rounding_mode/main.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
#include <assert.h>

int main(void)
{
__CPROVER_rounding_mode = 0;
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Please don't use the numbers, use the C standard names for them FE_UPWARD and FE_DOWNWARD.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, but the values for them are implementation defined and I can't use fesetround because it doesn't have a visible implementation in goto-analyzer. I could add a couple of defines like #define FE_TONEAREST 0 though if you think that'd improve readability.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

fesetround should work so you can use the macros. Redefining them will likely cause problems.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

fesetround doesn't work for me; If I call it with anything all the __CPROVER variables just become top immediately. I believe @tautschnig mentioned the math library is disabled in goto-analyzer or something along those lines?

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This sounds like a bug that should be fixed rather than working around. There are a couple of possible causes:

  1. the libraries are not loaded in goto-analyze.
  2. they are but the domain is not handling them correctly.

IIRC --show-goto-program should be after program loading and thus make 1 obvious. --show should show the effect of analysis and so should identify 2.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@martin-cs So I've checked. If I add src/ansi-c/library/fenv.c to the mix I can indeed use fesetround, so the problem is that goto-analyzer isn't loading the libraries for some reason.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Do you get the same issue with both Makefile and CMake based builds? Probably goto-analyzer needs to link against the ansi-c library/dependency if it's not already doing so?

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It's pretty basic, I think: link_to_library(goto_model, ui_message_handler); is #if 0'ed.

float rounded_up = 1.0f / 10.0f;
__CPROVER_rounding_mode = 1;
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Names not numbers here!

float rounded_down = 1.0f / 10.0f;
assert(rounded_up - 0.1f >= 0);
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't know if this is intentional but this covers an awful lot of the C standard as it raises the question of what rounding mode is used for (compile time) constants!

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah yes. I don't believe the C standard requires a particular rounding mode to be used for constants folding (only reference I found to that was this in section 6.6 of the C99 draft standard:

If a floating
expression is evaluated in the translation environment, the arithmetic precision and range
shall be at least as great as if the expression were being evaluated in the execution
environment.

In gcc these exact examples won't work for this reason, because it folds the constants at compile time; Which can be worked around with -O0 by putting the division by ten in a function. In goto-analyzer we don't fold the constants before analysis, of course if we ever do these tests might break.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

OK. Can I suggest that you use the hex format if you mean a particular float.

0x1.99999ap-4f is the single precision float above / rounded up from the real value of 1 / 10.
0x1.999998p-4f is the one below.

assert(rounded_down - 0.1f < 0);
return 0;
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

assert(rounded_down == 0.1f || rounded_up == 0.1f)

Should be true!

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The literal 0.1f is in this case going to be the same as 1/10.0f rounded up because of how we treat literals, so 1/10.0f != 0.1f in this case.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes; my point is to document that one or the other is true.

}
9 changes: 9 additions & 0 deletions regression/goto-analyzer/constant_propagation_rounding_mode/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
CORE
main.c
--constants --verify
^EXIT=0$
^SIGNAL=0$
^\[main.assertion.1\] file main.c line 9 function main, assertion rounded_up - 0.1f >= 0: Success
^\[main.assertion.2\] file main.c line 10 function main, assertion rounded_down - 0.1f < 0: Success
--
^warning: ignoring
108 changes: 86 additions & 22 deletions src/analyses/constant_propagator.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,13 +16,17 @@ Author: Peter Schrammel
#include <util/format_expr.h>
#endif

#include <util/ieee_float.h>
#include <util/find_symbols.h>
#include <util/arith_tools.h>
#include <util/simplify_expr.h>
#include <util/cprover_prefix.h>

#include <langapi/language_util.h>

#include <algorithm>
#include <array>

void constant_propagator_domaint::assign_rec(
valuest &values,
const exprt &lhs,
Expand All @@ -35,8 +39,7 @@ void constant_propagator_domaint::assign_rec(
const symbol_exprt &s=to_symbol_expr(lhs);

exprt tmp=rhs;
values.replace_const(tmp);
simplify(tmp, ns);
partial_evaluate(tmp, ns);

if(tmp.is_constant())
values.set_to(s, tmp);
Expand Down Expand Up @@ -99,10 +102,10 @@ void constant_propagator_domaint::transform(
// Comparing iterators is safe as the target must be within the same list
// of instructions because this is a GOTO.
if(from->get_target()==to)
g=simplify_expr(from->guard, ns);
g = from->guard;
else
g=simplify_expr(not_exprt(from->guard), ns);

g = not_exprt(from->guard);
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

g could be assigned with a ternary if operator

partial_evaluate(g, ns);
if(g.is_false())
values.set_to_bottom();
else
Expand Down Expand Up @@ -269,10 +272,7 @@ bool constant_propagator_domaint::ai_simplify(
exprt &condition,
const namespacet &ns) const
{
bool b=values.replace_const.replace(condition);
b&=simplify(condition, ns);

return b;
return partial_evaluate(condition, ns);
}


Expand Down Expand Up @@ -504,6 +504,74 @@ bool constant_propagator_domaint::merge(
return values.merge(other.values);
}

/// Attempt to evaluate expression using domain knowledge
/// This function changes the expression that is passed into it.
/// \param expr The expression to evaluate
/// \param ns The namespace for symbols in the expression
/// \return True if the expression is unchanged, false otherwise
bool constant_propagator_domaint::partial_evaluate(
exprt &expr,
const namespacet &ns) const
{
// if the current rounding mode is top we can
// still get a non-top result by trying all rounding
// modes and checking if the results are all the same
if(!values.is_constant(symbol_exprt(ID_cprover_rounding_mode_str)))
{
return partial_evaluate_with_all_rounding_modes(expr, ns);
}
return replace_constants_and_simplify(expr, ns);
}

/// Attempt to evaluate an expression in all rounding modes.
///
/// If the result is the same for all rounding modes, change
/// expr to that result and return false. Otherwise, return true.
bool constant_propagator_domaint::partial_evaluate_with_all_rounding_modes(
exprt &expr,
const namespacet &ns) const
{ // NOLINTNEXTLINE (whitespace/braces)
auto rounding_modes = std::array<ieee_floatt::rounding_modet, 4>{
// NOLINTNEXTLINE (whitespace/braces)
{ieee_floatt::ROUND_TO_EVEN,
ieee_floatt::ROUND_TO_ZERO,
ieee_floatt::ROUND_TO_MINUS_INF,
// NOLINTNEXTLINE (whitespace/braces)
ieee_floatt::ROUND_TO_PLUS_INF}};
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I believe this to be correct... but is it optimal? I think that ROUND_TO_*_INF should be sufficient.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Not necessarily, an expression may involve various floating point subexpressions that react differently to different rounding modes - for example, you might have two subexpressions where ROUND_TO_ZERO might lead to one of them being rounded up because its negative and the other being rounded down because its positive.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes; fair point. Each individual operation is equal to either round up or down, but the whole operation may not be.

exprt first_result;
for(std::size_t i = 0; i < rounding_modes.size(); ++i)
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Worth commenting that this boils down to "if the result is the same in all rounding modes, return that; otherwise, report failure".

{
constant_propagator_domaint child(*this);
child.values.set_to(
ID_cprover_rounding_mode_str,
from_integer(rounding_modes[i], integer_typet()));
exprt result = expr;
if(child.replace_constants_and_simplify(result, ns))
{
return true;
}
else if(i == 0)
{
first_result = result;
}
else if(result != first_result)
{
return true;
}
}
expr = first_result;
return false;
}

bool constant_propagator_domaint::replace_constants_and_simplify(
exprt &expr,
const namespacet &ns) const
{
bool did_not_change_anything = values.replace_const.replace(expr);
did_not_change_anything &= simplify(expr, ns);
return did_not_change_anything;
}

void constant_propagator_ait::replace(
goto_functionst &goto_functions,
const namespacet &ns)
Expand All @@ -529,38 +597,34 @@ void constant_propagator_ait::replace(

if(it->is_goto() || it->is_assume() || it->is_assert())
{
s_it->second.values.replace_const(it->guard);
simplify(it->guard, ns);
s_it->second.partial_evaluate(it->guard, ns);
}
else if(it->is_assign())
{
exprt &rhs=to_code_assign(it->code).rhs();
s_it->second.values.replace_const(rhs);
simplify(rhs, ns);
s_it->second.partial_evaluate(rhs, ns);
if(rhs.id()==ID_constant)
rhs.add_source_location()=it->code.op0().source_location();
}
else if(it->is_function_call())
{
s_it->second.values.replace_const(
to_code_function_call(it->code).function());

simplify(to_code_function_call(it->code).function(), ns);
exprt &function = to_code_function_call(it->code).function();
s_it->second.partial_evaluate(function, ns);

exprt::operandst &args=
to_code_function_call(it->code).arguments();

for(exprt::operandst::iterator o_it=args.begin();
o_it!=args.end(); ++o_it)
for(auto &arg : args)
{
s_it->second.values.replace_const(*o_it);
simplify(*o_it, ns);
s_it->second.partial_evaluate(arg, ns);
}
}
else if(it->is_other())
{
if(it->code.get_statement()==ID_expression)
s_it->second.values.replace_const(it->code);
{
s_it->second.partial_evaluate(it->code, ns);
}
}
}
}
Expand Down
8 changes: 8 additions & 0 deletions src/analyses/constant_propagator.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -138,6 +138,8 @@ class constant_propagator_domaint:public ai_domain_baset

valuest values;

bool partial_evaluate(exprt &expr, const namespacet &ns) const;

protected:
void assign_rec(
valuest &values,
Expand All @@ -147,6 +149,12 @@ class constant_propagator_domaint:public ai_domain_baset
bool two_way_propagate_rec(
const exprt &expr,
const namespacet &ns);

bool partial_evaluate_with_all_rounding_modes(
exprt &expr,
const namespacet &ns) const;

bool replace_constants_and_simplify(exprt &expr, const namespacet &ns) const;
};

class constant_propagator_ait:public ait<constant_propagator_domaint>
Expand Down
2 changes: 1 addition & 1 deletion src/cbmc/cbmc_parse_options.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -26,6 +26,7 @@ Author: Daniel Kroening, [email protected]

#include <ansi-c/c_preprocess.h>

#include <goto-programs/adjust_float_expressions.h>
#include <goto-programs/initialize_goto_model.h>
#include <goto-programs/instrument_preconditions.h>
#include <goto-programs/goto_convert_functions.h>
Expand All @@ -49,7 +50,6 @@ Author: Daniel Kroening, [email protected]
#include <goto-programs/string_instrumentation.h>

#include <goto-symex/rewrite_union.h>
#include <goto-symex/adjust_float_expressions.h>

#include <goto-instrument/reachability_slicer.h>
#include <goto-instrument/full_slicer.h>
Expand Down
1 change: 0 additions & 1 deletion src/clobber/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,6 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
../assembler/assembler$(LIBEXT) \
../solvers/solvers$(LIBEXT) \
../util/util$(LIBEXT) \
../goto-symex/adjust_float_expressions$(OBJEXT) \
../goto-symex/rewrite_union$(OBJEXT) \
../pointer-analysis/dereference$(OBJEXT) \
../goto-instrument/dump_c$(OBJEXT) \
Expand Down
2 changes: 2 additions & 0 deletions src/goto-analyzer/goto_analyzer_parse_options.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -56,6 +56,7 @@ Author: Daniel Kroening, [email protected]
#include <util/exit_codes.h>

#include <cbmc/version.h>
#include <goto-programs/adjust_float_expressions.h>

#include "taint_analysis.h"
#include "unreachable_instructions.h"
Expand Down Expand Up @@ -477,6 +478,7 @@ int goto_analyzer_parse_optionst::doit()
/// Depending on the command line mode, run one of the analysis tasks
int goto_analyzer_parse_optionst::perform_analysis(const optionst &options)
{
adjust_float_expressions(goto_model);
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm not sure if it is best to do this here or in the evaluation. How does this work with simplify and dump-c?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm honestly not 100% sure how goto-analyzer works, but

#include <assert.h>
#include <fenv.h>

float div_by_ten(float x) {
  return x/10.0f;
}

int main(void)
{
  float f = 1.0f/10.0f;
  __CPROVER_rounding_mode = 1;
  float g = 1.0f/10.0f;
  assert(g < f);
  __CPROVER_rounding_mode = 3;
  float h = 1.0f/10.0f;
  assert(g == h);
  assert(h < f);
  __CPROVER_rounding_mode = 2;
  float i = 1.0f/10.0f;
  assert(f == i);
}

putting this into goto-analyzer --simplify followed by --dump-c gives me

Reading GOTO program from `test.out'
#include <assert.h>

// div_by_ten
// file test.c line 4
float div_by_ten(float x);

// div_by_ten
// file test.c line 4
float div_by_ten(float x)
{
  return FLOAT/(x, 10.0f, __CPROVER_rounding_mode);
}

// main
// file test.c line 8
signed int main(void)
{
  float f=0.1f;
  __CPROVER_rounding_mode = 1;
  float g=0.1f;
  /* assertion g < f */
  assert((_Bool)1);
  __CPROVER_rounding_mode = 3;
  float h=0.1f;
  /* assertion g == h */
  assert((_Bool)1);
  /* assertion h < f */
  assert((_Bool)1);
  __CPROVER_rounding_mode = 2;
  float i=0.1f;
  /* assertion f == i */
  assert((_Bool)1);
}

which should be correct.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The problem is that it has the (internal) rounded float exprs rather than the correct ones. Please adjust the float expressions during evaluation, not in the program.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Maybe @martin-cs will hate me for that, but ... how about a final cleanup step that removes all the internal ones? Much like is now done for remove_returns -> restore_returns.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The expression is already being modified during evaluation (substituting constants, calling simplify, etc.), so one more modification there won't hurt. Doing it up front requires changing it one way and then changing it back at the end.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ok, but I have to clearly admit that it was me pushing @hannes-steffenhagen-diffblue in this direction with the rationale that repeated modifications would seem costly. With the added learnings ever since I am happy to backtrack on this. My bad.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Also my apologies to @hannes-steffenhagen-diffblue for not being more present in this one.

if(options.get_bool_option("taint"))
{
std::string taint_file=cmdline.get_value("taint");
Expand Down
1 change: 0 additions & 1 deletion src/goto-diff/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -25,7 +25,6 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
../goto-instrument/cover_instrument_mcdc$(OBJEXT) \
../goto-instrument/cover_instrument_other$(OBJEXT) \
../goto-instrument/cover_util$(OBJEXT) \
../goto-symex/adjust_float_expressions$(OBJEXT) \
../goto-symex/rewrite_union$(OBJEXT) \
../analyses/analyses$(LIBEXT) \
../langapi/langapi$(LIBEXT) \
Expand Down
2 changes: 1 addition & 1 deletion src/goto-diff/goto_diff_parse_options.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -24,6 +24,7 @@ Author: Peter Schrammel

#include <langapi/language.h>

#include <goto-programs/adjust_float_expressions.h>
#include <goto-programs/goto_convert_functions.h>
#include <goto-programs/instrument_preconditions.h>
#include <goto-programs/mm_io.h>
Expand All @@ -45,7 +46,6 @@ Author: Peter Schrammel
#include <goto-programs/link_to_library.h>

#include <goto-symex/rewrite_union.h>
#include <goto-symex/adjust_float_expressions.h>

#include <goto-instrument/cover.h>

Expand Down
3 changes: 2 additions & 1 deletion src/goto-programs/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
SRC = basic_blocks.cpp \
SRC = adjust_float_expressions.cpp \
basic_blocks.cpp \
builtin_functions.cpp \
class_hierarchy.cpp \
class_identifier.cpp \
Expand Down
2 changes: 1 addition & 1 deletion src/goto-symex/adjust_float_expressions.cpp → ...oto-programs/adjust_float_expressions.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@ Author: Daniel Kroening, [email protected]
#include <util/ieee_float.h>
#include <util/arith_tools.h>

#include <goto-programs/goto_model.h>
#include "goto_model.h"

static bool have_to_adjust_float_expressions(
const exprt &expr,
Expand Down
6 changes: 3 additions & 3 deletions src/goto-symex/adjust_float_expressions.h → src/goto-programs/adjust_float_expressions.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,8 +9,8 @@ Author: Daniel Kroening, [email protected]
/// \file
/// Symbolic Execution

#ifndef CPROVER_GOTO_SYMEX_ADJUST_FLOAT_EXPRESSIONS_H
#define CPROVER_GOTO_SYMEX_ADJUST_FLOAT_EXPRESSIONS_H
#ifndef CPROVER_GOTO_PROGRAMS_ADJUST_FLOAT_EXPRESSIONS_H
#define CPROVER_GOTO_PROGRAMS_ADJUST_FLOAT_EXPRESSIONS_H

#include <goto-programs/goto_functions.h>

Expand All @@ -31,4 +31,4 @@ void adjust_float_expressions(
const namespacet &ns);
void adjust_float_expressions(goto_modelt &goto_model);

#endif // CPROVER_GOTO_SYMEX_ADJUST_FLOAT_EXPRESSIONS_H
#endif // CPROVER_GOTO_PROGRAMS_ADJUST_FLOAT_EXPRESSIONS_H
3 changes: 1 addition & 2 deletions src/goto-symex/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,4 @@
SRC = adjust_float_expressions.cpp \
auto_objects.cpp \
SRC = auto_objects.cpp \
build_goto_trace.cpp \
goto_symex.cpp \
goto_symex_state.cpp \
Expand Down
Loading