Skip to content

Commit e0da7e7

Browse files
committed
parsing, type checking & conversion of loop assigns clauses
In this commit we implement the parsing actions, type checking and conversion routines for assigns clauses on loops. The syntax rules along with regressions tests were introduced in an earlier PR: #6196.
1 parent 2499f8a commit e0da7e7

File tree

13 files changed

+84
-42
lines changed

13 files changed

+84
-42
lines changed

regression/contracts/assigns_enforce_address_of/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ main.c
33
--enforce-contract foo
44
^EXIT=(1|64)$
55
^SIGNAL=0$
6-
^.*error: illegal target in assigns clause$
6+
^.*error: non-lvalue target in assigns clause$
77
^CONVERSION ERROR$
88
--
99
--

regression/contracts/assigns_enforce_elvis_4/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ main.c
33
--enforce-contract foo
44
^EXIT=(1|64)$
55
^SIGNAL=0$
6-
^.*error: void-typed targets not permitted$
6+
^.*error: void-typed targets not permitted in assigns clause$
77
--
88
--
99
Check that Elvis operator expressions '*(cond ? if_true : if_false)' with different types in true and false branches are rejected.

regression/contracts/assigns_enforce_function_calls/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ main.c
33
--enforce-contract foo
44
^EXIT=(1|64)$
55
^SIGNAL=0$
6-
^.*error: illegal target in assigns clause$
6+
^.*error: non-lvalue target in assigns clause$
77
^CONVERSION ERROR$
88
--
99
--

regression/contracts/assigns_enforce_literal/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ main.c
33
--enforce-contract foo
44
^EXIT=(1|64)$
55
^SIGNAL=0$
6-
^.*error: illegal target in assigns clause$
6+
^.*error: non-lvalue target in assigns clause$
77
^CONVERSION ERROR$
88
--
99
--

regression/contracts/assigns_enforce_side_effects_1/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ main.c
33
--enforce-contract foo
44
^EXIT=(1|64)$
55
^SIGNAL=0$
6-
^.*error: void-typed targets not permitted$
6+
^.*error: void-typed targets not permitted in assigns clause$
77
^CONVERSION ERROR$
88
--
99
--

regression/contracts/assigns_enforce_side_effects_2/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ main.c
33
--enforce-contract foo
44
^EXIT=(1|64)$
55
^SIGNAL=0$
6-
^.*error: illegal target in assigns clause$
6+
^.*error: non-lvalue target in assigns clause$
77
^CONVERSION ERROR$
88
--
99
--

regression/contracts/assigns_enforce_side_effects_3/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ main.c
33
--enforce-contract foo
44
^EXIT=(1|64)$
55
^SIGNAL=0$
6-
^.*error: illegal target in assigns clause$
6+
^.*error: non-lvalue target in assigns clause$
77
^CONVERSION ERROR$
88
--
99
--

regression/contracts/assigns_type_checking_invalid_case_01/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,6 @@ main.c
44
^EXIT=(1|64)$
55
^SIGNAL=0$
66
^CONVERSION ERROR$
7-
error: illegal target in assigns clause
7+
error: non-lvalue target in assigns clause
88
--
99
Checks whether type checking reports illegal target in assigns clause.

src/ansi-c/c_typecheck_base.cpp

Lines changed: 1 addition & 27 deletions
Original file line numberDiff line numberDiff line change
@@ -739,33 +739,7 @@ void c_typecheck_baset::typecheck_declaration(
739739
CPROVER_PREFIX "loop_entry is not allowed in preconditions.");
740740
}
741741

742-
for(auto &target : code_type.assigns())
743-
{
744-
typecheck_expr(target);
745-
746-
if(target.type().id() == ID_empty)
747-
{
748-
error().source_location = target.source_location();
749-
error() << "void-typed targets not permitted" << eom;
750-
throw 0;
751-
}
752-
else if(target.id() == ID_pointer_object)
753-
{
754-
// skip
755-
}
756-
else if(!target.get_bool(ID_C_lvalue))
757-
{
758-
error().source_location = target.source_location();
759-
error() << "illegal target in assigns clause" << eom;
760-
throw 0;
761-
}
762-
else if(has_subexpr(target, ID_side_effect))
763-
{
764-
error().source_location = target.source_location();
765-
error() << "assigns clause is not side-effect free" << eom;
766-
throw 0;
767-
}
768-
}
742+
typecheck_spec_assigns(code_type.assigns());
769743

770744
if(!as_const(code_type).ensures().empty())
771745
{

src/ansi-c/c_typecheck_base.h

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -144,6 +144,9 @@ class c_typecheck_baset:
144144
virtual void typecheck_while(code_whilet &code);
145145
virtual void typecheck_dowhile(code_dowhilet &code);
146146
virtual void typecheck_start_thread(codet &code);
147+
148+
// contracts
149+
virtual void typecheck_spec_assigns(exprt::operandst &targets);
147150
virtual void typecheck_spec_loop_invariant(codet &code);
148151
virtual void typecheck_spec_decreases(codet &code);
149152

0 commit comments

Comments
 (0)