Skip to content

SV-COMP fixes #157

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

Merged
merged 14 commits into from
Jan 17, 2022
Merged

SV-COMP fixes #157

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
14 commits
Select commit Hold shift + click to select a range
deceb82
Update CBMC prerequisites
viktormalik Oct 11, 2021
6318811
Fix dynobj_instance_analysis
viktormalik Oct 8, 2021
eff6f0f
Workaround problem with GOTO targets
viktormalik Oct 8, 2021
c88cdd7
SSA: drop conditional update of dynamic objects
viktormalik Oct 8, 2021
090c38d
Correctly add allocation guards
FrNecas Oct 10, 2021
bc5b1da
Heap: improve obtaining pointed object from solver
viktormalik Oct 11, 2021
646ac5d
Fix collection of free::record vars
viktormalik Oct 11, 2021
25f05f5
malloc: fix getting malloc size
viktormalik Oct 14, 2021
5a63242
Fix assert to limit array size
viktormalik Oct 18, 2021
2c45caf
Disable unsupported operations in competition mode
viktormalik Oct 18, 2021
11606bc
Configure gcc preprocessing to fix linking
FrNecas Oct 20, 2021
12cc730
Correctly guard hoisted assertions
FrNecas Oct 22, 2021
3f21ab9
Fix workaround for signed shl
FrNecas Oct 23, 2021
9071c90
Propagate #concrete for byte-array dynamic objs
viktormalik Oct 24, 2021
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
13 changes: 13 additions & 0 deletions src/ssa/local_ssa.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -51,6 +51,9 @@ void local_SSAt::build_SSA()
build_function_call(i_it);
// build_unknown_objs(i_it);
collect_record_frees(i_it);

if (options.get_bool_option("competition-mode"))
disable_unsupported_instructions(i_it);
}

// collect custom templates in loop heads
Expand Down Expand Up @@ -1644,3 +1647,13 @@ bool local_SSAt::can_reuse_symderef(

return true;
}

void local_SSAt::disable_unsupported_instructions(locationt loc)
{
if (loc->is_other())
{
auto st = loc->get_code().get_statement();
if(st=="array_copy" || st=="array_replace")
Copy link
Contributor

@FrNecas FrNecas Jan 14, 2022

Choose a reason for hiding this comment

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

Perhaps we could file an issue for support of memcpy?

Copy link
Collaborator Author

@viktormalik viktormalik Jan 14, 2022

Choose a reason for hiding this comment

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

Done: #160.

assert(false);
}
}
3 changes: 3 additions & 0 deletions src/ssa/local_ssa.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -271,6 +271,9 @@ class local_SSAt
void build_assertions(locationt loc);
void build_unknown_objs(locationt loc);

// competition-mode specific checks
void disable_unsupported_instructions(locationt loc);

void collect_allocation_guards(const code_assignt &assign, locationt loc);
void get_alloc_guard_rec(const exprt &expr, exprt old_guard);
void collect_record_frees(locationt loc);
Expand Down