Skip to content

Refactoring code contracts implementation #6234

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 6 commits into from
Jul 20, 2021
Merged

Refactoring code contracts implementation #6234

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
260b0bf
Adds a memory predicate moddule in contracts
feliperodri Jul 16, 2021
cc604be
Adds missing case to assigns clause type checking
feliperodri Jul 16, 2021
e8777aa
Removes dead code from assigns clause implementation
feliperodri Jul 16, 2021
c2a5d79
Adds a assigns clause module in contracts
feliperodri Jul 16, 2021
58612c4
Refactoring frame-condition checks
feliperodri Jul 16, 2021
5d0ffe0
Adds a code contract module to goto-instrument
feliperodri Jul 16, 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
4 changes: 2 additions & 2 deletions CODEOWNERS
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -45,8 +45,8 @@
/src/goto-analyzer/ @martin-cs @chrisr-diffblue @peterschrammel
/src/goto-harness/ @martin-cs @chrisr-diffblue @peterschrammel
/src/goto-instrument/ @martin-cs @chrisr-diffblue @peterschrammel
/src/goto-instrument/code_contracts.* @tautschnig @feliperodri @SaswatPadhi
doc/cprover-manual/contracts* @tautschnig @feliperodri @SaswatPadhi
/src/goto-instrument/contracts/ @tautschnig @feliperodri @SaswatPadhi
/doc/cprover-manual/contracts* @tautschnig @feliperodri @SaswatPadhi
/src/goto-diff/ @tautschnig @peterschrammel
/src/jsil/ @kroening @tautschnig
/src/memory-analyzer/ @tautschnig @chrisr-diffblue
Expand Down
4 changes: 2 additions & 2 deletions regression/contracts/assigns_replace_06/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,9 +1,9 @@
CORE
main.c
--replace-all-calls-with-contracts
^EXIT=0$
^EXIT=10$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
^VERIFICATION FAILED$
--
--
Checks whether the values outside the array range specified by the assigns
Expand Down
8 changes: 7 additions & 1 deletion regression/contracts/assigns_type_checking_valid_cases/main.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,10 +3,15 @@
int *x;
int y;

struct blob
{
int allocated;
};
struct buf
{
int *data;
size_t len;
struct blob aux;
};

void foo1(int a) __CPROVER_assigns(a)
Expand Down Expand Up @@ -76,9 +81,10 @@ void foo9(int array[]) __CPROVER_assigns(array)
}

void foo10(struct buf *buffer) __CPROVER_requires(buffer != NULL)
__CPROVER_assigns(*buffer)
__CPROVER_assigns(buffer->len, buffer->aux.allocated)
{
buffer->len = 0;
buffer->aux.allocated = 0;
}

int main()
Expand Down
2 changes: 1 addition & 1 deletion src/ansi-c/ansi_c_convert_type.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -257,7 +257,7 @@ void ansi_c_convert_typet::read_rec(const typet &type)
{
if(
operand.id() != ID_symbol && operand.id() != ID_ptrmember &&
operand.id() != ID_dereference)
operand.id() != ID_member && operand.id() != ID_dereference)
{
error().source_location = source_location;
error() << "illegal target in assigns clause" << eom;
Expand Down
4 changes: 3 additions & 1 deletion src/goto-instrument/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,9 @@ SRC = accelerate/accelerate.cpp \
alignment_checks.cpp \
branch.cpp \
call_sequences.cpp \
code_contracts.cpp \
contracts/assigns.cpp \
contracts/memory_predicates.cpp \
contracts/contracts.cpp \
concurrency.cpp \
count_eloc.cpp \
cover.cpp \
Expand Down
Loading