Skip to content

Commit f75d1e0

Browse files
committed
Fixed CEGIS control benchmark 2
CEGIS control benchmark 2 was not working anymore due to a bug introduced in the meta variable detection with the new control back-end. Fixed this bug.
1 parent 91257d1 commit f75d1e0

File tree

3 files changed

+13
-9
lines changed

3 files changed

+13
-9
lines changed

src/cegis/cegis-util/program_helper.cpp

+4-2
Original file line numberDiff line numberDiff line change
@@ -348,8 +348,10 @@ goto_programt::targett insert_after_preserving_source_location(
348348
goto_programt::targett insert_before_preserving_source_location(
349349
goto_programt &body, goto_programt::targett pos)
350350
{
351-
typedef goto_programt::targett(goto_programt::*ftype)(goto_programt::targett);
352-
const auto op=std::bind1st(std::mem_fun(static_cast<ftype>(&goto_programt::insert_before)), &body);
351+
typedef goto_programt::targett (goto_programt::*ftype)(
352+
goto_programt::targett);
353+
const auto op=std::bind1st(
354+
std::mem_fun(static_cast<ftype>(&goto_programt::insert_before)), &body);
353355
return insert_preserving_source_location(pos, op);
354356
}
355357

src/cegis/control/learn/rational_solution_configuration.cpp

+2-3
Original file line numberDiff line numberDiff line change
@@ -30,9 +30,8 @@ const struct_exprt &find_solution(const goto_tracet &trace)
3030
}
3131
}
3232

33-
void rational_solution_configurationt::convert(
34-
solutiont &current_candidate, const goto_tracet &trace,
35-
const symbol_tablet &st)
33+
void rational_solution_configurationt::convert(solutiont &current_candidate,
34+
const goto_tracet &trace, const symbol_tablet &st)
3635
{
3736
const struct_exprt &solution=find_solution(trace);
3837
const namespacet ns(st);

src/cegis/control/preprocessing/control_preprocessing.cpp

+7-4
Original file line numberDiff line numberDiff line change
@@ -11,12 +11,12 @@
1111
#include <cegis/control/preprocessing/control_preprocessing.h>
1212
#include <goto-programs/remove_returns.h>
1313

14+
#define TMP_MARKER "$tmp"
15+
1416
// XXX: Debug
1517
#include <iostream>
1618
// XXX: Debug
1719

18-
#define TMP_MARKER "$tmp"
19-
2020
control_preprocessingt::control_preprocessingt(const symbol_tablet &st,
2121
const goto_functionst &gf) :
2222
control_program(st, gf)
@@ -39,8 +39,11 @@ bool is_meta(const goto_programt::const_targett pos)
3939
const std::string &func=id2string(loc.get_function());
4040
for (const char * const excluded : excluded_functions)
4141
if (contains(func, excluded)) return true;
42-
if (goto_program_instruction_typet::ASSIGN != pos->type
43-
&& goto_program_instruction_typet::DECL != pos->type) return false;
42+
if ((goto_program_instruction_typet::ASSIGN != pos->type
43+
&& goto_program_instruction_typet::DECL != pos->type)
44+
|| !pos->code.has_operands()
45+
|| (pos->code.has_operands() && ID_symbol != pos->code.op0().id()))
46+
return false;
4447
const std::string &var=id2string(get_affected_variable(*pos));
4548
if (contains(var, TMP_MARKER) || contains(var, RETURN_VALUE_SUFFIX)
4649
|| contains(var, CPROVER_PREFIX)) return true;

0 commit comments

Comments
 (0)