-
Notifications
You must be signed in to change notification settings - Fork 259
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Move __CPROVER_uninterpreted_* conversion to C type checker
We already had type checking of mathematical_function types to support lambda expressions. Special-case symbols with name `__CPROVER_uninterpreted_*` will now also produce these types. GOTO conversion will no longer give specific treatment to function calls with symbol name `__CPROVER_uninterpreted_*`.
- Loading branch information
1 parent
8aee75f
commit 2c13d82
Showing
6 changed files
with
79 additions
and
40 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
28 changes: 28 additions & 0 deletions
28
regression/contracts-dfcc/quantifiers-uninterpreted-function/main.c
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,28 @@ | ||
#include <ctype.h> | ||
|
||
int __CPROVER_uninterpreted_tolower(int); | ||
|
||
// clang-format off | ||
void tl1(char *dst, __CPROVER_size_t len) | ||
__CPROVER_requires(__CPROVER_is_fresh(dst, len)) | ||
__CPROVER_assigns(__CPROVER_object_whole(dst)) | ||
__CPROVER_ensures(__CPROVER_forall { | ||
int i; | ||
(0 <= i && i < len) ==> dst[i % len] == | ||
__CPROVER_uninterpreted_tolower(__CPROVER_old(dst[i % len])) | ||
}); | ||
// clang-format on | ||
|
||
void tl1(char *dst, __CPROVER_size_t len) | ||
{ | ||
for(__CPROVER_size_t i = 0; i < len; i++) | ||
{ | ||
dst[i] = tolower(dst[i]); | ||
} | ||
} | ||
|
||
int main() | ||
{ | ||
char st[8] = "HELLOROD"; | ||
tl1(st, 8); | ||
} |
13 changes: 13 additions & 0 deletions
13
regression/contracts-dfcc/quantifiers-uninterpreted-function/test.desc
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,13 @@ | ||
CORE dfcc-only | ||
main.c | ||
--dfcc main --enforce-contract tl1 | ||
^\[tl1.postcondition.1\] line \d+ Check ensures clause of contract contract::tl1 for function tl1: FAILURE$ | ||
^\*\* 1 of \d+ failed | ||
^VERIFICATION FAILED$ | ||
^EXIT=10$ | ||
^SIGNAL=0$ | ||
-- | ||
^warning: ignoring | ||
-- | ||
The purpose of this test is to ensure that we can use uninterpreted functions | ||
within quantifiers. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters